qexists bug. install gappa. matmul

kdrag/notation.py

@@ -64,6 +64,9 @@ def define(self, args, body):
 rmul = SortDispatch(name="rmul")
 smt.ExprRef.__rmul__ = lambda x, y: rmul(x, y)
 
+matmul = SortDispatch(name="matmul")
+smt.ExprRef.__matmul__ = lambda x, y: matmul(x, y)
+
 neg = SortDispatch(name="neg")
 smt.ExprRef.__neg__ = lambda x: neg(x)
 
@@ -122,9 +125,9 @@ def QExists(vs: list[smt.ExprRef], *concs) -> smt.BoolRef:
     """
     concs = [v.wf() for v in vs if v.sort() in wf.methods] + list(concs)
     if len(concs) == 1:
-        smt.Exists(vars, concs[0])
+        smt.Exists(vs, concs[0])
     else:
-        smt.Exists(vars, smt.And(concs))
+        smt.Exists(vs, smt.And(concs))
 
 
 def ExistsUnique(v: smt.ExprRef, *concs) -> smt.BoolRef:

kdrag/solvers/.gitignore

@@ -10,4 +10,6 @@ nanoCoP-i20.tar.gz
 nanoCoP-i20/
 Prover9/
 kissat/
-kissat
+kissat
+gappa-1.4.2/
+gappa-1.4.2.tar.gz

kdrag/solvers/__init__.py

@@ -5,6 +5,7 @@
 import concurrent.futures
 import logging
 import shutil
+import re
 
 logger = logging.getLogger("knuckledragger")
 
@@ -262,7 +263,10 @@ def check(self):
                 "--mode",
                 "smtcomp",
                 "--input_syntax",
-                "smtlib2",  # "--ignore_unrecognized_logic", "on",
+                "smtlib2",
+                # "--ignore_unrecognized_logic", "on",
+                # "--proof_extra" "fast" / "full"
+                # "--latex_output" "/tmp/vampire.tex"
             ]
             if "timeout" in self.options:
                 cmd.extend(["-t", str(self.options["timeout"] // 100) + "d"])
@@ -300,7 +304,7 @@ def query(self, q):
                 "--mode",
                 "casc",
                 "--question_answering",
-                "synthesis",
+                "synthesis",  # "answer_literal"
                 "--proof",
                 "off",
                 "--input_syntax",
@@ -329,6 +333,15 @@ def unsat_core(self):
         cores = [smt.Bool(core) for core in cores]
         return cores
 
+    def proof(self):
+        res = []
+        # https://github.com/teorth/equational_theories/blob/main/equational_theories/Generated/VampireProven/src/vampire_proofs_cyc.py
+        for eqnum, statement, reason in re.findall(
+            r"(\d+)\. ([^[]+) \[([^\]]+)\]", self.res.stdout.decode()
+        ):
+            res.append((int(eqnum), statement, reason))  # TODO: Deeper parsing
+        return res
+
 
 class VampireTHFSolver(BaseSolver):
     def __init__(self):

kdrag/solvers/install.sh

@@ -55,4 +55,10 @@ echo "Installing Kissat"
 git -C kissat pull || git clone https://github.com/arminbiere/kissat.git --depth 1
 cd kissat
 ./configure && make test
-cd ..
+cd ..
+
+echo "Installing Gappa"
+wget -nc https://gappa.gitlabpages.inria.fr/releases/gappa-1.4.2.tar.gz
+tar -xzf gappa-1.4.2.tar.gz
+cd gappa-1.4.2
+./configure && ./remake