diff options
Diffstat (limited to 'src/theory/quantifiers/ematching')
7 files changed, 309 insertions, 25 deletions
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); |