diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-01 21:24:42 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-01 19:24:42 -0700 |
commit | ea426344ed44b28dcdbe4e631b52250ecef0551f (patch) | |
tree | 2d418d4691f49412761990e591092f304b92e380 /test/regress/regress1/quantifiers/repair-const-nterm.smt2 | |
parent | 551f82a1398c97a5cd1f75b2c411b6fe464cc6ec (diff) |
Improvements and fixes in cegqi arithmetic (#2247)
This includes several improvements for cegqi with arithmetic:
- Randomly choose either lower or upper bounds instead of always using lower bounds (this is similar to cegqi+BV),
- Equalities are handled by processAssertions,
- Resort to *only* model values at full effort instead of trying to mix model values/bounds (this is also similar to cegqi+BV),
- cegqi+arithmetic does not try multiple instantiations unless the flag cbqiMultiInst is set. This makes it so that ceg_instantiator does not have exponential behavior when the strategy is non-monotonic.
It also includes a core fix to computing what bound is optimal based on an ordering that incorporates virtual terms. Previously, we would consider, e.g.:
`a+b*delta > c+d*delta if a>=c and b>=d`
Whereas the correct check is lexicographic:
`a+b*delta > c+d*delta if a>c or a=c and b>d`
This means e.g. 2+(-1)*delta > 3 was previously wrongly inferred.
This is part of merging https://github.com/ajreynol/CVC4/tree/cegqiSingleInst, which is +3-0 on SMTLIB BV and +12-9 on SMTLIB LIA+LRA+NRA+NIA.
Diffstat (limited to 'test/regress/regress1/quantifiers/repair-const-nterm.smt2')
-rw-r--r-- | test/regress/regress1/quantifiers/repair-const-nterm.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/repair-const-nterm.smt2 b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 new file mode 100644 index 000000000..f9b1d6829 --- /dev/null +++ b/test/regress/regress1/quantifiers/repair-const-nterm.smt2 @@ -0,0 +1,12 @@ +(set-logic LIA) +(set-info :status unsat) + +(declare-fun k_20 () Int) +(declare-fun k_72 () Int) +(declare-fun k_73 () Int) + +(assert +(forall ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int) (x7 Int) (x8 Int) (x9 Int) (x10 Int)) (not (>= (+ (* 3 x7) (* (- 1) (ite (= x7 k_20) k_72 k_73))) 1)) ) +) + +(check-sat) |