Switch to accepting lambd as horizon parameter, grounding until it is hit.

Author: namcsi

telingo/__init__.py

@@ -21,7 +21,7 @@
 from . import theory as _ty
 
 
-def imain(prg, future_sigs, program_parts, on_model, imin=0, imax=None, istop="SAT"):
+def imain(prg, future_sigs, program_parts, on_model, imin=0, imax=None, lambd=0, istop="SAT"):
     """
     Take a program object and runs the incremental main solving loop.
 
@@ -46,15 +46,12 @@ def imain(prg, future_sigs, program_parts, on_model, imin=0, imax=None, istop="S
     program_parts -- Program parts to ground.
     imin          -- Minimum number of iterations.
     imax          -- Maximum number of iterations.
+    lambd        -- Number of steps to ground, then solve a single time (non-iterative)
     istop         -- When to stop.
     """
     thy = _ty.Theory()
     step, ret = 0, None
-    while ((imax is None or step < imax) and
-           (step == 0 or step < imin or (
-               (istop == "SAT" and not ret.satisfiable) or
-               (istop == "UNSAT" and not ret.unsatisfiable) or
-               (istop == "UNKNOWN" and not ret.unknown)))):
+    while True:
         parts = []
         for root_name, part_name, rng in program_parts:
             for i in rng:
@@ -73,7 +70,11 @@ def imain(prg, future_sigs, program_parts, on_model, imin=0, imax=None, istop="S
             for atom in prg.symbolic_atoms.by_signature(name, arity, positive):
                 if atom.symbol.arguments[-1].number > step:
                     assumptions.append(-atom.literal)
-        ret, step = prg.solve(on_model=lambda m: on_model(m, step), assumptions=assumptions), step+1
+        if step < lambd:
+            step += 1
+            continue
+        prg.solve(on_model=lambda m: on_model(m, step), assumptions=assumptions)
+        break
 
 
 class TelApp(Application):
@@ -95,6 +96,7 @@ def __init__(self):
         self.__imin = 0
         self.__imax = None
         self.__istop = "SAT"
+        self.__lambd = 0
         self.__horizon = 0
 
     def __on_model(self, model, horizon):
@@ -125,6 +127,16 @@ def __parse_imax(self, value):
         self.__imax = None
         return True
 
+    def __parse_lambd(self, value):
+        """
+        Parse lambd argument.
+        """
+        if len(value) > 0:
+            self.__lambd = int(value)
+            return self.__lambd >= 0
+        self.__lambd = None
+        return True
+
     def __parse_istop(self, value):
         """
         Parse istop argument.
@@ -157,6 +169,7 @@ def register_options(self, options):
         group = "Telingo Options"
         options.add(group, "imin", "Minimum number of solving steps [0]", self.__parse_imin, argument="<n>")
         options.add(group, "imax", "Maximum number of solving steps []", self.__parse_imax, argument="<n>")
+        options.add(group, "lambd", "Initial number of steps ground before single solve []", self.__parse_lambd, argument="<n>")
         options.add(group, "istop", dedent("""\
             Stop criterion [sat]
                   <arg>: {sat|unsat|unknown}"""), self.__parse_istop)
@@ -174,7 +187,7 @@ def main(self, control, files):
                 files.append(sys.stdin)
             future_sigs, program_parts = _tf.transform([path.read() for path in files], bld.add)
 
-        imain(control, future_sigs, program_parts, self.__on_model, self.__imin, self.__imax, self.__istop)
+        imain(control, future_sigs, program_parts, self.__on_model, self.__imin, self.__imax, self.__lambd, self.__istop)
 
 
 def main():