Use letification for the aliasing declarations as well (consequently, print the globa...

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 4864cbf46f025d94f977280a362ff558db30a8fc..100f606009be372e9d2a695fdc32421a77ce20fb 100644 (file)
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -830,7 +830,7 @@ void LFSCArithProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
   // Nothing to do here at this point.
 }
 
-void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCArithProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
   // Nothing to do here at this point.
 }
 

diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index d980654c4bc26d2aaa6814ccb877d837a59616bd..126e89ed255027bd0a740e78f7c986696ad99fe6 100644 (file)
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -74,7 +74,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 };
 
 

diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index 18e01728b4cc0dee126084fdf746b985abc5b20f..63758e573dadae153c4292e2923a2de9fcf7e055 100644 (file)
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -1380,7 +1380,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
   }
 }
 
-void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCArrayProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
     // Nothing to do here at this point.
 }
 

diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 69e62dbf397b0079a406ab687dd05a99622537a6..61f168a163ab584cf4b08d75c90a6726c70d2193 100644 (file)
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -124,7 +124,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 };
 
 

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index f557d506317e55626cd8a3c437c827a6d23471b2..2da0d5362f8a390ee2528d59c6884cb4a7a646be 100644 (file)
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -656,7 +656,7 @@ void LFSCBitVectorProof::printDeferredDeclarations(std::ostream& os, std::ostrea
   // Nothing to do here at this point.
 }
 
-void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
   // Print "trust" statements to bind complex bv variables to their associated terms
 
   ExprToString::const_iterator it = d_assignedAliases.begin();
@@ -673,8 +673,7 @@ void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostrea
     os << "(trust_f ";
     os << "(= (BitVec " << utils::getSize(it->first) << ") ";
     os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") ";
-    ProofLetMap emptyMap;
-    d_proofEngine->printBoundTerm(it->first, os, emptyMap);
+    d_proofEngine->printBoundTerm(it->first, os, globalLetMap);
     os << ")) ";
     os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n";
     paren << "))";

diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index a52292ec90c538ca99307f8bf867400073dff96a..8d0871ef8ede2504b72e66e61c1026e80bfeec43 100644 (file)
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -148,7 +148,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
   virtual void printBitblasting(std::ostream& os, std::ostream& paren);
   virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
   void calculateAtomsInBitblastingProof();

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index cb6eee330f3736b185676e555afc5e12bf3d4056..835990613b6d84b27cf09a150cdcd370f682a240 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -515,18 +515,16 @@ void LFSCProof::toStream(std::ostream& out) {
   out << " ;; Printing deferred declarations \n\n";
   d_theoryProof->printDeferredDeclarations(out, paren);
 
+  out << "\n ;; Printing the global let map";
   d_theoryProof->finalizeBvConflicts(used_lemmas, out);
   ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
-
-  out << "\n ;; Printing the global let map \n";
-
   ProofLetMap globalLetMap;
   if (options::lfscLetification()) {
     ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren);
   }
 
   out << " ;; Printing aliasing declarations \n\n";
-  d_theoryProof->printAliasingDeclarations(out, paren);
+  d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap);
 
   out << " ;; Rewrites for Lemmas \n";
   d_theoryProof->printLemmaRewrites(rewrites, out, paren);

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index f0f333598d0045e116f088921244526aa04a7f88..f544f5ff568d6e47c810c1e2319beca1018c628e 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -406,13 +406,13 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost
   }
 }
 
-void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl;
 
   TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
   TheoryProofTable::const_iterator end = d_theoryProofTable.end();
   for (; it != end; ++it) {
-    it->second->printAliasingDeclarations(os, paren);
+    it->second->printAliasingDeclarations(os, paren, globalLetMap);
   }
 }
 
@@ -1168,7 +1168,7 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream&
   // Nothing to do here at this point.
 }
 
-void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
   // Nothing to do here at this point.
 }
 

diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 5907f9bd587bc6152c309a9f6623a386c856a096..968d46e687bda02c14c86dd7e5aa614bc3f2a3a8 100644 (file)
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -109,7 +109,7 @@ public:
    * @param os
    * @param paren closing parenthesis
    */
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
 
   /**
    * Print proofs of all the theory lemmas (must prove
@@ -173,7 +173,7 @@ public:
   virtual void printAssertions(std::ostream& os, std::ostream& paren);
   virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
   virtual void printTheoryLemmas(const IdToSatClause& lemmas,
                                  std::ostream& os,
                                  std::ostream& paren,
@@ -274,7 +274,7 @@ public:
    * @param os
    * @param paren
    */
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
   /**
    * Register a term of this theory that appears in the proof.
    *
@@ -312,7 +312,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren) = 0;
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren) = 0;
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren) = 0;
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) = 0;
 };
 
 class LFSCBooleanProof : public BooleanProof {
@@ -326,7 +326,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 
   void treatBoolsAsFormulas(bool value) {
     d_treatBoolsAsFormulas = value;

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 139ce5ed2c84d458b6a43bc036bf900a61e6fcd6..e122a46bca10b8ec90f71baffabb69e14a4ac397 100644 (file)
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -797,7 +797,7 @@ void LFSCUFProof::printDeferredDeclarations(std::ostream& os, std::ostream& pare
   // Nothing to do here at this point.
 }
 
-void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap) {
   // Nothing to do here at this point.
 }
 

diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 444b602dcceab4eaa2cf0fdf678ba52be91aafa7..ff0f9a8799d27cccee86d5cc8c11b234701a9319 100644 (file)
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -70,7 +70,7 @@ public:
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
+  virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren, const ProofLetMap &globalLetMap);
 };