From: Guy <guy@Guy-X260>
Date: Fri, 16 Sep 2016 22:43:47 +0000 (-0700)
Subject: Let arith_proof print its own terms
X-Git-Tag: cvc5-1.0.0~6028^2~45
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=976ee5b66b7584b9fe46eab1facf5e5f857e723f;p=cvc5.git

Let arith_proof print its own terms
---

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 4e813d646..b7ed0b2ec 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -636,6 +636,10 @@ void ArithProof::registerTerm(Expr term) {
     d_realMode = true;
   }
 
+  if (term.isVariable() && !ProofManager::getSkolemizationManager()->isSkolem(term)) {
+    d_declarations.insert(term);
+  }
+
   // recursively declare all other terms
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
     // could belong to other theories
@@ -824,6 +828,14 @@ void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren
 }
 
 void LFSCArithProof::printTermDeclarations(std::ostream& os, std::ostream& paren) {
+  for (ExprSet::const_iterator it = d_declarations.begin(); it != d_declarations.end(); ++it) {
+    Expr term = *it;
+    Assert(term.isVariable());
+    os << "(% " << ProofManager::sanitize(term) << " ";
+    os << "(term ";
+    os << term.getType() << ")\n";
+    paren << ")";
+  }
 }
 
 void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& paren) {
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 126e89ed2..08985487d 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -53,7 +53,7 @@ protected:
   // std::map<Expr, std::string> d_constRationalString; // all the variable/function declarations
 
   //   TypeSet d_sorts;        // all the uninterpreted sorts in this theory
-  // ExprSet d_declarations; // all the variable/function declarations
+  ExprSet d_declarations; // all the variable/function declarations
 
   bool d_realMode;