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

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

2020-09-19	Andrew Reynolds	Standardize equality engine notifications in sets ...	blob \| commitdiff \| raw
2020-09-15	Andrew Reynolds	Move sets member propagation to SolverState (#5045)	blob \| commitdiff \| raw \| diff to current
2020-09-14	Andrew Reynolds	Refactoring the rewriter of sets (#4856)	blob \| commitdiff \| raw \| diff to current
2020-09-09	mudathirmahgoub	Add is_singleton operator to the theory of sets (#5033)	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-04	Gereon Kremer	Use arith::InferenceManager for CAD lemmas (#5015)	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-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-14	Andrew Reynolds	Simplify equality engine notifications (#4896)	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-07-14	Andres Noetzli	Use TypeNode in EmptySet (#4740)	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-23	mudathirmahgoub	remove unused field d_emp_exp in TheorySetsPrivate...	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-05-19	mudathirmahgoub	Renamed operator CHOICE to WITNESS (#4207)	blob \| commitdiff \| raw \| diff to current
2020-04-15	Andrew Reynolds	Always flush lemmas from downwards closure in sets...	blob \| commitdiff \| raw \| diff to current
2020-04-08	mudathirmahgoub	Added CHOOSE operator for sets (#4211)	blob \| commitdiff \| raw \| diff to current
2020-04-08	Andres Noetzli	Perform theory widening eagerly (#4044)	blob \| commitdiff \| raw \| diff to current
2020-03-06	Andrew Reynolds	Minor refactor for theory of sets (#3924)	blob \| commitdiff \| raw \| diff to current
2020-03-05	Mathias Preiner	Enable -Wshadow and fix warnings. (#3909)	blob \| commitdiff \| raw \| diff to current
2020-03-03	Andres Noetzli	Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)	blob \| commitdiff \| raw \| diff to current
2020-02-27	Andrew Reynolds	Initial work towards -Wshadow (#3817)	blob \| commitdiff \| raw \| diff to current
2020-02-07	mudathirmahgoub	Univeset Cardinality constraints for infinite types...	blob \| commitdiff \| raw \| diff to current
2020-01-08	mudathirmahgoub	Universe set cardinality for finite types with finite...	blob \| commitdiff \| raw \| diff to current
2019-12-13	Andrew Reynolds	Add support for set comprehension (#3312)	blob \| commitdiff \| raw \| diff to current
2019-10-30	Mathias Preiner	Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...	blob \| commitdiff \| raw \| diff to current
2019-10-23	Andrew Reynolds	Refactoring skolems for sets (#3381)	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-07-08	Andrew Reynolds	Towards refactoring relations (#3078)	blob \| commitdiff \| raw \| diff to current
2019-04-01	Andrew Reynolds	Modify strategy in sets+cardinality (#2909)	blob \| commitdiff \| raw \| diff to current
2019-03-29	Andrew Reynolds	Apply empty splits more aggressively in sets+cardinalit...	blob \| commitdiff \| raw \| diff to current
2019-03-26	Aina Niemetz	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-12-03	Andrew Reynolds	Skip non-cardinality types in sets min card inference...	blob \| commitdiff \| raw \| diff to current
2018-11-27	Andrew Reynolds	Make (T)NodeTrie a general utility (#2489)	blob \| commitdiff \| raw \| diff to current
2018-10-03	Andrew Reynolds	Fix stale op list in sets (#2572)	blob \| commitdiff \| raw \| diff to current
2018-08-24	Andrew Reynolds	Fix more simple coverity warnings (#2372)	blob \| commitdiff \| raw \| diff to current
2018-08-22	Andrew Reynolds	Fix invalid iterator comparisons (#2349)	blob \| commitdiff \| raw \| diff to current
2018-08-16	Andres Noetzli	Move node algorithms to separate file (#2311)	blob \| commitdiff \| raw \| diff to current
2018-07-24	Andrew Reynolds	Improvements to sets + cardinality + quantifiers (...	blob \| commitdiff \| raw \| diff to current
2018-06-25	Aina Niemetz	Updated copyright headers.	blob \| commitdiff \| raw \| diff to current
2018-05-04	Andrew Reynolds	Sets subtypes (#1095)	blob \| commitdiff \| raw \| diff to current
2018-03-07	Mathias Preiner	Make statistics output consistent. (#1647)	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-17	Tim King	Merge branch 'master' into cleanup-regexp	blob \| commitdiff \| raw \| diff to current
2017-07-14	Tim King	Removing BOOST_FOREACH usage.	blob \| commitdiff \| raw \| diff to current
2017-07-07	Mathias Preiner	Update copyright headers.	blob \| commitdiff \| raw \| diff to current
2017-05-17	Clark Barrett	Merge pull request #155 from makaimann/conditional_coverage	blob \| commitdiff \| raw \| diff to current
2017-05-16	Andrew Reynolds	Merge pull request #156 from 4tXJ7f/fix_safe_print	blob \| commitdiff \| raw \| diff to current
2017-05-15	Andrew Reynolds	Merge pull request #159 from 4tXJ7f/fix_set_types	blob \| commitdiff \| raw \| diff to current
2017-05-15	Andrew Reynolds	Merge pull request #157 from 4tXJ7f/fix_iterator	blob \| commitdiff \| raw \| diff to current
2017-05-15	Andres Noetzli	Fix condition in upwards closure check for sets	blob \| commitdiff \| raw \| diff to current
2017-04-21	Clark Barrett	Merge pull request #150 from 4tXJ7f/check_exceptions2	blob \| commitdiff \| raw \| diff to current
2017-04-21	ajreynol	Handle subtypes in sets. Bug fixes for tuples with...	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-14	ajreynol	Actively split for upwards closusure intersection....	blob \| commitdiff \| raw \| diff to current
2017-04-12	ajreynol	Add nullary operator metakind.	blob \| commitdiff \| raw \| diff to current
2017-04-04	ajreynol	Simplify Theory::collectModelInfo interface to not...	blob \| commitdiff \| raw \| diff to current
2017-03-21	ajreynol	Improve computeCareGraph functions to check shared...	blob \| commitdiff \| raw \| diff to current
2017-03-06	ajreynol	Do not eagerly construct explanations in relation solver.	blob \| commitdiff \| raw \| diff to current
2017-03-06	ajreynol	Support for set compliment and universe set. Simplify...	blob \| commitdiff \| raw \| diff to current
2017-03-03	ajreynol	Fix for collectModelInfo related to finite types +...	blob \| commitdiff \| raw \| diff to current
2017-03-03	ajreynol	Another minor fix for sets related to sharing + finite...	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Fixes related to sets.	blob \| commitdiff \| raw \| diff to current
2017-03-02	ajreynol	Eliminate Boolean term conversion. Generalizes removeIT...	blob \| commitdiff \| raw \| diff to current
2017-02-16	ajreynol	Fixes for sets+rels check. Minor.	blob \| commitdiff \| raw \| diff to current
2017-02-07	ajreynol	Generalize finite bound inference to unifiable variable...	blob \| commitdiff \| raw \| diff to current
2017-01-18	Andrew Reynolds	Merge pull request #128 from 4tXJ7f/fix_lfsc_perf	blob \| commitdiff \| raw \| diff to current
2017-01-14	Clark Barrett	Merge pull request #130 from chadbrewbaker/master	blob \| commitdiff \| raw \| diff to current
2017-01-11	Clark Barrett	Merge pull request #129 from timothy-king/regression...	blob \| commitdiff \| raw \| diff to current
2017-01-11	Clark Barrett	Merge pull request #131 from makaimann/fix_702	blob \| commitdiff \| raw \| diff to current
2017-01-11	ajreynol	Fix for when variables are (partially) bound in multipl...	blob \| commitdiff \| raw \| diff to current
2017-01-06	ajreynol	Minor fix for sets.	blob \| commitdiff \| raw \| diff to current
2016-12-07	ajreynol	Added cardinality to cvc language, fixes bug 753. Throw...	blob \| commitdiff \| raw \| diff to current
2016-12-06	ajreynol	Improve bounds for global heap in sep, refactor preproc...	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-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-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-28	Kshitij Bansal	Fix the merge of kbansal/card branch (2039eab).	blob \| commitdiff \| raw \| diff to current
2016-09-14	ajreynol	Lemma cache in theory sep. Minor optimization for sets...	blob \| commitdiff \| raw \| diff to current
2016-08-31	Tim King	Cleaning up the dead FORIT macros.	blob \| commitdiff \| raw \| diff to current
2016-08-31	Tim King	Removing the usage of typeof from theory_sets_private.	blob \| commitdiff \| raw \| diff to current
2016-08-24	PaulMeng	Merge remote-tracking branch 'origin/master'	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-05-04	PaulMeng	implemented TC for standard effort	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	update from the master	blob \| commitdiff \| raw \| diff to current
2016-04-20	PaulMeng	Refactored code	blob \| commitdiff \| raw \| diff to current
2016-04-15	PaulMeng	change transitive closure operator name to TCLOUSRE	blob \| commitdiff \| raw \| diff to current
2016-04-15	PaulMeng	- Implement constant rewriter for relational operators...	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
next

RSS Atom