1 

/********************* */ 
2 

/*! \file theory_sets_rewriter.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Kshitij Bansal, Andrew Reynolds, Andres Noetzli 
6 

** This file is part of the CVC4 project. 
7 

** Copyright (c) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel source 
10 

** directory for licensing information.\endverbatim 
11 

** 
12 

** \brief Sets theory rewriter. 
13 

** 
14 

** Sets theory rewriter. 
15 

**/ 
16 


17 

#include "cvc4_private.h" 
18 


19 

#ifndef CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H 
20 

#define CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H 
21 


22 

#include "theory/rewriter.h" 
23 


24 

namespace CVC4 { 
25 

namespace theory { 
26 

namespace sets { 
27 


28 
69055 
class TheorySetsRewriter : public TheoryRewriter 
29 

{ 
30 

public: 
31 

/** 
32 

* Rewrite a node into the normal form for the theory of sets. 
33 

* Called in postorder (really reversetopological order) when 
34 

* traversing the expression DAG during rewriting. This is the 
35 

* main function of the rewriter, and because of the ordering, 
36 

* it can assume its children are all rewritten already. 
37 

* 
38 

* This function can return one of three rewrite response codes 
39 

* along with the rewritten node: 
40 

* 
41 

* REWRITE_DONE indicates that no more rewriting is needed. 
42 

* REWRITE_AGAIN means that the toplevel expression should be 
43 

* rewritten again, but that its children are in final form. 
44 

* REWRITE_AGAIN_FULL means that the entire returned expression 
45 

* should be rewritten again (topdown with preRewrite(), then 
46 

* bottomup with postRewrite()). 
47 

* 
48 

* Even if this function returns REWRITE_DONE, if the returned 
49 

* expression belongs to a different theory, it will be fully 
50 

* rewritten by that theory's rewriter. 
51 

*/ 
52 

RewriteResponse postRewrite(TNode node) override; 
53 


54 

/** 
55 

* Rewrite a node into the normal form for the theory of sets 
56 

* in preorder (really topological order)meaning that the 
57 

* children may not be in the normal form. This is an optimization 
58 

* for theories with cancelling terms (e.g., 0 * (bignastyexpression) 
59 

* in arithmetic rewrites to 0 without the need to look at the big 
60 

* nasty expression). Since it's only an optimization, the 
61 

* implementation here can do nothing. 
62 

*/ 
63 

RewriteResponse preRewrite(TNode node) override; 
64 


65 

/** 
66 

* Rewrite an equality, in case special handling is required. 
67 

*/ 
68 

Node rewriteEquality(TNode equality) 
69 

{ 
70 

// often this will suffice 
71 

return postRewrite(equality).d_node; 
72 

} 
73 

private: 
74 

/** 
75 

* Returns true if elementTerm is in setTerm, where both terms are constants. 
76 

*/ 
77 

bool checkConstantMembership(TNode elementTerm, TNode setTerm); 
78 

}; /* class TheorySetsRewriter */ 
79 


80 

}/* CVC4::theory::sets namespace */ 
81 

}/* CVC4::theory namespace */ 
82 

}/* CVC4 namespace */ 
83 


84 

#endif /* CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */ 