diff options
| -rw-r--r-- | src/expr/node_algorithm.cpp | 26 | ||||
| -rw-r--r-- | src/expr/node_algorithm.h | 7 | ||||
| -rw-r--r-- | src/theory/arith/nl_model.cpp | 51 | ||||
| -rw-r--r-- | src/theory/arith/nl_model.h | 19 | ||||
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 2 |
5 files changed, 105 insertions, 0 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 9619e69d1..595adda55 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -129,6 +129,32 @@ bool hasSubtermMulti(TNode n, TNode t) return false; } +bool hasSubtermKind(Kind k, Node 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() == k) + { + return true; + } + for (const Node& cn : cur) + { + visit.push_back(cn); + } + } + } while (!visit.empty()); + return false; +} + bool hasSubterm(TNode n, const std::vector<Node>& t, bool strict) { if (t.empty()) diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h index 929e1c5ef..e47029284 100644 --- a/src/expr/node_algorithm.h +++ b/src/expr/node_algorithm.h @@ -45,6 +45,13 @@ bool hasSubterm(TNode n, TNode t, bool strict = false); bool hasSubtermMulti(TNode n, TNode t); /** + * @param k The kind of node to check + * @param n The node to search in. + * @return true iff there is a term in n that has kind k + */ +bool hasSubtermKind(Kind k, Node n); + +/** * Check if the node n has a subterm that occurs in t. * @param n The node to search in * @param t The set of subterms to search for diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index 929eb4acc..3c1d5f1e9 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -278,6 +278,11 @@ 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; @@ -424,6 +429,52 @@ 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<Node>& lemmas) diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h index 354f6f71c..a8746ca2e 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl_model.h @@ -163,6 +163,23 @@ class NlModel void setUsedApproximate(); /** Did we use an approximation during this check? */ bool usedApproximate() const; + /** Set tautology + * + * 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 /** print model value, for debugging. @@ -314,6 +331,8 @@ 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 arith diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index bcf7cae14..94c925131 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -559,6 +559,8 @@ void NonlinearExtension::sendLemmas(const std::vector<Node>& out, { d_lemmas.insert(lem); } + // also indicate this is a tautology + d_model.addTautology(lem); } } |