diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-10 06:08:46 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-08-11 01:06:50 -0500 |
commit | 4b5460a79838e93f8d417462c930806a77c09d31 (patch) | |
tree | cc5cff557348caf6310393fe7fb5996b46526b19 /src/theory/arith | |
parent | 0ce756c379c753899c62f88e725bac4a55dea1cd (diff) |
Maintain frontier for tangent planes.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 76 | ||||
-rw-r--r-- | src/theory/arith/nonlinear_extension.h | 3 |
2 files changed, 57 insertions, 22 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 42f9636dc..3c3301db1 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -2034,28 +2034,60 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() { 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); + Node a_v_c = computeModelValue(a, 1); + Node b_v_c = computeModelValue(b, 1); + // points we will add tangent planes for + std::vector< Node > pts[2]; + pts[0].push_back( a_v_c ); + pts[1].push_back( b_v_c ); + // if previously refined + bool prevRefine = d_tangent_val_bound[0][a].find( b )!=d_tangent_val_bound[0][a].end(); + // a_min, a_max, b_min, b_max + for( unsigned p=0; p<4; p++ ){ + Node curr_v = p<=1 ? a_v_c : b_v_c; + if( prevRefine ){ + Node pt_v = d_tangent_val_bound[p][a][b]; + Assert( !pt_v.isNull() ); + if( curr_v!=pt_v ){ + Node do_extend = NodeManager::currentNM()->mkNode( ( p==1 || p==3 ) ? GT : LT, curr_v, pt_v ); + do_extend = Rewriter::rewrite( do_extend ); + if( do_extend==d_true ){ + for( unsigned q=0; q<2; q++ ){ + pts[ p<=1 ? 0 : 1 ].push_back( curr_v ); + pts[ p<=1 ? 1 : 0 ].push_back( d_tangent_val_bound[ p<=1 ? 2+q : q ][a][b] ); + } + } + } + }else{ + d_tangent_val_bound[p][a][b] = curr_v; + } + } + + for( unsigned p=0; p<pts[0].size(); p++ ){ + Node a_v = pts[0][p]; + Node b_v = pts[1][p]; + + // 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); + } } } } diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index 1a19eb67a..e8cfae1d7 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -243,6 +243,9 @@ private: std::map< Node, Node > d_factor_skolem; Node getFactorSkolem( Node n, std::vector< Node >& lemmas ); + // tangent plane bounds + std::map< Node, std::map< Node, Node > > d_tangent_val_bound[4]; + 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 |