diff options
| -rw-r--r-- | src/options/arith_options | 6 | ||||
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 9 | ||||
| -rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 411 | ||||
| -rw-r--r-- | src/theory/arith/nonlinear_extension.h | 72 | ||||
| -rw-r--r-- | test/regress/regress0/nl/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/nl/nta/cos1-tc.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/nl/nta/sin1-sat.smt2 | 12 |
7 files changed, 399 insertions, 116 deletions
diff --git a/src/options/arith_options b/src/options/arith_options index 3ba1b00f6..e6f7fd6d0 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -195,4 +195,10 @@ option nlExtPurify --nl-ext-purify bool :default false option nlExtSplitZero --nl-ext-split-zero bool :default false intial splits on zero for all variables +option nlExtTfTaylorDegree --nl-ext-tf-taylor-deg=N int16_t :default 4 :read-write + initial degree of polynomials for Taylor approximation + +option nlExtTfIncPrecision --nl-ext-tf-inc-prec bool :default true + whether to increment the precision for transcendental function constraints + endmodule diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 72f9cdf4a..b47cb1e60 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -381,8 +381,15 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { case kind::SINE: if(t[0].getKind() == kind::CONST_RATIONAL){ const Rational& rat = t[0].getConst<Rational>(); + NodeManager* nm = NodeManager::currentNM(); if(rat.sgn() == 0){ - return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(0))); + return RewriteResponse(REWRITE_DONE, nm->mkConst(Rational(0))); + } + else if (rat.sgn() == -1) + { + Node ret = + nm->mkNode(kind::UMINUS, nm->mkNode(kind::SINE, nm->mkConst(-rat))); + return RewriteResponse(REWRITE_AGAIN_FULL, ret); } }else{ // get the factor of PI in the argument diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 20f19db9d..65a7597f1 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -236,6 +236,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, "a", NodeManager::currentNM()->realType()); d_taylor_real_fv_base_rem = NodeManager::currentNM()->mkBoundVar( "b", NodeManager::currentNM()->realType()); + d_taylor_degree = options::nlExtTfTaylorDegree(); } NonlinearExtension::~NonlinearExtension() {} @@ -1107,9 +1108,10 @@ int NonlinearExtension::flushLemmas(std::vector<Node>& lemmas) { return sum; } -std::set<Node> NonlinearExtension::getFalseInModel( - const std::vector<Node>& assertions) { - std::set<Node> false_asserts; +std::vector<Node> NonlinearExtension::checkModel( + const std::vector<Node>& assertions) +{ + std::vector<Node> false_asserts; for (size_t i = 0; i < assertions.size(); ++i) { Node lit = assertions[i]; Node atom = lit.getKind()==NOT ? lit[0] : lit; @@ -1119,7 +1121,7 @@ std::set<Node> NonlinearExtension::getFalseInModel( if (litv != d_true) { Trace("nl-ext-mv") << " [model-false]" << std::endl; //Assert(litv == d_false); - false_asserts.insert(lit); + false_asserts.push_back(lit); } else { Trace("nl-ext-mv") << std::endl; } @@ -1128,6 +1130,132 @@ std::set<Node> NonlinearExtension::getFalseInModel( return false_asserts; } +bool NonlinearExtension::checkModelTf(const std::vector<Node>& assertions) +{ + Trace("nl-ext-tf-check-model") << "check-model : Run" << std::endl; + // add bounds for PI + d_tf_check_model_bounds[d_pi] = + std::pair<Node, Node>(d_pi_bound[0], d_pi_bound[1]); + for (const std::pair<const Node, std::pair<Node, Node> >& tfb : + d_tf_check_model_bounds) + { + Node tf = tfb.first; + Trace("nl-ext-tf-check-model") + << "check-model : satisfied approximate bound : "; + Trace("nl-ext-tf-check-model") << tfb.second.first << " <= " << tf + << " <= " << tfb.second.second << std::endl; + } + + std::vector<Node> check_assertions; + for (const Node& a : assertions) + { + Node av = computeModelValue(a); + // simple check + if (!simpleCheckModelTfLit(av)) + { + check_assertions.push_back(av); + Trace("nl-ext-tf-check-model") << "check-model : assertion : " << av + << " (from " << a << ")" << std::endl; + } + } + + if (check_assertions.empty()) + { + return true; + } + else + { + // TODO (#1450) check model for general case + return false; + } +} + +bool NonlinearExtension::simpleCheckModelTfLit(Node lit) +{ + Trace("nl-ext-tf-check-model-simple") << "simple check-model for " << lit + << "..." << std::endl; + NodeManager* nm = NodeManager::currentNM(); + bool pol = lit.getKind() != kind::NOT; + Node atom = lit.getKind() == kind::NOT ? lit[0] : lit; + + if (atom.getKind() == kind::GEQ) + { + std::map<Node, Node> msum; + if (ArithMSum::getMonomialSumLit(atom, msum)) + { + // map from transcendental functions to whether they were set to lower + // bound + std::map<Node, bool> set_bound; + std::vector<Node> sum_bound; + for (std::pair<const Node, Node>& m : msum) + { + Node v = m.first; + if (v.isNull()) + { + sum_bound.push_back(m.second.isNull() ? d_one : m.second); + } + else + { + std::map<Node, std::pair<Node, Node> >::iterator bit = + d_tf_check_model_bounds.find(v); + if (bit != d_tf_check_model_bounds.end()) + { + bool set_lower = + (m.second.isNull() || m.second.getConst<Rational>().sgn() == 1) + == pol; + std::map<Node, bool>::iterator itsb = set_bound.find(v); + if (itsb != set_bound.end() && itsb->second != set_lower) + { + Trace("nl-ext-tf-check-model-simple") + << " failed due to conflicting bound for " << v << std::endl; + return false; + } + set_bound[v] = set_lower; + // must over/under approximate + Node vbound = set_lower ? bit->second.first : bit->second.second; + sum_bound.push_back(ArithMSum::mkCoeffTerm(m.second, vbound)); + } + else + { + Trace("nl-ext-tf-check-model-simple") + << " failed due to unknown bound for " << v << std::endl; + return false; + } + } + } + Node bound; + if (sum_bound.size() > 1) + { + bound = nm->mkNode(kind::PLUS, sum_bound); + } + else if (sum_bound.size() == 1) + { + bound = sum_bound[0]; + } + else + { + bound = d_zero; + } + Node comp = nm->mkNode(kind::GEQ, bound, d_zero); + if (!pol) + { + comp = comp.negate(); + } + Trace("nl-ext-tf-check-model-simple") << " comparison is : " << comp + << std::endl; + comp = Rewriter::rewrite(comp); + Assert(comp.isConst()); + Trace("nl-ext-tf-check-model-simple") << " returned : " << comp + << std::endl; + return comp == d_true; + } + } + + Trace("nl-ext-tf-check-model-simple") << " failed due to unknown literal." + << std::endl; + return false; +} + std::vector<Node> NonlinearExtension::checkSplitZero() { std::vector<Node> lemmas; for (unsigned i = 0; i < d_ms_vars.size(); i++) { @@ -1143,8 +1271,9 @@ std::vector<Node> NonlinearExtension::checkSplitZero() { } int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, - const std::set<Node>& false_asserts, - const std::vector<Node>& xts) { + const std::vector<Node>& false_asserts, + const std::vector<Node>& xts) +{ d_ms_vars.clear(); d_ms_proc.clear(); d_ms.clear(); @@ -1156,6 +1285,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, d_ci_max.clear(); d_tf_rep_map.clear(); d_tf_region.clear(); + d_tf_check_model_bounds.clear(); int lemmas_proc = 0; std::vector<Node> lemmas; @@ -1454,101 +1584,161 @@ void NonlinearExtension::check(Theory::Effort e) { } } } else { - Assert(e == Theory::EFFORT_LAST_CALL); - Trace("nl-ext-mv") << "Getting model values... check for [model-false]" - << std::endl; - // reset cached information - d_mv[0].clear(); - d_mv[1].clear(); - - // get the assertions - std::vector<Node> assertions; - for (Theory::assertions_iterator it = d_containing.facts_begin(); - it != d_containing.facts_end(); ++it) { - const Assertion& assertion = *it; - assertions.push_back(assertion.assertion); - } - // get the assertions that are false in the model - const std::set<Node> false_asserts = getFalseInModel(assertions); - - // get the extended terms belonging to this theory - std::vector<Node> xts; - d_containing.getExtTheory()->getTerms(xts); - - if( Trace.isOn("nl-ext-debug") ){ - Trace("nl-ext-debug") << " processing NonlinearExtension::check : " << std::endl; - Trace("nl-ext-debug") << " " << false_asserts.size() << " false assertions" << std::endl; - Trace("nl-ext-debug") << " " << xts.size() << " extended terms: " << std::endl; - Trace("nl-ext-debug") << " "; - for( unsigned j=0; j<xts.size(); j++ ){ - Trace("nl-ext-debug") << xts[j] << " "; - } - Trace("nl-ext-debug") << std::endl; - } - - // compute whether shared terms have correct values - unsigned num_shared_wrong_value = 0; - std::vector< Node > shared_term_value_splits; - //must ensure that shared terms are equal to their concrete value - for (context::CDList<TNode>::const_iterator its = d_containing.shared_terms_begin(); - its != d_containing.shared_terms_end(); ++its) { - TNode shared_term = *its; - // compute its value in the model, and its evaluation in the model - Node stv0 = computeModelValue( shared_term, 0 ); - Node stv1 = computeModelValue( shared_term, 1 ); - if( stv0!=stv1 ){ - num_shared_wrong_value++; - Trace("nl-ext-mv") << "Bad shared term value : " << shared_term << " : " << stv1 << ", actual is " << stv0 << std::endl; - if( shared_term!=stv0 ){ - //split on the value, this is non-terminating in general, TODO : improve this - Node eq = shared_term.eqNode(stv0); - shared_term_value_splits.push_back( eq ); - }else{ - // this can happen for transcendental functions - // the problem is that we cannot evaluate transcendental functions (they don't have a rewriter that returns constants) - // thus, the actual value in their model can be themselves, hence we have no reference - // point to rule out the current model. In this case, we may set incomplete below. + bool needsRecheck; + do + { + needsRecheck = false; + Assert(e == Theory::EFFORT_LAST_CALL); + Trace("nl-ext-mv") << "Getting model values... check for [model-false]" + << std::endl; + // reset cached information + d_mv[0].clear(); + d_mv[1].clear(); + + // get the assertions + std::vector<Node> assertions; + for (Theory::assertions_iterator it = d_containing.facts_begin(); + it != d_containing.facts_end(); + ++it) + { + const Assertion& assertion = *it; + assertions.push_back(assertion.assertion); + } + // get the assertions that are false in the model + const std::vector<Node> false_asserts = checkModel(assertions); + + // get the extended terms belonging to this theory + std::vector<Node> xts; + d_containing.getExtTheory()->getTerms(xts); + + if (Trace.isOn("nl-ext-debug")) + { + Trace("nl-ext-debug") << " processing NonlinearExtension::check : " + << std::endl; + Trace("nl-ext-debug") << " " << false_asserts.size() + << " false assertions" << std::endl; + Trace("nl-ext-debug") << " " << xts.size() + << " extended terms: " << std::endl; + Trace("nl-ext-debug") << " "; + for (unsigned j = 0; j < xts.size(); j++) + { + Trace("nl-ext-debug") << xts[j] << " "; } + Trace("nl-ext-debug") << std::endl; } - } - Trace("nl-ext-debug") << " " << num_shared_wrong_value << " shared terms with wrong model value." << std::endl; - - // we require a check either if an assertion is false or a shared term has a wrong value - bool isIncomplete = false; - int num_added_lemmas = 0; - if(!false_asserts.empty() || num_shared_wrong_value>0 ){ - isIncomplete = true; - num_added_lemmas = checkLastCall(assertions, false_asserts, xts); - } - - //if we did not add a lemma during check - if(num_added_lemmas==0) { - if(num_shared_wrong_value>0) { - // resort to splitting on shared terms with their model value - isIncomplete = true; - if( !shared_term_value_splits.empty() ){ - std::vector< Node > shared_term_value_lemmas; - for( unsigned i=0; i<shared_term_value_splits.size(); i++ ){ - Node eq = shared_term_value_splits[i]; - Node literal = d_containing.getValuation().ensureLiteral(eq); - d_containing.getOutputChannel().requirePhase(literal, true); - shared_term_value_lemmas.push_back(literal.orNode(literal.negate())); + + // compute whether shared terms have correct values + unsigned num_shared_wrong_value = 0; + std::vector<Node> shared_term_value_splits; + // must ensure that shared terms are equal to their concrete value + for (context::CDList<TNode>::const_iterator its = + d_containing.shared_terms_begin(); + its != d_containing.shared_terms_end(); + ++its) + { + TNode shared_term = *its; + // compute its value in the model, and its evaluation in the model + Node stv0 = computeModelValue(shared_term, 0); + Node stv1 = computeModelValue(shared_term, 1); + if (stv0 != stv1) + { + num_shared_wrong_value++; + Trace("nl-ext-mv") << "Bad shared term value : " << shared_term + << " : " << stv1 << ", actual is " << stv0 + << std::endl; + if (shared_term != stv0) + { + // split on the value, this is non-terminating in general, TODO : + // improve this + Node eq = shared_term.eqNode(stv0); + shared_term_value_splits.push_back(eq); + } + else + { + // this can happen for transcendental functions + // the problem is that we cannot evaluate transcendental functions + // (they don't have a rewriter that returns constants) + // thus, the actual value in their model can be themselves, hence we + // have no reference + // point to rule out the current model. In this case, we may set + // incomplete below. } - num_added_lemmas = flushLemmas(shared_term_value_lemmas); - Trace("nl-ext") << "...added " << num_added_lemmas << " shared term value split lemmas." << std::endl; - }else{ - // this can happen if we are trying to do theory combination with trancendental functions - // since their model value cannot even be computed exactly } } - + Trace("nl-ext-debug") << " " << num_shared_wrong_value + << " shared terms with wrong model value." + << std::endl; + + // we require a check either if an assertion is false or a shared term has + // a wrong value + bool isIncomplete = false; + int num_added_lemmas = 0; + if (!false_asserts.empty() || num_shared_wrong_value > 0) + { + isIncomplete = true; + num_added_lemmas = checkLastCall(assertions, false_asserts, xts); + } + + // if we did not add a lemma during check if(num_added_lemmas==0) { - if(isIncomplete) { - Trace("nl-ext") << "...failed to send lemma in NonLinearExtension, set incomplete" << std::endl; - d_containing.getOutputChannel().setIncomplete(); + if (num_shared_wrong_value > 0) + { + // resort to splitting on shared terms with their model value + isIncomplete = true; + if (!shared_term_value_splits.empty()) + { + std::vector<Node> shared_term_value_lemmas; + for (const Node& eq : shared_term_value_splits) + { + Node literal = d_containing.getValuation().ensureLiteral(eq); + d_containing.getOutputChannel().requirePhase(literal, true); + shared_term_value_lemmas.push_back( + literal.orNode(literal.negate())); + } + num_added_lemmas = flushLemmas(shared_term_value_lemmas); + Trace("nl-ext") << "...added " << num_added_lemmas + << " shared term value split lemmas." << std::endl; + } + else + { + // this can happen if we are trying to do theory combination with + // trancendental functions + // since their model value cannot even be computed exactly + } + } + if (num_added_lemmas == 0) + { + if (isIncomplete) + { + // check the model using error bounds on the Taylor approximation + if (!d_tf_rep_map.empty() && checkModelTf(false_asserts)) + { + isIncomplete = false; + } + } + if (isIncomplete) + { + if (options::nlExtTfIncPrecision() && !d_tf_rep_map.empty()) + { + d_taylor_degree++; + d_secant_points.clear(); + needsRecheck = true; + // increase precision for PI? + // Difficult since Taylor series is very slow to converge + Trace("nl-ext") << "...increment Taylor degree to " + << d_taylor_degree << std::endl; + } + else + { + Trace("nl-ext") << "...failed to send lemma in " + "NonLinearExtension, set incomplete" + << std::endl; + d_containing.getOutputChannel().setIncomplete(); + } + } } } - } + } while (needsRecheck); } } @@ -1666,8 +1856,8 @@ void NonlinearExtension::mkPi(){ void NonlinearExtension::getCurrentPiBounds( std::vector< Node >& lemmas ) { Node pi_lem = NodeManager::currentNM()->mkNode( AND, - NodeManager::currentNM()->mkNode(GT, d_pi, d_pi_bound[0]), - NodeManager::currentNM()->mkNode(LT, d_pi, d_pi_bound[1])); + NodeManager::currentNM()->mkNode(GEQ, d_pi, d_pi_bound[0]), + NodeManager::currentNM()->mkNode(LEQ, d_pi, d_pi_bound[1])); lemmas.push_back( pi_lem ); } @@ -2239,12 +2429,11 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() { Trace("nl-ext") << "...trying " << lemmas.size() << " tangent plane lemmas..." << std::endl; return lemmas; -} - +} - -std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node>& nt_lemmas, - const std::set<Node>& false_asserts ) { +std::vector<Node> NonlinearExtension::checkMonomialInferBounds( + std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts) +{ std::vector< Node > lemmas; // register constraints Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; @@ -2255,7 +2444,9 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node bool polarity = lit.getKind() != NOT; Node atom = lit.getKind() == NOT ? lit[0] : lit; registerConstraint(atom); - bool is_false_lit = false_asserts.find(lit) != false_asserts.end(); + bool is_false_lit = + std::find(false_asserts.begin(), false_asserts.end(), lit) + != false_asserts.end(); // add information about bounds to variables std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc = d_c_info.find(atom); @@ -2505,7 +2696,9 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node return lemmas; } -std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& false_asserts ) { +std::vector<Node> NonlinearExtension::checkFactoring( + const std::vector<Node>& false_asserts) +{ std::vector< Node > lemmas; Trace("nl-ext") << "Get factoring lemmas..." << std::endl; for (context::CDList<Assertion>::const_iterator it = @@ -2514,7 +2707,10 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& fals Node lit = (*it).assertion; bool polarity = lit.getKind() != NOT; Node atom = lit.getKind() == NOT ? lit[0] : lit; - if( false_asserts.find(lit) != false_asserts.end() || d_skolem_atoms.find(atom)!=d_skolem_atoms.end() ){ + if (std::find(false_asserts.begin(), false_asserts.end(), lit) + != false_asserts.end() + || d_skolem_atoms.find(atom) != d_skolem_atoms.end()) + { std::map<Node, Node> msum; if (ArithMSum::getMonomialSumLit(atom, msum)) { @@ -3044,7 +3240,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() std::map<int, Node> poly_approx_bounds_neg[2]; // the negative case is different for exp // n is the Taylor degree we are currently considering - unsigned n = 8; + unsigned n = 2 * d_taylor_degree; // n must be even std::pair<Node, Node> taylor = getTaylor(tft, n); Trace("nl-ext-tf-tplanes-debug") << "Taylor for " << k @@ -3241,6 +3437,13 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes() Trace("nl-ext-tf-tplanes-debug") << "...poly appoximation at c is " << poly_approx_c << std::endl; } + else + { + // store for check model bounds + Node atf = computeModelValue(tf); + d_tf_check_model_bounds[atf] = + std::pair<Node, Node>(model_values[0], model_values[1]); + } if (is_tangent) { diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index d95b3c0f4..34da28f6c 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -179,7 +179,7 @@ class NonlinearExtension { * TheoryArith. */ int checkLastCall(const std::vector<Node>& assertions, - const std::set<Node>& false_asserts, + const std::vector<Node>& false_asserts, const std::vector<Node>& xts); //---------------------------------------term utilities static bool isArithKind(Kind k); @@ -228,10 +228,48 @@ class NonlinearExtension { void assignOrderIds(std::vector<Node>& vars, NodeMultiset& d_order, unsigned orderType); - /** Returns the subset of assertions whose concrete values are - * false in the model. + /** check model + * + * Returns the subset of assertions whose concrete values we cannot show are + * true in the current model. Notice that we typically cannot compute concrete + * values for assertions involving transcendental functions. Any assertion + * whose model value cannot be computed is included in the return value of + * this function. + */ + std::vector<Node> checkModel(const std::vector<Node>& assertions); + + /** check model for transcendental functions + * + * Checks the current model using error bounds on the Taylor approximation. + * + * If this function returns true, then all assertions in the input argument + * "assertions" are satisfied for all interpretations of transcendental + * functions within their error bounds (as stored in d_tf_check_model_bounds). + * + * For details, see Section 3 of Cimatti et al CADE 2017 under the heading + * "Detecting Satisfiable Formulas". + */ + bool checkModelTf(const std::vector<Node>& assertions); + + /** simple check model for transcendental functions for literal + * + * This method returns true if literal is true for all interpretations of + * transcendental functions within their error bounds (as stored + * in d_tf_check_model_bounds). This is determined by a simple under/over + * approximation of the value of sum of (linear) monomials. For example, + * if we determine that .8 < sin( 1 ) < .9, this function will return + * true for literals like: + * 2.0*sin( 1 ) > 1.5 + * -1.0*sin( 1 ) < -0.79 + * -1.0*sin( 1 ) > -0.91 + * It will return false for literals like: + * sin( 1 ) > 0.85 + * It will also return false for literals like: + * -0.3*sin( 1 )*sin( 2 ) + sin( 2 ) > .7 + * sin( sin( 1 ) ) > .5 + * since the bounds on these terms cannot quickly be determined. */ - std::set<Node> getFalseInModel(const std::vector<Node>& assertions); + bool simpleCheckModelTfLit(Node lit); /** In the following functions, status states a relationship * between two arithmetic terms, where: @@ -438,8 +476,15 @@ private: * where r is the current representative of x * in the equality engine assoiated with this class. */ - std::map< Kind, std::map< Node, Node > > d_tf_rep_map; - + std::map<Kind, std::map<Node, Node> > d_tf_rep_map; + + /** bounds for transcendental functions + * + * For each transcendental function application t, if this stores the pair + * (c_l, c_u) then the model M is such that c_l <= M( t ) <= c_u. + */ + std::map<Node, std::pair<Node, Node> > d_tf_check_model_bounds; + // factor skolems std::map< Node, Node > d_factor_skolem; Node getFactorSkolem( Node n, std::vector< Node >& lemmas ); @@ -489,6 +534,15 @@ private: std::unordered_map<Node, std::unordered_map<unsigned, Node>, NodeHashFunction> d_taylor_rem; + /** taylor degree + * + * Indicates that the degree of the polynomials in the Taylor approximation of + * all transcendental functions is 2*d_taylor_degree. This value is set + * initially to options::nlExtTfTaylorDegree() and may be incremented + * if the option options::nlExtTfIncPrecision() is enabled. + */ + unsigned d_taylor_degree; + /** concavity region for transcendental functions * * This stores an integer that identifies an interval in @@ -614,8 +668,8 @@ private: * ...where (y > z + w) and x*y are a constraint and term * that occur in the current context. */ - std::vector<Node> checkMonomialInferBounds( std::vector<Node>& nt_lemmas, - const std::set<Node>& false_asserts ); + std::vector<Node> checkMonomialInferBounds( + std::vector<Node>& nt_lemmas, const std::vector<Node>& false_asserts); /** check factoring * @@ -629,7 +683,7 @@ private: * ...where k is fresh and x*z + y*z > t is a * constraint that occurs in the current context. */ - std::vector<Node> checkFactoring( const std::set<Node>& false_asserts ); + std::vector<Node> checkFactoring(const std::vector<Node>& false_asserts); /** check monomial infer resolution bounds * diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index 9fb581565..4f7c2172b 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -78,7 +78,8 @@ TESTS = \ nta/exp-n0.5-ub.smt2 \ nta/exp-n0.5-lb.smt2 \ nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \ - nta/NAVIGATION2.smt2 + nta/NAVIGATION2.smt2 \ + nta/sin1-sat.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/nl/nta/cos1-tc.smt2 b/test/regress/regress0/nl/nta/cos1-tc.smt2 index 80d3eec89..7ddae1453 100644 --- a/test/regress/regress0/nl/nta/cos1-tc.smt2 +++ b/test/regress/regress0/nl/nta/cos1-tc.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --nl-ext +; COMMAND-LINE: --nl-ext --no-nl-ext-tf-inc-prec ; EXPECT: unknown (set-logic UFNRA) (declare-fun f (Real) Real) diff --git a/test/regress/regress0/nl/nta/sin1-sat.smt2 b/test/regress/regress0/nl/nta/sin1-sat.smt2 new file mode 100644 index 000000000..d6275c6e8 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin1-sat.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 1) 0.84)) +(assert (< (sin 1) 0.85)) +(assert (< (- x (sin 1)) 0.000001)) +(assert (< (- (sin 1) x) 0.000001)) + +(check-sat) |