This PR refactors the initialization of the transcendental solver, decoupling the setup of generic caches from initial lemmas for exponential and sine functions.
d_tangentPlaneSlv.check(true);
break;
case InferStep::TRANS_INIT:
- d_trSlv.initLastCall(assertions, false_asserts, xts);
+ d_trSlv.initLastCall(xts);
break;
case InferStep::TRANS_INITIAL:
d_trSlv.checkTranscendentalInitialRefine();
ExponentialSolver::~ExponentialSolver() {}
+void ExponentialSolver::doPurification(TNode a, TNode new_a, TNode y)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ // do both equalities to ensure that new_a becomes a preregistered term
+ Node lem = nm->mkNode(Kind::AND, a.eqNode(new_a), a[0].eqNode(y));
+ // note we must do preprocess on this lemma
+ Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
+ << std::endl;
+ NlLemma nlem(
+ lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG);
+ d_data->d_im.addPendingArithLemma(nlem);
+}
+
void ExponentialSolver::checkInitialRefine()
{
NodeManager* nm = NodeManager::currentNM();
ExponentialSolver(TranscendentalState* tstate);
~ExponentialSolver();
- void initLastCall(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts);
+ /**
+ * Ensures that new_a is properly registered as a term where new_a is the
+ * purified version of a, y being the new skolem used for purification.
+ */
+ void doPurification(TNode a, TNode new_a, TNode y);
/**
* check initial refine
namespace arith {
namespace nl {
namespace transcendental {
+namespace {
+
+/**
+ * Ensure a is in the main phase:
+ * -pi <= a <= pi
+ */
+inline Node mkValidPhase(TNode a, TNode pi)
+{
+ return mkBounded(
+ NodeManager::currentNM()->mkNode(Kind::MULT, mkRationalNode(-1), pi),
+ a,
+ pi);
+}
+} // namespace
SineSolver::SineSolver(TranscendentalState* tstate) : d_data(tstate) {}
SineSolver::~SineSolver() {}
+void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ Assert(a.getKind() == Kind::SINE);
+ Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl;
+ Assert(!d_data->d_pi.isNull());
+ Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
+ // TODO (cvc4-projects #47) : do not introduce shift here, instead needs model-based
+ // refinement for constant shifts (cvc4-projects #1284)
+ Node lem = nm->mkNode(
+ Kind::AND,
+ mkValidPhase(y, d_data->d_pi),
+ nm->mkNode(Kind::ITE,
+ mkValidPhase(a[0], d_data->d_pi),
+ a[0].eqNode(y),
+ a[0].eqNode(nm->mkNode(Kind::PLUS,
+ y,
+ nm->mkNode(Kind::MULT,
+ nm->mkConst(Rational(2)),
+ shift,
+ d_data->d_pi)))),
+ new_a.eqNode(a));
+ // note we must do preprocess on this lemma
+ Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
+ << std::endl;
+ NlLemma nlem(
+ lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG);
+ d_data->d_im.addPendingArithLemma(nlem);
+}
+
void SineSolver::checkInitialRefine()
{
NodeManager* nm = NodeManager::currentNM();
if (d_tf_initial_refine.find(t) == d_tf_initial_refine.end())
{
d_tf_initial_refine[t] = true;
- Node lem;
Node symn = nm->mkNode(Kind::SINE,
nm->mkNode(Kind::MULT, d_data->d_neg_one, t[0]));
symn = Rewriter::rewrite(symn);
d_data->d_trMaster[symn] = symn;
d_data->d_trSlaves[symn].insert(symn);
Assert(d_data->d_trSlaves.find(t) != d_data->d_trSlaves.end());
- std::vector<Node> children;
- lem =
- nm->mkNode(Kind::AND,
- // bounds
- nm->mkNode(Kind::AND,
- nm->mkNode(Kind::LEQ, t, d_data->d_one),
- nm->mkNode(Kind::GEQ, t, d_data->d_neg_one)),
- // symmetry
- nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero),
- // sign
- nm->mkNode(Kind::EQUAL,
- nm->mkNode(Kind::LT, t[0], d_data->d_zero),
- nm->mkNode(Kind::LT, t, d_data->d_zero)),
- // zero val
- nm->mkNode(Kind::EQUAL,
- nm->mkNode(Kind::GT, t[0], d_data->d_zero),
- nm->mkNode(Kind::GT, t, d_data->d_zero)));
- lem = nm->mkNode(
- Kind::AND,
- lem,
- // zero tangent
- nm->mkNode(Kind::AND,
- nm->mkNode(Kind::IMPLIES,
- nm->mkNode(Kind::GT, t[0], d_data->d_zero),
- nm->mkNode(Kind::LT, t, t[0])),
- nm->mkNode(Kind::IMPLIES,
- nm->mkNode(Kind::LT, t[0], d_data->d_zero),
- nm->mkNode(Kind::GT, t, t[0]))),
- // pi tangent
- nm->mkNode(
- Kind::AND,
- nm->mkNode(
- Kind::IMPLIES,
- nm->mkNode(Kind::LT, t[0], d_data->d_pi),
- nm->mkNode(Kind::LT,
- t,
- nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))),
- nm->mkNode(
- Kind::IMPLIES,
- nm->mkNode(Kind::GT, t[0], d_data->d_pi_neg),
- nm->mkNode(
- Kind::GT,
- t,
- nm->mkNode(Kind::MINUS, d_data->d_pi_neg, t[0])))));
- if (!lem.isNull())
{
- d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_INIT_REFINE);
+ // sine bounds: -1 <= sin(t) <= 1
+ Node lem = nm->mkNode(Kind::AND,
+ nm->mkNode(Kind::LEQ, t, d_data->d_one),
+ nm->mkNode(Kind::GEQ, t, d_data->d_neg_one));
+ d_data->d_im.addPendingArithLemma(
+ lem, InferenceId::NL_T_INIT_REFINE);
+ }
+ {
+ // sine symmetry: sin(t) - sin(-t) = 0
+ Node lem = nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero);
+ d_data->d_im.addPendingArithLemma(
+ lem, InferenceId::NL_T_INIT_REFINE);
+ }
+ {
+ // sine zero tangent:
+ // t > 0 => sin(t) < t
+ // t < 0 => sin(t) > t
+ Node lem =
+ nm->mkNode(Kind::AND,
+ nm->mkNode(Kind::IMPLIES,
+ nm->mkNode(Kind::GT, t[0], d_data->d_zero),
+ nm->mkNode(Kind::LT, t, t[0])),
+ nm->mkNode(Kind::IMPLIES,
+ nm->mkNode(Kind::LT, t[0], d_data->d_zero),
+ nm->mkNode(Kind::GT, t, t[0])));
+ d_data->d_im.addPendingArithLemma(
+ lem, InferenceId::NL_T_INIT_REFINE);
+ }
+ {
+ // sine pi tangent:
+ // t > -pi => sin(t) > -pi-t
+ // t < pi => sin(t) < pi-t
+ Node lem = nm->mkNode(
+ Kind::AND,
+ nm->mkNode(
+ Kind::IMPLIES,
+ nm->mkNode(Kind::GT, t[0], d_data->d_pi_neg),
+ nm->mkNode(Kind::GT,
+ t,
+ nm->mkNode(Kind::MINUS, d_data->d_pi_neg, t[0]))),
+ nm->mkNode(
+ Kind::IMPLIES,
+ nm->mkNode(Kind::LT, t[0], d_data->d_pi),
+ nm->mkNode(Kind::LT,
+ t,
+ nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))));
+ d_data->d_im.addPendingArithLemma(
+ lem, InferenceId::NL_T_INIT_REFINE);
+ }
+ {
+ Node lem =
+ nm->mkNode(Kind::AND,
+ // sign
+ nm->mkNode(Kind::EQUAL,
+ nm->mkNode(Kind::LT, t[0], d_data->d_zero),
+ nm->mkNode(Kind::LT, t, d_data->d_zero)),
+ // zero val
+ nm->mkNode(Kind::EQUAL,
+ nm->mkNode(Kind::GT, t[0], d_data->d_zero),
+ nm->mkNode(Kind::GT, t, d_data->d_zero)));
+ d_data->d_im.addPendingArithLemma(
+ lem, InferenceId::NL_T_INIT_REFINE);
}
}
}
Trace("nl-ext-sine") << "*** Tangent plane lemma : " << lem << std::endl;
Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
// Figure 3 : line 9
- d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true);
+ d_data->d_im.addPendingArithLemma(
+ lem, InferenceId::NL_T_TANGENT, nullptr, true);
}
void SineSolver::doSecantLemmas(TNode e,
SineSolver(TranscendentalState* tstate);
~SineSolver();
- void initLastCall(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts);
+ /**
+ * Introduces new_a as purified version of a which is also shifted to the main
+ * phase (from -pi to pi). y is the new skolem used for purification.
+ */
+ void doPhaseShift(TNode a, TNode new_a, TNode y);
/**
* check initial refine
TranscendentalSolver::~TranscendentalSolver() {}
-void TranscendentalSolver::initLastCall(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts)
+void TranscendentalSolver::initLastCall(const std::vector<Node>& xts)
{
- d_tstate.init(assertions, false_asserts, xts);
+ std::vector<Node> needsMaster;
+ d_tstate.init(xts, needsMaster);
+
+ if (d_tstate.d_im.hasUsed()) {
+ return;
+ }
+
+ NodeManager* nm = NodeManager::currentNM();
+ for (const Node& a : needsMaster)
+ {
+ // should not have processed this already
+ Assert(d_tstate.d_trMaster.find(a) == d_tstate.d_trMaster.end());
+ Kind k = a.getKind();
+ Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
+ Node y =
+ nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
+ Node new_a = nm->mkNode(k, y);
+ d_tstate.d_trSlaves[new_a].insert(new_a);
+ d_tstate.d_trSlaves[new_a].insert(a);
+ d_tstate.d_trMaster[a] = new_a;
+ d_tstate.d_trMaster[new_a] = new_a;
+ switch (k)
+ {
+ case Kind::SINE: d_sineSlv.doPhaseShift(a, new_a, y); break;
+ case Kind::EXPONENTIAL: d_expSlv.doPurification(a, new_a, y); break;
+ default: AlwaysAssert(false) << "Unexpected Kind " << k;
+ }
+ }
}
bool TranscendentalSolver::preprocessAssertionsCheckModel(
* This call may add lemmas to lems based on registering term
* information (for example, purification of sine terms).
*/
- void initLastCall(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts);
+ void initLastCall(const std::vector<Node>& xts);
/** increment taylor degree */
void incrementTaylorDegree();
/** get taylor degree */
d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
}
-void TranscendentalState::init(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts)
+void TranscendentalState::init(const std::vector<Node>& xts,
+ std::vector<Node>& needsMaster)
{
d_funcCongClass.clear();
d_funcMap.clear();
d_tf_region.clear();
- NodeManager* nm = NodeManager::currentNM();
-
- // register the extended function terms
- std::vector<Node> trNeedsMaster;
bool needPi = false;
// for computing congruence
std::map<Kind, ArgTrie> argTrie;
- for (unsigned i = 0, xsize = xts.size(); i < xsize; i++)
+ for (std::size_t i = 0, xsize = xts.size(); i < xsize; ++i)
{
+ // Ignore if it is not a transcendental
+ if (!isTranscendentalKind(xts[i].getKind()))
+ {
+ continue;
+ }
Node a = xts[i];
Kind ak = a.getKind();
bool consider = true;
- // if is an unpurified application of SINE, or it is a transcendental
- // applied to a trancendental, purify.
- if (isTranscendentalKind(ak))
+ // if we've already computed master for a
+ if (d_trMaster.find(a) != d_trMaster.end())
+ {
+ // a master has at least one slave
+ consider = (d_trSlaves.find(a) != d_trSlaves.end());
+ }
+ else
{
- // if we've already computed master for a
- if (d_trMaster.find(a) != d_trMaster.end())
+ if (ak == Kind::SINE)
{
- // a master has at least one slave
- consider = (d_trSlaves.find(a) != d_trSlaves.end());
+ // always not a master
+ consider = false;
}
else
{
- if (ak == Kind::SINE)
- {
- // always not a master
- consider = false;
- }
- else
+ for (const Node& ac : a)
{
- for (const Node& ac : a)
+ if (isTranscendentalKind(ac.getKind()))
{
- if (isTranscendentalKind(ac.getKind()))
- {
- consider = false;
- break;
- }
+ consider = false;
+ break;
}
}
- if (!consider)
- {
- // wait to assign a master below
- trNeedsMaster.push_back(a);
- }
- else
- {
- d_trMaster[a] = a;
- d_trSlaves[a].insert(a);
- }
+ }
+ if (!consider)
+ {
+ // wait to assign a master below
+ needsMaster.push_back(a);
+ }
+ else
+ {
+ d_trMaster[a] = a;
+ d_trSlaves[a].insert(a);
}
}
if (ak == Kind::EXPONENTIAL || ak == Kind::SINE)
// if we didn't indicate that it should be purified above
if (consider)
{
- std::vector<Node> repList;
- for (const Node& ac : a)
- {
- Node r = d_model.computeConcreteModelValue(ac);
- repList.push_back(r);
- }
- Node aa = argTrie[ak].add(a, repList);
- if (aa != a)
- {
- // apply congruence to pairs of terms that are disequal and congruent
- Assert(aa.getNumChildren() == a.getNumChildren());
- Node mvaa = d_model.computeAbstractModelValue(a);
- Node mvaaa = d_model.computeAbstractModelValue(aa);
- if (mvaa != mvaaa)
- {
- std::vector<Node> exp;
- for (unsigned j = 0, size = a.getNumChildren(); j < size; j++)
- {
- exp.push_back(a[j].eqNode(aa[j]));
- }
- Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
- Node cong_lemma = nm->mkNode(Kind::OR, expn.negate(), a.eqNode(aa));
- d_im.addPendingArithLemma(cong_lemma, InferenceId::NL_CONGRUENCE);
- }
- }
- else
- {
- // new representative of congruence class
- d_funcMap[ak].push_back(a);
- }
- // add to congruence class
- d_funcCongClass[aa].push_back(a);
+ ensureCongruence(a, argTrie);
}
}
else if (ak == Kind::PI)
getCurrentPiBounds();
}
- if (d_im.hasUsed())
- {
- return;
- }
-
- // process SINE phase shifting
- for (const Node& a : trNeedsMaster)
- {
- // should not have processed this already
- Assert(d_trMaster.find(a) == d_trMaster.end());
- Kind k = a.getKind();
- Assert(k == Kind::SINE || k == Kind::EXPONENTIAL);
- Node y =
- nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
- Node new_a = nm->mkNode(k, y);
- d_trSlaves[new_a].insert(new_a);
- d_trSlaves[new_a].insert(a);
- d_trMaster[a] = new_a;
- d_trMaster[new_a] = new_a;
- Node lem;
- if (k == Kind::SINE)
- {
- Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a
- << std::endl;
- Assert(!d_pi.isNull());
- Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
- // TODO : do not introduce shift here, instead needs model-based
- // refinement for constant shifts (cvc4-projects #1284)
- lem = nm->mkNode(
- Kind::AND,
- transcendental::mkValidPhase(y, d_pi),
- nm->mkNode(
- Kind::ITE,
- transcendental::mkValidPhase(a[0], d_pi),
- a[0].eqNode(y),
- a[0].eqNode(nm->mkNode(
- Kind::PLUS,
- y,
- nm->mkNode(
- Kind::MULT, nm->mkConst(Rational(2)), shift, d_pi)))),
- new_a.eqNode(a));
- }
- else
- {
- // do both equalities to ensure that new_a becomes a preregistered term
- lem = nm->mkNode(Kind::AND, a.eqNode(new_a), a[0].eqNode(y));
- }
- // note we must do preprocess on this lemma
- Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
- << std::endl;
- NlLemma nlem(
- lem, LemmaProperty::PREPROCESS, nullptr, InferenceId::NL_T_PURIFY_ARG);
- d_im.addPendingArithLemma(nlem);
- }
-
if (Trace.isOn("nl-ext-mv"))
{
Trace("nl-ext-mv") << "Arguments of trancendental functions : "
}
}
+void TranscendentalState::ensureCongruence(TNode a,
+ std::map<Kind, ArgTrie>& argTrie)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ std::vector<Node> repList;
+ for (const Node& ac : a)
+ {
+ Node r = d_model.computeConcreteModelValue(ac);
+ repList.push_back(r);
+ }
+ Node aa = argTrie[a.getKind()].add(a, repList);
+ if (aa != a)
+ {
+ // apply congruence to pairs of terms that are disequal and congruent
+ Assert(aa.getNumChildren() == a.getNumChildren());
+ Node mvaa = d_model.computeAbstractModelValue(a);
+ Node mvaaa = d_model.computeAbstractModelValue(aa);
+ if (mvaa != mvaaa)
+ {
+ std::vector<Node> exp;
+ for (unsigned j = 0, size = a.getNumChildren(); j < size; j++)
+ {
+ exp.push_back(a[j].eqNode(aa[j]));
+ }
+ Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(Kind::AND, exp);
+ Node cong_lemma = expn.impNode(a.eqNode(aa));
+ d_im.addPendingArithLemma(cong_lemma, InferenceId::NL_CONGRUENCE);
+ }
+ }
+ else
+ {
+ // new representative of congruence class
+ d_funcMap[a.getKind()].push_back(a);
+ }
+ // add to congruence class
+ d_funcCongClass[aa].push_back(a);
+}
+
void TranscendentalState::mkPi()
{
NodeManager* nm = NodeManager::currentNM();
/** init last call
*
- * This is called at the beginning of last call effort check, where
- * assertions are the set of assertions belonging to arithmetic,
- * false_asserts is the subset of assertions that are false in the current
- * model, and xts is the set of extended function terms that are active in
- * the current context.
+ * This is called at the beginning of last call effort check xts is the set of
+ * extended function terms that are active in the current context.
*
* This call may add lemmas to lems based on registering term
- * information (for example, purification of sine terms).
+ * information (for example to ensure congruence of terms).
+ * It puts terms that need to be treated further as a master term on their own
+ * (for example purification of sine terms) into needsMaster.
*/
- void init(const std::vector<Node>& assertions,
- const std::vector<Node>& false_asserts,
- const std::vector<Node>& xts);
+ void init(const std::vector<Node>& xts, std::vector<Node>& needsMaster);
+
+ /**
+ * Checks for terms that are congruent but disequal to a.
+ * If any are found, appropriate lemmas are sent.
+ * @param a Some node
+ * @param argTrie Lookup for equivalence classes
+ */
+ void ensureCongruence(TNode a, std::map<Kind, ArgTrie>& argTrie);
/** Initialize members for pi-related values */
void mkPi();
projects / cvc5.git / commitdiff