GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/bv/theory_bv_rewriter.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 2 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_bv_rewriter.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Andres Noetzli, Morgan Deters
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__BV__THEORY_BV_REWRITER_H
21
#define CVC4__THEORY__BV__THEORY_BV_REWRITER_H
22
23
#include "theory/theory_rewriter.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace bv {
28
29
typedef RewriteResponse (*RewriteFunction) (TNode, bool);
30
31
8994
class TheoryBVRewriter : public TheoryRewriter
32
{
33
 public:
34
  /**
35
   * Temporary hack for devision-by-zero until we refactor theory code from
36
   * smt engine.
37
   *
38
   * @param node
39
   *
40
   * @return
41
   */
42
  static Node eliminateBVSDiv(TNode node);
43
44
  TheoryBVRewriter();
45
46
  RewriteResponse postRewrite(TNode node) override;
47
  RewriteResponse preRewrite(TNode node) override;
48
49
 private:
50
  static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false);
51
  static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false);
52
53
  static RewriteResponse RewriteBitOf(TNode node, bool prerewrite = false);
54
  static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false);
55
  static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false);
56
  static RewriteResponse RewriteUltBv(TNode node, bool prerewrite = false);
57
  static RewriteResponse RewriteSlt(TNode node, bool prerewrite = false);
58
  static RewriteResponse RewriteSltBv(TNode node, bool prerewrite = false);
59
  static RewriteResponse RewriteUle(TNode node, bool prerewrite = false);
60
  static RewriteResponse RewriteSle(TNode node, bool prerewrite = false);
61
  static RewriteResponse RewriteUgt(TNode node, bool prerewrite = false);
62
  static RewriteResponse RewriteSgt(TNode node, bool prerewrite = false);
63
  static RewriteResponse RewriteUge(TNode node, bool prerewrite = false);
64
  static RewriteResponse RewriteSge(TNode node, bool prerewrite = false);
65
  static RewriteResponse RewriteITEBv(TNode node, bool prerewrite = false);
66
  static RewriteResponse RewriteNot(TNode node, bool prerewrite = false);
67
  static RewriteResponse RewriteConcat(TNode node, bool prerewrite = false);
68
  static RewriteResponse RewriteAnd(TNode node, bool prerewrite = false);
69
  static RewriteResponse RewriteOr(TNode node, bool prerewrite = false);
70
  static RewriteResponse RewriteXnor(TNode node, bool prerewrite = false);
71
  static RewriteResponse RewriteXor(TNode node, bool prerewrite = false);
72
  static RewriteResponse RewriteNand(TNode node, bool prerewrite = false);
73
  static RewriteResponse RewriteNor(TNode node, bool prerewrite = false);
74
  static RewriteResponse RewriteComp(TNode node, bool prerewrite = false);
75
  static RewriteResponse RewriteMult(TNode node, bool prerewrite = false);
76
  static RewriteResponse RewritePlus(TNode node, bool prerewrite = false);
77
  static RewriteResponse RewriteSub(TNode node, bool prerewrite = false);
78
  static RewriteResponse RewriteNeg(TNode node, bool prerewrite = false);
79
  static RewriteResponse RewriteUdiv(TNode node, bool prerewrite = false);
80
  static RewriteResponse RewriteUrem(TNode node, bool prerewrite = false);
81
  static RewriteResponse RewriteUdivTotal(TNode node, bool prerewrite = false);
82
  static RewriteResponse RewriteUremTotal(TNode node, bool prerewrite = false);
83
  static RewriteResponse RewriteSmod(TNode node, bool prerewrite = false);
84
  static RewriteResponse RewriteSdiv(TNode node, bool prerewrite = false);
85
  static RewriteResponse RewriteSrem(TNode node, bool prerewrite = false);
86
  static RewriteResponse RewriteShl(TNode node, bool prerewrite = false);
87
  static RewriteResponse RewriteLshr(TNode node, bool prerewrite = false);
88
  static RewriteResponse RewriteAshr(TNode node, bool prerewrite = false);
89
  static RewriteResponse RewriteExtract(TNode node, bool prerewrite = false);
90
  static RewriteResponse RewriteRepeat(TNode node, bool prerewrite = false);
91
  static RewriteResponse RewriteZeroExtend(TNode node, bool prerewrite = false);
92
  static RewriteResponse RewriteSignExtend(TNode node, bool prerewrite = false);
93
  static RewriteResponse RewriteRotateRight(TNode node, bool prerewrite = false);
94
  static RewriteResponse RewriteRotateLeft(TNode node, bool prerewrite = false);
95
  static RewriteResponse RewriteRedor(TNode node, bool prerewrite = false);
96
  static RewriteResponse RewriteRedand(TNode node, bool prerewrite = false);
97
98
  static RewriteResponse RewriteBVToNat(TNode node, bool prerewrite = false);
99
  static RewriteResponse RewriteIntToBV(TNode node, bool prerewrite = false);
100
101
  void initializeRewrites();
102
103
  RewriteFunction d_rewriteTable[kind::LAST_KIND];
104
}; /* class TheoryBVRewriter */
105
106
}/* CVC4::theory::bv namespace */
107
}/* CVC4::theory namespace */
108
}/* CVC4 namespace */
109
110
#endif /* CVC4__THEORY__BV__THEORY_BV_REWRITER_H */