diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-10 19:02:32 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-03-20 17:18:57 -0400 |
| commit | d802bd27402c4e370177bc9e32f36ded4c49c860 (patch) | |
| tree | a91cd86535f8be7289cf5199709876fa55f6c213 /src/theory/sets/expr_patterns.h | |
| parent | c1f794f35cca4be9ad1ca0135806430d06101eb2 (diff) | |
work on set model
Diffstat (limited to 'src/theory/sets/expr_patterns.h')
| -rw-r--r-- | src/theory/sets/expr_patterns.h | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h index 75127f5d8..bc5b6b9e0 100644 --- a/src/theory/sets/expr_patterns.h +++ b/src/theory/sets/expr_patterns.h @@ -22,6 +22,7 @@ namespace CVC4 { namespace expr { namespace pattern { +/** Boolean operators */ static Node AND(TNode a, TNode b) { return NodeManager::currentNM()->mkNode(kind::AND, a, b); } @@ -34,16 +35,21 @@ static Node OR(TNode a, TNode b, TNode c) { return NodeManager::currentNM()->mkNode(kind::OR, a, b, c); } +static Node NOT(TNode a) { + return NodeManager::currentNM()->mkNode(kind::NOT, a); +} + +/** Theory operators */ static Node MEMBER(TNode a, TNode b) { return NodeManager::currentNM()->mkNode(kind::MEMBER, a, b); } -static Node EQUAL(TNode a, TNode b) { - return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); +static Node SET_SINGLETON(TNode a) { + return NodeManager::currentNM()->mkNode(kind::SET_SINGLETON, a); } -static Node NOT(TNode a) { - return NodeManager::currentNM()->mkNode(kind::NOT, a); +static Node EQUAL(TNode a, TNode b) { + return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b); } }/* CVC4::expr::pattern namespace */ |