diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-21 12:08:14 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-08-21 12:08:14 -0500 |
commit | b8301cde27c455c8da3e9017072a577a0816939b (patch) | |
tree | 816d1cccdda0625419b1b088644bafb85a857d14 /src/theory/arith | |
parent | 905dc2b51fd0145e0bb69a166c06a1731ef4c44b (diff) |
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.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/nl/nl_model.cpp | 52 | ||||
-rw-r--r-- | src/theory/arith/nl/nl_model.h | 18 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 50 | ||||
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 10 |
4 files changed, 54 insertions, 76 deletions
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<Node>& assertions, std::vector<Node> 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<TNode, TNodeHashFunction> visited; - std::vector<TNode> 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<NlLemma>& 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<Node, Node, NodeHashFunction> 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<Node, NodeHashFunction> 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<NlLemma>& 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<Node>& assertions, std::vector<Node>& 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<NlLemma>& out) { Trace("nl-ext-lemma-debug") @@ -251,6 +266,16 @@ unsigned NonlinearExtension::filterLemmas(std::vector<NlLemma>& lemmas, void NonlinearExtension::getAssertions(std::vector<Node>& 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<Node, Rational> init_bounds[2]; @@ -264,6 +289,11 @@ void NonlinearExtension::getAssertions(std::vector<Node>& 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<Node> NonlinearExtension::checkModelEval( } bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, - const std::vector<Node>& false_asserts, std::vector<NlLemma>& lemmas, std::vector<Node>& gs) { @@ -398,7 +427,17 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, // get the presubstitution Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; - std::vector<Node> passertions = assertions; + std::vector<Node> 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<NlLemma>& mlems) { ++(d_stats.d_mbrRuns); + d_checkCounter++; // get the assertions std::vector<Node> assertions; @@ -786,7 +826,7 @@ bool NonlinearExtension::modelBasedRefinement(std::vector<NlLemma>& mlems) // error bounds on the Taylor approximation of transcendental functions. std::vector<NlLemma> lemmas; std::vector<Node> 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<Node>& assertions, - const std::vector<Node>& false_asserts, std::vector<NlLemma>& lemmas, std::vector<Node>& gs); //---------------------------end check model - + /** compute relevant assertions */ + void computeRelevantAssertions(const std::vector<Node>& assertions, + std::vector<Node>& 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 |