summaryrefslogtreecommitdiff
path: root/src/proof/theory_proof.cpp
diff options
context:
space:
mode:
authorAlex Ozdemir <aozdemir@hmc.edu>2020-01-29 16:07:09 -0800
committerGitHub <noreply@github.com>2020-01-29 16:07:09 -0800
commit7849f09ece473f9822f91572115e50af7eae9564 (patch)
tree5282b3bc4cb2ab247189edfc0a5df63558cea852 /src/proof/theory_proof.cpp
parentf4a10a74ee45018836aa7d7c07910f294c32b2cc (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.cpp26
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback