diff options
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 6b07a87e0..53f67853b 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -71,7 +71,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind 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!=v ){ + if( it->first.isNull() || it->first!=v ){ Node m; if( !it->first.isNull() ){ if ( !it->second.isNull() ){ @@ -111,6 +111,12 @@ Node QuantArith::negate( Node t ) { return tt; } +Node QuantArith::offset( Node t, int i ) { + Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t ); + tt = Rewriter::rewrite( tt ); + return tt; +} + void QuantRelevance::registerQuantifier( Node f ){ //compute symbols in f |