diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-11-06 15:28:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-06 15:28:38 -0600 |
| commit | 63df35c477ee9e6c7bdeae677656dd374563de55 (patch) | |
| tree | 1ab725ce9c6f8dafdeda032d572963363f181f7b /src/theory/sets/solver_state.h | |
| parent | 6476c8c75ed7fd584b5afa658dd2c8ba277c59e2 (diff) | |
Fix issue #5342 (#5349)
This PR fixes issue #5342 by adding the rewrite rule (setminus A (setminus A B)) = (intersection A B).
Diffstat (limited to 'src/theory/sets/solver_state.h')
| -rw-r--r-- | src/theory/sets/solver_state.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/sets/solver_state.h b/src/theory/sets/solver_state.h index 32b4d6113..41d3ac717 100644 --- a/src/theory/sets/solver_state.h +++ b/src/theory/sets/solver_state.h @@ -146,6 +146,13 @@ class SolverState : public TheoryState */ const std::map<Kind, std::map<Node, std::map<Node, Node> > >& getBinaryOpIndex() const; + + /** Get binary operator index + * + * This returns the binary operator index of the given kind. + * See getBinaryOpIndex() above. + */ + const std::map<Node, std::map<Node, Node> >& getBinaryOpIndex(Kind k); /** get operator list * * This returns a mapping from set kinds to a list of terms of that kind |