1 /********************* */
2 /*! \file bv_quick_check.h
4 ** Top contributors (to current version):
5 ** Liana Hadarean, Paul Meng, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Sandboxed sat solver for bv quickchecks.
14 ** Sandboxed sat solver for bv quickchecks.
17 #include "cvc4_private.h"
19 #ifndef __CVC4__BV_QUICK_CHECK_H
20 #define __CVC4__BV_QUICK_CHECK_H
23 #include <unordered_set>
25 #include "context/cdo.h"
26 #include "expr/node.h"
27 #include "prop/sat_solver_types.h"
28 #include "theory/bv/theory_bv_utils.h"
29 #include "util/statistics_registry.h"
38 class TLazyBitblaster
;
42 context::Context d_ctx
;
43 TLazyBitblaster
* d_bitblaster
;
45 context::CDO
<bool> d_inConflict
;
49 BVQuickCheck(const std::string
& name
, theory::bv::TheoryBV
* bv
);
52 Node
getConflict() { return d_conflict
; }
54 * Checks the satisfiability for a given set of assumptions.
56 * @param assumptions literals assumed true
57 * @param budget max number of conflicts
61 prop::SatValue
checkSat(std::vector
<Node
>& assumptions
, unsigned long budget
);
63 * Checks the satisfiability of given assertions.
65 * @param budget max number of conflicts
69 prop::SatValue
checkSat(unsigned long budget
);
72 * Convert to CNF and assert the given literal.
74 * @param assumption bv literal
76 * @return false if a conflict has been found via bcp.
78 bool addAssertion(TNode assumption
);
84 * Deletes the SAT solver and CNF stream, but maintains the
85 * bit-blasting term cache.
91 * Computes the size of the circuit required to bit-blast
92 * atom, by not recounting the nodes in seen.
99 uint64_t computeAtomWeight(TNode atom
, NodeSet
& seen
);
100 void collectModelInfo(theory::TheoryModel
* model
, bool fullModel
);
102 typedef std::unordered_set
<TNode
, TNodeHashFunction
>::const_iterator vars_iterator
;
103 vars_iterator
beginVars();
104 vars_iterator
endVars();
106 Node
getVarValue(TNode var
, bool fullModel
);
113 TimerStat d_xplainTime
;
115 IntStat d_numUnknown
;
116 IntStat d_numUnknownWasUnsat
;
117 IntStat d_numConflictsMinimized
;
118 IntStat d_finalPeriod
;
119 AverageStat d_avgMinimizationRatio
;
120 Statistics(const std::string
&);
123 BVQuickCheck
* d_solver
;
124 unsigned long d_budget
;
126 // crazy heuristic variables
127 unsigned d_numCalled
; // number of times called
128 double d_minRatioSum
; // sum of minimization ratio for computing average min ratio
129 unsigned d_numConflicts
; // number of conflicts (including when minimization not applied)
130 // unsigned d_period; // after how many conflicts to try minimizing again
132 // double d_thresh; // if minimization ratio is less, increase period
133 // double d_hardThresh; // decrease period if minimization ratio is greater than this
136 Statistics d_statistics
;
138 * Uses solve with assumptions unsat core feature to
139 * further minimize a conflict. The minimized conflict
140 * will be between low and the returned value in conflict.
148 unsigned selectUnsatCore(unsigned low
, unsigned high
,
149 std::vector
<TNode
>& conflict
);
151 * Internal conflict minimization, attempts to minimize
152 * literals in conflict between low and high and adds the
153 * result in new_conflict.
158 * @param new_conflict
160 void minimizeConflictInternal(unsigned low
, unsigned high
,
161 std::vector
<TNode
>& conflict
,
162 std::vector
<TNode
>& new_conflict
);
166 QuickXPlain(const std::string
& name
, BVQuickCheck
* solver
, unsigned long budged
= 10000);
168 Node
minimizeConflict(TNode conflict
);
172 } /* theory namespace */
173 } /* CVC4 namespace */
175 #endif /* __CVC4__BV_QUICK_CHECK_H */