Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
33 lines (28 sloc) 1.03 KB
#script (python)
import clingo
def get(val, default):
return val if val != None else default
def main(prg):
imin = get(prg.get_const("imin"), clingo.Number(0))
imax = prg.get_const("imax")
istop = get(prg.get_const("istop"), clingo.String("SAT"))
step, ret = 0, None
while ((imax is None or step < imax.number) and
(step == 0 or step < imin.number or (
(istop.string == "SAT" and not ret.satisfiable) or
(istop.string == "UNSAT" and not ret.unsatisfiable) or
(istop.string == "UNKNOWN" and not ret.unknown)))):
parts = []
parts.append(("check", [step]))
if step > 0:
prg.release_external(clingo.Function("query", [step-1]))
parts.append(("step", [step]))
prg.cleanup()
else:
parts.append(("base", []))
prg.ground(parts)
prg.assign_external(clingo.Function("query", [step]), True)
ret, step = prg.solve(), step+1
#end.
#program check(t).
#external query(t).
You can’t perform that action at this time.