diff options
-rw-r--r-- | src/proof/arith_proof.cpp | 6 | ||||
-rw-r--r-- | src/proof/arith_proof.h | 7 | ||||
-rw-r--r-- | src/proof/array_proof.cpp | 6 | ||||
-rw-r--r-- | src/proof/array_proof.h | 7 | ||||
-rw-r--r-- | src/proof/bitvector_proof.cpp | 7 | ||||
-rw-r--r-- | src/proof/bitvector_proof.h | 7 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 26 | ||||
-rw-r--r-- | src/proof/theory_proof.h | 108 | ||||
-rw-r--r-- | src/proof/uf_proof.cpp | 6 | ||||
-rw-r--r-- | src/proof/uf_proof.h | 7 |
10 files changed, 149 insertions, 38 deletions
diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp index ba38a314c..9ee5f2143 100644 --- a/src/proof/arith_proof.cpp +++ b/src/proof/arith_proof.cpp @@ -681,7 +681,11 @@ void ArithProof::registerTerm(Expr term) { } } -void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { +void LFSCArithProof::printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) +{ Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind() << ". Type: " << term.getType() << ". Number of children: " << term.getNumChildren() << std::endl; diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h index c70754a1f..ac96ad1f3 100644 --- a/src/proof/arith_proof.h +++ b/src/proof/arith_proof.h @@ -82,9 +82,10 @@ public: LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine) : ArithProof(arith, proofEngine) {} - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; + void printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) override; void printOwnedSort(Type type, std::ostream& os) override; /** diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp index ec2f85829..75b7b7f1b 100644 --- a/src/proof/array_proof.cpp +++ b/src/proof/array_proof.cpp @@ -1123,7 +1123,11 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) { return d_skolemToLiteral[skolem]; } -void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { +void LFSCArrayProof::printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) +{ Assert(theory::Theory::theoryOf(term) == theory::THEORY_ARRAYS); if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAYS) { diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h index 372ad1f67..55cda0aba 100644 --- a/src/proof/array_proof.h +++ b/src/proof/array_proof.h @@ -95,9 +95,10 @@ public: : ArrayProof(arrays, proofEngine) {} - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; + void printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) override; void printOwnedSort(Type type, std::ostream& os) override; void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp index c60cc8274..e75b94c8e 100644 --- a/src/proof/bitvector_proof.cpp +++ b/src/proof/bitvector_proof.cpp @@ -121,9 +121,10 @@ std::string BitVectorProof::getBBTermName(Expr expr) return os.str(); } -void BitVectorProof::printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) +void BitVectorProof::printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) { Debug("pf::bv") << std::endl << "(pf::bv) BitVectorProof::printOwnedTerm( " << term diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h index f0a0717fa..8264d3bc4 100644 --- a/src/proof/bitvector_proof.h +++ b/src/proof/bitvector_proof.h @@ -135,9 +135,10 @@ class BitVectorProof : public TheoryProof theory::TheoryId getTheoryId() override; public: - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; + void printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) override; void printOwnedSort(Type type, std::ostream& os) override; diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index eee75e612..b74d4a4d2 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -283,7 +283,11 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { os << paren.str(); } -void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) { +void LFSCTheoryProofEngine::printTheoryTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) +{ theory::TheoryId theory_id = theory::Theory::theoryOf(term); // boolean terms and ITEs are special because they @@ -855,7 +859,11 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } } -void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map) { +void LFSCTheoryProofEngine::printBoundTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) +{ Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; ProofLetMap::const_iterator it = map.find(term); @@ -889,7 +897,11 @@ void LFSCTheoryProofEngine::printBoundFormula(Expr term, } } -void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) { +void LFSCTheoryProofEngine::printCoreTerm(Expr term, + std::ostream& os, + const ProofLetMap& map, + Type expectedType) +{ if (term.isVariable()) { os << ProofManager::sanitize(term); return; @@ -1034,7 +1046,6 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Pro default: Unhandled() << k; } - } void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, @@ -1181,7 +1192,11 @@ void LFSCBooleanProof::printConstantDisequalityProof(std::ostream& os, Expr c1, os << "(negsymm _ _ _ t_t_neq_f)"; } -void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { +void LFSCBooleanProof::printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) +{ Assert(term.getType().isBoolean()); if (term.isVariable()) { os << ProofManager::sanitize(term); @@ -1259,7 +1274,6 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe default: Unhandled() << k; } - } void LFSCBooleanProof::printOwnedSort(Type type, std::ostream& os) { diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 577f0c032..e8569d636 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -25,6 +25,7 @@ #include <unordered_set> #include "expr/expr.h" +#include "expr/type_node.h" #include "proof/clause_id.h" #include "proof/proof_utils.h" #include "prop/sat_solver_types.h" @@ -69,8 +70,34 @@ public: * @param os */ virtual void printLetTerm(Expr term, std::ostream& os) = 0; - virtual void printBoundTerm(Expr term, std::ostream& os, - const ProofLetMap& map) = 0; + + /** + * Print a term in some (core or non-core) theory + * + * @param term expression representing term + * @param os output stream + * @param expectedType The type that this is expected to have in a parent + * node. Null if there are no such requirements. This is useful for requesting + * type conversions from the theory. e.g. in (5.5 == 4) the right-hand-side + * should be converted to a real. + * + * The first version of this function has a default value for expectedType + * (null) The second version is virtual. + * + * They are split to avoid mixing virtual function and default argument + * values, which behave weirdly when combined. + */ + void printBoundTerm(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType = TypeNode()) + { + this->printBoundTermAsType(term, os, map, expectedType); + } + virtual void printBoundTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) = 0; /** * Print the proof representation of the given sort. @@ -152,7 +179,33 @@ public: void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2, const ProofLetMap &globalLetMap); - virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; + /** + * Print a term in some non-core theory + * + * @param term expression representing term + * @param os output stream + * @param expectedType The type that this is expected to have in a parent + * node. Null if there are no such requirements. This is useful for requesting + * type conversions from the theory. e.g. in (5.5 == 4) the right-hand-side + * should be converted to a real. + * + * The first version of this function has a default value for expectedType + * (null) The second version is virtual. + * + * They are split to avoid mixing virtual function and default argument + * values, which behave weirdly when combined. + */ + void printTheoryTerm(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType = TypeNode()) + { + this->printTheoryTermAsType(term, os, map, expectedType); + } + virtual void printTheoryTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) = 0; bool printsAsBool(const Node &n); }; @@ -163,18 +216,23 @@ public: LFSCTheoryProofEngine() : TheoryProofEngine() {} - void printTheoryTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; + void printTheoryTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) override; void registerTermsFromAssertions() override; void printSortDeclarations(std::ostream& os, std::ostream& paren); void printTermDeclarations(std::ostream& os, std::ostream& paren); - void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map); + void printCoreTerm(Expr term, + std::ostream& os, + const ProofLetMap& map, + Type expectedType = Type()); void printLetTerm(Expr term, std::ostream& os) override; - void printBoundTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; + void printBoundTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) override; void printAssertions(std::ostream& os, std::ostream& paren) override; void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, @@ -234,8 +292,29 @@ protected: * * @param term expression representing term * @param os output stream + * @param expectedType The type that this is expected to have in a parent + * node. Null if there are no such requirements. This is useful for requesting + * type conversions from the theory. e.g. in (5.5 == 4) the right-hand-side + * should be converted to a real. + * + * The first version of this function has a default value for expectedType + * (null) The second version is virtual. + * + * They are split to avoid mixing virtual function and default argument + * values, which behave weirdly when combined. */ - virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0; + void printOwnedTerm(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType = TypeNode()) + { + this->printOwnedTermAsType(term, os, map, expectedType); + } + virtual void printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) = 0; + /** * Print the proof representation of the given type that belongs to some theory. * @@ -388,9 +467,10 @@ public: LFSCBooleanProof(TheoryProofEngine* proofEngine) : BooleanProof(proofEngine) {} - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; + void printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode ty) override; void printOwnedSort(Type type, std::ostream& os) override; void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index b88f7dc33..3c4c7d381 100644 --- a/src/proof/uf_proof.cpp +++ b/src/proof/uf_proof.cpp @@ -623,7 +623,11 @@ void UFProof::registerTerm(Expr term) { } } -void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { +void LFSCUFProof::printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) +{ Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl; Assert(theory::Theory::theoryOf(term) == theory::THEORY_UF); diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h index ca8b3f90e..834f6ef9e 100644 --- a/src/proof/uf_proof.h +++ b/src/proof/uf_proof.h @@ -75,9 +75,10 @@ public: LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine) : UFProof(uf, proofEngine) {} - void printOwnedTerm(Expr term, - std::ostream& os, - const ProofLetMap& map) override; + void printOwnedTermAsType(Expr term, + std::ostream& os, + const ProofLetMap& map, + TypeNode expectedType) override; void printOwnedSort(Type type, std::ostream& os) override; void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, |