summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_instantiation.cpp
AgeCommit message (Expand)Author
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-12Minor improvements to sygus sampler (#1598)Andrew Reynolds
2018-02-10More minor improvements to synth-rr (#1597)Andrew Reynolds
2018-02-02Option to use sampling for CEGIS (#1555)Andrew Reynolds
2018-02-01Add interface in sygus to get synthesis solution Nodes (#1552)Andrew Reynolds
2017-11-14Make QEffort an enum (#1366)Andrew Reynolds
2017-11-14(Refactor) Split sygus term db (#1335)Andrew Reynolds
2017-10-09Split term database (#1206)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-08-07Change sygus output for failed reconstruction case.ajreynol
2017-07-20Fix a few bugs related to sygus.ajreynol
2017-07-10Separate sygus term utilities to new file, minor cleanup from last commit.ajreynol
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ...ajreynol
2017-07-07Update copyright headers.Mathias Preiner
2017-03-28Minor refactoring sygus.ajreynol
2017-03-28More work on sygus. Add regress4 to Makefile.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2017-03-22Work on new approach for sygus involving conditional solutions. Refactoring o...ajreynol
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boole...ajreynol
2016-12-02Bug fixes and refactoring of parametric datatypes, add some regressions.ajreynol
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + un...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-01Fix boolean term issue in invariants from sygus. Minor default options change...ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-05-18Refactor modes for sygus+single invocation. Add option --inst-rlv-cond. Mino...ajreynol
2016-05-16Enable --sygus-direct-eval by default, limit to terms that do not induce Bool...ajreynol
2016-05-15Work on --sygus-direct-eval. Minor optimizations, updates to casc scripts. En...ajreynol
2016-05-10Add smt comp 2016 scripts. Fix for --relevant-triggers. Add minor optimizatio...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-13Minor improvements for alpha equivalence and partial quantifier elimination i...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-24Freeing CegConjecture::d_ceg_si. Also making d_ceg_si a provate member of Ceg...Tim King
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2016-01-08Removing StatisticsRegistry's static functions current() and registerStat().Tim King
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-12-02Minor fixes for cegqi-si-partial.ajreynol
2015-12-01More work on --cegqi-si-partial, incomplete.ajreynol
2015-11-28Initial work on --cegqi-si-partial, refactoring.ajreynol
2015-09-06Improve quantifiers rewriter, minor refactoring.ajreynol
2015-08-28Improvements to sygus, register equivalent terms based on rewrites of origina...ajreynol
2015-08-27Do ITE term bookkeeping when solving Sygus inputs. Add missing script from S...ajreynol
2015-08-24Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ...ajreynol
2015-07-25Add option --sygus-inv-templ for synthesizing strengthening/weakening of pre/...ajreynol
2015-07-20Squashed merge of SygusComp 2015 branch.ajreynol
2015-06-10Support for printing solutions involving LetGTerm sygus. Bug fix define-fun w...ajreynol
2015-06-03Refactoring of sygus parsing, properly parse Constant/Variable constructors.ajreynol
2015-05-29Do not enforce dt fairness when single invocation sygus.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback