Branch data Line data Source code
1 : : /************************************************************************************[SimpSolver.h]
2 : : Copyright (c) 2006, Niklas Een, Niklas Sorensson
3 : : Copyright (c) 2007-2010, Niklas Sorensson
4 : :
5 : : Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
6 : : associated documentation files (the "Software"), to deal in the Software without restriction,
7 : : including without limitation the rights to use, copy, modify, merge, publish, distribute,
8 : : sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
9 : : furnished to do so, subject to the following conditions:
10 : :
11 : : The above copyright notice and this permission notice shall be included in all copies or
12 : : substantial portions of the Software.
13 : :
14 : : THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
15 : : NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
16 : : NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
17 : : DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
18 : : OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
19 : : **************************************************************************************************/
20 : :
21 : : #ifndef Minisat_SimpSolver_h
22 : : #define Minisat_SimpSolver_h
23 : :
24 : : #include "base/check.h"
25 : : #include "cvc5_private.h"
26 : : #include "proof/clause_id.h"
27 : : #include "prop/minisat/core/Solver.h"
28 : : #include "prop/minisat/mtl/Queue.h"
29 : :
30 : : namespace cvc5::internal {
31 : : namespace prop {
32 : : class TheoryProxy;
33 : : class PropPfManager;
34 : : }
35 : : } // namespace cvc5::internal
36 : :
37 : : namespace cvc5::internal {
38 : : namespace Minisat {
39 : :
40 : : //=================================================================================================
41 : :
42 : : class SimpSolver : public Solver {
43 : : public:
44 : : // Constructor/Destructor:
45 : : //
46 : : SimpSolver(Env& env,
47 : : prop::TheoryProxy* proxy,
48 : : context::Context* context,
49 : : bool enableIncremental = false);
50 : :
51 : 102436 : virtual ~SimpSolver() = default;
52 : :
53 : : void attachProofManager(prop::PropPfManager* ppm) override;
54 : :
55 : : // Problem specification:
56 : : //
57 : : Var newVar(bool polarity = true,
58 : : bool dvar = true,
59 : : bool isTheoryAtom = false,
60 : : bool canErase = true);
61 : : bool addClause(const vec<Lit>& ps, bool removable, ClauseId& id);
62 : : bool addEmptyClause(bool removable); // Add the empty clause to the solver.
63 : : bool addClause(Lit p,
64 : : bool removable,
65 : : ClauseId& id); // Add a unit clause to the solver.
66 : : bool addClause(Lit p,
67 : : Lit q,
68 : : bool removable,
69 : : ClauseId& id); // Add a binary clause to the solver.
70 : : bool addClause(Lit p,
71 : : Lit q,
72 : : Lit r,
73 : : bool removable,
74 : : ClauseId& id); // Add a ternary clause to the solver.
75 : : bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
76 : : bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may
77 : : // cause a contradiction).
78 : :
79 : : // Variable mode:
80 : : //
81 : : void setFrozen(Var v,
82 : : bool b); // If a variable is frozen it will not be eliminated.
83 : : bool isEliminated(Var v) const;
84 : :
85 : : // Solving:
86 : : //
87 : : lbool solve(const vec<Lit>& assumps,
88 : : bool do_simp = true,
89 : : bool turn_off_simp = false);
90 : : lbool solveLimited(const vec<Lit>& assumps,
91 : : bool do_simp = true,
92 : : bool turn_off_simp = false);
93 : : lbool solve(bool do_simp = true, bool turn_off_simp = false);
94 : : lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false);
95 : : lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
96 : : lbool solve(
97 : : Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
98 : : bool eliminate(bool turn_off_elim = false); // Perform variable elimination
99 : : // based simplification.
100 : :
101 : : // Memory managment:
102 : : //
103 : : void garbageCollect() override;
104 : :
105 : : // Generate a (possibly simplified) DIMACS file:
106 : : //
107 : : #if 0
108 : : void toDimacs (const char* file, const vec<Lit>& assumps);
109 : : void toDimacs (const char* file);
110 : : void toDimacs (const char* file, Lit p);
111 : : void toDimacs (const char* file, Lit p, Lit q);
112 : : void toDimacs (const char* file, Lit p, Lit q, Lit r);
113 : : #endif
114 : :
115 : : // Mode of operation:
116 : : //
117 : : int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
118 : : int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
119 : : // -1 means no limit.
120 : : int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
121 : : double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
122 : :
123 : : bool use_asymm; // Shrink clauses by asymmetric branching.
124 : : bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
125 : :
126 : : // Statistics:
127 : : //
128 : : int merges;
129 : : int asymm_lits;
130 : : int eliminated_vars;
131 : :
132 : : protected:
133 : :
134 : : // Helper structures:
135 : : //
136 : : struct ElimLt {
137 : : const vec<int>& n_occ;
138 : 51563 : explicit ElimLt(const vec<int>& no) : n_occ(no) {}
139 : :
140 : : // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
141 : : // 32-bit implementation instead then, but this will have to do for now.
142 : 4909518 : uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
143 : :
144 : : // old ordering function
145 : : // bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
146 : :
147 : 2454759 : bool operator()(Var x, Var y) const
148 : : {
149 : 2454759 : int c_x = cost(x);
150 : 2454759 : int c_y = cost(y);
151 [ + + ][ + + ]: 2454759 : return c_x < c_y || (c_x == c_y && x < y);
[ + + ]
152 : : }
153 : : };
154 : :
155 : : struct ClauseDeleted {
156 : : const ClauseAllocator& ca;
157 : 51563 : explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
158 : 384029 : bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
159 : :
160 : : // Solver state:
161 : : //
162 : : int elimorder;
163 : : bool use_simplification;
164 : : vec<uint32_t> elimclauses;
165 : : vec<char> touched;
166 : : OccLists<Var, vec<CRef>, ClauseDeleted>
167 : : occurs;
168 : : vec<int> n_occ;
169 : : Heap<ElimLt> elim_heap;
170 : : Queue<CRef> subsumption_queue;
171 : : vec<char> frozen;
172 : : vec<char> eliminated;
173 : : int bwdsub_assigns;
174 : : int n_touched;
175 : :
176 : : // Temporaries:
177 : : //
178 : : CRef bwdsub_tmpunit;
179 : :
180 : : // Main internal methods:
181 : : //
182 : : lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
183 : : bool asymm (Var v, CRef cr);
184 : : bool asymmVar (Var v);
185 : : void updateElimHeap (Var v);
186 : : void gatherTouchedClauses ();
187 : : bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
188 : : bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
189 : : bool backwardSubsumptionCheck (bool verbose = false);
190 : : bool eliminateVar (Var v);
191 : : void extendModel ();
192 : :
193 : : void removeClause (CRef cr);
194 : : bool strengthenClause (CRef cr, Lit l);
195 : : void cleanUpClauses ();
196 : : bool implied (const vec<Lit>& c);
197 : : void relocAll (ClauseAllocator& to);
198 : : };
199 : :
200 : :
201 : : //=================================================================================================
202 : : // Implementation of inline methods:
203 : :
204 : :
205 : 1664784 : inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
206 : 175301 : inline void SimpSolver::updateElimHeap(Var v) {
207 [ - + ][ - + ]: 175301 : Assert(use_simplification);
[ - - ]
208 : : // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
209 : 175301 : if (elim_heap.inHeap(v)
210 [ + + ][ + + ]: 175301 : || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
[ + + ][ + - ]
[ + + ]
211 : 124597 : elim_heap.update(v);
212 : 175301 : }
213 : :
214 : 5931961 : inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
215 : 5931961 : { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
216 : : inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); }
217 : : inline bool SimpSolver::addClause (Lit p, bool removable, ClauseId& id)
218 : : { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
219 : : inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, ClauseId& id)
220 : : { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
221 : : inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
222 : : { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
223 [ - - ][ - - ]: 0 : inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
224 : :
225 : : // the solver can always return unknown due to resource limiting
226 : 41333 : inline lbool SimpSolver::solve ( bool do_simp, bool turn_off_simp) {
227 : 41333 : budgetOff();
228 : 41333 : assumptions.clear();
229 : 41333 : return solve_(do_simp, turn_off_simp);
230 : : }
231 : :
232 : : inline lbool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) {
233 : : budgetOff();
234 : : assumptions.clear();
235 : : assumptions.push(p);
236 : : return solve_(do_simp, turn_off_simp);
237 : : }
238 : :
239 : : inline lbool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) {
240 : : budgetOff();
241 : : assumptions.clear();
242 : : assumptions.push(p);
243 : : assumptions.push(q);
244 : : return solve_(do_simp, turn_off_simp);
245 : : }
246 : :
247 : : inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) {
248 : : budgetOff();
249 : : assumptions.clear();
250 : : assumptions.push(p);
251 : : assumptions.push(q);
252 : : assumptions.push(r);
253 : : return solve_(do_simp, turn_off_simp);
254 : : }
255 : :
256 : 8953 : inline lbool SimpSolver::solve(const vec<Lit>& assumps,
257 : : bool do_simp,
258 : : bool turn_off_simp)
259 : : {
260 : 8953 : budgetOff();
261 : 8953 : assumps.copyTo(assumptions);
262 : 8953 : return solve_(do_simp, turn_off_simp);
263 : : }
264 : :
265 : 0 : inline lbool SimpSolver::solveLimited(const vec<Lit>& assumps,
266 : : bool do_simp,
267 : : bool turn_off_simp)
268 : : {
269 : 0 : assumps.copyTo(assumptions);
270 : 0 : return solve_(do_simp, turn_off_simp);
271 : : }
272 : :
273 : : //=================================================================================================
274 : : } // namespace Minisat
275 : : } // namespace cvc5::internal
276 : :
277 : : #endif
|
