lambda lift for solvers

Author: philzook58

src/kdrag/solvers/__init__.py

@@ -126,15 +126,21 @@ class BaseSolver:
     def __init__(self):
         self.adds = []
         self.assert_tracks = []
-        self.options = {}
+        self.options: dict = {"lambda_lift": True}
         self.res: Optional[subprocess.CompletedProcess] = None
 
     def add(self, thm: smt.BoolRef):
         if isinstance(thm, list):
-            self.adds.extend(thm)
-            return
+            for t in thm:
+                self.add(t)
         else:
             assert isinstance(thm, smt.BoolRef)
+            if self.options["lambda_lift"]:
+                thm1 = kd.utils.curry_arrays(thm)
+                thm1, extra = kd.utils.lambda_lift(thm1)
+                assert isinstance(thm1, smt.BoolRef)
+                thm = thm1
+                self.adds.extend(extra)
             self.adds.append(thm)
 
     def assert_and_track(self, thm: smt.BoolRef, name: str):
@@ -200,15 +206,15 @@ def write_tptp(self, filename, format="thf"):
                     if f not in predefined and f.name() not in predefined_names:
                         if f.arity() == 0:
                             fp.write(
-                                f"{format}({f.name()}_type, type, {f.name() if f in no_mangle else mangle_decl(f)} : {sort_to_tptp(f.range())} ).\n"
+                                f"{format}({f.name().replace('!', '__')}_type, type, {f.name().replace('!', '__') if f in no_mangle else mangle_decl(f)} : {sort_to_tptp(f.range())} ).\n"
                             )
                         else:
                             joiner = " > " if format == "thf" else " * "
                             dom_tptp = joiner.join(
                                 [sort_to_tptp(f.domain(i)) for i in range(f.arity())]
                             )
                             fp.write(
-                                f"{format}({f.name()}_decl, type, {f.name() if f in no_mangle else mangle_decl(f)} : {dom_tptp} > {sort_to_tptp(f.range())}).\n"
+                                f"{format}({f.name().replace('!', '__')}_decl, type, {f.name().replace('!', '__') if f in no_mangle else mangle_decl(f)} : {dom_tptp} > {sort_to_tptp(f.range())}).\n"
                             )
 
             # Write axioms and assertions in TPTP THF format
@@ -240,11 +246,10 @@ def check_tptp_status(self, res):
 
     def write_smt(self, fp):
         fp.write("(set-logic ALL)\n")
+        thms = self.adds + [thm for thm, name in self.assert_tracks]
         # Gather up all datatypes referenced
         predefined = set()
-        for sort in collect_sorts(
-            self.adds + [thm for thm, name in self.assert_tracks]
-        ):
+        for sort in collect_sorts(thms):
             if isinstance(sort, smt.DatatypeSortRef):
                 fp.write(smtlib_datatypes([sort]))
                 for i in range(sort.num_constructors()):
@@ -258,16 +263,17 @@ def write_smt(self, fp):
                 fp.write(f"(declare-sort {sort.name()} 0)\n")
         # Declare all function symbols
         fp.write(";;declarations\n")
-        for f in collect_decls(self.adds + [thm for thm, name in self.assert_tracks]):
+        for f in collect_decls(thms):
             if f not in predefined and f.name() not in predefined_names:
                 fp.write(funcdecl_smtlib(f))
                 fp.write("\n")
         fp.write(";;axioms\n")
-        for e in self.adds:
+        # TODO: Add back assert tracking
+        for e in thms:  # self.adds:
             # We can't use e.sexpr() because we need to mangle overloaded names
             fp.write("(assert " + expr_to_smtlib(e) + ")\n")
-        for thm, name in self.assert_tracks:
-            fp.write("(assert (! " + expr_to_smtlib(thm) + " :named " + name + "))\n")
+        # for thm, name in self.assert_tracks:
+        #    fp.write("(assert (! " + expr_to_smtlib(thm) + " :named " + name + "))\n")
 
 
 def collect_sorts(exprs) -> set[smt.SortRef]:
@@ -454,13 +460,12 @@ def check(self):
         return self.check_tptp_status(self.res.stdout)
 
 
-"""
 class EProverSolver(BaseSolver):
     def __init__(self):
-        new = download(
+        download(
             "https://github.com/philzook58/eprover/releases/download/E.3.2.5-ho/eprover-ho",
             "eprover-ho",
-            "56a1dd51be0ba3194851cfb6f4ecc563c82cd5e2f5009dd1a7268af91150c9cd",
+            "840170d1cb80cc3796b0f209e5879d23d1a19577fd922d84029c30783687b2c6",
         )
         super().__init__()
         self.options["format"] = "tff"
@@ -479,7 +484,6 @@ def check(self):
         if len(self.res.stderr) > 0:
             raise Exception("Eprover error", self.res.stderr)
         return self.check_tptp_status(self.res.stdout)
-"""
 
 
 class EProverTHFSolver(BaseSolver):

src/kdrag/solvers/sat.py

