diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-26 19:02:21 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-26 19:02:32 -0600 |
commit | dd7e0c66cab285c154f59ff27132059c34e09e23 (patch) | |
tree | 73d61f763801d0c115dfe2e2849abdd771918944 /src/theory/quantifiers/bounded_integers.cpp | |
parent | e45b3b0ff2ffc9bee6f090a4744f6d5eb6da8b72 (diff) |
Bug fix for E-matching select terms, minor fix for bounded integers, bug fix to improve performance of quantifiers rewriter
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index ab6b35e01..080550a16 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -174,15 +174,15 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 ); } Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl; - Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2; - if( !isBound( f, bv ) ){ - if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) { - Trace("bound-int-debug") << "The bound is relevant." << std::endl; - int loru = n1.getKind()==BOUND_VARIABLE ? 0 : 1; - d_bounds[loru][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1); - bound_lit_map[loru][bv] = lit; - bound_lit_pol_map[loru][bv] = pol; - } + Node t = n1==it->first ? n2 : n1; + if( !hasNonBoundVar( f, t ) ) { + Trace("bound-int-debug") << "The bound is relevant." << std::endl; + int loru = n1==it->first ? 0 : 1; + d_bounds[loru][f][it->first] = t; + bound_lit_map[loru][it->first] = lit; + bound_lit_pol_map[loru][it->first] = pol; + }else{ + Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl; } } } |