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
|
/********************* */
/*! \file theory_bv.h
** \verbatim
** Original author: mdeters
** Major contributors: dejan, lianah
** Minor contributors (to current version): barrett, ajreynol
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Bitvector theory.
**
** Bitvector theory.
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__BV__THEORY_BV_H
#define __CVC4__THEORY__BV__THEORY_BV_H
#include "theory/theory.h"
#include "context/context.h"
#include "context/cdlist.h"
#include "context/cdhashset.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
#include "context/cdqueue.h"
#include "theory/bv/bv_subtheory.h"
#include "theory/bv/bv_subtheory_eq.h"
#include "theory/bv/bv_subtheory_bitblast.h"
namespace CVC4 {
namespace theory {
namespace bv {
class TheoryBV : public Theory {
/** The context we are using */
context::Context* d_context;
/** Context dependent set of atoms we already propagated */
context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
context::CDHashSet<TNode, TNodeHashFunction> d_sharedTermsSet;
BitblastSolver d_bitblastSolver;
EqualitySolver d_equalitySolver;
public:
TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe);
~TheoryBV();
void preRegisterTerm(TNode n);
void check(Effort e);
void propagate(Effort e);
Node explain(TNode n);
void collectModelInfo( TheoryModel* m, bool fullModel );
std::string identify() const { return std::string("TheoryBV"); }
PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
Node ppRewrite(TNode t);
private:
class Statistics {
public:
AverageStat d_avgConflictSize;
IntStat d_solveSubstitutions;
TimerStat d_solveTimer;
Statistics();
~Statistics();
};
Statistics d_statistics;
// Are we in conflict?
context::CDO<bool> d_conflict;
/** The conflict node */
Node d_conflictNode;
/** Literals to propagate */
context::CDList<Node> d_literalsToPropagate;
/** Index of the next literal to propagate */
context::CDO<unsigned> d_literalsToPropagateIndex;
/**
* Keeps a map from nodes to the subtheory that propagated it so that we can explain it
* properly.
*/
typedef context::CDHashMap<Node, SubTheory, NodeHashFunction> PropagatedMap;
PropagatedMap d_propagatedBy;
bool propagatedBy(TNode literal, SubTheory subtheory) const {
PropagatedMap::const_iterator find = d_propagatedBy.find(literal);
if (find == d_propagatedBy.end()) return false;
else return (*find).second == subtheory;
}
/** Should be called to propagate the literal. */
bool storePropagation(TNode literal, SubTheory subtheory);
/**
* Explains why this literal (propagated by subtheory) is true by adding assumptions.
*/
void explain(TNode literal, std::vector<TNode>& assumptions);
void addSharedTerm(TNode t);
EqualityStatus getEqualityStatus(TNode a, TNode b);
inline std::string indent()
{
std::string indentStr(getSatContext()->getLevel(), ' ');
return indentStr;
}
void setConflict(Node conflict = Node::null()) {
d_conflict = true;
d_conflictNode = conflict;
}
bool inConflict() {
return d_conflict;
}
void sendConflict();
friend class Bitblaster;
friend class BitblastSolver;
friend class EqualitySolver;
};/* class TheoryBV */
}/* CVC4::theory::bv namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__BV__THEORY_BV_H */
|
