From f356ac03da7d908903db3e1328e3390b02fc3aac Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 28 Feb 2022 14:01:30 -0600 Subject: [PATCH] Add two reduction schemas for sin terms (#8171) This restores our reasoning for symmetry of sine, now on-demand and without introducing sin terms eagerly. It also ensures that sin terms whose arguments fall exactly on boundary points are removed from consideration from the transcendental solver. This allows us to answer sat for inputs involving sin(k) when k = pi/2. It also cleans the relationship of sine solver and transcendental state, and makes a small fix to the monotonicity of sin schema. --- .../arith/nl/transcendental/sine_solver.cpp | 152 ++++++++++++++---- .../arith/nl/transcendental/sine_solver.h | 47 ++++-- .../transcendental/transcendental_solver.cpp | 31 ++-- .../transcendental/transcendental_state.cpp | 33 +++- .../nl/transcendental/transcendental_state.h | 10 +- src/theory/inference_id.cpp | 3 + src/theory/inference_id.h | 4 + test/regress/CMakeLists.txt | 1 + .../regress0/nl/nta/sin-sym-schema.smt2 | 10 ++ .../nl/issue7948-3-unsound-sin-region.smt2 | 7 +- 10 files changed, 215 insertions(+), 83 deletions(-) create mode 100644 test/regress/regress0/nl/nta/sin-sym-schema.smt2 diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp index 21bbd4feb..245665d68 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.cpp +++ b/src/theory/arith/nl/transcendental/sine_solver.cpp @@ -54,32 +54,131 @@ inline Node mkValidPhase(TNode a, TNode pi) SineSolver::SineSolver(Env& env, TranscendentalState* tstate) : EnvObj(env), d_data(tstate) { + NodeManager* nm = NodeManager::currentNM(); + Node zero = nm->mkConstReal(Rational(0)); + Node one = nm->mkConstReal(Rational(1)); + Node negOne = nm->mkConstReal(Rational(-1)); + d_pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); + Node pi_2 = rewrite( + nm->mkNode(Kind::MULT, d_pi, nm->mkConstReal(Rational(1) / Rational(2)))); + Node pi_neg_2 = rewrite(nm->mkNode( + Kind::MULT, d_pi, nm->mkConstReal(Rational(-1) / Rational(2)))); + d_neg_pi = rewrite(nm->mkNode(Kind::MULT, d_pi, negOne)); + d_mpoints.push_back(d_pi); + d_mpointsSine[d_pi] = zero; + d_mpoints.push_back(pi_2); + d_mpointsSine[pi_2] = one; + d_mpoints.push_back(zero); + d_mpointsSine[zero] = zero; + d_mpoints.push_back(pi_neg_2); + d_mpointsSine[pi_neg_2] = negOne; + d_mpoints.push_back(d_neg_pi); + d_mpointsSine[d_neg_pi] = zero; } SineSolver::~SineSolver() {} +void SineSolver::doReductions() +{ + NodeManager* nm = NodeManager::currentNM(); + std::map >::iterator it = + d_data->d_funcMap.find(kind::SINE); + if (it == d_data->d_funcMap.end()) + { + return; + } + std::map mpvs; + for (std::pair& m : d_mpointsSine) + { + Node mv = d_data->d_model.computeAbstractModelValue(m.first); + mpvs[mv] = m.first; + } + std::map valForSym; + std::vector nreduced; + for (const Node& tf : it->second) + { + Node mva = d_data->d_model.computeAbstractModelValue(tf[0]); + Node mv = d_data->d_model.computeAbstractModelValue(tf); + Node mvaNeg = nm->mkConstReal(-mva.getConst()); + std::map::iterator itv = valForSym.find(mvaNeg); + bool reduced = false; + if (itv != valForSym.end()) + { + Node mvs = d_data->d_model.computeAbstractModelValue(itv->second); + if (mvs.getConst() != -mv.getConst()) + { + Node lem = + nm->mkNode(kind::IMPLIES, + tf[0].eqNode(nm->mkNode(kind::NEG, itv->second[0])), + tf.eqNode(nm->mkNode(kind::NEG, itv->second))); + d_data->d_im.addPendingLemma( + lem, InferenceId::ARITH_NL_T_SINE_SYMM, nullptr); + } + // we do not consider it reduced currently, since we require setting + // approximate bounds for it, alternatively we could carry the negation + // of the approximation in the transcendental solver + } + else + { + valForSym[mva] = tf; + itv = mpvs.find(mva); + if (itv != mpvs.end()) + { + Assert(d_mpointsSine.find(itv->second) != d_mpointsSine.end()); + Node mvs = d_mpointsSine[itv->second]; + if (mv != mvs) + { + // the argument is a boundary point, we reduce it if not already done + // so + Node lem = nm->mkNode( + kind::IMPLIES, tf[0].eqNode(itv->second), tf.eqNode(mvs)); + d_data->d_im.addPendingLemma( + lem, InferenceId::ARITH_NL_T_SINE_BOUNDARY_REDUCE, nullptr); + } + else + { + // remember that the argument is equal to the boundary point + d_data->d_model.addSubstitution(tf[0], itv->second); + // all congruent transcendental functions are exactly equal to its + // value + d_data->addModelBoundForPurifyTerm(tf, mvs, mvs); + } + reduced = true; + break; + } + } + if (!reduced) + { + nreduced.push_back(tf); + } + } + if (nreduced.size() < it->second.size()) + { + it->second = nreduced; + } +} + void SineSolver::doPhaseShift(TNode a, TNode new_a, TNode y) { NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); 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 = sm->mkDummySkolem("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::ADD, - y, - nm->mkNode(Kind::MULT, - nm->mkConstReal(Rational(2)), - shift, - d_data->d_pi)))), + mkValidPhase(y, d_pi), + nm->mkNode( + Kind::ITE, + mkValidPhase(a[0], d_pi), + a[0].eqNode(y), + a[0].eqNode(nm->mkNode( + Kind::ADD, + y, + nm->mkNode( + Kind::MULT, nm->mkConstReal(Rational(2)), shift, d_pi)))), new_a.eqNode(a)); CDProof* proof = nullptr; if (d_data->isProofEnabled()) @@ -156,15 +255,13 @@ void SineSolver::checkInitialRefine() 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::SUB, d_data->d_pi_neg, t[0]))), + nm->mkNode(Kind::GT, t[0], d_neg_pi), + nm->mkNode( + Kind::GT, t, nm->mkNode(Kind::SUB, d_neg_pi, t[0]))), nm->mkNode( Kind::IMPLIES, - nm->mkNode(Kind::LT, t[0], d_data->d_pi), - nm->mkNode( - Kind::LT, t, nm->mkNode(Kind::SUB, d_data->d_pi, t[0])))); + nm->mkNode(Kind::LT, t[0], d_pi), + nm->mkNode(Kind::LT, t, nm->mkNode(Kind::SUB, d_pi, t[0])))); CDProof* proof = nullptr; if (d_data->isProofEnabled()) { @@ -231,18 +328,13 @@ void SineSolver::checkMonotonic() sortByNlModel( tf_args.begin(), tf_args.end(), &d_data->d_model, true, false, true); - std::vector mpoints = {d_data->d_pi, - d_data->d_pi_2, - d_data->d_zero, - d_data->d_pi_neg_2, - d_data->d_pi_neg}; // 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; + TNode tpi = d_pi; for (size_t j = 0; j < 5; j++) { - Node point = mpoints[j]; + Node point = d_mpoints[j]; for (size_t i = 0; i < 2; i++) { Node mpointapprox = point; @@ -279,7 +371,7 @@ void SineSolver::checkMonotonic() // increment to the proper monotonicity region bool increment = true; - while (increment && mdir_index < mpoints.size()) + while (increment && mdir_index < d_mpoints.size()) { increment = false; // if we are less than the upper bound of the next point @@ -295,12 +387,12 @@ void SineSolver::checkMonotonic() if (increment) { tval = Node::null(); - mono_bounds[1] = mpoints[mdir_index]; + mono_bounds[1] = d_mpoints[mdir_index]; mdir_index++; monotonic_dir = regionToMonotonicityDir(mdir_index); - if (mdir_index < mpoints.size()) + if (mdir_index < d_mpoints.size()) { - mono_bounds[0] = mpoints[mdir_index]; + mono_bounds[0] = d_mpoints[mdir_index]; } else { @@ -313,6 +405,8 @@ void SineSolver::checkMonotonic() if (mdir_index > 0 && sargvalr > mpointsBound[0][mdir_index - 1].getConst()) { + // can't take this value into account for monotonicity + tval = Node::null(); d_data->d_tf_region[s] = -1; Trace("nl-ext-concavity") << "Cannot determine the region of transcendental function " << s diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h index 96bfa6009..88ca1b71e 100644 --- a/src/theory/arith/nl/transcendental/sine_solver.h +++ b/src/theory/arith/nl/transcendental/sine_solver.h @@ -46,6 +46,18 @@ class SineSolver : protected EnvObj SineSolver(Env& env, TranscendentalState* tstate); ~SineSolver(); + /** do reductions + * + * This method determines any applications of sin(x) that can be reasoned + * about "precisely", either via symmetry: + * x = -y => sin(x) = -sin(y) + * or via boundary points, e.g.: + * x = pi/2 => sin(x) = 1 + * Each application of sin(x) for which a reduction of the latter form exists + * is removed from the range of d_funcMap in the transcendental state, and + * thus will not be considered for other lemma schemas. + */ + void doReductions(); /** * 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. @@ -110,16 +122,14 @@ class SineSolver : protected EnvObj * is invalid, or there is no lower bound for the * region. */ - Node regionToLowerBound(int region) + Node regionToLowerBound(int region) const { - switch (region) + if (region >= 1 && region <= 4) { - case 1: return d_data->d_pi_2; - case 2: return d_data->d_zero; - case 3: return d_data->d_pi_neg_2; - case 4: return d_data->d_pi_neg; - default: return Node(); + size_t index = static_cast(region); + return d_mpoints[index]; } + return Node(); } /** region to upper bound @@ -130,19 +140,17 @@ class SineSolver : protected EnvObj * is invalid, or there is no upper bound for the * region. */ - Node regionToUpperBound(int region) + Node regionToUpperBound(int region) const { - switch (region) + if (region >= 1 && region <= 4) { - case 1: return d_data->d_pi; - case 2: return d_data->d_pi_2; - case 3: return d_data->d_zero; - case 4: return d_data->d_pi_neg_2; - default: return Node(); + size_t index = static_cast(region - 1); + return d_mpoints[index]; } + return Node(); } - int regionToMonotonicityDir(int region) + int regionToMonotonicityDir(int region) const { switch (region) { @@ -153,7 +161,7 @@ class SineSolver : protected EnvObj default: return 0; } } - Convexity regionToConvexity(int region) + Convexity regionToConvexity(int region) const { switch (region) { @@ -171,6 +179,13 @@ class SineSolver : protected EnvObj /** The transcendental functions we have done initial refinements on */ std::map d_tf_initial_refine; + /** PI, -PI */ + Node d_pi; + Node d_neg_pi; + /** the boundary points */ + std::vector d_mpoints; + /** mapping from values c to known points for sin(c) */ + std::map d_mpointsSine; }; /* class SineSolver */ } // namespace transcendental diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 7db06008f..ac94be864 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -58,6 +58,14 @@ void TranscendentalSolver::initLastCall(const std::vector& xts) std::vector needsMaster; d_tstate.init(xts, needsMaster); + if (d_tstate.d_im.hasUsed()) + { + return; + } + + // apply reduction reasoning, e.g. x = pi/2 => sin(x) = 1 + d_sineSlv.doReductions(); + if (d_tstate.d_im.hasUsed()) { return; } @@ -140,27 +148,8 @@ bool TranscendentalSolver::preprocessAssertionsCheckModel( } if (!bounds.first.isNull() && !bounds.second.isNull()) { - // for each function in the congruence classe - for (const Node& ctf : d_tstate.d_funcCongClass[tf]) - { - std::vector mset{ctf}; - // if this purifies another term, we set a bound on the term it - // purifies as well - context::CDHashMap::const_iterator itp = - d_tstate.d_trPurifies.find(ctf); - if (itp != d_tstate.d_trPurifies.end() && itp->second != ctf) - { - mset.push_back(itp->second); - } - for (const Node& stf : mset) - { - Trace("nl-ext-cm") - << "...bound for " << stf << " : [" << bounds.first << ", " - << bounds.second << "]" << std::endl; - success = - d_tstate.d_model.addBound(stf, bounds.first, bounds.second); - } - } + success = d_tstate.addModelBoundForPurifyTerm( + tf, bounds.first, bounds.second); } else { diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 45d2b81bb..c33ed5ef1 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -214,12 +214,6 @@ void TranscendentalState::mkPi() if (d_pi.isNull()) { d_pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); - d_pi_2 = rewrite(nm->mkNode( - Kind::MULT, d_pi, nm->mkConstReal(Rational(1) / Rational(2)))); - d_pi_neg_2 = rewrite(nm->mkNode( - Kind::MULT, d_pi, nm->mkConstReal(Rational(-1) / Rational(2)))); - d_pi_neg = - rewrite(nm->mkNode(Kind::MULT, d_pi, nm->mkConstReal(Rational(-1)))); // initialize bounds d_pi_bound[0] = nm->mkConstReal(Rational(103993) / Rational(33102)); d_pi_bound[1] = nm->mkConstReal(Rational(104348) / Rational(33215)); @@ -460,6 +454,33 @@ bool TranscendentalState::isPurified(TNode n) const return d_trPurifies.find(n) != d_trPurifies.end(); } +bool TranscendentalState::addModelBoundForPurifyTerm(TNode n, TNode l, TNode u) +{ + Assert(d_funcCongClass.find(n) != d_funcCongClass.end()); + // for each function in the congruence classe + for (const Node& ctf : d_funcCongClass[n]) + { + std::vector mset{ctf}; + // if this purifies another term, we set a bound on the term it + // purifies as well + context::CDHashMap::const_iterator itp = d_trPurifies.find(ctf); + if (itp != d_trPurifies.end() && itp->second != ctf) + { + mset.push_back(itp->second); + } + for (const Node& stf : mset) + { + Trace("nl-ext-cm") << "...bound for " << stf << " : [" << l << ", " << u + << "]" << std::endl; + if (!d_model.addBound(stf, l, u)) + { + return false; + } + } + } + return true; +} + } // namespace transcendental } // namespace nl } // namespace arith diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 292656e4e..31f7731af 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -167,6 +167,10 @@ class TranscendentalState : protected EnvObj * Is term t purified? (See d_trPurify below). */ bool isPurified(TNode n) const; + /** + * Add bound for n, and for what (if anything) it purifies + */ + bool addModelBoundForPurifyTerm(TNode n, TNode l, TNode u); Node d_true; Node d_false; @@ -267,12 +271,6 @@ class TranscendentalState : protected EnvObj * concrete lower and upper bounds stored in d_pi_bound below. */ Node d_pi; - /** PI/2 */ - Node d_pi_2; - /** -PI/2 */ - Node d_pi_neg_2; - /** -PI */ - Node d_pi_neg; /** the concrete lower and upper bounds for PI */ Node d_pi_bound[2]; }; diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 745f6d35b..b0d218e81 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -75,6 +75,9 @@ const char* toString(InferenceId i) case InferenceId::ARITH_NL_RES_INFER_BOUNDS: return "ARITH_NL_RES_INFER_BOUNDS"; case InferenceId::ARITH_NL_TANGENT_PLANE: return "ARITH_NL_TANGENT_PLANE"; + case InferenceId::ARITH_NL_T_SINE_SYMM: return "ARITH_NL_T_SINE_SYMM"; + case InferenceId::ARITH_NL_T_SINE_BOUNDARY_REDUCE: + return "ARITH_NL_T_SINE_BOUNDARY_REDUCE"; case InferenceId::ARITH_NL_T_PURIFY_ARG: return "ARITH_NL_T_PURIFY_ARG"; case InferenceId::ARITH_NL_T_INIT_REFINE: return "ARITH_NL_T_INIT_REFINE"; case InferenceId::ARITH_NL_T_PI_BOUND: return "ARITH_NL_T_PI_BOUND"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index ef63c224c..a34b40661 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -124,6 +124,10 @@ enum class InferenceId // tangent planes (NlSolver::checkTangentPlanes) ARITH_NL_TANGENT_PLANE, //-------------------- nonlinear transcendental solver + // sine symmetry + ARITH_NL_T_SINE_SYMM, + // boundary reduction + ARITH_NL_T_SINE_BOUNDARY_REDUCE, // purification of arguments to transcendental functions ARITH_NL_T_PURIFY_ARG, // initial refinement (TranscendentalSolver::checkTranscendentalInitialRefine) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 35fec0387..083edd4ec 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -795,6 +795,7 @@ set(regress_0_tests regress0/nl/nta/proj-issue460-pi-value.smt2 regress0/nl/nta/real-pi.smt2 regress0/nl/nta/sin-sym.smt2 + regress0/nl/nta/sin-sym-schema.smt2 regress0/nl/nta/sqrt-simple.smt2 regress0/nl/nta/tan-rewrite.smt2 regress0/nl/pow2-native-0.smt2 diff --git a/test/regress/regress0/nl/nta/sin-sym-schema.smt2 b/test/regress/regress0/nl/nta/sin-sym-schema.smt2 new file mode 100644 index 000000000..dd76b727b --- /dev/null +++ b/test/regress/regress0/nl/nta/sin-sym-schema.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () Real) +(declare-fun b () Real) +(declare-fun c () Real) +(assert (<= 0.0 a 2.0)) +(assert (or (= (+ a c) 0.0) (= (+ a b) 0.0))) +(assert (not (= (sin a) (- (sin b))))) +(assert (not (= (sin a) (- (sin c))))) +(check-sat) diff --git a/test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 b/test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 index fee1781ef..a27a5db73 100644 --- a/test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 +++ b/test/regress/regress1/nl/issue7948-3-unsound-sin-region.smt2 @@ -1,10 +1,7 @@ -; COMMAND-LINE: --simplification=none --tlimit=100 -; EXPECT-ERROR: cvc5 interrupted by timeout. -; EXIT: -6 +; COMMAND-LINE: --simplification=none -q +; EXPECT: sat (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) -- 2.30.2