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 /src/expr/expr_manager_template.cpp | |
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 'src/expr/expr_manager_template.cpp')
0 files changed, 0 insertions, 0 deletions