summaryrefslogtreecommitdiff
path: root/src/theory/sets/solver_state.h
AgeCommit message (Collapse)Author
2021-11-08sets: Rename kinds with a more consistent naming scheme. (#7595)Aina Niemetz
This prefixes sets kinds with SET_ and relation kinds with RELATION_. It also prefixes the corresponding SMT-LIB operators with 'set.' and relation operators with 'rel.'.
2021-08-16Push Env class into TheoryState (#7012)Gereon Kremer
This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
2021-04-14Rename public and private headers in src/include. (#6352)Aina Niemetz
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-09Rename CVC4__ header guards to CVC5__. (#6326)Aina Niemetz
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2020-11-06Fix issue #5342 (#5349)mudathirmahgoub
This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
This PR updates the update-copyright.pl script to also update/add copyright headers to CMake specific files. It further fixes a small typo in the header.
2020-09-15Move sets member propagation to SolverState (#5045)Andrew Reynolds
This eliminates the parent relationship from solver state to theory sets.
2020-09-08Split term registry from theory state in sets (#5037)Andrew Reynolds
Currently, the theory state object SolverState in sets sends lemmas and has a reference to the parent theory. This PR is work towards eliminating these dependencies. This adds a TermRegistry object which is responsible for some of the tasks currently done by SolverState, including all those involving lemmas. Notice this also makes a bug fix in getUnivSetEqClass where the universe set was being returned instead of its representative. A followup PR will make SolverState maintain SAT-context-dependent membership lists which is also required for breaking the dependence on the parent theory.
2020-09-03Update sets inference manager to inherit from InferenceManagerBuffered (#5007)Andrew Reynolds
This updates the inference manager of sets to inherit from the standard base class InferenceManagerBuffered. It matches that base class almost exactly, with cosmetic changes. Notice that sets currently has a design issue: the state object sends lemmas and hence currently requires a pointer to the theory. This will be untangled in a future PR. This PR makes a few very minor changes to the behavior, including not to use the "preprocess" property for subtype lemmas.
2020-08-19Make sets and strings solver states inherit from TheoryState (#4918)Andrew Reynolds
This is towards the new standard for theory solvers. This PR makes the custom states of sets and strings inherit from the standard base class TheoryState. It also makes a minor change to InferenceManager/SolverState to make sets more in line with the plan for a standard base class InferenceManager. Followup PRs will establish the official TheoryState classes for all other theories (which in most cases will be an instance of the base class).
2020-08-11Prepare theory of sets for dynamic allocation of equality engine (#4868)Andrew Reynolds
In forthcoming PRs, Theory objects will be assigned equality engine objects dynamically. This PR prepares the theory of sets for this update, which involves refactoring of its internal members.
2020-06-16Update copyright headers.Aina Niemetz
2020-02-07Univeset Cardinality constraints for infinite types (#3712)mudathirmahgoub
2020-01-07Universe set cardinality for finite types with finite cardinality (#3392)mudathirmahgoub
* rewrote set cardinality for finite-types * small changes and format
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-09-13Split, refactor and document the theory of sets (#3085)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback