diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-12-13 09:53:02 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-12-13 09:53:02 -0600 |
| commit | 9acb8b8d0d529c4780191660f8ef2b51e4a92926 (patch) | |
| tree | 1ee538fbc959102d4778cfc74047ee4df87a36c2 /src/theory/sets/solver_state.h | |
| parent | 866f7fb6d4642a51893b0978114b432f990f4c9d (diff) | |
Add support for set comprehension (#3312)
Diffstat (limited to 'src/theory/sets/solver_state.h')
| -rw-r--r-- | src/theory/sets/solver_state.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 2b4d93ed3..7426a701b 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -133,6 +133,8 @@ class SolverState * if none exist. */ Node getVariableSet(Node r) const; + /** Get comprehension sets in equivalence class with representative r */ + const std::vector<Node>& getComprehensionSets(Node r) const; /** Get (positive) members of the set equivalence class r * * The members are return as a map, which maps members to their explanation. @@ -161,6 +163,8 @@ class SolverState * map is a representative of its congruence class. */ const std::map<Kind, std::vector<Node> >& getOperatorList() const; + /** Get the list of all comprehension sets in the current context */ + const std::vector<Node>& getComprehensionSets() const; // --------------------------------------- commonly used terms /** Get type constraint skolem @@ -225,6 +229,8 @@ class SolverState std::map<Node, Node> d_congruent; /** Map from equivalence classes to the list of non-variable sets in it */ std::map<Node, std::vector<Node> > d_nvar_sets; + /** Map from equivalence classes to the list of comprehension sets in it */ + std::map<Node, std::vector<Node> > d_compSets; /** Map from equivalence classes to a variable sets in it */ std::map<Node, Node> d_var_set; /** polarity memberships @@ -262,6 +268,8 @@ class SolverState std::map<Node, Node> d_singleton_index; /** Indices for the binary kinds INTERSECT, SETMINUS and UNION. */ std::map<Kind, std::map<Node, std::map<Node, Node> > > d_bop_index; + /** A list of comprehension sets */ + std::vector<Node> d_allCompSets; // -------------------------------- end term indices std::map<Kind, std::vector<Node> > d_op_list; /** the skolem cache */ |