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

[cvc5.git] / src / theory / sets / theory_sets.cpp

2021-11-01	Andrew Reynolds	Eliminate calls to Rewriter::rewrite and options::...	blob \| commitdiff \| raw
2021-10-22	Andrew Reynolds	Refactor theory inference manager constructor (#7457)	blob \| commitdiff \| raw \| diff to current
2021-09-07	Andres Noetzli	Use `EnvObj` methods instead of `Theory` methods (...	blob \| commitdiff \| raw \| diff to current
2021-09-03	Aina Niemetz	EnvObj: Add options(), context(), userContext(). (...	blob \| commitdiff \| raw \| diff to current
2021-08-17	Gereon Kremer	Push Env class into TheoryState (#7012)	blob \| commitdiff \| raw \| diff to current
2021-08-16	Gereon Kremer	Make Theory class use Env (#7011)	blob \| commitdiff \| raw \| diff to current
2021-07-26	Andrew Reynolds	Enable default equality proofs for sets (#6931)	blob \| commitdiff \| raw \| diff to current
2021-06-22	Andrew Reynolds	Set up fine grained equality notifications (#6734)	blob \| commitdiff \| raw \| diff to current
2021-04-23	Andrew Reynolds	(proof-new) Proofs for sets purification lemmas (#6416)	blob \| commitdiff \| raw \| diff to current
2021-04-22	Andrew Reynolds	Move expand definition from Theory to TheoryRewriter...	blob \| commitdiff \| raw \| diff to current
2021-04-12	Aina Niemetz	Refactor and update copyright headers. (#6316)	blob \| commitdiff \| raw \| diff to current
2021-04-05	Haniel Barbosa	[proof-new] Registering proof checkers uniformly from...	blob \| commitdiff \| raw \| diff to current
2021-04-01	Aina Niemetz	Rename namespace CVC5 to cvc5. (#6258)	blob \| commitdiff \| raw \| diff to current
2021-03-31	Aina Niemetz	Rename namespace CVC4 to CVC5. (#6249)	blob \| commitdiff \| raw \| diff to current
2021-03-11	Andrew Reynolds	(proof-new) Clean up uses of witness with skolem lemmas...	blob \| commitdiff \| raw \| diff to current
2021-03-10	Andrew Reynolds	(proof-new) Update ppRewrite to use skolem lemmas ...	blob \| commitdiff \| raw \| diff to current
2021-03-09	Aina Niemetz	Update copyright headers to 2021. (#6081)	blob \| commitdiff \| raw \| diff to current
2021-03-02	Gereon Kremer	Clean up includes to reduce compile times (#6031)	blob \| commitdiff \| raw \| diff to current
2020-12-15	Andrew Reynolds	Proper expand definitions for sets (#5676)	blob \| commitdiff \| raw \| diff to current
2020-12-07	Andrew Reynolds	Do not expand theory definitions at the beginning of...	blob \| commitdiff \| raw \| diff to current
2020-12-03	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-10-06	Andrew Reynolds	(proof-new) Add interface for trusted substitution...	blob \| commitdiff \| raw \| diff to current
2020-09-22	Mathias Preiner	Update copyright header script to support CMake and...	blob \| commitdiff \| raw \| diff to current
2020-09-19	Andrew Reynolds	Standardize equality engine notifications in sets ...	blob \| commitdiff \| raw \| diff to current
2020-09-15	Andrew Reynolds	Move sets member propagation to SolverState (#5045)	blob \| commitdiff \| raw \| diff to current
2020-09-09	Andrew Reynolds	Split term registry from theory state in sets (#5037)	blob \| commitdiff \| raw \| diff to current
2020-09-03	Andrew Reynolds	Update sets inference manager to inherit from Inference...	blob \| commitdiff \| raw \| diff to current
2020-09-02	Andrew Reynolds	(new theory) Update TheorySets to the new interface...	blob \| commitdiff \| raw \| diff to current
2020-08-31	Andrew Reynolds	Simplify interface for computing relevant terms. (...	blob \| commitdiff \| raw \| diff to current
2020-08-24	Andrew Reynolds	Extend the standard Theory template based on equality...	blob \| commitdiff \| raw \| diff to current
2020-08-21	Andrew Reynolds	Remove spurious theory methods calls (#4931)	blob \| commitdiff \| raw \| diff to current
2020-08-20	Andrew Reynolds	Simplify trigger notifications in equality engine ...	blob \| commitdiff \| raw \| diff to current
2020-08-19	Andrew Reynolds	Make sets and strings solver states inherit from Theory...	blob \| commitdiff \| raw \| diff to current
2020-08-17	Andrew Reynolds	Dynamic allocation of equality engine in Theory (#4890)	blob \| commitdiff \| raw \| diff to current
2020-08-14	Andrew Reynolds	Simplify equality engine notifications (#4896)	blob \| commitdiff \| raw \| diff to current
2020-08-12	Andrew Reynolds	Fix connection to master equality engine in sets (...	blob \| commitdiff \| raw \| diff to current
2020-08-12	Andrew Reynolds	Prepare theory of sets for dynamic allocation of equali...	blob \| commitdiff \| raw \| diff to current
2020-08-09	Andrew Reynolds	Make valuation class more robust to null underlying...	blob \| commitdiff \| raw \| diff to current
2020-07-11	Andrew Reynolds	(proof-new) Update Theory interface for proof-new ...	blob \| commitdiff \| raw \| diff to current
2020-06-16	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2020-05-20	Andrew Reynolds	Do not eliminate variables that are equal to unevaluata...	blob \| commitdiff \| raw \| diff to current
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-04-03	Andres Noetzli	Update theory rewriter ownership, add stats to strings...	blob \| commitdiff \| raw \| diff to current
2020-04-02	Andres Noetzli	Initialize theory rewriters in theories (#4197)	blob \| commitdiff \| raw \| diff to current
2019-12-13	Andrew Reynolds	Add support for set comprehension (#3312)	blob \| commitdiff \| raw \| diff to current
2019-09-13	Andrew Reynolds	Split, refactor and document the theory of sets (#3085)	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-08-22	Tim King	Wrapping TheorySetsPrivate in a unique_ptr. (#2356)	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-12-08	Andrew Reynolds	Make collect model info return a Bool (#1421)	blob \| commitdiff \| raw \| diff to current
2017-09-10	Andrew Reynolds	Ensure that expand definitions is called on all non...	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-04-19	ajreynol	Fixes for handling set universe: restrict upwards rule...	blob \| commitdiff \| raw \| diff to current
2017-04-04	ajreynol	Simplify Theory::collectModelInfo interface to not...	blob \| commitdiff \| raw \| diff to current
2016-10-26	Andrew Reynolds	Merge pull request #98 from 4tXJ7f/fix_dist_build	blob \| commitdiff \| raw \| diff to current
2016-10-26	ajreynol	New implementation of sets+cardinality. Merge Paul...	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	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-09	Kshitij Bansal	cardinality operation for finite sets (based on my...	blob \| commitdiff \| raw \| diff to current
2016-04-04	Tim King	Updating the copyright headers and scripts.	blob \| commitdiff \| raw \| diff to current
2016-01-28	Tim King	Adding listeners to Options.	blob \| commitdiff \| raw \| diff to current
2016-01-06	Tim King	Add SmtGlobals Class	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-17	Morgan Deters	New, uniform checkTime statistic for all theories ...	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-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-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-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-03	Kshitij Bansal	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2014-09-03	Kshitij Bansal	check() optimization	blob \| commitdiff \| raw \| diff to current
2014-08-24	Kshitij Bansal	improvements to sets sharing	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-25	Kshitij Bansal	mv default care graph function inside the theory implem...	blob \| commitdiff \| raw \| diff to current
2014-06-03	ajreynol	Support E-matching/QCF for Set operators.	blob \| commitdiff \| raw \| diff to current
2014-04-06	Tim King	Merge pull request #21 from pcc/ite-fix	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-20	Kshitij Bansal	Fix for registration issues of term appearing in a...	blob \| commitdiff \| raw \| diff to current
next

RSS Atom