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