From 42eed1a8f72d4a5b9ac384100b42f7b0c8b46729 Mon Sep 17 00:00:00 2001 From: Guy Date: Thu, 30 Jun 2016 12:38:56 -0700 Subject: [PATCH] Support for the letification of chained AND and OR operations in LFSC proofs --- src/proof/proof_manager.cpp | 23 ++++++++++++++++++----- 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& atoms, @@ -708,7 +722,6 @@ void ProofManager::printGlobalLetMap(std::set& atoms, // TODO: give each theory a chance to add atoms. For now, just query BV directly... const std::set* 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: -- 2.30.2