Let arith_proof print its own terms

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 4e813d6462680c6b6f1d0b774ea4f56582a406c7..b7ed0b2ec76dea4330eef3227ccaf17352f9e19c 100644 (file)
--- 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 126e89ed255027bd0a740e78f7c986696ad99fe6..08985487ddd80cb2d982cfc602f687aedca0f30a 100644 (file)
--- 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;