summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ceg_instantiator.cpp
AgeCommit message (Expand)Author
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
2015-11-11Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to cbq...ajreynol
2015-11-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-10-26Extend counterexample-guided instantiation to extended theory of Int/Real, mi...ajreynol
2015-10-22Enable counterexample-guided quantifier instantiation by default for quantifi...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback