diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-08-01 09:36:10 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-08-01 09:36:10 -0700 |
| commit | a362e943bf543b7bd31d14525f8f76e15cb65f87 (patch) | |
| tree | be10b95d17382c4ad119860123360c68e367bc0b | |
| parent | 8078ed4c404238371a34d2c122e1489d6de9d3a9 (diff) | |
Bidirectional quantifier instantiationbidirQuantInst
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index f873b94f2..ac5566405 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -746,10 +746,17 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node if( ra==d_quantEngine->getTermUtil()->d_true ){ long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; - for( unsigned k=0; k<rr; k++ ){ - Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) ); - t = Rewriter::rewrite( t ); - elements.push_back( t ); + for (unsigned k = 0; k < rr; k++) + { + Node t = NodeManager::currentNM()->mkNode( + PLUS, tl, NodeManager::currentNM()->mkConst(Rational(k))); + t = Rewriter::rewrite(t); + elements.push_back(t); + + Node t2 = NodeManager::currentNM()->mkNode( + MINUS, tu, NodeManager::currentNM()->mkConst(Rational(k))); + t2 = Rewriter::rewrite(t2); + elements.push_back(t2); } return true; }else{ |