added proof to base solver

philzook58 · Sep 27, 2024 · f1ef7b6 · f1ef7b6
1 parent cda02d2
commit f1ef7b6
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/kdrag/solvers/__init__.py b/kdrag/solvers/__init__.py
@@ -107,6 +107,9 @@ def check(self):
     def unsat_core(self):
         raise NotImplementedError
 
+    def proof(self):
+        return self.res.stdout
+
     def set(self, option, value):
         self.options[option] = value
 

diff --git a/kdrag/utils.py b/kdrag/utils.py
@@ -1,6 +1,5 @@
 from kdrag.kernel import is_proof
 import kdrag.smt as smt
-import subprocess
 import sys
 import kdrag as kd
 from typing import Optional
@@ -205,6 +204,11 @@ def sort_to_tptp(sort: smt.SortRef):
         return name.lower()
 
 
+def expr_to_lean(expr: smt.ExprRef):
+    # TODO
+    pass
+
+
 def subterms(t: smt.ExprRef):
     todo = [t]
     while len(todo) > 0: