diff options
| author | Guy <katz911@gmail.com> | 2016-06-08 11:52:42 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-06-08 11:52:42 -0700 |
| commit | 4b8f92d23f7a75b4148f41e039f7bdc5f165babc (patch) | |
| tree | e2d8abdff6f2d6befa652a09188fff991caf1cf4 /src/proof/bitvector_proof.h | |
| parent | 8bfab32eed06973d53ce8ae066a9a26d4ae8a489 (diff) | |
Support for printing a global let map in LFSC proofs.
Added a flag to enable/disbale this feature (enabled by default).
Also, added some infrastructure for proving rewrite rules.
Diffstat (limited to 'src/proof/bitvector_proof.h')
| -rw-r--r-- | src/proof/bitvector_proof.h | 27 |
1 files changed, 17 insertions, 10 deletions
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index 5ea754e08..a52292ec9 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -113,41 +113,48 @@ public: 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; - + virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0; + virtual const std::set<Node>* getAtomsInBitblastingProof() = 0; + virtual void calculateAtomsInBitblastingProof() = 0; }; class LFSCBitVectorProof: public BitVectorProof { void printConstant(Expr term, std::ostream& os); - void printOperatorNary(Expr term, std::ostream& os, const LetMap& map); - void printOperatorUnary(Expr term, std::ostream& os, const LetMap& map); - 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); + void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map); + void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map); + void printPredicate(Expr term, std::ostream& os, const ProofLetMap& map); + void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map); + void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map); ExprToString d_exprToVariableName; ExprToString d_assignedAliases; std::map<std::string, std::string> d_aliasToBindDeclaration; std::string assignAlias(Expr expr); bool hasAlias(Expr expr); + + std::set<Node> d_atomsInBitblastingProof; + public: LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine) :BitVectorProof(bv, proofEngine) {} - virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map); + virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& 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 printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren); + virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map); 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); + virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap); + void calculateAtomsInBitblastingProof(); + const std::set<Node>* getAtomsInBitblastingProof(); void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2); + void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2); }; }/* CVC4 namespace */ |