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