Make get-proof command SMT-LIB compliant. (#4)

Make `get-proof` command SMT-LIB compliant.
HanielB · Nov 8, 2022 · cacfb32 · cacfb32
2 parents 6751c64 + 4347ea5
commit cacfb32
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 3 deletions.
diff --git a/src/parser/api/cpp/command.cpp b/src/parser/api/cpp/command.cpp
@@ -1490,7 +1490,12 @@ void GetProofCommand::invoke(cvc5::Solver* solver, SymbolManager* sm)
 
 void GetProofCommand::printResult(cvc5::Solver* solver, std::ostream& out) const
 {
-  out << d_result;
+  std::string result = d_result;
+  if (solver->getOption("proof-format-mode") == "lean")
+  {
+    result = "(proof \"" + result + "\")\n";
+  }
+  out << result;
 }
 
 std::string GetProofCommand::getCommandName() const { return "get-proof"; }

diff --git a/src/proof/lean/lean_node_converter.cpp b/src/proof/lean/lean_node_converter.cpp
@@ -277,7 +277,7 @@ Node LeanNodeConverter::convert(Node n)
         {
           TypeNode tn = cur.getType();
           AlwaysAssert(tn.isInteger()) << "Only support integer rationals\n";
-          res = mkInt(cur);
+          res = cur;
           break;
         }
         case kind::CONST_BITVECTOR:

diff --git a/src/proof/lean/lean_node_converter.h b/src/proof/lean/lean_node_converter.h
@@ -62,7 +62,6 @@ class LeanNodeConverter
   // Node mkList(const std::vector<Node>& nodes);
 
   Node mkInt(unsigned i);
-  Node mkInt(Node i);
 
   std::vector<Node> getOperatorIndices(Kind k, Node n);