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
|
/********************* */
/*! \file bv_sat.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__BV__SAT_H
#define __CVC4__BV__SAT_H
#include "expr/node.h"
#include <vector>
#include <list>
#include <iostream>
#include <math.h>
#include <ext/hash_map>
#include "context/cdo.h"
#include "context/cdset.h"
#include "context/cdlist.h"
#include "theory_bv_utils.h"
#include "util/stats.h"
#include "bitblast_strategies.h"
#include "prop/sat_module.h"
namespace CVC4 {
// forward declarations
namespace prop {
class CnfStream;
class BVSatSolverInterface;
}
namespace theory {
namespace bv {
std::string toString (Bits& bits);
/**
* The Bitblaster that manages the mapping between Nodes
* and their bitwise definition
*
*/
typedef std::vector<Node> Bits;
class Bitblaster {
typedef __gnu_cxx::hash_map <Node, Bits, TNodeHashFunction > TermDefMap;
typedef __gnu_cxx::hash_set<TNode, TNodeHashFunction> AtomSet;
typedef void (*TermBBStrategy) (TNode, Bits&, Bitblaster*);
typedef Node (*AtomBBStrategy) (TNode, Bitblaster*);
// sat solver used for bitblasting and associated CnfStream
prop::BVSatSolverInterface* d_satSolver;
prop::CnfStream* d_cnfStream;
// caches and mappings
TermDefMap d_termCache;
AtomSet d_bitblastedAtoms;
context::CDList<prop::SatLiteral> d_assertedAtoms; /**< context dependent list storing the atoms
currently asserted by the DPLL SAT solver. */
/// helper methods
bool hasBBAtom(TNode node);
bool hasBBTerm(TNode node);
void getBBTerm(TNode node, Bits& bits);
/// 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();
void bbAtom(TNode node);
// 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);
public:
Bitblaster(context::Context* c);
~Bitblaster() {
delete d_cnfStream;
delete d_satSolver;
}
void assertToSat(TNode node);
bool solve();
void bitblast(TNode node);
void getConflict(std::vector<TNode>& conflict);
private:
class Statistics {
public:
IntStat d_numTermClauses, d_numAtomClauses;
TimerStat d_bitblastTimer;
Statistics();
~Statistics();
};
Statistics d_statistics;
};
} /* bv namespace */
} /* theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__BV__SAT_H */
|