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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
|
/******************************************************************************
* Top contributors (to current version):
* Mathias Preiner, Liana Hadarean, Clark Barrett
*
* 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.
* ****************************************************************************
*
* Bitblaster for the lazy bv solver.
*/
#include "cvc5_private.h"
#ifndef CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
#define CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
#include "theory/bv/bitblast/bitblaster.h"
#include "context/cdhashmap.h"
#include "context/cdlist.h"
#include "prop/bv_sat_solver_notify.h"
#include "theory/bv/abstraction.h"
namespace cvc5 {
namespace prop {
class CnfStream;
class NullRegistrat;
}
namespace theory {
namespace bv {
class BVSolverLayered;
class TLazyBitblaster : public TBitblaster<Node>
{
public:
void bbTerm(TNode node, Bits& bits) override;
void bbAtom(TNode node) override;
Node getBBAtom(TNode atom) const override;
void storeBBAtom(TNode atom, Node atom_bb) override;
void storeBBTerm(TNode node, const Bits& bits) override;
bool hasBBAtom(TNode atom) const override;
TLazyBitblaster(context::Context* c,
BVSolverLayered* bv,
const std::string name = "",
bool emptyNotify = false);
~TLazyBitblaster();
/**
* Pushes the assumption literal associated with node to the SAT
* solver assumption queue.
*
* @param node assumption
* @param propagate run bcp or not
*
* @return false if a conflict detected
*/
bool assertToSat(TNode node, bool propagate = true);
bool propagate();
bool solve();
prop::SatValue solveWithBudget(unsigned long conflict_budget);
void getConflict(std::vector<TNode>& conflict);
void explain(TNode atom, std::vector<TNode>& explanation);
void setAbstraction(AbstractionModule* abs);
theory::EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
* Adds a constant value for each bit-blasted variable in the model.
*
* @param m the model
* @param termSet the set of relevant terms
*/
bool collectModelValues(TheoryModel* m,
const std::set<Node>& termSet);
typedef TNodeSet::const_iterator vars_iterator;
vars_iterator beginVars() { return d_variables.begin(); }
vars_iterator endVars() { return d_variables.end(); }
/**
* Creates the bits corresponding to the variable (or non-bv term).
*
* @param var
*/
void makeVariable(TNode var, Bits& bits) override;
bool isSharedTerm(TNode node);
uint64_t computeAtomWeight(TNode node, NodeSet& seen);
/**
* Deletes SatSolver and CnfCache, but maintains bit-blasting
* terms cache.
*
*/
void clearSolver();
private:
typedef std::vector<Node> Bits;
typedef context::CDList<prop::SatLiteral> AssertionList;
typedef context::CDHashMap<prop::SatLiteral,
std::vector<prop::SatLiteral>,
prop::SatLiteralHashFunction>
ExplanationMap;
/** This class gets callbacks from minisat on propagations */
class MinisatNotify : public prop::BVSatSolverNotify
{
prop::CnfStream* d_cnf;
BVSolverLayered* d_bv;
TLazyBitblaster* d_lazyBB;
public:
MinisatNotify(prop::CnfStream* cnf,
BVSolverLayered* bv,
TLazyBitblaster* lbv)
: d_cnf(cnf), d_bv(bv), d_lazyBB(lbv)
{
}
bool notify(prop::SatLiteral lit) override;
void notify(prop::SatClause& clause) override;
void spendResource(Resource r) override;
void safePoint(Resource r) override;
};
BVSolverLayered* d_bv;
context::Context* d_ctx;
std::unique_ptr<prop::NullRegistrar> d_nullRegistrar;
std::unique_ptr<prop::BVSatSolverInterface> d_satSolver;
std::unique_ptr<prop::BVSatSolverNotify> d_satSolverNotify;
AssertionList*
d_assertedAtoms; /**< context dependent list storing the atoms
currently asserted by the DPLL SAT solver. */
ExplanationMap* d_explanations; /**< context dependent list of explanations
for the propagated literals. Only used when
bvEagerPropagate option enabled. */
TNodeSet d_variables;
TNodeSet d_bbAtoms;
AbstractionModule* d_abstraction;
bool d_emptyNotify;
// The size of the fact queue when we most recently called solve() in the
// bit-vector SAT solver. This is the level at which we should have
// a full model in the bv SAT solver.
context::CDO<int> d_fullModelAssertionLevel;
void addAtom(TNode atom);
bool hasValue(TNode a);
Node getModelFromSatSolver(TNode a, bool fullModel) override;
prop::SatSolver* getSatSolver() override { return d_satSolver.get(); }
class Statistics
{
public:
IntStat d_numTermClauses, d_numAtomClauses;
IntStat d_numTerms, d_numAtoms;
IntStat d_numExplainedPropagations;
IntStat d_numBitblastingPropagations;
TimerStat d_bitblastTimer;
Statistics(const std::string& name);
};
std::string d_name;
// NOTE: d_statistics is public since d_bitblastTimer needs to be initalized
// prior to calling bbAtom. As it is now, the timer can't be initialized
// in bbAtom since the method is called recursively and the timer would
// be initialized multiple times, which is not allowed.
public:
Statistics d_statistics;
};
} // namespace bv
} // namespace theory
} // namespace cvc5
#endif // CVC5__THEORY__BV__BITBLAST__LAZY_BITBLASTER_H
|
