From: Andrew Reynolds Date: Fri, 21 Aug 2020 17:08:14 +0000 (-0500) Subject: Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic... X-Git-Tag: cvc5-1.0.0~2968 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b8301cde27c455c8da3e9017072a577a0816939b;p=cvc5.git Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930) This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this. This addresses CVC4/cvc4-projects#113. Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB: QF_NIA: +484-53 unsat +792-440 sat QF_NRA: +32-19 unsat +57-23 sat However, this PR does not (yet) enable this method by default. Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions. --- diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml index 23ced4d8f..ab33f123c 100644 --- a/src/options/arith_options.toml +++ b/src/options/arith_options.toml @@ -533,6 +533,24 @@ header = "options/arith_options.h" read_only = true help = "whether to increment the precision for irrational function constraints" +[[option]] + name = "nlRlvMode" + category = "regular" + long = "nl-rlv=MODE" + type = "NlRlvMode" + default = "NONE" + help = "choose mode for using relevance of assertoins in non-linear arithmetic" + help_mode = "Modes for using relevance of assertoins in non-linear arithmetic." +[[option.mode.NONE]] + name = "none" + help = "Do not use relevance." +[[option.mode.INTERLEAVE]] + name = "interleave" + help = "Alternate rounds using relevance." +[[option.mode.ALWAYS]] + name = "always" + help = "Always use relevance." + [[option]] name = "brabTest" category = "regular" diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 84c994c3f..6ec9d8854 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -34,3 +34,11 @@ header = "options/theory_options.h" default = "true" read_only = true help = "condense values for functions in models rather than explicitly representing them" + +[[option]] + name = "relevanceFilter" + category = "regular" + long = "relevance-filter" + type = "bool" + default = "false" + help = "enable analysis of relevance of asserted literals with respect to the input formula" diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 5376d7418..7d2427015 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1307,6 +1307,22 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } + if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear() + && options::nlRlvMode() != options::NlRlvMode::NONE) + { + if (!options::relevanceFilter()) + { + if (options::relevanceFilter.wasSetByUser()) + { + Warning() << "SmtEngine: turning on relevance filtering to support " + "--nl-ext-rlv=" + << options::nlRlvMode() << std::endl; + } + // must use relevance filtering techniques + options::relevanceFilter.set(true); + } + } + // For now, these array theory optimizations do not support model-building if (options::produceModels() || options::produceAssignments() || options::checkModels()) diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp index daa36f972..cc10d6659 100644 --- a/src/theory/arith/nl/nl_model.cpp +++ b/src/theory/arith/nl/nl_model.cpp @@ -16,6 +16,7 @@ #include "expr/node_algorithm.h" #include "options/arith_options.h" +#include "options/theory_options.h" #include "theory/arith/arith_msum.h" #include "theory/arith/arith_utilities.h" #include "theory/rewriter.h" @@ -279,11 +280,6 @@ bool NlModel::checkModel(const std::vector& assertions, std::vector check_assertions; for (const Node& a : assertions) { - // don't have to check tautological literals - if (d_tautology.find(a) != d_tautology.end()) - { - continue; - } if (d_check_model_solved.find(a) == d_check_model_solved.end()) { Node av = a; @@ -455,52 +451,6 @@ void NlModel::setUsedApproximate() { d_used_approx = true; } bool NlModel::usedApproximate() const { return d_used_approx; } -void NlModel::addTautology(Node n) -{ - // ensure rewritten - n = Rewriter::rewrite(n); - std::unordered_set visited; - std::vector visit; - TNode cur; - visit.push_back(n); - do - { - cur = visit.back(); - visit.pop_back(); - if (visited.find(cur) == visited.end()) - { - visited.insert(cur); - if (cur.getKind() == AND) - { - // children of AND are also implied - for (const Node& cn : cur) - { - visit.push_back(cn); - } - } - else - { - // is this an arithmetic literal? - Node atom = cur.getKind() == NOT ? cur[0] : cur; - if ((atom.getKind() == EQUAL && atom[0].getType().isReal()) - || atom.getKind() == LEQ) - { - // Add to tautological literals if it does not contain - // non-linear multiplication. We cannot consider literals - // with non-linear multiplication to be tautological since this - // model object is responsible for checking whether they hold. - // (TODO, cvc4-projects #113: revisit this). - if (!expr::hasSubtermKind(NONLINEAR_MULT, atom)) - { - Trace("nl-taut") << "Tautological literal: " << atom << std::endl; - d_tautology.insert(cur); - } - } - } - } - } while (!visit.empty()); -} - bool NlModel::solveEqualitySimple(Node eq, unsigned d, std::vector& lemmas) diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h index 1e6f6c8f3..dcbd9cce7 100644 --- a/src/theory/arith/nl/nl_model.h +++ b/src/theory/arith/nl/nl_model.h @@ -166,22 +166,6 @@ class NlModel void setUsedApproximate(); /** Did we use an approximation during this check? */ bool usedApproximate() const; - /** - * This states that formula n is a tautology (satisfied in all models). - * We call this on internally generated lemmas. This method computes a - * set of literals that are implied by n, that are hence tautological - * as well, such as: - * l_pi <= real.pi <= u_pi (pi approximations) - * sin(x) = -1*sin(-x) - * where these literals are internally generated for the purposes - * of guiding the models of the linear solver. - * - * TODO (cvc4-projects #113: would be helpful if we could do this even - * more aggressively by ignoring all internally generated literals. - * - * Tautological literals do not need be checked during checkModel. - */ - void addTautology(Node n); //------------------------------ end recording model substitutions and bounds /** @@ -334,8 +318,6 @@ class NlModel std::unordered_map d_check_model_solved; /** did we use an approximation on this call to last-call effort? */ bool d_used_approx; - /** the set of all tautological literals */ - std::unordered_set d_tautology; }; /* class NlModel */ } // namespace nl diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 9dbb95d93..fb5b6eec8 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -38,6 +38,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, d_containing(containing), d_ee(ee), d_needsLastCall(false), + d_checkCounter(0), d_extTheory(&containing), d_model(containing.getSatContext()), d_trSlv(d_model), @@ -182,8 +183,6 @@ void NonlinearExtension::sendLemmas(const std::vector& out) d_lemmas.insert(lem); } d_stats.d_inferences << nlem.d_id; - // also indicate this is a tautology - d_model.addTautology(lem); } } @@ -192,6 +191,22 @@ void NonlinearExtension::processSideEffect(const NlLemma& se) d_trSlv.processSideEffect(se); } +void NonlinearExtension::computeRelevantAssertions( + const std::vector& assertions, std::vector& keep) +{ + Trace("nl-ext-rlv") << "Compute relevant assertions..." << std::endl; + Valuation v = d_containing.getValuation(); + for (const Node& a : assertions) + { + if (v.isRelevant(a)) + { + keep.push_back(a); + } + } + Trace("nl-ext-rlv") << "...keep " << keep.size() << "/" << assertions.size() + << " assertions" << std::endl; +} + unsigned NonlinearExtension::filterLemma(NlLemma lem, std::vector& out) { Trace("nl-ext-lemma-debug") @@ -251,6 +266,16 @@ unsigned NonlinearExtension::filterLemmas(std::vector& lemmas, void NonlinearExtension::getAssertions(std::vector& assertions) { Trace("nl-ext") << "Getting assertions..." << std::endl; + bool useRelevance = false; + if (options::nlRlvMode() == options::NlRlvMode::INTERLEAVE) + { + useRelevance = (d_checkCounter % 2); + } + else if (options::nlRlvMode() == options::NlRlvMode::ALWAYS) + { + useRelevance = true; + } + Valuation v = d_containing.getValuation(); NodeManager* nm = NodeManager::currentNM(); // get the assertions std::map init_bounds[2]; @@ -264,6 +289,11 @@ void NonlinearExtension::getAssertions(std::vector& assertions) nassertions++; const Assertion& assertion = *it; Node lit = assertion.d_assertion; + if (useRelevance && !v.isRelevant(lit)) + { + // not relevant, skip + continue; + } init_assertions.insert(lit); // check for concrete bounds bool pol = lit.getKind() != NOT; @@ -390,7 +420,6 @@ std::vector NonlinearExtension::checkModelEval( } bool NonlinearExtension::checkModel(const std::vector& assertions, - const std::vector& false_asserts, std::vector& lemmas, std::vector& gs) { @@ -398,7 +427,17 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, // get the presubstitution Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; - std::vector passertions = assertions; + std::vector passertions; + if (options::nlRlvMode() != options::NlRlvMode::NONE) + { + // only keep the relevant assertions (those required for showing input + // is satisfied) + computeRelevantAssertions(assertions, passertions); + } + else + { + passertions = assertions; + } if (options::nlExt()) { // preprocess the assertions with the trancendental solver @@ -681,6 +720,7 @@ void NonlinearExtension::check(Theory::Effort e) bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) { ++(d_stats.d_mbrRuns); + d_checkCounter++; // get the assertions std::vector assertions; @@ -786,7 +826,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector& mlems) // error bounds on the Taylor approximation of transcendental functions. std::vector lemmas; std::vector gs; - if (checkModel(assertions, false_asserts, lemmas, gs)) + if (checkModel(assertions, lemmas, gs)) { complete_status = 1; } diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 6fb8dbbfa..ee58a9e2e 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -254,11 +254,12 @@ class NonlinearExtension * ensureLiteral respectively. */ bool checkModel(const std::vector& assertions, - const std::vector& false_asserts, std::vector& lemmas, std::vector& gs); //---------------------------end check model - + /** compute relevant assertions */ + void computeRelevantAssertions(const std::vector& assertions, + std::vector& keep); /** * Potentially adds lemmas to the set out and clears lemmas. Returns * the number of lemmas added to out. We do not add lemmas that have already @@ -293,6 +294,11 @@ class NonlinearExtension NlStats d_stats; // needs last call effort bool d_needsLastCall; + /** + * The number of times we have the called main check method + * (modelBasedRefinement). This counter is used for interleaving strategies. + */ + unsigned d_checkCounter; /** Extended theory, responsible for context-dependent simplification. */ ExtTheory d_extTheory; /** The non-linear model object diff --git a/src/theory/output_channel.cpp b/src/theory/output_channel.cpp index 9fe973569..c918438ee 100644 --- a/src/theory/output_channel.cpp +++ b/src/theory/output_channel.cpp @@ -49,6 +49,10 @@ bool isLemmaPropertySendAtoms(LemmaProperty p) { return (p & LemmaProperty::SEND_ATOMS) != LemmaProperty::NONE; } +bool isLemmaPropertyNeedsJustify(LemmaProperty p) +{ + return (p & LemmaProperty::NEEDS_JUSTIFY) != LemmaProperty::NONE; +} std::ostream& operator<<(std::ostream& out, LemmaProperty p) { @@ -71,6 +75,10 @@ std::ostream& operator<<(std::ostream& out, LemmaProperty p) { out << " SEND_ATOMS"; } + if (isLemmaPropertyNeedsJustify(p)) + { + out << " NEEDS_JUSTIFY"; + } out << " }"; } return out; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index d65d4fc53..0fd610c58 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -42,7 +42,9 @@ enum class LemmaProperty : uint32_t // whether the lemma needs preprocessing PREPROCESS = 2, // whether the processing of the lemma should send atoms to the caller - SEND_ATOMS = 4 + SEND_ATOMS = 4, + // whether the lemma is part of the justification for answering "sat" + NEEDS_JUSTIFY = 8 }; /** Define operator lhs | rhs */ LemmaProperty operator|(LemmaProperty lhs, LemmaProperty rhs); @@ -58,6 +60,8 @@ bool isLemmaPropertyRemovable(LemmaProperty p); bool isLemmaPropertyPreprocess(LemmaProperty p); /** is the send atoms bit set on p? */ bool isLemmaPropertySendAtoms(LemmaProperty p); +/** is the needs justify bit set on p? */ +bool isLemmaPropertyNeedsJustify(LemmaProperty p); /** * Writes an lemma property name to a stream. diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 9fdf7e7aa..9dc483f93 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -962,7 +962,8 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); + getOutputChannel().lemma( + lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY); } return; } diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index a8ebd921a..dce038fbf 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -374,8 +374,12 @@ void InferenceManager::doPendingLemmas() d_termReg.registerTermAtomic(n, sks.first); } } - - d_out.lemma(lem); + LemmaProperty p = LemmaProperty::NONE; + if (ii.d_id == Inference::REDUCTION) + { + p |= LemmaProperty::NEEDS_JUSTIFY; + } + d_out.lemma(lem, p); } // process the pending require phase calls for (const std::pair& prp : d_pendingReqPhase) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7431b26e4..f0966a96d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -47,6 +47,7 @@ #include "theory/quantifiers/fmf/model_engine.h" #include "theory/quantifiers/theory_quantifiers.h" #include "theory/quantifiers_engine.h" +#include "theory/relevance_manager.h" #include "theory/rewriter.h" #include "theory/theory.h" #include "theory/theory_model.h" @@ -152,6 +153,12 @@ void TheoryEngine::finishInit() { d_userContext, "DefaultModel", options::assignFunctionValues()); d_aloc_curr_model = true; } + // create the relevance filter if any option requires it + if (options::relevanceFilter()) + { + d_relManager.reset( + new RelevanceManager(d_userContext, theory::Valuation(this))); + } //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder if( d_curr_model_builder==NULL ){ @@ -201,6 +208,7 @@ TheoryEngine::TheoryEngine(context::Context* context, d_eeDistributed(nullptr), d_quantEngine(nullptr), d_decManager(new DecisionManager(userContext)), + d_relManager(nullptr), d_curr_model(nullptr), d_aloc_curr_model(false), d_curr_model_builder(nullptr), @@ -456,6 +464,12 @@ void TheoryEngine::check(Theory::Effort effort) { // If in full effort, we have a fake new assertion just to jumpstart the checking if (Theory::fullEffort(effort)) { d_factsAsserted = true; + // Reset round for the relevance manager, which notice only sets a flag + // to indicate that its information must be recomputed. + if (d_relManager != nullptr) + { + d_relManager->resetRound(); + } } // Check until done @@ -938,6 +952,16 @@ void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) { CVC4_FOR_EACH_THEORY; } +bool TheoryEngine::isRelevant(Node lit) const +{ + if (d_relManager != nullptr) + { + return d_relManager->isRelevant(lit); + } + // otherwise must assume its relevant + return true; +} + void TheoryEngine::shutdown() { // Set this first; if a Theory shutdown() throws an exception, // at least the destruction of the TheoryEngine won't confound @@ -998,6 +1022,10 @@ void TheoryEngine::notifyPreprocessedAssertions( theoryOf(theoryId)->ppNotifyAssertions(assertions); } } + if (d_relManager != nullptr) + { + d_relManager->notifyPreprocessedAssertions(assertions); + } } bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) { @@ -1659,6 +1687,14 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, lemmas.push_back(newLemmas[i].getNode()); } + // If specified, we must add this lemma to the set of those that need to be + // justified, where note we pass all auxiliary lemmas in lemmas, since these + // by extension must be justified as well. + if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p)) + { + d_relManager->notifyPreprocessedAssertions(lemmas.ref()); + } + // assert lemmas to prop engine for (size_t i = 0, lsize = lemmas.size(); i < lsize; ++i) { @@ -1999,6 +2035,11 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) { it != it_end; ++it) { Node assertion = (*it).d_assertion; + if (!isRelevant(assertion)) + { + // not relevant, skip + continue; + } Node val = getModel()->getValue(assertion); if (val != d_true) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 91984daca..549f4078e 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -35,7 +35,6 @@ #include "prop/prop_engine.h" #include "smt/command.h" #include "theory/atom_requests.h" -#include "theory/decision_manager.h" #include "theory/engine_output_channel.h" #include "theory/interrupted.h" #include "theory/rewriter.h" @@ -92,6 +91,9 @@ namespace theory { class TheoryEngineModelBuilder; class EqEngineManagerDistributed; + class DecisionManager; + class RelevanceManager; + namespace eq { class EqualityEngine; }/* CVC4::theory::eq namespace */ @@ -165,6 +167,8 @@ class TheoryEngine { * The decision manager */ std::unique_ptr d_decManager; + /** The relevance manager */ + std::unique_ptr d_relManager; /** * Default model object @@ -498,6 +502,12 @@ public: inline bool needCheck() const { return d_outputChannelUsed || d_lemmasAdded; } + /** + * Is the literal lit (possibly) critical for satisfying the input formula in + * the current context? This call is applicable only during collectModelInfo + * or during LAST_CALL effort. + */ + bool isRelevant(Node lit) const; /** * This is called at shutdown time by the SmtEngine, just before diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 1a2b9220a..9375a4868 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -172,5 +172,7 @@ bool Valuation::needCheck() const{ return d_engine->needCheck(); } +bool Valuation::isRelevant(Node lit) const { return d_engine->isRelevant(lit); } + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index d8d57d2e5..35d990715 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -156,7 +156,13 @@ public: /** need check ? */ bool needCheck() const; - + + /** + * Is the literal lit (possibly) critical for satisfying the input formula in + * the current context? This call is applicable only during collectModelInfo + * or during LAST_CALL effort. + */ + bool isRelevant(Node lit) const; };/* class Valuation */ }/* CVC4::theory namespace */ diff --git a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc index d01d7b7d2..eaefbe651 100644 --- a/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc +++ b/test/regress/regress0/quantifiers/cegqi-nl-simp.cvc @@ -1,2 +1,3 @@ +% COMMAND-LINE: --nl-rlv=none % EXPECT: entailed QUERY FORALL (x:INT) : EXISTS (y:INT) : (x*y=x) ; diff --git a/test/regress/regress1/nl/issue3647.smt2 b/test/regress/regress1/nl/issue3647.smt2 index 0fc0f55f9..6c66d2e4c 100644 --- a/test/regress/regress1/nl/issue3647.smt2 +++ b/test/regress/regress1/nl/issue3647.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --no-check-models --produce-models --decision=internal +; COMMAND-LINE: --no-check-models --produce-models --decision=internal --nl-rlv=always ; EXPECT: sat (set-logic ALL) (set-info :status sat) diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2 index d9e12c7b4..4fb0732a3 100644 --- a/test/regress/regress1/nl/sin1-deq-sat.smt2 +++ b/test/regress/regress1/nl/sin1-deq-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2 index d2a21fa60..9c1d9cef6 100644 --- a/test/regress/regress1/nl/sin1-sat.smt2 +++ b/test/regress/regress1/nl/sin1-sat.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models --nl-rlv=always ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) diff --git a/test/regress/regress1/sygus/issue3648.smt2 b/test/regress/regress1/sygus/issue3648.smt2 index e7b7547c4..2fc1a6115 100644 --- a/test/regress/regress1/sygus/issue3648.smt2 +++ b/test/regress/regress1/sygus/issue3648.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -; COMMAND-LINE: --sygus-inference --no-check-models +; COMMAND-LINE: --sygus-inference --no-check-models --nl-rlv=always (set-logic ALL) (declare-fun a () Real) (assert (> a 0.000001))