This makes relational triggers its own kind of instantiation match generator. Future PRs will delete the code interleaved in the core InstMatchGenerator class for handling relational triggers.
This PR also fixes two issues related to how trigger techniques are combined:
(1) instantiation match generators that are generated as part of multi-triggers now are properly specialized (using getInstMatchGenerator),
(2) there was a bug with auto-generated triggers: when the first auto-generated trigger was generated that was already a user trigger, then we would ignore all other auto-generated triggers.
This is work towards finding a solution for the choice.move.hard Facebook benchmark, where relational-triggers appear to be a possible solution.
theory/quantifiers/ematching/instantiation_engine.h
theory/quantifiers/ematching/pattern_term_selector.cpp
theory/quantifiers/ematching/pattern_term_selector.h
+ theory/quantifiers/ematching/relational_match_generator.cpp
+ theory/quantifiers/ematching/relational_match_generator.h
theory/quantifiers/ematching/trigger.cpp
theory/quantifiers/ematching/trigger.h
theory/quantifiers/ematching/trigger_database.cpp
#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"
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;
}
Node q,
Node n)
{
+ // maybe variable match generator
if (n.getKind() != INST_CONSTANT)
{
Trace("var-trigger-debug")
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);
}
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;
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]])
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
}
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);
}
--- /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.
+ * ****************************************************************************
+ *
+ * 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
--- /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.
+ * ****************************************************************************
+ *
+ * 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
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;
{
return 0;
}
- if (isAtomicTrigger(n))
+ if (isAtomicTrigger(n) || isUsableRelationTrigger(n))
{
return 1;
}
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
* 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);
regress0/quantifiers/simp-len.smt2
regress0/quantifiers/simp-typ-test.smt2
regress0/quantifiers/ufnia-fv-delta.smt2
+ regress0/quantifiers/veqt-delta.smt2
regress0/rec-fun-const-parse-bug.smt2
regress0/rels/addr_book_0.cvc.smt2
regress0/rels/atom_univ2.cvc.smt2
regress1/quantifiers/cee-npnt-dd.smt2
regress1/quantifiers/cee-os-delta.smt2
regress1/quantifiers/cdt-0208-to.smt2
+ regress1/quantifiers/choice-move-delta-relt.smt2
regress1/quantifiers/const.cvc.smt2
regress1/quantifiers/constfunc.cvc.smt2
regress1/quantifiers/ddatv-delta2.smt2
--- /dev/null
+; COMMAND-LINE: --relational-triggers
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort S 0)
+(declare-fun f () S)
+(assert (forall ((? S)) (= ? f)))
+(assert (exists ((? S) (v S)) (distinct ? v)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --relational-triggers --user-pat=use
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun F (Int) Bool)
+(assert (forall ((v Int)) (! (= (F 0) (< v 0)) :qid |outputbpl.194:24| :pattern ((F 0)))))
+(check-sat)
projects / cvc5.git / commitdiff