git.libre-soc.org Git - cvc5.git/history - src/theory/quantifiers/ce_guided_single

[cvc5.git] / src / theory / quantifiers / ce_guided_single_inv.h

2017-11-25	Andrew Reynolds	(Refactor) Instantiate utility (#1387)	blob \| commitdiff \| raw
2017-11-17	Andrew Reynolds	(Refactor) Document and clean single invocation partiti...	blob \| commitdiff \| raw \| diff to current
2017-09-30	Andrew Reynolds	SyGuS streaming solution mode (#1131)	blob \| commitdiff \| raw \| diff to current
2017-09-21	Andrew Reynolds	Sygus inv templ refactor (#1110)	blob \| commitdiff \| raw \| diff to current
2017-07-10	ajreynol	Merge datatype shared selectors/sygus comp 2017 branch...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2016-10-13	Tim King	Revert "Merge branch 'origin' of https://github.com...	blob \| commitdiff \| raw \| diff to current
2016-10-11	Paul Meng	Merge branch 'origin' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-10-01	Tim King	Merge pull request #93 from timothy-king/clang-format	blob \| commitdiff \| raw \| diff to current
2016-09-26	Tim King	Adding a destructor to CegqiOutputSingleInv.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-07-26	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-07-26	ajreynol	Add option to minimize sygus solutions based on using...	blob \| commitdiff \| raw \| diff to current
2016-07-05	PaulMeng	Merge branch 'master' of https://github.com/CVC4/CVC4.git	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-10	ajreynol	More work on instantiation propagation. Enable external...	blob \| commitdiff \| raw \| diff to current
2016-04-09	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-03-24	Tim King	Freeing CegConjecture::d_ceg_si. Also making d_ceg_si...	blob \| commitdiff \| raw \| diff to current
2016-03-08	ajreynol	Extend synthesis solver to handle single invocation...	blob \| commitdiff \| raw \| diff to current
2016-03-01	ajreynol	Shorter explanations for strings based on tracking...	blob \| commitdiff \| raw \| diff to current
2015-12-02	ajreynol	Minor fixes for cegqi-si-partial.	blob \| commitdiff \| raw \| diff to current
2015-12-02	Tim King	Merge pull request #79 from CVC4/fix-mac-build-script	blob \| commitdiff \| raw \| diff to current
2015-12-01	ajreynol	More work on --cegqi-si-partial, incomplete.	blob \| commitdiff \| raw \| diff to current
2015-11-28	ajreynol	Initial work on --cegqi-si-partial, refactoring.	blob \| commitdiff \| raw \| diff to current
2015-11-26	ajreynol	Update to new implementation of single invocation parti...	blob \| commitdiff \| raw \| diff to current
2015-11-26	ajreynol	Front-end support for get-value of sort cardinality...	blob \| commitdiff \| raw \| diff to current
2015-11-25	ajreynol	Infrastructure for partially single invocation properti...	blob \| commitdiff \| raw \| diff to current
2015-09-02	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2015-08-28	ajreynol	Improvements to sygus, register equivalent terms based...	blob \| commitdiff \| raw \| diff to current
2015-08-27	ajreynol	Do ITE term bookkeeping when solving Sygus inputs....	blob \| commitdiff \| raw \| diff to current
2015-08-24	ajreynol	Improvements to vts in cbqi, bug fix vts for non-atomic...	blob \| commitdiff \| raw \| diff to current
2015-08-19	ajreynol	Implementation of model-based projection in cbqi, clean...	blob \| commitdiff \| raw \| diff to current
2015-07-30	ajreynol	Implement virtual term substitution for non-nested...	blob \| commitdiff \| raw \| diff to current
2015-07-28	Tianyi Liang	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2015-07-25	ajreynol	Add option --sygus-inv-templ for synthesizing strengthe...	blob \| commitdiff \| raw \| diff to current
2015-07-20	ajreynol	Squashed merge of SygusComp 2015 branch.	blob \| commitdiff \| raw \| diff to current
2015-07-05	ajreynol	Add options --partial-triggers, --elim-taut-quant,...	blob \| commitdiff \| raw \| diff to current
2015-07-02	ajreynol	On-demand upper bound lemmas for deltas in quantified...	blob \| commitdiff \| raw \| diff to current
2015-05-29	ajreynol	Do not enforce dt fairness when single invocation sygus.	blob \| commitdiff \| raw \| diff to current
2015-05-12	barrettcw	Merge pull request #74 from finnhaedicke/namespace_minisat	blob \| commitdiff \| raw \| diff to current
2015-04-23	Clark Barrett	Merge branch 'master' into google	blob \| commitdiff \| raw \| diff to current
2015-04-21	Clark Barrett	Changes needed to compile at Google, plus some bug...	blob \| commitdiff \| raw \| diff to current
2015-04-17	Kshitij Bansal	Merge pull request #72 from kbansal/decision-requirephase	blob \| commitdiff \| raw \| diff to current
2015-04-02	Kshitij Bansal	Merge pull request #71 from kbansal/const-are-triggers	blob \| commitdiff \| raw \| diff to current
2015-04-01	ajreynol	Improvements and bug fixes related to cbqi/cegqi. ...	blob \| commitdiff \| raw \| diff to current
2015-03-23	ajreynol	Decouple counter-example guided quantifier instantiatio...	blob \| commitdiff \| raw \| diff to current
2015-03-11	ajreynol	Minor fixes and improvements to cegqi-si for linear...	blob \| commitdiff \| raw \| diff to current
2015-03-05	ajreynol	Minor fixes. Extend cegqi-si to real arithmetic.	blob \| commitdiff \| raw \| diff to current
2015-03-04	ajreynol	More work on arithmetic single invocation synthesis...	blob \| commitdiff \| raw \| diff to current
2015-02-26	ajreynol	Robust strategy for single invocation LIA synthesis...	blob \| commitdiff \| raw \| diff to current
2015-02-11	ajreynol	Better support for solving multiple functions with...	blob \| commitdiff \| raw \| diff to current
2015-02-11	ajreynol	Move si solution reconstruction to own file, make more...	blob \| commitdiff \| raw \| diff to current
2015-02-06	ajreynol	Handle missing cases for single inv solution reconstruc...	blob \| commitdiff \| raw \| diff to current
2015-02-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2015-02-05	ajreynol	Working version of sygus solution reconstruction from...	blob \| commitdiff \| raw \| diff to current
2015-02-04	ajreynol	Initial draft of solution reconstruction into syntax...	blob \| commitdiff \| raw \| diff to current
2015-02-04	ajreynol	Work on solution reconstruction for single inv. Fix...	blob \| commitdiff \| raw \| diff to current
2015-02-04	ajreynol	Refactor sygus_util to TermDb. Initial work on solutio...	blob \| commitdiff \| raw \| diff to current
2015-02-04	ajreynol	Start work on simplifying single inv solutions. Minor.	blob \| commitdiff \| raw \| diff to current
2015-02-03	ajreynol	Simple variable elimination for single inv properties...	blob \| commitdiff \| raw \| diff to current
2015-02-02	ajreynol	Solutions for single invocation conjectures.	blob \| commitdiff \| raw \| diff to current
2015-02-02	ajreynol	Single invocation module for counterexample guided...	blob \| commitdiff \| raw \| diff to current

RSS Atom