namespace quantifiers {
namespace inst {
-PatternTermSelector::PatternTermSelector(Node q,
+PatternTermSelector::PatternTermSelector(const Options& opts,
+ Node q,
options::TriggerSelMode tstrt,
const std::vector<Node>& exc,
bool filterInst)
- : d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
+ : d_opts(opts),
+ d_quant(q),
+ d_tstrt(tstrt),
+ d_excluded(exc),
+ d_filterInst(filterInst)
{
}
PatternTermSelector::~PatternTermSelector() {}
-bool PatternTermSelector::isUsable(Node n, Node q)
+bool PatternTermSelector::isUsable(const Options& opts, Node n, Node q)
{
if (quantifiers::TermUtil::getInstConstAttr(n) != q)
{
{
for (const Node& nc : n)
{
- if (!isUsable(nc, q))
+ if (!isUsable(opts, nc, q))
{
return false;
}
{
return true;
}
- if (options::purifyTriggers())
+ if (opts.quantifiers.purifyTriggers)
{
Node x = getInversionVariable(n);
if (!x.isNull())
return false;
}
-Node PatternTermSelector::getIsUsableEq(Node q, Node n)
+Node PatternTermSelector::getIsUsableEq(const Options& opts, Node q, Node n)
{
Assert(TriggerTermInfo::isRelationalTrigger(n));
for (size_t i = 0; i < 2; i++)
{
- if (isUsableEqTerms(q, n[i], n[1 - i]))
+ if (isUsableEqTerms(opts, q, n[i], n[1 - i]))
{
if (i == 1 && n.getKind() == EQUAL
&& !quantifiers::TermUtil::hasInstConstAttr(n[0]))
return Node::null();
}
-bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
+bool PatternTermSelector::isUsableEqTerms(const Options& opts,
+ Node q,
+ Node n1,
+ Node n2)
{
if (n1.getKind() == INST_CONSTANT)
{
- if (options::relationalTriggers())
+ if (opts.quantifiers.relationalTriggers)
{
Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
if (q1 != q)
// when n1 and n2 are swapped
}
}
- else if (isUsableAtomicTrigger(n1, q))
+ else if (isUsableAtomicTrigger(opts, n1, q))
{
- if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
+ if (opts.quantifiers.relationalTriggers && n2.getKind() == INST_CONSTANT
&& quantifiers::TermUtil::getInstConstAttr(n2) == q
&& !expr::hasSubterm(n1, n2))
{
return false;
}
-Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
+Node PatternTermSelector::getIsUsableTrigger(const Options& opts,
+ Node n,
+ Node q)
{
bool pol = true;
Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
}
else if (TriggerTermInfo::isRelationalTrigger(n))
{
- Node rtr = getIsUsableEq(q, n);
+ Node rtr = getIsUsableEq(opts, q, n);
if (rtr.isNull() && n[0].getType().isRealOrInt())
{
// try to solve relation
{
if (it->first.getKind() == INST_CONSTANT)
{
- trySolve = options::relationalTriggers();
+ trySolve = opts.quantifiers.relationalTriggers;
}
- else if (isUsableTrigger(it->first, q))
+ else if (isUsableTrigger(opts, it->first, q))
{
trySolve = true;
}
Node veq;
if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
{
- rtr = getIsUsableEq(q, veq);
+ rtr = getIsUsableEq(opts, q, veq);
}
// either all solves will succeed or all solves will fail
break;
Trace("trigger-debug") << n << " usable : "
<< (quantifiers::TermUtil::getInstConstAttr(n) == q)
<< " " << TriggerTermInfo::isAtomicTrigger(n) << " "
- << isUsable(n, q) << std::endl;
- if (isUsableAtomicTrigger(n, q))
+ << isUsable(opts, n, q) << std::endl;
+ if (isUsableAtomicTrigger(opts, n, q))
{
return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
}
return Node::null();
}
-bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
+bool PatternTermSelector::isUsableAtomicTrigger(const Options& opts,
+ Node n,
+ Node q)
{
return quantifiers::TermUtil::getInstConstAttr(n) == q
- && TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
+ && TriggerTermInfo::isAtomicTrigger(n) && isUsable(opts, n, q);
}
-bool PatternTermSelector::isUsableTrigger(Node n, Node q)
+bool PatternTermSelector::isUsableTrigger(const Options& opts, Node n, Node q)
{
- Node nu = getIsUsableTrigger(n, q);
+ Node nu = getIsUsableTrigger(opts, n, q);
return !nu.isNull();
}
&& std::find(d_excluded.begin(), d_excluded.end(), n)
== d_excluded.end())
{
- nu = getIsUsableTrigger(n, d_quant);
+ nu = getIsUsableTrigger(d_opts, n, d_quant);
if (!nu.isNull() && nu != n)
{
collectTermsInternal(
}
}
Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
- Assert(isUsableTrigger(nu, d_quant));
+ Assert(isUsableTrigger(d_opts, nu, d_quant));
Trace("auto-gen-trigger-debug2")
<< "...add usable trigger : " << nu << std::endl;
tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
return Node::null();
}
-void PatternTermSelector::getTriggerVariables(Node n,
+void PatternTermSelector::getTriggerVariables(const Options& opts,
+ Node n,
Node q,
std::vector<Node>& tvars)
{
- PatternTermSelector pts(q, options::TriggerSelMode::ALL);
+ PatternTermSelector pts(opts, q, options::TriggerSelMode::ALL);
std::vector<Node> patTerms;
std::map<Node, TriggerTermInfo> tinfo;
// collect all patterns from n
{
public:
/**
+ * @param opts Reference to the options, which impacts pattern term selection
* @param q The quantified formula we are selecting pattern terms for
* @param tstrt the selection strategy (see options/quantifiers_mode.h),
* @param exc The set of terms we are excluding as pattern terms.
* also returning f(f(x)). This is default true since it helps in practice
* to filter trigger instances.
*/
- PatternTermSelector(Node q,
+ PatternTermSelector(const Options& opts,
+ Node q,
options::TriggerSelMode tstrt,
const std::vector<Node>& exc = {},
bool filterInst = true);
* (2) Relational triggers are put into solved form, e.g.
* getIsUsableTrigger( (= (+ x a) 5), q ) may return (= x (- 5 a)).
*/
- static Node getIsUsableTrigger(Node n, Node q);
+ static Node getIsUsableTrigger(const Options& opts, Node n, Node q);
/** get the variable associated with an inversion for n
*
* A term n with an inversion variable x has the following property :
* This returns the union of all free variables in usable triggers that are
* subterms of n.
*/
- static void getTriggerVariables(Node n, Node q, std::vector<Node>& tvars);
+ static void getTriggerVariables(const Options& opts,
+ Node n,
+ Node q,
+ std::vector<Node>& tvars);
protected:
/** Is n a usable trigger in quantified formula q?
* A usable trigger is one that is matchable and contains free variables only
* from q.
*/
- static bool isUsableTrigger(Node n, Node q);
+ static bool isUsableTrigger(const Options& opts, Node n, Node q);
/** Is n a usable atomic trigger?
*
* A usable atomic trigger is a term that is both a useable trigger and an
* atomic trigger.
*/
- static bool isUsableAtomicTrigger(Node n, Node q);
+ static bool isUsableAtomicTrigger(const Options& opts, Node n, Node q);
/** is subterm of trigger usable (helper function for isUsableTrigger) */
- static bool isUsable(Node n, Node q);
+ static bool isUsable(const Options& opts, Node n, Node q);
/** returns an equality that is equivalent to the equality eq and
* is a usable trigger for q if one exists, otherwise returns Node::null().
*/
- static Node getIsUsableEq(Node q, Node eq);
+ static Node getIsUsableEq(const Options& opts, Node q, Node eq);
/** returns whether n1 == n2 is a usable (relational) trigger for q. */
- static bool isUsableEqTerms(Node q, Node n1, Node n2);
+ static bool isUsableEqTerms(const Options& opts, Node q, Node n1, Node n2);
/** Helper for collect, with a fixed strategy for selection and filtering */
void collectInternal(Node n,
std::vector<Node>& patTerms,
Node n2,
const std::vector<Node>& fv1,
const std::vector<Node>& fv2);
+ /** Reference to options */
+ const Options& d_opts;
/** The quantified formula this trigger is for. */
Node d_quant;
/** The trigger selection strategy */
namespace theory {
namespace quantifiers {
-QuantifiersMacros::QuantifiersMacros(QuantifiersRegistry& qr) : d_qreg(qr) {}
+QuantifiersMacros::QuantifiersMacros(Env& env, QuantifiersRegistry& qr)
+ : EnvObj(env), d_qreg(qr)
+{
+}
Node QuantifiersMacros::solve(Node lit, bool reqGround)
{
Trace("macros-debug")
<< "...does not contain bad (recursive) operator." << std::endl;
// must be ground UF term if mode is GROUND_UF
- if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF
+ if (options().quantifiers.macrosQuantMode
+ != options::MacrosQuantMode::GROUND_UF
|| preservesTriggerVariables(lit, n_def))
{
Trace("macros-debug")
quantifiers::TermUtil::computeInstConstContainsForQuant(q, icn, var);
Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl;
std::vector<Node> trigger_var;
- inst::PatternTermSelector::getTriggerVariables(icn, q, trigger_var);
+ inst::PatternTermSelector::getTriggerVariables(
+ d_env.getOptions(), icn, q, trigger_var);
Trace("macros-debug2") << "Done." << std::endl;
// only if all variables are also trigger variables
return trigger_var.size() >= var.size();
projects / cvc5.git / commitdiff