From 05a2414a2742ee0c7e5af40ac9c725cb49d1f196 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Feb 2018 12:53:12 -0600 Subject: [PATCH] Minor fixes and additions for transcendental functions (#1612) Also adds parsing support for PI in smt2 with syntax "real.pi". --- src/parser/smt2/Smt2.g | 6 ++ src/theory/arith/arith_rewriter.cpp | 6 +- src/theory/arith/nonlinear_extension.cpp | 98 ++++++++++++++----- src/theory/arith/nonlinear_extension.h | 13 ++- src/theory/arith/theory_arith_private.cpp | 2 +- test/regress/regress0/nl/Makefile.am | 4 +- test/regress/regress0/nl/nta/real-pi.smt2 | 7 ++ test/regress/regress0/nl/nta/sqrt-simple.smt2 | 6 ++ test/regress/regress1/nl/Makefile.am | 3 +- test/regress/regress1/nl/sin1-deq-sat.smt2 | 14 +++ test/regress/regress1/nl/sin1-sat.smt2 | 2 +- 11 files changed, 128 insertions(+), 33 deletions(-) create mode 100644 test/regress/regress0/nl/nta/real-pi.smt2 create mode 100644 test/regress/regress0/nl/nta/sqrt-simple.smt2 create mode 100644 test/regress/regress1/nl/sin1-deq-sat.smt2 diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index d424fefad..b9a2a8805 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -2348,6 +2348,10 @@ termNonVariable[CVC4::Expr& expr, CVC4::Expr& expr2] | FP_RTN_FULL_TOK { expr = MK_CONST(roundTowardNegative); } | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); } + | REAL_PI_TOK { + expr = EXPR_MANAGER->mkNullaryOperator(EXPR_MANAGER->realType(), kind::PI); + } + | RENOSTR_TOK { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); @@ -3191,6 +3195,8 @@ TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) }? 'tupSe // tokenized and handled directly when // processing a term +REAL_PI_TOK : 'real.pi'; + FP_PINF_TOK : '+oo'; FP_NINF_TOK : '-oo'; FP_PZERO_TOK : '+zero'; diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index a9761ade4..355aa7b0f 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -115,7 +115,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::ARCTANGENT: case kind::ARCCOSECANT: case kind::ARCSECANT: - case kind::ARCCOTANGENT: return preRewriteTranscendental(t); + case kind::ARCCOTANGENT: + case kind::SQRT: return preRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); @@ -179,7 +180,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ case kind::ARCTANGENT: case kind::ARCCOSECANT: case kind::ARCSECANT: - case kind::ARCCOTANGENT: return postRewriteTranscendental(t); + case kind::ARCCOTANGENT: + case kind::SQRT: return postRewriteTranscendental(t); case kind::INTS_DIVISION: case kind::INTS_MODULUS: return RewriteResponse(REWRITE_DONE, t); diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index e8f8b9fa5..5694ce451 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -1137,9 +1137,12 @@ std::vector NonlinearExtension::checkModel( bool NonlinearExtension::checkModelTf(const std::vector& assertions) { Trace("nl-ext-tf-check-model") << "check-model : Run" << std::endl; - // add bounds for PI - d_tf_check_model_bounds[d_pi] = - std::pair(d_pi_bound[0], d_pi_bound[1]); + if (!d_pi.isNull()) + { + // add bounds for PI + d_tf_check_model_bounds[d_pi] = + std::pair(d_pi_bound[0], d_pi_bound[1]); + } for (const std::pair >& tfb : d_tf_check_model_bounds) { @@ -1256,6 +1259,27 @@ bool NonlinearExtension::simpleCheckModelTfLit(Node lit) return comp == d_true; } } + else if (atom.getKind() == EQUAL) + { + // x = a is ( x >= a ^ x <= a ) + for (unsigned i = 0; i < 2; i++) + { + Node lit = nm->mkNode(GEQ, atom[i], atom[1 - i]); + if (!pol) + { + lit = lit.negate(); + } + lit = Rewriter::rewrite(lit); + bool success = simpleCheckModelTfLit(lit); + if (success != pol) + { + // false != true -> one conjunct of equality is false, we fail + // true != false -> one disjunct of disequality is true, we succeed + return success; + } + } + } + Trace("nl-ext-tf-check-model-simple") << " failed due to unknown literal." << std::endl; return false; @@ -1300,6 +1324,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // register the extended function terms std::map< Node, Node > mvarg_to_term; std::vector trig_no_base; + bool needPi = false; for( unsigned i=0; i& assertions, << d_mv[0][a] << " ]" << std::endl; //Assert(d_mv[1][a].isConst()); //Assert(d_mv[0][a].isConst()); - if (a.getKind() == NONLINEAR_MULT) { d_ms.push_back( a ); @@ -1349,11 +1373,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, if( d_trig_is_base.find( a )==d_trig_is_base.end() ){ consider = false; trig_no_base.push_back(a); - if (d_pi.isNull()) - { - mkPi(); - getCurrentPiBounds(lemmas); - } + needPi = true; } } if( consider ){ @@ -1375,12 +1395,21 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } else if (a.getKind() == PI) { - //TODO? - }else{ + needPi = true; + d_tf_rep_map[a.getKind()][a] = a; + } + else + { Assert( false ); } } - + // initialize pi if necessary + if (needPi && d_pi.isNull()) + { + mkPi(); + getCurrentPiBounds(lemmas); + } + lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { Trace("nl-ext") << " ...finished with " << lemmas_proc << " new lemmas during registration." << std::endl; @@ -1426,6 +1455,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, << " new lemmas SINE phase shifting." << std::endl; return lemmas_proc; } + Trace("nl-ext") << "We have " << d_ms.size() << " monomials." << std::endl; // register constants registerMonomial(d_one); @@ -1497,11 +1527,12 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, for (unsigned c = 0; c < 3; c++) { // c is effort level lemmas = checkMonomialMagnitude( c ); + unsigned nlem = lemmas.size(); lemmas_proc = flushLemmas(lemmas); if (lemmas_proc > 0) { Trace("nl-ext") << " ...finished with " << lemmas_proc - << " new lemmas (out of possible " << lemmas.size() - << ")." << std::endl; + << " new lemmas (out of possible " << nlem << ")." + << std::endl; return lemmas_proc; } } @@ -1678,9 +1709,8 @@ void NonlinearExtension::check(Theory::Effort e) { // the problem is that we cannot evaluate transcendental functions // (they don't have a rewriter that returns constants) // thus, the actual value in their model can be themselves, hence we - // have no reference - // point to rule out the current model. In this case, we may set - // incomplete below. + // have no reference point to rule out the current model. In this + // case, we may set incomplete below. } } } @@ -2332,7 +2362,7 @@ std::vector NonlinearExtension::checkMonomialMagnitude( unsigned c ) { } // 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() + Trace("nl-ext-comp") << "Compute redundancies for " << lemmas.size() << " lemmas." << std::endl; // naive std::vector r_lemmas; @@ -3101,15 +3131,24 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { 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; + Kind k = it->first; + if (k == EXPONENTIAL || k == SINE) + { + for (std::map::iterator itt = it->second.begin(); + itt != it->second.end(); + ++itt) + { + Node a = itt->second[0]; + computeModelValue(a, 1); + Assert(d_mv[1].find(a) != d_mv[1].end()); + if (d_mv[1][a].isConst()) + { + Trace("nl-ext-tf-mono-debug") << "...tf term : " << a << std::endl; + sorted_tf_args[k].push_back(a); + tf_arg_to_term[k][a] = itt->second; + } } - } + } } SortNonlinearExtension smv; @@ -3256,6 +3295,13 @@ std::vector NonlinearExtension::checkTranscendentalTangentPlanes() for (std::pair >& tfs : d_tf_rep_map) { Kind k = tfs.first; + if (k == PI) + { + // We do not use Taylor approximation for PI currently. + // This is because the convergence is extremely slow, and hence an + // initial approximation is superior. + continue; + } Node tft = nm->mkNode(k, d_zero); Trace("nl-ext-tf-tplanes-debug") << "Taylor variables: " << std::endl; Trace("nl-ext-tf-tplanes-debug") diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 84acc0269..a37ef97f8 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -390,6 +390,10 @@ class NonlinearExtension { typedef std::map MonomialExponentMap; MonomialExponentMap d_m_exp; + /** + * Mapping from monomials to the list of variables that occur in it. For + * example, x*x*y*z -> { x, y, z }. + */ std::map > d_m_vlist; NodeMultiset d_m_degree; // monomial index, by sorted variables @@ -475,7 +479,8 @@ private: std::vector< Node > d_ms; std::vector< Node > d_ms_vars; std::map d_ms_proc; - std::vector d_mterms; + 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; @@ -668,6 +673,12 @@ private: * * |x|>|y| => |x*z|>|y*z| * |x|>|y| ^ |z|>|w| ^ |x|>=1 => |x*x*z*u|>|y*w| + * + * Argument c indicates the class of inferences to perform for the (non-linear) + * monomials in the vector d_ms. + * 0 : compare non-linear monomials against 1, + * 1 : compare non-linear monomials against variables, + * 2 : compare non-linear monomials against other non-linear monomials. */ std::vector checkMonomialMagnitude( unsigned c ); diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index d7706201d..da17dd2f5 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -4995,7 +4995,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) Node lem; if (k == kind::SQRT) { - lem = nm->mkNode(kind::MULT, node[0], node[0]).eqNode(var); + lem = nm->mkNode(kind::MULT, var, var).eqNode(node[0]); } else { diff --git a/test/regress/regress0/nl/Makefile.am b/test/regress/regress0/nl/Makefile.am index c10b65931..0347dbd8b 100644 --- a/test/regress/regress0/nl/Makefile.am +++ b/test/regress/regress0/nl/Makefile.am @@ -35,7 +35,9 @@ TESTS = \ nta/tan-rewrite.smt2 \ nta/exp1-ub.smt2 \ nta/exp-n0.5-ub.smt2 \ - nta/exp-n0.5-lb.smt2 + nta/exp-n0.5-lb.smt2 \ + nta/real-pi.smt2 \ + nta/sqrt-simple.smt2 # unsolved : garbage_collect.cvc diff --git a/test/regress/regress0/nl/nta/real-pi.smt2 b/test/regress/regress0/nl/nta/real-pi.smt2 new file mode 100644 index 000000000..a303f48b1 --- /dev/null +++ b/test/regress/regress0/nl/nta/real-pi.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --nl-ext --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(assert (<= 3.0 real.pi)) +(assert (<= real.pi 4.0)) +(check-sat) diff --git a/test/regress/regress0/nl/nta/sqrt-simple.smt2 b/test/regress/regress0/nl/nta/sqrt-simple.smt2 new file mode 100644 index 000000000..ade068152 --- /dev/null +++ b/test/regress/regress0/nl/nta/sqrt-simple.smt2 @@ -0,0 +1,6 @@ +(set-logic QF_NRA) +(set-info :status unsat) +(declare-fun x () Real) +(assert (> x 0.0)) +(assert (not (= (* (sqrt x) (sqrt x)) x))) +(check-sat) diff --git a/test/regress/regress1/nl/Makefile.am b/test/regress/regress1/nl/Makefile.am index bafaf665a..a95715253 100644 --- a/test/regress/regress1/nl/Makefile.am +++ b/test/regress/regress1/nl/Makefile.am @@ -63,7 +63,8 @@ TESTS = \ sin2-lb.smt2 \ sin2-ub.smt2 \ sugar-ident.smt2 \ - zero-subset.smt2 + zero-subset.smt2 \ + sin1-deq-sat.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/nl/sin1-deq-sat.smt2 b/test/regress/regress1/nl/sin1-deq-sat.smt2 new file mode 100644 index 000000000..4c8302e9f --- /dev/null +++ b/test/regress/regress1/nl/sin1-deq-sat.smt2 @@ -0,0 +1,14 @@ +; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models +; EXPECT: sat +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun x () Real) + +(assert (not (= (sin 1.0) 0.5))) +(assert (not (= (sin 1.0) 0.8))) +(assert (not (= (sin 1.0) 0.9))) +(assert (not (= (sin 1.0) (- 0.84)))) +(assert (< (- x (sin 1)) 0.000001)) +(assert (< (- (sin 1) x) 0.000001)) + +(check-sat) diff --git a/test/regress/regress1/nl/sin1-sat.smt2 b/test/regress/regress1/nl/sin1-sat.smt2 index d6275c6e8..d45fd1453 100644 --- a/test/regress/regress1/nl/sin1-sat.smt2 +++ b/test/regress/regress1/nl/sin1-sat.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --nl-ext-tf-tplanes --no-check-models ; EXPECT: sat (set-logic QF_NRA) -(set-info :status unsat) +(set-info :status sat) (declare-fun x () Real) (assert (> (sin 1) 0.84)) -- 2.30.2