summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ceg_instantiator.h
AgeCommit message (Expand)Author
2017-07-07Update copyright headers.Mathias Preiner
2017-05-15Fix issue in ceg_instantiator related to types and theoryOf, fixes bug 802.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-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-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
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-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
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