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
|
/******************************************************************************
* 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 "proof/eager_proof_generator.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "theory/bv/bitblast/node_bitblaster.h"
#include "theory/bv/bv_solver.h"
#include "theory/bv/proof_checker.h"
namespace cvc5 {
namespace theory {
namespace bv {
class NotifyResetAssertions;
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"; };
void computeRelevantTerms(std::set<Node>& termSet) override;
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet) override;
/**
* Get the current value of `node`.
*
* The `initialize` flag indicates whether bits should be zero-initialized
* if they were not bit-blasted yet.
*/
Node getValue(TNode node, bool initialize) override;
private:
/** Initialize SAT solver and CNF stream. */
void initSatSolver();
/**
* Handle BITVECTOR_EAGER_ATOM atoms and assert/assume to CnfStream.
*
* @param assertFact: Indicates whether the fact should be asserted (true) or
* assumed (false).
*/
void handleEagerAtom(TNode fact, bool assertFact);
/** Bit-blaster used to bit-blast atoms/terms. */
std::unique_ptr<NodeBitblaster> d_bitblaster;
/** Used for initializing `d_cnfStream`. */
std::unique_ptr<BBRegistrar> d_bbRegistrar;
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.
*
* Gets 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;
/** 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;
/** Notifies when reset-assertion was called. */
std::unique_ptr<NotifyResetAssertions> d_resetNotify;
};
} // namespace bv
} // namespace theory
} // namespace cvc5
#endif
|
