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
181
182
183
184
185
186
187
|
/********************* */
/*! \file bitblaster.h
** \verbatim
** Original author: lianah
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Wrapper around the SAT solver used for bitblasting
**
** Wrapper around the SAT solver used for bitblasting.
**/
#include "cvc4_private.h"
#ifndef __CVC4__BITBLASTER_H
#define __CVC4__BITBLASTER_H
#include "expr/node.h"
#include <vector>
#include <list>
#include <iostream>
#include <math.h>
#include <ext/hash_map>
#include "context/cdo.h"
#include "context/cdhashset.h"
#include "context/cdlist.h"
#include "theory/theory.h"
#include "theory_bv_utils.h"
#include "util/statistics_registry.h"
#include "bitblast_strategies.h"
#include "prop/sat_solver.h"
namespace CVC4 {
// forward declarations
namespace prop {
class CnfStream;
class BVSatSolverInterface;
}
namespace theory {
class OutputChannel;
class TheoryModel;
namespace bv {
typedef std::vector<Node> Bits;
std::string toString (Bits& bits);
class TheoryBV;
/**
* The Bitblaster that manages the mapping between Nodes
* and their bitwise definition
*
*/
class Bitblaster {
/** This class gets callbacks from minisat on propagations */
class MinisatNotify : public prop::BVSatSolverInterface::Notify {
prop::CnfStream* d_cnf;
TheoryBV *d_bv;
public:
MinisatNotify(prop::CnfStream* cnf, TheoryBV *bv)
: d_cnf(cnf)
, d_bv(bv)
{}
bool notify(prop::SatLiteral lit);
void notify(prop::SatClause& clause);
void safePoint();
};
typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap;
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet;
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> VarSet;
typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*);
typedef Node (*AtomBBStrategy) (TNode, Bitblaster*);
// sat solver used for bitblasting and associated CnfStream
theory::OutputChannel* d_bvOutput;
prop::BVSatSolverInterface* d_satSolver;
prop::CnfStream* d_cnfStream;
// caches and mappings
TermDefMap d_termCache;
AtomSet d_bitblastedAtoms;
VarSet d_variables;
context::CDList<prop::SatLiteral> d_assertedAtoms; /**< context dependent list storing the atoms
currently asserted by the DPLL SAT solver. */
/// helper methods
public:
bool hasBBAtom(TNode node) const;
private:
bool hasBBTerm(TNode node) const;
void getBBTerm(TNode node, Bits& bits) const;
/// function tables for the various bitblasting strategies indexed by node kind
TermBBStrategy d_termBBStrategies[kind::LAST_KIND];
AtomBBStrategy d_atomBBStrategies[kind::LAST_KIND];
// helper methods to initialize function tables
void initAtomBBStrategies();
void initTermBBStrategies();
// returns a node that might be easier to bitblast
Node bbOptimize(TNode node);
void addAtom(TNode atom);
// division is bitblasted in terms of constraints
// so it needs to use private bitblaster interface
void bbUdiv(TNode node, Bits& bits);
void bbUrem(TNode node, Bits& bits);
public:
void cacheTermDef(TNode node, Bits def); // public so we can cache remainder for division
void bbTerm(TNode node, Bits& bits);
void bbAtom(TNode node);
Bitblaster(context::Context* c, bv::TheoryBV* bv);
~Bitblaster();
bool assertToSat(TNode node, bool propagate = true);
bool propagate();
bool solve(bool quick_solve = false);
void getConflict(std::vector<TNode>& conflict);
void explain(TNode atom, std::vector<TNode>& explanation);
EqualityStatus getEqualityStatus(TNode a, TNode b);
/**
* Return a constant Node representing the value of a variable
* in the current model.
* @param a
*
* @return
*/
Node getVarValue(TNode a);
/**
* Adds a constant value for each bit-blasted variable in the model.
*
* @param m the model
*/
void collectModelInfo(TheoryModel* m);
/**
* Stores the variable (or non-bv term) and its corresponding bits.
*
* @param var
* @param bits
*/
void storeVariable(TNode var) {
d_variables.insert(var);
}
private:
class Statistics {
public:
IntStat d_numTermClauses, d_numAtomClauses;
IntStat d_numTerms, d_numAtoms;
TimerStat d_bitblastTimer;
Statistics();
~Statistics();
};
Statistics d_statistics;
};
} /* bv namespace */
} /* theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__BITBLASTER_H */
|
