diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-01-29 16:07:09 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-29 16:07:09 -0800 |
commit | 7849f09ece473f9822f91572115e50af7eae9564 (patch) | |
tree | 5282b3bc4cb2ab247189edfc0a5df63558cea852 /src/proof/theory_proof.cpp | |
parent | f4a10a74ee45018836aa7d7c07910f294c32b2cc (diff) |
expectedType in proof-printing code (#3665)
* expectedType in proof-printing code
To print lemma proofs in theories that use multiple sorts that have a
subtype relationship, we need to increase communication between the
TheoryProofEngine and the theory proofs themselves.
This commit add an (optional) argument `expectedType` to many
term-printing functions in TheoryProofEngine and TheoryProof.
Right now it is unused, so always takes on the default value of "null"
(meaning no type expectation), but in the future the TheoryProofEngine
will use it to signal TheoryProof about what type is expected to be
printed.
* TypeNode, Don't mix default args & virtual
* Use TypeNode instead of Type (The former are lighter)
* Don't add default arguments to virtual functions, because these cannot
be dynamically overriden during a dynamic dispatch.
* Since we don't want them to be overidable anyway, we use two
functions: one that is non-virtual and has a default, the other that
is virtual but has no default. The former just calls the latter.
* clang-format after signature changes
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r-- | src/proof/theory_proof.cpp | 26 |
1 files changed, 20 insertions, 6 deletions
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) { |