From 70391b799bf75f3410844eef1cc8029d5f3c9e6e Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 30 Mar 2022 14:17:09 -0500 Subject: [PATCH] Fix policy for purifying arguments of exp (#8416) 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. --- src/proof/proof_rule.h | 6 +++--- src/theory/arith/nl/ext/monomial_check.cpp | 10 +++++++--- .../nl/transcendental/exponential_solver.cpp | 4 +--- .../arith/nl/transcendental/proof_checker.cpp | 17 +++++++++++------ .../nl/transcendental/transcendental_solver.cpp | 1 + .../nl/transcendental/transcendental_state.cpp | 4 +++- src/theory/theory_model_builder.cpp | 7 +++++-- test/regress/cli/CMakeLists.txt | 1 + .../regress0/nl/nta/issue8415-embed-arg.smt2 | 6 ++++++ 9 files changed, 38 insertions(+), 18 deletions(-) create mode 100644 test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2 diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h index 6231806d3..e44802edd 100644 --- a/src/proof/proof_rule.h +++ b/src/proof/proof_rule.h @@ -1734,12 +1734,12 @@ enum class PfRule : uint32_t * **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:: diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp index adcd084dd..2f20435f4 100644 --- a/src/theory/arith/nl/ext/monomial_check.cpp +++ b/src/theory/arith/nl/ext/monomial_check.cpp @@ -109,11 +109,14 @@ void MonomialCheck::checkMagnitude(unsigned c) // 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); } @@ -454,7 +457,8 @@ bool MonomialCheck::compareMonomial( 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; @@ -664,7 +668,7 @@ void MonomialCheck::assignOrderIds(std::vector& vars, 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) diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index b869f2e72..93786f646 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -219,8 +219,6 @@ void ExponentialSolver::doTangentLemma(TNode e, 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; @@ -230,7 +228,7 @@ void ExponentialSolver::doTangentLemma(TNode e, 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); diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index d7b990db3..69854ef09 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -192,19 +192,24 @@ Node TranscendentalProofRuleChecker::checkInternal( 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().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{nm->mkNode(Kind::EXPONENTIAL, t), evalt}); + Kind::IMPLIES, + nm->mkNode(Kind::GEQ, t, c), + nm->mkNode(Kind::GEQ, + std::vector{nm->mkNode(Kind::EXPONENTIAL, t), evalt})); } else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS) { diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 0d5a75b86..e0e1fc50f 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -265,6 +265,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) // Figure 3 : c Node c = d_tstate.d_model.computeAbstractModelValue(tf[0]); + Assert(c.isConst()); int csign = c.getConst().sgn(); if (csign == 0) { diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index dc5d2a495..8b117b870 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -102,9 +102,11 @@ void TranscendentalState::init(const std::vector& xts, } 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; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 942374a47..2119054a2 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -527,8 +527,11 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) } 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; diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 47d070413..a4179b203 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -816,6 +816,7 @@ set(regress_0_tests 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 diff --git a/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2 b/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2 new file mode 100644 index 000000000..1be656f19 --- /dev/null +++ b/test/regress/cli/regress0/nl/nta/issue8415-embed-arg.smt2 @@ -0,0 +1,6 @@ +(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) -- 2.30.2