1 #include "theory/sets/theory_sets_rewriter.h"
7 bool checkConstantMembership(TNode elementTerm
, TNode setTerm
)
9 switch(setTerm
.getKind()) {
12 case kind::SET_SINGLETON
:
13 return elementTerm
== setTerm
[0];
15 return checkConstantMembership(elementTerm
, setTerm
[0]) ||
16 checkConstantMembership(elementTerm
, setTerm
[1]);
17 case kind::INTERSECTION
:
18 return checkConstantMembership(elementTerm
, setTerm
[0]) &&
19 checkConstantMembership(elementTerm
, setTerm
[1]);
21 return checkConstantMembership(elementTerm
, setTerm
[0]) &&
22 !checkConstantMembership(elementTerm
, setTerm
[1]);
29 RewriteResponse
TheorySetsRewriter::postRewrite(TNode node
) {
30 NodeManager
* nm
= NodeManager::currentNM();
32 switch(node
.getKind()) {
35 if(!node
[0].isConst() || !node
[1].isConst())
39 bool isMember
= checkConstantMembership(node
[0], node
[1]);
40 return RewriteResponse(REWRITE_DONE
, nm
->mkConst(isMember
));
44 // rewrite (A subset-or-equal B) as (A union B = B)
47 return RewriteResponse(REWRITE_AGAIN
,
48 nm
->mkNode(kind::EQUAL
,
49 nm
->mkNode(kind::UNION
, A
, B
),
55 //rewrite: t = t with true (t term)
56 //rewrite: c = c' with c different from c' false (c, c' constants)
57 //otherwise: sort them
58 if(node
[0] == node
[1]) {
59 Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl
;
60 return RewriteResponse(REWRITE_DONE
, nm
->mkConst(true));
62 else if (node
[0].isConst() && node
[1].isConst()) {
63 Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl
;
64 return RewriteResponse(REWRITE_DONE
, nm
->mkConst(false));
66 else if (node
[0] > node
[1]) {
67 Node newNode
= nm
->mkNode(node
.getKind(), node
[1], node
[0]);
68 Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode
<< std::endl
;
69 return RewriteResponse(REWRITE_DONE
, newNode
);
75 case kind::INTERSECTION
: {
76 if(node
[0] == node
[1]) {
77 Trace("sets-postrewrite") << "Sets::postRewrite returning " << node
[0] << std::endl
;
78 return RewriteResponse(REWRITE_DONE
, node
[0]);
79 } else if (node
[0] > node
[1]) {
80 Node newNode
= nm
->mkNode(node
.getKind(), node
[1], node
[0]);
81 Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode
<< std::endl
;
82 return RewriteResponse(REWRITE_DONE
, newNode
);
90 }//switch(node.getKind())
92 // This default implementation
93 return RewriteResponse(REWRITE_DONE
, node
);
97 RewriteResponse
TheorySetsRewriter::preRewrite(TNode node
) {
98 NodeManager
* nm
= NodeManager::currentNM();
101 if(node
.getKind() == kind::EQUAL
&& node
[0] == node
[1])
102 return RewriteResponse(REWRITE_DONE
, nm
->mkConst(true));
103 // Further optimization, if constants but differing ones
105 return RewriteResponse(REWRITE_DONE
, node
);
108 }/* CVC4::theory::sets namespace */
109 }/* CVC4::theory namespace */
110 }/* CVC4 namespace */