Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-09-17 | Move inst_strategy_cbqi to inst_strategy_cegqi (#2477) | Andrew Reynolds | |
2018-09-14 | Refactor how assertions are added to decision engine (#2396) | Andres Noetzli | |
Before refactoring the preprocessing passes, we were using three arguments to add assertions to the decision engine. Now all that information lives in the AssertionPipeline. This commit moves the AssertionPipeline to its own file and changes the `addAssertions()` methods related to the decision engine to take an AssertionPipeline as an arguement instead of three separate ones. Additionally, the TheoryEngine now uses an AssertionPipeline for lemmas. | |||
2018-09-13 | Decision strategy: incorporate CEGQI (#2460) | Andrew Reynolds | |
2018-09-10 | Squash implementation of counterexample-guided instantiation (#2423) | Andrew Reynolds | |
2018-09-07 | Make isClosedEnumerable a member of TypeNode (#2434) | Andrew Reynolds | |
2018-08-27 | Address more coverity warnings (#2394) | Andrew Reynolds | |
2018-08-24 | Fix more simple coverity warnings (#2372) | Andrew Reynolds | |
2018-08-16 | Move node algorithms to separate file (#2311) | Andres Noetzli | |
2018-08-02 | Improve CEGQI heuristics involving equality and multiple instantiations (#2254) | Andrew Reynolds | |
2018-08-01 | Improvements and fixes in cegqi arithmetic (#2247) | Andrew Reynolds | |
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. | |||
2018-07-02 | Modify cegqi heuristic for finite datatypes (#2126) | Andrew Reynolds | |
2018-06-28 | Split and document ceg theory instantiators (#2094) | Andrew Reynolds | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-06-15 | Disable solving non-linear BV literals by default (#2070) | Andrew Reynolds | |
2018-06-04 | Enable cegqi (with model values) for floating point by default (#2023) | Andrew Reynolds | |
2018-06-02 | Fix corner case of mixed int/real cegqi. (#2046) | Andrew Reynolds | |
2018-06-01 | Apply preprocessing to counterexample lemmas in CEGQI (#2027) | Andrew Reynolds | |
2018-05-30 | Fixes for quantifiers + incremental (#2009) | Andrew Reynolds | |
2018-05-27 | Fix cegqi assertions for quantified non-linear cases. (#1999) | Andrew Reynolds | |
2018-05-22 | Repair constants using symbolic constructors (#1960) | Andrew Reynolds | |
2018-05-15 | Fix free variables in cbqi preregister inst. (#1921) | Andrew Reynolds | |
2018-05-08 | Infrastructure for CEGQI handled status (#1873) | Andrew Reynolds | |
2018-05-03 | Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834) | Andrew Reynolds | |
2018-04-16 | Skolemize candidate rewrite rule checks (#1777) | Andrew Reynolds | |
2018-04-09 | Fix hasSubterm calls for higher-order (#1760) | Andrew Reynolds | |
2018-03-19 | Enable CEGQI for non-linear (#1674) | Andrew Reynolds | |
2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
Adds missing override keywords. | |||
2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds | |