GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_rewriter.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 1 4 25.0 %

Line Exec Source
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) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level 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 post-order (really reverse-topological 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 top-level 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 (top-down with preRewrite(), then
46
   *     bottom-up 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 pre-order (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 * (big-nasty-expression)
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 */