diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-27 09:27:19 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-09-27 09:27:29 -0500 |
| commit | e277b4d220a1d15ac32f6e4fc5f06e88f55b7f68 (patch) | |
| tree | 2a56691dea81453e5f9ba42e859fdc6783fa1545 /src/theory/rep_set.cpp | |
| parent | ccd1ca4c32e8a3eac8b18911a7b2d32b55203707 (diff) | |
Add new symmetry breaking technique for finite model finding. Improvements to bounded integer quantifier instantiation.
Diffstat (limited to 'src/theory/rep_set.cpp')
| -rw-r--r-- | src/theory/rep_set.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 647ef965a..800e007f7 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -278,7 +278,12 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); d_domain[ii].clear(); - d_lower_bounds[ii] = l; + Node tl = l; + Node tu = u; + if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ + d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu ); + } + d_lower_bounds[ii] = tl; if( ra==NodeManager::currentNM()->mkConst(true) ){ long rr = range.getConst<Rational>().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; |