From: ajreynol Date: Mon, 10 Jul 2017 21:22:19 +0000 (-0500) Subject: Merge ntExt branch. Adds support for transcendental functions. Refactoring of non... X-Git-Tag: cvc5-1.0.0~5729 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2c0482cfb9b8164670cf56187e127d38c5d05bcf;p=cvc5.git Merge ntExt branch. Adds support for transcendental functions. Refactoring of non-linear extension. Add factoring lemma scheme for non-linear. Add regressions. --- diff --git a/src/options/arith_options b/src/options/arith_options index 32310a495..bddde7a16 100644 --- a/src/options/arith_options +++ b/src/options/arith_options @@ -171,6 +171,9 @@ option nlExt --nl-ext bool :default true option nlExtResBound --nl-ext-rbound bool :default false use resolution-style inference for inferring new bounds +option nlExtFactor --nl-ext-factor bool :default true + use factoring inference in non-linear solver + option nlExtTangentPlanes --nl-ext-tplanes bool :default false use non-terminating tangent plane strategy for non-linear diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index fe5eb3ac8..674dbe49d 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -53,6 +53,12 @@ void Smt2::addArithmeticOperators() { Parser::addOperator(kind::LEQ); Parser::addOperator(kind::GT); Parser::addOperator(kind::GEQ); + + addOperator(kind::POW, "^"); + addOperator(kind::EXPONENTIAL, "exp"); + addOperator(kind::SINE, "sin"); + addOperator(kind::COSINE, "cos"); + addOperator(kind::TANGENT, "tan"); } void Smt2::addBitvectorOperators() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 074041262..2ba593377 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -383,6 +383,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::PLUS: case kind::MULT: case kind::NONLINEAR_MULT: + case kind::EXPONENTIAL: + case kind::SINE: + case kind::COSINE: + case kind::TANGENT: case kind::MINUS: case kind::UMINUS: case kind::LT: @@ -817,6 +821,10 @@ static string smtKindString(Kind k) throw() { case kind::PLUS: return "+"; case kind::MULT: case kind::NONLINEAR_MULT: return "*"; + case kind::EXPONENTIAL: return "exp"; + case kind::SINE: return "sin"; + case kind::COSINE: return "cos"; + case kind::TANGENT: return "tan"; case kind::MINUS: return "-"; case kind::UMINUS: return "-"; case kind::LT: return "<"; 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 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().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 product; + for( unsigned i=0; imkNode( 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(); + 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 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 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 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); + } + //Assert( ret.isConst() ); + } else if (n.getNumChildren() == 0) { + if( n.getKind()==kind::PI ){ + ret = n; + }else{ + 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()); + } else { + // otherwise, compute true value + std::vector 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 b, a b, we know a 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 children; @@ -1033,27 +1058,26 @@ std::set NonlinearExtension::getFalseInModel( std::set 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 NonlinearExtension::splitOnZeros( - const std::vector& ms_vars) { +std::vector NonlinearExtension::checkSplitZero() { std::vector 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 NonlinearExtension::splitOnZeros( } void NonlinearExtension::checkLastCall(const std::vector& assertions, - const std::set& false_asserts) { - // processed monomials - std::map ms_proc; - - // list of monomials - std::vector ms; - d_containing.getExtTheory()->getTerms(ms); - // list of variables occurring in monomials - std::vector 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& false_asserts, + const std::vector& 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 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 " << d_mv[1][a] << " [" - << d_mv[0][a] << "]" << std::endl; - - std::map >::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 >::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& assertions, computeModelValue(c, 1); } - int lemmas_proc; - std::vector 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 + 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; + } } - // possibly split on zero? - lemmas = splitOnZeros(ms_vars); + //-----------------------------------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 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 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 > > 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 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::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 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::iterator itmeb = - d_m_exp.find(b); - Assert(itmeb != d_m_exp.end()); - - std::vector 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 r_lemmas; - for (std::map > >::iterator itb = - cmp_infers.begin(); - itb != cmp_infers.end(); ++itb) { - for (std::map >::iterator itc = - itb->second.begin(); - itc != itb->second.end(); ++itc) { - for (std::map::iterator itc2 = itc->second.begin(); - itc2 != itc->second.end(); ++itc2) { - std::map visited; - for (std::map::iterator itc3 = itc->second.begin(); - itc3 != itc->second.end(); ++itc3) { - if (itc3->first != itc2->first) { - std::vector 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 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 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 rhs ) - // b is true if degree( term ) >= degree( rhs ) - std::map > > ci; - std::map > > ci_exp; - std::map > > ci_max; - - // If ( m, p1, true ), then it would help satisfiability if m were ( > - // if p1=true, < if p1=false ) - std::map > tplane_refine_dir; - - // register constraints - Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; - for (context::CDList::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 >::iterator itc = - d_c_info.find(atom); - std::map >::iterator itcm = - d_c_info_maxm.find(atom); - if (itc != d_c_info.end()) { - Assert(itcm != d_c_info_maxm.end()); - for (std::map::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::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() > rhs_v.getConst()) { - 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 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 >::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 > >::iterator itc = - ci.find(x); - if (itc != ci.end()) { - for (std::map >::iterator itcc = - itc->second.begin(); - itcc != itc->second.end(); ++itcc) { - Node coeff = itcc->first; - Node t = QuantArith::mkCoeffTerm(coeff, x); - for (std::map::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 t => m*x 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().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& assertions, << std::endl; return; } + + // 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; + } + } - //------------------------------------resolution bound inferences, e.g. - //( - // y>=0 ^ s <= x*z ^ x*y <= t ) => y*s <= z*t + //------------------------------------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 > >::iterator itca = - ci.find(a); - if (itca != ci.end()) { - for (unsigned k = (j + 1); k < terms.size(); k++) { - Node b = terms[k]; - std::map > >::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::iterator ita = d_mono_diff[a].find(b); - if (ita != d_mono_diff[a].end()) { - std::map::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().sgn(); - Assert(mv_a_sgn != 0); - Node mv_b = computeModelValue(itb->second, 1); - Assert(mv_b.isConst()); - int mv_b_sgn = mv_b.getConst().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 exp; - // bounds of a - for (std::map >::iterator itcac = - itca->second.begin(); - itcac != itca->second.end(); ++itcac) { - Node coeff_a = itcac->first; - for (std::map::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 >::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::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 = checkMonomialInferResBounds(); 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; } } - - // from inferred bound inferences - lemmas_proc = flushLemmas(nt_lemmas); - if (lemmas_proc > 0) { - Trace("nl-ext") << " ...finished with " << lemmas_proc - << " new (monomial-introducing) lemmas." << std::endl; - return; - } - + + //------------------------------------tangent planes 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 >::iterator it = - d_m_contain_children.find(t); - if (it != d_m_contain_children.end()) { - std::map > 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; + 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 false_asserts = getFalseInModel(assertions); + + std::vector 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& 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& 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& exp, std::vector& 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().sgn(); + Assert( d_mv[1].find(av) != d_mv[0].end() ); + Assert( d_mv[1][av].isConst() ); + int sgn = d_mv[1][av].getConst().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 NonlinearExtension::checkMonomialSign() { + std::vector lemmas; + std::map 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 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 NonlinearExtension::checkMonomialMagnitude( unsigned c ) { + unsigned r = 1; + std::vector lemmas; +// if (x,y,L) in cmp_infers, then x > y inferred as conclusion of L + // in lemmas + std::map > > 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 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::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 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::iterator itmeb = + d_m_exp.find(b); + Assert(itmeb != d_m_exp.end()); + + std::vector 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 r_lemmas; + for (std::map > >::iterator itb = + cmp_infers.begin(); + itb != cmp_infers.end(); ++itb) { + for (std::map >::iterator itc = + itb->second.begin(); + itc != itb->second.end(); ++itc) { + for (std::map::iterator itc2 = itc->second.begin(); + itc2 != itc->second.end(); ++itc2) { + std::map visited; + for (std::map::iterator itc3 = itc->second.begin(); + itc3 != itc->second.end(); ++itc3) { + if (itc3->first != itc2->first) { + std::vector 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 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 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 >::iterator it = + d_m_contain_children.find(t); + if (it != d_m_contain_children.end()) { + std::map > 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 NonlinearExtension::checkMonomialInferBounds( std::vector& nt_lemmas, + const std::set& false_asserts ) { + std::vector< Node > lemmas; + // register constraints + Trace("nl-ext-debug") << "Register bound constraints..." << std::endl; + for (context::CDList::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 >::iterator itc = + d_c_info.find(atom); + std::map >::iterator itcm = + d_c_info_maxm.find(atom); + if (itc != d_c_info.end()) { + Assert(itcm != d_c_info_maxm.end()); + for (std::map::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::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() > rhs_v.getConst()) { + 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 >::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 > >::iterator itc = + d_ci.find(x); + if (itc != d_ci.end()) { + for (std::map >::iterator itcc = + itc->second.begin(); + itcc != itc->second.end(); ++itcc) { + Node coeff = itcc->first; + Node t = QuantArith::mkCoeffTerm(coeff, x); + for (std::map::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 t => m*x 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().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 NonlinearExtension::checkFactoring( const std::set& false_asserts ) { + std::vector< Node > lemmas; + Trace("nl-ext") << "Get factoring lemmas..." << std::endl; + for (context::CDList::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 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::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; ifirst.getNumChildren(); i++ ){ + children.push_back( itm->first[i] ); + } + std::map< Node, bool > processed; + for( unsigned i=0; ifirst.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::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 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 > >::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 > >::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::iterator ita = d_mono_diff[a].find(b); + if (ita != d_mono_diff[a].end()) { + std::map::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().sgn(); + Assert(mv_a_sgn != 0); + Node mv_b = computeModelValue(itb->second, 1); + Assert(mv_b.isConst()); + int mv_b_sgn = mv_b.getConst().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 exp; + // bounds of a + for (std::map >::iterator itcac = + itca->second.begin(); + itcac != itca->second.end(); ++itcac) { + Node coeff_a = itcac->first; + for (std::map::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 >::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::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 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() > d_one.getConst() ){ + lemmas.push_back( NodeManager::currentNM()->mkNode( kind::LEQ, t, d_one ) ); + }else if( tv.getConst() < d_neg_one.getConst() ){ + lemmas.push_back( NodeManager::currentNM()->mkNode( kind::GEQ, t, d_neg_one ) ); + } + */ + /* + if( tv.getConst().sgn()!=0 ){ + //symmetry (model-based) + Node neg_tv = NodeManager::currentNM()->mkConst( -tv.getConst() ); + 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().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().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 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; ifirst].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; ifirst].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() < pval.getConst() ){ + 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() > tval.getConst() ){ + 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() < tval.getConst() ){ + 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( countermkNode( 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& assertions, - const std::set& 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 splitOnZeros(const std::vector& terms); + const std::set& false_asserts, + const std::vector& 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 d_mv[2]; // ordering, stores variables and 0,1,-1 - std::map d_order_vars; + std::map d_order_vars; std::vector d_order_points; + + //transcendent functions + std::map d_trig_base; + std::map 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 d_ms_proc; + std::vector d_mterms; + //list of monomials with factors whose model value is non-constant in model + // e.g. y*cos( x ) + std::map d_m_nconst_factor; + // If ( m, p1, true ), then it would help satisfiability if m were ( > + // if p1=true, < if p1=false ) + std::map > d_tplane_refine_dir; + // term -> coeff -> rhs -> ( status, exp, b ), + // where we have that : exp => ( coeff * term rhs ) + // b is true if degree( term ) >= degree( rhs ) + std::map > > d_ci; + std::map > > d_ci_exp; + std::map > > 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 checkSplitZero(); + + std::vector checkMonomialSign(); + + std::vector checkMonomialMagnitude( unsigned c ); + + std::vector checkMonomialInferBounds( std::vector& nt_lemmas, + const std::set& false_asserts ); + + std::vector checkFactoring( const std::set& false_asserts ); + + std::vector checkMonomialInferResBounds(); + + std::vector checkTangentPlanes(); + + std::vector checkTranscendentalInitialRefine(); + + std::vector 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) { diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index 53e04a1ef..e8bff57bd 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -49,7 +49,22 @@ TESTS = \ bug698.smt2 \ real-div-ufnra.smt2 \ div-mod-partial.smt2 \ - all-logic.smt2 + all-logic.smt2 \ + nta/bad-050217.smt2 \ + nta/cos-bound.smt2 \ + nta/cos-sig-value.smt2 \ + nta/exp_monotone.smt2 \ + nta/shifting2.smt2 \ + nta/shifting.smt2 \ + nta/sin-compare-across-phase.smt2 \ + nta/sin-compare.smt2 \ + nta/sin-sign.smt2 \ + nta/sin-sym2.smt2 \ + nta/sin-sym.smt2 \ + nta/tan-rewrite2.smt2 \ + nta/tan-rewrite.smt2 \ + nta/arrowsmith-050317.smt2 \ + nta/sin-init-tangents.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/nl/nta/arrowsmith-050317.smt2 b/test/regress/regress0/nl/nta/arrowsmith-050317.smt2 new file mode 100644 index 000000000..04b06e1f5 --- /dev/null +++ b/test/regress/regress0/nl/nta/arrowsmith-050317.smt2 @@ -0,0 +1,95 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.location.0__AT0@0 () Bool) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun instance.location.0__AT0@4 () Bool) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.location.0__AT0@1 () Bool) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun time__AT0@1 () Real) +(declare-fun event_is_timed__AT0@3 () Bool) +(declare-fun instance.location.0__AT0@3 () Bool) +(declare-fun instance.x__AT0@3 () Real) +(declare-fun instance.y__AT0@3 () Real) +(declare-fun instance.EVENT.0__AT0@2 () Bool) +(declare-fun instance.EVENT.1__AT0@2 () Bool) +(declare-fun time__AT0@3 () Real) +(declare-fun event_is_timed__AT0@2 () Bool) +(declare-fun instance.location.0__AT0@2 () Bool) +(declare-fun instance.x__AT0@2 () Real) +(declare-fun instance.y__AT0@2 () Real) +(declare-fun instance.EVENT.0__AT0@1 () Bool) +(declare-fun instance.EVENT.1__AT0@1 () Bool) +(declare-fun time__AT0@2 () Real) +(declare-fun event_is_timed__AT0@4 () Bool) +(declare-fun instance.x__AT0@4 () Real) +(declare-fun instance.y__AT0@4 () Real) +(declare-fun instance.EVENT.0__AT0@3 () Bool) +(declare-fun instance.EVENT.1__AT0@3 () Bool) +(declare-fun time__AT0@4 () Real) +(assert (let ((.def_0 (not instance.EVENT.1__AT0@3))) (let ((.def_1 (not instance.EVENT.0__AT0@3))) (let ((.def_2 (or .def_1 .def_0))) (let ((.def_3 (= event_is_timed__AT0@3 instance.EVENT.1__AT0@3))) (let ((.def_4 (<= time__AT0@3 +time__AT0@4))) (let ((.def_5 (or .def_0 .def_4))) (let ((.def_6 (and .def_5 .def_3))) (let ((.def_7 (= time__AT0@3 time__AT0@4))) (let ((.def_8 (or instance.EVENT.1__AT0@3 .def_7))) (let ((.def_9 (and .def_8 .def_6))) (let +((.def_10 (<= instance.x__AT0@3 0.0))) (let ((.def_11 (not .def_10))) (let ((.def_12 (not instance.location.0__AT0@3))) (let ((.def_13 (and .def_12 .def_11))) (let ((.def_14 (and instance.location.0__AT0@4 .def_13))) (let ((.def_15 +(= instance.x__AT0@3 instance.x__AT0@4))) (let ((.def_16 (and .def_15 .def_14))) (let ((.def_17 (= instance.y__AT0@3 instance.y__AT0@4))) (let ((.def_18 (and .def_17 .def_16))) (let ((.def_19 (<= instance.y__AT0@3 0.0))) (let +((.def_20 (and .def_12 .def_19))) (let ((.def_21 (and instance.location.0__AT0@4 .def_20))) (let ((.def_22 (and .def_15 .def_21))) (let ((.def_23 (and .def_17 .def_22))) (let ((.def_24 (or .def_23 .def_18))) (let ((.def_25 (and +.def_7 .def_24))) (let ((.def_26 (or instance.EVENT.1__AT0@3 .def_25))) (let ((.def_27 (not .def_7))) (let ((.def_28 (and .def_15 .def_17))) (let ((.def_29 (or .def_28 .def_27))) (let ((.def_30 (and .def_28 .def_29))) (let +((.def_31 (or .def_30 .def_12))) (let ((.def_32 (* (- 1.0) time__AT0@3))) (let ((.def_33 (+ .def_32 time__AT0@4))) (let ((.def_34 (exp .def_33))) (let ((.def_35 (* instance.x__AT0@3 .def_34))) (let ((.def_36 (= instance.x__AT0@4 +.def_35))) (let ((.def_37 (* 2.0 instance.x__AT0@4))) (let ((.def_38 (* instance.y__AT0@4 .def_37))) (let ((.def_39 (* (- 1.0) .def_38))) (let ((.def_40 (* 2.0 instance.x__AT0@3))) (let ((.def_41 (* instance.y__AT0@3 .def_40))) +(let ((.def_42 (* (- 1.0) .def_41))) (let ((.def_43 (+ instance.y__AT0@3 .def_42))) (let ((.def_44 (* .def_43 .def_34))) (let ((.def_45 (* (- 1.0) .def_44))) (let ((.def_46 (+ .def_45 .def_39))) (let ((.def_47 (+ instance.y__AT0@4 +.def_46))) (let ((.def_48 (= .def_47 0.0))) (let ((.def_49 (and .def_48 .def_36))) (let ((.def_50 (and .def_49 .def_29))) (let ((.def_51 (or instance.location.0__AT0@3 .def_50))) (let ((.def_52 (and .def_51 .def_31))) (let +((.def_53 (and .def_52 .def_4))) (let ((.def_54 (= instance.location.0__AT0@4 instance.location.0__AT0@3))) (let ((.def_55 (and .def_54 .def_53))) (let ((.def_56 (or .def_0 .def_55))) (let ((.def_57 (and .def_56 .def_26))) (let +((.def_58 (and .def_1 .def_0))) (let ((.def_59 (or .def_58 .def_57))) (let ((.def_60 (and .def_59 .def_9))) (let ((.def_61 (not .def_58))) (let ((.def_62 (and .def_54 .def_15))) (let ((.def_63 (and .def_62 .def_17))) (let ((.def_64 +(or .def_63 .def_61))) (let ((.def_65 (and .def_64 .def_60))) (let ((.def_66 (not event_is_timed__AT0@3))) (let ((.def_67 (= event_is_timed__AT0@4 .def_66))) (let ((.def_68 (and .def_67 .def_65))) (let ((.def_69 (and .def_68 +.def_2))) (let ((.def_70 (not instance.EVENT.1__AT0@2))) (let ((.def_71 (not instance.EVENT.0__AT0@2))) (let ((.def_72 (or .def_71 .def_70))) (let ((.def_73 (= event_is_timed__AT0@2 instance.EVENT.1__AT0@2))) (let ((.def_74 (<= +time__AT0@2 time__AT0@3))) (let ((.def_75 (or .def_70 .def_74))) (let ((.def_76 (and .def_75 .def_73))) (let ((.def_77 (= time__AT0@2 time__AT0@3))) (let ((.def_78 (or instance.EVENT.1__AT0@2 .def_77))) (let ((.def_79 (and .def_78 +.def_76))) (let ((.def_80 (<= instance.x__AT0@2 0.0))) (let ((.def_81 (not .def_80))) (let ((.def_82 (not instance.location.0__AT0@2))) (let ((.def_83 (and .def_82 .def_81))) (let ((.def_84 (and instance.location.0__AT0@3 +.def_83))) (let ((.def_85 (= instance.x__AT0@2 instance.x__AT0@3))) (let ((.def_86 (and .def_85 .def_84))) (let ((.def_87 (= instance.y__AT0@2 instance.y__AT0@3))) (let ((.def_88 (and .def_87 .def_86))) (let ((.def_89 (<= +instance.y__AT0@2 0.0))) (let ((.def_90 (and .def_82 .def_89))) (let ((.def_91 (and instance.location.0__AT0@3 .def_90))) (let ((.def_92 (and .def_85 .def_91))) (let ((.def_93 (and .def_87 .def_92))) (let ((.def_94 (or .def_93 +.def_88))) (let ((.def_95 (and .def_77 .def_94))) (let ((.def_96 (or instance.EVENT.1__AT0@2 .def_95))) (let ((.def_97 (not .def_77))) (let ((.def_98 (and .def_85 .def_87))) (let ((.def_99 (or .def_98 .def_97))) (let ((.def_100 +(and .def_98 .def_99))) (let ((.def_101 (or .def_100 .def_82))) (let ((.def_102 (* (- 1.0) time__AT0@2))) (let ((.def_103 (+ .def_102 time__AT0@3))) (let ((.def_104 (exp .def_103))) (let ((.def_105 (* instance.x__AT0@2 .def_104))) +(let ((.def_106 (= instance.x__AT0@3 .def_105))) (let ((.def_107 (* 2.0 instance.x__AT0@2))) (let ((.def_108 (* instance.y__AT0@2 .def_107))) (let ((.def_109 (* (- 1.0) .def_108))) (let ((.def_110 (+ instance.y__AT0@2 .def_109))) +(let ((.def_111 (* .def_110 .def_104))) (let ((.def_112 (* (- 1.0) .def_111))) (let ((.def_113 (+ .def_112 .def_42))) (let ((.def_114 (+ instance.y__AT0@3 .def_113))) (let ((.def_115 (= .def_114 0.0))) (let ((.def_116 (and .def_115 +.def_106))) (let ((.def_117 (and .def_116 .def_99))) (let ((.def_118 (or instance.location.0__AT0@2 .def_117))) (let ((.def_119 (and .def_118 .def_101))) (let ((.def_120 (and .def_119 .def_74))) (let ((.def_121 (= +instance.location.0__AT0@2 instance.location.0__AT0@3))) (let ((.def_122 (and .def_121 .def_120))) (let ((.def_123 (or .def_70 .def_122))) (let ((.def_124 (and .def_123 .def_96))) (let ((.def_125 (and .def_71 .def_70))) (let +((.def_126 (or .def_125 .def_124))) (let ((.def_127 (and .def_126 .def_79))) (let ((.def_128 (not .def_125))) (let ((.def_129 (and .def_121 .def_85))) (let ((.def_130 (and .def_129 .def_87))) (let ((.def_131 (or .def_130 +.def_128))) (let ((.def_132 (and .def_131 .def_127))) (let ((.def_133 (not event_is_timed__AT0@2))) (let ((.def_134 (= event_is_timed__AT0@3 .def_133))) (let ((.def_135 (and .def_134 .def_132))) (let ((.def_136 (and .def_135 +.def_72))) (let ((.def_137 (not instance.EVENT.1__AT0@1))) (let ((.def_138 (not instance.EVENT.0__AT0@1))) (let ((.def_139 (or .def_138 .def_137))) (let ((.def_140 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_141 +(<= time__AT0@1 time__AT0@2))) (let ((.def_142 (or .def_137 .def_141))) (let ((.def_143 (and .def_142 .def_140))) (let ((.def_144 (= time__AT0@1 time__AT0@2))) (let ((.def_145 (or instance.EVENT.1__AT0@1 .def_144))) (let ((.def_146 +(and .def_145 .def_143))) (let ((.def_147 (<= instance.x__AT0@1 0.0))) (let ((.def_148 (not .def_147))) (let ((.def_149 (not instance.location.0__AT0@1))) (let ((.def_150 (and .def_149 .def_148))) (let ((.def_151 (and +instance.location.0__AT0@2 .def_150))) (let ((.def_152 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_153 (and .def_152 .def_151))) (let ((.def_154 (= instance.y__AT0@1 instance.y__AT0@2))) (let ((.def_155 (and .def_154 +.def_153))) (let ((.def_156 (<= instance.y__AT0@1 0.0))) (let ((.def_157 (and .def_149 .def_156))) (let ((.def_158 (and instance.location.0__AT0@2 .def_157))) (let ((.def_159 (and .def_152 .def_158))) (let ((.def_160 (and .def_154 +.def_159))) (let ((.def_161 (or .def_160 .def_155))) (let ((.def_162 (and .def_144 .def_161))) (let ((.def_163 (or instance.EVENT.1__AT0@1 .def_162))) (let ((.def_164 (not .def_144))) (let ((.def_165 (and .def_152 .def_154))) (let +((.def_166 (or .def_165 .def_164))) (let ((.def_167 (and .def_165 .def_166))) (let ((.def_168 (or .def_167 .def_149))) (let ((.def_169 (* (- 1.0) time__AT0@1))) (let ((.def_170 (+ .def_169 time__AT0@2))) (let ((.def_171 (exp +.def_170))) (let ((.def_172 (* instance.x__AT0@1 .def_171))) (let ((.def_173 (= instance.x__AT0@2 .def_172))) (let ((.def_174 (* 2.0 instance.x__AT0@1))) (let ((.def_175 (* instance.y__AT0@1 .def_174))) (let ((.def_176 (* (- 1.0) +.def_175))) (let ((.def_177 (+ instance.y__AT0@1 .def_176))) (let ((.def_178 (* .def_177 .def_171))) (let ((.def_179 (* (- 1.0) .def_178))) (let ((.def_180 (+ .def_179 .def_109))) (let ((.def_181 (+ instance.y__AT0@2 .def_180))) +(let ((.def_182 (= .def_181 0.0))) (let ((.def_183 (and .def_182 .def_173))) (let ((.def_184 (and .def_183 .def_166))) (let ((.def_185 (or instance.location.0__AT0@1 .def_184))) (let ((.def_186 (and .def_185 .def_168))) (let +((.def_187 (and .def_186 .def_141))) (let ((.def_188 (= instance.location.0__AT0@1 instance.location.0__AT0@2))) (let ((.def_189 (and .def_188 .def_187))) (let ((.def_190 (or .def_137 .def_189))) (let ((.def_191 (and .def_190 +.def_163))) (let ((.def_192 (and .def_138 .def_137))) (let ((.def_193 (or .def_192 .def_191))) (let ((.def_194 (and .def_193 .def_146))) (let ((.def_195 (not .def_192))) (let ((.def_196 (and .def_188 .def_152))) (let ((.def_197 +(and .def_196 .def_154))) (let ((.def_198 (or .def_197 .def_195))) (let ((.def_199 (and .def_198 .def_194))) (let ((.def_200 (not event_is_timed__AT0@1))) (let ((.def_201 (= event_is_timed__AT0@2 .def_200))) (let ((.def_202 (and +.def_201 .def_199))) (let ((.def_203 (and .def_202 .def_139))) (let ((.def_204 (not instance.EVENT.1__AT0@0))) (let ((.def_205 (not instance.EVENT.0__AT0@0))) (let ((.def_206 (or .def_205 .def_204))) (let ((.def_207 (= +event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_208 (<= time__AT0@0 time__AT0@1))) (let ((.def_209 (or .def_204 .def_208))) (let ((.def_210 (and .def_209 .def_207))) (let ((.def_211 (= time__AT0@0 time__AT0@1))) (let +((.def_212 (or instance.EVENT.1__AT0@0 .def_211))) (let ((.def_213 (and .def_212 .def_210))) (let ((.def_214 (<= instance.x__AT0@0 0.0))) (let ((.def_215 (not .def_214))) (let ((.def_216 (not instance.location.0__AT0@0))) (let +((.def_217 (and .def_216 .def_215))) (let ((.def_218 (and instance.location.0__AT0@1 .def_217))) (let ((.def_219 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_220 (and .def_219 .def_218))) (let ((.def_221 (= +instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_222 (and .def_221 .def_220))) (let ((.def_223 (<= instance.y__AT0@0 0.0))) (let ((.def_224 (and .def_216 .def_223))) (let ((.def_225 (and instance.location.0__AT0@1 .def_224))) +(let ((.def_226 (and .def_219 .def_225))) (let ((.def_227 (and .def_221 .def_226))) (let ((.def_228 (or .def_227 .def_222))) (let ((.def_229 (and .def_211 .def_228))) (let ((.def_230 (or instance.EVENT.1__AT0@0 .def_229))) (let +((.def_231 (not .def_211))) (let ((.def_232 (and .def_219 .def_221))) (let ((.def_233 (or .def_232 .def_231))) (let ((.def_234 (and .def_232 .def_233))) (let ((.def_235 (or .def_216 .def_234))) (let ((.def_236 (* (- 1.0) +time__AT0@0))) (let ((.def_237 (+ .def_236 time__AT0@1))) (let ((.def_238 (exp .def_237))) (let ((.def_239 (* instance.x__AT0@0 .def_238))) (let ((.def_240 (= instance.x__AT0@1 .def_239))) (let ((.def_241 (* 2.0 +instance.x__AT0@0))) (let ((.def_242 (* instance.y__AT0@0 .def_241))) (let ((.def_243 (* (- 1.0) .def_242))) (let ((.def_244 (+ instance.y__AT0@0 .def_243))) (let ((.def_245 (* .def_244 .def_238))) (let ((.def_246 (* (- 1.0) +.def_245))) (let ((.def_247 (+ .def_246 .def_176))) (let ((.def_248 (+ instance.y__AT0@1 .def_247))) (let ((.def_249 (= .def_248 0.0))) (let ((.def_250 (and .def_249 .def_240))) (let ((.def_251 (and .def_250 .def_233))) (let +((.def_252 (or instance.location.0__AT0@0 .def_251))) (let ((.def_253 (and .def_252 .def_235))) (let ((.def_254 (and .def_253 .def_208))) (let ((.def_255 (= instance.location.0__AT0@0 instance.location.0__AT0@1))) (let ((.def_256 +(and .def_255 .def_254))) (let ((.def_257 (or .def_204 .def_256))) (let ((.def_258 (and .def_257 .def_230))) (let ((.def_259 (and .def_205 .def_204))) (let ((.def_260 (or .def_259 .def_258))) (let ((.def_261 (and .def_260 +.def_213))) (let ((.def_262 (not .def_259))) (let ((.def_263 (and .def_255 .def_219))) (let ((.def_264 (and .def_263 .def_221))) (let ((.def_265 (or .def_264 .def_262))) (let ((.def_266 (and .def_265 .def_261))) (let ((.def_267 +(not event_is_timed__AT0@0))) (let ((.def_268 (= event_is_timed__AT0@1 .def_267))) (let ((.def_269 (and .def_268 .def_266))) (let ((.def_270 (and .def_269 .def_206))) (let ((.def_271 (= instance.x__AT0@0 (- 1.0)))) (let ((.def_272 +(= instance.y__AT0@0 1.0))) (let ((.def_273 (and .def_272 .def_271))) (let ((.def_274 (and .def_216 .def_273))) (let ((.def_275 (= time__AT0@0 0.0))) (let ((.def_276 (and .def_275 .def_274))) (let ((.def_277 (and .def_276 .def_270 +.def_203 .def_136 .def_69 instance.location.0__AT0@4))) +.def_277))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/nta/bad-050217.smt2 b/test/regress/regress0/nl/nta/bad-050217.smt2 new file mode 100644 index 000000000..3b9310748 --- /dev/null +++ b/test/regress/regress0/nl/nta/bad-050217.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun time__AT0@1 () Real) +(assert (let ((.def_0 (<= 0.0 instance.x__AT0@1))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@0))) (let ((.def_3 (not instance.EVENT.0__AT0@0))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_6 (<= time__AT0@0 time__AT0@1))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@0 time__AT0@1))) (let ((.def_10 (or instance.EVENT.1__AT0@0 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) instance.y__AT0@0))) (let ((.def_13 (+ instance.x__AT0@0 .def_12))) (let ((.def_14 (* (- 1.0) time__AT0@0))) (let ((.def_15 (+ .def_14 time__AT0@1))) (let ((.def_16 (exp .def_15))) (let ((.def_17 (* .def_16 .def_13))) (let ((.def_18 (* (- 1.0) .def_17))) (let ((.def_19 (* (- 1.0) instance.y__AT0@1))) (let ((.def_20 (+ .def_19 .def_18))) (let ((.def_21 (+ instance.x__AT0@1 .def_20))) (let ((.def_22 (= .def_21 0.0))) (let ((.def_23 (+ instance.y__AT0@0 instance.x__AT0@0))) (let ((.def_24 (* .def_23 .def_16))) (let ((.def_25 (* (- 1.0) .def_24))) (let ((.def_26 (+ instance.y__AT0@1 .def_25))) (let ((.def_27 (+ instance.x__AT0@1 .def_26))) (let ((.def_28 (= .def_27 0.0))) (let ((.def_29 (and .def_28 .def_22))) (let ((.def_30 (not .def_9))) (let ((.def_31 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_32 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_33 (and .def_32 .def_31))) (let ((.def_34 (or .def_33 .def_30))) (let ((.def_35 (and .def_34 .def_29))) (let ((.def_36 (and .def_35 .def_6))) (let ((.def_37 (or .def_2 .def_36))) (let ((.def_38 (and .def_37 .def_10))) (let ((.def_39 (and .def_3 .def_2))) (let ((.def_40 (or .def_39 .def_38))) (let ((.def_41 (and .def_40 .def_11))) (let ((.def_42 (not .def_39))) (let ((.def_43 (or .def_42 .def_33))) (let ((.def_44 (and .def_43 .def_41))) (let ((.def_45 (not event_is_timed__AT0@0))) (let ((.def_46 (= event_is_timed__AT0@1 .def_45))) (let ((.def_47 (and .def_46 .def_44))) (let ((.def_48 (and .def_47 .def_4))) (let ((.def_49 (= instance.x__AT0@0 1.0))) (let ((.def_50 (= instance.y__AT0@0 0.0))) (let ((.def_51 (and .def_50 .def_49))) (let ((.def_52 (= time__AT0@0 0.0))) (let ((.def_53 (and .def_52 .def_51))) (let ((.def_54 (and .def_53 .def_48 .def_1))) .def_54)))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/nta/cos-bound.smt2 b/test/regress/regress0/nl/nta/cos-bound.smt2 new file mode 100644 index 000000000..e19260d63 --- /dev/null +++ b/test/regress/regress0/nl/nta/cos-bound.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(declare-fun x () Real) +(assert (> (cos x) 1.0)) +(check-sat) diff --git a/test/regress/regress0/nl/nta/cos-sig-value.smt2 b/test/regress/regress0/nl/nta/cos-sig-value.smt2 new file mode 100644 index 000000000..e1baeed9c --- /dev/null +++ b/test/regress/regress0/nl/nta/cos-sig-value.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (not (= (cos 0.0) 1.0))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/dumortier-050317.smt2 b/test/regress/regress0/nl/nta/dumortier-050317.smt2 new file mode 100644 index 000000000..04c498ca0 --- /dev/null +++ b/test/regress/regress0/nl/nta/dumortier-050317.smt2 @@ -0,0 +1,38 @@ +(set-logic QF_NRA) +(declare-fun time__AT0@0 () Real) +(declare-fun instance.y__AT0@0 () Real) +(declare-fun instance.x__AT0@0 () Real) +(declare-fun event_is_timed__AT0@3 () Bool) +(declare-fun instance.EVENT.0__AT0@2 () Bool) +(declare-fun instance.EVENT.1__AT0@2 () Bool) +(declare-fun instance.y__AT0@3 () Real) +(declare-fun instance.x__AT0@3 () Real) +(declare-fun time__AT0@3 () Real) +(declare-fun instance.y__AT0@5 () Real) +(declare-fun event_is_timed__AT0@1 () Bool) +(declare-fun event_is_timed__AT0@0 () Bool) +(declare-fun instance.EVENT.0__AT0@0 () Bool) +(declare-fun instance.EVENT.1__AT0@0 () Bool) +(declare-fun instance.y__AT0@1 () Real) +(declare-fun instance.x__AT0@1 () Real) +(declare-fun time__AT0@1 () Real) +(declare-fun event_is_timed__AT0@4 () Bool) +(declare-fun instance.EVENT.0__AT0@3 () Bool) +(declare-fun instance.EVENT.1__AT0@3 () Bool) +(declare-fun instance.y__AT0@4 () Real) +(declare-fun instance.x__AT0@4 () Real) +(declare-fun time__AT0@4 () Real) +(declare-fun event_is_timed__AT0@2 () Bool) +(declare-fun instance.EVENT.0__AT0@1 () Bool) +(declare-fun instance.EVENT.1__AT0@1 () Bool) +(declare-fun instance.y__AT0@2 () Real) +(declare-fun instance.x__AT0@2 () Real) +(declare-fun time__AT0@2 () Real) +(declare-fun event_is_timed__AT0@5 () Bool) +(declare-fun instance.EVENT.0__AT0@4 () Bool) +(declare-fun instance.EVENT.1__AT0@4 () Bool) +(declare-fun instance.x__AT0@5 () Real) +(declare-fun time__AT0@5 () Real) +(assert (let ((.def_0 (<= instance.y__AT0@5 2.0))) (let ((.def_1 (not .def_0))) (let ((.def_2 (not instance.EVENT.1__AT0@4))) (let ((.def_3 (not instance.EVENT.0__AT0@4))) (let ((.def_4 (or .def_3 .def_2))) (let ((.def_5 (= event_is_timed__AT0@4 instance.EVENT.1__AT0@4))) (let ((.def_6 (<= time__AT0@4 time__AT0@5))) (let ((.def_7 (or .def_2 .def_6))) (let ((.def_8 (and .def_7 .def_5))) (let ((.def_9 (= time__AT0@4 time__AT0@5))) (let ((.def_10 (or instance.EVENT.1__AT0@4 .def_9))) (let ((.def_11 (and .def_10 .def_8))) (let ((.def_12 (* (- 1.0) time__AT0@4))) (let ((.def_13 (+ .def_12 time__AT0@5))) (let ((.def_14 (exp .def_13))) (let ((.def_15 (* instance.y__AT0@4 .def_14))) (let ((.def_16 (= instance.y__AT0@5 .def_15))) (let ((.def_17 (* 970143.0 instance.x__AT0@5))) (let ((.def_18 (* (- 970143.0) instance.x__AT0@4))) (let ((.def_19 (+ .def_18 .def_17))) (let ((.def_20 (* (- 242536.0) instance.y__AT0@4))) (let ((.def_21 (+ .def_20 .def_19))) (let ((.def_22 (* 242536.0 instance.y__AT0@5))) (let ((.def_23 (+ .def_22 .def_21))) (let ((.def_24 (= .def_23 0.0))) (let ((.def_25 (and .def_24 .def_16))) (let ((.def_26 (not .def_9))) (let ((.def_27 (= instance.x__AT0@4 instance.x__AT0@5))) (let ((.def_28 (= instance.y__AT0@5 instance.y__AT0@4))) (let ((.def_29 (and .def_28 .def_27))) (let ((.def_30 (or .def_29 .def_26))) (let ((.def_31 (and .def_30 .def_25))) (let ((.def_32 (and .def_31 .def_6))) (let ((.def_33 (or .def_2 .def_32))) (let ((.def_34 (and .def_33 .def_10))) (let ((.def_35 (and .def_3 .def_2))) (let ((.def_36 (or .def_35 .def_34))) (let ((.def_37 (and .def_36 .def_11))) (let ((.def_38 (not .def_35))) (let ((.def_39 (or .def_38 .def_29))) (let ((.def_40 (and .def_39 .def_37))) (let ((.def_41 (not event_is_timed__AT0@4))) (let ((.def_42 (= event_is_timed__AT0@5 .def_41))) (let ((.def_43 (and .def_42 .def_40))) (let ((.def_44 (and .def_43 .def_4))) (let ((.def_45 (not instance.EVENT.1__AT0@3))) (let ((.def_46 (not instance.EVENT.0__AT0@3))) (let ((.def_47 (or .def_46 .def_45))) (let ((.def_48 (= event_is_timed__AT0@3 instance.EVENT.1__AT0@3))) (let ((.def_49 (<= time__AT0@3 time__AT0@4))) (let ((.def_50 (or .def_45 .def_49))) (let ((.def_51 (and .def_50 .def_48))) (let ((.def_52 (= time__AT0@3 time__AT0@4))) (let ((.def_53 (or instance.EVENT.1__AT0@3 .def_52))) (let ((.def_54 (and .def_53 .def_51))) (let ((.def_55 (* (- 1.0) time__AT0@3))) (let ((.def_56 (+ .def_55 time__AT0@4))) (let ((.def_57 (exp .def_56))) (let ((.def_58 (* instance.y__AT0@3 .def_57))) (let ((.def_59 (= instance.y__AT0@4 .def_58))) (let ((.def_60 (+ .def_20 .def_18))) (let ((.def_61 (* 970143.0 instance.x__AT0@3))) (let ((.def_62 (+ .def_61 .def_60))) (let ((.def_63 (* 242536.0 instance.y__AT0@3))) (let ((.def_64 (+ .def_63 .def_62))) (let ((.def_65 (= .def_64 0.0))) (let ((.def_66 (and .def_65 .def_59))) (let ((.def_67 (not .def_52))) (let ((.def_68 (= instance.x__AT0@3 instance.x__AT0@4))) (let ((.def_69 (= instance.y__AT0@3 instance.y__AT0@4))) (let ((.def_70 (and .def_69 .def_68))) (let ((.def_71 (or .def_70 .def_67))) (let ((.def_72 (and .def_71 .def_66))) (let ((.def_73 (and .def_72 .def_49))) (let ((.def_74 (or .def_45 .def_73))) (let ((.def_75 (and .def_74 .def_53))) (let ((.def_76 (and .def_46 .def_45))) (let ((.def_77 (or .def_76 .def_75))) (let ((.def_78 (and .def_77 .def_54))) (let ((.def_79 (not .def_76))) (let ((.def_80 (or .def_79 .def_70))) (let ((.def_81 (and .def_80 .def_78))) (let ((.def_82 (not event_is_timed__AT0@3))) (let ((.def_83 (= event_is_timed__AT0@4 .def_82))) (let ((.def_84 (and .def_83 .def_81))) (let ((.def_85 (and .def_84 .def_47))) (let ((.def_86 (not instance.EVENT.1__AT0@2))) (let ((.def_87 (not instance.EVENT.0__AT0@2))) (let ((.def_88 (or .def_87 .def_86))) (let ((.def_89 (= event_is_timed__AT0@2 instance.EVENT.1__AT0@2))) (let ((.def_90 (<= time__AT0@2 time__AT0@3))) (let ((.def_91 (or .def_86 .def_90))) (let ((.def_92 (and .def_91 .def_89))) (let ((.def_93 (= time__AT0@2 time__AT0@3))) (let ((.def_94 (or instance.EVENT.1__AT0@2 .def_93))) (let ((.def_95 (and .def_94 .def_92))) (let ((.def_96 (* (- 1.0) time__AT0@2))) (let ((.def_97 (+ .def_96 time__AT0@3))) (let ((.def_98 (exp .def_97))) (let ((.def_99 (* instance.y__AT0@2 .def_98))) (let ((.def_100 (= instance.y__AT0@3 .def_99))) (let ((.def_101 (* (- 970143.0) instance.x__AT0@3))) (let ((.def_102 (* (- 242536.0) instance.y__AT0@3))) (let ((.def_103 (+ .def_102 .def_101))) (let ((.def_104 (* 970143.0 instance.x__AT0@2))) (let ((.def_105 (+ .def_104 .def_103))) (let ((.def_106 (* 242536.0 instance.y__AT0@2))) (let ((.def_107 (+ .def_106 .def_105))) (let ((.def_108 (= .def_107 0.0))) (let ((.def_109 (and .def_108 .def_100))) (let ((.def_110 (not .def_93))) (let ((.def_111 (= instance.x__AT0@2 instance.x__AT0@3))) (let ((.def_112 (= instance.y__AT0@2 instance.y__AT0@3))) (let ((.def_113 (and .def_112 .def_111))) (let ((.def_114 (or .def_113 .def_110))) (let ((.def_115 (and .def_114 .def_109))) (let ((.def_116 (and .def_115 .def_90))) (let ((.def_117 (or .def_86 .def_116))) (let ((.def_118 (and .def_117 .def_94))) (let ((.def_119 (and .def_87 .def_86))) (let ((.def_120 (or .def_119 .def_118))) (let ((.def_121 (and .def_120 .def_95))) (let ((.def_122 (not .def_119))) (let ((.def_123 (or .def_122 .def_113))) (let ((.def_124 (and .def_123 .def_121))) (let ((.def_125 (not event_is_timed__AT0@2))) (let ((.def_126 (= event_is_timed__AT0@3 .def_125))) (let ((.def_127 (and .def_126 .def_124))) (let ((.def_128 (and .def_127 .def_88))) (let ((.def_129 (not instance.EVENT.1__AT0@1))) (let ((.def_130 (not instance.EVENT.0__AT0@1))) (let ((.def_131 (or .def_130 .def_129))) (let ((.def_132 (= event_is_timed__AT0@1 instance.EVENT.1__AT0@1))) (let ((.def_133 (<= time__AT0@1 time__AT0@2))) (let ((.def_134 (or .def_129 .def_133))) (let ((.def_135 (and .def_134 .def_132))) (let ((.def_136 (= time__AT0@1 time__AT0@2))) (let ((.def_137 (or instance.EVENT.1__AT0@1 .def_136))) (let ((.def_138 (and .def_137 .def_135))) (let ((.def_139 (* (- 1.0) time__AT0@1))) (let ((.def_140 (+ .def_139 time__AT0@2))) (let ((.def_141 (exp .def_140))) (let ((.def_142 (* instance.y__AT0@1 .def_141))) (let ((.def_143 (= instance.y__AT0@2 .def_142))) (let ((.def_144 (* (- 970143.0) instance.x__AT0@2))) (let ((.def_145 (* (- 242536.0) instance.y__AT0@2))) (let ((.def_146 (+ .def_145 .def_144))) (let ((.def_147 (* 970143.0 instance.x__AT0@1))) (let ((.def_148 (+ .def_147 .def_146))) (let ((.def_149 (* 242536.0 instance.y__AT0@1))) (let ((.def_150 (+ .def_149 .def_148))) (let ((.def_151 (= .def_150 0.0))) (let ((.def_152 (and .def_151 .def_143))) (let ((.def_153 (not .def_136))) (let ((.def_154 (= instance.x__AT0@1 instance.x__AT0@2))) (let ((.def_155 (= instance.y__AT0@1 instance.y__AT0@2))) (let ((.def_156 (and .def_155 .def_154))) (let ((.def_157 (or .def_156 .def_153))) (let ((.def_158 (and .def_157 .def_152))) (let ((.def_159 (and .def_158 .def_133))) (let ((.def_160 (or .def_129 .def_159))) (let ((.def_161 (and .def_160 .def_137))) (let ((.def_162 (and .def_130 .def_129))) (let ((.def_163 (or .def_162 .def_161))) (let ((.def_164 (and .def_163 .def_138))) (let ((.def_165 (not .def_162))) (let ((.def_166 (or .def_165 .def_156))) (let ((.def_167 (and .def_166 .def_164))) (let ((.def_168 (not event_is_timed__AT0@1))) (let ((.def_169 (= event_is_timed__AT0@2 .def_168))) (let ((.def_170 (and .def_169 .def_167))) (let ((.def_171 (and .def_170 .def_131))) (let ((.def_172 (not instance.EVENT.1__AT0@0))) (let ((.def_173 (not instance.EVENT.0__AT0@0))) (let ((.def_174 (or .def_173 .def_172))) (let ((.def_175 (= event_is_timed__AT0@0 instance.EVENT.1__AT0@0))) (let ((.def_176 (<= time__AT0@0 time__AT0@1))) (let ((.def_177 (or .def_172 .def_176))) (let ((.def_178 (and .def_177 .def_175))) (let ((.def_179 (= time__AT0@0 time__AT0@1))) (let ((.def_180 (or instance.EVENT.1__AT0@0 .def_179))) (let ((.def_181 (and .def_180 .def_178))) (let ((.def_182 (* (- 1.0) time__AT0@0))) (let ((.def_183 (+ .def_182 time__AT0@1))) (let ((.def_184 (exp .def_183))) (let ((.def_185 (* instance.y__AT0@0 .def_184))) (let ((.def_186 (= instance.y__AT0@1 .def_185))) (let ((.def_187 (* (- 970143.0) instance.x__AT0@1))) (let ((.def_188 (* (- 242536.0) instance.y__AT0@1))) (let ((.def_189 (+ .def_188 .def_187))) (let ((.def_190 (* 970143.0 instance.x__AT0@0))) (let ((.def_191 (+ .def_190 .def_189))) (let ((.def_192 (* 242536.0 instance.y__AT0@0))) (let ((.def_193 (+ .def_192 .def_191))) (let ((.def_194 (= .def_193 0.0))) (let ((.def_195 (and .def_194 .def_186))) (let ((.def_196 (not .def_179))) (let ((.def_197 (= instance.x__AT0@0 instance.x__AT0@1))) (let ((.def_198 (= instance.y__AT0@0 instance.y__AT0@1))) (let ((.def_199 (and .def_198 .def_197))) (let ((.def_200 (or .def_199 .def_196))) (let ((.def_201 (and .def_200 .def_195))) (let ((.def_202 (and .def_201 .def_176))) (let ((.def_203 (or .def_172 .def_202))) (let ((.def_204 (and .def_203 .def_180))) (let ((.def_205 (and .def_173 .def_172))) (let ((.def_206 (or .def_205 .def_204))) (let ((.def_207 (and .def_206 .def_181))) (let ((.def_208 (not .def_205))) (let ((.def_209 (or .def_208 .def_199))) (let ((.def_210 (and .def_209 .def_207))) (let ((.def_211 (not event_is_timed__AT0@0))) (let ((.def_212 (= event_is_timed__AT0@1 .def_211))) (let ((.def_213 (and .def_212 .def_210))) (let ((.def_214 (and .def_213 .def_174))) (let ((.def_215 (<= instance.x__AT0@0 (- (/ 1 2))))) (let ((.def_216 (not .def_215))) (let ((.def_217 (<= 0.0 instance.x__AT0@0))) (let ((.def_218 (not .def_217))) (let ((.def_219 (and .def_218 .def_216))) (let ((.def_220 (<= 0.0 instance.y__AT0@0))) (let ((.def_221 (not .def_220))) (let ((.def_222 (<= (- (/ 1 2)) instance.y__AT0@0))) (let ((.def_223 (and .def_222 .def_221))) (let ((.def_224 (and .def_223 .def_219))) (let ((.def_225 (= time__AT0@0 0.0))) (let ((.def_226 (and .def_225 .def_224))) (let ((.def_227 (and .def_226 .def_214 .def_171 .def_128 .def_85 .def_44 .def_1))) .def_227))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/nl/nta/exp_monotone.smt2 b/test/regress/regress0/nl/nta/exp_monotone.smt2 new file mode 100644 index 000000000..a1360dc22 --- /dev/null +++ b/test/regress/regress0/nl/nta/exp_monotone.smt2 @@ -0,0 +1,17 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun z () Real) +(declare-fun w () Real) + +(assert (< x w)) + +(assert (> (exp x) (exp y))) +(assert (> (exp y) (exp z))) +(assert (> (exp z) (exp w))) + + +(check-sat) diff --git a/test/regress/regress0/nl/nta/shifting.smt2 b/test/regress/regress0/nl/nta/shifting.smt2 new file mode 100644 index 000000000..320c92d58 --- /dev/null +++ b/test/regress/regress0/nl/nta/shifting.smt2 @@ -0,0 +1,20 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: sat +(set-logic QF_NIRA) +(set-info :status sat) +(declare-fun pi () Real) + +(assert (and (< 3.0 pi) (< pi 3.5))) + +(declare-fun y () Real) +(assert (and (<= (- pi) y) (<= y pi))) + +(declare-fun s () Int) + +(declare-fun z () Real) + +(assert (= z (* 2 pi s))) + +(assert (> z 60)) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/shifting2.smt2 b/test/regress/regress0/nl/nta/shifting2.smt2 new file mode 100644 index 000000000..c5e805c50 --- /dev/null +++ b/test/regress/regress0/nl/nta/shifting2.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NIRA) +(set-info :status unsat) +(declare-fun pi () Real) + +(assert (and (< 3.0 pi) (< pi 3.5))) + +(declare-fun y () Real) +(assert (and (< (- pi) y) (< y pi))) + +(declare-fun s () Int) + +(declare-fun z () Real) + +(assert (= z (+ y (* 2 pi s)))) + +(assert (and (< (- pi) z) (< z pi))) + +(assert (not (= z y))) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2 b/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2 new file mode 100644 index 000000000..f5d7fe32d --- /dev/null +++ b/test/regress/regress0/nl/nta/sin-compare-across-phase.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (< (sin 3.1) (sin 3.3))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin-compare.smt2 b/test/regress/regress0/nl/nta/sin-compare.smt2 new file mode 100644 index 000000000..790d7037f --- /dev/null +++ b/test/regress/regress0/nl/nta/sin-compare.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (or (> (sin 0.1) (sin 0.2)) (> (sin 6.4) (sin 6.5)))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin-init-tangents.smt2 b/test/regress/regress0/nl/nta/sin-init-tangents.smt2 new file mode 100644 index 000000000..e71ab231f --- /dev/null +++ b/test/regress/regress0/nl/nta/sin-init-tangents.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(assert (or (> (sin 0.8) 0.9) (< (sin (- 0.7)) (- 0.75)) (= (sin 3.0) 0.8))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin-sign.smt2 b/test/regress/regress0/nl/nta/sin-sign.smt2 new file mode 100644 index 000000000..9b05a3d52 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin-sign.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (or (< (sin 0.2) (- 0.1)) (> (sin (- 0.05)) 0.05))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin-sym.smt2 b/test/regress/regress0/nl/nta/sin-sym.smt2 new file mode 100644 index 000000000..366906464 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin-sym.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (not (= (+ (sin 0.2) (sin (- 0.2))) 0.0))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/sin-sym2.smt2 b/test/regress/regress0/nl/nta/sin-sym2.smt2 new file mode 100644 index 000000000..2e5d4eac2 --- /dev/null +++ b/test/regress/regress0/nl/nta/sin-sym2.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --nl-ext --nl-ext-tplanes +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) +(declare-fun y () Real) +(assert (and (< 0.0 x) (< x 1.0) (< 0.0 y) (< y 1.0))) +(assert (= (+ (sin x) (sin y)) 0.0)) +(assert (not (= (+ x y) 0.0))) +(check-sat) diff --git a/test/regress/regress0/nl/nta/tan-rewrite.smt2 b/test/regress/regress0/nl/nta/tan-rewrite.smt2 new file mode 100644 index 000000000..0def70806 --- /dev/null +++ b/test/regress/regress0/nl/nta/tan-rewrite.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) + +(assert (= (sin x) 0.24)) +(assert (= (cos x) 0.4)) +(assert (= (tan x) 0.5)) + +(check-sat) diff --git a/test/regress/regress0/nl/nta/tan-rewrite2.smt2 b/test/regress/regress0/nl/nta/tan-rewrite2.smt2 new file mode 100644 index 000000000..af39f7559 --- /dev/null +++ b/test/regress/regress0/nl/nta/tan-rewrite2.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_UFNRA) +(set-info :status unsat) +(declare-fun x () Real) + + +(assert (= (tan x) (sin x))) +(assert (> (cos x) 0)) +(assert (not (= (cos x) 1))) +(assert (not (= (sin x) 0))) + +(check-sat) diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index aebf0de3b..9bf23f555 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf strings sets sygus sep quantifiers +SUBDIRS = . bv aufbv auflia datatypes rewriterules lemmas decision fmf nl strings sets sygus sep quantifiers # don't override a BINARY imported from a personal.mk @mk_if@eq ($(BINARY),) diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am new file mode 100644 index 000000000..a7e4c1411 --- /dev/null +++ b/test/regress/regress1/nl/Makefile.am @@ -0,0 +1,31 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + siegel-nl-bases.smt2 \ + mirko-050417.smt2 + +EXTRA_DIST = $(TESTS) + +# synonyms for "check" in this directory +.PHONY: regress regress1 test +regress regress1 test: check + +# do nothing in this subdir +.PHONY: regress0 regress2 regress3 regress4 +regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/nl/mirko-050417.smt2 b/test/regress/regress1/nl/mirko-050417.smt2 new file mode 100644 index 000000000..21fd61f9f --- /dev/null +++ b/test/regress/regress1/nl/mirko-050417.smt2 @@ -0,0 +1,74 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun t@0 () Real) +(declare-fun y2@0 () Real) +(declare-fun y1@0 () Real) +(declare-fun t@5 () Real) +(declare-fun y1@5 () Real) +(declare-fun y2@5 () Real) +(declare-fun t@6 () Real) +(declare-fun y1@6 () Real) +(declare-fun y2@6 () Real) +(declare-fun t@1 () Real) +(declare-fun y1@1 () Real) +(declare-fun y2@1 () Real) +(declare-fun t@7 () Real) +(declare-fun y1@7 () Real) +(declare-fun y2@7 () Real) +(declare-fun y1@10 () Real) +(declare-fun y2@10 () Real) +(declare-fun t@2 () Real) +(declare-fun y1@2 () Real) +(declare-fun y2@2 () Real) +(declare-fun t@8 () Real) +(declare-fun y1@8 () Real) +(declare-fun y2@8 () Real) +(declare-fun t@3 () Real) +(declare-fun y1@3 () Real) +(declare-fun y2@3 () Real) +(declare-fun t@9 () Real) +(declare-fun y1@9 () Real) +(declare-fun y2@9 () Real) +(declare-fun t@4 () Real) +(declare-fun y1@4 () Real) +(declare-fun y2@4 () Real) +(declare-fun t@10 () Real) +(assert (let ((.def_0 (<= (- 3.0) y2@10))) (let ((.def_1 (<= y2@10 3.0))) (let ((.def_2 (<= y1@10 3.0))) (let ((.def_3 (<= (- 3.0) y1@10))) (let ((.def_4 (and .def_3 .def_2))) (let ((.def_5 (and .def_4 .def_1))) (let ((.def_6 (and +.def_5 .def_0))) (let ((.def_7 (not .def_6))) (let ((.def_8 (cos t@10))) (let ((.def_9 (* (- 2.0) .def_8))) (let ((.def_10 (sin t@10))) (let ((.def_11 (* (- 2.0) .def_10))) (let ((.def_12 (+ .def_11 .def_9))) (let ((.def_13 (+ +y2@10 .def_12))) (let ((.def_14 (= .def_13 0.0))) (let ((.def_15 (* 2.0 .def_10))) (let ((.def_16 (+ .def_15 .def_9))) (let ((.def_17 (+ y1@10 .def_16))) (let ((.def_18 (= .def_17 0.0))) (let ((.def_19 (<= t@10 7.0))) (let +((.def_20 (* (- 1.0) t@10))) (let ((.def_21 (+ t@9 .def_20))) (let ((.def_22 (= .def_21 (- (/ 1 2))))) (let ((.def_23 (and .def_22 .def_19))) (let ((.def_24 (and .def_23 .def_18))) (let ((.def_25 (and .def_24 .def_14))) (let +((.def_26 (* (- 1.0) y2@9))) (let ((.def_27 (cos t@9))) (let ((.def_28 (* 2.0 .def_27))) (let ((.def_29 (+ .def_28 .def_26))) (let ((.def_30 (sin t@9))) (let ((.def_31 (* 2.0 .def_30))) (let ((.def_32 (+ .def_31 .def_29))) (let +((.def_33 (= .def_32 0.0))) (let ((.def_34 (* (- 2.0) .def_27))) (let ((.def_35 (+ .def_34 y1@9))) (let ((.def_36 (+ .def_31 .def_35))) (let ((.def_37 (= .def_36 0.0))) (let ((.def_38 (<= t@9 7.0))) (let ((.def_39 (* (- 1.0) t@9))) +(let ((.def_40 (+ t@8 .def_39))) (let ((.def_41 (= .def_40 (- (/ 1 2))))) (let ((.def_42 (and .def_41 .def_38))) (let ((.def_43 (and .def_42 .def_37))) (let ((.def_44 (and .def_43 .def_33))) (let ((.def_45 (* (- 1.0) y2@8))) (let +((.def_46 (cos t@8))) (let ((.def_47 (* 2.0 .def_46))) (let ((.def_48 (+ .def_47 .def_45))) (let ((.def_49 (sin t@8))) (let ((.def_50 (* 2.0 .def_49))) (let ((.def_51 (+ .def_50 .def_48))) (let ((.def_52 (= .def_51 0.0))) (let +((.def_53 (* (- 2.0) .def_46))) (let ((.def_54 (+ .def_53 y1@8))) (let ((.def_55 (+ .def_50 .def_54))) (let ((.def_56 (= .def_55 0.0))) (let ((.def_57 (<= t@8 7.0))) (let ((.def_58 (* (- 1.0) t@8))) (let ((.def_59 (+ t@7 .def_58))) +(let ((.def_60 (= .def_59 (- (/ 1 2))))) (let ((.def_61 (and .def_60 .def_57))) (let ((.def_62 (and .def_61 .def_56))) (let ((.def_63 (and .def_62 .def_52))) (let ((.def_64 (* (- 1.0) y2@7))) (let ((.def_65 (cos t@7))) (let +((.def_66 (* 2.0 .def_65))) (let ((.def_67 (+ .def_66 .def_64))) (let ((.def_68 (sin t@7))) (let ((.def_69 (* 2.0 .def_68))) (let ((.def_70 (+ .def_69 .def_67))) (let ((.def_71 (= .def_70 0.0))) (let ((.def_72 (* (- 2.0) .def_65))) +(let ((.def_73 (+ .def_72 y1@7))) (let ((.def_74 (+ .def_69 .def_73))) (let ((.def_75 (= .def_74 0.0))) (let ((.def_76 (<= t@7 7.0))) (let ((.def_77 (* (- 1.0) t@7))) (let ((.def_78 (+ t@6 .def_77))) (let ((.def_79 (= .def_78 (- (/ +1 2))))) (let ((.def_80 (and .def_79 .def_76))) (let ((.def_81 (and .def_80 .def_75))) (let ((.def_82 (and .def_81 .def_71))) (let ((.def_83 (* (- 1.0) y2@6))) (let ((.def_84 (cos t@6))) (let ((.def_85 (* 2.0 .def_84))) (let +((.def_86 (+ .def_85 .def_83))) (let ((.def_87 (sin t@6))) (let ((.def_88 (* 2.0 .def_87))) (let ((.def_89 (+ .def_88 .def_86))) (let ((.def_90 (= .def_89 0.0))) (let ((.def_91 (* (- 2.0) .def_84))) (let ((.def_92 (+ .def_91 +y1@6))) (let ((.def_93 (+ .def_88 .def_92))) (let ((.def_94 (= .def_93 0.0))) (let ((.def_95 (<= t@6 7.0))) (let ((.def_96 (* (- 1.0) t@6))) (let ((.def_97 (+ t@5 .def_96))) (let ((.def_98 (= .def_97 (- (/ 1 2))))) (let ((.def_99 +(and .def_98 .def_95))) (let ((.def_100 (and .def_99 .def_94))) (let ((.def_101 (and .def_100 .def_90))) (let ((.def_102 (* (- 1.0) y2@5))) (let ((.def_103 (cos t@5))) (let ((.def_104 (* 2.0 .def_103))) (let ((.def_105 (+ .def_104 +.def_102))) (let ((.def_106 (sin t@5))) (let ((.def_107 (* 2.0 .def_106))) (let ((.def_108 (+ .def_107 .def_105))) (let ((.def_109 (= .def_108 0.0))) (let ((.def_110 (* (- 2.0) .def_103))) (let ((.def_111 (+ .def_110 y1@5))) (let +((.def_112 (+ .def_107 .def_111))) (let ((.def_113 (= .def_112 0.0))) (let ((.def_114 (<= t@5 7.0))) (let ((.def_115 (* (- 1.0) t@5))) (let ((.def_116 (+ t@4 .def_115))) (let ((.def_117 (= .def_116 (- (/ 1 2))))) (let ((.def_118 +(and .def_117 .def_114))) (let ((.def_119 (and .def_118 .def_113))) (let ((.def_120 (and .def_119 .def_109))) (let ((.def_121 (* (- 1.0) y2@4))) (let ((.def_122 (cos t@4))) (let ((.def_123 (* 2.0 .def_122))) (let ((.def_124 (+ +.def_123 .def_121))) (let ((.def_125 (sin t@4))) (let ((.def_126 (* 2.0 .def_125))) (let ((.def_127 (+ .def_126 .def_124))) (let ((.def_128 (= .def_127 0.0))) (let ((.def_129 (* (- 2.0) .def_122))) (let ((.def_130 (+ .def_129 +y1@4))) (let ((.def_131 (+ .def_126 .def_130))) (let ((.def_132 (= .def_131 0.0))) (let ((.def_133 (<= t@4 7.0))) (let ((.def_134 (* (- 1.0) t@4))) (let ((.def_135 (+ t@3 .def_134))) (let ((.def_136 (= .def_135 (- (/ 1 2))))) (let +((.def_137 (and .def_136 .def_133))) (let ((.def_138 (and .def_137 .def_132))) (let ((.def_139 (and .def_138 .def_128))) (let ((.def_140 (* (- 1.0) y2@3))) (let ((.def_141 (cos t@3))) (let ((.def_142 (* 2.0 .def_141))) (let +((.def_143 (+ .def_142 .def_140))) (let ((.def_144 (sin t@3))) (let ((.def_145 (* 2.0 .def_144))) (let ((.def_146 (+ .def_145 .def_143))) (let ((.def_147 (= .def_146 0.0))) (let ((.def_148 (* (- 2.0) .def_141))) (let ((.def_149 (+ +.def_148 y1@3))) (let ((.def_150 (+ .def_145 .def_149))) (let ((.def_151 (= .def_150 0.0))) (let ((.def_152 (<= t@3 7.0))) (let ((.def_153 (* (- 1.0) t@3))) (let ((.def_154 (+ t@2 .def_153))) (let ((.def_155 (= .def_154 (- (/ 1 +2))))) (let ((.def_156 (and .def_155 .def_152))) (let ((.def_157 (and .def_156 .def_151))) (let ((.def_158 (and .def_157 .def_147))) (let ((.def_159 (* (- 1.0) y2@2))) (let ((.def_160 (cos t@2))) (let ((.def_161 (* 2.0 .def_160))) +(let ((.def_162 (+ .def_161 .def_159))) (let ((.def_163 (sin t@2))) (let ((.def_164 (* 2.0 .def_163))) (let ((.def_165 (+ .def_164 .def_162))) (let ((.def_166 (= .def_165 0.0))) (let ((.def_167 (* (- 2.0) .def_160))) (let +((.def_168 (+ .def_167 y1@2))) (let ((.def_169 (+ .def_164 .def_168))) (let ((.def_170 (= .def_169 0.0))) (let ((.def_171 (<= t@2 7.0))) (let ((.def_172 (* (- 1.0) t@2))) (let ((.def_173 (+ t@1 .def_172))) (let ((.def_174 (= +.def_173 (- (/ 1 2))))) (let ((.def_175 (and .def_174 .def_171))) (let ((.def_176 (and .def_175 .def_170))) (let ((.def_177 (and .def_176 .def_166))) (let ((.def_178 (* (- 1.0) y2@1))) (let ((.def_179 (cos t@1))) (let ((.def_180 (* +2.0 .def_179))) (let ((.def_181 (+ .def_180 .def_178))) (let ((.def_182 (sin t@1))) (let ((.def_183 (* 2.0 .def_182))) (let ((.def_184 (+ .def_183 .def_181))) (let ((.def_185 (= .def_184 0.0))) (let ((.def_186 (* (- 2.0) +.def_179))) (let ((.def_187 (+ .def_186 y1@1))) (let ((.def_188 (+ .def_183 .def_187))) (let ((.def_189 (= .def_188 0.0))) (let ((.def_190 (<= t@1 7.0))) (let ((.def_191 (* (- 1.0) t@1))) (let ((.def_192 (+ t@0 .def_191))) (let +((.def_193 (= .def_192 (- (/ 1 2))))) (let ((.def_194 (and .def_193 .def_190))) (let ((.def_195 (and .def_194 .def_189))) (let ((.def_196 (and .def_195 .def_185))) (let ((.def_197 (= t@0 0.0))) (let ((.def_198 (cos t@0))) (let +((.def_199 (* (- 2.0) .def_198))) (let ((.def_200 (+ .def_199 y1@0))) (let ((.def_201 (sin t@0))) (let ((.def_202 (* 2.0 .def_201))) (let ((.def_203 (+ .def_202 .def_200))) (let ((.def_204 (= .def_203 0.0))) (let ((.def_205 (* (- +1.0) y2@0))) (let ((.def_206 (* 2.0 .def_198))) (let ((.def_207 (+ .def_206 .def_205))) (let ((.def_208 (+ .def_202 .def_207))) (let ((.def_209 (= .def_208 0.0))) (let ((.def_210 (and .def_209 .def_204))) (let ((.def_211 (and +.def_210 .def_197))) (let ((.def_212 (and .def_211 .def_196 .def_177 .def_158 .def_139 .def_120 .def_101 .def_82 .def_63 .def_44 .def_25 .def_7))) +.def_212)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/nl/siegel-nl-bases.smt2 b/test/regress/regress1/nl/siegel-nl-bases.smt2 new file mode 100644 index 000000000..cf6e3ab5e --- /dev/null +++ b/test/regress/regress1/nl/siegel-nl-bases.smt2 @@ -0,0 +1,22 @@ +; COMMAND-LINE: --nl-ext +; EXPECT: unsat +(set-logic QF_NIA) +(declare-const n Int) +(declare-const i1 Int) +(declare-const i2 Int) +(declare-const j1 Int) +(declare-const j2 Int) +(assert (>= n 0)) +(assert (not (= i1 i2))) +(assert (<= 0 i1)) +(assert (<= i1 j1)) +(assert (< j1 n)) +(assert (<= 0 i2)) +(assert (<= i2 j2)) +(assert (< j2 n)) +(assert (or + (= (+ (* i1 n) j1) (+ (* i2 n) j2)) + (= (+ (* i1 n) j1) (+ (* j2 n) i2)) + (= (+ (* j1 n) i1) (+ (* i2 n) j2)) + (= (+ (* j1 n) i1) (+ (* j2 n) i2)))) +(check-sat)