From: Guy <katz911@gmail.com>
Date: Mon, 25 Jul 2016 05:35:05 +0000 (-0700)
Subject: Use letification for the aliasing declarations as well (consequently, print the globa... 
X-Git-Tag: cvc5-1.0.0~6040^2~36
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1aa6f7798ff47c3a6af665adb95a6d5266f3c34b;p=cvc5.git

Use letification for the aliasing declarations as well (consequently, print the global let map before the aliasing part)
---

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 4864cbf46..100f60600 100644
--- 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 d980654c4..126e89ed2 100644
--- 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 18e01728b..63758e573 100644
--- 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 69e62dbf3..61f168a16 100644
--- 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 f557d5063..2da0d5362 100644
--- 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 a52292ec9..8d0871ef8 100644
--- 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 cb6eee330..835990613 100644
--- 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 f0f333598..f544f5ff5 100644
--- 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 5907f9bd5..968d46e68 100644
--- 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 139ce5ed2..e122a46bc 100644
--- 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 444b602dc..ff0f9a879 100644
--- 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);
 };