diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:19 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 16:22:26 -0500 |
commit | 2c0482cfb9b8164670cf56187e127d38c5d05bcf (patch) | |
tree | 804f7806944b9175fdaea8cc919566ca302ddf09 /src/theory/arith | |
parent | 0e513c05b2e0ae3b8e2d08514ccb8007258f963b (diff) |
Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 135 | ||||
-rw-r--r-- | src/theory/arith/arith_rewriter.h | 4 | ||||
-rw-r--r-- | src/theory/arith/congruence_manager.cpp | 2 | ||||
-rw-r--r-- | src/theory/arith/kinds | 14 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 2100 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 78 | ||||
-rw-r--r-- | src/theory/arith/normal_form.cpp | 13 | ||||
-rw-r--r-- | src/theory/arith/normal_form.h | 7 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 5 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 15 | ||||
-rw-r--r-- | src/theory/arith/theory_arith_type_rules.h | 33 |
11 files changed, 1634 insertions, 772 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 4684ec4a3..57428d209 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -101,7 +101,12 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return preRewritePlus(t); case kind::MULT: case kind::NONLINEAR_MULT: - return preRewriteMult(t); + return preRewriteMult(t); + case kind::EXPONENTIAL: + case kind::SINE: + case kind::COSINE: + case kind::TANGENT: + return preRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); @@ -126,6 +131,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ return RewriteResponse(REWRITE_DONE, t[0]); case kind::POW: return RewriteResponse(REWRITE_DONE, t); + case kind::PI: + return RewriteResponse(REWRITE_DONE, t); default: Unhandled(k); } @@ -150,7 +157,12 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ return postRewritePlus(t); case kind::MULT: case kind::NONLINEAR_MULT: - return postRewriteMult(t); + return postRewriteMult(t); + case kind::EXPONENTIAL: + case kind::SINE: + case kind::COSINE: + case kind::TANGENT: + return postRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); @@ -197,15 +209,21 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ if(exp.sgn() == 0){ return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1))); }else if(exp.sgn() > 0 && exp.isIntegral()){ - Integer num = exp.getNumerator(); - NodeBuilder<> nb(kind::MULT); - Integer one(1); - for(Integer i(0); i < num; i = i + one){ - nb << base; + CVC4::Rational r(INT_MAX); + if( exp<r ){ + unsigned num = exp.getNumerator().toUnsignedInt(); + if( num==1 ){ + return RewriteResponse(REWRITE_AGAIN, base); + }else{ + NodeBuilder<> nb(kind::MULT); + for(unsigned i=0; i < num; ++i){ + nb << base; + } + Assert(nb.getNumChildren() > 0); + Node mult = nb; + return RewriteResponse(REWRITE_AGAIN, mult); + } } - Assert(nb.getNumChildren() > 0); - Node mult = nb; - return RewriteResponse(REWRITE_AGAIN, mult); } } @@ -216,6 +234,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ ss << " " << t; throw LogicException(ss.str()); } + case kind::PI: + return RewriteResponse(REWRITE_DONE, t); default: Unreachable(); } @@ -332,6 +352,100 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){ return RewriteResponse(REWRITE_DONE, res.getNode()); } + +RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t) { + return RewriteResponse(REWRITE_DONE, t); +} + +RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) { + Trace("arith-tf-rewrite") << "Rewrite transcendental function : " << t << std::endl; + switch( t.getKind() ){ + case kind::EXPONENTIAL: { + if(t[0].getKind() == kind::CONST_RATIONAL){ + Node one = NodeManager::currentNM()->mkConst(Rational(1)); + if(t[0].getConst<Rational>().sgn()>=0 && t[0].getType().isInteger() && t[0]!=one){ + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::POW, NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, one ), t[0])); + }else{ + return RewriteResponse(REWRITE_DONE, t); + } + }else if(t[0].getKind() == kind::PLUS ){ + std::vector<Node> product; + for( unsigned i=0; i<t[0].getNumChildren(); i++ ){ + product.push_back( NodeManager::currentNM()->mkNode( kind::EXPONENTIAL, t[0][i] ) ); + } + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkNode(kind::MULT, product)); + } + } + break; + case kind::SINE: + if(t[0].getKind() == kind::CONST_RATIONAL){ + const Rational& rat = t[0].getConst<Rational>(); + if(rat.sgn() == 0){ + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(0))); + } + }else{ + Node pi_factor; + Node pi; + if( t[0].getKind()==kind::PI ){ + pi_factor = NodeManager::currentNM()->mkConst(Rational(1)); + pi = t[0]; + }else if( t[0].getKind()==kind::MULT && t[0][0].isConst() && t[0][1].getKind()==kind::PI ){ + pi_factor = t[0][0]; + pi = t[0][1]; + } + if( !pi_factor.isNull() ){ + Trace("arith-tf-rewrite-debug") << "Process pi factor = " << pi_factor << std::endl; + Rational r = pi_factor.getConst<Rational>(); + Rational ra = r.abs(); + Rational rone = Rational(1); + Node ntwo = NodeManager::currentNM()->mkConst( Rational(2) ); + if( ra > rone ){ + //add/substract 2*pi beyond scope + Node ra_div_two = NodeManager::currentNM()->mkNode( kind::INTS_DIVISION, NodeManager::currentNM()->mkConst( ra + rone ), ntwo ); + Node new_pi_factor; + if( r.sgn()==1 ){ + new_pi_factor = NodeManager::currentNM()->mkNode( kind::MINUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) ); + }else{ + Assert( r.sgn()==-1 ); + new_pi_factor = NodeManager::currentNM()->mkNode( kind::PLUS, pi_factor, NodeManager::currentNM()->mkNode( kind::MULT, ntwo, ra_div_two ) ); + } + return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode( kind::SINE, + NodeManager::currentNM()->mkNode( kind::MULT, new_pi_factor, pi ) ) ); + }else if( ra == rone ){ + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(Rational(0))); + }else{ + Integer one = Integer(1); + Integer two = Integer(2); + Integer six = Integer(6); + if( ra.getDenominator()==two ){ + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst( Rational( r.sgn() ) ) ); + }else if( ra.getDenominator()==six ){ + Integer five = Integer(5); + if( ra.getNumerator()==one || ra.getNumerator()==five ){ + return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst( Rational( r.sgn() )/Rational(2) ) ); + } + } + } + } + } + break; + case kind::COSINE: { + return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode( kind::SINE, + NodeManager::currentNM()->mkNode( kind::MINUS, + NodeManager::currentNM()->mkNode( kind::MULT, + NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ), + NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI ) ), + t[0] ) ) ); + } break; + case kind::TANGENT: + return RewriteResponse(REWRITE_AGAIN_FULL, NodeManager::currentNM()->mkNode(kind::DIVISION, NodeManager::currentNM()->mkNode( kind::SINE, t[0] ), + NodeManager::currentNM()->mkNode( kind::COSINE, t[0] ) )); + default: + break; + } + return RewriteResponse(REWRITE_DONE, t); +} + RewriteResponse ArithRewriter::postRewriteAtom(TNode atom){ if(atom.getKind() == kind::IS_INTEGER) { if(atom[0].isConst()) { @@ -440,7 +554,6 @@ Node ArithRewriter::makeSubtractionNode(TNode l, TNode r){ RewriteResponse ArithRewriter::rewriteDiv(TNode t, bool pre){ Assert(t.getKind() == kind::DIVISION_TOTAL || t.getKind()== kind::DIVISION); - Node left = t[0]; Node right = t[1]; if(right.getKind() == kind::CONST_RATIONAL){ diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h index 38b6c9451..a4472d6c3 100644 --- a/src/theory/arith/arith_rewriter.h +++ b/src/theory/arith/arith_rewriter.h @@ -57,7 +57,9 @@ private: static RewriteResponse preRewriteMult(TNode t); static RewriteResponse postRewriteMult(TNode t); - + + static RewriteResponse preRewriteTranscendental(TNode t); + static RewriteResponse postRewriteTranscendental(TNode t); static RewriteResponse preRewriteAtom(TNode t); static RewriteResponse postRewriteAtom(TNode t); diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 04d8d50ea..f6e702f5b 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -43,6 +43,8 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true) { d_ee.addFunctionKind(kind::NONLINEAR_MULT); + d_ee.addFunctionKind(kind::EXPONENTIAL); + d_ee.addFunctionKind(kind::SINE); //module to infer additional equalities based on normalization if( options::sNormInferEq() ){ d_eq_infer = new quantifiers::EqualityInference(c, true); diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index 61029ac48..0884083c0 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -27,6 +27,11 @@ operator ABS 1 "absolute value" parameterized DIVISIBLE DIVISIBLE_OP 1 "divisibility-by-k predicate; first parameter is a DIVISIBLE_OP, second is integer term" operator POW 2 "arithmetic power" +operator EXPONENTIAL 1 "exponential" +operator SINE 1 "sine" +operator COSINE 1 "consine" +operator TANGENT 1 "tangent" + constant DIVISIBLE_OP \ ::CVC4::Divisible \ ::CVC4::DivisibleHashFunction \ @@ -112,4 +117,13 @@ typerule DIVISION_TOTAL ::CVC4::theory::arith::ArithOperatorTypeRule typerule INTS_DIVISION_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule typerule INTS_MODULUS_TOTAL ::CVC4::theory::arith::IntOperatorTypeRule +typerule EXPONENTIAL ::CVC4::theory::arith::RealOperatorTypeRule +typerule SINE ::CVC4::theory::arith::RealOperatorTypeRule +typerule COSINE ::CVC4::theory::arith::RealOperatorTypeRule +typerule TANGENT ::CVC4::theory::arith::RealOperatorTypeRule + +nullaryoperator PI "pi" + +typerule PI ::CVC4::theory::arith::RealNullaryOperatorTypeRule + endtheory diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 02266f331..42f9636dc 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -217,6 +217,7 @@ NonlinearExtension::NonlinearExtension(TheoryArith& containing, eq::EqualityEngine* ee) : d_lemmas(containing.getUserContext()), d_zero_split(containing.getUserContext()), + d_skolem_atoms(containing.getUserContext()), d_containing(containing), d_ee(ee), d_needsLastCall(false) { @@ -235,7 +236,7 @@ NonlinearExtension::~NonlinearExtension() {} // Returns a reference to either map[key] if it exists in the map // or to a default value otherwise. // -// Warning: special care must be taken if value is a temporary object. +// Warning: sped_cial care must be taken if value is a temporary object. template <class MapType, class Key, class Value> const Value& FindWithDefault(const MapType& map, const Key& key, const Value& value) { @@ -699,49 +700,58 @@ Node NonlinearExtension::computeModelValue(Node n, unsigned index) { if (it != d_mv[index].end()) { return it->second; } else { - Trace("nl-ext-debug") << "computeModelValue " << n << std::endl; + Trace("nl-ext-mv-debug") << "computeModelValue " << n << ", index=" << index << std::endl; Node ret; if (n.isConst()) { ret = n; - } else { - if (n.getNumChildren() == 0) { - ret = d_containing.getValuation().getModel()->getValue(n); + } else if (index == 1 && ( n.getKind() == kind::NONLINEAR_MULT || isTranscendentalKind( n.getKind() ) )) { + if (d_containing.getValuation().getModel()->hasTerm(n)) { + // use model value for abstraction + ret = d_containing.getValuation().getModel()->getRepresentative(n); } else { - if (index == 1 && n.getKind() == kind::NONLINEAR_MULT) { - if (d_containing.getValuation().getModel()->hasTerm(n)) { - // use model value for abstraction - ret = d_containing.getValuation().getModel()->getRepresentative(n); - } else { - // abstraction does not exist, use concrete - ret = computeModelValue(n, 0); - } - } else { - // otherwise, compute true value - std::vector<Node> children; - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { - children.push_back(n.getOperator()); - } - for (unsigned i = 0; i < n.getNumChildren(); i++) { - Node mc = computeModelValue(n[i], index); - children.push_back(mc); - } - ret = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(n.getKind(), children)); - if (!ret.isConst()) { - Trace("nl-ext-debug") << "...got non-constant : " << ret << " for " - << n << ", ask model directly." << std::endl; - ret = d_containing.getValuation().getModel()->getValue(ret); - } - } + // abstraction does not exist, use model value + //ret = computeModelValue(n, 0); + ret = d_containing.getValuation().getModel()->getValue(n); } - if (ret.getType().isReal() && !isArithKind(n.getKind())) { - // Trace("nl-ext-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n - // << " ] -> " << ret << std::endl; - Assert(ret.isConst()); + //Assert( ret.isConst() ); + } else if (n.getNumChildren() == 0) { + if( n.getKind()==kind::PI ){ + ret = n; + }else{ + ret = d_containing.getValuation().getModel()->getValue(n); + } + } else { + // otherwise, compute true value + std::vector<Node> children; + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + children.push_back(n.getOperator()); + } + for (unsigned i = 0; i < n.getNumChildren(); i++) { + Node mc = computeModelValue(n[i], index); + children.push_back(mc); + } + ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + if( n.getKind()==kind::APPLY_UF ){ + ret = d_containing.getValuation().getModel()->getValue(ret); + }else{ + ret = Rewriter::rewrite(ret); + } + /* + if (!ret.isConst()) { + Trace("nl-ext-debug") << "...got non-constant : " << ret << " for " + << n << ", ask model directly." << std::endl; + ret = d_containing.getValuation().getModel()->getValue(ret); } + */ } - Trace("nl-ext-debug") << "computed " << (index == 0 ? "M" : "M_A") << "[" - << n << "] = " << ret << std::endl; + //if (ret.getType().isReal() && !isArithKind(n.getKind())) { + // Trace("nl-ext-mv-debug") << ( index==0 ? "M" : "M_A" ) << "[ " << n + // << " ] -> " << ret << std::endl; + //may involve transcendental functions + //Assert(ret.isConst()); + //} + Trace("nl-ext-mv-debug") << "computed " << (index == 0 ? "M" : "M_A") << "[" + << n << "] = " << ret << std::endl; d_mv[index][n] = ret; return ret; } @@ -898,6 +908,16 @@ Node NonlinearExtension::mkAbs(Node a) { } } +Node NonlinearExtension::mkValidPhase(Node a, Node pi) { + return mkBounded( NodeManager::currentNM()->mkNode( kind::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 ) ); +} + // by a <k1> b, a <k2> b, we know a <ret> b Kind NonlinearExtension::joinKinds(Kind k1, Kind k2) { if (k2 < k1) { @@ -956,6 +976,11 @@ 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; +} + Node NonlinearExtension::mkMonomialRemFactor( Node n, const NodeMultiset& n_exp_rem) const { std::vector<Node> children; @@ -1033,27 +1058,26 @@ std::set<Node> NonlinearExtension::getFalseInModel( std::set<Node> false_asserts; for (size_t i = 0; i < assertions.size(); ++i) { Node lit = assertions[i]; - Node litv = computeModelValue(lit); - Trace("nl-ext-mv") << "M[[ " << lit << " ]] -> " << litv; - if (litv != d_true) { - Trace("nl-ext-mv") << " [model-false]" << std::endl; - Assert(litv == d_false); - false_asserts.insert(lit); - } else { - Trace("nl-ext-mv") << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + if( d_skolem_atoms.find( atom )==d_skolem_atoms.end() ){ + Node litv = computeModelValue(lit); + Trace("nl-ext-mv") << "M[[ " << lit << " ]] -> " << litv; + if (litv != d_true) { + Trace("nl-ext-mv") << " [model-false]" << std::endl; + //Assert(litv == d_false); + false_asserts.insert(lit); + } else { + Trace("nl-ext-mv") << std::endl; + } } } return false_asserts; } -std::vector<Node> NonlinearExtension::splitOnZeros( - const std::vector<Node>& ms_vars) { +std::vector<Node> NonlinearExtension::checkSplitZero() { std::vector<Node> lemmas; - if (!options::nlExtSplitZero()) { - return lemmas; - } - for (unsigned i = 0; i < ms_vars.size(); i++) { - Node v = ms_vars[i]; + for (unsigned i = 0; i < d_ms_vars.size(); i++) { + Node v = d_ms_vars[i]; if (d_zero_split.insert(v)) { Node lem = v.eqNode(d_zero); lem = Rewriter::rewrite(lem); @@ -1067,50 +1091,123 @@ std::vector<Node> NonlinearExtension::splitOnZeros( } void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, - const std::set<Node>& false_asserts) { - // processed monomials - std::map<Node, bool> ms_proc; - - // list of monomials - std::vector<Node> ms; - d_containing.getExtTheory()->getTerms(ms); - // list of variables occurring in monomials - std::vector<Node> ms_vars; - - // register monomials - Trace("nl-ext-mv") << "Monomials : " << std::endl; - for (unsigned j = 0; j < ms.size(); j++) { - Node a = ms[j]; - registerMonomial(a); + const std::set<Node>& false_asserts, + const std::vector<Node>& xts) { + d_ms_vars.clear(); + d_ms_proc.clear(); + d_ms.clear(); + d_mterms.clear(); + d_m_nconst_factor.clear(); + d_tplane_refine_dir.clear(); + d_ci.clear(); + d_ci_exp.clear(); + d_ci_max.clear(); + d_tf_rep_map.clear(); + + int lemmas_proc = 0; + std::vector<Node> lemmas; + + Trace("nl-ext-mv") << "Extended terms : " << std::endl; + // register the extended function terms + std::map< Node, Node > mvarg_to_term; + for( unsigned i=0; i<xts.size(); i++ ){ + Node a = xts[i]; computeModelValue(a, 0); computeModelValue(a, 1); - Assert(d_mv[1][a].isConst()); - Assert(d_mv[0][a].isConst()); - Trace("nl-ext-mv") << " " << a << " -> " << d_mv[1][a] << " [" - << d_mv[0][a] << "]" << std::endl; - - std::map<Node, std::vector<Node> >::iterator itvl = d_m_vlist.find(a); - Assert(itvl != d_m_vlist.end()); - for (unsigned k = 0; k < itvl->second.size(); k++) { - if (!IsInVector(ms_vars, itvl->second[k])) { - ms_vars.push_back(itvl->second[k]); + Trace("nl-ext-mv") << " " << a << " -> " << d_mv[1][a] << " [actual: " + << d_mv[0][a] << " ]" << std::endl; + //Assert(d_mv[1][a].isConst()); + //Assert(d_mv[0][a].isConst()); + + if( a.getKind()==kind::NONLINEAR_MULT ){ + d_ms.push_back( a ); + + //context-independent registration + registerMonomial(a); + + std::map<Node, std::vector<Node> >::iterator itvl = d_m_vlist.find(a); + Assert(itvl != d_m_vlist.end()); + for (unsigned k = 0; k < itvl->second.size(); k++) { + if (!IsInVector(d_ms_vars, itvl->second[k])) { + d_ms_vars.push_back(itvl->second[k]); + } + Node mvk = computeModelValue( itvl->second[k], 1 ); + if( !mvk.isConst() ){ + d_m_nconst_factor[a] = true; + } } - } - /* - //mark processed if has a "one" factor (will look at reduced monomial) - std::map< Node, std::map< Node, unsigned > >::iterator itme = - d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node, - unsigned >::iterator itme2 = itme->second.begin(); itme2 != - itme->second.end(); ++itme2 ){ Node v = itme->first; Assert( - d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if( - mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true; - Trace("nl-ext-mv") - << "...mark " << a << " reduced since has 1 factor." << std::endl; - break; + /* + //mark processed if has a "one" factor (will look at reduced monomial) + std::map< Node, std::map< Node, unsigned > >::iterator itme = + d_m_exp.find( a ); Assert( itme!=d_m_exp.end() ); for( std::map< Node, + unsigned >::iterator itme2 = itme->second.begin(); itme2 != + itme->second.end(); ++itme2 ){ Node v = itme->first; Assert( + d_mv[0].find( v )!=d_mv[0].end() ); Node mvv = d_mv[0][ v ]; if( + mvv==d_one || mvv==d_neg_one ){ ms_proc[ a ] = true; + Trace("nl-ext-mv") + << "...mark " << a << " reduced since has 1 factor." << std::endl; + break; + } + } + */ + }else if( a.getNumChildren()==1 ){ + bool consider = true; + // get shifted version + if( a.getKind()==kind::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() ){ + Node y = NodeManager::currentNM()->mkSkolem("y",NodeManager::currentNM()->realType(),"phase shifted trigonometric arg"); + Node new_a = NodeManager::currentNM()->mkNode( a.getKind(), y ); + d_trig_is_base[new_a] = true; + d_trig_base[a] = new_a; + Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a << std::endl; + if( d_pi.isNull() ){ + mkPi(); + getCurrentPiBounds( lemmas ); + } + Node shift = NodeManager::currentNM()->mkSkolem( "s", NodeManager::currentNM()->integerType(), "number of shifts" ); + 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 ) ); + //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); + lemmas_proc++; + } + } } + if( consider ){ + Node r = d_containing.getValuation().getModel()->getRepresentative(a[0]); + std::map< Node, Node >::iterator itrm = d_tf_rep_map[a.getKind()].find( r ); + if( itrm!=d_tf_rep_map[a.getKind()].end() ){ + //verify they have the same model value + if( d_mv[1][a]!=d_mv[1][itrm->second] ){ + //congruence lemma + Node cong_lemma = NodeManager::currentNM()->mkNode( kind::IMPLIES, a[0].eqNode( itrm->second[0] ), a.eqNode( itrm->second ) ); + lemmas.push_back( cong_lemma ); + //Assert( false ); + } + }else{ + d_tf_rep_map[a.getKind()][r] = a; + } + } + }else if( a.getKind()==kind::PI ){ + //TODO? + }else{ + Assert( false ); } - */ } + + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas during registration." << std::endl; + return; + } + // register constants registerMonomial(d_one); @@ -1120,471 +1217,92 @@ void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, computeModelValue(c, 1); } - int lemmas_proc; - std::vector<Node> lemmas; - // register variables - Trace("nl-ext-mv") << "Variables : " << std::endl; - Trace("nl-ext") << "Get zero split lemmas..." << std::endl; - for (unsigned i = 0; i < ms_vars.size(); i++) { - Node v = ms_vars[i]; + Trace("nl-ext-mv") << "Variables in monomials : " << std::endl; + for (unsigned i = 0; i < d_ms_vars.size(); i++) { + Node v = d_ms_vars[i]; registerMonomial(v); computeModelValue(v, 0); computeModelValue(v, 1); - Trace("nl-ext-mv") << " " << v << " -> " << d_mv[0][v] << std::endl; + Trace("nl-ext-mv") << " " << v << " -> " << d_mv[1][v] << " [actual: " << d_mv[0][v] << " ]" << std::endl; } - // possibly split on zero? - lemmas = splitOnZeros(ms_vars); + //----------------------------------- possibly split on zero + if (options::nlExtSplitZero()) { + Trace("nl-ext") << "Get zero split lemmas..." << std::endl; + lemmas = checkSplitZero(); + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; + return; + } + } + + //-----------------------------------initial lemmas for transcendental functions + lemmas = checkTranscendentalInitialRefine(); lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." - << std::endl; + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } - + //-----------------------------------lemmas based on sign (comparison to zero) - std::map<Node, int> signs; - Trace("nl-ext") << "Get sign lemmas..." << std::endl; - for (unsigned j = 0; j < ms.size(); j++) { - Node a = ms[j]; - if (ms_proc.find(a) == ms_proc.end()) { - std::vector<Node> exp; - Trace("nl-ext-debug") << " process " << a << "..." << std::endl; - signs[a] = compareSign(a, a, 0, 1, exp, lemmas); - if (signs[a] == 0) { - ms_proc[a] = true; - Trace("nl-ext-mv") << "...mark " << a - << " reduced since its value is 0." << std::endl; - } - } + lemmas = checkMonomialSign(); + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; + return; } + + //-----------------------------------monotonicity of transdental functions + lemmas = checkTranscendentalMonotonic(); lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." - << std::endl; + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } - //-----------------------------lemmas based on magnitude of non-zero monomials - for (unsigned r = 1; r <= 1; r++) { - assignOrderIds(ms_vars, d_order_vars[r], r); - - // sort individual variable lists - SortNonlinearExtension smv; - smv.d_nla = this; - smv.d_order_type = r; - smv.d_reverse_order = true; - for (unsigned j = 0; j < ms.size(); j++) { - std::sort(d_m_vlist[ms[j]].begin(), d_m_vlist[ms[j]].end(), smv); - } - for (unsigned c = 0; c < 3; c++) { - // if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L - // in lemmas - std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers; - Trace("nl-ext") << "Get comparison lemmas (order=" << r - << ", compare=" << c << ")..." << std::endl; - for (unsigned j = 0; j < ms.size(); j++) { - Node a = ms[j]; - if (ms_proc.find(a) == ms_proc.end()) { - if (c == 0) { - // compare magnitude against 1 - std::vector<Node> exp; - NodeMultiset a_exp_proc; - NodeMultiset b_exp_proc; - compareMonomial(a, a, a_exp_proc, d_one, d_one, b_exp_proc, exp, - lemmas, cmp_infers); - } else { - std::map<Node, NodeMultiset>::iterator itmea = d_m_exp.find(a); - Assert(itmea != d_m_exp.end()); - if (c == 1) { - // TODO : not just against containing variables? - // compare magnitude against variables - for (unsigned k = 0; k < ms_vars.size(); k++) { - Node v = ms_vars[k]; - std::vector<Node> exp; - NodeMultiset a_exp_proc; - NodeMultiset b_exp_proc; - if (itmea->second.find(v) != itmea->second.end()) { - a_exp_proc[v] = 1; - b_exp_proc[v] = 1; - setMonomialFactor(a, v, a_exp_proc); - setMonomialFactor(v, a, b_exp_proc); - compareMonomial(a, a, a_exp_proc, v, v, b_exp_proc, exp, - lemmas, cmp_infers); - } - } - } else { - // compare magnitude against other non-linear monomials - for (unsigned k = (j + 1); k < ms.size(); k++) { - Node b = ms[k]; - //(signs[a]==signs[b])==(r==0) - if (ms_proc.find(b) == ms_proc.end()) { - std::map<Node, NodeMultiset>::iterator itmeb = - d_m_exp.find(b); - Assert(itmeb != d_m_exp.end()); - - std::vector<Node> exp; - // take common factors of monomials, set minimum of - // common exponents as processed - NodeMultiset a_exp_proc; - NodeMultiset b_exp_proc; - for (NodeMultiset::iterator itmea2 = itmea->second.begin(); - itmea2 != itmea->second.end(); ++itmea2) { - NodeMultiset::iterator itmeb2 = - itmeb->second.find(itmea2->first); - if (itmeb2 != itmeb->second.end()) { - unsigned min_exp = itmea2->second > itmeb2->second - ? itmeb2->second - : itmea2->second; - a_exp_proc[itmea2->first] = min_exp; - b_exp_proc[itmea2->first] = min_exp; - Trace("nl-ext-comp") - << "Common exponent : " << itmea2->first << " : " - << min_exp << std::endl; - } - } - if (!a_exp_proc.empty()) { - setMonomialFactor(a, b, a_exp_proc); - setMonomialFactor(b, a, b_exp_proc); - } - /* - if( !a_exp_proc.empty() ){ - //reduction based on common exponents a > 0 => ( a * b - <> a * c <=> b <> c ), a < 0 => ( a * b <> a * c <=> b - !<> c ) ? }else{ compareMonomial( a, a, a_exp_proc, b, - b, b_exp_proc, exp, lemmas ); - } - */ - compareMonomial(a, a, a_exp_proc, b, b, b_exp_proc, exp, - lemmas, cmp_infers); - } - } - } - } - } - } - // remove redundant lemmas, e.g. if a > b, b > c, a > c were - // inferred, discard lemma with conclusion a > c - Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size() - << " lemmas." << std::endl; - // naive - std::vector<Node> r_lemmas; - for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb = - cmp_infers.begin(); - itb != cmp_infers.end(); ++itb) { - for (std::map<Node, std::map<Node, Node> >::iterator itc = - itb->second.begin(); - itc != itb->second.end(); ++itc) { - for (std::map<Node, Node>::iterator itc2 = itc->second.begin(); - itc2 != itc->second.end(); ++itc2) { - std::map<Node, bool> visited; - for (std::map<Node, Node>::iterator itc3 = itc->second.begin(); - itc3 != itc->second.end(); ++itc3) { - if (itc3->first != itc2->first) { - std::vector<Node> exp; - if (cmp_holds(itc3->first, itc2->first, itb->second, exp, - visited)) { - r_lemmas.push_back(itc2->second); - Trace("nl-ext-comp") - << "...inference of " << itc->first << " > " - << itc2->first << " was redundant." << std::endl; - break; - } - } - } - } - } - } - std::vector<Node> nr_lemmas; - for (unsigned i = 0; i < lemmas.size(); i++) { - if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i]) == - r_lemmas.end()) { - nr_lemmas.push_back(lemmas[i]); - } - } - // TODO: only take maximal lower/minimial lower bounds? + //-----------------------------------lemmas based on magnitude of non-zero monomials + Trace("nl-ext-proc") << "Assign order ids..." << std::endl; + unsigned r = 3; + assignOrderIds(d_ms_vars, d_order_vars, r); - Trace("nl-ext-comp") << nr_lemmas.size() << " / " << lemmas.size() - << " were non-redundant." << std::endl; - lemmas_proc = flushLemmas(nr_lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc - << " new lemmas (out of possible " << lemmas.size() - << ")." << std::endl; - return; - } + // sort individual variable lists + Trace("nl-ext-proc") << "Assign order var lists..." << std::endl; + SortNonlinearExtension smv; + smv.d_nla = this; + smv.d_order_type = r; + smv.d_reverse_order = true; + for (unsigned j = 0; j < d_ms.size(); j++) { + std::sort(d_m_vlist[d_ms[j]].begin(), d_m_vlist[d_ms[j]].end(), smv); + } + for (unsigned c = 0; c < 3; c++) { + // c is effort level + lemmas = checkMonomialMagnitude( c ); + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-ext") << " ...finished with " << lemmas_proc + << " new lemmas (out of possible " << lemmas.size() + << ")." << std::endl; + return; } } // sort monomials by degree + Trace("nl-ext-proc") << "Sort monomials by degree..." << std::endl; SortNonlinearExtension snlad; snlad.d_nla = this; snlad.d_order_type = 4; snlad.d_reverse_order = false; - std::sort(ms.begin(), ms.end(), snlad); + std::sort(d_ms.begin(), d_ms.end(), snlad); // all monomials - std::vector<Node> terms; - terms.insert(terms.end(), ms_vars.begin(), ms_vars.end()); - terms.insert(terms.end(), ms.begin(), ms.end()); - - // term -> coeff -> rhs -> ( status, exp, b ), - // where we have that : exp => ( coeff * term <status> rhs ) - // b is true if degree( term ) >= degree( rhs ) - std::map<Node, std::map<Node, std::map<Node, Kind> > > ci; - std::map<Node, std::map<Node, std::map<Node, Node> > > ci_exp; - std::map<Node, std::map<Node, std::map<Node, bool> > > ci_max; - - // If ( m, p1, true ), then it would help satisfiability if m were ( > - // if p1=true, < if p1=false ) - std::map<Node, std::map<bool, bool> > tplane_refine_dir; - - // register constraints - Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; - for (context::CDList<Assertion>::const_iterator it = - 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; - registerConstraint(atom); - bool is_false_lit = false_asserts.find(lit) != false_asserts.end(); - // add information about bounds to variables - std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc = - d_c_info.find(atom); - std::map<Node, std::map<Node, bool> >::iterator itcm = - d_c_info_maxm.find(atom); - if (itc != d_c_info.end()) { - Assert(itcm != d_c_info_maxm.end()); - for (std::map<Node, ConstraintInfo>::iterator itcc = itc->second.begin(); - itcc != itc->second.end(); ++itcc) { - Node x = itcc->first; - Node coeff = itcc->second.d_coeff; - Node rhs = itcc->second.d_rhs; - Kind type = itcc->second.d_type; - Node exp = lit; - if (!polarity) { - // reverse - if (type == kind::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_mv = computeModelValue(query, 1); - if (query_mv == d_true) { - exp = query; - type = kind::GT; - } else { - Assert(query_mv == d_false); - exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs); - type = kind::LT; - } - } else { - type = negateKind(type); - } - } - // add to status if maximal degree - ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end(); - if (Trace.isOn("nl-ext-bound-debug2")) { - Node t = QuantArith::mkCoeffTerm(coeff, x); - Trace("nl-ext-bound-debug2") - << "Add Bound: " << t << " " << type << " " << rhs << " by " - << exp << std::endl; - } - bool updated = true; - std::map<Node, Kind>::iterator its = ci[x][coeff].find(rhs); - if (its == ci[x][coeff].end()) { - ci[x][coeff][rhs] = type; - ci_exp[x][coeff][rhs] = exp; - } else if (type != its->second) { - Trace("nl-ext-bound-debug2") - << "Joining kinds : " << type << " " << its->second << std::endl; - Kind jk = joinKinds(type, its->second); - if (jk == kind::UNDEFINED_KIND) { - updated = false; - } else if (jk != its->second) { - if (jk == type) { - ci[x][coeff][rhs] = type; - ci_exp[x][coeff][rhs] = exp; - } else { - ci[x][coeff][rhs] = jk; - ci_exp[x][coeff][rhs] = NodeManager::currentNM()->mkNode( - kind::AND, ci_exp[x][coeff][rhs], exp); - } - } else { - updated = false; - } - } - if (Trace.isOn("nl-ext-bound")) { - if (updated) { - Trace("nl-ext-bound") << "Bound: "; - debugPrintBound("nl-ext-bound", coeff, x, ci[x][coeff][rhs], rhs); - Trace("nl-ext-bound") << " by " << ci_exp[x][coeff][rhs]; - if (ci_max[x][coeff][rhs]) { - Trace("nl-ext-bound") << ", is max degree"; - } - Trace("nl-ext-bound") << std::endl; - } - } - // compute if bound is not satisfied, and store what is required - // for a possible refinement - if (options::nlExtTangentPlanes()) { - if (is_false_lit) { - Node rhs_v = computeModelValue(rhs, 0); - Node x_v = computeModelValue(x, 0); - bool needsRefine = false; - bool refineDir; - if (rhs_v == x_v) { - if (type == kind::GT) { - needsRefine = true; - refineDir = true; - } else if (type == kind::LT) { - needsRefine = true; - refineDir = false; - } - } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) { - if (type != kind::GT && type != kind::GEQ) { - needsRefine = true; - refineDir = false; - } - } else { - if (type != kind::LT && type != kind::LEQ) { - needsRefine = true; - refineDir = true; - } - } - Trace("nl-ext-tplanes-cons-debug") - << "...compute if bound corresponds to a required " - "refinement" - << std::endl; - Trace("nl-ext-tplanes-cons-debug") - << "...M[" << x << "] = " << x_v << ", M[" << rhs - << "] = " << rhs_v << std::endl; - Trace("nl-ext-tplanes-cons-debug") << "...refine = " << needsRefine - << "/" << refineDir << std::endl; - if (needsRefine) { - Trace("nl-ext-tplanes-cons") - << "---> By " << lit << " and since M[" << x << "] = " << x_v - << ", M[" << rhs << "] = " << rhs_v << ", "; - Trace("nl-ext-tplanes-cons") - << "monomial " << x << " should be " - << (refineDir ? "larger" : "smaller") << std::endl; - tplane_refine_dir[x][refineDir] = true; - } - } - } - } - } - } - // reflexive constraints - Node null_coeff; - for (unsigned j = 0; j < terms.size(); j++) { - Node n = terms[j]; - ci[n][null_coeff][n] = kind::EQUAL; - ci_exp[n][null_coeff][n] = d_true; - ci_max[n][null_coeff][n] = false; - } + d_mterms.insert(d_mterms.end(), d_ms_vars.begin(), d_ms_vars.end()); + d_mterms.insert(d_mterms.end(), d_ms.begin(), d_ms.end()); - //-----------------------------------------------------------------------------------------inferred - // bounds lemmas, e.g. x >= t => y*x >= y*t - Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl; - - std::vector<Node> nt_lemmas; - for (unsigned k = 0; k < terms.size(); k++) { - Node x = terms[k]; - Trace("nl-ext-bound-debug") - << "Process bounds for " << x << " : " << std::endl; - std::map<Node, std::vector<Node> >::iterator itm = - d_m_contain_parent.find(x); - if (itm != d_m_contain_parent.end()) { - Trace("nl-ext-bound-debug") << "...has " << itm->second.size() - << " parent monomials." << std::endl; - // check derived bounds - std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc = - ci.find(x); - if (itc != ci.end()) { - for (std::map<Node, std::map<Node, Kind> >::iterator itcc = - itc->second.begin(); - itcc != itc->second.end(); ++itcc) { - Node coeff = itcc->first; - Node t = QuantArith::mkCoeffTerm(coeff, x); - for (std::map<Node, Kind>::iterator itcr = itcc->second.begin(); - itcr != itcc->second.end(); ++itcr) { - Node rhs = itcr->first; - // only consider this bound if maximal degree - if (ci_max[x][coeff][rhs]) { - Kind type = itcr->second; - for (unsigned j = 0; j < itm->second.size(); j++) { - Node y = itm->second[j]; - Assert(d_m_contain_mult[x].find(y) != - d_m_contain_mult[x].end()); - Node mult = d_m_contain_mult[x][y]; - // x <k> t => m*x <k'> t where y = m*x - // get the sign of mult - Node mmv = computeModelValue(mult); - Trace("nl-ext-bound-debug2") - << "Model value of " << mult << " is " << mmv << std::endl; - Assert(mmv.isConst()); - int mmv_sign = mmv.getConst<Rational>().sgn(); - Trace("nl-ext-bound-debug2") - << " sign of " << mmv << " is " << mmv_sign << std::endl; - if (mmv_sign != 0) { - Trace("nl-ext-bound-debug") - << " from " << x << " * " << mult << " = " << y - << " and " << t << " " << type << " " << rhs - << ", infer : " << std::endl; - Kind infer_type = - mmv_sign == -1 ? reverseRelationKind(type) : type; - Node infer_lhs = - NodeManager::currentNM()->mkNode(kind::MULT, mult, t); - Node infer_rhs = - NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs); - Node infer = NodeManager::currentNM()->mkNode( - infer_type, infer_lhs, infer_rhs); - Trace("nl-ext-bound-debug") << " " << infer << std::endl; - infer = Rewriter::rewrite(infer); - Trace("nl-ext-bound-debug2") - << " ...rewritten : " << infer << std::endl; - // check whether it is false in model for abstraction - Node infer_mv = computeModelValue(infer, 1); - Trace("nl-ext-bound-debug") - << " ...infer model value is " << infer_mv - << std::endl; - if (infer_mv == d_false) { - Node exp = NodeManager::currentNM()->mkNode( - kind::AND, - NodeManager::currentNM()->mkNode( - mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero), - ci_exp[x][coeff][rhs]); - Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES, - exp, infer); - Node pr_iblem = iblem; - iblem = Rewriter::rewrite(iblem); - bool introNewTerms = hasNewMonomials(iblem, ms); - Trace("nl-ext-bound-lemma") - << "*** Bound inference lemma : " << iblem - << " (pre-rewrite : " << pr_iblem << ")" << std::endl; - // Trace("nl-ext-bound-lemma") << " intro new - // monomials = " << introNewTerms << std::endl; - if (!introNewTerms) { - lemmas.push_back(iblem); - } else { - nt_lemmas.push_back(iblem); - } - } - } else { - Trace("nl-ext-bound-debug") << " ...coefficient " << mult - << " is zero." << std::endl; - } - } - } - } - } - } - } else { - Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl; - } - } + //-----------------------------------inferred bounds lemmas + // e.g. x >= t => y*x >= y*t + std::vector< Node > nt_lemmas; + lemmas = checkMonomialInferBounds( nt_lemmas, false_asserts ); // Trace("nl-ext") << "Bound lemmas : " << lemmas.size() << ", " << // nt_lemmas.size() << std::endl; prioritize lemmas that do not // introduce new monomials @@ -1594,226 +1312,43 @@ void NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, << std::endl; return; } - - //------------------------------------resolution bound inferences, e.g. - //( - // y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t - if (options::nlExtResBound()) { - Trace("nl-ext") << "Get resolution inferred bound lemmas..." << std::endl; - for (unsigned j = 0; j < terms.size(); j++) { - Node a = terms[j]; - std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca = - ci.find(a); - if (itca != ci.end()) { - for (unsigned k = (j + 1); k < terms.size(); k++) { - Node b = terms[k]; - std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator - itcb = ci.find(b); - if (itcb != ci.end()) { - Trace("nl-ext-rbound-debug") << "resolution inferences : compare " - << a << " and " << b << std::endl; - // if they have common factors - std::map<Node, Node>::iterator ita = d_mono_diff[a].find(b); - if (ita != d_mono_diff[a].end()) { - std::map<Node, Node>::iterator itb = d_mono_diff[b].find(a); - Assert(itb != d_mono_diff[b].end()); - Node mv_a = computeModelValue(ita->second, 1); - Assert(mv_a.isConst()); - int mv_a_sgn = mv_a.getConst<Rational>().sgn(); - Assert(mv_a_sgn != 0); - Node mv_b = computeModelValue(itb->second, 1); - Assert(mv_b.isConst()); - int mv_b_sgn = mv_b.getConst<Rational>().sgn(); - Assert(mv_b_sgn != 0); - Trace("nl-ext-rbound") << "Get resolution inferences for [a] " - << a << " vs [b] " << b << std::endl; - Trace("nl-ext-rbound") - << " [a] factor is " << ita->second - << ", sign in model = " << mv_a_sgn << std::endl; - Trace("nl-ext-rbound") - << " [b] factor is " << itb->second - << ", sign in model = " << mv_b_sgn << std::endl; - - std::vector<Node> exp; - // bounds of a - for (std::map<Node, std::map<Node, Kind> >::iterator itcac = - itca->second.begin(); - itcac != itca->second.end(); ++itcac) { - Node coeff_a = itcac->first; - for (std::map<Node, Kind>::iterator itcar = - 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); - rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base); - if (!hasNewMonomials(rhs_a_res_base, ms)) { - Kind type_a = itcar->second; - exp.push_back(ci_exp[a][coeff_a][rhs_a]); - - // bounds of b - for (std::map<Node, std::map<Node, Kind> >::iterator itcbc = - itcb->second.begin(); - itcbc != itcb->second.end(); ++itcbc) { - Node coeff_b = itcbc->first; - Node rhs_a_res = - QuantArith::mkCoeffTerm(coeff_b, rhs_a_res_base); - for (std::map<Node, Kind>::iterator itcbr = - itcbc->second.begin(); - itcbr != itcbc->second.end(); ++itcbr) { - Node rhs_b = itcbr->first; - Node rhs_b_res = NodeManager::currentNM()->mkNode( - kind::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, ms)) { - Kind type_b = itcbr->second; - exp.push_back(ci_exp[b][coeff_b][rhs_b]); - if (Trace.isOn("nl-ext-rbound")) { - Trace("nl-ext-rbound") << "* try bounds : "; - debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, - rhs_a); - Trace("nl-ext-rbound") << std::endl; - Trace("nl-ext-rbound") << " "; - debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, - rhs_b); - Trace("nl-ext-rbound") << std::endl; - } - Kind types[2]; - for (unsigned r = 0; r < 2; r++) { - Node pivot_factor = - r == 0 ? itb->second : ita->second; - int pivot_factor_sign = - r == 0 ? mv_b_sgn : mv_a_sgn; - types[r] = r == 0 ? type_a : type_b; - if (pivot_factor_sign == (r == 0 ? 1 : -1)) { - types[r] = reverseRelationKind(types[r]); - } - if (pivot_factor_sign == 1) { - exp.push_back(NodeManager::currentNM()->mkNode( - kind::GT, pivot_factor, d_zero)); - } else { - exp.push_back(NodeManager::currentNM()->mkNode( - kind::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) { - 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), - conc); - Trace("nl-ext-rbound-lemma-debug") - << "Resolution bound lemma " - "(pre-rewrite) " - ": " - << rblem << std::endl; - rblem = Rewriter::rewrite(rblem); - Trace("nl-ext-rbound-lemma") - << "Resolution bound lemma : " << rblem - << std::endl; - lemmas.push_back(rblem); - } - } - exp.pop_back(); - exp.pop_back(); - exp.pop_back(); - } - } - } - exp.pop_back(); - } - } - } - } - } - } - } - } - lemmas_proc = flushLemmas(lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." - << std::endl; - return; - } - } - - // from inferred bound inferences + + // from inferred bound inferences : now do ones that introduce new terms lemmas_proc = flushLemmas(nt_lemmas); if (lemmas_proc > 0) { Trace("nl-ext") << " ...finished with " << lemmas_proc << " new (monomial-introducing) lemmas." << std::endl; return; } + + //------------------------------------factoring lemmas + // x*y + x*z >= t => exists k. k = y + z ^ x*k >= t + if( options::nlExtFactor() ){ + lemmas = checkFactoring( false_asserts ); + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; + return; + } + } - if (options::nlExtTangentPlanes()) { - Trace("nl-ext") << "Get tangent plane lemmas..." << std::endl; - unsigned kstart = ms_vars.size(); - for (unsigned k = kstart; k < terms.size(); k++) { - Node t = terms[k]; - // if this term requires a refinement - if (tplane_refine_dir.find(t) != tplane_refine_dir.end()) { - Trace("nl-ext-tplanes") - << "Look at monomial requiring refinement : " << t << std::endl; - // get a decomposition - std::map<Node, std::vector<Node> >::iterator it = - d_m_contain_children.find(t); - if (it != d_m_contain_children.end()) { - std::map<Node, std::map<Node, bool> > dproc; - for (unsigned j = 0; j < it->second.size(); j++) { - Node tc = it->second[j]; - if (tc != d_one) { - Node tc_diff = d_m_contain_umult[tc][t]; - Assert(!tc_diff.isNull()); - Node a = tc < tc_diff ? tc : tc_diff; - Node b = tc < tc_diff ? tc_diff : tc; - if (dproc[a].find(b) == dproc[a].end()) { - dproc[a][b] = true; - Trace("nl-ext-tplanes") - << " decomposable into : " << a << " * " << b << std::endl; - Node a_v = computeModelValue(a, 1); - Node b_v = computeModelValue(b, 1); - // tangent plane - Node tplane = NodeManager::currentNM()->mkNode( - kind::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)); - for (unsigned d = 0; d < 4; d++) { - Node aa = NodeManager::currentNM()->mkNode( - d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v); - Node ab = NodeManager::currentNM()->mkNode( - d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v); - Node conc = NodeManager::currentNM()->mkNode( - d <= 1 ? kind::LEQ : kind::GEQ, t, tplane); - Node tlem = NodeManager::currentNM()->mkNode( - kind::OR, aa.negate(), ab.negate(), conc); - Trace("nl-ext-tplanes") - << "Tangent plane lemma : " << tlem << std::endl; - lemmas.push_back(tlem); - } - } - } - } - } - } + //------------------------------------resolution bound inferences + // e.g. ( y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t + if (options::nlExtResBound()) { + lemmas = checkMonomialInferResBounds(); + lemmas_proc = flushLemmas(lemmas); + if (lemmas_proc > 0) { + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; + return; } - Trace("nl-ext") << "...trying " << lemmas.size() - << " tangent plane lemmas..." << std::endl; + } + + //------------------------------------tangent planes + if (options::nlExtTangentPlanes()) { + lemmas = checkTangentPlanes(); lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." - << std::endl; + Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas." << std::endl; return; } } @@ -1852,10 +1387,13 @@ void NonlinearExtension::check(Theory::Effort e) { const Assertion& assertion = *it; assertions.push_back(assertion.assertion); } - const std::set<Node> false_asserts = getFalseInModel(assertions); + + std::vector<Node> xts; + d_containing.getExtTheory()->getTerms(xts); + if (!false_asserts.empty()) { - checkLastCall(assertions, false_asserts); + checkLastCall(assertions, false_asserts, xts); }else{ //must ensure that shared terms are equal to their concrete value std::vector< Node > lemmas; @@ -1902,6 +1440,11 @@ void NonlinearExtension::assignOrderIds(std::vector<Node>& vars, for (unsigned j = 0; j < vars.size(); j++) { Node x = vars[j]; Node v = get_compare_value(x, orderType); + if( !v.isConst() ){ + Trace("nl-ext-mvo") << "..do not assign order to " << x << " : " << v << std::endl; + //don't assign for non-constant values (transcendental function apps) + break; + } Trace("nl-ext-mvo") << " order " << x << " : " << v << std::endl; if (v != prev) { // builtin points @@ -1944,8 +1487,21 @@ void NonlinearExtension::assignOrderIds(std::vector<Node>& vars, int NonlinearExtension::compare(Node i, Node j, unsigned orderType) const { Assert(orderType >= 0); if (orderType <= 3) { - return compare_value(get_compare_value(i, orderType), - get_compare_value(j, orderType), orderType); + Node ci = get_compare_value(i, orderType); + Node cj = get_compare_value(j, orderType); + if( ci.isConst() ){ + if( cj.isConst() ){ + return compare_value(ci, cj, orderType); + }else{ + return 1; + } + }else{ + if( cj.isConst() ){ + return -1; + }else{ + return 0; + } + } // minimal degree } else if (orderType == 4) { unsigned i_count = getCount(d_m_degree, i); @@ -1956,10 +1512,32 @@ 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) ) ) ); + //initialize bounds + d_pi_bound[0] = NodeManager::currentNM()->mkConst( Rational(333)/Rational(106) ); + d_pi_bound[1] = NodeManager::currentNM()->mkConst( Rational(355)/Rational(113) ); + } +} + +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] ) ); + lemmas.push_back( pi_lem ); +} + int NonlinearExtension::compare_value(Node i, Node j, unsigned orderType) const { Assert(orderType >= 0 && orderType <= 3); - Trace("nl-ext-debug") << "compare_value " << i << " " << j + Assert( i.isConst() && j.isConst() ); + Trace("nl-ext-debug") << "compare value " << i << " " << j << ", o = " << orderType << std::endl; int ret; if (i == j) { @@ -1991,8 +1569,7 @@ Node NonlinearExtension::get_compare_value(Node i, unsigned orderType) const { return iti->second; } -// trying to show a <> 0 by inequalities between variables in monomial a w.r.t -// 0 +// show a <> 0 by inequalities between variables in monomial a w.r.t 0 int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, int status, std::vector<Node>& exp, std::vector<Node>& lem) { @@ -2011,8 +1588,9 @@ int NonlinearExtension::compareSign(Node oa, Node a, unsigned a_index, Node av = d_m_vlist[a][a_index]; unsigned aexp = d_m_exp[a][av]; // take current sign in model - Assert(d_mv[0].find(av) != d_mv[0].end()); - int sgn = d_mv[0][av].getConst<Rational>().sgn(); + Assert( d_mv[1].find(av) != d_mv[0].end() ); + Assert( d_mv[1][av].isConst() ); + int sgn = d_mv[1][av].getConst<Rational>().sgn(); Trace("nl-ext-debug") << "Process var " << av << "^" << aexp << ", model sign = " << sgn << std::endl; if (sgn == 0) { @@ -2126,8 +1704,8 @@ bool NonlinearExtension::compareMonomial( return compareMonomial(oa, a, a_index + 1, a_exp_proc, ob, b, b_index, b_exp_proc, status, exp, lem, cmp_infers); } - Assert(d_order_vars[1].find(av) != d_order_vars[1].end()); - avo = d_order_vars[1][av]; + Assert(d_order_vars.find(av) != d_order_vars.end()); + avo = d_order_vars[av]; } Node bv; unsigned bexp = 0; @@ -2140,12 +1718,12 @@ bool NonlinearExtension::compareMonomial( return compareMonomial(oa, a, a_index, a_exp_proc, ob, b, b_index + 1, b_exp_proc, status, exp, lem, cmp_infers); } - Assert(d_order_vars[1].find(bv) != d_order_vars[1].end()); - bvo = d_order_vars[1][bv]; + Assert(d_order_vars.find(bv) != d_order_vars.end()); + bvo = d_order_vars[bv]; } // get "one" information - Assert(d_order_vars[1].find(d_one) != d_order_vars[1].end()); - unsigned ovo = d_order_vars[1][d_one]; + Assert(d_order_vars.find(d_one) != d_order_vars.end()); + unsigned ovo = d_order_vars[d_one]; Trace("nl-ext-comp-debug") << "....vars : " << av << "^" << aexp << " " << bv << "^" << bexp << std::endl; @@ -2266,6 +1844,1024 @@ void NonlinearExtension::MonomialIndex::addTerm(Node n, } } +std::vector<Node> NonlinearExtension::checkMonomialSign() { + std::vector<Node> lemmas; + std::map<Node, int> signs; + Trace("nl-ext") << "Get monomial sign lemmas..." << std::endl; + for (unsigned j = 0; j < d_ms.size(); j++) { + Node a = d_ms[j]; + if (d_ms_proc.find(a) == d_ms_proc.end()) { + std::vector<Node> exp; + Trace("nl-ext-debug") << " process " << a << ", mv=" << d_mv[0][a] << "..." << std::endl; + if( d_m_nconst_factor.find( a )==d_m_nconst_factor.end() ){ + signs[a] = compareSign(a, a, 0, 1, exp, lemmas); + if (signs[a] == 0) { + d_ms_proc[a] = true; + Trace("nl-ext-debug") << "...mark " << a + << " reduced since its value is 0." << std::endl; + } + }else{ + Trace("nl-ext-debug") << "...can't conclude sign lemma for " << a << " since model value of a factor is non-constant." << std::endl; + //TODO + } + } + } + return lemmas; +} + +std::vector<Node> NonlinearExtension::checkMonomialMagnitude( unsigned c ) { + unsigned r = 1; + std::vector<Node> lemmas; +// if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L + // in lemmas + std::map<int, std::map<Node, std::map<Node, Node> > > cmp_infers; + Trace("nl-ext") << "Get monomial comparison lemmas (order=" << r + << ", compare=" << c << ")..." << std::endl; + for (unsigned j = 0; j < d_ms.size(); j++) { + Node a = d_ms[j]; + if (d_ms_proc.find(a) == d_ms_proc.end() && + d_m_nconst_factor.find( a )==d_m_nconst_factor.end()) { + if (c == 0) { + // compare magnitude against 1 + std::vector<Node> exp; + NodeMultiset a_exp_proc; + NodeMultiset b_exp_proc; + compareMonomial(a, a, a_exp_proc, d_one, d_one, b_exp_proc, exp, + lemmas, cmp_infers); + } else { + std::map<Node, NodeMultiset>::iterator itmea = d_m_exp.find(a); + Assert(itmea != d_m_exp.end()); + if (c == 1) { + // TODO : not just against containing variables? + // compare magnitude against variables + for (unsigned k = 0; k < d_ms_vars.size(); k++) { + Node v = d_ms_vars[k]; + Assert( d_mv[0].find( v )!=d_mv[0].end() ); + if( d_mv[0][v].isConst() ){ + std::vector<Node> exp; + NodeMultiset a_exp_proc; + NodeMultiset b_exp_proc; + if (itmea->second.find(v) != itmea->second.end()) { + a_exp_proc[v] = 1; + b_exp_proc[v] = 1; + setMonomialFactor(a, v, a_exp_proc); + setMonomialFactor(v, a, b_exp_proc); + compareMonomial(a, a, a_exp_proc, v, v, b_exp_proc, exp, + lemmas, cmp_infers); + } + } + } + } else { + // compare magnitude against other non-linear monomials + for (unsigned k = (j + 1); k < d_ms.size(); k++) { + Node b = d_ms[k]; + //(signs[a]==signs[b])==(r==0) + if (d_ms_proc.find(b) == d_ms_proc.end() && + d_m_nconst_factor.find( b )==d_m_nconst_factor.end()) { + std::map<Node, NodeMultiset>::iterator itmeb = + d_m_exp.find(b); + Assert(itmeb != d_m_exp.end()); + + std::vector<Node> exp; + // take common factors of monomials, set minimum of + // common exponents as processed + NodeMultiset a_exp_proc; + NodeMultiset b_exp_proc; + for (NodeMultiset::iterator itmea2 = itmea->second.begin(); + itmea2 != itmea->second.end(); ++itmea2) { + NodeMultiset::iterator itmeb2 = + itmeb->second.find(itmea2->first); + if (itmeb2 != itmeb->second.end()) { + unsigned min_exp = itmea2->second > itmeb2->second + ? itmeb2->second + : itmea2->second; + a_exp_proc[itmea2->first] = min_exp; + b_exp_proc[itmea2->first] = min_exp; + Trace("nl-ext-comp") + << "Common exponent : " << itmea2->first << " : " + << min_exp << std::endl; + } + } + if (!a_exp_proc.empty()) { + setMonomialFactor(a, b, a_exp_proc); + setMonomialFactor(b, a, b_exp_proc); + } + /* + if( !a_exp_proc.empty() ){ + //reduction based on common exponents a > 0 => ( a * b + <> a * c <=> b <> c ), a < 0 => ( a * b <> a * c <=> b + !<> c ) ? }else{ compareMonomial( a, a, a_exp_proc, b, + b, b_exp_proc, exp, lemmas ); + } + */ + compareMonomial(a, a, a_exp_proc, b, b, b_exp_proc, exp, + lemmas, cmp_infers); + } + } + } + } + } + } + // remove redundant lemmas, e.g. if a > b, b > c, a > c were + // inferred, discard lemma with conclusion a > c + Trace("nl-ext-comp") << "Compute redundand_cies for " << lemmas.size() + << " lemmas." << std::endl; + // naive + std::vector<Node> r_lemmas; + for (std::map<int, std::map<Node, std::map<Node, Node> > >::iterator itb = + cmp_infers.begin(); + itb != cmp_infers.end(); ++itb) { + for (std::map<Node, std::map<Node, Node> >::iterator itc = + itb->second.begin(); + itc != itb->second.end(); ++itc) { + for (std::map<Node, Node>::iterator itc2 = itc->second.begin(); + itc2 != itc->second.end(); ++itc2) { + std::map<Node, bool> visited; + for (std::map<Node, Node>::iterator itc3 = itc->second.begin(); + itc3 != itc->second.end(); ++itc3) { + if (itc3->first != itc2->first) { + std::vector<Node> exp; + if (cmp_holds(itc3->first, itc2->first, itb->second, exp, + visited)) { + r_lemmas.push_back(itc2->second); + Trace("nl-ext-comp") + << "...inference of " << itc->first << " > " + << itc2->first << " was redundant." << std::endl; + break; + } + } + } + } + } + } + std::vector<Node> nr_lemmas; + for (unsigned i = 0; i < lemmas.size(); i++) { + if (std::find(r_lemmas.begin(), r_lemmas.end(), lemmas[i]) == + r_lemmas.end()) { + nr_lemmas.push_back(lemmas[i]); + } + } + // TODO: only take maximal lower/minimial lower bounds? + + Trace("nl-ext-comp") << nr_lemmas.size() << " / " << lemmas.size() + << " were non-redundant." << std::endl; + return nr_lemmas; +} + +std::vector<Node> NonlinearExtension::checkTangentPlanes() { + std::vector< Node > lemmas; + Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl; + unsigned kstart = d_ms_vars.size(); + for (unsigned k = kstart; k < d_mterms.size(); k++) { + Node t = d_mterms[k]; + // if this term requires a refinement + if (d_tplane_refine_dir.find(t) != d_tplane_refine_dir.end()) { + Trace("nl-ext-tplanes") + << "Look at monomial requiring refinement : " << t << std::endl; + // get a decomposition + std::map<Node, std::vector<Node> >::iterator it = + d_m_contain_children.find(t); + if (it != d_m_contain_children.end()) { + std::map<Node, std::map<Node, bool> > dproc; + for (unsigned j = 0; j < it->second.size(); j++) { + Node tc = it->second[j]; + if (tc != d_one) { + Node tc_diff = d_m_contain_umult[tc][t]; + Assert(!tc_diff.isNull()); + Node a = tc < tc_diff ? tc : tc_diff; + Node b = tc < tc_diff ? tc_diff : tc; + if (dproc[a].find(b) == dproc[a].end()) { + dproc[a][b] = true; + Trace("nl-ext-tplanes") + << " decomposable into : " << a << " * " << b << std::endl; + Node a_v = computeModelValue(a, 1); + Node b_v = computeModelValue(b, 1); + // tangent plane + Node tplane = NodeManager::currentNM()->mkNode( + kind::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)); + for (unsigned d = 0; d < 4; d++) { + Node aa = NodeManager::currentNM()->mkNode( + d == 0 || d == 3 ? kind::GEQ : kind::LEQ, a, a_v); + Node ab = NodeManager::currentNM()->mkNode( + d == 1 || d == 3 ? kind::GEQ : kind::LEQ, b, b_v); + Node conc = NodeManager::currentNM()->mkNode( + d <= 1 ? kind::LEQ : kind::GEQ, t, tplane); + Node tlem = NodeManager::currentNM()->mkNode( + kind::OR, aa.negate(), ab.negate(), conc); + Trace("nl-ext-tplanes") + << "Tangent plane lemma : " << tlem << std::endl; + lemmas.push_back(tlem); + } + } + } + } + } + } + } + Trace("nl-ext") << "...trying " << lemmas.size() + << " tangent plane lemmas..." << std::endl; + return lemmas; +} + + + +std::vector<Node> NonlinearExtension::checkMonomialInferBounds( std::vector<Node>& nt_lemmas, + const std::set<Node>& false_asserts ) { + std::vector< Node > lemmas; + // register constraints + Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; + for (context::CDList<Assertion>::const_iterator it = + 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; + registerConstraint(atom); + bool is_false_lit = false_asserts.find(lit) != false_asserts.end(); + // add information about bounds to variables + std::map<Node, std::map<Node, ConstraintInfo> >::iterator itc = + d_c_info.find(atom); + std::map<Node, std::map<Node, bool> >::iterator itcm = + d_c_info_maxm.find(atom); + if (itc != d_c_info.end()) { + Assert(itcm != d_c_info_maxm.end()); + for (std::map<Node, ConstraintInfo>::iterator itcc = itc->second.begin(); + itcc != itc->second.end(); ++itcc) { + Node x = itcc->first; + Node coeff = itcc->second.d_coeff; + Node rhs = itcc->second.d_rhs; + Kind type = itcc->second.d_type; + Node exp = lit; + if (!polarity) { + // reverse + if (type == kind::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_mv = computeModelValue(query, 1); + if (query_mv == d_true) { + exp = query; + type = kind::GT; + } else { + Assert(query_mv == d_false); + exp = NodeManager::currentNM()->mkNode(kind::LT, lhs, rhs); + type = kind::LT; + } + } else { + type = negateKind(type); + } + } + // add to status if maximal degree + d_ci_max[x][coeff][rhs] = itcm->second.find(x) != itcm->second.end(); + if (Trace.isOn("nl-ext-bound-debug2")) { + Node t = QuantArith::mkCoeffTerm(coeff, x); + Trace("nl-ext-bound-debug2") + << "Add Bound: " << t << " " << type << " " << rhs << " by " + << exp << std::endl; + } + bool updated = true; + std::map<Node, Kind>::iterator its = d_ci[x][coeff].find(rhs); + if (its == d_ci[x][coeff].end()) { + d_ci[x][coeff][rhs] = type; + d_ci_exp[x][coeff][rhs] = exp; + } else if (type != its->second) { + Trace("nl-ext-bound-debug2") + << "Joining kinds : " << type << " " << its->second << std::endl; + Kind jk = joinKinds(type, its->second); + if (jk == kind::UNDEFINED_KIND) { + updated = false; + } else if (jk != its->second) { + if (jk == type) { + d_ci[x][coeff][rhs] = type; + d_ci_exp[x][coeff][rhs] = exp; + } 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); + } + } else { + updated = false; + } + } + if (Trace.isOn("nl-ext-bound")) { + if (updated) { + Trace("nl-ext-bound") << "Bound: "; + debugPrintBound("nl-ext-bound", coeff, x, d_ci[x][coeff][rhs], rhs); + Trace("nl-ext-bound") << " by " << d_ci_exp[x][coeff][rhs]; + if (d_ci_max[x][coeff][rhs]) { + Trace("nl-ext-bound") << ", is max degree"; + } + Trace("nl-ext-bound") << std::endl; + } + } + // compute if bound is not satisfied, and store what is required + // for a possible refinement + if (options::nlExtTangentPlanes()) { + if (is_false_lit) { + Node rhs_v = computeModelValue(rhs, 0); + Node x_v = computeModelValue(x, 0); + if( rhs_v.isConst() && x_v.isConst() ){ + bool needsRefine = false; + bool refineDir; + if (rhs_v == x_v) { + if (type == kind::GT) { + needsRefine = true; + refineDir = true; + } else if (type == kind::LT) { + needsRefine = true; + refineDir = false; + } + } else if (x_v.getConst<Rational>() > rhs_v.getConst<Rational>()) { + if (type != kind::GT && type != kind::GEQ) { + needsRefine = true; + refineDir = false; + } + } else { + if (type != kind::LT && type != kind::LEQ) { + needsRefine = true; + refineDir = true; + } + } + Trace("nl-ext-tplanes-cons-debug") + << "...compute if bound corresponds to a required " + "refinement" + << std::endl; + Trace("nl-ext-tplanes-cons-debug") + << "...M[" << x << "] = " << x_v << ", M[" << rhs + << "] = " << rhs_v << std::endl; + Trace("nl-ext-tplanes-cons-debug") << "...refine = " << needsRefine + << "/" << refineDir << std::endl; + if (needsRefine) { + Trace("nl-ext-tplanes-cons") + << "---> By " << lit << " and since M[" << x << "] = " << x_v + << ", M[" << rhs << "] = " << rhs_v << ", "; + Trace("nl-ext-tplanes-cons") + << "monomial " << x << " should be " + << (refineDir ? "larger" : "smaller") << std::endl; + d_tplane_refine_dir[x][refineDir] = true; + } + } + } + } + } + } + } + // reflexive constraints + 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_exp[n][null_coeff][n] = d_true; + d_ci_max[n][null_coeff][n] = false; + } + + Trace("nl-ext") << "Get inferred bound lemmas..." << std::endl; + + for (unsigned k = 0; k < d_mterms.size(); k++) { + Node x = d_mterms[k]; + Trace("nl-ext-bound-debug") + << "Process bounds for " << x << " : " << std::endl; + std::map<Node, std::vector<Node> >::iterator itm = + d_m_contain_parent.find(x); + if (itm != d_m_contain_parent.end()) { + Trace("nl-ext-bound-debug") << "...has " << itm->second.size() + << " parent monomials." << std::endl; + // check derived bounds + std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itc = + d_ci.find(x); + if (itc != d_ci.end()) { + for (std::map<Node, std::map<Node, Kind> >::iterator itcc = + itc->second.begin(); + itcc != itc->second.end(); ++itcc) { + Node coeff = itcc->first; + Node t = QuantArith::mkCoeffTerm(coeff, x); + for (std::map<Node, Kind>::iterator itcr = itcc->second.begin(); + itcr != itcc->second.end(); ++itcr) { + Node rhs = itcr->first; + // only consider this bound if maximal degree + if (d_ci_max[x][coeff][rhs]) { + Kind type = itcr->second; + for (unsigned j = 0; j < itm->second.size(); j++) { + Node y = itm->second[j]; + Assert(d_m_contain_mult[x].find(y) != + d_m_contain_mult[x].end()); + Node mult = d_m_contain_mult[x][y]; + // x <k> t => m*x <k'> t where y = m*x + // get the sign of mult + Node mmv = computeModelValue(mult); + Trace("nl-ext-bound-debug2") + << "Model value of " << mult << " is " << mmv << std::endl; + if(mmv.isConst()){ + int mmv_sign = mmv.getConst<Rational>().sgn(); + Trace("nl-ext-bound-debug2") + << " sign of " << mmv << " is " << mmv_sign << std::endl; + if (mmv_sign != 0) { + Trace("nl-ext-bound-debug") + << " from " << x << " * " << mult << " = " << y + << " and " << t << " " << type << " " << rhs + << ", infer : " << std::endl; + Kind infer_type = + mmv_sign == -1 ? reverseRelationKind(type) : type; + Node infer_lhs = + NodeManager::currentNM()->mkNode(kind::MULT, mult, t); + Node infer_rhs = + NodeManager::currentNM()->mkNode(kind::MULT, mult, rhs); + Node infer = NodeManager::currentNM()->mkNode( + infer_type, infer_lhs, infer_rhs); + Trace("nl-ext-bound-debug") << " " << infer << std::endl; + infer = Rewriter::rewrite(infer); + Trace("nl-ext-bound-debug2") + << " ...rewritten : " << infer << std::endl; + // check whether it is false in model for abstraction + Node infer_mv = computeModelValue(infer, 1); + Trace("nl-ext-bound-debug") + << " ...infer model value is " << infer_mv + << std::endl; + if (infer_mv == d_false) { + Node exp = NodeManager::currentNM()->mkNode( + kind::AND, + NodeManager::currentNM()->mkNode( + mmv_sign == 1 ? kind::GT : kind::LT, mult, d_zero), + d_ci_exp[x][coeff][rhs]); + Node iblem = NodeManager::currentNM()->mkNode(kind::IMPLIES, + exp, infer); + Node pr_iblem = iblem; + iblem = Rewriter::rewrite(iblem); + bool introNewTerms = hasNewMonomials(iblem, d_ms); + Trace("nl-ext-bound-lemma") + << "*** Bound inference lemma : " << iblem + << " (pre-rewrite : " << pr_iblem << ")" << std::endl; + // Trace("nl-ext-bound-lemma") << " intro new + // monomials = " << introNewTerms << std::endl; + if (!introNewTerms) { + lemmas.push_back(iblem); + } else { + nt_lemmas.push_back(iblem); + } + } + } else { + Trace("nl-ext-bound-debug") << " ...coefficient " << mult + << " is zero." << std::endl; + } + }else{ + Trace("nl-ext-bound-debug") << " ...coefficient " << mult + << " is non-constant (probably transcendental)." << std::endl; + } + } + } + } + } + } + } else { + Trace("nl-ext-bound-debug") << "...has no parent monomials." << std::endl; + } + } + return lemmas; +} + +std::vector<Node> NonlinearExtension::checkFactoring( const std::set<Node>& false_asserts ) { + std::vector< Node > lemmas; + Trace("nl-ext") << "Get factoring lemmas..." << std::endl; + for (context::CDList<Assertion>::const_iterator it = + 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; + 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)) { + Trace("nl-ext-factor") << "Factoring for literal " << lit << ", monomial sum is : " << std::endl; + if (Trace.isOn("nl-ext-factor")) { + QuantArith::debugPrintMonomialSum(msum, "nl-ext-factor"); + } + std::map< Node, std::vector< Node > > factor_to_mono; + std::map< Node, std::vector< Node > > factor_to_mono_orig; + for( std::map<Node, Node>::iterator itm = msum.begin(); itm != msum.end(); ++itm ){ + if( !itm->first.isNull() ){ + if( itm->first.getKind()==NONLINEAR_MULT ){ + std::vector< Node > children; + for( unsigned i=0; i<itm->first.getNumChildren(); i++ ){ + children.push_back( itm->first[i] ); + } + std::map< Node, bool > processed; + for( unsigned i=0; i<itm->first.getNumChildren(); i++ ){ + if( processed.find( itm->first[i] )==processed.end() ){ + processed[itm->first[i]] = true; + children[i] = d_one; + if( !itm->second.isNull() ){ + children.push_back( itm->second ); + } + Node val = NodeManager::currentNM()->mkNode( kind::MULT, children ); + if( !itm->second.isNull() ){ + children.pop_back(); + } + children[i] = itm->first[i]; + val = Rewriter::rewrite( val ); + factor_to_mono[itm->first[i]].push_back( val ); + factor_to_mono_orig[itm->first[i]].push_back( itm->first ); + } + } + } /* else{ + factor_to_mono[itm->first].push_back( itm->second.isNull() ? d_one : itm->second ); + factor_to_mono_orig[itm->first].push_back( itm->first ); + }*/ + } + } + 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 ); + 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 ) ); + 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 ){ + if( std::find( itfo->second.begin(), itfo->second.end(), itm->first )==itfo->second.end() ){ + 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 ); + 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 ); + d_skolem_atoms.insert( conc_lit ); + if( !polarity ){ + conc_lit = conc_lit.negate(); + } + + 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 ); + Trace("nl-ext-factor") << "...lemma is " << flem << std::endl; + lemmas.push_back( flem ); + } + } + } + } + } + return lemmas; +} + +Node NonlinearExtension::getFactorSkolem( Node n, std::vector< Node >& lemmas ) { + std::map< Node, Node >::iterator itf = d_factor_skolem.find( n ); + if( itf==d_factor_skolem.end() ){ + Node k = NodeManager::currentNM()->mkSkolem( "kf", n.getType() ); + Node k_eq = Rewriter::rewrite( k.eqNode( n ) ); + d_skolem_atoms.insert( k_eq ); + lemmas.push_back( k_eq ); + d_factor_skolem[n] = k; + return k; + }else{ + return itf->second; + } +} + +std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() { + std::vector< Node > lemmas; + Trace("nl-ext") << "Get monomial resolution inferred bound lemmas..." << std::endl; + for (unsigned j = 0; j < d_mterms.size(); j++) { + Node a = d_mterms[j]; + std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator itca = + d_ci.find(a); + if (itca != d_ci.end()) { + for (unsigned k = (j + 1); k < d_mterms.size(); k++) { + Node b = d_mterms[k]; + std::map<Node, std::map<Node, std::map<Node, Kind> > >::iterator + itcb = d_ci.find(b); + if (itcb != d_ci.end()) { + Trace("nl-ext-rbound-debug") << "resolution inferences : compare " + << a << " and " << b << std::endl; + // if they have common factors + std::map<Node, Node>::iterator ita = d_mono_diff[a].find(b); + if (ita != d_mono_diff[a].end()) { + std::map<Node, Node>::iterator itb = d_mono_diff[b].find(a); + Assert(itb != d_mono_diff[b].end()); + Node mv_a = computeModelValue(ita->second, 1); + Assert(mv_a.isConst()); + int mv_a_sgn = mv_a.getConst<Rational>().sgn(); + Assert(mv_a_sgn != 0); + Node mv_b = computeModelValue(itb->second, 1); + Assert(mv_b.isConst()); + int mv_b_sgn = mv_b.getConst<Rational>().sgn(); + Assert(mv_b_sgn != 0); + Trace("nl-ext-rbound") << "Get resolution inferences for [a] " + << a << " vs [b] " << b << std::endl; + Trace("nl-ext-rbound") + << " [a] factor is " << ita->second + << ", sign in model = " << mv_a_sgn << std::endl; + Trace("nl-ext-rbound") + << " [b] factor is " << itb->second + << ", sign in model = " << mv_b_sgn << std::endl; + + std::vector<Node> exp; + // bounds of a + for (std::map<Node, std::map<Node, Kind> >::iterator itcac = + itca->second.begin(); + itcac != itca->second.end(); ++itcac) { + Node coeff_a = itcac->first; + for (std::map<Node, Kind>::iterator itcar = + 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); + rhs_a_res_base = Rewriter::rewrite(rhs_a_res_base); + if (!hasNewMonomials(rhs_a_res_base, d_ms)) { + Kind type_a = itcar->second; + exp.push_back(d_ci_exp[a][coeff_a][rhs_a]); + + // bounds of b + for (std::map<Node, std::map<Node, Kind> >::iterator itcbc = + itcb->second.begin(); + itcbc != itcb->second.end(); ++itcbc) { + Node coeff_b = itcbc->first; + Node rhs_a_res = + QuantArith::mkCoeffTerm(coeff_b, rhs_a_res_base); + for (std::map<Node, Kind>::iterator itcbr = + itcbc->second.begin(); + itcbr != itcbc->second.end(); ++itcbr) { + Node rhs_b = itcbr->first; + Node rhs_b_res = NodeManager::currentNM()->mkNode( + kind::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)) { + Kind type_b = itcbr->second; + exp.push_back(d_ci_exp[b][coeff_b][rhs_b]); + if (Trace.isOn("nl-ext-rbound")) { + Trace("nl-ext-rbound") << "* try bounds : "; + debugPrintBound("nl-ext-rbound", coeff_a, a, type_a, + rhs_a); + Trace("nl-ext-rbound") << std::endl; + Trace("nl-ext-rbound") << " "; + debugPrintBound("nl-ext-rbound", coeff_b, b, type_b, + rhs_b); + Trace("nl-ext-rbound") << std::endl; + } + Kind types[2]; + for (unsigned r = 0; r < 2; r++) { + Node pivot_factor = + r == 0 ? itb->second : ita->second; + int pivot_factor_sign = + r == 0 ? mv_b_sgn : mv_a_sgn; + types[r] = r == 0 ? type_a : type_b; + if (pivot_factor_sign == (r == 0 ? 1 : -1)) { + types[r] = reverseRelationKind(types[r]); + } + if (pivot_factor_sign == 1) { + exp.push_back(NodeManager::currentNM()->mkNode( + kind::GT, pivot_factor, d_zero)); + } else { + exp.push_back(NodeManager::currentNM()->mkNode( + kind::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) { + 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), + conc); + Trace("nl-ext-rbound-lemma-debug") + << "Resolution bound lemma " + "(pre-rewrite) " + ": " + << rblem << std::endl; + rblem = Rewriter::rewrite(rblem); + Trace("nl-ext-rbound-lemma") + << "Resolution bound lemma : " << rblem + << std::endl; + lemmas.push_back(rblem); + } + } + exp.pop_back(); + exp.pop_back(); + exp.pop_back(); + } + } + } + exp.pop_back(); + } + } + } + } + } + } + } + } + return lemmas; +} + +std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() { + std::vector< Node > lemmas; + Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl; + for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){ + std::map< Node, Node > mv_to_term; + for( std::map< Node, Node >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){ + Node t = itt->second; + Assert( d_mv[1].find( t )!=d_mv[1].end() ); + Node tv = d_mv[1][t]; + mv_to_term[tv] = t; + // easy model-based bounds (TODO: make these unconditional?) + if( it->first==kind::SINE ){ + Assert( tv.isConst() ); + /* + if( tv.getConst<Rational>() > d_one.getConst<Rational>() ){ + lemmas.push_back( NodeManager::currentNM()->mkNode( kind::LEQ, t, d_one ) ); + }else if( tv.getConst<Rational>() < d_neg_one.getConst<Rational>() ){ + lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, t, d_neg_one ) ); + } + */ + /* + if( tv.getConst<Rational>().sgn()!=0 ){ + //symmetry (model-based) + Node neg_tv = NodeManager::currentNM()->mkConst( -tv.getConst<Rational>() ); + if( mv_to_term.find( neg_tv )!=mv_to_term.end() ){ + Node sum = NodeManager::currentNM()->mkNode( kind::PLUS, mv_to_term[neg_tv][0], t[0] ); + Node res = computeModelValue( sum, 0 ); + if( !res.isConst() || res.getConst<Rational>().sgn()!=0 ){ + Node tsum = NodeManager::currentNM()->mkNode( kind::PLUS, mv_to_term[neg_tv], t ); + Node sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, tsum.eqNode( d_zero ), sum.eqNode( d_zero ) ); + lemmas.push_back( sym_lem ); + } + } + } + */ + }else if( it->first==kind::EXPONENTIAL ){ + if( tv.getConst<Rational>().sgn()==-1 ){ + lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GT, t, d_zero ) ); + } + } + //initial refinements + 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] ) ); + 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 ){ + // exp(x)>0 ^ x < 0 <=> exp( x ) < 1 ^ ( x = 0 V exp( x ) > x + 1 ) + lem = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::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 ) ), + NodeManager::currentNM()->mkNode( kind::OR, + NodeManager::currentNM()->mkNode( kind::LEQ, t[0], d_zero ), + NodeManager::currentNM()->mkNode( kind::GT, t, NodeManager::currentNM()->mkNode( kind::PLUS, t[0], d_one ) ) ) ); + + } + if( !lem.isNull() ){ + lemmas.push_back( lem ); + } + } + } + } + + return lemmas; +} + +std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() { + std::vector< Node > lemmas; + Trace("nl-ext") << "Get monotonicity lemmas for transcendental functions..." << std::endl; + + //sort arguments of all transcendentals + std::map< Kind, std::vector< Node > > sorted_tf_args; + std::map< Kind, std::map< Node, Node > > tf_arg_to_term; + + for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){ + for( std::map< Node, Node >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){ + computeModelValue( itt->second[0], 1 ); + Assert( d_mv[1].find( itt->second[0] )!=d_mv[1].end() ); + if( d_mv[1][itt->second[0]].isConst() ){ + Trace("nl-ext-tf-mono-debug") << "...tf term : " << itt->second[0] << std::endl; + sorted_tf_args[ it->first ].push_back( itt->second[0] ); + tf_arg_to_term[ it->first ][ itt->second[0] ] = itt->second; + } + } + } + + SortNonlinearExtension smv; + smv.d_nla = this; + //sort by concrete values + smv.d_order_type = 0; + smv.d_reverse_order = true; + for( std::map< Kind, std::map< Node, Node > >::iterator it = d_tf_rep_map.begin(); it != d_tf_rep_map.end(); ++it ){ + Kind k = it->first; + if( !sorted_tf_args[k].empty() ){ + std::sort( sorted_tf_args[k].begin(), sorted_tf_args[k].end(), smv ); + Trace("nl-ext-tf-mono") << "Sorted transcendental function list for " << k << " : " << std::endl; + for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){ + Node targ = sorted_tf_args[k][i]; + Assert( d_mv[1].find( targ )!=d_mv[1].end() ); + Trace("nl-ext-tf-mono") << " " << targ << " -> " << d_mv[1][targ] << std::endl; + Node t = tf_arg_to_term[k][targ]; + Assert( d_mv[1].find( t )!=d_mv[1].end() ); + Trace("nl-ext-tf-mono") << " f-val : " << d_mv[1][t] << std::endl; + } + std::vector< int > mdirs; + std::vector< Node > mpoints; + std::vector< Node > mpoints_vals; + if( it->first==kind::SINE ){ + mdirs.push_back( -1 ); + mpoints.push_back( d_pi ); + mdirs.push_back( 1 ); + mpoints.push_back( d_pi_2 ); + mdirs.push_back( -1 ); + mpoints.push_back( d_pi_neg_2 ); + mdirs.push_back( 0 ); + mpoints.push_back( d_pi_neg ); + }else if( it->first==kind::EXPONENTIAL ){ + mdirs.push_back( 1 ); + mpoints.push_back( Node::null() ); + } + if( !mpoints.empty() ){ + //get model values for points + for( unsigned i=0; i<mpoints.size(); i++ ){ + Node mpv; + if( !mpoints[i].isNull() ){ + mpv = computeModelValue( mpoints[i], 1 ); + Assert( mpv.isConst() ); + } + mpoints_vals.push_back( mpv ); + } + + unsigned mdir_index = 0; + int monotonic_dir = -1; + Node mono_bounds[2]; + Node targ, targval, t, tval; + for( unsigned i=0; i<sorted_tf_args[it->first].size(); i++ ){ + Node sarg = sorted_tf_args[k][i]; + Assert( d_mv[1].find( sarg )!=d_mv[1].end() ); + Node sargval = d_mv[1][sarg]; + Assert( sargval.isConst() ); + Node s = tf_arg_to_term[k][ sarg ]; + Assert( d_mv[1].find( s )!=d_mv[1].end() ); + Node sval = d_mv[1][s]; + Assert( sval.isConst() ); + + //increment to the proper monotonicity region + bool increment = true; + while( increment && mdir_index<mdirs.size() ){ + increment = false; + if( mpoints[mdir_index].isNull() ){ + increment = true; + }else{ + Node pval = mpoints_vals[mdir_index]; + Assert( pval.isConst() ); + if( sargval.getConst<Rational>() < pval.getConst<Rational>() ){ + increment = true; + Trace("nl-ext-tf-mono") << "...increment at " << sarg << " since model value is less than " << mpoints[mdir_index] << std::endl; + } + } + if( increment ){ + tval = Node::null(); + monotonic_dir = mdirs[mdir_index]; + mono_bounds[1] = mpoints[mdir_index]; + mdir_index++; + if( mdir_index<mdirs.size() ){ + mono_bounds[0] = mpoints[mdir_index]; + }else{ + mono_bounds[0] = Node::null(); + } + } + } + + + 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 ) ); + }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 ) ); + } + 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 ); + } + Trace("nl-ext-tf-mono") << "Monotonicity lemma : " << mono_lem << std::endl; + lemmas.push_back( mono_lem ); + } + } + targ = sarg; + targval = sargval; + t = s; + tval = sval; + } + } + } + } + + + + + return lemmas; +} + + +Node NonlinearExtension::getTaylor( Node tf, Node x, unsigned n, std::vector< Node >& lemmas ) { + Node i_exp_base_term = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MINUS, x, tf[0] ) ); + Node i_exp_base = getFactorSkolem( i_exp_base_term, lemmas ); + Node i_derv = tf; + Node i_fact = d_one; + Node i_exp = d_one; + int i_derv_status = 0; + unsigned counter = 0; + std::vector< Node > sum; + do { + counter++; + if( tf.getKind()==kind::EXPONENTIAL ){ + //unchanged + }else if( tf.getKind()==kind::SINE ){ + if( i_derv_status%2==1 ){ + Node arg = NodeManager::currentNM()->mkNode( kind::MINUS, + NodeManager::currentNM()->mkNode( kind::MULT, + NodeManager::currentNM()->mkConst( Rational(1)/Rational(2) ), + NodeManager::currentNM()->mkNullaryOperator( NodeManager::currentNM()->realType(), kind::PI ) ), + tf[0] ); + i_derv = NodeManager::currentNM()->mkNode( kind::SINE, arg ); + }else{ + i_derv = tf; + } + if( i_derv_status>=2 ){ + i_derv = NodeManager::currentNM()->mkNode( kind::MINUS, d_zero, i_derv ); + } + i_derv = Rewriter::rewrite( i_derv ); + i_derv_status = i_derv_status==3 ? 0 : i_derv_status+1; + } + Node curr = NodeManager::currentNM()->mkNode( kind::MULT, + NodeManager::currentNM()->mkNode( kind::DIVISION, i_derv, i_fact ), i_exp ); + sum.push_back( curr ); + i_fact = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, NodeManager::currentNM()->mkConst( Rational( counter ) ) ) ); + i_exp = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::MULT, i_exp_base, i_exp ) ); + }while( counter<n ); + return sum.size()==1 ? sum[0] : NodeManager::currentNM()->mkNode( kind::PLUS, sum ); +} + } // namespace arith } // namespace theory } // namespace CVC4 diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index dc93046c0..1a19eb67a 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -86,17 +86,17 @@ class NonlinearExtension { // Check assertions for consistency in the effort LAST_CALL with a subset of // the assertions, false_asserts, evaluate to false in the current model. void checkLastCall(const std::vector<Node>& assertions, - const std::set<Node>& false_asserts); - - // Returns a vector containing a split on whether each term is 0 or not for - // those terms that have not been split on in the current context. - std::vector<Node> splitOnZeros(const std::vector<Node>& terms); + const std::set<Node>& false_asserts, + const std::vector<Node>& xts); static bool isArithKind(Kind k); static Node mkLit(Node a, Node b, int status, int orderType = 0); static Node mkAbs(Node a); + static Node mkValidPhase(Node a, Node pi); + static Node mkBounded( Node l, Node a, Node u ); static Kind joinKinds(Kind k1, Kind k2); static Kind transKinds(Kind k1, Kind k2); + static bool isTranscendentalKind(Kind k); Node mkMonomialRemFactor(Node n, const NodeMultiset& n_exp_rem) const; // register monomial @@ -171,6 +171,9 @@ class NonlinearExtension { // cache of all lemmas sent NodeSet d_lemmas; NodeSet d_zero_split; + + // literals with Skolems (need not be satisfied by model) + NodeSet d_skolem_atoms; // utilities Node d_zero; @@ -197,8 +200,71 @@ class NonlinearExtension { std::map<Node, Node> d_mv[2]; // ordering, stores variables and 0,1,-1 - std::map<unsigned, NodeMultiset> d_order_vars; + std::map<Node, unsigned> d_order_vars; std::vector<Node> d_order_points; + + //transcendent functions + std::map<Node, Node> d_trig_base; + std::map<Node, bool> d_trig_is_base; + std::map< Node, bool > d_tf_initial_refine; + Node d_pi; + Node d_pi_2; + Node d_pi_neg_2; + Node d_pi_neg; + Node d_pi_bound[2]; + + void mkPi(); + void getCurrentPiBounds( std::vector< Node >& lemmas ); +private: + //per last-call effort check + + //information about monomials + std::vector< Node > d_ms; + std::vector< Node > d_ms_vars; + std::map<Node, bool> d_ms_proc; + std::vector<Node> d_mterms; + //list of monomials with factors whose model value is non-constant in model + // e.g. y*cos( x ) + std::map<Node, bool> d_m_nconst_factor; + // If ( m, p1, true ), then it would help satisfiability if m were ( > + // if p1=true, < if p1=false ) + std::map<Node, std::map<bool, bool> > d_tplane_refine_dir; + // term -> coeff -> rhs -> ( status, exp, b ), + // where we have that : exp => ( coeff * term <status> rhs ) + // b is true if degree( term ) >= degree( rhs ) + std::map<Node, std::map<Node, std::map<Node, Kind> > > d_ci; + std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp; + std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max; + + //information about transcendental functions + std::map< Kind, std::map< Node, Node > > d_tf_rep_map; + + // factor skolems + std::map< Node, Node > d_factor_skolem; + Node getFactorSkolem( Node n, std::vector< Node >& lemmas ); + + Node getTaylor( Node tf, Node x, unsigned n, std::vector< Node >& lemmas ); +private: + // Returns a vector containing a split on whether each term is 0 or not for + // those terms that have not been split on in the current context. + std::vector<Node> checkSplitZero(); + + std::vector<Node> checkMonomialSign(); + + std::vector<Node> checkMonomialMagnitude( unsigned c ); + + std::vector<Node> checkMonomialInferBounds( std::vector<Node>& nt_lemmas, + const std::set<Node>& false_asserts ); + + std::vector<Node> checkFactoring( const std::set<Node>& false_asserts ); + + std::vector<Node> checkMonomialInferResBounds(); + + std::vector<Node> checkTangentPlanes(); + + std::vector<Node> checkTranscendentalInitialRefine(); + + std::vector<Node> checkTranscendentalMonotonic(); }; /* class NonlinearExtension */ } // namespace arith diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 605dfe495..ef22e1c0d 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -89,6 +89,19 @@ bool Variable::isDivMember(Node n){ } } +bool Variable::isTranscendentalMember(Node n) { + switch(n.getKind()){ + case kind::EXPONENTIAL: + case kind::SINE: + case kind::COSINE: + case kind::TANGENT: + return Polynomial::isMember(n[0]); + case kind::PI: + return true; + default: + return false; + } +} bool VarList::isSorted(iterator start, iterator end) { diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 4a2b6114f..d8f5259fc 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -245,6 +245,12 @@ public: case kind::INTS_MODULUS_TOTAL: case kind::DIVISION_TOTAL: return isDivMember(n); + case kind::EXPONENTIAL: + case kind::SINE: + case kind::COSINE: + case kind::TANGENT: + case kind::PI: + return isTranscendentalMember(n); case kind::ABS: case kind::TO_INTEGER: // Treat to_int as a variable; it is replaced in early preprocessing @@ -260,6 +266,7 @@ public: bool isDivLike() const{ return isDivMember(getNode()); } + static bool isTranscendentalMember(Node n); bool isNormalForm() { return isMember(getNode()); } diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index c0af3827e..985799e88 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -40,6 +40,11 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, if (options::nlExt()) { setupExtTheory(); getExtTheory()->addFunctionKind(kind::NONLINEAR_MULT); + getExtTheory()->addFunctionKind(kind::EXPONENTIAL); + getExtTheory()->addFunctionKind(kind::SINE); + getExtTheory()->addFunctionKind(kind::COSINE); + getExtTheory()->addFunctionKind(kind::TANGENT); + getExtTheory()->addFunctionKind(kind::PI); } } diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index c5e8de96a..5fb31e93f 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1454,7 +1454,6 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ } if( !options::nlExt() ){ - setIncomplete(); d_nlIncomplete = true; } @@ -1464,6 +1463,13 @@ void TheoryArithPrivate::setupVariableList(const VarList& vl){ //setupInitialValue(av); markSetup(vlNode); + }else{ + if( !options::nlExt() ){ + if( vlNode.getKind()==kind::EXPONENTIAL || vlNode.getKind()==kind::SINE || + vlNode.getKind()==kind::COSINE || vlNode.getKind()==kind::TANGENT ){ + d_nlIncomplete = true; + } + } } /* Note: @@ -3823,7 +3829,6 @@ void TheoryArithPrivate::check(Theory::Effort effortLevel){ } if(Theory::fullEffort(effortLevel) && d_nlIncomplete){ - // TODO this is total paranoia setIncomplete(); } @@ -4865,6 +4870,12 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) { NodeManager* nm = NodeManager::currentNM(); + // eliminate here since involves division + if( node.getKind()==kind::TANGENT ){ + node = nm->mkNode(kind::DIVISION, nm->mkNode( kind::SINE, node[0] ), + nm->mkNode( kind::COSINE, node[0] ) ); + } + switch(node.getKind()) { case kind::DIVISION: { // partial function: division diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index e13dee0fe..59c2aaa8f 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -93,6 +93,24 @@ public: } };/* class IntOperatorTypeRule */ +class RealOperatorTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + TNode::iterator child_it = n.begin(); + TNode::iterator child_it_end = n.end(); + if(check) { + for(; child_it != child_it_end; ++child_it) { + TypeNode childType = (*child_it).getType(check); + if (!childType.isReal()) { + throw TypeCheckingExceptionPrivate(n, "expecting a real subterm"); + } + } + } + return nodeManager->realType(); + } +};/* class RealOperatorTypeRule */ + class ArithPredicateTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) @@ -139,6 +157,21 @@ public: } };/* class IntUnaryPredicateTypeRule */ +class RealNullaryOperatorTypeRule { +public: + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + // for nullary operators, we only computeType for check=true, since they are given TypeAttr() on creation + Assert(check); + TypeNode realType = n.getType(); + if(realType!=NodeManager::currentNM()->realType()) { + throw TypeCheckingExceptionPrivate(n, "expecting real type"); + } + return realType; + } +};/* class RealNullaryOperatorTypeRule */ + + class SubrangeProperties { public: inline static Cardinality computeCardinality(TypeNode type) { |