Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl;
std::vector<Node> pvars;
std::vector<Node> psubs;
- for (std::pair<const Node, Node>& tb : d_tr_base)
+ for (std::pair<const Node, Node>& tb : d_trMaster)
{
pvars.push_back(tb.first);
psubs.push_back(tb.second);
}
// get model bounds for all transcendental functions
- Trace("nl-ext-cm-debug") << " get bounds for transcendental functions..."
- << std::endl;
- for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
+ Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..."
+ << std::endl;
+ for (std::pair<const Kind, std::vector<Node> >& tfs : d_funcMap)
{
Kind k = tfs.first;
for (const Node& tf : tfs.second)
{
+ Trace("nl-ext-cm") << "- Term: " << tf << std::endl;
bool success = true;
// tf is Figure 3 : tf( x )
- Node atf = d_model.computeConcreteModelValue(tf);
- Trace("nl-ext-cm-debug")
- << "Value for is " << tf << " is " << atf << std::endl;
Node bl;
Node bu;
if (k == PI)
bl = d_pi_bound[0];
bu = d_pi_bound[1];
}
- else if (d_model.isRefineableTfFun(tf))
+ else
{
- d_model.setUsedApproximate();
std::pair<Node, Node> bounds = getTfModelBounds(tf, d_taylor_degree);
bl = bounds.first;
bu = bounds.second;
+ if (bl != bu)
+ {
+ d_model.setUsedApproximate();
+ }
}
if (!bl.isNull() && !bu.isNull())
{
- // We have rewritten an application of a transcendental function
- // based on the current model values.It could be that the model value
- // rewrites sin(x) ---> sin(-c) ---> -sin(c), thus we need
- // to negate the bounds in this case.
- if (atf.getKind() != tf.getKind())
+ // for each function in the congruence classe
+ for (const Node& ctf : d_funcCongClass[tf])
{
- if (atf.getKind() == MULT && atf.getNumChildren() == 2
- && atf[0] == d_neg_one)
+ // each term in congruence classes should be master terms
+ Assert(d_trSlaves.find(ctf) != d_trSlaves.end());
+ // we set the bounds for each slave of tf
+ for (const Node& stf : d_trSlaves[ctf])
{
- atf = atf[1];
- Node btmp = bl;
- bl = ArithMSum::negate(bu);
- bu = ArithMSum::negate(btmp);
+ Trace("nl-ext-cm") << "...bound for " << stf << " : [" << bl << ", "
+ << bu << "]" << std::endl;
+ success = d_model.addCheckModelBound(stf, bl, bu);
}
}
- success = d_model.addCheckModelBound(atf, bl, bu);
+ }
+ else
+ {
+ Trace("nl-ext-cm") << "...no bound for " << tf << std::endl;
}
if (!success)
{
- Trace("nl-ext-cm-debug")
- << "...failed to set bound for transcendental function."
- << std::endl;
+ // a bound was conflicting
+ Trace("nl-ext-cm") << "...failed to set bound for " << tf << std::endl;
+ Trace("nl-ext-cm") << "-----" << std::endl;
return false;
}
}
}
+ Trace("nl-ext-cm") << "-----" << std::endl;
bool ret = d_model.checkModel(
passertions, false_asserts, d_taylor_degree, lemmas, gs);
return ret;
d_ci.clear();
d_ci_exp.clear();
d_ci_max.clear();
- d_f_map.clear();
+ d_funcCongClass.clear();
+ d_funcMap.clear();
d_tf_region.clear();
std::vector<Node> lemmas;
Trace("nl-ext-mv") << "Extended terms : " << std::endl;
// register the extended function terms
std::map< Node, Node > mvarg_to_term;
- std::vector<Node> tr_no_base;
+ std::vector<Node> trNeedsMaster;
bool needPi = false;
// for computing congruence
std::map<Kind, ArgTrie> argTrie;
d_model.computeAbstractModelValue(a);
d_model.printModelValue("nl-ext-mv", a);
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 (ak == SINE)
+ {
+ // always not a master
+ consider = false;
+ }
+ else
+ {
+ for (const Node& ac : a)
+ {
+ if (isTranscendentalKind(ac.getKind()))
+ {
+ consider = false;
+ break;
+ }
+ }
+ }
+ if (!consider)
+ {
+ // wait to assign a master below
+ trNeedsMaster.push_back(a);
+ }
+ else
+ {
+ d_trMaster[a] = a;
+ d_trSlaves[a].push_back(a);
+ }
+ }
+ }
if (ak == NONLINEAR_MULT)
{
d_ms.push_back( a );
{
needPi = true;
}
- bool consider = true;
- // if is an unpurified application of SINE, or it is a transcendental
- // applied to a trancendental, purify.
- if (isTranscendentalKind(ak))
- {
- if (ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end())
- {
- consider = false;
- }
- else
- {
- for (const Node& ac : a)
- {
- if (isTranscendentalKind(ac.getKind()))
- {
- consider = false;
- break;
- }
- }
- }
- if (!consider)
- {
- tr_no_base.push_back(a);
- }
- }
+ // if we didn't indicate that it should be purified above
if( consider ){
std::vector<Node> repList;
for (const Node& ac : a)
}
else
{
- d_f_map[ak].push_back(a);
+ // new representative of congruence class
+ d_funcMap[ak].push_back(a);
}
+ // add to congruence class
+ d_funcCongClass[aa].push_back(a);
}
}
else if (ak == PI)
{
+ Assert(consider);
needPi = true;
- d_f_map[ak].push_back(a);
+ d_funcMap[ak].push_back(a);
+ d_funcCongClass[a].push_back(a);
}
else
{
}
// process SINE phase shifting
- for (const Node& a : tr_no_base)
- {
- if (d_tr_base.find(a) == d_tr_base.end())
+ 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 == SINE || k == EXPONENTIAL);
+ Node y =
+ nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
+ Node new_a = nm->mkNode(k, y);
+ d_trSlaves[new_a].push_back(new_a);
+ d_trSlaves[new_a].push_back(a);
+ d_trMaster[a] = new_a;
+ d_trMaster[new_a] = new_a;
+ Node lem;
+ if (k == 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(
+ AND,
+ mkValidPhase(y, d_pi),
+ nm->mkNode(
+ ITE,
+ mkValidPhase(a[0], d_pi),
+ a[0].eqNode(y),
+ a[0].eqNode(nm->mkNode(
+ PLUS,
+ y,
+ nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))),
+ new_a.eqNode(a));
+ }
+ else
{
- Node y =
- nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
- Node new_a = nm->mkNode(a.getKind(), y);
- d_tr_is_base[new_a] = true;
- d_tr_base[a] = new_a;
- Node lem;
- if (a.getKind() == 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");
- // FIXME : do not introduce shift here, instead needs model-based
- // refinement for constant shifts (#1284)
- lem = nm->mkNode(
- AND,
- mkValidPhase(y, d_pi),
- nm->mkNode(
- ITE,
- mkValidPhase(a[0], d_pi),
- a[0].eqNode(y),
- a[0].eqNode(nm->mkNode(
- PLUS,
- y,
- nm->mkNode(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(AND, a.eqNode(new_a), a[0].eqNode(y));
- }
- // must do preprocess on this one
- Trace("nl-ext-lemma")
- << "NonlinearExtension::Lemma : purify : " << lem << std::endl;
- lemsPp.push_back(lem);
+ // do both equalities to ensure that new_a becomes a preregistered term
+ lem = nm->mkNode(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;
+ lemsPp.push_back(lem);
}
if (!lemsPp.empty())
{
{
Trace("nl-ext-mv") << "Arguments of trancendental functions : "
<< std::endl;
- for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
{
Kind k = tfl.first;
if (k == SINE || k == EXPONENTIAL)
std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
std::vector< Node > lemmas;
Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl;
- for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
{
Kind k = tfl.first;
for (const Node& t : tfl.second)
Node symn = NodeManager::currentNM()->mkNode(
SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0]));
symn = Rewriter::rewrite( symn );
- //can assume its basis since phase is split over 0
- d_tr_is_base[symn] = true;
- Assert(d_tr_is_base.find(t) != d_tr_is_base.end());
+ // Can assume it is its own master since phase is split over 0,
+ // hence -pi <= t[0] <= pi implies -pi <= -t[0] <= pi.
+ d_trMaster[symn] = symn;
+ d_trSlaves[symn].push_back(symn);
+ Assert(d_trSlaves.find(t) != d_trSlaves.end());
std::vector< Node > children;
lem = NodeManager::currentNM()->mkNode(
std::map< Kind, std::vector< Node > > sorted_tf_args;
std::map< Kind, std::map< Node, Node > > tf_arg_to_term;
- for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
{
Kind k = tfl.first;
if (k == EXPONENTIAL || k == SINE)
//sort by concrete values
smv.d_isConcrete = true;
smv.d_reverse_order = true;
- for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+ for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
{
Kind k = tfl.first;
if( !sorted_tf_args[k].empty() ){
<< std::endl;
// this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
// via Incremental Linearization" by Cimatti et al
- for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
+ for (std::pair<const Kind, std::vector<Node> >& tfs : d_funcMap)
{
Kind k = tfs.first;
if (k == PI)
for (const Node& tf : tfs.second)
{
// tf is Figure 3 : tf( x )
- if (d_model.isRefineableTfFun(tf))
+ Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;
+ // go until max degree is reached, or we don't meet bound criteria
+ for (unsigned d = 1; d <= d_taylor_degree; d++)
{
- Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;
- // go until max degree is reached, or we don't meet bound criteria
- for (unsigned d = 1; d <= d_taylor_degree; d++)
+ Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
+ unsigned prev = lemmas.size();
+ if (checkTfTangentPlanesFun(tf, d, lemmas, lemSE))
{
- Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
- unsigned prev = lemmas.size();
- if (!checkTfTangentPlanesFun(tf, d, lemmas, lemSE))
- {
- Trace("nl-ext-tftp")
- << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl;
- break;
- }
- else
- {
- Trace("nl-ext-tftp") << "...success" << std::endl;
- }
+ Trace("nl-ext-tftp")
+ << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl;
+ break;
+ }
+ else
+ {
+ Trace("nl-ext-tftp") << "...success" << std::endl;
}
}
}
std::vector<Node>& lemmas,
std::map<Node, NlLemmaSideEffect>& lemSE)
{
- Assert(d_model.isRefineableTfFun(tf));
-
NodeManager* nm = NodeManager::currentNM();
Kind k = tf.getKind();
+ // this should only be run on master applications
+ Assert(d_trSlaves.find(tf) != d_trSlaves.end());
// Figure 3 : c
Node c = d_model.computeAbstractModelValue(tf[0]);
int csign = c.getConst<Rational>().sgn();
+ if (csign == 0)
+ {
+ // no secant/tangent plane is necessary
+ return true;
+ }
Assert(csign == 1 || csign == -1);
// Figure 3: P_l, P_u
Trace("nl-ext-tftp-debug") << " concavity is : " << concavity << std::endl;
if (concavity == 0)
{
- return false;
+ // no secant/tangent plane is necessary
+ return true;
}
// bounds for which we are this concavity
// Figure 3: < l, u >
else
{
// we may want to continue getting better bounds
- return true;
+ return false;
}
if (is_tangent)
// secant point c for (tf,d).
lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c));
}
- return false;
+ return true;
}
int NonlinearExtension::regionToMonotonicityDir(Kind k, int region)
Node c = d_model.computeAbstractModelValue(tf[0]);
Assert(c.isConst());
int csign = c.getConst<Rational>().sgn();
- Assert(csign != 0);
+ Kind k = tf.getKind();
+ if (csign == 0)
+ {
+ // at zero, its trivial
+ if (k == SINE)
+ {
+ return std::pair<Node, Node>(d_zero, d_zero);
+ }
+ Assert(k == EXPONENTIAL);
+ return std::pair<Node, Node>(d_one, d_one);
+ }
bool isNeg = csign == -1;
std::vector<Node> pbounds;
- getPolynomialApproximationBoundForArg(tf.getKind(), c, d, pbounds);
+ getPolynomialApproximationBoundForArg(k, c, d, pbounds);
std::vector<Node> bounds;
TNode tfv = d_taylor_real_fv;
//transcendental functions
/**
- * Maps arguments of SINE applications to a fresh skolem. This is used for
- * ensuring that the argument of SINE we process are on the interval
- * [-pi .. pi].
+ * Some transcendental functions f(t) are "purified", e.g. we add
+ * t = y ^ f(t) = f(y) where y is a fresh variable. Those that are not
+ * purified we call "master terms".
+ *
+ * The maps below maintain a master/slave relationship over
+ * transcendental functions (SINE, EXPONENTIAL, PI), where above
+ * f(y) is the master of itself and of f(t).
+ *
+ * This is used for ensuring that the argument y of SINE we process is on the
+ * interval [-pi .. pi], and that exponentials are not applied to arguments
+ * that contain transcendental functions.
*/
- std::map<Node, Node> d_tr_base;
- /** Stores skolems in the range of the above map */
- std::map<Node, bool> d_tr_is_base;
+ std::map<Node, Node> d_trMaster;
+ std::map<Node, std::vector<Node> > d_trSlaves;
+ /** The transcendental functions we have done initial refinements on */
std::map< Node, bool > d_tf_initial_refine;
void mkPi();
std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp;
std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max;
- /** A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } */
- std::map<Kind, std::vector<Node> > d_f_map;
+ /**
+ * Maps representives of a congruence class to the members of that class.
+ *
+ * In detail, a congruence class is a set of terms of the form
+ * { f(t1), ..., f(tn) }
+ * such that t1 = ... = tn in the current context. We choose an arbitrary
+ * term among these to be the repesentative of this congruence class.
+ *
+ * Moreover, notice we compute congruence classes only over terms that
+ * are transcendental function applications that are "master terms",
+ * see d_trMaster/d_trSlave.
+ */
+ std::map<Node, std::vector<Node> > d_funcCongClass;
+ /**
+ * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI }
+ * that are representives of their congruence class.
+ */
+ std::map<Kind, std::vector<Node> > d_funcMap;
// factor skolems
std::map< Node, Node > d_factor_skolem;
* on the model value of its argument.
*/
std::pair<Node, Node> getTfModelBounds(Node tf, unsigned d);
- /** is refinable transcendental function
- *
- * A transcendental function application is not refineable if its current
- * model value is zero, or if it is an application of SINE applied
- * to a non-variable.
- */
- bool isRefineableTfFun(Node tf);
/** get approximate sqrt
*
* This approximates the square root of positive constant c. If this method
std::map<Node, NlLemmaSideEffect>& lemSE);
/** check transcendental function refinement for tf
*
- * This method is called by the above method for each refineable
- * transcendental function (see isRefineableTfFun) that occurs in an
- * assertion in the current context.
+ * This method is called by the above method for each "master"
+ * transcendental function application that occurs in an assertion in the
+ * current context. For example, an application like sin(t) is not a master
+ * if we have introduced the constraints:
+ * t=y+2*pi*n ^ -pi <= y <= pi ^ sin(t) = sin(y).
+ * See d_trMaster/d_trSlaves for more detail.
*
* This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental
* function application tf for Taylor degree d. It may add a secant or
* tangent plane lemma to lems and its side effect (if one exists)
* to lemSE.
+ *
+ * It returns false if the bounds are not precise enough to add a
+ * secant or tangent plane lemma.
*/
bool checkTfTangentPlanesFun(Node tf,
unsigned d,
projects / cvc5.git / commitdiff