diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-06 12:31:31 -0600 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-11-06 17:19:09 -0600 |
commit | 6d2def1c2e44974227fb06d3aa199722a4193a04 (patch) | |
tree | 1020f03dfbef0e9e5c8759b888dd75885aa2ac37 /src/theory/quantifiers/bounded_integers.cpp | |
parent | 4ab031f6173ca18aa21c938bc2672ef25c283428 (diff) |
Bug fixes for bounded integer quantification. Current best strategy is to turn off MBQI. Disable relevant triggers by default.
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r-- | src/theory/quantifiers/bounded_integers.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 30ff5242b..ab6b35e01 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -190,7 +190,6 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, } }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; - exit(0); } } @@ -232,7 +231,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { if( f[0][i].getType().isInteger() ){ hasIntType = true; } - else if( f[0][i].getType().isSort() ){ + else if( f[0][i].getType().isSort() || f[0][i].getType().getCardinality().isFinite() ){ finiteTypes++; } } @@ -292,6 +291,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { } }else{ Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl; + //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl; } } } |