diff options
Diffstat (limited to 'src/proof/bitvector_proof.h')
-rw-r--r-- | src/proof/bitvector_proof.h | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 4e5e98541..4a1f4015d 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -60,7 +60,6 @@ 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: @@ -109,8 +108,7 @@ public: virtual void registerTerm(Expr term); virtual void printTermBitblasting(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 printAtomBitblasting(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; @@ -125,12 +123,6 @@ 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) @@ -138,13 +130,11 @@ 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, bool swap); - virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os); + virtual void printAtomBitblasting(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); }; |