From 466b45c52d83cf19caef2c1eee6e7c5fd2ecb1bc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 13 Sep 2018 12:18:12 -0500 Subject: [PATCH] Simplify storing of transcendental function applications that occur in assertions (#2458) --- src/theory/arith/nonlinear_extension.cpp | 160 +++++++++++++++-------- src/theory/arith/nonlinear_extension.h | 10 +- 2 files changed, 109 insertions(+), 61 deletions(-) diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index f4e9f9d6b..9f6608dc5 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -883,13 +883,12 @@ bool NonlinearExtension::checkModel(const std::vector& assertions, // get model bounds for all transcendental functions Trace("nl-ext-cm-debug") << " get bounds for transcendental functions..." << std::endl; - for (std::pair >& tfs : d_tf_rep_map) + for (std::pair >& tfs : d_f_map) { Kind k = tfs.first; - for (std::pair& tfr : tfs.second) + for (const Node& tf : tfs.second) { - // Figure 3 : tf( x ) - Node tf = tfr.second; + // tf is Figure 3 : tf( x ) Node atf = computeModelValue(tf, 0); if (k == PI) { @@ -1827,6 +1826,33 @@ std::vector NonlinearExtension::checkSplitZero() { return lemmas; } +/** An argument trie, for computing congruent terms */ +class ArgTrie +{ + public: + /** children of this node */ + std::map d_children; + /** the data of this node */ + Node d_data; + /** + * Set d as the data on the node whose path is [args], return either d if + * that node has no data, or the data that already occurs there. + */ + Node add(Node d, const std::vector& args) + { + ArgTrie* at = this; + for (const Node& a : args) + { + at = &(at->d_children[a]); + } + if (at->d_data.isNull()) + { + at->d_data = d; + } + return at->d_data; + } +}; + int NonlinearExtension::checkLastCall(const std::vector& assertions, const std::vector& false_asserts, const std::vector& xts) @@ -1840,7 +1866,7 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, d_ci.clear(); d_ci_exp.clear(); d_ci_max.clear(); - d_tf_rep_map.clear(); + d_f_map.clear(); d_tf_region.clear(); d_waiting_lemmas.clear(); @@ -1853,6 +1879,8 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, std::map< Node, Node > mvarg_to_term; std::vector tr_no_base; bool needPi = false; + // for computing congruence + std::map argTrie; for (unsigned i = 0, xsize = xts.size(); i < xsize; i++) { Node a = xts[i]; @@ -1894,7 +1922,9 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, } } */ - }else if( a.getNumChildren()==1 ){ + } + else if (a.getNumChildren() > 0) + { if (ak == SINE) { needPi = true; @@ -1904,35 +1934,61 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, // applied to a trancendental, purify. if (isTranscendentalKind(ak)) { - if ((ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end()) - || isTranscendentalKind(a[0].getKind())) + if (ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end()) { consider = false; + } + else + { + for (const Node& ac : a) + { + if (isTranscendentalKind(ac.getKind())) + { + consider = false; + break; + } + } + } + if (!consider) + { tr_no_base.push_back(a); } } if( consider ){ - Node r = d_containing.getValuation().getModel()->getRepresentative(a[0]); - std::map::iterator itrm = d_tf_rep_map[ak].find(r); - if (itrm != d_tf_rep_map[ak].end()) + std::vector repList; + for (const Node& ac : a) + { + Node r = + d_containing.getValuation().getModel()->getRepresentative(a[0]); + repList.push_back(r); + } + Node aa = argTrie[ak].add(a, repList); + if (aa != a) { - //verify they have the same model value - if( d_mv[1][a]!=d_mv[1][itrm->second] ){ - // if not, add congruence lemma - Node cong_lemma = nm->mkNode( - IMPLIES, a[0].eqNode(itrm->second[0]), a.eqNode(itrm->second)); + // apply congruence to pairs of terms that are disequal and congruent + Assert(aa.getNumChildren() == a.getNumChildren()); + if (d_mv[1][a] != d_mv[1][aa]) + { + std::vector exp; + for (unsigned j = 0, size = a.getNumChildren(); j < size; j++) + { + exp.push_back(a[j].eqNode(aa[j])); + } + Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp); + Node cong_lemma = nm->mkNode(OR, expn.negate(), a.eqNode(aa)); lemmas.push_back( cong_lemma ); - //Assert( false ); } - }else{ - d_tf_rep_map[ak][r] = a; + } + else + { + d_f_map[ak].push_back(a); } } } else if (ak == PI) { needPi = true; - d_tf_rep_map[ak][a] = a; + d_f_map[ak].push_back(a); } else { @@ -2025,19 +2081,14 @@ int NonlinearExtension::checkLastCall(const std::vector& assertions, { Trace("nl-ext-mv") << "Arguments of trancendental functions : " << std::endl; - for (std::map >::iterator it = - d_tf_rep_map.begin(); - it != d_tf_rep_map.end(); - ++it) + for (std::pair >& tfl : d_f_map) { - Kind k = it->first; + Kind k = tfl.first; if (k == SINE || k == EXPONENTIAL) { - for (std::map::iterator itt = it->second.begin(); - itt != it->second.end(); - ++itt) + for (const Node& tf : tfl.second) { - Node v = itt->second[0]; + Node v = tf[0]; computeModelValue(v, 0); computeModelValue(v, 1); printModelValue("nl-ext-mv", v); @@ -3769,15 +3820,17 @@ std::vector NonlinearExtension::checkMonomialInferResBounds() { 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 ){ - for( std::map< Node, Node >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){ - Node t = itt->second; + for (std::pair >& tfl : d_f_map) + { + Kind k = tfl.first; + for (const Node& t : tfl.second) + { Assert( d_mv[1].find( t )!=d_mv[1].end() ); //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 == SINE) + if (k == SINE) { Node symn = NodeManager::currentNM()->mkNode( SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0])); @@ -3839,7 +3892,7 @@ std::vector NonlinearExtension::checkTranscendentalInitialRefine() { NodeManager::currentNM()->mkNode( MINUS, d_pi_neg, t[0]))))); } - else if (it->first == EXPONENTIAL) + else if (k == EXPONENTIAL) { // ( exp(x) > 0 ) ^ ( x=0 <=> exp( x ) = 1 ) ^ ( x < 0 <=> exp( x ) < // 1 ) ^ ( x <= 0 V exp( x ) > x + 1 ) @@ -3877,23 +3930,22 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { //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 ){ - Kind k = it->first; + + for (std::pair >& tfl : d_f_map) + { + Kind k = tfl.first; if (k == EXPONENTIAL || k == SINE) { - for (std::map::iterator itt = it->second.begin(); - itt != it->second.end(); - ++itt) + for (const Node& tf : tfl.second) { - Node a = itt->second[0]; + Node a = tf[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; + tf_arg_to_term[k][a] = tf; } } } @@ -3904,12 +3956,14 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { //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; + for (std::pair >& tfl : d_f_map) + { + Kind k = tfl.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++ ){ + for (unsigned i = 0; i < sorted_tf_args[k].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; @@ -3919,7 +3973,7 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { } std::vector< Node > mpoints; std::vector< Node > mpoints_vals; - if (it->first == SINE) + if (k == SINE) { mpoints.push_back( d_pi ); mpoints.push_back( d_pi_2 ); @@ -3927,7 +3981,7 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { mpoints.push_back( d_pi_neg_2 ); mpoints.push_back( d_pi_neg ); } - else if (it->first == EXPONENTIAL) + else if (k == EXPONENTIAL) { mpoints.push_back( Node::null() ); } @@ -3946,7 +4000,8 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { int monotonic_dir = -1; Node mono_bounds[2]; Node targ, targval, t, tval; - for( unsigned i=0; ifirst].size(); i++ ){ + for (unsigned i = 0, size = sorted_tf_args[k].size(); i < 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]; @@ -3975,7 +4030,7 @@ std::vector NonlinearExtension::checkTranscendentalMonotonic() { tval = Node::null(); mono_bounds[1] = mpoints[mdir_index]; mdir_index++; - monotonic_dir = regionToMonotonicityDir(it->first, mdir_index); + monotonic_dir = regionToMonotonicityDir(k, mdir_index); if (mdir_index < mpoints.size()) { mono_bounds[0] = mpoints[mdir_index]; @@ -4038,7 +4093,7 @@ std::vector NonlinearExtension::checkTranscendentalTangentPlanes() << std::endl; // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions // via Incremental Linearization" by Cimatti et al - for (std::pair >& tfs : d_tf_rep_map) + for (std::pair >& tfs : d_f_map) { Kind k = tfs.first; if (k == PI) @@ -4060,10 +4115,9 @@ std::vector NonlinearExtension::checkTranscendentalTangentPlanes() // we substitute into the Taylor sum P_{n,f(0)}( x ) - for (std::pair& tfr : tfs.second) + for (const Node& tf : tfs.second) { - // Figure 3 : tf( x ) - Node tf = tfr.second; + // tf is Figure 3 : tf( x ) if (isRefineableTfFun(tf)) { Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl; diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 1e5ca9ad1..c0af312b3 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -580,14 +580,8 @@ class NonlinearExtension { std::map > > d_ci_exp; std::map > > d_ci_max; - /** transcendental function representative map - * - * For each transcendental function n = tf( x ), - * this stores ( n.getKind(), r ) -> n - * where r is the current representative of x - * in the equality engine assoiated with this class. - */ - std::map > d_tf_rep_map; + /** A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } */ + std::map > d_f_map; // factor skolems std::map< Node, Node > d_factor_skolem; -- 2.30.2