This corrects the policy for when to purify exp. It ensures we purify exp whenever the kind is not a variable or constant, instead of when the kind is a transcendental function app. The latter permits problematic terms like (exp (* (exp 1.0) (exp 1.0)).
This also corrects an issue where information for ordering on variables would be skipped if we failed to produce a model value for a single variable, which was the original source of the error on #8415.
It furthermore fixes the PfRule ARITH_TRANS_EXP_APPROX_BELOW, which did not handle non-constant arguments of exp.
Fixes #8415.
* **Arithmetic -- Transcendentals -- Exp is approximated from below**
*
* .. math::
- * \inferrule{- \mid d,t}{exp(t) \geq \texttt{maclaurin}(\exp, d, t)}
+ * \inferrule{- \mid d,c,t}{t \geq c \rightarrow exp(t) \geq \texttt{maclaurin}(\exp, d, c)}
*
* where :math:`d` is an odd positive number, :math:`t` an arithmetic term and
- * :math:`\texttt{maclaurin}(\exp, d, t)` is the :math:`d`'th taylor
+ * :math:`\texttt{maclaurin}(\exp, d, c)` is the :math:`d`'th taylor
* polynomial at zero (also called the Maclaurin series) of the exponential
- * function evaluated at :math:`t`. The Maclaurin series for the exponential
+ * function evaluated at :math:`c`. The Maclaurin series for the exponential
* function is the following:
*
* .. math::
// ensure information is setup
if (c == 0)
{
+ Trace("nl-ext-proc") << "Assign order ids for " << d_data->d_ms_vars
+ << "..." << std::endl;
// sort by absolute values of abstract model values
assignOrderIds(d_data->d_ms_vars, d_order_vars, false, true);
// sort individual variable lists
- Trace("nl-ext-proc") << "Assign order var lists..." << std::endl;
+ Trace("nl-ext-proc") << "Assign order var lists for " << d_data->d_ms
+ << "..." << std::endl;
d_data->d_mdb.sortVariablesByModel(d_data->d_ms, d_data->d_model);
}
lem,
cmp_infers);
}
- Assert(d_order_vars.find(av) != d_order_vars.end());
+ Assert(d_order_vars.find(av) != d_order_vars.end())
+ << "Missing order information for variable " << av;
avo = d_order_vars[av];
}
Node bv;
Trace("nl-ext-mvo") << "..do not assign order to " << x << " : " << v
<< std::endl;
// don't assign for non-constant values (transcendental function apps)
- break;
+ continue;
}
Trace("nl-ext-mvo") << " order " << x << " : " << v << std::endl;
if (v != prev)
nm->mkNode(Kind::GEQ, e, poly_approx));
Trace("nl-ext-exp") << "*** Tangent plane lemma (pre-rewrite): " << lem
<< std::endl;
- lem = rewrite(lem);
- Trace("nl-ext-exp") << "*** Tangent plane lemma : " << lem << std::endl;
Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false);
// Figure 3 : line 9
CDProof* proof = nullptr;
proof->addStep(lem,
PfRule::ARITH_TRANS_EXP_APPROX_BELOW,
{},
- {nm->mkConstInt(Rational(d)), e[0]});
+ {nm->mkConstInt(Rational(d)), c, e[0]});
}
d_data->d_im.addPendingLemma(
lem, InferenceId::ARITH_NL_T_TANGENT, proof, true);
else if (id == PfRule::ARITH_TRANS_EXP_APPROX_BELOW)
{
Assert(children.empty());
- Assert(args.size() == 2);
+ Assert(args.size() == 3);
Assert(args[0].isConst() && args[0].getType().isInteger());
- Assert(args[1].getType().isReal());
+ Assert(args[1].isConst() && args[1].getType().isRealOrInt());
+ Assert(args[2].getType().isReal());
std::uint64_t d =
args[0].getConst<Rational>().getNumerator().toUnsignedInt();
- Node t = args[1];
+ Node c = args[1];
+ Node t = args[2];
TaylorGenerator tg;
TaylorGenerator::ApproximationBounds bounds;
- tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d, bounds);
+ tg.getPolynomialApproximationBoundForArg(Kind::EXPONENTIAL, c, d, bounds);
Evaluator eval(nullptr);
- Node evalt = eval.eval(bounds.d_lower, {tg.getTaylorVariable()}, {t});
+ Node evalt = eval.eval(bounds.d_lower, {tg.getTaylorVariable()}, {c});
return nm->mkNode(
- Kind::GEQ, std::vector<Node>{nm->mkNode(Kind::EXPONENTIAL, t), evalt});
+ Kind::IMPLIES,
+ nm->mkNode(Kind::GEQ, t, c),
+ nm->mkNode(Kind::GEQ,
+ std::vector<Node>{nm->mkNode(Kind::EXPONENTIAL, t), evalt}));
}
else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS)
{
// Figure 3 : c
Node c = d_tstate.d_model.computeAbstractModelValue(tf[0]);
+ Assert(c.isConst());
int csign = c.getConst<Rational>().sgn();
if (csign == 0)
{
}
else
{
+ // for others, if all arguments are variables or constants, we don't
+ // have to purify
for (const Node& ac : a)
{
- if (isTranscendentalKind(ac.getKind()))
+ if (!ac.isVar() && !ac.isConst())
{
consider = false;
break;
}
else
{
- warning() << "Model values in the same equivalence class "
- << constRep << " " << n << std::endl;
+ // This is currently a trace message, as it often triggers for
+ // non-linear arithmetic before the model is refined enough to
+ // e.g. show transcendental function apps are not equal to rationals
+ Trace("model-warn") << "Model values in the same equivalence class "
+ << constRep << " " << n << std::endl;
if (!constRepBaseModelValue)
{
assignConstRep = isBaseValue;
regress0/nl/nta/issue8183-tc-pi.smt2
regress0/nl/nta/issue8208-red-nred.smt2
regress0/nl/nta/issue8294-2-double-solve.smt2
+ regress0/nl/nta/issue8415-embed-arg.smt2
regress0/nl/nta/proj-issue376.smt2
regress0/nl/nta/proj-issue403.smt2
regress0/nl/nta/proj-issue460-pi-value.smt2
--- /dev/null
+(set-logic ALL)
+(set-info :status unsat)
+(declare-fun r8 () Real)
+(declare-fun v57 () Bool)
+(assert (and (= 0.0 (exp (exp (+ 1.0 1.0)))) (not (= 0 (* r8 (ite v57 1 0))))))
+(check-sat)
projects / cvc5.git / commitdiff