diff options
Diffstat (limited to 'src/theory/quantifiers')
26 files changed, 1008 insertions, 650 deletions
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<Node>& m, InferenceId id) 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; @@ -291,8 +292,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& 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/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index d8e3b7950..075299583 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -23,6 +23,7 @@ #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h" #include "theory/quantifiers/ematching/inst_match_generator_simple.h" #include "theory/quantifiers/ematching/pattern_term_selector.h" +#include "theory/quantifiers/ematching/relational_match_generator.h" #include "theory/quantifiers/ematching/var_match_generator.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_state.h" @@ -618,7 +619,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( InstMatchGenerator* init; std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] ); if( iti==pat_map_init.end() ){ - init = new InstMatchGenerator(tparent, pats[pCounter]); + init = getInstMatchGenerator(tparent, q, pats[pCounter]); }else{ init = iti->second; } @@ -645,6 +646,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, Node q, Node n) { + // maybe variable match generator if (n.getKind() != INST_CONSTANT) { Trace("var-trigger-debug") @@ -672,6 +674,16 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent, return vmg; } } + Trace("relational-trigger") + << "Is " << n << " a relational trigger?" << std::endl; + // relational triggers + bool hasPol, pol; + Node lit; + if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit)) + { + Trace("relational-trigger") << "...yes, for literal " << lit << std::endl; + return new RelationalMatchGenerator(tparent, lit, hasPol, pol); + } return new InstMatchGenerator(tparent, n); } diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 30be83ecc..fdb0d0db3 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -339,20 +339,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ TriggerDatabase::TR_GET_OLD, d_num_trigger_vars[f]); } - if (tr == nullptr) + // if we generated a trigger above, add it + if (tr != nullptr) { - // did not generate a trigger - continue; - } - addTrigger(tr, f); - if (tr->isMultiTrigger()) - { - // only add a single multi-trigger - continue; + addTrigger(tr, f); + if (tr->isMultiTrigger()) + { + // only add a single multi-trigger + continue; + } } // if we are generating additional triggers... - size_t index = 0; - if (index < patTerms.size()) + if (patTerms.size() > 1) { // check if similar patterns exist, and if so, add them additionally unsigned nqfs_curr = 0; @@ -361,7 +359,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ nqfs_curr = d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator()); } - index++; + size_t index = 1; bool success = true; while (success && index < patTerms.size() && d_is_single_trigger[patTerms[index]]) @@ -527,16 +525,22 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl; + // Currently, we have ad-hoc treatment for relational triggers that + // are not handled by RelationalMatchGen. + bool isAdHocRelationalTrigger = + TriggerTermInfo::isRelationalTrigger(pat) + && !TriggerTermInfo::isUsableRelationTrigger(pat); if (rpol != 0) { Assert(rpol == 1 || rpol == -1); - if (TriggerTermInfo::isRelationalTrigger(pat)) + if (isAdHocRelationalTrigger) { pat = rpol == -1 ? pat.negate() : pat; } else { - Assert(TriggerTermInfo::isAtomicTrigger(pat)); + Assert(TriggerTermInfo::isAtomicTrigger(pat) + || TriggerTermInfo::isUsableRelationTrigger(pat)); if (pat.getType().isBoolean() && rpoleq.isNull()) { if (options().quantifiers.literalMatchMode @@ -575,13 +579,10 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f) } Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl; } - else + else if (isAdHocRelationalTrigger) { - if (TriggerTermInfo::isRelationalTrigger(pat)) - { - // consider both polarities - addPatternToPool(f, pat.negate(), num_fv, mpat); - } + // consider both polarities + addPatternToPool(f, pat.negate(), num_fv, mpat); } addPatternToPool(f, pat, num_fv, mpat); } diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp new file mode 100644 index 000000000..8981a7a2d --- /dev/null +++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp @@ -0,0 +1,125 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Relational match generator class. + */ + +#include "theory/quantifiers/ematching/relational_match_generator.h" + +#include "theory/quantifiers/term_util.h" +#include "util/rational.h" + +using namespace cvc5::kind; + +namespace cvc5 { +namespace theory { +namespace quantifiers { +namespace inst { + +RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent, + Node rtrigger, + bool hasPol, + bool pol) + : InstMatchGenerator(tparent, Node::null()), + d_vindex(-1), + d_hasPol(hasPol), + d_pol(pol), + d_counter(0) +{ + Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal()) + || rtrigger.getKind() == GEQ); + Trace("relational-match-gen") + << "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol + << "/" << pol << std::endl; + for (size_t i = 0; i < 2; i++) + { + if (rtrigger[i].getKind() == INST_CONSTANT) + { + d_var = rtrigger[i]; + d_vindex = d_var.getAttribute(InstVarNumAttribute()); + d_rhs = rtrigger[1 - i]; + Assert(!quantifiers::TermUtil::hasInstConstAttr(d_rhs)); + Kind k = rtrigger.getKind(); + d_rel = (i == 0 ? k : (k == GEQ ? LEQ : k)); + break; + } + } + Trace("relational-match-gen") << "...processed " << d_var << " (" << d_vindex + << ") " << d_rel << " " << d_rhs << std::endl; + AlwaysAssert(!d_var.isNull()) + << "Failed to initialize RelationalMatchGenerator"; +} + +bool RelationalMatchGenerator::reset(Node eqc) +{ + d_counter = 0; + return true; +} + +int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m) +{ + Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl; + // try (up to) two different terms + Node s; + Node rhs = d_rhs; + bool rmPrev = m.get(d_vindex).isNull(); + while (d_counter < 2) + { + bool checkPol = false; + if (d_counter == 0) + { + checkPol = d_pol; + } + else + { + Assert(d_counter == 1); + if (d_hasPol) + { + break; + } + // try the opposite polarity + checkPol = !d_pol; + } + NodeManager* nm = NodeManager::currentNM(); + // falsify ( d_var <d_rel> d_rhs ) = checkPol + s = rhs; + if (!checkPol) + { + s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1))); + } + d_counter++; + Trace("relational-match-gen") + << "...try set " << s << " for " << checkPol << std::endl; + if (m.set(d_qstate, d_vindex, s)) + { + Trace("relational-match-gen") << "...success" << std::endl; + int ret = continueNextMatch(q, m, InferenceId::UNKNOWN); + if (ret > 0) + { + Trace("relational-match-gen") << "...returned " << ret << std::endl; + return ret; + } + Trace("relational-match-gen") << "...failed to gen inst" << std::endl; + // failed + if (rmPrev) + { + m.d_vals[d_vindex] = Node::null(); + } + } + } + return -1; +} + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h new file mode 100644 index 000000000..eead2876a --- /dev/null +++ b/src/theory/quantifiers/ematching/relational_match_generator.h @@ -0,0 +1,92 @@ +/****************************************************************************** + * 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. + * **************************************************************************** + * + * Relational match generator class. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H +#define CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H + +#include "expr/node.h" +#include "theory/quantifiers/ematching/inst_match_generator.h" + +namespace cvc5 { +namespace theory { +namespace quantifiers { +namespace inst { + +/** + * Match generator for relational triggers x ~ t where t is a ground term. + * This match generator tries a small fixed set of terms based on the kind of + * relation and the required polarity of the trigger in the quantified formula. + * + * For example, for quantified formula (forall ((x Int)) (=> (> x n) (P x))), + * we have that (> x n) is a relational trigger with required polarity "true". + * This generator will try the match `x -> n+1` only, where notice that n+1 is + * the canonical term chosen to satisfy x>n. Canonical terms for arithmetic + * relations (~ x n) are in set { n, n+1, n-1 }. + * + * If a relational trigger does not have a required polarity, then up to 2 + * terms are tried, a term that satisfies the relation, and one that does not. + * If (>= x n) is a relational trigger with no polarity, then `x -> n` and + * `x -> n-1` will be generated. + * + * Currently this class handles only equality between real or integer valued + * terms, or inequalities (kind GEQ). It furthermore only considers ground terms + * t for the right hand side of relations. + */ +class RelationalMatchGenerator : public InstMatchGenerator +{ + public: + /** + * @param tparent The parent trigger that this match generator belongs to + * @param rtrigger The relational trigger + * @param hasPol Whether the trigger has an entailed polarity + * @param pol The entailed polarity of the relational trigger. + */ + RelationalMatchGenerator(Trigger* tparent, + Node rtrigger, + bool hasPol, + bool pol); + + /** Reset */ + bool reset(Node eqc) override; + /** Get the next match. */ + int getNextMatch(Node q, InstMatch& m) override; + + private: + /** the variable */ + Node d_var; + /** The index of the variable */ + int64_t d_vindex; + /** the relation kind */ + Kind d_rel; + /** the right hand side */ + Node d_rhs; + /** whether we have a required polarity */ + bool d_hasPol; + /** the required polarity, if it exists */ + bool d_pol; + /** + * The current number of terms we have generated since the last call to reset + */ + size_t d_counter; +}; + +} // namespace inst +} // namespace quantifiers +} // namespace theory +} // namespace cvc5 + +#endif diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp index 600797f4e..f31ec088a 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.cpp +++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp @@ -70,6 +70,46 @@ bool TriggerTermInfo::isRelationalTriggerKind(Kind k) return k == EQUAL || k == GEQ; } +bool TriggerTermInfo::isUsableRelationTrigger(Node n) +{ + bool hasPol, pol; + Node lit; + return isUsableRelationTrigger(n, hasPol, pol, lit); +} +bool TriggerTermInfo::isUsableRelationTrigger(Node n, + bool& hasPol, + bool& pol, + Node& lit) +{ + // relational triggers (not) (= (~ x t) true|false), where ~ in { =, >= }. + hasPol = false; + pol = n.getKind() != NOT; + lit = pol ? n : n[0]; + if (lit.getKind() == EQUAL && lit[1].getType().isBoolean() + && lit[1].isConst()) + { + hasPol = true; + pol = lit[1].getConst<bool>() ? pol : !pol; + lit = lit[0]; + } + // is it a relational trigger? + if ((lit.getKind() == EQUAL && lit[0].getType().isReal()) + || lit.getKind() == GEQ) + { + // if one side of the relation is a variable and the other side is a ground + // term, we can treat this using the relational match generator + for (size_t i = 0; i < 2; i++) + { + if (lit[i].getKind() == INST_CONSTANT + && !quantifiers::TermUtil::hasInstConstAttr(lit[1 - i])) + { + return true; + } + } + } + return false; +} + bool TriggerTermInfo::isSimpleTrigger(Node n) { Node t = n.getKind() == NOT ? n[0] : n; @@ -105,7 +145,7 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n) { return 0; } - if (isAtomicTrigger(n)) + if (isAtomicTrigger(n) || isUsableRelationTrigger(n)) { return 1; } diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h index 753d0850c..3816d0988 100644 --- a/src/theory/quantifiers/ematching/trigger_term_info.h +++ b/src/theory/quantifiers/ematching/trigger_term_info.h @@ -108,6 +108,19 @@ class TriggerTermInfo static bool isRelationalTrigger(Node n); /** Is k a relational trigger kind? */ static bool isRelationalTriggerKind(Kind k); + /** + * Is n a usable relational trigger, which is true if RelationalMatchGenerator + * can process n. + */ + static bool isUsableRelationTrigger(Node n); + /** + * Same as above, but lit / hasPol / pol are updated to the required + * constructor arguments for RelationalMatchGenerator. + */ + static bool isUsableRelationTrigger(Node n, + bool& hasPol, + bool& pol, + Node& lit); /** is n a simple trigger (see inst_match_generator.h)? */ static bool isSimpleTrigger(Node n); /** get trigger weight @@ -116,7 +129,8 @@ class TriggerTermInfo * trigger term n, where the smaller the value, the easier. * * Returns 0 for triggers that are APPLY_UF terms. - * Returns 1 for other triggers whose kind is atomic. + * Returns 1 for other triggers whose kind is atomic, or are usable + * relational triggers. * Returns 2 otherwise. */ static int32_t getTriggerWeight(Node n); diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp new file mode 100644 index 000000000..543414a4e --- /dev/null +++ b/src/theory/quantifiers/entailment_check.cpp @@ -0,0 +1,411 @@ +/****************************************************************************** + * 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::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map<TNode, Node>::iterator itv = visited.find(n); + if (itv != visited.end()) + { + return itv->second; + } + Trace("term-db-eval") << "evaluate term : " << n << std::endl; + Node ret = n; + Kind k = n.getKind(); + if (k == FORALL) + { + // do nothing + } + else if (k == BOUND_VARIABLE) + { + std::map<TNode, TNode>::iterator it = subs.find(n); + if (it != subs.end()) + { + if (!subsRep) + { + Assert(d_qstate.hasTerm(it->second)); + ret = d_qstate.getRepresentative(it->second); + } + else + { + ret = it->second; + } + } + } + else if (d_qstate.hasTerm(n)) + { + Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; + ret = d_qstate.getRepresentative(n); + reqHasTerm = false; + } + else if (n.hasOperator()) + { + std::vector<TNode> args; + bool ret_set = false; + for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = evaluateTerm2( + n[i], visited, subs, subsRep, useEntailmentTests, 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, + subs, + subsRep, + useEntailmentTests, + reqHasTerm); + ret_set = true; + reqHasTerm = false; + break; + } + } + Trace("term-db-eval") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + if (!ret_set) + { + // 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()) + { + ret = d_qstate.getRepresentative(nn); + Trace("term-db-eval") << "return rep" << std::endl; + ret_set = true; + reqHasTerm = false; + Assert(!ret.isNull()); + } + } + 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; + break; + } + } + } + } + } + } + } + // must have the term + if (reqHasTerm && !ret.isNull()) + { + Kind rk = ret.getKind(); + if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT + && rk != FORALL) + { + if (!d_qstate.hasTerm(ret)) + { + ret = Node::null(); + } + } + } + Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret + << ", reqHasTerm = " << reqHasTerm << std::endl; + visited[n] = ret; + return ret; +} + +TNode EntailmentCheck::getEntailedTerm2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep) +{ + 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) + { + 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); + } + } + else if (n.getKind() == ITE) + { + for (uint32_t i = 0; i < 2; i++) + { + if (isEntailed2(n[0], subs, subsRep, i == 0)) + { + return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep); + } + } + } + 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); + 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, + std::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map<TNode, Node> visited; + return evaluateTerm2( + n, visited, subs, subsRep, useEntailmentTests, reqHasTerm); +} + +Node EntailmentCheck::evaluateTerm(TNode n, + bool useEntailmentTests, + bool reqHasTerm) +{ + std::map<TNode, Node> visited; + std::map<TNode, TNode> subs; + return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep) +{ + return getEntailedTerm2(n, subs, subsRep); +} + +TNode EntailmentCheck::getEntailedTerm(TNode n) +{ + std::map<TNode, TNode> subs; + return getEntailedTerm2(n, subs, false); +} + +bool EntailmentCheck::isEntailed2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + 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); + if (!n1.isNull()) + { + TNode n2 = getEntailedTerm2(n[1], subs, subsRep); + 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, !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, 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, 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, reqPol); + } + } + } + else if (n.getKind() == APPLY_UF) + { + TNode n1 = getEntailedTerm2(n, subs, subsRep); + 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, pol); + } + return false; +} + +bool EntailmentCheck::isEntailed(TNode n, bool pol) +{ + std::map<TNode, TNode> subs; + return isEntailed2(n, subs, false, pol); +} + +bool EntailmentCheck::isEntailed(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool pol) +{ + return isEntailed2(n, subs, subsRep, 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..ecf74fe85 --- /dev/null +++ b/src/theory/quantifiers/entailment_check.h @@ -0,0 +1,156 @@ +/****************************************************************************** + * 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 * subs = n' is entailed based on the current + * set of equalities, where ( n * subs ) is term n under the substitution + * subs. + * + * This function may generate new terms. In particular, we typically rewrite + * subterms of n of maximal size (in terms of the AST) to terms that exist + * in the equality engine. + * + * 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. + * + * 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). + * + * @param n The term under consideration + * @param subs The substitution under consideration + * @param subsRep Whether the range of subs are representatives in the current + * equality engine + * @param useEntailmentTests Whether to use entailment tests to show + * n * subs is equivalent to true/false. + * @param reqHasTerm Whether we require the returned term to be a Boolean + * combination of terms known to the current equality engine + * @return the term n * subs evaluates to + */ + Node evaluateTerm(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** Same as above, without a substitution */ + 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::map<TNode, TNode>& subs, + bool subsRep, + bool useEntailmentTests, + bool reqHasTerm); + /** helper for get entailed term */ + TNode getEntailedTerm2(TNode n, std::map<TNode, TNode>& subs, bool subsRep); + /** helper for is entailed */ + bool isEntailed2(TNode n, + std::map<TNode, TNode>& subs, + bool subsRep, + 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/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index d648a7a29..fad95612f 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -53,17 +53,23 @@ Node ExprMiner::convertToSkolem(Node n) void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker, Node query) { + initializeChecker(checker, query, options(), logicInfo()); +} + +void ExprMiner::initializeChecker(std::unique_ptr<SolverEngine>& checker, + Node query, + const Options& opts, + const LogicInfo& logicInfo) +{ Assert (!query.isNull()); if (Options::current().quantifiers.sygusExprMinerCheckTimeoutWasSetByUser) { - initializeSubsolver(checker, - d_env, - true, - options::sygusExprMinerCheckTimeout()); + initializeSubsolver( + checker, opts, logicInfo, true, options::sygusExprMinerCheckTimeout()); } else { - initializeSubsolver(checker, d_env); + initializeSubsolver(checker, opts, logicInfo); } // also set the options checker->setOption("sygus-rr-synth-input", "false"); diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 3933b9635..702dbf5aa 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -85,7 +85,12 @@ class ExprMiner : protected EnvObj * of the argument "query", which is a formula whose free variables (of * kind BOUND_VARIABLE) are a subset of d_vars. */ - void initializeChecker(std::unique_ptr<SolverEngine>& smte, Node query); + void initializeChecker(std::unique_ptr<SolverEngine>& checker, Node query); + /** Also with configurable options and logic */ + void initializeChecker(std::unique_ptr<SolverEngine>& checker, + Node query, + const Options& opts, + const LogicInfo& logicInfo); /** * Run the satisfiability check on query and return the result * (sat/unsat/unknown). diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 7c1d36ce8..94351274a 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -951,10 +951,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n Node r = n; if( !n.isConst() ){ TypeNode tn = n.getType(); - if( !fm->hasTerm(n) && tn.isFirstClass() ){ - r = getSomeDomainElement(fm, tn ); + if (!fm->hasTerm(n) && tn.isFirstClass()) + { + // if the term is unknown, we do not assume any value for it + r = Node::null(); + } + else + { + r = fm->getRepresentative(r); } - r = fm->getRepresentative( r ); } Trace("fmc-debug") << "Add constant entry..." << std::endl; d.addEntry(fm, mkCondDefault(fm, f), r); 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<Node>& 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..323398879 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -52,12 +52,6 @@ QuantInfo::~QuantInfo() { d_var_mg.clear(); } -QuantifiersInferenceManager& QuantInfo::getInferenceManager() -{ - Assert(d_parent != nullptr); - return d_parent->getInferenceManager(); -} - void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { d_parent = p; d_q = q; @@ -577,30 +571,33 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, { if( options::qcfEagerTest() ){ //check whether the instantiation evaluates as expected + EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck(); + std::map<TNode, TNode> subs; + for (size_t i = 0, tsize = terms.size(); i < tsize; i++) + { + Trace("qcf-instance-check") << " " << terms[i] << std::endl; + subs[d_q[0][i]] = terms[i]; + } + for (size_t i = 0, evsize = d_extra_var.size(); i < evsize; 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 (p->atConflictEffort()) { Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl; - std::map< TNode, TNode > subs; - for( unsigned i=0; i<terms.size(); i++ ){ - 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; } }else{ - Node inst = - getInferenceManager().getInstantiate()->getInstantiation(d_q, terms); - inst = Rewriter::rewrite(inst); - Node inst_eval = p->getTermDatabase()->evaluateTerm( - inst, options::qcfTConstraint(), true); + // see if the body of the quantified formula evaluates to a Boolean + // combination of known terms under the current substitution. We use + // the helper method evaluateTerm from the entailment check utility. + Node inst_eval = echeck->evaluateTerm( + d_q[1], subs, false, 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++ ){ @@ -608,6 +605,10 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p, } Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl; } + // If it is the case that instantiation can be rewritten to a Boolean + // combination of terms that exist in the current context, then inst_eval + // is non-null. Moreover, we insist that inst_eval is not true, or else + // the instantiation is trivially entailed and hence is spurious. if (inst_eval.isNull() || (inst_eval.isConst() && inst_eval.getConst<bool>())) { @@ -1219,11 +1220,11 @@ bool MatchGen::reset_round(QuantConflictFind* p) // 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; } @@ -1233,13 +1234,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 +1290,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 +2165,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/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 927a74ff2..d14e281fb 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -132,8 +132,6 @@ public: public: QuantInfo(); ~QuantInfo(); - /** Get quantifiers inference manager */ - QuantifiersInferenceManager& getInferenceManager(); std::vector< TNode > d_vars; std::vector< TypeNode > d_var_types; std::map< TNode, int > d_var_num; diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 7c7c7aade..52e90e26e 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -15,6 +15,7 @@ #include "theory/quantifiers/quantifiers_rewriter.h" +#include "expr/ascription_type.h" #include "expr/bound_var_manager.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" @@ -895,12 +896,25 @@ bool QuantifiersRewriter::getVarElimLit(Node body, const DType& dt = datatypes::utils::datatypeOf(tester); const DTypeConstructor& c = dt[index]; std::vector<Node> newChildren; - newChildren.push_back(c.getConstructor()); + Node cons = c.getConstructor(); + TypeNode tspec; + // take into account if parametric + if (dt.isParametric()) + { + tspec = c.getSpecializedConstructorType(lit[0].getType()); + cons = nm->mkNode( + APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons); + } + else + { + tspec = cons.getType(); + } + newChildren.push_back(cons); std::vector<Node> newVars; BoundVarManager* bvm = nm->getBoundVarManager(); - for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++) + for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++) { - TypeNode tn = c[j].getRangeType(); + TypeNode tn = tspec[j]; Node rn = nm->mkConst(Rational(j)); Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn); Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn); diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index c8e14e4bd..fdc0b28e0 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -39,6 +39,7 @@ Cegis::Cegis(Env& env, SynthConjecture* p) : SygusModule(env, qs, qim, tds, p), d_eval_unfold(tds->getEvalUnfold()), + d_cexClosedEnum(false), d_cegis_sampler(env), d_usingSymCons(false) { @@ -47,11 +48,18 @@ Cegis::Cegis(Env& env, bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates) { d_base_body = n; + d_cexClosedEnum = true; if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL) { for (const Node& v : d_base_body[0][0]) { d_base_vars.push_back(v); + if (!v.getType().isClosedEnumerable()) + { + // not closed enumerable, refinement lemmas cannot be sent to the + // quantifier-free datatype solver + d_cexClosedEnum = false; + } } d_base_body = d_base_body[0][1]; } @@ -467,14 +475,18 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter, void Cegis::registerRefinementLemma(const std::vector<Node>& vars, Node lem) { addRefinementLemma(lem); - // Make the refinement lemma and add it to lems. - // This lemma is guarded by the parent's guard, which has the semantics - // "this conjecture has a solution", hence this lemma states: - // if the parent conjecture has a solution, it satisfies the specification - // for the given concrete point. - Node rlem = - NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem); - d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + // must be closed enumerable + if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold) + { + // Make the refinement lemma and add it to lems. + // This lemma is guarded by the parent's guard, which has the semantics + // "this conjecture has a solution", hence this lemma states: + // if the parent conjecture has a solution, it satisfies the specification + // for the given concrete point. + Node rlem = NodeManager::currentNM()->mkNode( + OR, d_parent->getGuard().negate(), lem); + d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE); + } } bool Cegis::usingRepairConst() { return true; } diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 8e0fffdd1..8d1f0a1b2 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -119,6 +119,13 @@ class Cegis : public SygusModule std::vector<Node> d_rl_vals; /** all variables appearing in refinement lemmas */ std::unordered_set<Node> d_refinement_lemma_vars; + /** + * Are the counterexamples we are handling in this class of only closed + * enumerable types (see TypeNode::isClosedEnumerable). If this is false, + * then CEGIS refinement lemmas can contain terms that are unhandled by + * theory solvers, e.g. uninterpreted constants. + */ + bool d_cexClosedEnum; /** adds lem as a refinement lemma */ void addRefinementLemma(Node lem); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp index 936310e4e..5a0cf8724 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp +++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp @@ -33,41 +33,6 @@ namespace cvc5 { namespace theory { namespace quantifiers { -bool VariadicTrie::add(Node n, const std::vector<Node>& i) -{ - VariadicTrie* curr = this; - for (const Node& ic : i) - { - curr = &(curr->d_children[ic]); - } - if (curr->d_data.isNull()) - { - curr->d_data = n; - return true; - } - return false; -} - -bool VariadicTrie::hasSubset(const std::vector<Node>& is) const -{ - if (!d_data.isNull()) - { - return true; - } - for (const std::pair<const Node, VariadicTrie>& p : d_children) - { - Node n = p.first; - if (std::find(is.begin(), is.end(), n) != is.end()) - { - if (p.second.hasSubset(is)) - { - return true; - } - } - } - return false; -} - CegisCoreConnective::CegisCoreConnective(Env& env, QuantifiersState& qs, QuantifiersInferenceManager& qim, @@ -595,38 +560,6 @@ bool CegisCoreConnective::Component::addToAsserts(CegisCoreConnective* p, return true; } -void CegisCoreConnective::getModel(SolverEngine& smt, - std::vector<Node>& vals) const -{ - for (const Node& v : d_vars) - { - Node mv = smt.getValue(v); - Trace("sygus-ccore-model") << v << " -> " << mv << " "; - vals.push_back(mv); - } -} - -bool CegisCoreConnective::getUnsatCore( - SolverEngine& smt, - const std::unordered_set<Node>& queryAsserts, - std::vector<Node>& uasserts) const -{ - UnsatCore uc = smt.getUnsatCore(); - bool hasQuery = false; - for (UnsatCore::const_iterator i = uc.begin(); i != uc.end(); ++i) - { - Node uassert = *i; - Trace("sygus-ccore-debug") << " uc " << uassert << std::endl; - if (queryAsserts.find(uassert) != queryAsserts.end()) - { - hasQuery = true; - continue; - } - uasserts.push_back(uassert); - } - return hasQuery; -} - Result CegisCoreConnective::checkSat(Node n, std::vector<Node>& mvs) const { Trace("sygus-ccore-debug") << "...check-sat " << n << "..." << std::endl; @@ -758,7 +691,8 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, std::unordered_set<Node> queryAsserts; queryAsserts.insert(ccheck.getFormula()); queryAsserts.insert(d_sc); - bool hasQuery = getUnsatCore(*checkSol, queryAsserts, uasserts); + bool hasQuery = + getUnsatCoreFromSubsolver(*checkSol, queryAsserts, uasserts); // now, check the side condition bool falseCore = false; if (!d_sc.isNull()) @@ -794,7 +728,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, uasserts.clear(); std::unordered_set<Node> queryAsserts2; queryAsserts2.insert(d_sc); - getUnsatCore(*checkSc, queryAsserts2, uasserts); + getUnsatCoreFromSubsolver(*checkSc, queryAsserts2, uasserts); falseCore = true; } } @@ -838,7 +772,7 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck, // it does not entail the postcondition, add an assertion that blocks // the current point mvs.clear(); - getModel(*checkSol, mvs); + getModelFromSubsolver(*checkSol, d_vars, mvs); // should evaluate to true Node ean = evaluatePt(an, Node::null(), mvs); Assert(ean.isConst() && ean.getConst<bool>()); diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.h b/src/theory/quantifiers/sygus/cegis_core_connective.h index 3ee631dea..26784f939 100644 --- a/src/theory/quantifiers/sygus/cegis_core_connective.h +++ b/src/theory/quantifiers/sygus/cegis_core_connective.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/node_trie.h" +#include "expr/variadic_trie.h" #include "smt/env_obj.h" #include "theory/quantifiers/sygus/cegis.h" #include "util/result.h" @@ -33,30 +34,6 @@ class SolverEngine; namespace theory { namespace quantifiers { -/** - * A trie that stores data at undetermined depth. Storing data at - * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which - * assumes all data is stored at a fixed depth. - * - * Since data can be stored at any depth, we require both a d_children field - * and a d_data field. - */ -class VariadicTrie -{ - public: - /** the children of this node */ - std::map<Node, VariadicTrie> d_children; - /** the data at this node */ - Node d_data; - /** - * Add data with identifier n indexed by i, return true if data is not already - * stored at the node indexed by i. - */ - bool add(Node n, const std::vector<Node>& i); - /** Is there any data in this trie that is indexed by any subset of is? */ - bool hasSubset(const std::vector<Node>& is) const; -}; - /** CegisCoreConnective * * A sygus module that is specialized in handling conjectures of the form: @@ -336,23 +313,6 @@ class CegisCoreConnective : public Cegis Node d_sc; //-----------------------------------for SMT engine calls /** - * Assuming smt has just been called to check-sat and returned "SAT", this - * method adds the model for d_vars to mvs. - */ - void getModel(SolverEngine& smt, std::vector<Node>& mvs) const; - /** - * Assuming smt has just been called to check-sat and returned "UNSAT", this - * method get the unsat core and adds it to uasserts. - * - * The assertions in the argument queryAsserts (which we are not interested - * in tracking in the unsat core) are excluded from uasserts. - * If one of the formulas in queryAsserts was in the unsat core, then this - * method returns true. Otherwise, this method returns false. - */ - bool getUnsatCore(SolverEngine& smt, - const std::unordered_set<Node>& queryAsserts, - std::vector<Node>& uasserts) const; - /** * Return the result of checking satisfiability of formula n. * If n was satisfiable, then we store the model for d_vars in mvs. */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 43c958ff9..9b4cfb9e1 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,6 +20,7 @@ #include "expr/ascription_type.h" #include "expr/dtype_cons.h" +#include "expr/node_algorithm.h" #include "options/quantifiers_options.h" #include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/sygus_datatype_utils.h" @@ -420,6 +421,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, { // generate constant array over the first element of the constituent type Node c = type.mkGroundTerm(); + // note that c should never contain an uninterpreted constant + Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c)); ops.push_back(c); } else if (type.isRoundingMode()) 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<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()); 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<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: @@ -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<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 */ 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<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 */ |