diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-24 18:34:25 +0200 |
| commit | d7dc7c2b3038b862af5ea55e7cf6b1fc4e1fe684 (patch) | |
| tree | d6c229a2659bfcb3cdf7c7c786414ecc1e59e61c /src/theory/quantifiers/quant_util.cpp | |
| parent | 1ec95c559074ed7575a0165deb16fcee45920e9f (diff) | |
Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default.
Diffstat (limited to 'src/theory/quantifiers/quant_util.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 938245871..ebeb4b871 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -115,10 +115,14 @@ int QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind (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 ); + if( vc.getType().isInteger() ){ + if( doCoeff ){ + vc = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( r.abs() ), vc ); + }else{ + return 0; + } }else{ - return 0; + veq = NodeManager::currentNM()->mkNode( MULT, veq, NodeManager::currentNM()->mkConst( Rational(1) / r.abs() ) ); } } if( r.sgn()==1 ){ |