Towards addressing some bottlenecks on Facebook benchmarks.
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
// 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;
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 );
}
}
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 ){
d_lchildren.clear();
d_arg_to_arg_rep.clear();
d_arg_vector.clear();
+ EntailmentCheck* echeck = d_treg.getEntailmentCheck();
for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
{
TNode var = ha.first;
{
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();
}
--- /dev/null
+/******************************************************************************
+ * 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<TNode, Node>& visited,
+ std::vector<Node>& 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<TNode> args;
+ bool ret_set = false;
+ Kind k = n.getKind();
+ std::vector<Node> 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<bool, Node> 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<TNode, TNode>& 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 (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<TNode> 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<TNode, Node> visited;
+ std::vector<Node> exp;
+ return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
+}
+
+Node EntailmentCheck::evaluateTerm(TNode n,
+ std::vector<Node>& exp,
+ bool useEntailmentTests,
+ bool reqHasTerm)
+{
+ std::map<TNode, Node> visited;
+ return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
+}
+
+TNode EntailmentCheck::getEntailedTerm(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep)
+{
+ return getEntailedTerm2(n, subs, subsRep, true);
+}
+
+TNode EntailmentCheck::getEntailedTerm(TNode n)
+{
+ std::map<TNode, TNode> subs;
+ return getEntailedTerm2(n, subs, false, false);
+}
+
+bool EntailmentCheck::isEntailed2(
+ TNode n, std::map<TNode, TNode>& 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<TNode, TNode> subs;
+ return isEntailed2(n, subs, false, false, pol);
+}
+
+bool EntailmentCheck::isEntailed(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ bool pol)
+{
+ return isEntailed2(n, subs, subsRep, true, pol);
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace cvc5
--- /dev/null
+/******************************************************************************
+ * 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 <map>
+#include <vector>
+
+#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<Node>& 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<TNode, TNode>& 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<TNode, TNode>& subs,
+ bool subsRep,
+ bool pol);
+
+ protected:
+ /** helper for evaluate term */
+ Node evaluateTerm2(TNode n,
+ std::map<TNode, Node>& visited,
+ std::vector<Node>& exp,
+ bool useEntailmentTests,
+ bool computeExp,
+ bool reqHasTerm);
+ /** helper for get entailed term */
+ TNode getEntailedTerm2(TNode n,
+ std::map<TNode, TNode>& subs,
+ bool subsRep,
+ bool hasSubs);
+ /** helper for is entailed */
+ bool isEntailed2(TNode n,
+ std::map<TNode, TNode>& 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 */
#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"
#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
{
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);
// check based on instantiation level
if (options::instMaxLevel() != -1)
{
+ TermDb* tdb = d_treg.getTermDatabase();
for (Node& t : terms)
{
if (!tdb->isTermEligibleForInstantiation(t, 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<Node>& vars = d_qreg.d_vars[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
{
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;
Trace("qcf-instance-check") << " " << terms[i] << std::endl;
subs[d_q[0][i]] = terms[i];
}
- TermDb* tdb = p->getTermDatabase();
for( unsigned i=0; i<d_extra_var.size(); i++ ){
Node n = getCurrentExpValue( d_extra_var[i] );
Trace("qcf-instance-check") << " " << d_extra_var[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;
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; i<terms.size(); i++ ){
// d_ground_eval[0] = p->d_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;
}
}
}
}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;
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{
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
}
}
-Node TermDb::evaluateTerm2(TNode n,
- std::map<TNode, Node>& visited,
- std::vector<Node>& 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<TNode> args;
- bool ret_set = false;
- Kind k = n.getKind();
- std::vector<Node> 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<bool, Node> 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<TNode, TNode>& 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<n.getNumChildren(); 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 = getCongruentTerm(f, args);
- Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl;
- return nn;
- }
- }
- }
- return TNode::null();
-}
-
-Node TermDb::evaluateTerm(TNode n,
- bool useEntailmentTests,
- bool reqHasTerm)
-{
- std::map< TNode, Node > visited;
- std::vector<Node> exp;
- return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
-}
-
-Node TermDb::evaluateTerm(TNode n,
- std::vector<Node>& exp,
- bool useEntailmentTests,
- bool reqHasTerm)
-{
- std::map<TNode, Node> visited;
- return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
-}
-
-TNode TermDb::getEntailedTerm(TNode n,
- std::map<TNode, TNode>& 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<TNode, TNode>& 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<n.getNumChildren(); 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( unsigned i=0; i<2; i++ ){
- if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
- {
- unsigned 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 TermDb::isEntailed(TNode n, bool pol)
-{
- Assert(d_consistent_ee);
- std::map< TNode, TNode > subs;
- return isEntailed2(n, subs, false, false, pol);
-}
-
-bool TermDb::isEntailed(TNode n,
- std::map<TNode, TNode>& 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());
* 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<Node>& 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<TNode, TNode>& 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<TNode, TNode>& 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:
//----------------------------- end implementation-specific
/** set has term */
void setHasTerm( Node n );
- /** helper for evaluate term */
- Node evaluateTerm2(TNode n,
- std::map<TNode, Node>& visited,
- std::vector<Node>& exp,
- bool useEntailmentTests,
- bool computeExp,
- bool reqHasTerm);
- /** helper for get entailed term */
- TNode getEntailedTerm2(TNode n,
- std::map<TNode, TNode>& subs,
- bool subsRep,
- bool hasSubs);
- /** helper for is entailed */
- bool isEntailed2(TNode n,
- std::map<TNode, TNode>& 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
*/
#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"
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)
{
return d_sygusTdb.get();
}
+EntailmentCheck* TermRegistry::getEntailmentCheck() const
+{
+ return d_echeck.get();
+}
+
TermEnumeration* TermRegistry::getTermEnumeration() const
{
return d_termEnum.get();
#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"
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 */
std::unique_ptr<TermPools> d_termPools;
/** term database */
std::unique_ptr<TermDb> d_termDb;
+ /** entailment check */
+ std::unique_ptr<EntailmentCheck> d_echeck;
/** sygus term database */
std::unique_ptr<TermDbSygus> d_sygusTdb;
/** extended model object */
projects / cvc5.git / commitdiff