From 5c481b34eef5860d29ea1f2f62cea696fea01619 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Oct 2021 14:15:29 -0500 Subject: [PATCH] Split entailment check from term database (#7342) Towards addressing some bottlenecks on Facebook benchmarks. --- src/CMakeLists.txt | 2 + .../quantifiers/conjecture_generator.cpp | 6 +- .../quantifiers/ematching/ho_trigger.cpp | 4 +- src/theory/quantifiers/entailment_check.cpp | 443 ++++++++++++++++++ src/theory/quantifiers/entailment_check.h | 150 ++++++ src/theory/quantifiers/instantiate.cpp | 10 +- .../quantifiers/quant_conflict_find.cpp | 30 +- src/theory/quantifiers/term_database.cpp | 360 -------------- src/theory/quantifiers/term_database.h | 90 ---- src/theory/quantifiers/term_registry.cpp | 7 + src/theory/quantifiers/term_registry.h | 5 + 11 files changed, 632 insertions(+), 475 deletions(-) create mode 100644 src/theory/quantifiers/entailment_check.cpp create mode 100644 src/theory/quantifiers/entailment_check.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 31dccdbc6..374c57726 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -805,6 +805,8 @@ libcvc5_add_sources( theory/quantifiers/ematching/trigger_trie.h theory/quantifiers/ematching/var_match_generator.cpp theory/quantifiers/ematching/var_match_generator.h + theory/quantifiers/entailment_check.cpp + theory/quantifiers/entailment_check.h theory/quantifiers/equality_query.cpp theory/quantifiers/equality_query.h theory/quantifiers/expr_miner.cpp diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index b98088a71..d778a679e 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -245,6 +245,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) // now, do instantiation-based merging for each of these terms Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl; //merge all pending equalities + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); while( !d_upendingAdds.empty() ){ Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl; std::vector< Node > pending; @@ -256,7 +257,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add) Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl; std::vector< Node > eq_terms; //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine - Node gt = getTermDatabase()->evaluateTerm(t); + Node gt = echeck->evaluateTerm(t); if( !gt.isNull() && gt!=t ){ eq_terms.push_back( gt ); } @@ -1362,7 +1363,8 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode } Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl; //get the representative of rhs with substitution subs - TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true ); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); + TNode grhs = echeck->getEntailedTerm(rhs, subs, true); Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl; if( !grhs.isNull() ){ if( glhs!=grhs ){ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index a8ab760ce..d2b0b0542 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -238,6 +238,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) d_lchildren.clear(); d_arg_to_arg_rep.clear(); d_arg_vector.clear(); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); for (std::pair >& ha : ho_var_apps_subs) { TNode var = ha.first; @@ -291,8 +292,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector& m, InferenceId id) { if (!d_qstate.areEqual(itf->second, args[k])) { - if (!d_treg.getTermDatabase()->isEntailed( - itf->second.eqNode(args[k]), true)) + if (!echeck->isEntailed(itf->second.eqNode(args[k]), true)) { fixed_vals[k] = Node::null(); } diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp new file mode 100644 index 000000000..f27e14121 --- /dev/null +++ b/src/theory/quantifiers/entailment_check.cpp @@ -0,0 +1,443 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of entailment check class. + */ + +#include "theory/quantifiers/entailment_check.h" + +#include "theory/quantifiers/quantifiers_state.h" +#include "theory/quantifiers/term_database.h" + +using namespace cvc5::kind; +using namespace cvc5::context; + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb) + : EnvObj(env), d_qstate(qs), d_tdb(tdb) +{ + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); +} + +EntailmentCheck::~EntailmentCheck() {} +Node EntailmentCheck::evaluateTerm2(TNode n, + std::map& visited, + std::vector& exp, + bool useEntailmentTests, + bool computeExp, + bool reqHasTerm) +{ + std::map::iterator itv = visited.find(n); + if (itv != visited.end()) + { + return itv->second; + } + size_t prevSize = exp.size(); + Trace("term-db-eval") << "evaluate term : " << n << std::endl; + Node ret = n; + if (n.getKind() == FORALL || n.getKind() == BOUND_VARIABLE) + { + // do nothing + } + else if (d_qstate.hasTerm(n)) + { + Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; + ret = d_qstate.getRepresentative(n); + if (computeExp) + { + if (n != ret) + { + exp.push_back(n.eqNode(ret)); + } + } + reqHasTerm = false; + } + else if (n.hasOperator()) + { + std::vector args; + bool ret_set = false; + Kind k = n.getKind(); + std::vector tempExp; + for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = evaluateTerm2( + n[i], visited, tempExp, useEntailmentTests, computeExp, reqHasTerm); + if (c.isNull()) + { + ret = Node::null(); + ret_set = true; + break; + } + else if (c == d_true || c == d_false) + { + // short-circuiting + if ((k == AND && c == d_false) || (k == OR && c == d_true)) + { + ret = c; + ret_set = true; + reqHasTerm = false; + break; + } + else if (k == ITE && i == 0) + { + ret = evaluateTerm2(n[c == d_true ? 1 : 2], + visited, + tempExp, + useEntailmentTests, + computeExp, + reqHasTerm); + ret_set = true; + reqHasTerm = false; + break; + } + } + if (computeExp) + { + exp.insert(exp.end(), tempExp.begin(), tempExp.end()); + } + Trace("term-db-eval") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + if (ret_set) + { + // if we short circuited + if (computeExp) + { + exp.clear(); + exp.insert(exp.end(), tempExp.begin(), tempExp.end()); + } + } + else + { + // get the (indexed) operator of n, if it exists + TNode f = d_tdb.getMatchOperator(n); + // if it is an indexed term, return the congruent term + if (!f.isNull()) + { + // if f is congruent to a term indexed by this class + TNode nn = d_tdb.getCongruentTerm(f, args); + Trace("term-db-eval") << " got congruent term " << nn + << " from DB for " << n << std::endl; + if (!nn.isNull()) + { + if (computeExp) + { + Assert(nn.getNumChildren() == n.getNumChildren()); + for (size_t i = 0, nchild = nn.getNumChildren(); i < nchild; i++) + { + if (nn[i] != n[i]) + { + exp.push_back(nn[i].eqNode(n[i])); + } + } + } + ret = d_qstate.getRepresentative(nn); + Trace("term-db-eval") << "return rep" << std::endl; + ret_set = true; + reqHasTerm = false; + Assert(!ret.isNull()); + if (computeExp) + { + if (n != ret) + { + exp.push_back(nn.eqNode(ret)); + } + } + } + } + if (!ret_set) + { + Trace("term-db-eval") << "return rewrite" << std::endl; + // a theory symbol or a new UF term + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + args.insert(args.begin(), n.getOperator()); + } + ret = NodeManager::currentNM()->mkNode(n.getKind(), args); + ret = rewrite(ret); + if (ret.getKind() == EQUAL) + { + if (d_qstate.areDisequal(ret[0], ret[1])) + { + ret = d_false; + } + } + if (useEntailmentTests) + { + if (ret.getKind() == EQUAL || ret.getKind() == GEQ) + { + Valuation& val = d_qstate.getValuation(); + for (unsigned j = 0; j < 2; j++) + { + std::pair et = val.entailmentCheck( + options::TheoryOfMode::THEORY_OF_TYPE_BASED, + j == 0 ? ret : ret.negate()); + if (et.first) + { + ret = j == 0 ? d_true : d_false; + if (computeExp) + { + exp.push_back(et.second); + } + break; + } + } + } + } + } + } + } + // must have the term + if (reqHasTerm && !ret.isNull()) + { + Kind k = ret.getKind(); + if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT + && k != FORALL) + { + if (!d_qstate.hasTerm(ret)) + { + ret = Node::null(); + } + } + } + Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret + << ", reqHasTerm = " << reqHasTerm << std::endl; + // clear the explanation if failed + if (computeExp && ret.isNull()) + { + exp.resize(prevSize); + } + visited[n] = ret; + return ret; +} + +TNode EntailmentCheck::getEntailedTerm2(TNode n, + std::map& subs, + bool subsRep, + bool hasSubs) +{ + Trace("term-db-entail") << "get entailed term : " << n << std::endl; + if (d_qstate.hasTerm(n)) + { + Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; + return n; + } + else if (n.getKind() == BOUND_VARIABLE) + { + if (hasSubs) + { + std::map::iterator it = subs.find(n); + if (it != subs.end()) + { + Trace("term-db-entail") + << "...substitution is : " << it->second << std::endl; + if (subsRep) + { + Assert(d_qstate.hasTerm(it->second)); + Assert(d_qstate.getRepresentative(it->second) == it->second); + return it->second; + } + return getEntailedTerm2(it->second, subs, subsRep, hasSubs); + } + } + } + else if (n.getKind() == ITE) + { + for (uint32_t i = 0; i < 2; i++) + { + if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + { + return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); + } + } + } + else + { + if (n.hasOperator()) + { + TNode f = d_tdb.getMatchOperator(n); + if (!f.isNull()) + { + std::vector args; + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs); + if (c.isNull()) + { + return TNode::null(); + } + c = d_qstate.getRepresentative(c); + Trace("term-db-entail") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + TNode nn = d_tdb.getCongruentTerm(f, args); + Trace("term-db-entail") + << " got congruent term " << nn << " for " << n << std::endl; + return nn; + } + } + } + return TNode::null(); +} + +Node EntailmentCheck::evaluateTerm(TNode n, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map visited; + std::vector exp; + return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); +} + +Node EntailmentCheck::evaluateTerm(TNode n, + std::vector& exp, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map visited; + return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n, + std::map& subs, + bool subsRep) +{ + return getEntailedTerm2(n, subs, subsRep, true); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n) +{ + std::map subs; + return getEntailedTerm2(n, subs, false, false); +} + +bool EntailmentCheck::isEntailed2( + TNode n, std::map& subs, bool subsRep, bool hasSubs, bool pol) +{ + Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol + << std::endl; + Assert(n.getType().isBoolean()); + if (n.getKind() == EQUAL && !n[0].getType().isBoolean()) + { + TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); + if (!n1.isNull()) + { + TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); + if (!n2.isNull()) + { + if (n1 == n2) + { + return pol; + } + else + { + Assert(d_qstate.hasTerm(n1)); + Assert(d_qstate.hasTerm(n2)); + if (pol) + { + return d_qstate.areEqual(n1, n2); + } + else + { + return d_qstate.areDisequal(n1, n2); + } + } + } + } + } + else if (n.getKind() == NOT) + { + return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); + } + else if (n.getKind() == OR || n.getKind() == AND) + { + bool simPol = (pol && n.getKind() == OR) || (!pol && n.getKind() == AND); + for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + if (isEntailed2(n[i], subs, subsRep, hasSubs, pol)) + { + if (simPol) + { + return true; + } + } + else + { + if (!simPol) + { + return false; + } + } + } + return !simPol; + // Boolean equality here + } + else if (n.getKind() == EQUAL || n.getKind() == ITE) + { + for (size_t i = 0; i < 2; i++) + { + if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) + { + size_t ch = (n.getKind() == EQUAL || i == 0) ? 1 : 2; + bool reqPol = (n.getKind() == ITE || i == 0) ? pol : !pol; + return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol); + } + } + } + else if (n.getKind() == APPLY_UF) + { + TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs); + if (!n1.isNull()) + { + Assert(d_qstate.hasTerm(n1)); + if (n1 == d_true) + { + return pol; + } + else if (n1 == d_false) + { + return !pol; + } + else + { + return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false); + } + } + } + else if (n.getKind() == FORALL && !pol) + { + return isEntailed2(n[1], subs, subsRep, hasSubs, pol); + } + return false; +} + +bool EntailmentCheck::isEntailed(TNode n, bool pol) +{ + std::map subs; + return isEntailed2(n, subs, false, false, pol); +} + +bool EntailmentCheck::isEntailed(TNode n, + std::map& subs, + bool subsRep, + bool pol) +{ + return isEntailed2(n, subs, subsRep, true, pol); +} + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/entailment_check.h b/src/theory/quantifiers/entailment_check.h new file mode 100644 index 000000000..5f0af60a6 --- /dev/null +++ b/src/theory/quantifiers/entailment_check.h @@ -0,0 +1,150 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Entailment check class + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H +#define CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H + +#include +#include + +#include "expr/node.h" +#include "smt/env_obj.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { + +class QuantifiersState; +class TermDb; + +/** + * Entailment check utility, which determines whether formulas are entailed + * in the current context. The main focus of this class is on UF formulas. + * It works by looking at the term argument trie data structures in term + * database. For details, see e.g. Section 4.1 of Reynolds et al TACAS 2018. + */ +class EntailmentCheck : protected EnvObj +{ + public: + EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb); + ~EntailmentCheck(); + /** evaluate term + * + * Returns a term n' such that n = n' is entailed based on the equality + * information ee. This function may generate new terms. In particular, + * we typically rewrite subterms of n of maximal size to terms that exist in + * the equality engine specified by ee. + * + * useEntailmentTests is whether to call the theory engine's entailmentTest + * on literals n for which this call fails to find a term n' that is + * equivalent to n, for increased precision. This is not frequently used. + * + * The vector exp stores the explanation for why n evaluates to that term, + * that is, if this call returns a non-null node n', then: + * exp => n = n' + * + * If reqHasTerm, then we require that the returned term is a Boolean + * combination of terms that exist in the equality engine used by this call. + * If no such term is constructable, this call returns null. The motivation + * for setting this to true is to "fail fast" if we require the return value + * of this function to only involve existing terms. This is used e.g. in + * the "propagating instances" portion of conflict-based instantiation + * (quant_conflict_find.h). + */ + Node evaluateTerm(TNode n, + std::vector& exp, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** same as above, without exp */ + Node evaluateTerm(TNode n, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n = n' is entailed in the current context. + * It returns null if no such term can be found. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n); + /** get entailed term + * + * If possible, returns a term n' such that: + * (1) n' exists in the current equality engine (as specified by the state), + * (2) n * subs = n' is entailed in the current context, where * denotes + * substitution application. + * It returns null if no such term can be found. + * subsRep is whether the substitution maps to terms that are representatives + * according to the quantifiers state. + * Wrt evaluateTerm, this version does not construct new terms, and + * thus is less aggressive. + */ + TNode getEntailedTerm(TNode n, std::map& subs, bool subsRep); + /** is entailed + * Checks whether the current context entails n with polarity pol, based on + * the equality information in the quantifiers state. Returns true if the + * entailment can be successfully shown. + */ + bool isEntailed(TNode n, bool pol); + /** is entailed + * + * Checks whether the current context entails ( n * subs ) with polarity pol, + * based on the equality information in the quantifiers state, + * where * denotes substitution application. + * subsRep is whether the substitution maps to terms that are representatives + * according to in the quantifiers state. + */ + bool isEntailed(TNode n, + std::map& subs, + bool subsRep, + bool pol); + + protected: + /** helper for evaluate term */ + Node evaluateTerm2(TNode n, + std::map& visited, + std::vector& exp, + bool useEntailmentTests, + bool computeExp, + bool reqHasTerm); + /** helper for get entailed term */ + TNode getEntailedTerm2(TNode n, + std::map& subs, + bool subsRep, + bool hasSubs); + /** helper for is entailed */ + bool isEntailed2(TNode n, + std::map& subs, + bool subsRep, + bool hasSubs, + bool pol); + /** The quantifiers state object */ + QuantifiersState& d_qstate; + /** Reference to the term database */ + TermDb& d_tdb; + /** boolean terms */ + Node d_true; + Node d_false; +}; /* class EntailmentCheck */ + +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif /* CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index f756fcfd1..be04f9404 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -25,6 +25,7 @@ #include "smt/logic_exception.h" #include "smt/smt_statistics_registry.h" #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_preprocess.h" @@ -183,7 +184,7 @@ bool Instantiate::addInstantiation(Node q, #endif } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* ec = d_treg.getEntailmentCheck(); // Note we check for entailment before checking for term vector duplication. // Although checking for term vector duplication is a faster check, it is // included automatically with recordInstantiationInternal, hence we prefer @@ -206,7 +207,7 @@ bool Instantiate::addInstantiation(Node q, { subs[q[0][i]] = terms[i]; } - if (tdb->isEntailed(q[1], subs, false, true)) + if (ec->isEntailed(q[1], subs, false, true)) { Trace("inst-add-debug") << " --> Currently entailed." << std::endl; ++(d_statistics.d_inst_duplicate_ent); @@ -217,6 +218,7 @@ bool Instantiate::addInstantiation(Node q, // check based on instantiation level if (options::instMaxLevel() != -1) { + TermDb* tdb = d_treg.getTermDatabase(); for (Node& t : terms) { if (!tdb->isTermEligibleForInstantiation(t, q)) @@ -409,7 +411,7 @@ bool Instantiate::addInstantiationExpFail(Node q, // will never succeed with 1 variable return false; } - TermDb* tdb = d_treg.getTermDatabase(); + EntailmentCheck* echeck = d_treg.getEntailmentCheck(); Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl; // set up information for below std::vector& vars = d_qreg.d_vars[q]; @@ -445,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q, if (options::instNoEntail()) { Trace("inst-exp-fail") << " check entailment" << std::endl; - success = tdb->isEntailed(q[1], subs, false, true); + success = echeck->isEntailed(q[1], subs, false, true); Trace("inst-exp-fail") << " entailed: " << success << std::endl; } // check whether the instantiation rewrites to the same thing diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 361adfd54..dc1043d28 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -577,6 +577,7 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, { if( options::qcfEagerTest() ){ //check whether the instantiation evaluates as expected + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); if (p->atConflictEffort()) { Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl; std::map< TNode, TNode > subs; @@ -584,13 +585,12 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, Trace("qcf-instance-check") << " " << terms[i] << std::endl; subs[d_q[0][i]] = terms[i]; } - TermDb* tdb = p->getTermDatabase(); for( unsigned i=0; i " << n << std::endl; subs[d_extra_var[i]] = n; } - if (!tdb->isEntailed(d_q[1], subs, false, false)) + if (!echeck->isEntailed(d_q[1], subs, false, false)) { Trace("qcf-instance-check") << "...not entailed to be false." << std::endl; return true; @@ -599,8 +599,8 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, Node inst = getInferenceManager().getInstantiate()->getInstantiation(d_q, terms); inst = Rewriter::rewrite(inst); - Node inst_eval = p->getTermDatabase()->evaluateTerm( - inst, options::qcfTConstraint(), true); + Node inst_eval = + echeck->evaluateTerm(inst, options::qcfTConstraint(), true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; for( unsigned i=0; id_false; //} // modified - TermDb* tdb = p->getTermDatabase(); + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); QuantifiersState& qs = p->getState(); for (unsigned i = 0; i < 2; i++) { - if (tdb->isEntailed(d_n, i == 0)) + if (echeck->isEntailed(d_n, i == 0)) { d_ground_eval[0] = i==0 ? p->d_true : p->d_false; } @@ -1233,13 +1233,13 @@ bool MatchGen::reset_round(QuantConflictFind* p) } } }else if( d_type==typ_eq ){ - TermDb* tdb = p->getTermDatabase(); + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); QuantifiersState& qs = p->getState(); for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++) { if (!expr::hasBoundVar(d_n[i])) { - TNode t = tdb->getEntailedTerm(d_n[i]); + TNode t = echeck->getEntailedTerm(d_n[i]); if (qs.isInConflict()) { return false; @@ -1289,13 +1289,9 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { TNode n = qi->getCurrentValue( d_n ); int vn = qi->getCurrentRepVar( qi->getVarNum( n ) ); if( vn==-1 ){ - //evaluate the value, see if it is compatible - //int e = p->evaluate( n ); - //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){ - // d_child_counter = 0; - //} - //modified - if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){ + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); + if (echeck->isEntailed(n, d_tgt)) + { d_child_counter = 0; } }else{ @@ -2168,8 +2164,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q, Node inst = qinst->getInstantiation(q, terms); Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert(!getTermDatabase()->isEntailed(inst, true)); - Assert(getTermDatabase()->isEntailed(inst, false) + Assert(!getTermRegistry().getEntailmentCheck()->isEntailed(inst, true)); + Assert(getTermRegistry().getEntailmentCheck()->isEntailed(inst, false) || d_effort > EFFORT_CONFLICT); } // Process the lemma: either add an instantiation or specific lemmas diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index b1537a390..573cab7bf 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -451,366 +451,6 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { } } -Node TermDb::evaluateTerm2(TNode n, - std::map& visited, - std::vector& exp, - bool useEntailmentTests, - bool computeExp, - bool reqHasTerm) -{ - std::map< TNode, Node >::iterator itv = visited.find( n ); - if( itv != visited.end() ){ - return itv->second; - } - size_t prevSize = exp.size(); - Trace("term-db-eval") << "evaluate term : " << n << std::endl; - Node ret = n; - if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){ - //do nothing - } - else if (d_qstate.hasTerm(n)) - { - Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; - ret = d_qstate.getRepresentative(n); - if (computeExp) - { - if (n != ret) - { - exp.push_back(n.eqNode(ret)); - } - } - reqHasTerm = false; - } - else if (n.hasOperator()) - { - std::vector args; - bool ret_set = false; - Kind k = n.getKind(); - std::vector tempExp; - for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) - { - TNode c = evaluateTerm2(n[i], - visited, - tempExp, - useEntailmentTests, - computeExp, - reqHasTerm); - if (c.isNull()) - { - ret = Node::null(); - ret_set = true; - break; - } - else if (c == d_true || c == d_false) - { - // short-circuiting - if ((k == AND && c == d_false) || (k == OR && c == d_true)) - { - ret = c; - ret_set = true; - reqHasTerm = false; - break; - } - else if (k == ITE && i == 0) - { - ret = evaluateTerm2(n[c == d_true ? 1 : 2], - visited, - tempExp, - useEntailmentTests, - computeExp, - reqHasTerm); - ret_set = true; - reqHasTerm = false; - break; - } - } - if (computeExp) - { - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } - Trace("term-db-eval") << " child " << i << " : " << c << std::endl; - args.push_back(c); - } - if (ret_set) - { - // if we short circuited - if (computeExp) - { - exp.clear(); - exp.insert(exp.end(), tempExp.begin(), tempExp.end()); - } - } - else - { - // get the (indexed) operator of n, if it exists - TNode f = getMatchOperator(n); - // if it is an indexed term, return the congruent term - if (!f.isNull()) - { - // if f is congruent to a term indexed by this class - TNode nn = getCongruentTerm(f, args); - Trace("term-db-eval") << " got congruent term " << nn - << " from DB for " << n << std::endl; - if (!nn.isNull()) - { - if (computeExp) - { - Assert(nn.getNumChildren() == n.getNumChildren()); - for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++) - { - if (nn[i] != n[i]) - { - exp.push_back(nn[i].eqNode(n[i])); - } - } - } - ret = d_qstate.getRepresentative(nn); - Trace("term-db-eval") << "return rep" << std::endl; - ret_set = true; - reqHasTerm = false; - Assert(!ret.isNull()); - if (computeExp) - { - if (n != ret) - { - exp.push_back(nn.eqNode(ret)); - } - } - } - } - if( !ret_set ){ - Trace("term-db-eval") << "return rewrite" << std::endl; - // a theory symbol or a new UF term - if (n.getMetaKind() == metakind::PARAMETERIZED) - { - args.insert(args.begin(), n.getOperator()); - } - ret = NodeManager::currentNM()->mkNode(n.getKind(), args); - ret = rewrite(ret); - if (ret.getKind() == EQUAL) - { - if (d_qstate.areDisequal(ret[0], ret[1])) - { - ret = d_false; - } - } - if (useEntailmentTests) - { - if (ret.getKind() == EQUAL || ret.getKind() == GEQ) - { - Valuation& val = d_qstate.getValuation(); - for (unsigned j = 0; j < 2; j++) - { - std::pair et = val.entailmentCheck( - options::TheoryOfMode::THEORY_OF_TYPE_BASED, - j == 0 ? ret : ret.negate()); - if (et.first) - { - ret = j == 0 ? d_true : d_false; - if (computeExp) - { - exp.push_back(et.second); - } - break; - } - } - } - } - } - } - } - // must have the term - if (reqHasTerm && !ret.isNull()) - { - Kind k = ret.getKind(); - if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT - && k != FORALL) - { - if (!d_qstate.hasTerm(ret)) - { - ret = Node::null(); - } - } - } - Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret - << ", reqHasTerm = " << reqHasTerm << std::endl; - // clear the explanation if failed - if (computeExp && ret.isNull()) - { - exp.resize(prevSize); - } - visited[n] = ret; - return ret; -} - -TNode TermDb::getEntailedTerm2(TNode n, - std::map& subs, - bool subsRep, - bool hasSubs) -{ - Trace("term-db-entail") << "get entailed term : " << n << std::endl; - if (d_qstate.hasTerm(n)) - { - Trace("term-db-entail") << "...exists in ee, return rep " << std::endl; - return n; - }else if( n.getKind()==BOUND_VARIABLE ){ - if( hasSubs ){ - std::map< TNode, TNode >::iterator it = subs.find( n ); - if( it!=subs.end() ){ - Trace("term-db-entail") << "...substitution is : " << it->second << std::endl; - if( subsRep ){ - Assert(d_qstate.hasTerm(it->second)); - Assert(d_qstate.getRepresentative(it->second) == it->second); - return it->second; - } - return getEntailedTerm2(it->second, subs, subsRep, hasSubs); - } - } - }else if( n.getKind()==ITE ){ - for( unsigned i=0; i<2; i++ ){ - if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0)) - { - return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs); - } - } - }else{ - if( n.hasOperator() ){ - TNode f = getMatchOperator( n ); - if( !f.isNull() ){ - std::vector< TNode > args; - for( unsigned i=0; i visited; - std::vector exp; - return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm); -} - -Node TermDb::evaluateTerm(TNode n, - std::vector& exp, - bool useEntailmentTests, - bool reqHasTerm) -{ - std::map visited; - return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm); -} - -TNode TermDb::getEntailedTerm(TNode n, - std::map& subs, - bool subsRep) -{ - return getEntailedTerm2(n, subs, subsRep, true); -} - -TNode TermDb::getEntailedTerm(TNode n) -{ - std::map< TNode, TNode > subs; - return getEntailedTerm2(n, subs, false, false); -} - -bool TermDb::isEntailed2( - TNode n, std::map& subs, bool subsRep, bool hasSubs, bool pol) -{ - Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl; - Assert(n.getType().isBoolean()); - if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ - TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs); - if( !n1.isNull() ){ - TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs); - if( !n2.isNull() ){ - if( n1==n2 ){ - return pol; - }else{ - Assert(d_qstate.hasTerm(n1)); - Assert(d_qstate.hasTerm(n2)); - if( pol ){ - return d_qstate.areEqual(n1, n2); - }else{ - return d_qstate.areDisequal(n1, n2); - } - } - } - } - }else if( n.getKind()==NOT ){ - return isEntailed2(n[0], subs, subsRep, hasSubs, !pol); - }else if( n.getKind()==OR || n.getKind()==AND ){ - bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND ); - for( unsigned i=0; i subs; - return isEntailed2(n, subs, false, false, pol); -} - -bool TermDb::isEntailed(TNode n, - std::map& subs, - bool subsRep, - bool pol) -{ - Assert(d_consistent_ee); - return isEntailed2(n, subs, subsRep, true, pol); -} - bool TermDb::isTermActive( Node n ) { return d_inactive_map.find( n )==d_inactive_map.end(); //return !n.getAttribute(NoMatchAttribute()); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index af0b87bd8..0e5c7bc01 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -176,78 +176,6 @@ class TermDb : public QuantifiersUtil { * equivalence class of r. */ bool inRelevantDomain(TNode f, unsigned i, TNode r); - /** evaluate term - * - * Returns a term n' such that n = n' is entailed based on the equality - * information ee. This function may generate new terms. In particular, - * we typically rewrite subterms of n of maximal size to terms that exist in - * the equality engine specified by ee. - * - * useEntailmentTests is whether to call the theory engine's entailmentTest - * on literals n for which this call fails to find a term n' that is - * equivalent to n, for increased precision. This is not frequently used. - * - * The vector exp stores the explanation for why n evaluates to that term, - * that is, if this call returns a non-null node n', then: - * exp => n = n' - * - * If reqHasTerm, then we require that the returned term is a Boolean - * combination of terms that exist in the equality engine used by this call. - * If no such term is constructable, this call returns null. The motivation - * for setting this to true is to "fail fast" if we require the return value - * of this function to only involve existing terms. This is used e.g. in - * the "propagating instances" portion of conflict-based instantiation - * (quant_conflict_find.h). - */ - Node evaluateTerm(TNode n, - std::vector& exp, - bool useEntailmentTests = false, - bool reqHasTerm = false); - /** same as above, without exp */ - Node evaluateTerm(TNode n, - bool useEntailmentTests = false, - bool reqHasTerm = false); - /** get entailed term - * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by the state), - * (2) n = n' is entailed in the current context. - * It returns null if no such term can be found. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n); - /** get entailed term - * - * If possible, returns a term n' such that: - * (1) n' exists in the current equality engine (as specified by the state), - * (2) n * subs = n' is entailed in the current context, where * denotes - * substitution application. - * It returns null if no such term can be found. - * subsRep is whether the substitution maps to terms that are representatives - * according to the quantifiers state. - * Wrt evaluateTerm, this version does not construct new terms, and - * thus is less aggressive. - */ - TNode getEntailedTerm(TNode n, std::map& subs, bool subsRep); - /** is entailed - * Checks whether the current context entails n with polarity pol, based on - * the equality information in the quantifiers state. Returns true if the - * entailment can be successfully shown. - */ - bool isEntailed(TNode n, bool pol); - /** is entailed - * - * Checks whether the current context entails ( n * subs ) with polarity pol, - * based on the equality information in the quantifiers state, - * where * denotes substitution application. - * subsRep is whether the substitution maps to terms that are representatives - * according to in the quantifiers state. - */ - bool isEntailed(TNode n, - std::map& subs, - bool subsRep, - bool pol); /** is the term n active in the current context? * * By default, all terms are active. A term is inactive if: @@ -355,24 +283,6 @@ class TermDb : public QuantifiersUtil { //----------------------------- end implementation-specific /** set has term */ void setHasTerm( Node n ); - /** helper for evaluate term */ - Node evaluateTerm2(TNode n, - std::map& visited, - std::vector& exp, - bool useEntailmentTests, - bool computeExp, - bool reqHasTerm); - /** helper for get entailed term */ - TNode getEntailedTerm2(TNode n, - std::map& subs, - bool subsRep, - bool hasSubs); - /** helper for is entailed */ - bool isEntailed2(TNode n, - std::map& subs, - bool subsRep, - bool hasSubs, - bool pol); /** compute uf eqc terms : * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes */ diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp index ab999ad9b..d11fb0b8d 100644 --- a/src/theory/quantifiers/term_registry.cpp +++ b/src/theory/quantifiers/term_registry.cpp @@ -18,6 +18,7 @@ #include "options/base_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/fmf/first_order_model_fmc.h" #include "theory/quantifiers/ho_term_database.h" @@ -39,6 +40,7 @@ TermRegistry::TermRegistry(Env& env, d_termPools(new TermPools(env, qs)), d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr) : new TermDb(env, qs, qr)), + d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())), d_sygusTdb(nullptr), d_qmodel(nullptr) { @@ -132,6 +134,11 @@ TermDbSygus* TermRegistry::getTermDatabaseSygus() const return d_sygusTdb.get(); } +EntailmentCheck* TermRegistry::getEntailmentCheck() const +{ + return d_echeck.get(); +} + TermEnumeration* TermRegistry::getTermEnumeration() const { return d_termEnum.get(); diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h index 175d450df..60a87a91f 100644 --- a/src/theory/quantifiers/term_registry.h +++ b/src/theory/quantifiers/term_registry.h @@ -23,6 +23,7 @@ #include "context/cdhashset.h" #include "smt/env_obj.h" +#include "theory/quantifiers/entailment_check.h" #include "theory/quantifiers/sygus/term_database_sygus.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_enumeration.h" @@ -83,6 +84,8 @@ class TermRegistry : protected EnvObj TermDb* getTermDatabase() const; /** get term database sygus */ TermDbSygus* getTermDatabaseSygus() const; + /** get entailment check utility */ + EntailmentCheck* getEntailmentCheck() const; /** get term enumeration utility */ TermEnumeration* getTermEnumeration() const; /** get the term pools utility */ @@ -103,6 +106,8 @@ class TermRegistry : protected EnvObj std::unique_ptr d_termPools; /** term database */ std::unique_ptr d_termDb; + /** entailment check */ + std::unique_ptr d_echeck; /** sygus term database */ std::unique_ptr d_sygusTdb; /** extended model object */ -- 2.30.2