summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/cegqi
AgeCommit message (Collapse)Author
2018-09-17Move inst_strategy_cbqi to inst_strategy_cegqi (#2477)Andrew Reynolds
2018-09-14Refactor 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-10Squash 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-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-08-02Improve CEGQI heuristics involving equality and multiple instantiations (#2254)Andrew Reynolds
2018-08-01Improvements 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-02Modify cegqi heuristic for finite datatypes (#2126)Andrew Reynolds
2018-06-28Split and document ceg theory instantiators (#2094)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-15Disable solving non-linear BV literals by default (#2070)Andrew Reynolds
2018-06-04Enable cegqi (with model values) for floating point by default (#2023)Andrew Reynolds
2018-06-02Fix corner case of mixed int/real cegqi. (#2046)Andrew Reynolds
2018-06-01Apply preprocessing to counterexample lemmas in CEGQI (#2027)Andrew Reynolds
2018-05-30Fixes for quantifiers + incremental (#2009)Andrew Reynolds
2018-05-27Fix cegqi assertions for quantified non-linear cases. (#1999)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-15Fix free variables in cbqi preregister inst. (#1921)Andrew Reynolds
2018-05-08Infrastructure for CEGQI handled status (#1873)Andrew Reynolds
2018-05-03Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)Andrew Reynolds
2018-04-16Skolemize candidate rewrite rule checks (#1777)Andrew Reynolds
2018-04-09Fix hasSubterm calls for higher-order (#1760)Andrew Reynolds
2018-03-19Enable CEGQI for non-linear (#1674)Andrew Reynolds
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback