GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/passes/bool_to_bv.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file bool_to_bv.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Makai Mann, Yoni Zohar, Mathias Preiner
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 The BoolToBV preprocessing pass
13
 **
14
 **/
15
16
#include "cvc4_private.h"
17
18
#ifndef CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
19
#define CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H
20
21
#include "expr/node.h"
22
#include "options/bv_options.h"
23
#include "preprocessing/preprocessing_pass.h"
24
#include "util/statistics_registry.h"
25
26
namespace CVC4 {
27
namespace preprocessing {
28
namespace passes {
29
30
17988
class BoolToBV : public PreprocessingPass
31
{
32
 public:
33
  BoolToBV(PreprocessingPassContext* preprocContext);
34
35
 protected:
36
  PreprocessingPassResult applyInternal(
37
      AssertionPipeline* assertionsToPreprocess) override;
38
39
 private:
40
  struct Statistics
41
  {
42
    IntStat d_numIteToBvite;
43
    IntStat d_numTermsLowered;
44
    IntStat d_numIntroducedItes;
45
    Statistics();
46
    ~Statistics();
47
  };
48
49
  /** Takes an assertion and attempts to create more bit-vector structure
50
      by replacing boolean operators with bit-vector operators.
51
52
      It passes the allowIteIntroduction argument down to lowerNode, however it
53
      never allows ite introduction in the top-level assertion. There's no point
54
      forcing the assertion to be a bit-vector when it will just be converted
55
      back into a boolean.
56
  */
57
  Node lowerAssertion(const TNode& node, bool allowIteIntroduction = false);
58
59
  /** Traverses subterms to turn booleans into bit-vectors using visit
60
   *  Passes the allowIteIntroduction argument to visit
61
   *  Returns the lowered node
62
   */
63
  Node lowerNode(const TNode& node, bool allowIteIntroduction = false);
64
65
  /** Tries to lower one node to a width-one bit-vector
66
   *  Caches the result if successful
67
   *
68
   *  allowIteIntroduction = true causes booleans to be converted to bit-vectors
69
   *     using an ITE this is only used by mode ALL currently, but could
70
   *     conceivably be used in new modes.
71
   */
72
  void visit(const TNode& n, bool allowIteIntroduction = false);
73
74
  /* Traverses formula looking for ITEs to lower to BITVECTOR_ITE using
75
   * lowerNode*/
76
  Node lowerIte(const TNode& node);
77
78
  /** Rebuilds node using the provided kind
79
   *  Note: The provided kind is not necessarily different from the
80
   *        existing one, but still might need to be rebuilt because
81
   *        of subterms
82
   */
83
  void rebuildNode(const TNode& n, Kind new_kind);
84
85
  /** Updates the cache, the cache is actually supported by two maps
86
      one for ITEs and one for everything else
87
88
      This is necessary so that when in ITE mode, the regular cache
89
      can be cleared to prevent lowering boolean operators that are
90
      not in an ITE
91
   */
92
  void updateCache(TNode n, TNode rebuilt);
93
94
  /* Returns cached node if it exists, otherwise returns the node */
95
  Node fromCache(TNode n) const;
96
97
  /* Checks both caches for membership */
98
  bool inCache(const Node& n) const;
99
100
  /** Checks if any of the node's children were rebuilt,
101
   *  in which case n needs to be rebuilt as well
102
   */
103
  bool needToRebuild(TNode n) const;
104
105
  Statistics d_statistics;
106
107
  /** Keeps track of lowered ITEs
108
      Note: it only keeps mappings for ITEs of type bit-vector.
109
      Other ITEs will be in the d_lowerCache
110
   */
111
  std::unordered_map<Node, Node, NodeHashFunction> d_iteBVLowerCache;
112
113
  /** Keeps track of other lowered nodes
114
      -- will be cleared periodically in ITE mode
115
  */
116
  std::unordered_map<Node, Node, NodeHashFunction> d_lowerCache;
117
118
  /** Stores the bool-to-bv mode option */
119
  options::BoolToBVMode d_boolToBVMode;
120
};  // class BoolToBV
121
122
}  // namespace passes
123
}  // namespace preprocessing
124
}  // namespace CVC4
125
126
#endif /* CVC4__PREPROCESSING__PASSES__BOOL_TO_BV_H */