@@ -481,12 +481,12 @@ def lambda_lift(expr: smt.ExprRef) -> tuple[smt.ExprRef, list[smt.BoolRef]]:
     >>> lambda_lift(smt.ForAll([x,y], smt.Exists([z], x + y + 1 == smt.Lambda([z], x)[z])))
     (ForAll([x, y], Exists(z, x + y + 1 == f!...(x, y)[z])), [ForAll([x, y, z], f!...(x, y)[z] == x)])
     """
-    lift_defs = []
+    lift_defs: list[smt.BoolRef] = []
 
     def worker(expr, env):
         if isinstance(expr, smt.QuantifierRef):
             vs, body = kd.utils.open_binder_unhygienic(expr)
-            env = [v for v in env if v not in vs]  # shadowing
+            env = [v for v in env if not any(v.eq(v1) for v1 in vs)]  # shadowing
             env1 = env + vs
             if expr.is_lambda():
                 f = smt.FreshFunction(*[v.sort() for v in env], expr.sort())
@@ -496,18 +496,71 @@ def worker(expr, env):
                 return smt.ForAll(vs, worker(body, env1))
             elif expr.is_exists():
                 return smt.Exists(vs, worker(body, env1))
+            else:
+                raise NotImplementedError("Unknown quantifier type", expr)
         elif smt.is_const(expr):
             return expr
-        if smt.is_app(expr):
+        elif smt.is_app(expr):
             args = [worker(arg, env) for arg in expr.children()]
             return expr.decl()(*args)
         else:
-            return expr
+            raise Exception("Unexpected term in lambda_lift", expr)
 
     env = []
     return worker(expr, env), lift_defs
 
 
+def curry_arrays(e: smt.ExprRef) -> smt.ExprRef:
+    """
+    Curry all selects and lambdas into single argument versions.
+    >>> f = smt.Array("f", smt.IntSort(), smt.RealSort(), smt.BoolSort())
+    >>> curry_arrays(smt.Select(f, smt.IntVal(3), smt.RealVal(2.0)))
+    f[3][2]
+    >>> x,y,z = smt.Ints("x y z")
+    >>> curry_arrays(smt.Lambda([x,y], x + y)[2,3])
+    Lambda(x, Lambda(y, x + y))[2][3]
+    """
+    # TODO  Possibility of clashing names here.
+    # If you have the same name for the curried version you're nuts though.
+    if isinstance(e, smt.QuantifierRef):
+        vs, body = open_binder_unhygienic(e)
+        body = curry_arrays(body)
+        if e.is_lambda():
+            for v in reversed(vs):
+                body = smt.Lambda([v], body)
+            return body
+        elif e.is_forall():
+            return smt.ForAll(vs, body)
+        elif e.is_exists():
+            return smt.Exists(vs, body)
+        else:
+            raise NotImplementedError("Unknown quantifier type", e)
+    elif smt.is_const(e):
+        if isinstance(e, smt.ArrayRef):
+            doms = smt.domains(e)
+            if len(doms) == 1:
+                return e
+            else:
+                sort = e.range()
+                for d in reversed(doms):
+                    sort = smt.ArraySort(d, sort)
+                return smt.Const(e.decl().name(), sort)
+        else:
+            return e
+    elif smt.is_app(e):
+        f, children = e.decl(), e.children()
+        children = [curry_arrays(c) for c in children]
+        if smt.is_select(e):
+            arr = children[0]
+            for index in children[1:]:
+                arr = smt.Select(arr, index)
+            return arr
+        else:
+            return f(*children)
+    else:
+        raise Exception("Unexpected term in curry_arrays", e)
+
+
 def generate(sort: smt.SortRef, pred=None) -> Generator[smt.ExprRef, None, None]:
     """
     A generator of values for a sort. Repeatedly calls z3 to get a new value.

src/kdrag/utils.py

@@ -8,6 +8,8 @@
     TweeSolver,
     SATSolver,
     LeanSolver,
+    EProverSolver,
+    VampireSolver
 )
 import kdrag.solvers as solvers
 import kdrag.smt as smt
@@ -19,6 +21,15 @@
 import kdrag.solvers.kb as kb
 import kdrag.rewrite as rw
 
+@pytest.mark.slow
+def test_eprover():
+    s = EProverSolver()
+    a,b,c = smt.Bools("a b c")
+    s.add(smt.And(a,b))
+    assert s.check() == smt.sat
+    s.add(smt.Not(a))
+    assert s.check() == smt.unsat
+
 @pytest.mark.slow
 def test_vampirethf():
     s = VampireTHFSolver()
@@ -46,9 +57,11 @@ def test_vampirethf():
     s.add(f == g)
     s.add(smt.Not(smt.ForAll([x], (f(x) == g(x)))))
     assert s.check() == smt.unsat
-
+    """
+    
+    """
     x, y, z = smt.Reals("x y z")
-    s = VampireTHFSolver()
+    s = VampireSolver()
     s.add(x + y == z)
     s.add(x == y)
     assert s.check() == smt.sat
@@ -59,12 +72,13 @@ def test_vampirethf():
     x, y, z = smt.Consts("x y z", S)
     f, g = smt.Consts("f g", S >> T)
 
-    """
+
     s = VampireTHFSolver()
     s.add(f == g)
     s.add(smt.Not(smt.ForAll([x], (f(x) == g(x)))))
     assert s.check() == smt.unsat
-    """
+
+
     s = EProverTHFSolver()
     s.add(f == g)
     s.add(smt.Not(smt.ForAll([x], (f(x) == g(x)))))
@@ -112,13 +126,23 @@ def test_vampirethf():
     f = smt.Const("f", smt.BoolSort() >> smt.BoolSort())
     p, q = smt.Bools("p q")
 
+    s = EProverTHFSolver()
+    s.set("lambda_lift", False)
+    s.add(smt.Not(smt.ForAll(
+            [p],
+            p == (smt.Lambda([f], f(p)) == smt.Lambda([f], f(smt.BoolVal(True)))),
+        )))
+    assert s.check() == smt.unsat
+    """
+    # lambda lifting makes this come back unknown
     kd.kernel.prove(
         smt.ForAll(
             [p],
             p == (smt.Lambda([f], f(p)) == smt.Lambda([f], f(smt.BoolVal(True)))),
         ),
         solver=EProverTHFSolver,
     )
+    """
 
     s = TweeSolver()
     x, y, z = smt.Consts("x y z", S)