From: Andrew Reynolds Date: Thu, 24 Feb 2022 19:08:07 +0000 (-0600) Subject: Make sine solver sound with respect to region boundaries (#8117) X-Git-Tag: cvc5-1.0.0~386 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4bba39f1b52210c7a31b8e7542df9dc15b9700c1;p=cvc5.git Make sine solver sound with respect to region boundaries (#8117) Fixes the last benchmark on #7948. Fixes a refutation soundness issue in the transcendental solver where a concavity region would be incorrectly assigned to a point if it was between the current model value of c*PI and its true value, where c in {-1, -1/2, 1/2, 1}. We now only assign a concavity region if the model value of the argument lies within sound lower/upper bounds for the boundaries. Notice that this means that points may be unassignable to a region if they lie inside the approximation interval for c*PI. An application of sin applied to an argument whose model value is that point cannot be refined. A followup PR will address termination issues where the Taylor degree is incremented even when no function can be refined. --- diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 926894a49..3299a0586 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -244,13 +244,32 @@ void SineSolver::checkMonotonic() d_data->d_zero, d_data->d_pi_neg_2, d_data->d_pi_neg}; - std::vector mpoints_vals; - - // get model values for points - for (const auto& point : mpoints) + // Sound lower (index=0), upper (index=1) bounds for the above points. We + // compute this by plugging in the upper and lower bound of pi. + std::vector mpointsBound[2]; + TNode tpi = d_data->d_pi; + for (size_t j = 0; j < 5; j++) { - mpoints_vals.emplace_back(d_data->d_model.computeAbstractModelValue(point)); - Assert(mpoints_vals.back().isConst()); + Node point = mpoints[j]; + for (size_t i = 0; i < 2; i++) + { + Node mpointapprox = point; + if (j != 2) + { + // substitute the lower or upper bound of pi + TNode tb = d_data->d_pi_bound[i]; + mpointapprox = point.substitute(tpi, tb); + mpointapprox = d_data->d_model.computeConcreteModelValue(mpointapprox); + } + Assert(mpointapprox.isConst()); + mpointsBound[i].emplace_back(mpointapprox); + } + // bounds are flipped for negative pi + if (mpointsBound[0].back().getConst() + > mpointsBound[1].back().getConst()) + { + std::swap(mpointsBound[0].back(), mpointsBound[1].back()); + } } unsigned mdir_index = 0; @@ -261,6 +280,7 @@ void SineSolver::checkMonotonic() { Node sargval = d_data->d_model.computeAbstractModelValue(sarg); Assert(sargval.isConst()); + const Rational& sargvalr = sargval.getConst(); Node s = tf_arg_to_term[sarg]; Node sval = d_data->d_model.computeAbstractModelValue(s); Assert(sval.isConst()); @@ -270,14 +290,15 @@ void SineSolver::checkMonotonic() while (increment && mdir_index < mpoints.size()) { increment = false; - Node pval = mpoints_vals[mdir_index]; - Assert(pval.isConst()); - if (sargval.getConst() < pval.getConst()) + // if we are less than the upper bound of the next point + Node pvalUpper = mpointsBound[1][mdir_index]; + Assert(pvalUpper.isConst()); + if (sargvalr < pvalUpper.getConst()) { increment = true; Trace("nl-ext-tf-mono") << "...increment at " << sarg << " since model value is less than " - << mpoints[mdir_index] << std::endl; + << mpointsBound[1][mdir_index] << std::endl; } if (increment) { @@ -295,10 +316,24 @@ void SineSolver::checkMonotonic() } } } - // store the concavity region - d_data->d_tf_region[s] = mdir_index; - Trace("nl-ext-concavity") - << "Transcendental function " << s << " is in region #" << mdir_index; + // must ensure that we are actually less than or equal to the lower bound of + // the previous point + if (mdir_index > 0 + && sargvalr > mpointsBound[0][mdir_index - 1].getConst()) + { + d_data->d_tf_region[s] = -1; + Trace("nl-ext-concavity") + << "Cannot determine the region of transcendental function " << s + << ", perhaps its value is close to the boundary " + << mpointsBound[1][mdir_index - 1]; + } + else + { + // store the concavity region + d_data->d_tf_region[s] = mdir_index; + Trace("nl-ext-concavity") + << "Transcendental function " << s << " is in region #" << mdir_index; + } Trace("nl-ext-concavity") << ", arg model value = " << sargval << std::endl; if (!tval.isNull()) @@ -350,7 +385,9 @@ void SineSolver::doTangentLemma( TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d) { NodeManager* nm = NodeManager::currentNM(); + Assert(region != -1); + Trace("nl-ext-sine") << c << " in region " << region << std::endl; // compute tangent plane // Figure 3: T( x ) // We use zero slope tangent planes, since the concavity of the Taylor @@ -440,6 +477,7 @@ void SineSolver::doSecantLemmas(TNode e, unsigned actual_d, int region) { + Assert(region != -1); d_data->doSecantLemmas(getSecantBounds(e, c, d, region), poly_approx, c, diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 1448bdbd2..6a254fc54 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -307,6 +307,11 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) region = itr->second; Trace("nl-ext-tftp-debug") << " region is : " << region << std::endl; } + if (region == -1) + { + // the region cannot be assigned, return false without lemma + return false; + } // Figure 3 : conc int concavity = regionToConcavity(k, itr->second); Trace("nl-ext-tftp-debug") << " concavity is : " << concavity << std::endl; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b89f1da47..5f299152f 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1906,6 +1906,7 @@ set(regress_1_tests regress1/nl/issue5662-nl-tc.smt2 regress1/nl/issue5662-nl-tc-min.smt2 regress1/nl/issue7924-sqrt-partial.smt2 + regress1/nl/issue7948-3-unsound-sin-region.smt2 regress1/nl/issue8016-iand-rewrite.smt2 regress1/nl/issue8052-iand-rewrite.smt2 regress1/nl/issue8118-elim-sin.smt2 diff --git a/test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 b/test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 new file mode 100644 index 000000000..fee1781ef --- /dev/null +++ b/test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --simplification=none --tlimit=100 +; EXPECT-ERROR: cvc5 interrupted by timeout. +; EXIT: -6 +(set-logic ALL) +(declare-fun a () Real) +(declare-fun b () Real) +(assert (and (= a 0) (= b (cos a)))) + +; currently this cannot be solved due to limitations on how arguments to sin are processed +(check-sat)