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
|
/******************************************************************************
* Top contributors (to current version):
* Liana Hadarean, Mathias Preiner, Morgan Deters
*
* 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.
* ****************************************************************************
*
* Sandboxed SAT solver for bv quickchecks.
*/
#include "cvc4_private.h"
#ifndef CVC5__BV_QUICK_CHECK_H
#define CVC5__BV_QUICK_CHECK_H
#include <unordered_set>
#include <vector>
#include "context/cdo.h"
#include "expr/node.h"
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv_utils.h"
#include "util/statistics_registry.h"
#include "util/stats_timer.h"
namespace cvc5 {
namespace theory {
class TheoryModel;
namespace bv {
class TLazyBitblaster;
class BVSolverLazy;
class BVQuickCheck
{
context::Context d_ctx;
std::unique_ptr<TLazyBitblaster> d_bitblaster;
Node d_conflict;
context::CDO<bool> d_inConflict;
void setConflict();
public:
BVQuickCheck(const std::string& name, theory::bv::BVSolverLazy* bv);
~BVQuickCheck();
bool inConflict();
Node getConflict() { return d_conflict; }
/**
* Checks the satisfiability for a given set of assumptions.
*
* @param assumptions literals assumed true
* @param budget max number of conflicts
*
* @return
*/
prop::SatValue checkSat(std::vector<Node>& assumptions, unsigned long budget);
/**
* Checks the satisfiability of given assertions.
*
* @param budget max number of conflicts
*
* @return
*/
prop::SatValue checkSat(unsigned long budget);
/**
* Convert to CNF and assert the given literal.
*
* @param assumption bv literal
*
* @return false if a conflict has been found via bcp.
*/
bool addAssertion(TNode assumption);
void push();
void pop();
void popToZero();
/**
* Deletes the SAT solver and CNF stream, but maintains the
* bit-blasting term cache.
*
*/
void clearSolver();
/**
* Computes the size of the circuit required to bit-blast
* atom, by not recounting the nodes in seen.
*
* @param node
* @param seen
*
* @return
*/
uint64_t computeAtomWeight(TNode atom, NodeSet& seen);
bool collectModelValues(theory::TheoryModel* model,
const std::set<Node>& termSet);
typedef std::unordered_set<TNode, TNodeHashFunction>::const_iterator
vars_iterator;
vars_iterator beginVars();
vars_iterator endVars();
Node getVarValue(TNode var, bool fullModel);
};
class QuickXPlain
{
struct Statistics
{
TimerStat d_xplainTime;
IntStat d_numSolved;
IntStat d_numUnknown;
IntStat d_numUnknownWasUnsat;
IntStat d_numConflictsMinimized;
IntStat d_finalPeriod;
AverageStat d_avgMinimizationRatio;
Statistics(const std::string& name);
~Statistics();
};
BVQuickCheck* d_solver;
unsigned long d_budget;
// crazy heuristic variables
unsigned d_numCalled; // number of times called
double d_minRatioSum; // sum of minimization ratio for computing average min
// ratio
unsigned d_numConflicts; // number of conflicts (including when minimization
// not applied)
// unsigned d_period; // after how many conflicts to try minimizing again
// double d_thresh; // if minimization ratio is less, increase period
// double d_hardThresh; // decrease period if minimization ratio is greater
// than this
Statistics d_statistics;
/**
* Uses solve with assumptions unsat core feature to
* further minimize a conflict. The minimized conflict
* will be between low and the returned value in conflict.
*
* @param low
* @param high
* @param conflict
*
* @return
*/
unsigned selectUnsatCore(unsigned low,
unsigned high,
std::vector<TNode>& conflict);
/**
* Internal conflict minimization, attempts to minimize
* literals in conflict between low and high and adds the
* result in new_conflict.
*
* @param low
* @param high
* @param conflict
* @param new_conflict
*/
void minimizeConflictInternal(unsigned low,
unsigned high,
std::vector<TNode>& conflict,
std::vector<TNode>& new_conflict);
bool useHeuristic();
public:
QuickXPlain(const std::string& name,
BVQuickCheck* solver,
unsigned long budged = 10000);
~QuickXPlain();
Node minimizeConflict(TNode conflict);
};
} // namespace bv
} // namespace theory
} // namespace cvc5
#endif /* CVC5__BV_QUICK_CHECK_H */
|
