diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:27 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-03-04 10:39:38 +0100 |
commit | 74f1358ca108f3ae4bc8b2d01a2c14e0c20bcc9b (patch) | |
tree | ffcd22bc1205e4619e05af2eac79918287af2374 /src/theory/quantifiers/quant_util.cpp | |
parent | f6833bca76627f970d3c61ee163a32869ffa1b10 (diff) |
More work on arithmetic single invocation synthesis conjectures.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
-rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 61 |
1 files changed, 13 insertions, 48 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 1d3bf7c2a..c10f1db53 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -90,47 +90,7 @@ bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) { return false; } -bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ) { - if( msum.find(v)!=msum.end() ){ - std::vector< Node > children; - Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>(); - if ( r.sgn()!=0 ){ - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if( it->first.isNull() || it->first!=v ){ - Node m; - if( !it->first.isNull() ){ - if ( !it->second.isNull() ){ - m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first ); - }else{ - m = it->first; - } - }else{ - m = it->second; - } - children.push_back(m); - } - } - veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : - (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); - if( !r.isNegativeOne() ){ - if( r.isOne() ){ - veq = negate(veq); - }else{ - //TODO : gcd computation - return false; - } - } - veq = Rewriter::rewrite( veq ); - veq = NodeManager::currentNM()->mkNode( k, r.sgn()==1 ? v : veq, r.sgn()==1 ? veq : v ); - return true; - } - return false; - }else{ - return false; - } -} - -bool QuantArith::isolateEqCoeff( Node v, std::map< Node, Node >& msum, Node & veq ) { +int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k, bool doCoeff ) { std::map< Node, Node >::iterator itv = msum.find( v ); if( itv!=msum.end() ){ std::vector< Node > children; @@ -153,19 +113,24 @@ bool QuantArith::isolateEqCoeff( Node v, std::map< Node, Node >& msum, Node & ve } veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) : (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) )); + Node vc = v; + if( !r.isOne() && !r.isNegativeOne() ){ + if( doCoeff ){ + vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); + }else{ + return 0; + } + } if( r.sgn()==1 ){ veq = negate(veq); } veq = Rewriter::rewrite( veq ); - Node vc = v; - if( !r.isOne() && !r.isNegativeOne() ){ - vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); - } - veq = NodeManager::currentNM()->mkNode( EQUAL, vc, veq ); - return true; + bool inOrder = r.sgn()==1 || k==EQUAL; + veq = NodeManager::currentNM()->mkNode( k, inOrder ? vc : veq, inOrder ? veq : vc ); + return inOrder ? 1 : -1; } } - return false; + return 0; } Node QuantArith::negate( Node t ) { |