diff options
-rw-r--r-- | src/options/proof_options | 3 | ||||
-rw-r--r-- | src/proof/proof_manager.cpp | 135 | ||||
-rw-r--r-- | src/proof/proof_manager.h | 15 | ||||
-rw-r--r-- | src/proof/theory_proof.cpp | 5 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 7 |
5 files changed, 145 insertions, 20 deletions
diff --git a/src/options/proof_options b/src/options/proof_options index 8a496bda6..322ef5a9c 100644 --- a/src/options/proof_options +++ b/src/options/proof_options @@ -11,4 +11,7 @@ option lfscLetification --lfsc-letification bool :default true option aggressiveCoreMin --aggressive-core-min bool :default false turns on aggressive unsat core minimization (experimental) +option fewerPreprocessingHoles --fewer-preprocessing-holes bool :default false :read-write + try to eliminate preprocessing holes in proofs + endmodule diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e987f1c6f..1c9bb0ff0 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -211,6 +211,10 @@ std::string ProofManager::getLitName(prop::SatLiteral lit, std::string ProofManager::getPreprocessedAssertionName(Node node, const std::string& prefix) { + if (currentPM()->d_assertionFilters.find(node) != currentPM()->d_assertionFilters.end()) { + return currentPM()->d_assertionFilters[node]; + } + node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node; return append(prefix+".PA", node.getId()); } @@ -218,6 +222,9 @@ std::string ProofManager::getAssertionName(Node node, const std::string& prefix) { return append(prefix+".A", node.getId()); } +std::string ProofManager::getInputFormulaName(const Expr& expr) { + return currentPM()->d_inputFormulaToName[expr]; +} std::string ProofManager::getAtomName(TNode atom, const std::string& prefix) { @@ -252,7 +259,7 @@ std::string ProofManager::sanitize(TNode node) { return name; } -void ProofManager::traceDeps(TNode n) { +void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) { Debug("cores") << "trace deps " << n << std::endl; if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) || (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) { @@ -261,7 +268,7 @@ void ProofManager::traceDeps(TNode n) { if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) { // originating formula was in core set Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl; - d_outputCoreFormulas.insert(n.toExpr()); + coreAssertions->insert(n.toExpr()); } else { Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl; if(d_deps.find(n) == d_deps.end()) { @@ -272,7 +279,7 @@ void ProofManager::traceDeps(TNode n) { for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) { Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl; if( !(*i).isNull() ){ - traceDeps(*i); + traceDeps(*i, coreAssertions); } } } @@ -296,7 +303,7 @@ void ProofManager::traceUnsatCore() { rule == RULE_GIVEN) { // trace dependences back to actual assertions // (this adds them to the unsat core) - traceDeps(node); + traceDeps(node, &d_outputCoreFormulas); } } } @@ -444,6 +451,9 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { 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) { @@ -468,6 +478,10 @@ void ProofManager::addUnsatCore(Expr formula) { d_outputCoreFormulas.insert(formula); } +void ProofManager::addAssertionFilter(const Node& node, const std::string& rewritten) { + d_assertionFilters[node] = rewritten; +} + void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } @@ -682,21 +696,118 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl; - for (; it != end; ++it) { - os << "(th_let_pf _ "; + if (options::fewerPreprocessingHoles()) { + // Check for assertions that did not get rewritten, and update the printing filter. + checkUnrewrittenAssertion(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())) { + os << "(th_let_pf _ (trust_f (iff "; + + Expr inputAssertion; + + if (((*it).isConst() && *it == NodeManager::currentNM()->mkConst<bool>(true)) || + ((*it).getKind() == kind::NOT && (*it)[0] == NodeManager::currentNM()->mkConst<bool>(false))) { + inputAssertion = NodeManager::currentNM()->mkConst<bool>(true).toExpr(); + } else { + // Figure out which input assertion led to this assertion + ExprSet inputAssertions; + ProofManager::currentPM()->traceDeps(*it, &inputAssertions); + + Debug("pf::pm") << "Original assertions for " << *it << " are: " << std::endl; + + ProofManager::assertions_iterator assertionIt; + for (assertionIt = inputAssertions.begin(); assertionIt != inputAssertions.end(); ++assertionIt) { + Debug("pf::pm") << "\t" << *assertionIt << std::endl; + } + + 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()); + } else { + if (inputAssertions.size() != 1) { + Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl; + } + inputAssertion = *inputAssertions.begin(); + } + } + + 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 + << ", AKA " + << ProofManager::currentPM()->getInputFormulaName(inputAssertion) + << std::endl; + + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap); + os << " "; + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + + os << "))"; + os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; + paren << "))"; - //TODO - os << "(trust_f "; - ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); - os << ") "; + std::ostringstream rewritten; - os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; - paren << "))"; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << ProofManager::currentPM()->getInputFormulaName(inputAssertion); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << ProofManager::getPreprocessedAssertionName(*it, ""); + rewritten << "))"; + + ProofManager::currentPM()->addAssertionFilter(*it, rewritten.str()); + } + } + } else { + for (; it != end; ++it) { + os << "(th_let_pf _ "; + + //TODO + os << "(trust_f "; + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + os << ") "; + + os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; + paren << "))"; + } } os << "\n"; } +void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) { + Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl; + + 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())); + Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl + << "\tAdding filter: " + << ProofManager::getPreprocessedAssertionName(*rewrite, "") + << " --> " + << ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr()) + << std::endl; + ProofManager::currentPM()->addAssertionFilter(*rewrite, + ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr())); + } else { + Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion WAS rewritten! " << *rewrite << std::endl; + } + } +} + //---from Morgan--- bool ProofManager::hasOp(TNode n) const { diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index cb5a2bdd1..fa7224d72 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -145,6 +145,7 @@ class ProofManager { // information that will need to be shared across proofs ExprSet d_inputFormulas; + std::map<Expr, std::string> d_inputFormulaToName; ExprSet d_inputCoreFormulas; ExprSet d_outputCoreFormulas; @@ -156,12 +157,11 @@ class ProofManager { ProofFormat d_format; // used for now only in debug builds NodeToNodes d_deps; - // trace dependences back to unsat core - void traceDeps(TNode n); std::set<Type> d_printedTypes; std::map<std::string, std::string> d_rewriteFilters; + std::map<Node, std::string> d_assertionFilters; std::vector<RewriteLogEntry> d_rewriteLog; @@ -202,6 +202,9 @@ public: } 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(); + } //---from Morgan--- Node mkOp(TNode n); @@ -220,6 +223,7 @@ public: static std::string getLearntClauseName(ClauseId id, const std::string& prefix = ""); static std::string getPreprocessedAssertionName(Node node, const std::string& prefix = ""); static std::string getAssertionName(Node node, const std::string& prefix = ""); + static std::string getInputFormulaName(const Expr& expr); static std::string getVarName(prop::SatVariable var, const std::string& prefix = ""); static std::string getAtomName(prop::SatVariable var, const std::string& prefix = ""); @@ -239,6 +243,8 @@ public: void addDependence(TNode n, TNode dep); void addUnsatCore(Expr formula); + // trace dependences back to unsat core + void traceDeps(TNode n, ExprSet* coreAssertions); void traceUnsatCore(); assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); } assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); } @@ -260,6 +266,8 @@ public: void addRewriteFilter(const std::string &original, const std::string &substitute); void clearRewriteFilters(); + void addAssertionFilter(const Node& node, const std::string& rewritten); + static void registerRewrite(unsigned ruleId, Node original, Node result); static void clearRewriteLog(); @@ -287,6 +295,9 @@ class LFSCProof : public Proof { std::ostream& os, std::ostream& paren, ProofLetMap& globalLetMap); + + void checkUnrewrittenAssertion(const NodeSet& assertions); + public: LFSCProof(SmtEngine* smtEngine, LFSCCoreSatProof* sat, diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index d29fc8615..1912dbada 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -321,15 +321,12 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions called" << std::endl << std::endl; - unsigned counter = 0; ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); for (; it != end; ++it) { Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; - std::ostringstream name; - name << "A" << counter++; - os << "(% " << name.str() << " (th_holds "; + os << "(% " << ProofManager::currentPM()->getInputFormulaName(*it) << " (th_holds "; // Assertions appear before the global let map, so we use a dummpMap to avoid letification here. ProofLetMap dummyMap; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b76b90e84..d7b7f9c3e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -57,6 +57,7 @@ #include "options/open_ostream.h" #include "options/option_exception.h" #include "options/printer_options.h" +#include "options/proof_options.h" #include "options/prop_options.h" #include "options/quantifiers_options.h" #include "options/set_language.h" @@ -92,9 +93,9 @@ #include "theory/quantifiers/fun_def_process.h" #include "theory/quantifiers/macros.h" #include "theory/quantifiers/quantifiers_rewriter.h" +#include "theory/sep/theory_sep.h" #include "theory/sort_inference.h" #include "theory/strings/theory_strings.h" -#include "theory/sep/theory_sep.h" #include "theory/substitutions.h" #include "theory/theory_engine.h" #include "theory/theory_model.h" @@ -4283,8 +4284,10 @@ void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput) PROOF( if( inInput ){ // n is an input assertion - if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores()) + if (inUnsatCore || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) { + ProofManager::currentPM()->addCoreAssertion(n.toExpr()); + } }else{ // n is the result of an unknown preprocessing step, add it to dependency map to null ProofManager::currentPM()->addDependence(n, Node::null()); |