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

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

2015-09-11	ajreynol	Minor cleanup related to codatatypes.	blob \| commitdiff \| raw
2015-09-06	ajreynol	Improve quantifiers rewriter, minor refactoring.	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-24	ajreynol	Improvements to vts in cbqi, bug fix vts for non-atomic...	blob \| commitdiff \| raw \| diff to current
2015-08-19	ajreynol	Make cbqi robust to term ITE removal. Separate vts...	blob \| commitdiff \| raw \| diff to current
2015-08-16	ajreynol	More optimizations to --macros-quant, add --macros...	blob \| commitdiff \| raw \| diff to current
2015-07-31	ajreynol	Sygus support for inductive datatypes.	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-20	ajreynol	Squashed merge of SygusComp 2015 branch.	blob \| commitdiff \| raw \| diff to current
2015-06-29	ajreynol	Module to infer alpha equivalence of quantified formula...	blob \| commitdiff \| raw \| diff to current
2015-06-27	ajreynol	Refactor various corner cases of fmf, quantifiers modul...	blob \| commitdiff \| raw \| diff to current
2015-06-16	ajreynol	Avoid completion for large finite types. Fix bug for...	blob \| commitdiff \| raw \| diff to current
2015-06-12	ajreynol	Accelerate sygus solution reconstruction for constants...	blob \| commitdiff \| raw \| diff to current
2015-06-10	ajreynol	Support for printing solutions involving LetGTerm 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-05-10	ajreynol	Minor improvements to infrastructure. Minor changes...	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-08	ajreynol	Make fun-def quantifiers carry the function app they...	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	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-01-24	ajreynol	Variable patterns only look at eligible terms. Minor...	blob \| commitdiff \| raw \| diff to current
2015-01-24	ajreynol	Add --lte-restrict-inst-closure option. Push dt.size...	blob \| commitdiff \| raw \| diff to current
2015-01-23	ajreynol	Rework inst-closure.	blob \| commitdiff \| raw \| diff to current
2015-01-22	ajreynol	Add option --lte-partial-inst. Remove inst-closure.	blob \| commitdiff \| raw \| diff to current
2014-12-03	Kshitij Bansal	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-27	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-11-25	ajreynol	Fix bug in --term-db-mode=relevant with variable trigge...	blob \| commitdiff \| raw \| diff to current
2014-11-18	ajreynol	Add local theory extensions instantiation strategy...	blob \| commitdiff \| raw \| diff to current
2014-11-13	Morgan Deters	Merge pull request #69 from mdeters/bug594	blob \| commitdiff \| raw \| diff to current
2014-11-13	ajreynol	More preparation for filtering relevant terms in TermDb.	blob \| commitdiff \| raw \| diff to current
2014-11-11	Kshitij Bansal	Merge pull request #64 from mdeters/theorysets-hashset...	blob \| commitdiff \| raw \| diff to current
2014-11-11	ajreynol	Work on synchronizing decision=justification and E...	blob \| commitdiff \| raw \| diff to current
2014-11-10	Tianyi Liang	Merge pull request #63 from mdeters/theorystrings-hashs...	blob \| commitdiff \| raw \| diff to current
2014-11-10	ajreynol	Do not eliminate variables only occurring in patterns...	blob \| commitdiff \| raw \| diff to current
2014-11-10	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-31	ajreynol	Do not allow duplication of function definitions. ...	blob \| commitdiff \| raw \| diff to current
2014-10-28	ajreynol	Preprocessing step for finding finite runs of well...	blob \| commitdiff \| raw \| diff to current
2014-10-28	ajreynol	Initial infrastructure for function definition quantifi...	blob \| commitdiff \| raw \| diff to current
2014-10-17	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	Kshitij Bansal	Merge remote-tracking branch 'origin/1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-10	ajreynol	Initial draft of CEGQI.	blob \| commitdiff \| raw \| diff to current
2014-10-10	ajreynol	Add owner map to better manage QuantifiersModules....	blob \| commitdiff \| raw \| diff to current
2014-10-09	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-07	ajreynol	Refactor quantifiers attributes.	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-06	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-03	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-02	Morgan Deters	Merge branch '1.4.x'.	blob \| commitdiff \| raw \| diff to current
2014-09-30	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-27	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-26	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x' while ignoring commit 8d5eb49.	blob \| commitdiff \| raw \| diff to current
2014-09-17	Kshitij Bansal	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-16	ajreynol	Refactoring of conjecture generator. Determine subgoal...	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-19	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-18	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-08-18	ajreynol	Add support for quantifier-specific instantiation level...	blob \| commitdiff \| raw \| diff to current
2014-08-01	ajreynol	Minor cleanup from previous commit. Better organizatio...	blob \| commitdiff \| raw \| diff to current
2014-07-31	ajreynol	New module for generating candidate equality conjecture...	blob \| commitdiff \| raw \| diff to current
2014-07-10	Kshitij Bansal	Merge remote-tracking branch 'origin/master' into segfa...	blob \| commitdiff \| raw \| diff to current
2014-07-01	Morgan Deters	Update copyrights.	blob \| commitdiff \| raw \| diff to current
2014-06-26	Morgan Deters	Merge tag 'smtcomp2014-resubmission'	blob \| commitdiff \| raw \| diff to current
2014-06-22	Morgan Deters	Merge tag 'smtcomp2014-application'	blob \| commitdiff \| raw \| diff to current
2014-06-19	ajreynol	More proof support for CASC : include skolemization	blob \| commitdiff \| raw \| diff to current
2014-06-16	ajreynol	More proof support for CASC : include skolemization	blob \| commitdiff \| raw \| diff to current
2014-06-03	ajreynol	Support E-matching/QCF for Set operators.	blob \| commitdiff \| raw \| diff to current
2014-05-23	Andrew Reynolds	Fix bug in E-matching Real/Int terms.	blob \| commitdiff \| raw \| diff to current
2014-05-02	Andrew Reynolds	Add option --dt-stc-ind for strengthening skolemization...	blob \| commitdiff \| raw \| diff to current
2014-05-01	Kshitij Bansal	Merge remote-tracking branch 'upstream/master' into...	blob \| commitdiff \| raw \| diff to current
2014-04-30	Tim King	T-entailment work, and QCF (quant conflict find) work...	blob \| commitdiff \| raw \| diff to current
2014-04-01	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-26	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-21	Kshitij Bansal	Merge pull request #22 from kbansal/sets-model	blob \| commitdiff \| raw \| diff to current
2014-03-12	Andrew Reynolds	Work on array pf signature, add working example. Add...	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-03-11	Andrew Reynolds	Initial refactor of rewrite rules, make theory_rewriter...	blob \| commitdiff \| raw \| diff to current
2014-03-10	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-03-08	Tim King	Merge remote-tracking branch 'CVC4root/master'	blob \| commitdiff \| raw \| diff to current
2014-03-08	Morgan Deters	Remove --ite-remove-quant; support pulling ground ITEs...	blob \| commitdiff \| raw \| diff to current
2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-21	Morgan Deters	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-02-19	Tim King	Merge branch '1.3.x'	blob \| commitdiff \| raw \| diff to current
2014-01-28	Andrew Reynolds	More optimizations of quantifier instantiation data...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom