Age | Commit message (Collapse) | Author |
|
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.'.
|
|
This PR is a follow-up to #7011, making the Env object available in the TheoryState base class.
|
|
Eliminates NodeHashFunction, TNodeHashFunction and TypeNodeHashFunction.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).
|
|
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.
|
|
This eliminates the parent relationship from solver state to theory sets.
|
|
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.
|
|
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.
|
|
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).
|
|
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.
|
|
|
|
|
|
* rewrote set cardinality for finite-types
* small changes and format
|
|
|
|
|