diff options
author | Guy <katz911@gmail.com> | 2016-06-30 12:38:56 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-30 12:38:56 -0700 |
commit | 42eed1a8f72d4a5b9ac384100b42f7b0c8b46729 (patch) | |
tree | 8a6da332537f17ed9917a4fffa58eb33f4c1c7f5 /src | |
parent | c167446c59939a56f10f853e7d33a92fc16df460 (diff) |
Support for the letification of chained AND and OR operations in LFSC proofs
Diffstat (limited to 'src')
-rw-r--r-- | src/proof/proof_manager.cpp | 23 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 28 |
2 files changed, 46 insertions, 5 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index d61261b38..d155630e5 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -689,10 +689,24 @@ void bind(Expr term, ProofLetMap& map, Bindings& letOrder) { for (unsigned i = 0; i < term.getNumChildren(); ++i) bind(term[i], map, letOrder); - unsigned newId = ProofLetCount::newId(); - ProofLetCount letCount(newId); - map[term] = letCount; - letOrder.push_back(LetOrderElement(term, newId)); + // Special case: chain operators. If we have and(a,b,c), it will be prineted as and(a,and(b,c)). + // The subterm and(b,c) may repeat elsewhere, so we need to bind it, too. + Kind k = term.getKind(); + if (((k == kind::OR) || (k == kind::AND)) && term.getNumChildren() > 2) { + Node currentExpression = term[term.getNumChildren() - 1]; + for (int i = term.getNumChildren() - 2; i >= 0; --i) { + NodeBuilder<> builder(k); + builder << term[i]; + builder << currentExpression.toExpr(); + currentExpression = builder; + bind(currentExpression.toExpr(), map, letOrder); + } + } else { + unsigned newId = ProofLetCount::newId(); + ProofLetCount letCount(newId); + map[term] = letCount; + letOrder.push_back(LetOrderElement(term, newId)); + } } void ProofManager::printGlobalLetMap(std::set<Node>& atoms, @@ -708,7 +722,6 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms, // TODO: give each theory a chance to add atoms. For now, just query BV directly... const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof(); for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) { - Debug("gk::temp") << "Binding additional atom: " << *atom << std::endl; bind(atom->toExpr(), letMap, letOrder); } diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 634b2b738..eff0a8247 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -19,6 +19,7 @@ #include "base/cvc4_assert.h" #include "context/context.h" #include "options/bv_options.h" +#include "options/proof_options.h" #include "proof/arith_proof.h" #include "proof/array_proof.h" #include "proof/bitvector_proof.h" @@ -801,6 +802,7 @@ void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const Pr if (it != map.end()) { unsigned id = it->second.id; unsigned count = it->second.count; + if (count > LET_COUNT) { os << "let" << id; return; @@ -1044,6 +1046,32 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLe switch(k) { case kind::OR: case kind::AND: + if (options::lfscLetification() && term.getNumChildren() > 2) { + // If letification is on, the entire term is probably a let expression. + // However, we need to transform it from (and a b c) into (and a (and b c)) form first. + Node currentExpression = term[term.getNumChildren() - 1]; + for (int i = term.getNumChildren() - 2; i >= 0; --i) { + NodeBuilder<> builder(k); + builder << term[i]; + builder << currentExpression.toExpr(); + currentExpression = builder; + } + + // The let map should already have the current expression. + 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; + break; + } + } + } + + // If letification is off or there were 2 children, same treatment as the other cases. + // (No break is intentional). case kind::XOR: case kind::IFF: case kind::IMPLIES: |