diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
commit | 4dac1ec234ee0d0885f058b4b35a7eeba2ca5007 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/proof/bitvector_proof.h | |
parent | de0dd1dc966b05467f1a5443ff33094262f5076a (diff) |
Merge from proof branch
Diffstat (limited to 'src/proof/bitvector_proof.h')
-rw-r--r-- | src/proof/bitvector_proof.h | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4a1f4015d..4e5e98541 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -60,6 +60,7 @@ typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet; typedef __gnu_cxx::hash_map<Expr, ClauseId, ExprHashFunction> ExprToClauseId; typedef __gnu_cxx::hash_map<Expr, unsigned, ExprHashFunction> ExprToId; typedef __gnu_cxx::hash_map<Expr, Expr, ExprHashFunction> ExprToExpr; +typedef __gnu_cxx::hash_map<Expr, std::string, ExprHashFunction> ExprToString; class BitVectorProof : public TheoryProof { protected: @@ -108,7 +109,8 @@ public: virtual void registerTerm(Expr term); virtual void printTermBitblasting(Expr term, std::ostream& os) = 0; - virtual void printAtomBitblasting(Expr term, std::ostream& os) = 0; + virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap) = 0; + virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0; virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0; virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0; @@ -123,6 +125,12 @@ class LFSCBitVectorProof: public BitVectorProof { void printPredicate(Expr term, std::ostream& os, const LetMap& map); void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map); void printBitOf(Expr term, std::ostream& os, const LetMap& map); + + ExprToString d_exprToVariableName; + ExprToString d_assignedAliases; + std::map<std::string, std::string> d_aliasToBindDeclaration; + std::string assignAlias(Expr expr); + bool hasAlias(Expr expr); public: LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) :BitVectorProof(bv, proofEngine) @@ -130,11 +138,13 @@ public: virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); virtual void printOwnedSort(Type type, std::ostream& os); virtual void printTermBitblasting(Expr term, std::ostream& os); - virtual void printAtomBitblasting(Expr term, std::ostream& os); + virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap); + virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os); virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); 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 printBitblasting(std::ostream& os, std::ostream& paren); virtual void printResolutionProof(std::ostream& os, std::ostream& paren); }; |