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 : : context::UserContext* userContext,
50 : : prop::PropPfManager* ppm,
51 : : bool enableIncremental = false);
52 : : ~SimpSolver();
53 : :
54 : : // Problem specification:
55 : : //
56 : : Var newVar(bool polarity = true,
57 : : bool dvar = true,
58 : : bool isTheoryAtom = false,
59 : : bool canErase = true);
60 : : bool addClause(const vec<Lit>& ps, bool removable, ClauseId& id);
61 : : bool addEmptyClause(bool removable); // Add the empty clause to the solver.
62 : : bool addClause(Lit p,
63 : : bool removable,
64 : : ClauseId& id); // Add a unit clause to the solver.
65 : : bool addClause(Lit p,
66 : : Lit q,
67 : : bool removable,
68 : : ClauseId& id); // Add a binary clause to the solver.
69 : : bool addClause(Lit p,
70 : : Lit q,
71 : : Lit r,
72 : : bool removable,
73 : : ClauseId& id); // Add a ternary clause to the solver.
74 : : bool addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
75 : : bool substitute(Var v, Lit x); // Replace all occurrences of v with x (may
76 : : // cause a contradiction).
77 : :
78 : : // Variable mode:
79 : : //
80 : : void setFrozen(Var v,
81 : : bool b); // If a variable is frozen it will not be eliminated.
82 : : bool isEliminated(Var v) const;
83 : :
84 : : // Solving:
85 : : //
86 : : lbool solve(const vec<Lit>& assumps,
87 : : bool do_simp = true,
88 : : bool turn_off_simp = false);
89 : : lbool solveLimited(const vec<Lit>& assumps,
90 : : bool do_simp = true,
91 : : bool turn_off_simp = false);
92 : : lbool solve(bool do_simp = true, bool turn_off_simp = false);
93 : : lbool solve(Lit p, bool do_simp = true, bool turn_off_simp = false);
94 : : lbool solve(Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
95 : : lbool solve(
96 : : Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
97 : : bool eliminate(bool turn_off_elim = false); // Perform variable elimination
98 : : // based simplification.
99 : :
100 : : // Memory managment:
101 : : //
102 : : void garbageCollect() override;
103 : :
104 : : // Generate a (possibly simplified) DIMACS file:
105 : : //
106 : : #if 0
107 : : void toDimacs (const char* file, const vec<Lit>& assumps);
108 : : void toDimacs (const char* file);
109 : : void toDimacs (const char* file, Lit p);
110 : : void toDimacs (const char* file, Lit p, Lit q);
111 : : void toDimacs (const char* file, Lit p, Lit q, Lit r);
112 : : #endif
113 : :
114 : : // Mode of operation:
115 : : //
116 : : int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
117 : : int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
118 : : // -1 means no limit.
119 : : int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
120 : : double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
121 : :
122 : : bool use_asymm; // Shrink clauses by asymmetric branching.
123 : : bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
124 : :
125 : : // Statistics:
126 : : //
127 : : int merges;
128 : : int asymm_lits;
129 : : int eliminated_vars;
130 : :
131 : : protected:
132 : :
133 : : // Helper structures:
134 : : //
135 : : struct ElimLt {
136 : : const vec<int>& n_occ;
137 : 50267 : explicit ElimLt(const vec<int>& no) : n_occ(no) {}
138 : :
139 : : // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
140 : : // 32-bit implementation instead then, but this will have to do for now.
141 : 4944900 : uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
142 : :
143 : : // old ordering function
144 : : // bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
145 : :
146 : 2472450 : bool operator()(Var x, Var y) const
147 : : {
148 : 2472450 : int c_x = cost(x);
149 : 2472450 : int c_y = cost(y);
150 [ + + ][ + + ]: 2472450 : return c_x < c_y || (c_x == c_y && x < y);
[ + + ]
151 : : }
152 : : };
153 : :
154 : : struct ClauseDeleted {
155 : : const ClauseAllocator& ca;
156 : 50267 : explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
157 : 390402 : bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
158 : :
159 : : // Solver state:
160 : : //
161 : : int elimorder;
162 : : bool use_simplification;
163 : : vec<uint32_t> elimclauses;
164 : : vec<char> touched;
165 : : OccLists<Var, vec<CRef>, ClauseDeleted>
166 : : occurs;
167 : : vec<int> n_occ;
168 : : Heap<ElimLt> elim_heap;
169 : : Queue<CRef> subsumption_queue;
170 : : vec<char> frozen;
171 : : vec<char> eliminated;
172 : : int bwdsub_assigns;
173 : : int n_touched;
174 : :
175 : : // Temporaries:
176 : : //
177 : : CRef bwdsub_tmpunit;
178 : :
179 : : // Main internal methods:
180 : : //
181 : : lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
182 : : bool asymm (Var v, CRef cr);
183 : : bool asymmVar (Var v);
184 : : void updateElimHeap (Var v);
185 : : void gatherTouchedClauses ();
186 : : bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
187 : : bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
188 : : bool backwardSubsumptionCheck (bool verbose = false);
189 : : bool eliminateVar (Var v);
190 : : void extendModel ();
191 : :
192 : : void removeClause (CRef cr);
193 : : bool strengthenClause (CRef cr, Lit l);
194 : : void cleanUpClauses ();
195 : : bool implied (const vec<Lit>& c);
196 : : void relocAll (ClauseAllocator& to);
197 : : };
198 : :
199 : :
200 : : //=================================================================================================
201 : : // Implementation of inline methods:
202 : :
203 : :
204 : 1819890 : inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
205 : 177355 : inline void SimpSolver::updateElimHeap(Var v) {
206 [ - + ][ - + ]: 177355 : Assert(use_simplification);
[ - - ]
207 : : // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
208 : 177355 : if (elim_heap.inHeap(v)
209 [ + + ][ + + ]: 177355 : || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
[ + + ][ + - ]
[ + + ]
210 : 126661 : elim_heap.update(v);
211 : 177355 : }
212 : :
213 : 6256730 : inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
214 : 6256730 : { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
215 : : inline bool SimpSolver::addEmptyClause(bool removable) { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); }
216 : : inline bool SimpSolver::addClause (Lit p, bool removable, ClauseId& id)
217 : : { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
218 : : inline bool SimpSolver::addClause (Lit p, Lit q, bool removable, ClauseId& id)
219 : : { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
220 : : inline bool SimpSolver::addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
221 : : { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
222 [ - - ][ - - ]: 0 : inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
223 : :
224 : : // the solver can always return unknown due to resource limiting
225 : 40767 : inline lbool SimpSolver::solve ( bool do_simp, bool turn_off_simp) {
226 : 40767 : budgetOff();
227 : 40767 : assumptions.clear();
228 : 40767 : return solve_(do_simp, turn_off_simp);
229 : : }
230 : :
231 : : inline lbool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) {
232 : : budgetOff();
233 : : assumptions.clear();
234 : : assumptions.push(p);
235 : : return solve_(do_simp, turn_off_simp);
236 : : }
237 : :
238 : : inline lbool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) {
239 : : budgetOff();
240 : : assumptions.clear();
241 : : assumptions.push(p);
242 : : assumptions.push(q);
243 : : return solve_(do_simp, turn_off_simp);
244 : : }
245 : :
246 : : inline lbool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) {
247 : : budgetOff();
248 : : assumptions.clear();
249 : : assumptions.push(p);
250 : : assumptions.push(q);
251 : : assumptions.push(r);
252 : : return solve_(do_simp, turn_off_simp);
253 : : }
254 : :
255 : 8910 : inline lbool SimpSolver::solve(const vec<Lit>& assumps,
256 : : bool do_simp,
257 : : bool turn_off_simp)
258 : : {
259 : 8910 : budgetOff();
260 : 8910 : assumps.copyTo(assumptions);
261 : 8910 : return solve_(do_simp, turn_off_simp);
262 : : }
263 : :
264 : 0 : inline lbool SimpSolver::solveLimited(const vec<Lit>& assumps,
265 : : bool do_simp,
266 : : bool turn_off_simp)
267 : : {
268 : 0 : assumps.copyTo(assumptions);
269 : 0 : return solve_(do_simp, turn_off_simp);
270 : : }
271 : :
272 : : //=================================================================================================
273 : : } // namespace Minisat
274 : : } // namespace cvc5::internal
275 : :
276 : : #endif
|
