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

Line Exec Source
1
/*********************                                                        */
2
/*! \file eager_bitblaster.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Liana Hadarean, Tim King
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 eager BV solver.
13
 **
14
 ** Bitblaster for the eager BV solver.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
20
#define CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H
21
22
#include <memory>
23
#include <unordered_set>
24
25
#include "theory/bv/bitblast/bitblaster.h"
26
27
#include "prop/sat_solver.h"
28
29
namespace CVC4 {
30
namespace theory {
31
namespace bv {
32
33
class BitblastingRegistrar;
34
class BVSolverLazy;
35
36
class EagerBitblaster : public TBitblaster<Node>
37
{
38
 public:
39
  EagerBitblaster(BVSolverLazy* theory_bv, context::Context* context);
40
  ~EagerBitblaster();
41
42
  void addAtom(TNode atom);
43
  void makeVariable(TNode node, Bits& bits) override;
44
  void bbTerm(TNode node, Bits& bits) override;
45
  void bbAtom(TNode node) override;
46
  Node getBBAtom(TNode node) const override;
47
  bool hasBBAtom(TNode atom) const override;
48
  void bbFormula(TNode formula);
49
  void storeBBAtom(TNode atom, Node atom_bb) override;
50
  void storeBBTerm(TNode node, const Bits& bits) override;
51
52
  bool assertToSat(TNode node, bool propagate = true);
53
  bool solve();
54
  bool solve(const std::vector<Node>& assumptions);
55
  bool collectModelInfo(TheoryModel* m, bool fullModel);
56
57
 private:
58
  context::Context* d_context;
59
60
  typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
61
  std::unique_ptr<prop::SatSolver> d_satSolver;
62
  std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar;
63
64
  BVSolverLazy* d_bv;
65
  TNodeSet d_bbAtoms;
66
  TNodeSet d_variables;
67
68
  // This is either an MinisatEmptyNotify or NULL.
69
  std::unique_ptr<MinisatEmptyNotify> d_notify;
70
71
  Node getModelFromSatSolver(TNode a, bool fullModel) override;
72
  prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
73
  bool isSharedTerm(TNode node);
74
};
75
76
62
class BitblastingRegistrar : public prop::Registrar
77
{
78
 public:
79
31
  BitblastingRegistrar(EagerBitblaster* bb) : d_bitblaster(bb) {}
80
2598
  void preRegister(Node n) override { d_bitblaster->bbAtom(n); }
81
82
 private:
83
  EagerBitblaster* d_bitblaster;
84
};
85
86
}  // namespace bv
87
}  // namespace theory
88
}  // namespace CVC4
89
#endif  //  CVC4__THEORY__BV__BITBLAST__EAGER_BITBLASTER_H