git.libre-soc.org Git - cvc5.git/history

2015-04-09	ajreynol	Fix unsat-core issues related to rewrite rules, quantif...	blob \| commitdiff \| raw
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-16	Liana Hadarean	Fixed proof unitialized memory and minor memory leaks.	blob \| commitdiff \| raw \| diff to current
2015-03-10	ajreynol	CNF proofs. Infrastructure for preprocessing proofs...	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-06	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2015-02-02	ajreynol	Single invocation module for counterexample guided...	blob \| commitdiff \| raw \| diff to current
2015-01-27	ajreynol	Always miniscope nested quantifiers. Disable miniscopi...	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-22	ajreynol	Narrow sygus search space based on NNF and rewriting...	blob \| commitdiff \| raw \| diff to current
2015-01-22	ajreynol	Do not drop patterns during boolean term rewriting...	blob \| commitdiff \| raw \| diff to current
2015-01-13	Morgan Deters	Fix a memory issue in ResourceManager on 32-bit (resolv...	blob \| commitdiff \| raw \| diff to current
2015-01-07	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-12-28	ajreynol	Disable prenex by default when using fmf bound int...	blob \| commitdiff \| raw \| diff to current
2014-12-16	Morgan Deters	Fix oversight in dumping assertions in preprocessing.	blob \| commitdiff \| raw \| diff to current
2014-12-04	Morgan Deters	Fix segfault in lambdas when constructed via API.	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-22	lianah	added number of resource units used as a stat	blob \| commitdiff \| raw \| diff to current
2014-11-21	ajreynol	Change default option to --inst-when=full-last-call...	blob \| commitdiff \| raw \| diff to current
2014-11-19	Kshitij Bansal	Merge pull request #70 from kbansal/sets-for-merge...	blob \| commitdiff \| raw \| diff to current
2014-11-19	Kshitij Bansal	Set Constant's normal form and other short fixes	blob \| commitdiff \| raw \| diff to current
2014-11-18	ajreynol	Add local theory extensions instantiation strategy...	blob \| commitdiff \| raw \| diff to current
2014-11-17	Liana Hadarean	Resource-limiting work.	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-11	Kshitij Bansal	Merge pull request #64 from mdeters/theorysets-hashset...	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	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-11-09	Morgan Deters	Fix a deterministic assignment-ordering for get-assignm...	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	Corrected fix for missing case in model postprocessor...	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	Revert "Fix missing case in model postprocessor (resolv...	blob \| commitdiff \| raw \| diff to current
2014-11-07	Morgan Deters	Revert "Fix missing case in model postprocessor (resolv...	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	Fix missing case in model postprocessor (resolves bug...	blob \| commitdiff \| raw \| diff to current
2014-11-05	Morgan Deters	Merge branch '1.4.x'	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-23	Morgan Deters	Parsing and infrastructure support for SMT-LIBv2.5...	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	ajreynol	Make --user-pat=trust default. Fix a few warnings...	blob \| commitdiff \| raw \| diff to current
2014-10-16	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-14	Morgan Deters	Merge pull request #58 from mdeters/smt-attributes	blob \| commitdiff \| raw \| diff to current
2014-10-14	Morgan Deters	Context-dependent expr attributes are now attached...	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-10-11	Morgan Deters	Some defensive programming at destruction time, and...	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-09	Morgan Deters	Merge branch '1.4.x'	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-06	Morgan Deters	Support for RESET command in CVC native language (and...	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-10-02	Morgan Deters	Fix comment in SmtEngine.	blob \| commitdiff \| raw \| diff to current
2014-09-30	Morgan Deters	Merge branch '1.4.x'	blob \| commitdiff \| raw \| diff to current
2014-09-30	Morgan Deters	Proofs- and cores-related segfault fixes (mainly a...	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-09-03	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2014-09-03	ajreynol	Implement and enable --dt-var-exp-quant, cleanup trace...	blob \| commitdiff \| raw \| diff to current
2014-08-29	ajreynol	Do not use pure theory terms as single triggers. Minor...	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-23	Morgan Deters	Unsat core printing.	blob \| commitdiff \| raw \| diff to current
2014-08-23	Morgan Deters	Some fixes for dump- and get-unsat-core.	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	One small thing forgotten in core commit.	blob \| commitdiff \| raw \| diff to current
2014-08-22	Morgan Deters	Unsat core infrastruture and API (SMT-LIB compliance...	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-15	Kshitij Bansal	Update smt_engine.cpp	blob \| commitdiff \| raw \| diff to current
2014-07-13	Morgan Deters	Fix a bug in Boolean terms and arrays. Thanks to Jean...	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-07-01	Morgan Deters	Merge pull request #44 from mdeters/prio-queue-updates	blob \| commitdiff \| raw \| diff to current
2014-07-01	Morgan Deters	Merge pull request #45 from mdeters/turn-off-strings-exp	blob \| commitdiff \| raw \| diff to current
2014-06-30	Kshitij Bansal	Merge pull request #47 from kbansal/sets	blob \| commitdiff \| raw \| diff to current
2014-06-26	Morgan Deters	Merge tag 'smtcomp2014-resubmission'	blob \| commitdiff \| raw \| diff to current
2014-06-25	Andrew Reynolds	Merge pull request #34 from mdeters/datatypes-kinds	blob \| commitdiff \| raw \| diff to current
2014-06-25	Andrew Reynolds	Merge pull request #37 from mdeters/quants-kinds	blob \| commitdiff \| raw \| diff to current
2014-06-25	Andrew Reynolds	Merge pull request #38 from mdeters/uf-kinds	blob \| commitdiff \| raw \| diff to current
2014-06-25	Morgan Deters	Turn strings-exp off by default (for the release)	blob \| commitdiff \| raw \| diff to current
2014-06-23	Morgan Deters	Fatal error if --unconstrained-simp and --produce-model...	blob \| commitdiff \| raw \| diff to current
2014-06-22	Morgan Deters	Merge tag 'smtcomp2014-application'	blob \| commitdiff \| raw \| diff to current
2014-06-19	lianah	fixed merge conflict	blob \| commitdiff \| raw \| diff to current
2014-06-19	lianah	added model generation to eager bit-blasting and turned...	blob \| commitdiff \| raw \| diff to current
2014-06-19	Morgan Deters	New translator features: expand define-funs and combine...	blob \| commitdiff \| raw \| diff to current
2014-06-19	Morgan Deters	Fix for new CASC features, fixes Java builds.	blob \| commitdiff \| raw \| diff to current
2014-06-19	ajreynol	For casc : print models of functions rewritten by sort...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom