From: Andrew Reynolds Date: Mon, 9 Mar 2020 14:33:14 +0000 (-0500) Subject: Fixes for bounds on transcendental functions (#3832) X-Git-Tag: cvc5-1.0.0~3549 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=31e30d52a3fc6ac2a2a2f5e8d4a17a4ca954d8e8;p=cvc5.git Fixes for bounds on transcendental functions (#3832) This PR refactors and fixes how bounds are set for transcendental functions. The new code ensures that all transcendental function applications are given bounds. (Our previous failures to do so were hindering our ability to say "sat", due to NlModel::checkModel failures). There were previously two issues on why transcendental function applications were not being assigned bounds: "Slave" transcendental functions (e.g. those that we reduce via sin(t) = sin(y) ^ -pi <= y <= pi ^ y + 2*pi*N = t) were not being given bounds explicitly, Transcendental functions that are congruent to others (e.g. f(x) where f(y) exists and x=y in the current context) were being ignored and hence not bound. This PR clarifies the master/slave relationship that tracks which transcendental function applications have been purified, and furthermore tracks congruence classes. The setting of bounds and the check-model is further simplified by setting bounds on the original terms, whereas the current code sets bounds on the model values of terms. In other words, previously if we had term sin(y) and y^M = c, then we'd set bounds for sin(c), whereas the new code sets the bound on sin(y) directly. Fixes #3783. We answer unknown without an assertion failure on that benchmark now. Further work based on ignoring literals from internally generated lemmas is necessary for solving it sat. --- diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp index 65aaceb80..cbb27197f 100644 --- a/src/theory/arith/arith_utilities.cpp +++ b/src/theory/arith/arith_utilities.cpp @@ -224,10 +224,13 @@ Node arithSubstitute(Node n, std::vector& vars, std::vector& subs) else { TheoryId ctid = theory::kindToTheoryId(ck); - if (ctid != THEORY_ARITH && ctid != THEORY_BOOL - && ctid != THEORY_BUILTIN) + if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL + && ctid != THEORY_BUILTIN) + || isTranscendentalKind(ck)) { - // do not traverse beneath applications that belong to another theory + // Do not traverse beneath applications that belong to another theory + // besides (core) arithmetic. Notice that transcendental function + // applications are also not traversed here. visited[cur] = cur; } else diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index d09a138fe..904300004 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -1208,31 +1208,6 @@ bool NlModel::simpleCheckModelMsum(const std::map& msum, bool pol) return comp == d_true; } -bool NlModel::isRefineableTfFun(Node tf) -{ - Assert(tf.getKind() == SINE || tf.getKind() == EXPONENTIAL); - if (tf.getKind() == SINE) - { - // we do not consider e.g. sin( -1*x ), since considering sin( x ) will - // have the same effect. We also do not consider sin(x+y) since this is - // handled by introducing a fresh variable (see the map d_tr_base in - // NonlinearExtension). - if (!tf[0].isVar()) - { - return false; - } - } - // Figure 3 : c - Node c = computeAbstractModelValue(tf[0]); - Assert(c.isConst()); - int csign = c.getConst().sgn(); - if (csign == 0) - { - return false; - } - return true; -} - bool NlModel::getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter) const { Assert(c.isConst()); diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h index a8746ca2e..5129a7a32 100644 --- a/src/theory/arith/nl_model.h +++ b/src/theory/arith/nl_model.h @@ -256,15 +256,6 @@ class NlModel bool simpleCheckModelLit(Node lit); bool simpleCheckModelMsum(const std::map& msum, bool pol); //---------------------------end check model - - /** 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 diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index cd9352b3a..af384be49 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -781,7 +781,7 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; std::vector pvars; std::vector psubs; - for (std::pair& tb : d_tr_base) + for (std::pair& tb : d_trMaster) { pvars.push_back(tb.first); psubs.push_back(tb.second); @@ -804,18 +804,16 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, } // get model bounds for all transcendental functions - Trace("nl-ext-cm-debug") << " get bounds for transcendental functions..." - << std::endl; - for (std::pair >& tfs : d_f_map) + Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..." + << std::endl; + for (std::pair >& 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) @@ -823,41 +821,46 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, bl = d_pi_bound[0]; bu = d_pi_bound[1]; } - else if (d_model.isRefineableTfFun(tf)) + else { - d_model.setUsedApproximate(); std::pair 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; @@ -923,7 +926,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, 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 lemmas; @@ -932,7 +936,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, Trace("nl-ext-mv") << "Extended terms : " << std::endl; // register the extended function terms std::map< Node, Node > mvarg_to_term; - std::vector tr_no_base; + std::vector trNeedsMaster; bool needPi = false; // for computing congruence std::map argTrie; @@ -943,6 +947,47 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, 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 ); @@ -969,31 +1014,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { 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 repList; for (const Node& ac : a) @@ -1022,14 +1043,19 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } 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 { @@ -1052,47 +1078,50 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } // 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()) { @@ -1123,7 +1152,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext-mv") << "Arguments of trancendental functions : " << std::endl; - for (std::pair >& tfl : d_f_map) + for (std::pair >& tfl : d_funcMap) { Kind k = tfl.first; if (k == SINE || k == EXPONENTIAL) @@ -2774,7 +2803,7 @@ std::vector NonlinearExtension::checkMonomialInferResBounds() { std::vector NonlinearExtension::checkTranscendentalInitialRefine() { std::vector< Node > lemmas; Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl; - for (std::pair >& tfl : d_f_map) + for (std::pair >& tfl : d_funcMap) { Kind k = tfl.first; for (const Node& t : tfl.second) @@ -2788,9 +2817,11 @@ std::vector NonlinearExtension::checkTranscendentalInitialRefine() { 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( @@ -2884,7 +2915,7 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { std::map< Kind, std::vector< Node > > sorted_tf_args; std::map< Kind, std::map< Node, Node > > tf_arg_to_term; - for (std::pair >& tfl : d_f_map) + for (std::pair >& tfl : d_funcMap) { Kind k = tfl.first; if (k == EXPONENTIAL || k == SINE) @@ -2908,7 +2939,7 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { //sort by concrete values smv.d_isConcrete = true; smv.d_reverse_order = true; - for (std::pair >& tfl : d_f_map) + for (std::pair >& tfl : d_funcMap) { Kind k = tfl.first; if( !sorted_tf_args[k].empty() ){ @@ -3045,7 +3076,7 @@ std::vector NonlinearExtension::checkTranscendentalTangentPlanes( << std::endl; // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions // via Incremental Linearization" by Cimatti et al - for (std::pair >& tfs : d_f_map) + for (std::pair >& tfs : d_funcMap) { Kind k = tfs.first; if (k == PI) @@ -3070,24 +3101,21 @@ std::vector NonlinearExtension::checkTranscendentalTangentPlanes( 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; } } } @@ -3102,14 +3130,19 @@ bool NonlinearExtension::checkTfTangentPlanesFun( std::vector& lemmas, std::map& 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().sgn(); + if (csign == 0) + { + // no secant/tangent plane is necessary + return true; + } Assert(csign == 1 || csign == -1); // Figure 3: P_l, P_u @@ -3148,7 +3181,8 @@ bool NonlinearExtension::checkTfTangentPlanesFun( 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 > @@ -3239,7 +3273,7 @@ bool NonlinearExtension::checkTfTangentPlanesFun( else { // we may want to continue getting better bounds - return true; + return false; } if (is_tangent) @@ -3415,7 +3449,7 @@ bool NonlinearExtension::checkTfTangentPlanesFun( // 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) @@ -3819,11 +3853,21 @@ std::pair NonlinearExtension::getTfModelBounds(Node tf, unsigned d) Node c = d_model.computeAbstractModelValue(tf[0]); Assert(c.isConst()); int csign = c.getConst().sgn(); - Assert(csign != 0); + Kind k = tf.getKind(); + if (csign == 0) + { + // at zero, its trivial + if (k == SINE) + { + return std::pair(d_zero, d_zero); + } + Assert(k == EXPONENTIAL); + return std::pair(d_one, d_one); + } bool isNeg = csign == -1; std::vector pbounds; - getPolynomialApproximationBoundForArg(tf.getKind(), c, d, pbounds); + getPolynomialApproximationBoundForArg(k, c, d, pbounds); std::vector bounds; TNode tfv = d_taylor_real_fv; diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 64a601cc5..2fda9a895 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -511,13 +511,21 @@ class NonlinearExtension { //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 d_tr_base; - /** Stores skolems in the range of the above map */ - std::map d_tr_is_base; + std::map d_trMaster; + std::map > d_trSlaves; + /** The transcendental functions we have done initial refinements on */ std::map< Node, bool > d_tf_initial_refine; void mkPi(); @@ -544,8 +552,24 @@ class NonlinearExtension { std::map > > d_ci_exp; std::map > > d_ci_max; - /** A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } */ - std::map > 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 > d_funcCongClass; + /** + * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } + * that are representives of their congruence class. + */ + std::map > d_funcMap; // factor skolems std::map< Node, Node > d_factor_skolem; @@ -644,13 +668,6 @@ class NonlinearExtension { * on the model value of its argument. */ std::pair 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 @@ -953,14 +970,20 @@ class NonlinearExtension { std::map& 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,