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/quantifiers/bounded_integers.cpp | |
parent | ccd1ca4c32e8a3eac8b18911a7b2d32b55203707 (diff) |
Add new symmetry breaking technique for finite model finding. Improvements to bounded integer quantifier instantiation.
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index e1e2f96c2..30ff5242b 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -321,7 +321,7 @@ Node BoundedIntegers::getNextDecisionRequest() { return Node::null(); } -void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { +void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { l = d_bounds[0][f][v]; u = d_bounds[1][f][v]; if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){ @@ -356,6 +356,10 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); } } +} + +void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { + getBounds( f, v, rsi, l, u ); Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl; l = d_quantEngine->getModel()->getCurrentModelValue( l ); u = d_quantEngine->getModel()->getCurrentModelValue( u ); |