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

[cvc5.git] / src / theory / quantifiers / model_engine.cpp

2017-11-25	Andrew Reynolds	(Refactor) Instantiate utility (#1387)	blob \| commitdiff \| raw
2017-11-15	Andrew Reynolds	Make QEffort an enum (#1366)	blob \| commitdiff \| raw \| diff to current
2017-11-14	Andrew Reynolds	(Refactor) Decouple rep set iterator and quantifiers...	blob \| commitdiff \| raw \| diff to current
2017-11-01	Andrew Reynolds	(Refactor) Split term util (#1303)	blob \| commitdiff \| raw \| diff to current
2017-10-27	Andrew Reynolds	Refactor theory model (#1236)	blob \| commitdiff \| raw \| diff to current
2017-10-10	Andrew Reynolds	Split term database (#1206)	blob \| commitdiff \| raw \| diff to current
2017-08-24	Andrew Reynolds	Merge pull request #191 from timothy-king/cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-08-17	ajreynol	Add mbqi interleave option, change option fs-inst to...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-03-29	ajreynol	Add quantifiers options related to model and master...	blob \| commitdiff \| raw \| diff to current
2017-03-24	ajreynol	Refactor model building for quantifiers to be a single...	blob \| commitdiff \| raw \| diff to current
2016-12-02	Tim King	Merge pull request #95 from 4tXJ7f/fix_sierra_build	blob \| commitdiff \| raw \| diff to current
2016-12-02	Clark Barrett	Merge pull request #113 from 4tXJ7f/remove_extract_rule	blob \| commitdiff \| raw \| diff to current
2016-12-02	ajreynol	Refactor preprocessing of models in fmf. Fix options...	blob \| commitdiff \| raw \| diff to current
2016-12-01	ajreynol	Improvement and bug fix for str.indexof reduction,...	blob \| commitdiff \| raw \| diff to current
2016-11-09	Tim King	Merge branch 'master' into uniq-ptr	blob \| commitdiff \| raw \| diff to current
2016-11-08	ajreynol	Add a few options to separation logic and sets. Minor...	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-29	ajreynol	Minor cleanup and additions to quantifiers statistics.	blob \| commitdiff \| raw \| diff to current
2016-09-15	ajreynol	Refactor setIncomplete in quantifiers.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2016-08-15	ajreynol	Enable bounded set membership with --fmf-bound. Map...	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-06-20	Guy	Merge branch 'master' of https://github.com/CVC4/CVC4	blob \| commitdiff \| raw \| diff to current
2016-06-17	ajreynol	Support for separation logic. Enable cbqi by default...	blob \| commitdiff \| raw \| diff to current
2016-06-01	ajreynol	Initial infrastructure for bounded set quantification...	blob \| commitdiff \| raw \| diff to current
2016-05-06	ajreynol	Minor clean up, fixes related to sygus.	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-13	ajreynol	Minor improvements for alpha equivalence and partial...	blob \| commitdiff \| raw \| diff to current
2016-04-12	ajreynol	Optimizations for QCF to check relevant domain of varia...	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-16	ajreynol	Change internal representative selection for finite...	blob \| commitdiff \| raw \| diff to current
2016-01-15	ajreynol	Type enumerators take optional argument indicating...	blob \| commitdiff \| raw \| diff to current
2016-01-09	Tim King	Removing StatisticsRegistry's static functions current...	blob \| commitdiff \| raw \| diff to current
2015-12-15	Tim King	Refactoring Options Handler & Library Cycle Breaking	blob \| commitdiff \| raw \| diff to current
2015-12-10	ajreynol	Add option fmf-empty-sorts.	blob \| commitdiff \| raw \| diff to current
2015-09-26	ajreynol	Better organization of quantifiers modules, promote...	blob \| commitdiff \| raw \| diff to current
2015-09-16	ajreynol	Add option --fmf-fun-rlv, remove deprecated option...	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-06-27	ajreynol	Refactor various corner cases of fmf, quantifiers modul...	blob \| commitdiff \| raw \| diff to current
2015-05-13	ajreynol	Refactor interface for incompleteness in quantifiers...	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-24	ajreynol	More parser related bug fixes (define-funs-rec, declare...	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-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	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-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	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-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-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-24	ajreynol	Refactor option for uf+cardinality constraints solver.	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-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-01	ajreynol	Minor cleanup from previous commit. Better organizatio...	blob \| commitdiff \| raw \| diff to current
2014-07-21	Kshitij Bansal	initialization in model_engine	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-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	ajreynol	Optimizations for datatypes: check for clashes modulo...	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
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-02-26	Tianyi Liang	Merge branch 'master' of github.com:tiliang/CVC4	blob \| commitdiff \| raw \| diff to current
2014-02-25	Andrew Reynolds	Add options --full-saturate-quant and --mbqi=trust...	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
next

RSS Atom