From 490f664c35d717d5bd01f43f3026fb2abf3e99ff Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Jul 2018 18:25:13 +0200 Subject: [PATCH] Purify applications of exp to transcendental arguments (#2097) --- src/theory/arith/nonlinear_extension.cpp | 101 ++++++++++++++--------- src/theory/arith/nonlinear_extension.h | 4 +- 2 files changed, 62 insertions(+), 43 deletions(-) diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 8380014f3..30debf6d7 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -856,7 +856,7 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, Trace("nl-ext-cm-debug") << " apply pre-substitution..." << std::endl; std::vector pvars; std::vector psubs; - for (std::pair& tb : d_trig_base) + for (std::pair& tb : d_tr_base) { pvars.push_back(tb.first); psubs.push_back(tb.second); @@ -1850,16 +1850,18 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, Trace("nl-ext-mv") << "Extended terms : " << std::endl; // register the extended function terms std::map< Node, Node > mvarg_to_term; - std::vector trig_no_base; + std::vector tr_no_base; bool needPi = false; - for( unsigned i=0; i& assertions, } */ }else if( a.getNumChildren()==1 ){ + if (ak == SINE) + { + needPi = true; + } bool consider = true; - // get shifted version - if (a.getKind() == SINE) + // if is an unpurified application of SINE, or it is a transcendental + // applied to a trancendental, purify. + if (isTranscendentalKind(ak)) { - if( d_trig_is_base.find( a )==d_trig_is_base.end() ){ + if ((ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end()) + || isTranscendentalKind(a[0].getKind())) + { consider = false; - trig_no_base.push_back(a); - needPi = true; + tr_no_base.push_back(a); } } 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() ){ + std::map::iterator itrm = d_tf_rep_map[ak].find(r); + if (itrm != d_tf_rep_map[ak].end()) + { //verify they have the same model value if( d_mv[1][a]!=d_mv[1][itrm->second] ){ // if not, add congruence lemma @@ -1915,14 +1924,14 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, //Assert( false ); } }else{ - d_tf_rep_map[a.getKind()][r] = a; + d_tf_rep_map[ak][r] = a; } } } - else if (a.getKind() == PI) + else if (ak == PI) { needPi = true; - d_tf_rep_map[a.getKind()][a] = a; + d_tf_rep_map[ak][a] = a; } else { @@ -1943,37 +1952,46 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } // process SINE phase shifting - for (const Node& a : trig_no_base) + for (const Node& a : tr_no_base) { - if (d_trig_base.find(a) == d_trig_base.end()) + if (d_tr_base.find(a) == d_tr_base.end()) { Node y = nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg"); Node new_a = nm->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; - Assert(!d_pi.isNull()); - Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts"); - // FIXME : do not introduce shift here, instead needs model-based - // refinement for constant shifts (#1284) - Node shift_lem = nm->mkNode( - AND, - mkValidPhase(y, d_pi), - nm->mkNode( - ITE, - mkValidPhase(a[0], d_pi), - a[0].eqNode(y), - a[0].eqNode(nm->mkNode( - PLUS, - y, - nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))), - new_a.eqNode(a)); + d_tr_is_base[new_a] = true; + d_tr_base[a] = new_a; + Node lem; + if (a.getKind() == SINE) + { + Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a + << std::endl; + Assert(!d_pi.isNull()); + Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts"); + // FIXME : do not introduce shift here, instead needs model-based + // refinement for constant shifts (#1284) + lem = nm->mkNode( + AND, + mkValidPhase(y, d_pi), + nm->mkNode( + ITE, + mkValidPhase(a[0], d_pi), + a[0].eqNode(y), + a[0].eqNode(nm->mkNode( + PLUS, + y, + nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))), + new_a.eqNode(a)); + } + else + { + // do both equalities to ensure that new_a becomes a preregistered term + lem = nm->mkNode(AND, a.eqNode(new_a), a[0].eqNode(y)); + } // 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); + << "NonlinearExtension::Lemma : purify : " << lem << std::endl; + d_containing.getOutputChannel().lemma(lem, false, true); lemmas_proc++; } } @@ -3764,8 +3782,8 @@ std::vector NonlinearExtension::checkTranscendentalInitialRefine() { SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0])); symn = Rewriter::rewrite( symn ); //can assume its basis since phase is split over 0 - d_trig_is_base[symn] = true; - Assert( d_trig_is_base.find( t ) != d_trig_is_base.end() ); + d_tr_is_base[symn] = true; + Assert(d_tr_is_base.find(t) != d_tr_is_base.end()); std::vector< Node > children; lem = NodeManager::currentNM()->mkNode( @@ -4169,9 +4187,10 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, Node v_pab = r == 0 ? mvb.first : mvb.second; if (!v_pab.isNull()) { - Assert(v_pab.isConst()); Trace("nl-ext-tftp-debug2") << "...model value of " << pab << " is " << v_pab << std::endl; + + Assert(v_pab.isConst()); Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab); Trace("nl-ext-tftp-debug2") << "...compare : " << comp << std::endl; Node compr = Rewriter::rewrite(comp); diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index d3698aa94..1e5ca9ad1 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -544,8 +544,8 @@ class NonlinearExtension { std::vector d_order_points; //transcendental functions - std::map d_trig_base; - std::map d_trig_is_base; + std::map d_tr_base; + std::map d_tr_is_base; std::map< Node, bool > d_tf_initial_refine; /** the list of lemmas we are waiting to flush until after check model */ std::vector d_waiting_lemmas; -- 2.30.2