Age | Commit message (Expand) | Author |
2018-02-14 | Quantifiers subdirectories (#1608) | Andrew Reynolds |
2018-01-04 | Improvements for CBQI (#1478) | Andrew Reynolds |
2017-12-29 | Cbqi repeat solve literal (#1458) | Andrew Reynolds |
2017-12-28 | Fixes for cbqi (#1453) | Andrew Reynolds |
2017-11-30 | Remove remaining references to QuantArith (#1408) | Andrew Reynolds |
2017-11-29 | Minor improvements and changes to defaults for cbqi bv (#1406) | Andrew Reynolds |
2017-11-21 | Cegqi bv remove extract terms preprocess pass (#1376) | Andrew Reynolds |
2017-11-14 | Clean Ceg Instantiators (#1365) | Andrew Reynolds |
2017-11-01 | (Refactor) Split term util (#1303) | Andrew Reynolds |
2017-11-01 | CBQI BV choice expressions (#1296) | Andrew Reynolds |
2017-10-27 | Cbqi multiple instantiation (#1289) | Andrew Reynolds |
2017-10-12 | Initial support for solving bit-vector inequalities (#1229) | Andrew Reynolds |
2017-10-09 | Split term database (#1206) | Andrew Reynolds |
2017-09-29 | Simplify representation of inversion Skolems for bv cegqi (#1164) | Andrew Reynolds |
2017-09-28 | Cegqi refactor prep bv (#1155) | Andrew Reynolds |
2017-09-25 | Cegqi refactor substitutions (#1129) | Andrew Reynolds |
2017-09-19 | Refactor cegqi instantiation infrastructure so that it is more independent of... | Andrew Reynolds |
2017-09-12 | Initial infrastructure for BV instantiation via word-level inversions. (#1056) | Andrew Reynolds |
2017-07-07 | Update copyright headers. | Mathias Preiner |
2017-06-30 | Minor change to trigger selection, fixes related to subtypes (in macros, cbqi... | ajreynol |
2017-05-15 | Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802. | ajreynol |
2017-03-29 | Add quantifiers options related to model and master equality engine. | ajreynol |
2017-03-10 | Minor fix for cbqi-all. | ajreynol |
2017-03-02 | Minor cleanup and reorganization related to last commit. | ajreynol |
2017-03-02 | Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole... | ajreynol |
2016-10-13 | Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git" | Tim King |
2016-10-11 | Merge branch 'origin' of https://github.com/CVC4/CVC4.git | Paul Meng |
2016-09-29 | Address some coverity warnings, add another stat. | ajreynol |
2016-09-21 | Remove duplicate code from my last commit | ajreynol |
2016-09-20 | Refactor, separate theory-specific counterexample-guided instantiation. | ajreynol |
2016-09-20 | More refactoring of cbqi. Add a few regressions. Add option for qcf. | ajreynol |
2016-09-16 | Use matching heuristics for EPR instantiation. | ajreynol |
2016-09-16 | More refactoring of cbqi, start developing new interface. | ajreynol |
2016-09-15 | Further refactor cbqi. | ajreynol |
2016-09-15 | Begin refactoring of cbqi, remove a few dead options. Pre-skolemize by defaul... | ajreynol |
2016-09-01 | Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifier... | ajreynol |
2016-08-25 | Options for counterexample guided instantiation. | ajreynol |
2016-08-24 | Merge remote-tracking branch 'origin/master' | PaulMeng |
2016-08-12 | Minor fixes to model construction to take singleton equivalence classes into ... | ajreynol |
2016-07-05 | Merge branch 'master' of https://github.com/CVC4/CVC4.git | PaulMeng |
2016-05-26 | Use term indexing in TheoryUF::computeCareGraph. Do not reject model value in... | ajreynol |
2016-05-17 | Minor fix cbqi for constant monomials. | ajreynol |
2016-04-20 | update from the master | PaulMeng |
2016-04-10 | More work on instantiation propagation. Enable external filtering of instanti... | ajreynol |
2016-04-03 | Updating the copyright headers and scripts. | Tim King |
2016-03-02 | Work towards complete instantiation for datatypes. | ajreynol |
2016-02-02 | Moving dump.*, command.*, model.*, and ite_removal.* from smt_util/ to smt/. ... | Tim King |
2015-12-22 | Bug fix for cbqi, do not use model values for terms involving non-enumerable ... | ajreynol |
2015-12-14 | Refactoring Options Handler & Library Cycle Breaking | Tim King |
2015-11-18 | Option for midpoints in cbqi. | ajreynol |