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