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/nl/nl_model.cpp | |
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/nl/nl_model.cpp')
-rw-r--r-- | src/theory/arith/nl/nl_model.cpp | 52 |
1 files changed, 1 insertions, 51 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) |