summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/ce_guided_instantiation.h
AgeCommit message (Expand)Author
2018-02-01Add interface in sygus to get synthesis solution Nodes (#1552)Andrew Reynolds
2017-11-14Make QEffort an enum (#1366)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
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
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-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
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-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
2015-12-14Refactoring Options Handler & Library Cycle BreakingTim King
2015-12-01More work on --cegqi-si-partial, incomplete.ajreynol
2015-11-28Initial work on --cegqi-si-partial, refactoring.ajreynol
2015-08-28Improvements to sygus, register equivalent terms based on rewrites of origina...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-05-29Do not enforce dt fairness when single invocation sygus.ajreynol
2015-05-10Minor improvements to infrastructure. Minor changes to default options. Add t...ajreynol
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-03-11Minor fixes and improvements to cegqi-si for linear arithmetic.ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation -...ajreynol
2015-01-30Generalize conflict clauses in sygus sym break, merge caches, refactor. Prep...ajreynol
2015-01-28Minor refactor CEGQI.ajreynol
2015-01-27Recognize when synthesis conjectures are in single invocation fragment.ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor refactor...ajreynol
2015-01-20Handle miniscoping of conjunctions in synthesis properties. Refactor constru...ajreynol
2015-01-16Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding de...ajreynol
2014-11-07Properly distinguish which EQC to assign values in datatypes, use assertRepre...ajreynol
2014-11-01Fix cegqi for synthesis without syntax.ajreynol
2014-10-16Add dt.size to datatypes theory. Add option for fairness strategy used by CE...ajreynol
2014-10-13CEGQI uses model. Enforce fairness in CEGQI natively.ajreynol
2014-10-13Refactor model builder from model engine to quant engine. Work on fairness s...ajreynol
2014-10-10Initial draft of CEGQI.ajreynol
2014-10-10Add owner map to better manage QuantifiersModules. Initial infrastructure fo...ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback