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

Line Exec Source
1
/*********************                                                        */
2
/*! \file bv_solver_bitblast.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Mathias Preiner, Andrew Reynolds
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 Bit-blasting solver
13
 **
14
 ** Bit-blasting solver that supports multiple SAT back ends.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
20
#define CVC4__THEORY__BV__BV_SOLVER_BITBLAST_H
21
22
#include <unordered_map>
23
24
#include "context/cdqueue.h"
25
#include "prop/cnf_stream.h"
26
#include "prop/sat_solver.h"
27
#include "theory/bv/bitblast/simple_bitblaster.h"
28
#include "theory/bv/bv_solver.h"
29
#include "theory/bv/proof_checker.h"
30
#include "theory/eager_proof_generator.h"
31
32
namespace CVC4 {
33
34
namespace theory {
35
namespace bv {
36
37
/**
38
 * Bit-blasting solver with support for different SAT back ends.
39
 */
40
class BVSolverBitblast : public BVSolver
41
{
42
 public:
43
  BVSolverBitblast(TheoryState* state,
44
                   TheoryInferenceManager& inferMgr,
45
                   ProofNodeManager* pnm);
46
  ~BVSolverBitblast() = default;
47
48
  bool needsEqualityEngine(EeSetupInfo& esi) override { return true; }
49
50
  void preRegisterTerm(TNode n) override {}
51
52
  void postCheck(Theory::Effort level) override;
53
54
  bool preNotifyFact(TNode atom,
55
                     bool pol,
56
                     TNode fact,
57
                     bool isPrereg,
58
                     bool isInternal) override;
59
60
  TrustNode explain(TNode n) override;
61
62
  std::string identify() const override { return "BVSolverBitblast"; };
63
64
  Theory::PPAssertStatus ppAssert(
65
      TrustNode in, TrustSubstitutionMap& outSubstitutions) override
66
  {
67
    return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
68
  }
69
70
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
71
72
  bool collectModelValues(TheoryModel* m,
73
                          const std::set<Node>& termSet) override;
74
75
 private:
76
  /**
77
   * Get value of `node` from SAT solver.
78
   *
79
   * The `initialize` flag indicates whether bits should be zero-initialized
80
   * if they were not bit-blasted yet.
81
   */
82
  Node getValueFromSatSolver(TNode node, bool initialize);
83
84
  /**
85
   * Get the current value of `node`.
86
   *
87
   * Computes the value if `node` was not yet bit-blasted.
88
   */
89
  Node getValue(TNode node);
90
91
  /**
92
   * Cache for getValue() calls.
93
   *
94
   * Is cleared at the beginning of a getValue() call if the
95
   * `d_invalidateModelCache` flag is set to true.
96
   */
97
  std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
98
99
  /** Bit-blaster used to bit-blast atoms/terms. */
100
  std::unique_ptr<BBSimple> d_bitblaster;
101
102
  /** Used for initializing `d_cnfStream`. */
103
  std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
104
  std::unique_ptr<context::Context> d_nullContext;
105
106
  /** SAT solver back end (configured via options::bvSatSolver. */
107
  std::unique_ptr<prop::SatSolver> d_satSolver;
108
  /** CNF stream. */
109
  std::unique_ptr<prop::CnfStream> d_cnfStream;
110
111
  /**
112
   * Bit-blast queue for facts sent to this solver.
113
   *
114
   * Get populated on preNotifyFact().
115
   */
116
  context::CDQueue<Node> d_bbFacts;
117
118
  /** Corresponds to the SAT literals of the currently asserted facts. */
119
  context::CDList<prop::SatLiteral> d_assumptions;
120
121
  /** Flag indicating whether `d_modelCache` should be invalidated. */
122
  context::CDO<bool> d_invalidateModelCache;
123
124
  /** Indicates whether the last check() call was satisfiable. */
125
  context::CDO<bool> d_inSatMode;
126
127
  /** Proof generator that manages proofs for lemmas generated by this class. */
128
  std::unique_ptr<EagerProofGenerator> d_epg;
129
130
  BVProofRuleChecker d_bvProofChecker;
131
132
  /** Stores the SatLiteral for a given fact. */
133
  context::CDHashMap<Node, prop::SatLiteral, NodeHashFunction>
134
      d_factLiteralCache;
135
136
  /** Reverse map of `d_factLiteralCache`. */
137
  context::CDHashMap<prop::SatLiteral, Node, prop::SatLiteralHashFunction>
138
      d_literalFactCache;
139
140
  /** Option to enable/disable bit-level propagation. */
141
  bool d_propagate;
142
};
143
144
}  // namespace bv
145
}  // namespace theory
146
}  // namespace CVC4
147
148
#endif