summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2017-11-24 06:44:46 -0600
committerGitHub <noreply@github.com>2017-11-24 06:44:46 -0600
commitbb095659fb12e3733a73f1be31769ff5b5eb6055 (patch)
treed9e6e40196e80c0bce9983ed00791df32cfd7396
parent612509379a1417f8d4a5e001ff143ba819f5516f (diff)
Implement tangent and secant planes for transcendental functions (#1401)
Diffstat
-rw-r--r--src/options/arith_options3
-rw-r--r--src/theory/arith/nonlinear_extension.cpp939
-rw-r--r--src/theory/arith/nonlinear_extension.h59
-rw-r--r--test/regress/regress0/nl/Makefile.am15
-rw-r--r--test/regress/regress0/nl/nta/NAVIGATION2.smt223
-rw-r--r--test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt222
-rw-r--r--test/regress/regress0/nl/nta/exp-4.5-lt.smt29
-rw-r--r--test/regress/regress0/nl/nta/exp-n0.5-lb.smt210
-rw-r--r--test/regress/regress0/nl/nta/exp-n0.5-ub.smt210
-rw-r--r--test/regress/regress0/nl/nta/exp1-lb.smt210
-rw-r--r--test/regress/regress0/nl/nta/exp1-ub.smt211
-rw-r--r--test/regress/regress0/nl/nta/sin1-lb.smt210
-rw-r--r--test/regress/regress0/nl/nta/sin1-ub.smt210
-rw-r--r--test/regress/regress0/nl/nta/sin2-lb.smt210
-rw-r--r--test/regress/regress0/nl/nta/sin2-ub.smt210
15 files changed, 931 insertions, 220 deletions
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<Node>& 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<bool, Node> NonlinearExtension::isExtfReduced(
int effort, Node n, Node on, const std::vector<Node>& 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<bool, Node> NonlinearExtension::isExtfReduced(
Trace("nl-ext-zero-exp") << " exp[" << i << "] = " << exp[i]
<< std::endl;
std::vector<Node> 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<Node> 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<Rational>().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 <k1> b, a <k2> b, we know a <ret> 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Node>& 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<Rational>().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<Node> 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<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
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;
registerConstraint(atom);
bool is_false_lit = false_asserts.find(lit) != false_asserts.end();
// add information about bounds to variables
@@ -2211,19 +2268,20 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
Node exp = lit;
if (!polarity) {
// reverse
- if (type == kind::EQUAL) {
+ if (type == EQUAL)
+ {
// we will take the strict inequality in the direction of the
// model
Node lhs = QuantArith::mkCoeffTerm(coeff, x);
- Node query = NodeManager::currentNM()->mkNode(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<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
Trace("nl-ext-bound-debug2")
<< "Joining kinds : " << type << " " << its->second << 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<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
} else {
d_ci[x][coeff][rhs] = jk;
d_ci_exp[x][coeff][rhs] = NodeManager::currentNM()->mkNode(
- 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<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
bool needsRefine = false;
bool refineDir;
if (rhs_v == x_v) {
- if (type == kind::GT) {
+ if (type == GT)
+ {
needsRefine = true;
refineDir = true;
- } else if (type == kind::LT) {
+ }
+ else if (type == LT)
+ {
needsRefine = true;
refineDir = false;
}
} else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) {
- 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<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
Node null_coeff;
for (unsigned j = 0; j < d_mterms.size(); j++) {
Node n = d_mterms[j];
- d_ci[n][null_coeff][n] = kind::EQUAL;
+ d_ci[n][null_coeff][n] = EQUAL;
d_ci_exp[n][null_coeff][n] = d_true;
d_ci_max[n][null_coeff][n] = false;
}
@@ -2381,9 +2445,9 @@ std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
Kind infer_type =
mmv_sign == -1 ? reverseRelationKind(type) : type;
Node infer_lhs =
- NodeManager::currentNM()->mkNode(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<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node
<< std::endl;
if (infer_mv == d_false) {
Node exp = NodeManager::currentNM()->mkNode(
- 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<Node> NonlinearExtension::checkFactoring( const std::set<Node>& 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<Node, Node> msum;
if (QuantArith::getMonomialSumLit(atom, msum)) {
@@ -2470,7 +2534,7 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& 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<Node> NonlinearExtension::checkFactoring( const std::set<Node>& 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<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){
@@ -2501,7 +2566,9 @@ std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& 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<Node> NonlinearExtension::checkFactoring( const std::set<Node>& 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Node> NonlinearExtension::checkTranscendentalMonotonic() {
if( !tval.isNull() ){
Node mono_lem;
if( monotonic_dir==1 && sval.getConst<Rational>() > tval.getConst<Rational>() ){
- 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<Rational>() < tval.getConst<Rational>() ){
- 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<Node> NonlinearExtension::checkTranscendentalMonotonic() {
return lemmas;
}
+std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes()
+{
+ std::vector<Node> 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<const Kind, std::map<Node, Node> >& 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<Node> taylor_vars;
+ taylor_vars.push_back(d_taylor_real_fv);
+
+ // Figure 3: P_l, P_u
+ // mapped to for signs of c
+ std::map<int, Node> poly_approx_bounds[2];
+ 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;
+ // n must be even
+ std::pair<Node, Node> 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<const Node, Node>& 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<Rational>().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<Node, int, NodeHashFunction>::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<unsigned, Node> model_values;
+ for (unsigned d = 0; d < 2; d++)
+ {
+ Node pab = poly_approx_bounds[d][csign];
+ if (!pab.isNull())
+ {
+ // { x -> tf[0] }
+ std::vector<Node> 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<Node> 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<Node> 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<Node> 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<Node> 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<Rational>();
+ 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<Node> 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<Node> 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<Node, Node> 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<Node, Node> 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<Node, Node> 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<Node, Node> 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<Node, Node> 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<Node> 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<Node> 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback