summaryrefslogtreecommitdiff
path: root/src/proof/theory_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r--src/proof/theory_proof.cpp102
1 files changed, 81 insertions, 21 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index b74d4a4d2..b516c250f 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -176,6 +176,30 @@ void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1,
getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2, globalLetMap);
}
+void TheoryProofEngine::printTheoryTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map,
+ TypeNode expectedType)
+{
+ this->printTheoryTermAsType(term, os, map, expectedType);
+}
+
+TypeNode TheoryProofEngine::equalityType(const Expr& left, const Expr& right)
+{
+ // Ask the two theories what they think..
+ TypeNode leftType = getTheoryProof(theory::Theory::theoryOf(left))->equalityType(left, right);
+ TypeNode rightType = getTheoryProof(theory::Theory::theoryOf(right))->equalityType(left, right);
+
+ // Error if the disagree.
+ Assert(leftType.isNull() || rightType.isNull() || leftType == rightType)
+ << "TheoryProofEngine::equalityType(" << left << ", " << right << "):" << std::endl
+ << "theories disagree about the type of an equality:" << std::endl
+ << "\tleft: " << leftType << std::endl
+ << "\tright:" << rightType;
+
+ return leftType.isNull() ? rightType : leftType;
+}
+
void TheoryProofEngine::registerTerm(Expr term) {
Debug("pf::tp::register") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl;
@@ -295,11 +319,11 @@ void LFSCTheoryProofEngine::printTheoryTermAsType(Expr term,
if (theory_id == theory::THEORY_BUILTIN ||
term.getKind() == kind::ITE ||
term.getKind() == kind::EQUAL) {
- printCoreTerm(term, os, map);
+ printCoreTerm(term, os, map, expectedType);
return;
}
// dispatch to proper theory
- getTheoryProof(theory_id)->printOwnedTerm(term, os, map);
+ getTheoryProof(theory_id)->printOwnedTerm(term, os, map, expectedType);
}
void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) {
@@ -866,18 +890,29 @@ void LFSCTheoryProofEngine::printBoundTermAsType(Expr term,
{
Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
- ProofLetMap::const_iterator it = map.find(term);
- if (it != map.end()) {
- unsigned id = it->second.id;
- unsigned count = it->second.count;
+ // Since let-abbreviated terms are abbreviated with their default type, only
+ // use the let map if there is no expectedType or the expectedType matches
+ // the default.
+ if (expectedType.isNull()
+ || TypeNode::fromType(term.getType()) == expectedType)
+ {
+ ProofLetMap::const_iterator it = map.find(term);
+ if (it != map.end())
+ {
+ unsigned id = it->second.id;
+ unsigned count = it->second.count;
- if (count > LET_COUNT) {
- os << "let" << id;
- return;
+ if (count > LET_COUNT)
+ {
+ os << "let" << id;
+ Debug("pf::tp::letmap") << "Using let map for " << term << std::endl;
+ return;
+ }
}
}
+ Debug("pf::tp::letmap") << "Skipping let map for " << term << std::endl;
- printTheoryTerm(term, os, map);
+ printTheoryTerm(term, os, map, expectedType);
}
void LFSCTheoryProofEngine::printBoundFormula(Expr term,
@@ -900,7 +935,7 @@ void LFSCTheoryProofEngine::printBoundFormula(Expr term,
void LFSCTheoryProofEngine::printCoreTerm(Expr term,
std::ostream& os,
const ProofLetMap& map,
- Type expectedType)
+ TypeNode expectedType)
{
if (term.isVariable()) {
os << ProofManager::sanitize(term);
@@ -911,6 +946,9 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term,
switch(k) {
case kind::ITE: {
+ TypeNode armType = expectedType.isNull()
+ ? TypeNode::fromType(term.getType())
+ : expectedType;
bool useFormulaType = term.getType().isBoolean();
Assert(term[1].getType().isSubtypeOf(term.getType()));
Assert(term[2].getType().isSubtypeOf(term.getType()));
@@ -924,7 +962,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term,
}
else
{
- printBoundTerm(term[1], os, map);
+ printBoundTerm(term[1], os, map, armType);
}
os << " ";
if (useFormulaType)
@@ -941,6 +979,7 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term,
case kind::EQUAL: {
bool booleanCase = term[0].getType().isBoolean();
+ TypeNode armType = equalityType(term[0], term[1]);
os << "(";
if (booleanCase) {
@@ -952,13 +991,13 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term,
}
if (booleanCase && printsAsBool(term[0])) os << "(p_app ";
- printBoundTerm(term[0], os, map);
+ printBoundTerm(term[0], os, map, armType);
if (booleanCase && printsAsBool(term[0])) os << ")";
os << " ";
if (booleanCase && printsAsBool(term[1])) os << "(p_app ";
- printBoundTerm(term[1], os, map);
+ printBoundTerm(term[1], os, map, armType);
if (booleanCase && printsAsBool(term[1])) os << ") ";
os << ")";
@@ -966,16 +1005,18 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term,
}
case kind::DISTINCT:
+ {
// Distinct nodes can have any number of chidlren.
Assert(term.getNumChildren() >= 2);
+ TypeNode armType = equalityType(term[0], term[1]);
if (term.getNumChildren() == 2) {
os << "(not (= ";
printSort(term[0].getType(), os);
os << " ";
- printBoundTerm(term[0], os, map);
+ printBoundTerm(term[0], os, map, armType);
os << " ";
- printBoundTerm(term[1], os, map);
+ printBoundTerm(term[1], os, map, armType);
os << "))";
} else {
unsigned numOfPairs = term.getNumChildren() * (term.getNumChildren() - 1) / 2;
@@ -985,28 +1026,29 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term,
for (unsigned i = 0; i < term.getNumChildren(); ++i) {
for (unsigned j = i + 1; j < term.getNumChildren(); ++j) {
+ TypeNode armType = equalityType(term[i], term[j]);
if ((i != 0) || (j != 1)) {
os << "(not (= ";
printSort(term[0].getType(), os);
os << " ";
- printBoundTerm(term[i], os, map);
+ printBoundTerm(term[i], os, map, armType);
os << " ";
- printBoundTerm(term[j], os, map);
+ printBoundTerm(term[j], os, map, armType);
os << ")))";
} else {
os << "(not (= ";
printSort(term[0].getType(), os);
os << " ";
- printBoundTerm(term[0], os, map);
+ printBoundTerm(term[0], os, map, armType);
os << " ";
- printBoundTerm(term[1], os, map);
+ printBoundTerm(term[1], os, map, armType);
os << "))";
}
}
}
}
-
return;
+ }
case kind::CHAIN: {
// LFSC doesn't allow declarations with variable numbers of
@@ -1345,6 +1387,24 @@ void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node
os << "))";
}
+void TheoryProof::printOwnedTerm(Expr term,
+ std::ostream& os,
+ const ProofLetMap& map,
+ TypeNode expectedType)
+{
+ this->printOwnedTermAsType(term, os, map, expectedType);
+}
+
+TypeNode TheoryProof::equalityType(const Expr& left, const Expr& right)
+{
+ Assert(left.getType() == right.getType())
+ << "TheoryProof::equalityType(" << left << ", " << right << "):" << std::endl
+ << "types disagree:" << std::endl
+ << "\tleft: " << left.getType() << std::endl
+ << "\tright:" << right.getType();
+ return TypeNode::fromType(left.getType());
+}
+
bool TheoryProof::match(TNode n1, TNode n2)
{
theory::TheoryId theoryId = this->getTheoryId();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback