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

[cvc5.git] / src / theory / quantifiers_engine.cpp

2015-04-26	ajreynol	Bug fixes and improvements for mbqi with theory symbols...	blob \| commitdiff \| raw
2015-04-17	Kshitij Bansal	Merge pull request #72 from kbansal/decision-requirephase	blob \| commitdiff \| raw \| diff to current
2015-04-09	ajreynol	Fix performance issue with variable triggers + instanti...	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-02-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	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-01-29	ajreynol	Restrict LtePartialInst instantiations based on E-match...	blob \| commitdiff \| raw \| diff to current
2015-01-26	ajreynol	Output solutions for synthesis conjectures with --dump...	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-28	ajreynol	Synchronize conjecture generation with E-matching....	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-20	ajreynol	Disable constants sharing in eq engine, disable hack...	blob \| commitdiff \| raw \| diff to current
2014-11-18	ajreynol	Compute model basis only for fmf. Add another co-datat...	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	Remove two obsolete versions of MBQI.	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	ajreynol	Enable --quant-cf by default. Fix bug in qcf for mixed...	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	ajreynol	Properly distinguish which EQC to assign values in...	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	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-13	ajreynol	CEGQI uses model. Enforce fairness in CEGQI natively.	blob \| commitdiff \| raw \| diff to current
2014-10-13	ajreynol	Model building into quantifiers engine. Simplify axiom...	blob \| commitdiff \| raw \| diff to current
2014-10-13	ajreynol	Refactor model builder from model engine to quant engin...	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	Kshitij Bansal	Merge remote-tracking branch 'upstream/master' into...	blob \| commitdiff \| raw \| diff to current
2014-10-07	ajreynol	Cache for getInstance, thanks to Johannes Kanig for...	blob \| commitdiff \| raw \| diff to current
2014-10-07	ajreynol	Refactor quantifiers attributes.	blob \| commitdiff \| raw \| diff to current
2014-10-07	Morgan Deters	Fix a resource limiting issue where interruption didn...	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-26	Morgan Deters	Finer-grained resource-limiting in quantifiers.	blob \| commitdiff \| raw \| diff to current
2014-09-24	ajreynol	Refactor option for uf+cardinality constraints solver.	blob \| commitdiff \| raw \| diff to current
2014-09-23	ajreynol	Do not throw error when codatatype is not well-founded...	blob \| commitdiff \| raw \| diff to current
2014-09-18	Morgan Deters	Resource spending support in theories (and especially...	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	Bug fix variable triggers with --inst-max-level : use...	blob \| commitdiff \| raw \| diff to current
2014-09-08	ajreynol	Accept user-provided triggers with variable terms....	blob \| commitdiff \| raw \| diff to current
2014-08-29	ajreynol	Set instantiation level on skolemized bodies of quantif...	blob \| commitdiff \| raw \| diff to current
2014-08-26	ajreynol	Bug fixes for --purify-triggers, --dt-force-assignment.	blob \| commitdiff \| raw \| diff to current
2014-08-25	ajreynol	New option --purify-triggers. Refactoring of InstMatch...	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-21	ajreynol	Avoid doing work in quantifiers engine when no quantifi...	blob \| commitdiff \| raw \| diff to current
2014-08-20	ajreynol	Fix --inst-max-level for strategies that use arbitrary...	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-05-30	ajreynol	Fixes for --inst-max-level	blob \| commitdiff \| raw \| diff to current
2014-05-14	Andrew Reynolds	Finish --dump-instantiations option. Update scripts.	blob \| commitdiff \| raw \| diff to current
2014-05-13	ajreynol	Add lazy strategy for bounded integers to avoid non...	blob \| commitdiff \| raw \| diff to current
2014-05-13	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-05-12	Andrew Reynolds	Minor updates/fix to --cbqi-recurse	blob \| commitdiff \| raw \| diff to current
2014-05-12	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-05-11	Andrew Reynolds	More preparation for CASC proofs. Minor fix for sort...	blob \| commitdiff \| raw \| diff to current
2014-05-08	Andrew Reynolds	Fixes to quantifiers rewriter to prevent miniscoping...	blob \| commitdiff \| raw \| diff to current
2014-05-06	Andrew Reynolds	First draft of ambqi_builder (new implementation of...	blob \| commitdiff \| raw \| diff to current
2014-04-30	Morgan Deters	Mostly resolves bug #561 memory leaks, and more.	blob \| commitdiff \| raw \| diff to current
2014-04-28	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-04-28	Kshitij Bansal	Merge pull request #25 from kbansal/sets	blob \| commitdiff \| raw \| diff to current
2014-04-28	Andrew Reynolds	Preparation for models for co-inductive datatypes....	blob \| commitdiff \| raw \| diff to current
2014-04-28	ajreynol	Optimizations for datatypes: check for clashes modulo...	blob \| commitdiff \| raw \| diff to current
2014-04-28	Kshitij Bansal	Merge remote-tracking branch 'upstream/master' into...	blob \| commitdiff \| raw \| diff to current
2014-04-24	Andrew Reynolds	Add --inst-max-level=N option for Kshitij. Support...	blob \| commitdiff \| raw \| diff to current
2014-04-10	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-04-09	Kshitij Bansal	Merge pull request #24 from kbansal/sets-model	blob \| commitdiff \| raw \| diff to current
2014-04-09	Andrew Reynolds	Handle fmf.card as input from user, add support in...	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
next

RSS Atom