From bb095659fb12e3733a73f1be31769ff5b5eb6055 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 24 Nov 2017 06:44:46 -0600 Subject: [PATCH] Implement tangent and secant planes for transcendental functions (#1401) --- src/options/arith_options | 3 + src/theory/arith/nonlinear_extension.cpp | 939 ++++++++++++++---- src/theory/arith/nonlinear_extension.h | 59 ++ test/regress/regress0/nl/Makefile.am | 15 +- test/regress/regress0/nl/nta/NAVIGATION2.smt2 | 23 + ...libre_artes_ex_5_13.transcendental.k2.smt2 | 22 + test/regress/regress0/nl/nta/exp-4.5-lt.smt2 | 9 + test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 | 10 + test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 | 10 + test/regress/regress0/nl/nta/exp1-lb.smt2 | 10 + test/regress/regress0/nl/nta/exp1-ub.smt2 | 11 + test/regress/regress0/nl/nta/sin1-lb.smt2 | 10 + test/regress/regress0/nl/nta/sin1-ub.smt2 | 10 + test/regress/regress0/nl/nta/sin2-lb.smt2 | 10 + test/regress/regress0/nl/nta/sin2-ub.smt2 | 10 + 15 files changed, 931 insertions(+), 220 deletions(-) create mode 100644 test/regress/regress0/nl/nta/NAVIGATION2.smt2 create mode 100644 test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 create mode 100644 test/regress/regress0/nl/nta/exp-4.5-lt.smt2 create mode 100644 test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 create mode 100644 test/regress/regress0/nl/nta/exp1-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/exp1-ub.smt2 create mode 100644 test/regress/regress0/nl/nta/sin1-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/sin1-ub.smt2 create mode 100644 test/regress/regress0/nl/nta/sin2-lb.smt2 create mode 100644 test/regress/regress0/nl/nta/sin2-ub.smt2 diff --git a/src/options/arith_options b/src/options/arith_options index bddde7a16..3ba1b00f6 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -177,6 +177,9 @@ option nlExtFactor --nl-ext-factor bool :default true option nlExtTangentPlanes --nl-ext-tplanes bool :default false use non-terminating tangent plane strategy for non-linear +option nlExtTfTangentPlanes --nl-ext-tf-tplanes bool :default false + use non-terminating tangent plane strategy for transcendental functions for non-linear + option nlExtEntailConflicts --nl-ext-ent-conf bool :default false check for entailed conflicts in non-linear solver diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index e3e078bbe..77c4e2e40 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -26,7 +26,6 @@ #include "theory/quantifiers/quant_util.h" #include "theory/theory_model.h" -using namespace std; using namespace CVC4::kind; namespace CVC4 { @@ -199,7 +198,8 @@ bool hasNewMonomials(Node n, const std::vector& existing) { worklist.pop_back(); if (!Contains(visited, current)) { visited.insert(current); - if (current.getKind() == kind::NONLINEAR_MULT) { + if (current.getKind() == NONLINEAR_MULT) + { if (!IsInVector(existing, current)) { return true; } @@ -280,8 +280,8 @@ void NonlinearExtension::registerMonomialSubset(Node a, Node b) { d_m_contain_parent[a].push_back(b); d_m_contain_children[b].push_back(a); - Node mult_term = safeConstructNary(kind::MULT, diff_children); - Node nlmult_term = safeConstructNary(kind::NONLINEAR_MULT, diff_children); + Node mult_term = safeConstructNary(MULT, diff_children); + Node nlmult_term = safeConstructNary(NONLINEAR_MULT, diff_children); d_m_contain_mult[a][b] = mult_term; d_m_contain_umult[a][b] = nlmult_term; Trace("nl-ext-mindex") << "..." << a << " is a subset of " << b @@ -405,7 +405,10 @@ bool NonLinearExtentionSubstitutionSolver::solve( if (!QuantArith::getMonomialSum(ns, msum)) { success = false; }else{ - d_rep_sum_unique_exp[n] = exp_rm.size()==1 ? exp_rm[0] : NodeManager::currentNM()->mkNode( kind::AND, exp_rm ); + d_rep_sum_unique_exp[n] = + exp_rm.size() == 1 + ? exp_rm[0] + : NodeManager::currentNM()->mkNode(AND, exp_rm); d_rep_sum_unique[n] = ns; } } @@ -487,9 +490,8 @@ bool NonLinearExtentionSubstitutionSolver::setSubstitutionConst( d_rep_to_const[r] = r_c; Node expn; if (!r_c_exp.empty()) { - expn = r_c_exp.size() == 1 - ? r_c_exp[0] - : NodeManager::currentNM()->mkNode(kind::AND, r_c_exp); + expn = r_c_exp.size() == 1 ? r_c_exp[0] + : NodeManager::currentNM()->mkNode(AND, r_c_exp); Trace("nl-subs-debug") << "...explanation is " << expn << std::endl; d_rep_to_const_exp[r] = expn; } @@ -670,11 +672,11 @@ std::pair NonlinearExtension::isExtfReduced( int effort, Node n, Node on, const std::vector& exp) const { if (n != d_zero) { Kind k = n.getKind(); - return std::make_pair(k != kind::NONLINEAR_MULT && !isTranscendentalKind(k), + return std::make_pair(k != NONLINEAR_MULT && !isTranscendentalKind(k), Node::null()); } Assert(n == d_zero); - if (on.getKind() == kind::NONLINEAR_MULT) + if (on.getKind() == NONLINEAR_MULT) { Trace("nl-ext-zero-exp") << "Infer zero : " << on << " == " << n << std::endl; @@ -686,15 +688,15 @@ std::pair NonlinearExtension::isExtfReduced( Trace("nl-ext-zero-exp") << " exp[" << i << "] = " << exp[i] << std::endl; std::vector eqs; - if (exp[i].getKind() == kind::EQUAL) + if (exp[i].getKind() == EQUAL) { eqs.push_back(exp[i]); } - else if (exp[i].getKind() == kind::AND) + else if (exp[i].getKind() == AND) { for (const Node& ec : exp[i]) { - if (ec.getKind() == kind::EQUAL) + if (ec.getKind() == EQUAL) { eqs.push_back(ec); } @@ -727,7 +729,10 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { Node ret; if (n.isConst()) { ret = n; - } else if (index == 1 && ( n.getKind() == kind::NONLINEAR_MULT || isTranscendentalKind( n.getKind() ) )) { + } + else if (index == 1 && (n.getKind() == NONLINEAR_MULT + || isTranscendentalKind(n.getKind()))) + { if (d_containing.getValuation().getModel()->hasTerm(n)) { // use model value for abstraction ret = d_containing.getValuation().getModel()->getRepresentative(n); @@ -738,7 +743,8 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { } //Assert( ret.isConst() ); } else if (n.getNumChildren() == 0) { - if( n.getKind()==kind::PI ){ + if (n.getKind() == PI) + { // we are interested in the exact value of PI, which cannot be computed. // hence, we return PI itself when asked for the concrete value. ret = n; @@ -748,7 +754,8 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { } else { // otherwise, compute true value std::vector children; - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (n.getMetaKind() == metakind::PARAMETERIZED) + { children.push_back(n.getOperator()); } for (unsigned i = 0; i < n.getNumChildren(); i++) { @@ -756,7 +763,8 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { children.push_back(mc); } ret = NodeManager::currentNM()->mkNode(n.getKind(), children); - if( n.getKind()==kind::APPLY_UF ){ + if (n.getKind() == APPLY_UF) + { ret = d_containing.getValuation().getModel()->getValue(ret); }else{ ret = Rewriter::rewrite(ret); @@ -786,7 +794,8 @@ void NonlinearExtension::registerMonomial(Node n) { if (!IsInVector(d_monomials, n)) { d_monomials.push_back(n); Trace("nl-ext-debug") << "Register monomial : " << n << std::endl; - if (n.getKind() == kind::NONLINEAR_MULT) { + if (n.getKind() == NONLINEAR_MULT) + { // get exponent count for (unsigned k = 0; k < n.getNumChildren(); k++) { d_m_exp[n][n[k]]++; @@ -886,7 +895,7 @@ void NonlinearExtension::registerConstraint(Node atom) { } bool NonlinearExtension::isArithKind(Kind k) { - return k == kind::PLUS || k == kind::MULT || k == kind::NONLINEAR_MULT; + return k == PLUS || k == MULT || k == NONLINEAR_MULT; } Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) { @@ -896,7 +905,7 @@ Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) { return a_eq_b; } else { // return mkAbs( a ).eqNode( mkAbs( b ) ); - Node negate_b = NodeManager::currentNM()->mkNode(kind::UMINUS, b); + Node negate_b = NodeManager::currentNM()->mkNode(UMINUS, b); return a_eq_b.orNode(a.eqNode(negate_b)); } } else if (status < 0) { @@ -904,16 +913,16 @@ Node NonlinearExtension::mkLit(Node a, Node b, int status, int orderType) { } else { Assert(status == 1 || status == 2); NodeManager* nm = NodeManager::currentNM(); - Kind greater_op = status == 1 ? kind::GEQ : kind::GT; + Kind greater_op = status == 1 ? GEQ : GT; if (orderType == 0) { return nm->mkNode(greater_op, a, b); } else { // return nm->mkNode( greater_op, mkAbs( a ), mkAbs( b ) ); Node zero = mkRationalNode(0); - Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, zero); - Node b_is_nonnegative = nm->mkNode(kind::GEQ, b, zero); - Node negate_a = nm->mkNode(kind::UMINUS, a); - Node negate_b = nm->mkNode(kind::UMINUS, b); + Node a_is_nonnegative = nm->mkNode(GEQ, a, zero); + Node b_is_nonnegative = nm->mkNode(GEQ, b, zero); + Node negate_a = nm->mkNode(UMINUS, a); + Node negate_b = nm->mkNode(UMINUS, b); return a_is_nonnegative.iteNode( b_is_nonnegative.iteNode(nm->mkNode(greater_op, a, b), nm->mkNode(greater_op, a, negate_b)), @@ -928,19 +937,21 @@ Node NonlinearExtension::mkAbs(Node a) { return mkRationalNode(a.getConst().abs()); } else { NodeManager* nm = NodeManager::currentNM(); - Node a_is_nonnegative = nm->mkNode(kind::GEQ, a, mkRationalNode(0)); - return a_is_nonnegative.iteNode(a, nm->mkNode(kind::UMINUS, a)); + Node a_is_nonnegative = nm->mkNode(GEQ, a, mkRationalNode(0)); + return a_is_nonnegative.iteNode(a, nm->mkNode(UMINUS, a)); } } Node NonlinearExtension::mkValidPhase(Node a, Node pi) { - return mkBounded( NodeManager::currentNM()->mkNode( kind::MULT, mkRationalNode(-1), pi ), a, pi ); + return mkBounded( + NodeManager::currentNM()->mkNode(MULT, mkRationalNode(-1), pi), a, pi); } Node NonlinearExtension::mkBounded( Node l, Node a, Node u ) { - return NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::GEQ, a, l ), - NodeManager::currentNM()->mkNode( kind::LEQ, a, u ) ); + return NodeManager::currentNM()->mkNode( + AND, + NodeManager::currentNM()->mkNode(GEQ, a, l), + NodeManager::currentNM()->mkNode(LEQ, a, u)); } // by a b, a b, we know a b @@ -950,24 +961,33 @@ Kind NonlinearExtension::joinKinds(Kind k1, Kind k2) { } else if (k1 == k2) { return k1; } else { - Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ || - k1 == kind::GT || k1 == kind::GEQ); - Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ || - k2 == kind::GT || k2 == kind::GEQ); - if (k1 == kind::EQUAL) { - if (k2 == kind::LEQ || k2 == kind::GEQ) { + Assert(k1 == EQUAL || k1 == LT || k1 == LEQ || k1 == GT || k1 == GEQ); + Assert(k2 == EQUAL || k2 == LT || k2 == LEQ || k2 == GT || k2 == GEQ); + if (k1 == EQUAL) + { + if (k2 == LEQ || k2 == GEQ) + { return k1; } - } else if (k1 == kind::LT) { - if (k2 == kind::LEQ) { + } + else if (k1 == LT) + { + if (k2 == LEQ) + { return k1; } - } else if (k1 == kind::LEQ) { - if (k2 == kind::GEQ) { - return kind::EQUAL; + } + else if (k1 == LEQ) + { + if (k2 == GEQ) + { + return EQUAL; } - } else if (k1 == kind::GT) { - if (k2 == kind::GEQ) { + } + else if (k1 == GT) + { + if (k2 == GEQ) + { return k1; } } @@ -982,18 +1002,23 @@ Kind NonlinearExtension::transKinds(Kind k1, Kind k2) { } else if (k1 == k2) { return k1; } else { - Assert(k1 == kind::EQUAL || k1 == kind::LT || k1 == kind::LEQ || - k1 == kind::GT || k1 == kind::GEQ); - Assert(k2 == kind::EQUAL || k2 == kind::LT || k2 == kind::LEQ || - k2 == kind::GT || k2 == kind::GEQ); - if (k1 == kind::EQUAL) { + Assert(k1 == EQUAL || k1 == LT || k1 == LEQ || k1 == GT || k1 == GEQ); + Assert(k2 == EQUAL || k2 == LT || k2 == LEQ || k2 == GT || k2 == GEQ); + if (k1 == EQUAL) + { return k2; - } else if (k1 == kind::LT) { - if (k2 == kind::LEQ) { + } + else if (k1 == LT) + { + if (k2 == LEQ) + { return k1; } - } else if (k1 == kind::GT) { - if (k2 == kind::GEQ) { + } + else if (k1 == GT) + { + if (k2 == GEQ) + { return k1; } } @@ -1002,8 +1027,8 @@ Kind NonlinearExtension::transKinds(Kind k1, Kind k2) { } bool NonlinearExtension::isTranscendentalKind(Kind k) { - Assert( k != kind::TANGENT && k != kind::COSINE ); //eliminated - return k==kind::EXPONENTIAL || k==kind::SINE || k==kind::PI; + Assert(k != TANGENT && k != COSINE); // eliminated + return k == EXPONENTIAL || k == SINE || k == PI; } Node NonlinearExtension::mkMonomialRemFactor( @@ -1023,7 +1048,7 @@ Node NonlinearExtension::mkMonomialRemFactor( << "......rem, now " << inc << " factors of " << v << std::endl; children.insert(children.end(), inc, v); } - Node ret = safeConstructNary(kind::MULT, children); + Node ret = safeConstructNary(MULT, children); ret = Rewriter::rewrite(ret); Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl; return ret; @@ -1142,8 +1167,9 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, << d_mv[0][a] << " ]" << std::endl; //Assert(d_mv[1][a].isConst()); //Assert(d_mv[0][a].isConst()); - - if( a.getKind()==kind::NONLINEAR_MULT ){ + + if (a.getKind() == NONLINEAR_MULT) + { d_ms.push_back( a ); //context-independent registration @@ -1177,7 +1203,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, }else if( a.getNumChildren()==1 ){ bool consider = true; // get shifted version - if( a.getKind()==kind::SINE ){ + if (a.getKind() == SINE) + { if( d_trig_is_base.find( a )==d_trig_is_base.end() ){ consider = false; if( d_trig_base.find( a )==d_trig_base.end() ){ @@ -1193,12 +1220,21 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, Node shift = NodeManager::currentNM()->mkSkolem( "s", NodeManager::currentNM()->integerType(), "number of shifts" ); // FIXME : do not introduce shift here, instead needs model-based // refinement for constant shifts (#1284) - Node shift_lem = NodeManager::currentNM()->mkNode( kind::AND, mkValidPhase( y, d_pi ), - a[0].eqNode( NodeManager::currentNM()->mkNode( kind::PLUS, y, - NodeManager::currentNM()->mkNode( kind::MULT, NodeManager::currentNM()->mkConst( Rational(2) ), shift, d_pi ) ) ), - //particular case of above for shift=0 - NodeManager::currentNM()->mkNode( kind::IMPLIES, mkValidPhase( a[0], d_pi ), a[0].eqNode( y ) ), - new_a.eqNode( a ) ); + Node shift_lem = NodeManager::currentNM()->mkNode( + AND, + mkValidPhase(y, d_pi), + a[0].eqNode(NodeManager::currentNM()->mkNode( + PLUS, + y, + NodeManager::currentNM()->mkNode( + MULT, + NodeManager::currentNM()->mkConst(Rational(2)), + shift, + d_pi))), + // particular case of above for shift=0 + NodeManager::currentNM()->mkNode( + IMPLIES, mkValidPhase(a[0], d_pi), a[0].eqNode(y)), + new_a.eqNode(a)); //must do preprocess on this one Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : shift : " << shift_lem << std::endl; d_containing.getOutputChannel().lemma(shift_lem, false, true); @@ -1213,7 +1249,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, //verify they have the same model value if( d_mv[1][a]!=d_mv[1][itrm->second] ){ // if not, add congruence lemma - Node cong_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, a[0].eqNode( itrm->second[0] ), a.eqNode( itrm->second ) ); + Node cong_lemma = NodeManager::currentNM()->mkNode( + IMPLIES, a[0].eqNode(itrm->second[0]), a.eqNode(itrm->second)); lemmas.push_back( cong_lemma ); //Assert( false ); } @@ -1221,7 +1258,9 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, d_tf_rep_map[a.getKind()][r] = a; } } - }else if( a.getKind()==kind::PI ){ + } + else if (a.getKind() == PI) + { //TODO? }else{ Assert( false ); @@ -1370,9 +1409,19 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } //------------------------------------tangent planes - if (options::nlExtTangentPlanes()) { - lemmas = checkTangentPlanes(); - lemmas_proc = flushLemmas(lemmas); + if (options::nlExtTangentPlanes() || options::nlExtTfTangentPlanes()) + { + lemmas_proc = 0; + if (options::nlExtTangentPlanes()) + { + lemmas = checkTangentPlanes(); + lemmas_proc += flushLemmas(lemmas); + } + if (options::nlExtTfTangentPlanes()) + { + lemmas = checkTranscendentalTangentPlanes(); + lemmas_proc += flushLemmas(lemmas); + } if (lemmas_proc > 0) { Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return lemmas_proc; @@ -1592,10 +1641,18 @@ int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const { void NonlinearExtension::mkPi(){ if( d_pi.isNull() ){ - d_pi = NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI ); - d_pi_2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ) ) ); - d_pi_neg_2 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(-1)/Rational(2) ) ) ); - d_pi_neg = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, d_pi, NodeManager::currentNM()->mkConst( Rational(-1) ) ) ); + d_pi = NodeManager::currentNM()->mkNullaryOperator( + NodeManager::currentNM()->realType(), PI); + d_pi_2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + MULT, + d_pi, + NodeManager::currentNM()->mkConst(Rational(1) / Rational(2)))); + d_pi_neg_2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + MULT, + d_pi, + NodeManager::currentNM()->mkConst(Rational(-1) / Rational(2)))); + d_pi_neg = Rewriter::rewrite(NodeManager::currentNM()->mkNode( + MULT, d_pi, NodeManager::currentNM()->mkConst(Rational(-1)))); //initialize bounds d_pi_bound[0] = NodeManager::currentNM()->mkConst( Rational(333)/Rational(106) ); d_pi_bound[1] = NodeManager::currentNM()->mkConst( Rational(355)/Rational(113) ); @@ -1603,9 +1660,10 @@ void NonlinearExtension::mkPi(){ } void NonlinearExtension::getCurrentPiBounds( std::vector< Node >& lemmas ) { - Node pi_lem = NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::GT, d_pi, d_pi_bound[0] ), - NodeManager::currentNM()->mkNode( kind::LT, d_pi, d_pi_bound[1] ) ); + 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])); lemmas.push_back( pi_lem ); } @@ -1658,8 +1716,8 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, Assert(d_mv[1].find(oa) != d_mv[1].end()); if (a_index == d_m_vlist[a].size()) { if (d_mv[1][oa].getConst().sgn() != status) { - Node lemma = safeConstructNary(kind::AND, exp) - .impNode(mkLit(oa, d_zero, status * 2)); + Node lemma = + safeConstructNary(AND, exp).impNode(mkLit(oa, d_zero, status * 2)); lem.push_back(lemma); } return status; @@ -1684,8 +1742,8 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, exp.push_back(av.eqNode(d_zero).negate()); return compareSign(oa, a, a_index + 1, status, exp, lem); } else { - exp.push_back(NodeManager::currentNM()->mkNode( - sgn == 1 ? kind::GT : kind::LT, av, d_zero)); + exp.push_back( + NodeManager::currentNM()->mkNode(sgn == 1 ? GT : LT, av, d_zero)); return compareSign(oa, a, a_index + 1, status * sgn, exp, lem); } } @@ -1764,8 +1822,7 @@ bool NonlinearExtension::compareMonomial( } } Node clem = NodeManager::currentNM()->mkNode( - kind::IMPLIES, safeConstructNary(kind::AND, exp), - mkLit(oa, ob, status, 1)); + IMPLIES, safeConstructNary(AND, exp), mkLit(oa, ob, status, 1)); Trace("nl-ext-comp-lemma") << "comparison lemma : " << clem << std::endl; lem.push_back(clem); cmp_infers[status][oa][ob] = clem; @@ -2149,21 +2206,21 @@ std::vector NonlinearExtension::checkTangentPlanes() { // tangent plane Node tplane = NodeManager::currentNM()->mkNode( - kind::MINUS, + MINUS, NodeManager::currentNM()->mkNode( - kind::PLUS, - NodeManager::currentNM()->mkNode(kind::MULT, b_v, a), - NodeManager::currentNM()->mkNode(kind::MULT, a_v, b)), - NodeManager::currentNM()->mkNode(kind::MULT, a_v, b_v)); + PLUS, + NodeManager::currentNM()->mkNode(MULT, b_v, a), + NodeManager::currentNM()->mkNode(MULT, a_v, b)), + NodeManager::currentNM()->mkNode(MULT, a_v, b_v)); for (unsigned d = 0; d < 4; d++) { Node aa = NodeManager::currentNM()->mkNode( - d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v); + d == 0 || d == 3 ? GEQ : LEQ, a, a_v); Node ab = NodeManager::currentNM()->mkNode( - d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v); + d == 1 || d == 3 ? GEQ : LEQ, b, b_v); Node conc = NodeManager::currentNM()->mkNode( - d <= 1 ? kind::LEQ : kind::GEQ, t, tplane); + d <= 1 ? LEQ : GEQ, t, tplane); Node tlem = NodeManager::currentNM()->mkNode( - kind::OR, aa.negate(), ab.negate(), conc); + OR, aa.negate(), ab.negate(), conc); Trace("nl-ext-tplanes") << "Tangent plane lemma : " << tlem << std::endl; lemmas.push_back(tlem); @@ -2191,8 +2248,8 @@ std::vector NonlinearExtension::checkMonomialInferBounds( std::vector NonlinearExtension::checkMonomialInferBounds( std::vectormkNode(kind::GT, lhs, rhs); + Node query = NodeManager::currentNM()->mkNode(GT, lhs, rhs); Node query_mv = computeModelValue(query, 1); if (query_mv == d_true) { exp = query; - type = kind::GT; + type = GT; } else { Assert(query_mv == d_false); - exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs); - type = kind::LT; + exp = NodeManager::currentNM()->mkNode(LT, lhs, rhs); + type = LT; } } else { type = negateKind(type); @@ -2246,7 +2304,8 @@ std::vector NonlinearExtension::checkMonomialInferBounds( std::vectorsecond << std::endl; Kind jk = joinKinds(type, its->second); - if (jk == kind::UNDEFINED_KIND) { + if (jk == UNDEFINED_KIND) + { updated = false; } else if (jk != its->second) { if (jk == type) { @@ -2255,7 +2314,7 @@ std::vector NonlinearExtension::checkMonomialInferBounds( std::vectormkNode( - kind::AND, d_ci_exp[x][coeff][rhs], exp); + AND, d_ci_exp[x][coeff][rhs], exp); } } else { updated = false; @@ -2282,20 +2341,25 @@ std::vector NonlinearExtension::checkMonomialInferBounds( std::vector() > rhs_v.getConst()) { - if (type != kind::GT && type != kind::GEQ) { + if (type != GT && type != GEQ) + { needsRefine = true; refineDir = false; } } else { - if (type != kind::LT && type != kind::LEQ) { + if (type != LT && type != LEQ) + { needsRefine = true; refineDir = true; } @@ -2328,7 +2392,7 @@ std::vector NonlinearExtension::checkMonomialInferBounds( std::vector NonlinearExtension::checkMonomialInferBounds( std::vectormkNode(kind::MULT, mult, t); + NodeManager::currentNM()->mkNode(MULT, mult, t); Node infer_rhs = - NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs); + NodeManager::currentNM()->mkNode(MULT, mult, rhs); Node infer = NodeManager::currentNM()->mkNode( infer_type, infer_lhs, infer_rhs); Trace("nl-ext-bound-debug") << " " << infer << std::endl; @@ -2397,12 +2461,12 @@ std::vector NonlinearExtension::checkMonomialInferBounds( std::vectormkNode( - kind::AND, + AND, NodeManager::currentNM()->mkNode( - mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero), + mmv_sign == 1 ? GT : LT, mult, d_zero), d_ci_exp[x][coeff][rhs]); - Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES, - exp, infer); + Node iblem = + NodeManager::currentNM()->mkNode(IMPLIES, exp, infer); Node pr_iblem = iblem; iblem = Rewriter::rewrite(iblem); bool introNewTerms = hasNewMonomials(iblem, d_ms); @@ -2444,8 +2508,8 @@ std::vector NonlinearExtension::checkFactoring( const std::set& fals d_containing.facts_begin(); it != d_containing.facts_end(); ++it) { Node lit = (*it).assertion; - bool polarity = lit.getKind() != kind::NOT; - Node atom = lit.getKind() == kind::NOT ? lit[0] : lit; + 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() ){ std::map msum; if (QuantArith::getMonomialSumLit(atom, msum)) { @@ -2470,7 +2534,7 @@ std::vector NonlinearExtension::checkFactoring( const std::set& fals if( !itm->second.isNull() ){ children.push_back( itm->second ); } - Node val = NodeManager::currentNM()->mkNode( kind::MULT, children ); + Node val = NodeManager::currentNM()->mkNode(MULT, children); if( !itm->second.isNull() ){ children.pop_back(); } @@ -2488,12 +2552,13 @@ std::vector NonlinearExtension::checkFactoring( const std::set& fals } for( std::map< Node, std::vector< Node > >::iterator itf = factor_to_mono.begin(); itf != factor_to_mono.end(); ++itf ){ if( itf->second.size()>1 ){ - Node sum = NodeManager::currentNM()->mkNode( kind::PLUS, itf->second ); + Node sum = NodeManager::currentNM()->mkNode(PLUS, itf->second); sum = Rewriter::rewrite( sum ); Trace("nl-ext-factor") << "* Factored sum for " << itf->first << " : " << sum << std::endl; Node kf = getFactorSkolem( sum, lemmas ); std::vector< Node > poly; - poly.push_back( NodeManager::currentNM()->mkNode( kind::MULT, itf->first, kf ) ); + poly.push_back( + NodeManager::currentNM()->mkNode(MULT, itf->first, kf)); std::map< Node, std::vector< Node > >::iterator itfo = factor_to_mono_orig.find( itf->first ); Assert( itfo!=factor_to_mono_orig.end() ); for( std::map::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ @@ -2501,7 +2566,9 @@ std::vector NonlinearExtension::checkFactoring( const std::set& fals poly.push_back( QuantArith::mkCoeffTerm(itm->second, itm->first.isNull() ? d_one : itm->first) ); } } - Node polyn = poly.size()==1 ? poly[0] : NodeManager::currentNM()->mkNode( kind::PLUS, poly ); + Node polyn = poly.size() == 1 + ? poly[0] + : NodeManager::currentNM()->mkNode(PLUS, poly); Trace("nl-ext-factor") << "...factored polynomial : " << polyn << std::endl; Node conc_lit = NodeManager::currentNM()->mkNode( atom.getKind(), polyn, d_zero ); conc_lit = Rewriter::rewrite( conc_lit ); @@ -2513,7 +2580,7 @@ std::vector NonlinearExtension::checkFactoring( const std::set& fals std::vector< Node > lemma_disj; lemma_disj.push_back( lit.negate() ); lemma_disj.push_back( conc_lit ); - Node flem = NodeManager::currentNM()->mkNode( kind::OR, lemma_disj ); + Node flem = NodeManager::currentNM()->mkNode(OR, lemma_disj); Trace("nl-ext-factor") << "...lemma is " << flem << std::endl; lemmas.push_back( flem ); } @@ -2585,8 +2652,8 @@ std::vector NonlinearExtension::checkMonomialInferResBounds() { itcac->second.begin(); itcar != itcac->second.end(); ++itcar) { Node rhs_a = itcar->first; - Node rhs_a_res_base = NodeManager::currentNM()->mkNode( - kind::MULT, itb->second, rhs_a); + Node rhs_a_res_base = + NodeManager::currentNM()->mkNode(MULT, itb->second, rhs_a); rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base); if (!hasNewMonomials(rhs_a_res_base, d_ms)) { Kind type_a = itcar->second; @@ -2604,7 +2671,7 @@ std::vector NonlinearExtension::checkMonomialInferResBounds() { itcbr != itcbc->second.end(); ++itcbr) { Node rhs_b = itcbr->first; Node rhs_b_res = NodeManager::currentNM()->mkNode( - kind::MULT, ita->second, rhs_b); + MULT, ita->second, rhs_b); rhs_b_res = QuantArith::mkCoeffTerm(coeff_a, rhs_b_res); rhs_b_res = Rewriter::rewrite(rhs_b_res); if (!hasNewMonomials(rhs_b_res, d_ms)) { @@ -2632,25 +2699,25 @@ std::vector NonlinearExtension::checkMonomialInferResBounds() { } if (pivot_factor_sign == 1) { exp.push_back(NodeManager::currentNM()->mkNode( - kind::GT, pivot_factor, d_zero)); + GT, pivot_factor, d_zero)); } else { exp.push_back(NodeManager::currentNM()->mkNode( - kind::LT, pivot_factor, d_zero)); + LT, pivot_factor, d_zero)); } } Kind jk = transKinds(types[0], types[1]); Trace("nl-ext-rbound-debug") << "trans kind : " << types[0] << " + " << types[1] << " = " << jk << std::endl; - if (jk != kind::UNDEFINED_KIND) { + if (jk != UNDEFINED_KIND) + { Node conc = NodeManager::currentNM()->mkNode( jk, rhs_a_res, rhs_b_res); Node conc_mv = computeModelValue(conc, 1); if (conc_mv == d_false) { Node rblem = NodeManager::currentNM()->mkNode( - kind::IMPLIES, - NodeManager::currentNM()->mkNode(kind::AND, - exp), + IMPLIES, + NodeManager::currentNM()->mkNode(AND, exp), conc); Trace("nl-ext-rbound-lemma-debug") << "Resolution bound lemma " @@ -2693,67 +2760,88 @@ std::vector NonlinearExtension::checkTranscendentalInitialRefine() { if( d_tf_initial_refine.find( t )==d_tf_initial_refine.end() ){ d_tf_initial_refine[t] = true; Node lem; - if( it->first==kind::SINE ){ - Node symn = NodeManager::currentNM()->mkNode( kind::SINE, - NodeManager::currentNM()->mkNode( kind::MULT, d_neg_one, t[0] ) ); + if (it->first == SINE) + { + 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_trig_is_base[symn] = true; Assert( d_trig_is_base.find( t ) != d_trig_is_base.end() ); std::vector< Node > children; - - lem = NodeManager::currentNM()->mkNode( kind::AND, - //bounds - NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::LEQ, t, d_one ), - NodeManager::currentNM()->mkNode( kind::GEQ, t, d_neg_one ) ), - //symmetry - NodeManager::currentNM()->mkNode( kind::PLUS, t, symn ).eqNode( d_zero ), - //sign - NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::LT, t[0], d_zero ), - NodeManager::currentNM()->mkNode( kind::LT, t, d_zero ) ), - //zero val - NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::GT, t[0], d_zero ), - NodeManager::currentNM()->mkNode( kind::GT, t, d_zero ) ) ); - lem = NodeManager::currentNM()->mkNode( kind::AND, lem, - //zero tangent - NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::GT, t[0], d_zero ), - NodeManager::currentNM()->mkNode( kind::LT, t, t[0] ) ), - NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::LT, t[0], d_zero ), - NodeManager::currentNM()->mkNode( kind::GT, t, t[0] ) ) ), - //pi tangent - NodeManager::currentNM()->mkNode( kind::AND, - NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::LT, t[0], d_pi ), - NodeManager::currentNM()->mkNode( kind::LT, t, NodeManager::currentNM()->mkNode( kind::MINUS, d_pi, t[0] ) ) ), - NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::GT, t[0], d_pi_neg ), - NodeManager::currentNM()->mkNode( kind::GT, t, NodeManager::currentNM()->mkNode( kind::MINUS, d_pi_neg, t[0] ) ) ) ) ); - }else if( it->first==kind::EXPONENTIAL ){ + + lem = NodeManager::currentNM()->mkNode( + AND, + // bounds + NodeManager::currentNM()->mkNode( + AND, + NodeManager::currentNM()->mkNode(LEQ, t, d_one), + NodeManager::currentNM()->mkNode(GEQ, t, d_neg_one)), + // symmetry + NodeManager::currentNM()->mkNode(PLUS, t, symn).eqNode(d_zero), + // sign + NodeManager::currentNM()->mkNode( + EQUAL, + NodeManager::currentNM()->mkNode(LT, t[0], d_zero), + NodeManager::currentNM()->mkNode(LT, t, d_zero)), + // zero val + NodeManager::currentNM()->mkNode( + EQUAL, + NodeManager::currentNM()->mkNode(GT, t[0], d_zero), + NodeManager::currentNM()->mkNode(GT, t, d_zero))); + lem = NodeManager::currentNM()->mkNode( + AND, + lem, + // zero tangent + NodeManager::currentNM()->mkNode( + AND, + NodeManager::currentNM()->mkNode( + IMPLIES, + NodeManager::currentNM()->mkNode(GT, t[0], d_zero), + NodeManager::currentNM()->mkNode(LT, t, t[0])), + NodeManager::currentNM()->mkNode( + IMPLIES, + NodeManager::currentNM()->mkNode(LT, t[0], d_zero), + NodeManager::currentNM()->mkNode(GT, t, t[0]))), + // pi tangent + NodeManager::currentNM()->mkNode( + AND, + NodeManager::currentNM()->mkNode( + IMPLIES, + NodeManager::currentNM()->mkNode(LT, t[0], d_pi), + NodeManager::currentNM()->mkNode( + LT, + t, + NodeManager::currentNM()->mkNode(MINUS, d_pi, t[0]))), + NodeManager::currentNM()->mkNode( + IMPLIES, + NodeManager::currentNM()->mkNode(GT, t[0], d_pi_neg), + NodeManager::currentNM()->mkNode( + GT, + t, + NodeManager::currentNM()->mkNode( + MINUS, d_pi_neg, t[0]))))); + } + else if (it->first == EXPONENTIAL) + { // ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) < // 1 ) ^ ( x <= 0 V exp( x ) > x + 1 ) lem = NodeManager::currentNM()->mkNode( - kind::AND, - NodeManager::currentNM()->mkNode(kind::GT, t, d_zero), + AND, + NodeManager::currentNM()->mkNode(GT, t, d_zero), NodeManager::currentNM()->mkNode( - kind::EQUAL, t[0].eqNode(d_zero), t.eqNode(d_one)), + EQUAL, t[0].eqNode(d_zero), t.eqNode(d_one)), NodeManager::currentNM()->mkNode( - kind::EQUAL, - NodeManager::currentNM()->mkNode(kind::LT, t[0], d_zero), - NodeManager::currentNM()->mkNode(kind::LT, t, d_one)), + EQUAL, + NodeManager::currentNM()->mkNode(LT, t[0], d_zero), + NodeManager::currentNM()->mkNode(LT, t, d_one)), NodeManager::currentNM()->mkNode( - kind::OR, - NodeManager::currentNM()->mkNode(kind::LEQ, t[0], d_zero), + OR, + NodeManager::currentNM()->mkNode(LEQ, t[0], d_zero), NodeManager::currentNM()->mkNode( - kind::GT, + GT, t, - NodeManager::currentNM()->mkNode( - kind::PLUS, t[0], d_one)))); + NodeManager::currentNM()->mkNode(PLUS, t[0], d_one)))); } if( !lem.isNull() ){ lemmas.push_back( lem ); @@ -2805,13 +2893,16 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { } std::vector< Node > mpoints; std::vector< Node > mpoints_vals; - if( it->first==kind::SINE ){ + if (it->first == SINE) + { mpoints.push_back( d_pi ); mpoints.push_back( d_pi_2 ); mpoints.push_back(d_zero); mpoints.push_back( d_pi_neg_2 ); mpoints.push_back( d_pi_neg ); - }else if( it->first==kind::EXPONENTIAL ){ + } + else if (it->first == EXPONENTIAL) + { mpoints.push_back( Node::null() ); } if( !mpoints.empty() ){ @@ -2877,22 +2968,26 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { if( !tval.isNull() ){ Node mono_lem; if( monotonic_dir==1 && sval.getConst() > tval.getConst() ){ - mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::GEQ, targ, sarg ), - NodeManager::currentNM()->mkNode( kind::GEQ, t, s ) ); + mono_lem = NodeManager::currentNM()->mkNode( + IMPLIES, + NodeManager::currentNM()->mkNode(GEQ, targ, sarg), + NodeManager::currentNM()->mkNode(GEQ, t, s)); }else if( monotonic_dir==-1 && sval.getConst() < tval.getConst() ){ - mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::LEQ, targ, sarg ), - NodeManager::currentNM()->mkNode( kind::LEQ, t, s ) ); + mono_lem = NodeManager::currentNM()->mkNode( + IMPLIES, + NodeManager::currentNM()->mkNode(LEQ, targ, sarg), + NodeManager::currentNM()->mkNode(LEQ, t, s)); } if( !mono_lem.isNull() ){ if( !mono_bounds[0].isNull() ){ Assert( !mono_bounds[1].isNull() ); - mono_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, - NodeManager::currentNM()->mkNode( kind::AND, - mkBounded( mono_bounds[0], targ, mono_bounds[1] ), - mkBounded( mono_bounds[0], sarg, mono_bounds[1] ) ), - mono_lem ); + mono_lem = NodeManager::currentNM()->mkNode( + IMPLIES, + NodeManager::currentNM()->mkNode( + AND, + mkBounded(mono_bounds[0], targ, mono_bounds[1]), + mkBounded(mono_bounds[0], sarg, mono_bounds[1])), + mono_lem); } Trace("nl-ext-tf-mono") << "Monotonicity lemma : " << mono_lem << std::endl; lemmas.push_back( mono_lem ); @@ -2910,16 +3005,424 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { return lemmas; } +std::vector NonlinearExtension::checkTranscendentalTangentPlanes() +{ + std::vector lemmas; + Trace("nl-ext") << "Get tangent plane lemmas for transcendental functions..." + << std::endl; + + NodeManager* nm = NodeManager::currentNM(); + // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions + // via Incremental Linearization" by Cimatti et al + for (std::pair >& tfs : d_tf_rep_map) + { + Kind k = tfs.first; + Node tft = nm->mkNode(k, d_zero); + Trace("nl-ext-tf-tplanes-debug") << "Taylor variables: " << std::endl; + Trace("nl-ext-tf-tplanes-debug") + << " taylor_real_fv : " << d_taylor_real_fv << std::endl; + Trace("nl-ext-tf-tplanes-debug") + << " taylor_real_fv_base : " << d_taylor_real_fv_base << std::endl; + Trace("nl-ext-tf-tplanes-debug") + << " taylor_real_fv_base_rem : " << d_taylor_real_fv_base_rem + << std::endl; + Trace("nl-ext-tf-tplanes-debug") << std::endl; + + // we substitute into the Taylor sum P_{n,f(0)}( x ) + std::vector taylor_vars; + taylor_vars.push_back(d_taylor_real_fv); + + // Figure 3: P_l, P_u + // mapped to for signs of c + std::map poly_approx_bounds[2]; + std::map + poly_approx_bounds_neg[2]; // the negative case is different for exp + // n is the Taylor degree we are currently considering + unsigned n = 8; + // n must be even + std::pair taylor = getTaylor(tft, n); + Trace("nl-ext-tf-tplanes-debug") << "Taylor for " << k + << " is : " << taylor.first << std::endl; + Node taylor_sum = Rewriter::rewrite(taylor.first); + Trace("nl-ext-tf-tplanes-debug") << "Taylor for " << k + << " is (post-rewrite) : " << taylor_sum + << std::endl; + Assert(taylor.second.getKind() == MULT); + Assert(taylor.second.getNumChildren() == 2); + Assert(taylor.second[0].getKind() == DIVISION); + Trace("nl-ext-tf-tplanes-debug") << "Taylor remainder for " << k << " is " + << taylor.second << std::endl; + // ru is x^{n+1}/(n+1)! + Node ru = nm->mkNode(DIVISION, taylor.second[1], taylor.second[0][1]); + ru = Rewriter::rewrite(ru); + Trace("nl-ext-tf-tplanes-debug") + << "Taylor remainder factor is (post-rewrite) : " << ru << std::endl; + if (k == EXPONENTIAL) + { + poly_approx_bounds[0][1] = taylor_sum; + poly_approx_bounds[0][-1] = taylor_sum; + poly_approx_bounds[1][1] = Rewriter::rewrite( + nm->mkNode(MULT, taylor_sum, nm->mkNode(PLUS, d_one, ru))); + poly_approx_bounds[1][-1] = + Rewriter::rewrite(nm->mkNode(PLUS, taylor_sum, ru)); + } + else + { + Assert(k == SINE); + poly_approx_bounds[0][1] = + Rewriter::rewrite(nm->mkNode(MINUS, taylor_sum, ru)); + poly_approx_bounds[0][-1] = poly_approx_bounds[0][1]; + poly_approx_bounds[1][1] = + Rewriter::rewrite(nm->mkNode(PLUS, taylor_sum, ru)); + poly_approx_bounds[1][-1] = poly_approx_bounds[1][1]; + } + Trace("nl-ext-tf-tplanes") << "Polynomial approximation for " << k + << " is: " << std::endl; + Trace("nl-ext-tf-tplanes") << " Lower (pos): " << poly_approx_bounds[0][1] + << std::endl; + Trace("nl-ext-tf-tplanes") << " Upper (pos): " << poly_approx_bounds[1][1] + << std::endl; + Trace("nl-ext-tf-tplanes") << " Lower (neg): " << poly_approx_bounds[0][-1] + << std::endl; + Trace("nl-ext-tf-tplanes") << " Upper (neg): " << poly_approx_bounds[1][-1] + << std::endl; + + for (std::pair& tfr : tfs.second) + { + // Figure 3 : tf( x ) + Node tf = tfr.second; + + bool consider = true; + if (k == SINE) + { + // we do not consider e.g. sin( -1*x ), since considering sin( x ) will + // have the same effect + consider = tf[0].isVar(); + } + int csign; + Node c; + if (consider) + { + // Figure 3 : c + c = computeModelValue(tf[0], 1); + Assert(c.isConst()); + csign = c.getConst().sgn(); + consider = csign != 0; + } + + if (consider) + { + Assert(csign == 1 || csign == -1); + + // Figure 3 : v + Node v = computeModelValue(tf, 1); + + // check value of tf + Trace("nl-ext-tf-tplanes") << "Process tangent plane refinement for " + << tf << "..." << std::endl; + Trace("nl-ext-tf-tplanes") << " value in model : v = " << v + << std::endl; + Trace("nl-ext-tf-tplanes") << " arg value in model : c = " << c + << std::endl; + + // compute the concavity + int region = -1; + std::unordered_map::iterator itr = + d_tf_region.find(tf); + if (itr != d_tf_region.end()) + { + region = itr->second; + Trace("nl-ext-tf-tplanes") << " region is : " << region << std::endl; + } + // Figure 3 : conc + int concavity = regionToConcavity(k, itr->second); + Trace("nl-ext-tf-tplanes") << " concavity is : " << concavity + << std::endl; + if (concavity != 0) + { + // bounds for which we are this concavity + // Figure 3: < l, u > + Node bounds[2]; + if (k == SINE) + { + bounds[0] = regionToLowerBound(k, region); + Assert(!bounds[0].isNull()); + bounds[1] = regionToUpperBound(k, region); + Assert(!bounds[1].isNull()); + } + + // Figure 3: P + Node poly_approx; + + // compute whether this is a tangent refinement or a secant refinement + bool is_tangent = false; + bool is_secant = false; + std::map model_values; + for (unsigned d = 0; d < 2; d++) + { + Node pab = poly_approx_bounds[d][csign]; + if (!pab.isNull()) + { + // { x -> tf[0] } + std::vector taylor_subs; + taylor_subs.push_back(tf[0]); + Assert(taylor_vars.size() == taylor_subs.size()); + pab = pab.substitute(taylor_vars.begin(), + taylor_vars.end(), + taylor_subs.begin(), + taylor_subs.end()); + pab = Rewriter::rewrite(pab); + Node v_pab = computeModelValue(pab, 1); + model_values[d] = v_pab; + Assert(v_pab.isConst()); + Trace("nl-ext-tf-tplanes-debug") << "...model value of " << pab + << " is " << v_pab << std::endl; + Node comp = nm->mkNode(d == 0 ? LT : GT, v, v_pab); + Trace("nl-ext-tf-tplanes-debug") << "...compare : " << comp + << std::endl; + Node compr = Rewriter::rewrite(comp); + Trace("nl-ext-tf-tplanes-debug") << "...got : " << compr + << std::endl; + if (compr == d_true) + { + // beyond the bounds + if (d == 0) + { + poly_approx = poly_approx_bounds[d][csign]; + is_tangent = concavity == 1; + is_secant = concavity == -1; + } + else + { + poly_approx = poly_approx_bounds[d][csign]; + is_tangent = concavity == -1; + is_secant = concavity == 1; + } + Trace("nl-ext-tf-tplanes") << "*** Outside boundary point ("; + Trace("nl-ext-tf-tplanes") << (d == 0 ? "low" : "high") << ") "; + Trace("nl-ext-tf-tplanes") << comp << ", will refine..." + << std::endl; + Trace("nl-ext-tf-tplanes") + << " poly_approx = " << poly_approx << std::endl; + Trace("nl-ext-tf-tplanes") << " is_tangent = " << is_tangent + << std::endl; + Trace("nl-ext-tf-tplanes") << " is_secant = " << is_secant + << std::endl; + break; + } + else + { + Trace("nl-ext-tf-tplanes") << " ...within " + << (d == 0 ? "low" : "high") + << " bound : "; + Trace("nl-ext-tf-tplanes") << comp << std::endl; + } + } + } + + // Figure 3: P( c ) + Node poly_approx_c; + if (is_tangent || is_secant) + { + Assert(!poly_approx.isNull()); + std::vector taylor_subs; + taylor_subs.push_back(c); + Assert(taylor_vars.size() == taylor_subs.size()); + poly_approx_c = poly_approx.substitute(taylor_vars.begin(), + taylor_vars.end(), + taylor_subs.begin(), + taylor_subs.end()); + Trace("nl-ext-tf-tplanes-debug") << "...poly appoximation at c is " + << poly_approx_c << std::endl; + } + + if (is_tangent) + { + // compute tangent plane + // Figure 3: T( x ) + Node tplane; + Node poly_approx_deriv = + getDerivative(poly_approx, d_taylor_real_fv); + Assert(!poly_approx_deriv.isNull()); + poly_approx_deriv = Rewriter::rewrite(poly_approx_deriv); + Trace("nl-ext-tf-tplanes-debug") << "...derivative of " + << poly_approx << " is " + << poly_approx_deriv << std::endl; + std::vector taylor_subs; + taylor_subs.push_back(c); + Assert(taylor_vars.size() == taylor_subs.size()); + Node poly_approx_c_deriv = + poly_approx_deriv.substitute(taylor_vars.begin(), + taylor_vars.end(), + taylor_subs.begin(), + taylor_subs.end()); + tplane = nm->mkNode( + PLUS, + poly_approx_c, + nm->mkNode( + MULT, poly_approx_c_deriv, nm->mkNode(MINUS, tf[0], c))); + + Node lem = nm->mkNode(concavity == 1 ? GEQ : LEQ, tf, tplane); + std::vector antec; + for (unsigned i = 0; i < 2; i++) + { + if (!bounds[i].isNull()) + { + antec.push_back( + nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], bounds[i])); + } + } + if (!antec.empty()) + { + Node antec_n = + antec.size() == 1 ? antec[0] : nm->mkNode(AND, antec); + lem = nm->mkNode(IMPLIES, antec_n, lem); + } + Trace("nl-ext-tf-tplanes") << "*** Tangent plane lemma : " << lem + << std::endl; + // Figure 3 : line 9 + lemmas.push_back(lem); + } + else if (is_secant) + { + // bounds are the minimum and maximum previous secant points + Assert(std::find(d_secant_points[tf].begin(), + d_secant_points[tf].end(), + c) + == d_secant_points[tf].end()); + // insert into the vector + d_secant_points[tf].push_back(c); + // sort + SortNonlinearExtension smv; + smv.d_nla = this; + smv.d_order_type = 0; + std::sort( + d_secant_points[tf].begin(), d_secant_points[tf].end(), smv); + // get the resulting index of c + unsigned index = + std::find( + d_secant_points[tf].begin(), d_secant_points[tf].end(), c) + - d_secant_points[tf].begin(); + // bounds are the next closest upper/lower bound values + if (index > 0) + { + bounds[0] = d_secant_points[tf][index - 1]; + } + else + { + // otherwise, we use the lower boundary point for this concavity + // region + if (k == SINE) + { + Assert(!bounds[0].isNull()); + } + else if (k == EXPONENTIAL) + { + // pick c-1 + bounds[0] = Rewriter::rewrite(nm->mkNode(MINUS, c, d_one)); + } + } + if (index < d_secant_points[tf].size() - 1) + { + bounds[1] = d_secant_points[tf][index + 1]; + } + else + { + // otherwise, we use the upper boundary point for this concavity + // region + if (k == SINE) + { + Assert(!bounds[1].isNull()); + } + else if (k == EXPONENTIAL) + { + // pick c+1 + bounds[1] = Rewriter::rewrite(nm->mkNode(PLUS, c, d_one)); + } + } + Trace("nl-ext-tf-tplanes-debug") + << "...secant bounds are : " << bounds[0] << " ... " + << bounds[1] << std::endl; + + for (unsigned s = 0; s < 2; s++) + { + // compute secant plane + Assert(!poly_approx.isNull()); + Assert(!bounds[s].isNull()); + // take the model value of l or u (since may contain PI) + Node b = computeModelValue(bounds[s], 1); + Trace("nl-ext-tf-tplanes-debug") << "...model value of bound " + << bounds[s] << " is " << b + << std::endl; + Assert(b.isConst()); + if (c != b) + { + // Figure 3 : P(l), P(u), for s = 0,1 + Node poly_approx_b; + std::vector taylor_subs; + taylor_subs.push_back(b); + Assert(taylor_vars.size() == taylor_subs.size()); + poly_approx_b = poly_approx.substitute(taylor_vars.begin(), + taylor_vars.end(), + taylor_subs.begin(), + taylor_subs.end()); + // Figure 3: S_l( x ), S_u( x ) for s = 0,1 + Node splane; + Node rcoeff_n = Rewriter::rewrite(nm->mkNode(MINUS, b, c)); + Assert(rcoeff_n.isConst()); + Rational rcoeff = rcoeff_n.getConst(); + Assert(rcoeff.sgn() != 0); + splane = nm->mkNode( + PLUS, + poly_approx_b, + nm->mkNode(MULT, + nm->mkNode(MINUS, poly_approx_b, poly_approx_c), + nm->mkConst(Rational(1) / rcoeff), + nm->mkNode(MINUS, tf[0], b))); + + Node lem = nm->mkNode(concavity == 1 ? LEQ : GEQ, tf, splane); + // With respect to Figure 3, this is slightly different. + // In particular, we chose b to be the model value of bounds[s], + // which is a constant although bounds[s] may not be (e.g. if it + // contains PI). + // To ensure that c...b does not cross an inflection point, + // we guard with the symbolic version of bounds[s]. + // This leads to lemmas e.g. of this form: + // ( c <= x <= PI/2 ) => ( sin(x) < ( P( b ) - P( c ) )*( x - + // b ) + P( b ) ) + // where b = (PI/2)^M, the current value of PI/2 in the model. + // This is sound since we are guarded by the symbolic + // representation of PI/2. + Node antec_n = + nm->mkNode(AND, + nm->mkNode(GEQ, tf[0], s == 0 ? bounds[s] : c), + nm->mkNode(LEQ, tf[0], s == 0 ? c : bounds[s])); + lem = nm->mkNode(IMPLIES, antec_n, lem); + Trace("nl-ext-tf-tplanes") << "*** Secant plane lemma : " << lem + << std::endl; + // Figure 3 : line 22 + lemmas.push_back(lem); + } + } + } + } + } + } + } + + return lemmas; +} + int NonlinearExtension::regionToMonotonicityDir(Kind k, int region) { - if (k == kind::EXPONENTIAL) + if (k == EXPONENTIAL) { if (region == 1) { return 1; } } - else if (k == kind::SINE) + else if (k == SINE) { if (region == 1 || region == 4) { @@ -2935,14 +3438,14 @@ int NonlinearExtension::regionToMonotonicityDir(Kind k, int region) int NonlinearExtension::regionToConcavity(Kind k, int region) { - if (k == kind::EXPONENTIAL) + if (k == EXPONENTIAL) { if (region == 1) { return 1; } } - else if (k == kind::SINE) + else if (k == SINE) { if (region == 1 || region == 2) { @@ -2958,7 +3461,7 @@ int NonlinearExtension::regionToConcavity(Kind k, int region) Node NonlinearExtension::regionToLowerBound(Kind k, int region) { - if (k == kind::SINE) + if (k == SINE) { if (region == 1) { @@ -2982,7 +3485,7 @@ Node NonlinearExtension::regionToLowerBound(Kind k, int region) Node NonlinearExtension::regionToUpperBound(Kind k, int region) { - if (k == kind::SINE) + if (k == SINE) { if (region == 1) { @@ -3008,24 +3511,24 @@ Node NonlinearExtension::getDerivative(Node n, Node x) { Assert(x.isVar()); // only handle the cases of the taylor expansion of d - if (n.getKind() == kind::EXPONENTIAL) + if (n.getKind() == EXPONENTIAL) { if (n[0] == x) { return n; } } - else if (n.getKind() == kind::SINE) + else if (n.getKind() == SINE) { if (n[0] == x) { - Node na = NodeManager::currentNM()->mkNode(kind::MINUS, d_pi_2, n[0]); - Node ret = NodeManager::currentNM()->mkNode(kind::SINE, na); + Node na = NodeManager::currentNM()->mkNode(MINUS, d_pi_2, n[0]); + Node ret = NodeManager::currentNM()->mkNode(SINE, na); ret = Rewriter::rewrite(ret); return ret; } } - else if (n.getKind() == kind::PLUS) + else if (n.getKind() == PLUS) { std::vector dchildren; for (unsigned i = 0; i < n.getNumChildren(); i++) @@ -3039,18 +3542,18 @@ Node NonlinearExtension::getDerivative(Node n, Node x) dchildren.push_back(dc); } } - return NodeManager::currentNM()->mkNode(kind::PLUS, dchildren); + return NodeManager::currentNM()->mkNode(PLUS, dchildren); } - else if (n.getKind() == kind::MULT) + else if (n.getKind() == MULT) { Assert(n[0].isConst()); Node dc = getDerivative(n[1], x); if (!dc.isNull()) { - return NodeManager::currentNM()->mkNode(kind::MULT, n[0], dc); + return NodeManager::currentNM()->mkNode(MULT, n[0], dc); } } - else if (n.getKind() == kind::NONLINEAR_MULT) + else if (n.getKind() == NONLINEAR_MULT) { unsigned xcount = 0; std::vector children; @@ -3072,7 +3575,7 @@ Node NonlinearExtension::getDerivative(Node n, Node x) { children[xindex] = NodeManager::currentNM()->mkConst(Rational(xcount)); } - return NodeManager::currentNM()->mkNode(kind::MULT, children); + return NodeManager::currentNM()->mkNode(MULT, children); } else if (n.isVar()) { @@ -3115,7 +3618,7 @@ std::pair NonlinearExtension::getTaylor(TNode fa, unsigned n) else { i_exp_base = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::MINUS, d_taylor_real_fv, d_taylor_real_fv_base)); + MINUS, d_taylor_real_fv, d_taylor_real_fv_base)); } Node i_derv = fac; Node i_fact = d_one; @@ -3126,17 +3629,17 @@ std::pair NonlinearExtension::getTaylor(TNode fa, unsigned n) do { counter++; - if (fa.getKind() == kind::EXPONENTIAL) + if (fa.getKind() == EXPONENTIAL) { // unchanged } - else if (fa.getKind() == kind::SINE) + else if (fa.getKind() == SINE) { if (i_derv_status % 2 == 1) { Node arg = NodeManager::currentNM()->mkNode( - kind::PLUS, d_pi_2, d_taylor_real_fv_base); - i_derv = NodeManager::currentNM()->mkNode(kind::SINE, arg); + PLUS, d_pi_2, d_taylor_real_fv_base); + i_derv = NodeManager::currentNM()->mkNode(SINE, arg); } else { @@ -3144,8 +3647,7 @@ std::pair NonlinearExtension::getTaylor(TNode fa, unsigned n) } if (i_derv_status >= 2) { - i_derv = - NodeManager::currentNM()->mkNode(kind::MINUS, d_zero, i_derv); + i_derv = NodeManager::currentNM()->mkNode(MINUS, d_zero, i_derv); } i_derv = Rewriter::rewrite(i_derv); i_derv_status = i_derv_status == 3 ? 0 : i_derv_status + 1; @@ -3156,8 +3658,8 @@ std::pair NonlinearExtension::getTaylor(TNode fa, unsigned n) i_derv = i_derv.substitute(x, d_taylor_real_fv_base_rem); } Node curr = NodeManager::currentNM()->mkNode( - kind::MULT, - NodeManager::currentNM()->mkNode(kind::DIVISION, i_derv, i_fact), + MULT, + NodeManager::currentNM()->mkNode(DIVISION, i_derv, i_fact), i_exp); if (counter == (n + 1)) { @@ -3167,16 +3669,15 @@ std::pair NonlinearExtension::getTaylor(TNode fa, unsigned n) { sum.push_back(curr); i_fact = Rewriter::rewrite(NodeManager::currentNM()->mkNode( - kind::MULT, + MULT, NodeManager::currentNM()->mkConst(Rational(counter)), i_fact)); i_exp = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(kind::MULT, i_exp_base, i_exp)); + NodeManager::currentNM()->mkNode(MULT, i_exp_base, i_exp)); } } while (counter <= n); - taylor_sum = sum.size() == 1 - ? sum[0] - : NodeManager::currentNM()->mkNode(kind::PLUS, sum); + taylor_sum = + sum.size() == 1 ? sum[0] : NodeManager::currentNM()->mkNode(PLUS, sum); if (fac[0] != d_taylor_real_fv_base) { diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 7c41fa096..d95b3c0f4 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -705,6 +705,65 @@ private: */ std::vector checkTranscendentalMonotonic(); + /** check transcendental tangent planes + * + * Returns a set of valid theory lemmas, based on + * computing an "incremental linearization" of + * transcendental functions based on the model values + * of transcendental functions and their arguments. + * It is based on Figure 3 of "Satisfiability + * Modulo Transcendental Functions via Incremental + * Linearization" by Cimatti et al., CADE 2017. + * This schema is not terminating in general. + * It is not enabled by default, and can + * be enabled by --nl-ext-tf-tplanes. + * + * Example: + * + * Assume we have a term sin(y) where M( y ) = 1 where M is the current model. + * Note that: + * sin(1) ~= .841471 + * + * The Taylor series and remainder of sin(y) of degree 7 is + * P_{7,sin(0)}( x ) = x + (-1/6)*x^3 + (1/20)*x^5 + * R_{7,sin(0),b}( x ) = (-1/5040)*x^7 + * + * This gives us lower and upper bounds : + * P_u( x ) = P_{7,sin(0)}( x ) + R_{7,sin(0),b}( x ) + * ...where note P_u( 1 ) = 4243/5040 ~= .841865 + * P_l( x ) = P_{7,sin(0)}( x ) - R_{7,sin(0),b}( x ) + * ...where note P_l( 1 ) = 4241/5040 ~= .841468 + * + * Assume that M( sin(y) ) > P_u( 1 ). + * Since the concavity of sine in the region 0 < x < PI/2 is -1, + * we add a tangent plane refinement. + * The tangent plane at the point 1 in P_u is + * given by the formula: + * T( x ) = P_u( 1 ) + ((d/dx)(P_u(x)))( 1 )*( x - 1 ) + * We add the lemma: + * ( 0 < y < PI/2 ) => sin( y ) <= T( y ) + * which is: + * ( 0 < y < PI/2 ) => sin( y ) <= (391/720)*(y - 2737/1506) + * + * Assume that M( sin(y) ) < P_u( 1 ). + * Since the concavity of sine in the region 0 < x < PI/2 is -1, + * we add a secant plane refinement for some constants ( l, u ) + * such that 0 <= l < M( y ) < u <= PI/2. Assume we choose + * l = 0 and u = M( PI/2 ) = 150517/47912. + * The secant planes at point 1 for P_l + * are given by the formulas: + * S_l( x ) = (x-l)*(P_l( l )-P_l(c))/(l-1) + P_l( l ) + * S_u( x ) = (x-u)*(P_l( u )-P_l(c))/(u-1) + P_l( u ) + * We add the lemmas: + * ( 0 < y < 1 ) => sin( y ) >= S_l( y ) + * ( 1 < y < PI/2 ) => sin( y ) >= S_u( y ) + * which are: + * ( 0 < y < 1 ) => (sin y) >= 4251/5040*y + * ( 1 < y < PI/2 ) => (sin y) >= c1*(y+c2) + * where c1, c2 are rationals (for brevity, omitted here) + * such that c1 ~= .277 and c2 ~= 2.032. + */ + std::vector checkTranscendentalTangentPlanes(); //-------------------------------------------- end lemma schemas }; /* class NonlinearExtension */ diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index d26d53d07..9881b3e72 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -66,7 +66,20 @@ TESTS = \ nta/tan-rewrite.smt2 \ nta/arrowsmith-050317.smt2 \ nta/sin-init-tangents.smt2 \ - nta/cos1-tc.smt2 + nta/cos1-tc.smt2 \ + nta/sin1-ub.smt2 \ + nta/sin1-lb.smt2 \ + nta/sin2-ub.smt2 \ + nta/sin2-lb.smt2 \ + nta/exp1-ub.smt2 \ + nta/exp1-lb.smt2 \ + nta/exp-4.5-lt.smt2 \ + 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 + +# unsolved : garbage_collect.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/nl/nta/NAVIGATION2.smt2 b/test/regress/regress0/nl/nta/NAVIGATION2.smt2 new file mode 100644 index 000000000..445b8a21e --- /dev/null +++ b/test/regress/regress0/nl/nta/NAVIGATION2.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :source |printed by MathSAT|) +(declare-fun X () Real) + +(assert (let ((.def_44 (* (- (/ 11 10)) X))) +(let ((.def_45 (exp .def_44))) +(let ((.def_50 (* 250 .def_45))) +(let ((.def_40 (* (- (/ 13 10)) X))) +(let ((.def_41 (exp .def_40))) +(let ((.def_52 (* 173 .def_41))) +(let ((.def_53 (+ .def_52 .def_50))) +(let ((.def_54 (* 250 X))) +(let ((.def_55 (+ .def_54 .def_53))) +(let ((.def_56 (<= .def_55 (/ 595 2)))) +(let ((.def_57 (not .def_56))) +(let ((.def_31 (<= 0 X))) +(let ((.def_32 (not .def_31))) +(let ((.def_58 (or .def_32 .def_57))) +(let ((.def_59 (not .def_58))) +.def_59)))))))))))))))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 b/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 new file mode 100644 index 000000000..5dce6ddca --- /dev/null +++ b/test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: sat +(set-logic QF_NRA) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun instance.y__AT0@2 () Real) +(declare-fun event_is_timed__AT0@2 () Bool) +(declare-fun instance.EVENT.0__AT0@1 () Bool) +(declare-fun instance.EVENT.1__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun time__AT0@1 () Real) +(declare-fun instance.x__AT0@2 () Real) +(declare-fun time__AT0@2 () Real) +(assert (let ((.def_0 (<= instance.y__AT0@2 2.0))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@1))) (let ((.def_3 (not instance.EVENT.0__AT0@1))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_6 (<= time__AT0@1 time__AT0@2))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@1 time__AT0@2))) (let ((.def_10 (or instance.EVENT.1__AT0@1 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) time__AT0@1))) (let ((.def_13 (+ .def_12 time__AT0@2))) (let ((.def_14 (exp .def_13))) (let ((.def_15 (* instance.y__AT0@1 .def_14))) (let ((.def_16 (= instance.y__AT0@2 .def_15))) (let ((.def_17 (* 970143.0 instance.x__AT0@2))) (let ((.def_18 (* (- 970143.0) instance.x__AT0@1))) (let ((.def_19 (+ .def_18 .def_17))) (let ((.def_20 (* (- 242536.0) instance.y__AT0@1))) (let ((.def_21 (+ .def_20 .def_19))) (let ((.def_22 (* 242536.0 instance.y__AT0@2))) (let ((.def_23 (+ .def_22 .def_21))) (let ((.def_24 (= .def_23 0.0))) (let ((.def_25 (and .def_24 .def_16))) (let ((.def_26 (not .def_9))) (let ((.def_27 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_28 (= instance.y__AT0@2 instance.y__AT0@1))) (let ((.def_29 (and .def_28 .def_27))) (let ((.def_30 (or .def_29 .def_26))) (let ((.def_31 (and .def_30 .def_25))) (let ((.def_32 (and .def_31 .def_6))) (let ((.def_33 (or .def_2 .def_32))) (let ((.def_34 (and .def_33 .def_10))) (let ((.def_35 (and .def_3 .def_2))) (let ((.def_36 (or .def_35 .def_34))) (let ((.def_37 (and .def_36 .def_11))) (let ((.def_38 (not .def_35))) (let ((.def_39 (or .def_38 .def_29))) (let ((.def_40 (and .def_39 .def_37))) (let ((.def_41 (not event_is_timed__AT0@1))) (let ((.def_42 (= event_is_timed__AT0@2 .def_41))) (let ((.def_43 (and .def_42 .def_40))) (let ((.def_44 (and .def_43 .def_4))) (let ((.def_45 (not instance.EVENT.1__AT0@0))) (let ((.def_46 (not instance.EVENT.0__AT0@0))) (let ((.def_47 (or .def_46 .def_45))) (let ((.def_48 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_49 (<= time__AT0@0 time__AT0@1))) (let ((.def_50 (or .def_45 .def_49))) (let ((.def_51 (and .def_50 .def_48))) (let ((.def_52 (= time__AT0@0 time__AT0@1))) (let ((.def_53 (or instance.EVENT.1__AT0@0 .def_52))) (let ((.def_54 (and .def_53 .def_51))) (let ((.def_55 (* (- 1.0) time__AT0@0))) (let ((.def_56 (+ .def_55 time__AT0@1))) (let ((.def_57 (exp .def_56))) (let ((.def_58 (* instance.y__AT0@0 .def_57))) (let ((.def_59 (= instance.y__AT0@1 .def_58))) (let ((.def_60 (+ .def_20 .def_18))) (let ((.def_61 (* 970143.0 instance.x__AT0@0))) (let ((.def_62 (+ .def_61 .def_60))) (let ((.def_63 (* 242536.0 instance.y__AT0@0))) (let ((.def_64 (+ .def_63 .def_62))) (let ((.def_65 (= .def_64 0.0))) (let ((.def_66 (and .def_65 .def_59))) (let ((.def_67 (not .def_52))) (let ((.def_68 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_69 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_70 (and .def_69 .def_68))) (let ((.def_71 (or .def_70 .def_67))) (let ((.def_72 (and .def_71 .def_66))) (let ((.def_73 (and .def_72 .def_49))) (let ((.def_74 (or .def_45 .def_73))) (let ((.def_75 (and .def_74 .def_53))) (let ((.def_76 (and .def_46 .def_45))) (let ((.def_77 (or .def_76 .def_75))) (let ((.def_78 (and .def_77 .def_54))) (let ((.def_79 (not .def_76))) (let ((.def_80 (or .def_79 .def_70))) (let ((.def_81 (and .def_80 .def_78))) (let ((.def_82 (not event_is_timed__AT0@0))) (let ((.def_83 (= event_is_timed__AT0@1 .def_82))) (let ((.def_84 (and .def_83 .def_81))) (let ((.def_85 (and .def_84 .def_47))) (let ((.def_86 (<= instance.x__AT0@0 (- (/ 1 2))))) (let ((.def_87 (not .def_86))) (let ((.def_88 (<= 0.0 instance.x__AT0@0))) (let ((.def_89 (not .def_88))) (let ((.def_90 (and .def_89 .def_87))) (let ((.def_91 (<= 0.0 instance.y__AT0@0))) (let ((.def_92 (not .def_91))) (let ((.def_93 (<= (- (/ 1 2)) instance.y__AT0@0))) (let ((.def_94 (and .def_93 .def_92))) (let ((.def_95 (and .def_94 .def_90))) (let ((.def_96 (= time__AT0@0 0.0))) (let ((.def_97 (and .def_96 .def_95))) (let ((.def_98 (and .def_97 .def_85 .def_44 .def_1))) .def_98)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/nta/exp-4.5-lt.smt2 b/test/regress/regress0/nl/nta/exp-4.5-lt.smt2 new file mode 100644 index 000000000..b0d39ff44 --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-4.5-lt.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) + +(assert (> (exp x) 2000.0)) +(assert (< x 4.5)) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 new file mode 100644 index 000000000..33806cf75 --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-n0.5-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) + +(assert (> (exp (- (/ 1 2))) 0.65)) +(assert (= x (exp (- (/ 1 2))))) + + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 new file mode 100644 index 000000000..b0ea1b39e --- /dev/null +++ b/test/regress/regress0/nl/nta/exp-n0.5-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(declare-fun x () Real) + +(assert (< (exp (- (/ 1 2))) 0.6)) +(assert (= x (exp (- (/ 1 2))))) + + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp1-lb.smt2 b/test/regress/regress0/nl/nta/exp1-lb.smt2 new file mode 100644 index 000000000..b0bc3079c --- /dev/null +++ b/test/regress/regress0/nl/nta/exp1-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (exp 1) 2.719)) +(assert (= x (exp 1))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/exp1-ub.smt2 b/test/regress/regress0/nl/nta/exp1-ub.smt2 new file mode 100644 index 000000000..3b3a14c89 --- /dev/null +++ b/test/regress/regress0/nl/nta/exp1-ub.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (exp 1) 2.717)) +(assert (= x (exp 1))) + + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin1-lb.smt2 b/test/regress/regress0/nl/nta/sin1-lb.smt2 new file mode 100644 index 000000000..f8070cdb8 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin1-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 1) 0.842)) +(assert (= x (sin 1))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin1-ub.smt2 b/test/regress/regress0/nl/nta/sin1-ub.smt2 new file mode 100644 index 000000000..47d322a77 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin1-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (sin 1) 0.8414)) +(assert (= x (sin 1))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin2-lb.smt2 b/test/regress/regress0/nl/nta/sin2-lb.smt2 new file mode 100644 index 000000000..686708230 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin2-lb.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (> (sin 2) 0.96)) +(assert (= x (sin 2))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin2-ub.smt2 b/test/regress/regress0/nl/nta/sin2-ub.smt2 new file mode 100644 index 000000000..51c9eb8a9 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin2-ub.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (< (sin 2) 0.901)) +(assert (= x (sin 2))) + +(check-sat) -- 2.30.2