From 41c08f745d5f6750a12e6cef4c48ac37c4844997 Mon Sep 17 00:00:00 2001 From: Andres Notzli Date: Sat, 10 Dec 2016 23:34:42 -0800 Subject: Remove input assertions --- src/proof/proof_manager.cpp | 33 ++++++++++++--------------------- src/proof/proof_manager.h | 19 ++++++++----------- src/proof/theory_proof.cpp | 15 ++++++++++----- src/smt/smt_engine.cpp | 10 ++-------- 4 files changed, 32 insertions(+), 45 deletions(-) diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 5ce615366..879635d7b 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -60,7 +60,6 @@ ProofManager::ProofManager(ProofFormat format): d_satProof(NULL), d_cnfProof(NULL), d_theoryProof(NULL), - d_inputFormulas(), d_inputCoreFormulas(), d_outputCoreFormulas(), d_nextId(0), @@ -223,7 +222,7 @@ std::string ProofManager::getAssertionName(Node node, return append(prefix+".A", node.getId()); } std::string ProofManager::getInputFormulaName(const Expr& expr) { - return currentPM()->d_inputFormulaToName[expr]; + return currentPM()->d_inputCoreFormulaToName[expr]; } std::string ProofManager::getAtomName(TNode atom, @@ -452,18 +451,13 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { return builder; } -void ProofManager::addAssertion(Expr formula) { - Debug("proof:pm") << "assert: " << formula << std::endl; - d_inputFormulas.insert(formula); - std::ostringstream name; - name << "A" << d_inputFormulaToName.size(); - d_inputFormulaToName[formula] = name.str(); -} - void ProofManager::addCoreAssertion(Expr formula) { Debug("cores") << "assert: " << formula << std::endl; d_deps[Node::fromExpr(formula)]; // empty vector of deps d_inputCoreFormulas.insert(formula); + std::ostringstream name; + name << "A" << d_inputCoreFormulaToName.size(); + d_inputCoreFormulaToName[formula] = name.str(); } void ProofManager::addDependence(TNode n, TNode dep) { @@ -707,7 +701,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, // For the remaining assertions, bind them to input assertions. for (; it != end; ++it) { // Rewrite preprocessing step if it cannot be eliminated - if (!ProofManager::currentPM()->have_input_assertion((*it).toExpr())) { + if (!ProofManager::currentPM()->have_input_core_assertion( + (*it).toExpr())) { os << "(th_let_pf _ (trust_f (iff "; Expr inputAssertion; @@ -730,7 +725,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, if (inputAssertions.size() == 0) { Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl; // For now just use the first assertion... - inputAssertion = *(ProofManager::currentPM()->begin_assertions()); + inputAssertion = + *(ProofManager::currentPM()->begin_input_core_assertions()); } else { if (inputAssertions.size() != 1) { Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl; @@ -739,13 +735,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, } } - if (!ProofManager::currentPM()->have_input_assertion(inputAssertion)) { - // The thing returned by traceDeps does not appear in the input assertions... - Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl; - // For now just use the first assertion... - inputAssertion = *(ProofManager::currentPM()->begin_assertions()); - } - Debug("pf::pm") << "Original assertion for " << *it << " is: " << inputAssertion @@ -796,8 +785,10 @@ void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) { NodeSet::const_iterator rewrite; for (rewrite = rewrites.begin(); rewrite != rewrites.end(); ++rewrite) { Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite << std::endl; - if (ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())) { - Assert(ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())); + if (ProofManager::currentPM()->have_input_core_assertion( + (*rewrite).toExpr())) { + Assert(ProofManager::currentPM()->have_input_core_assertion( + (*rewrite).toExpr())); Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl << "\tAdding filter: " << ProofManager::getPreprocessedAssertionName(*rewrite, "") diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index fa7224d72..13edab601 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -144,8 +144,7 @@ class ProofManager { TheoryProofEngine* d_theoryProof; // information that will need to be shared across proofs - ExprSet d_inputFormulas; - std::map d_inputFormulaToName; + std::map d_inputCoreFormulaToName; ExprSet d_inputCoreFormulas; ExprSet d_outputCoreFormulas; @@ -197,13 +196,14 @@ public: typedef ExprSet::const_iterator assertions_iterator; // iterate over the assertions (these are arbitrary boolean formulas) - assertions_iterator begin_assertions() const { - return d_inputFormulas.begin(); + assertions_iterator begin_input_core_assertions() const { + return d_inputCoreFormulas.begin(); } - assertions_iterator end_assertions() const { return d_inputFormulas.end(); } - size_t num_assertions() const { return d_inputFormulas.size(); } - bool have_input_assertion(const Expr& assertion) { - return d_inputFormulas.find(assertion) != d_inputFormulas.end(); + assertions_iterator end_input_core_assertions() const { + return d_inputCoreFormulas.end(); + } + bool have_input_core_assertion(const Expr& assertion) const { + return d_inputCoreFormulas.find(assertion) != d_inputCoreFormulas.end(); } //---from Morgan--- @@ -234,9 +234,6 @@ public: // for SMT variable names that have spaces and other things static std::string sanitize(TNode var); - /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/ - void addAssertion(Expr formula); - /** Public unsat core methods **/ void addCoreAssertion(Expr formula); diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 1912dbada..2d89bfe24 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -308,8 +308,10 @@ void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) { } void LFSCTheoryProofEngine::registerTermsFromAssertions() { - ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); - ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); + ProofManager::assertions_iterator it = + ProofManager::currentPM()->begin_input_core_assertions(); + ProofManager::assertions_iterator end = + ProofManager::currentPM()->end_input_core_assertions(); for(; it != end; ++it) { registerTerm(*it); @@ -321,14 +323,17 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions called" << std::endl << std::endl; - ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); - ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); + ProofManager::assertions_iterator it = + ProofManager::currentPM()->begin_input_core_assertions(); + ProofManager::assertions_iterator end = + ProofManager::currentPM()->end_input_core_assertions(); for (; it != end; ++it) { Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; os << "(% " << ProofManager::currentPM()->getInputFormulaName(*it) << " (th_holds "; - // Assertions appear before the global let map, so we use a dummpMap to avoid letification here. + // Assertions appear before the global let map, so we use a dummyMap to + // avoid letification here. ProofLetMap dummyMap; printBoundTerm(*it, os, dummyMap); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index a79416b76..a0066f9ff 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3835,6 +3835,8 @@ void SmtEnginePrivate::processAssertions() { // Add dummy assertion in last position - to be used as a // placeholder for any new assertions to get added + PROOF(ProofManager::currentPM()->addCoreAssertion( + NodeManager::currentNM()->mkConst(true).toExpr())); d_assertions.push_back(NodeManager::currentNM()->mkConst(true)); // any assertions added beyond realAssertionsEnd must NOT affect the // equisatisfiability @@ -3856,14 +3858,6 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl; dumpAssertions("post-definition-expansion", d_assertions); - // save the assertions now - THEORY_PROOF - ( - for (unsigned i = 0; i < d_assertions.size(); ++i) { - ProofManager::currentPM()->addAssertion(d_assertions[i].toExpr()); - } - ); - Debug("smt") << " d_assertions : " << d_assertions.size() << endl; if( options::ceGuidedInst() ){ -- cgit v1.2.3