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

Line Exec Source
1
/*********************                                                        */
2
/*! \file simple_bitblaster.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   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 Bitblaster for simple BV solver.
13
 **
14
 **/
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
18
#define CVC4__THEORY__BV__BITBLAST_SIMPLE_BITBLASTER_H
19
20
#include "theory/bv/bitblast/bitblaster.h"
21
22
namespace CVC4 {
23
namespace theory {
24
namespace bv {
25
26
/**
27
 * Implementation of a simple Node-based bit-blaster.
28
 *
29
 * Implements the bare minimum to bit-blast bit-vector atoms/terms.
30
 */
31
class BBSimple : public TBitblaster<Node>
32
{
33
  using Bits = std::vector<Node>;
34
35
 public:
36
  BBSimple(TheoryState* state);
37
20
  ~BBSimple() = default;
38
39
  /** Bit-blast term 'node' and return bit-blasted 'bits'. */
40
  void bbTerm(TNode node, Bits& bits) override;
41
  /** Bit-blast atom 'node'. */
42
  void bbAtom(TNode node) override;
43
  /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */
44
  Node getBBAtom(TNode atom) const override;
45
  /** Store Boolean node representing the bit-blasted atom. */
46
  void storeBBAtom(TNode atom, Node atom_bb) override;
47
  /** Store bits of bit-blasted term. */
48
  void storeBBTerm(TNode node, const Bits& bits) override;
49
  /** Check if atom was already bit-blasted. */
50
  bool hasBBAtom(TNode atom) const override;
51
  /** Get bit-blasted node stored for atom. */
52
  Node getStoredBBAtom(TNode node);
53
  /** Create 'bits' for variable 'var'. */
54
  void makeVariable(TNode var, Bits& bits) override;
55
56
  /** Collect model values for all relevant terms given in 'relevantTerms'. */
57
  bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
58
59
  prop::SatSolver* getSatSolver() override { Unreachable(); }
60
61
  /** Checks whether node is a variable introduced via `makeVariable`.*/
62
  bool isVariable(TNode node);
63
64
 private:
65
  /** Query SAT solver for assignment of node 'a'. */
66
  Node getModelFromSatSolver(TNode a, bool fullModel) override;
67
68
  /** Caches variables for which we already created bits. */
69
  TNodeSet d_variables;
70
  /** Stores bit-blasted atoms. */
71
  std::unordered_map<Node, Node, NodeHashFunction> d_bbAtoms;
72
  /** Theory state. */
73
  TheoryState* d_state;
74
};
75
76
}  // namespace bv
77
}  // namespace theory
78
}  // namespace CVC4
79
80
#endif