1 /****************************************************************************************[Solver.h]
2 Copyright (c) 2003-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 BVMinisat_Solver_h
22 #define BVMinisat_Solver_h
23
24 #include <vector>
25
26 #include "context/context.h"
27 #include "proof/clause_id.h"
28 #include "proof/sat_proof.h"
29 #include "prop/bvminisat/core/SolverTypes.h"
30 #include "prop/bvminisat/mtl/Alg.h"
31 #include "prop/bvminisat/mtl/Heap.h"
32 #include "prop/bvminisat/mtl/Vec.h"
33 #include "prop/bvminisat/utils/Options.h"
34
35
36 namespace CVC4 {
37
38 namespace BVMinisat {
39 class Solver;
40 }
41
42 // TODO (aozdemir) replace this forward declaration with an include
43 namespace proof {
44 class ResolutionBitVectorProof;
45 }
46
47 namespace BVMinisat {
48
49 /** Interface for minisat callbacks */
50 class Notify {
51
52 public:
53
~Notify()54 virtual ~Notify() {}
55
56 /**
57 * If the notify returns false, the solver will break out of whatever it's currently doing
58 * with an "unknown" answer.
59 */
60 virtual bool notify(Lit lit) = 0;
61
62 /**
63 * Notify about a new learnt clause with marked literals only.
64 */
65 virtual void notify(vec<Lit>& learnt) = 0;
66
67 virtual void spendResource(unsigned amount) = 0;
68 virtual void safePoint(unsigned amount) = 0;
69 };
70
71 //=================================================================================================
72 // Solver -- the main class:
73 class Solver {
74 friend class CVC4::TSatProof< CVC4::BVMinisat::Solver>;
75 public:
76 typedef Var TVar;
77 typedef Lit TLit;
78 typedef Clause TClause;
79 typedef CRef TCRef;
80 typedef vec<Lit> TLitVec;
81
82 static CRef TCRef_Undef;
83 static CRef TCRef_Lazy;
84 private:
85 /** To notify */
86 Notify* d_notify;
87
88 /** Cvc4 context */
89 CVC4::context::Context* c;
90
91 /** True constant */
92 Var varTrue;
93
94 /** False constant */
95 Var varFalse;
96
97 public:
98
99 // Constructor/Destructor:
100 //
101 Solver(CVC4::context::Context* c);
102 virtual ~Solver();
103
104 void setNotify(Notify* toNotify);
105
106 // Problem specification:
107 //
108 Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
trueVar()109 Var trueVar() const { return varTrue; }
falseVar()110 Var falseVar() const { return varFalse; }
111
112
113 bool addClause (const vec<Lit>& ps, ClauseId& id); // Add a clause to the solver.
114 bool addEmptyClause(); // Add the empty clause, making the solver contradictory.
115 bool addClause (Lit p, ClauseId& id); // Add a unit clause to the solver.
116 bool addClause (Lit p, Lit q, ClauseId& id); // Add a binary clause to the solver.
117 bool addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver.
118 bool addClause_( vec<Lit>& ps, ClauseId& id); // Add a clause to the solver without making superflous internal copy. Will
119 // change the passed vector 'ps'.
120
121 // Solving:
122 //
123 bool simplify (); // Removes already satisfied clauses.
124 lbool solve (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
125 lbool solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
126 lbool solve (); // Search without assumptions.
127 lbool solve (Lit p); // Search for a model that respects a single assumption.
128 lbool solve (Lit p, Lit q); // Search for a model that respects two assumptions.
129 lbool solve (Lit p, Lit q, Lit r); // Search for a model that respects three assumptions.
130 bool okay () const; // FALSE means solver is in a conflicting state
131 lbool assertAssumption(Lit p, bool propagate); // Assert a new assumption, start BCP if propagate = true
132 lbool propagateAssumptions(); // Do BCP over asserted assumptions
133 void popAssumption(); // Pop an assumption
134
135 void toDimacs (FILE* f, const vec<Lit>& assumps); // Write CNF to file in DIMACS-format.
136 void toDimacs (const char *file, const vec<Lit>& assumps);
137 void toDimacs (FILE* f, Clause& c, vec<Var>& map, Var& max);
138
139 // Convenience versions of 'toDimacs()':
140 void toDimacs (const char* file);
141 void toDimacs (const char* file, Lit p);
142 void toDimacs (const char* file, Lit p, Lit q);
143 void toDimacs (const char* file, Lit p, Lit q, Lit r);
144
145 // Variable mode:
146 //
147 void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
148 void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
149
150 // Read state:
151 //
152 lbool value (Var x) const; // The current value of a variable.
153 lbool value (Lit p) const; // The current value of a literal.
154 lbool modelValue (Var x) const; // The value of a variable in the last model. The last call to solve must have been satisfiable.
155 lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable.
156 int nAssigns () const; // The current number of assigned literals.
157 int nClauses () const; // The current number of original clauses.
158 int nLearnts () const; // The current number of learnt clauses.
159 int nVars () const; // The current number of variables.
160 int nFreeVars () const;
161
162 // Resource contraints:
163 //
164 void setConfBudget(int64_t x);
165 void setPropBudget(int64_t x);
166 void budgetOff();
167 void interrupt(); // Trigger a (potentially asynchronous) interruption of the solver.
168 void clearInterrupt(); // Clear interrupt indicator flag.
169
170 // Memory managment:
171 //
172 virtual void garbageCollect();
173 void checkGarbage(double gf);
174 void checkGarbage();
175
176 // Extra results: (read-only member variable)
177 //
178 vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
179 vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions),
180 // this vector represent the final conflict clause expressed in the assumptions.
181
182 // Mode of operation:
183 //
184 int verbosity;
185 double var_decay;
186 double clause_decay;
187 double random_var_freq;
188 double random_seed;
189 bool luby_restart;
190 int ccmin_mode; // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
191 int phase_saving; // Controls the level of phase saving (0=none, 1=limited, 2=full).
192 bool rnd_pol; // Use random polarities for branching heuristics.
193 bool rnd_init_act; // Initialize variable activities with a small random value.
194 double garbage_frac; // The fraction of wasted memory allowed before a garbage collection is triggered.
195
196 int restart_first; // The initial restart limit. (default 100)
197 double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5)
198 double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3)
199 double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1)
200
201 int learntsize_adjust_start_confl;
202 double learntsize_adjust_inc;
203
204 // Statistics: (read-only member variable)
205 //
206 uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
207 uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
208
209 // Bitvector Propagations
210 //
211
212 void addMarkerLiteral(Var var);
213
214 bool need_to_propagate; // true if we added new clauses, set to true in propagation
215 bool only_bcp; // solving mode in which only boolean constraint propagation is done
setOnlyBCP(bool val)216 void setOnlyBCP (bool val) { only_bcp = val;}
217 void explain(Lit l, std::vector<Lit>& explanation);
218
219 void setProofLog(CVC4::proof::ResolutionBitVectorProof* bvp);
220
221 protected:
222
223 // has a clause been added
224 bool clause_added;
225
226 // Helper structures:
227 //
228 struct VarData { CRef reason; int level; };
mkVarData(CRef cr,int l)229 static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
230
231 struct Watcher {
232 CRef cref;
233 Lit blocker;
WatcherWatcher234 Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
235 bool operator==(const Watcher& w) const { return cref == w.cref; }
236 bool operator!=(const Watcher& w) const { return cref != w.cref; }
237 };
238
239 struct WatcherDeleted
240 {
241 const ClauseAllocator& ca;
WatcherDeletedWatcherDeleted242 WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
operatorWatcherDeleted243 bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
244 };
245
246 struct VarOrderLt {
247 const vec<double>& activity;
operatorVarOrderLt248 bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
VarOrderLtVarOrderLt249 VarOrderLt(const vec<double>& act) : activity(act) { }
250 };
251
252 // Solver state:
253 //
254 bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
255 vec<CRef> clauses; // List of problem clauses.
256 vec<CRef> learnts; // List of learnt clauses.
257 double cla_inc; // Amount to bump next clause with.
258 vec<double> activity; // A heuristic measurement of the activity of a variable.
259 double var_inc; // Amount to bump next variable with.
260 OccLists<Lit, vec<Watcher>, WatcherDeleted>
261 watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
262 vec<lbool> assigns; // The current assignments.
263 vec<char> polarity; // The preferred polarity of each variable.
264 vec<char> marker; // Is the variable a marker literal
265 vec<char> decision; // Declares if a variable is eligible for selection in the decision heuristic.
266 vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
267 vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
268 vec<VarData> vardata; // Stores reason and level for each variable.
269 int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
270 int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
271 int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
272 vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
273 Heap<VarOrderLt> order_heap; // A priority queue of variables ordered with respect to the variable activity.
274 double progress_estimate;// Set by 'search()'.
275 bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
276
277 ClauseAllocator ca;
278
279 // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
280 // used, exept 'seen' wich is used in several places.
281 //
282 vec<char> seen;
283 vec<Lit> analyze_stack;
284 vec<Lit> analyze_toclear;
285 vec<Lit> add_tmp;
286
287 double max_learnts;
288 double learntsize_adjust_confl;
289 int learntsize_adjust_cnt;
290
291 // Resource contraints:
292 //
293 int64_t conflict_budget; // -1 means no budget.
294 int64_t propagation_budget; // -1 means no budget.
295 bool asynch_interrupt;
296
297 //proof log
298 CVC4::proof::ResolutionBitVectorProof* d_bvp;
299
300 // Main internal methods:
301 //
302 void insertVarOrder (Var x); // Insert a variable in the decision order priority queue.
303 Lit pickBranchLit (); // Return the next decision variable.
304 void newDecisionLevel (); // Begins a new decision level.
305 void uncheckedEnqueue (Lit p, CRef from = CRef_Undef); // Enqueue a literal. Assumes value of literal is undefined.
306 bool enqueue (Lit p, CRef from = CRef_Undef); // Test if fact 'p' contradicts current state, enqueue otherwise.
307 CRef propagate (); // Perform unit propagation. Returns possibly conflicting clause.
308 void cancelUntil (int level); // Backtrack until a certain level.
309
310 enum UIP {
311 UIP_FIRST,
312 UIP_LAST
313 };
314
315 void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip = UIP_FIRST); // (bt = backtrack)
316 void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
317 void analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict);
318 bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()')
319 lbool search (int nof_conflicts, UIP uip = UIP_FIRST); // Search for a given number of conflicts.
320 lbool solve_ (); // Main solve method (assumptions given in 'assumptions').
321 void reduceDB (); // Reduce the set of learnt clauses.
322 void removeSatisfied (vec<CRef>& cs); // Shrink 'cs' to contain only non-satisfied clauses.
323 void rebuildOrderHeap ();
324
325 // Maintaining Variable/Clause activity:
326 //
327 void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
328 void varBumpActivity (Var v, double inc); // Increase a variable with the current 'bump' value.
329 void varBumpActivity (Var v); // Increase a variable with the current 'bump' value.
330 void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
331 void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value.
332
333 // Operations on clauses:
334 //
335 void attachClause (CRef cr); // Attach a clause to watcher lists.
336 void detachClause (CRef cr, bool strict = false); // Detach a clause to watcher lists.
337 void removeClause (CRef cr); // Detach and free a clause.
338 bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
339 bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
340
341 void relocAll (ClauseAllocator& to);
342
343 // Misc:
344 //
345 int decisionLevel () const; // Gives the current decisionlevel.
346 uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels.
347 CRef reason (Var x) const;
348 int level (Var x) const;
349 double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
350 bool withinBudget (uint64_t amount) const;
351
352 // Static helpers:
353 //
354
355 // Returns a random float 0 <= x < 1. Seed must never be 0.
drand(double & seed)356 static inline double drand(double& seed) {
357 seed *= 1389796;
358 int q = (int)(seed / 2147483647);
359 seed -= (double)q * 2147483647;
360 return seed / 2147483647; }
361
362 // Returns a random integer 0 <= x < size. Seed must never be 0.
irand(double & seed,int size)363 static inline int irand(double& seed, int size) {
364 return (int)(drand(seed) * size); }
365
366 // Less than for literals in an added clause when proofs are on.
367 struct assign_lt {
368 Solver& solver;
assign_ltassign_lt369 assign_lt(Solver& solver) : solver(solver) {}
operatorassign_lt370 bool operator () (Lit x, Lit y) {
371 lbool x_value = solver.value(x);
372 lbool y_value = solver.value(y);
373 // Two unassigned literals are sorted arbitrarily
374 if (x_value == l_Undef && y_value == l_Undef) {
375 return x < y;
376 }
377 // Unassigned literals are put to front
378 if (x_value == l_Undef) return true;
379 if (y_value == l_Undef) return false;
380 // Literals of the same value are sorted by decreasing levels
381 if (x_value == y_value) {
382 return solver.level(var(x)) > solver.level(var(y));
383 } else {
384 // True literals go up front
385 if (x_value == l_True) {
386 return true;
387 } else {
388 return false;
389 }
390 }
391 }
392 };
393
394 };
395
396
397 //=================================================================================================
398 // Implementation of inline methods:
399
reason(Var x)400 inline CRef Solver::reason(Var x) const { assert(x < vardata.size()); return vardata[x].reason; }
level(Var x)401 inline int Solver::level (Var x) const { assert(x < vardata.size()); return vardata[x].level; }
402
insertVarOrder(Var x)403 inline void Solver::insertVarOrder(Var x) {
404 if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
405
varDecayActivity()406 inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
varBumpActivity(Var v)407 inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
varBumpActivity(Var v,double inc)408 inline void Solver::varBumpActivity(Var v, double inc) {
409 if ( (activity[v] += inc) > 1e100 ) {
410 // Rescale:
411 for (int i = 0; i < nVars(); i++)
412 activity[i] *= 1e-100;
413 var_inc *= 1e-100; }
414
415 // Update order_heap with respect to new activity:
416 if (order_heap.inHeap(v))
417 order_heap.decrease(v); }
418
claDecayActivity()419 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
claBumpActivity(Clause & c)420 inline void Solver::claBumpActivity (Clause& c) {
421 if ( (c.activity() += cla_inc) > 1e20 ) {
422 // Rescale:
423 for (int i = 0; i < learnts.size(); i++)
424 ca[learnts[i]].activity() *= 1e-20;
425 cla_inc *= 1e-20; } }
426
checkGarbage(void)427 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
checkGarbage(double gf)428 inline void Solver::checkGarbage(double gf){
429 if (ca.wasted() > ca.size() * gf)
430 garbageCollect(); }
431
432 // NOTE: enqueue does not set the ok flag! (only public methods do)
enqueue(Lit p,CRef from)433 inline bool Solver::enqueue (Lit p, CRef from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
addClause(const vec<Lit> & ps,ClauseId & id)434 inline bool Solver::addClause (const vec<Lit>& ps, ClauseId& id) { ps.copyTo(add_tmp); return addClause_(add_tmp, id); }
addEmptyClause()435 inline bool Solver::addEmptyClause () { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, tmp); }
addClause(Lit p,ClauseId & id)436 inline bool Solver::addClause (Lit p, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); }
addClause(Lit p,Lit q,ClauseId & id)437 inline bool Solver::addClause (Lit p, Lit q, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); }
addClause(Lit p,Lit q,Lit r,ClauseId & id)438 inline bool Solver::addClause (Lit p, Lit q, Lit r, ClauseId& id) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); }
locked(const Clause & c)439 inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
newDecisionLevel()440 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); }
441
decisionLevel()442 inline int Solver::decisionLevel () const { return trail_lim.size(); }
abstractLevel(Var x)443 inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); }
value(Var x)444 inline lbool Solver::value (Var x) const { return assigns[x]; }
value(Lit p)445 inline lbool Solver::value (Lit p) const { return assigns[var(p)] ^ sign(p); }
modelValue(Var x)446 inline lbool Solver::modelValue (Var x) const { return model[x]; }
modelValue(Lit p)447 inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); }
nAssigns()448 inline int Solver::nAssigns () const { return trail.size(); }
nClauses()449 inline int Solver::nClauses () const { return clauses.size(); }
nLearnts()450 inline int Solver::nLearnts () const { return learnts.size(); }
nVars()451 inline int Solver::nVars () const { return vardata.size(); }
nFreeVars()452 inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
setPolarity(Var v,bool b)453 inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
setDecisionVar(Var v,bool b)454 inline void Solver::setDecisionVar(Var v, bool b)
455 {
456 if ( b && !decision[v]) dec_vars++;
457 else if (!b && decision[v]) dec_vars--;
458
459 decision[v] = b;
460 insertVarOrder(v);
461 }
setConfBudget(int64_t x)462 inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
setPropBudget(int64_t x)463 inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
interrupt()464 inline void Solver::interrupt(){ asynch_interrupt = true; }
clearInterrupt()465 inline void Solver::clearInterrupt(){ asynch_interrupt = false; }
budgetOff()466 inline void Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
467
solve()468 inline lbool Solver::solve () { budgetOff(); return solve_(); }
solve(Lit p)469 inline lbool Solver::solve (Lit p) { budgetOff(); assumptions.push(p); return solve_(); }
solve(Lit p,Lit q)470 inline lbool Solver::solve (Lit p, Lit q) { budgetOff(); assumptions.push(p); assumptions.push(q); return solve_(); }
solve(Lit p,Lit q,Lit r)471 inline lbool Solver::solve (Lit p, Lit q, Lit r) { budgetOff(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(); }
solve(const vec<Lit> & assumps)472 inline lbool Solver::solve (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_(); }
solveLimited(const vec<Lit> & assumps)473 inline lbool Solver::solveLimited (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
okay()474 inline bool Solver::okay () const { return ok; }
475
toDimacs(const char * file)476 inline void Solver::toDimacs (const char* file){ vec<Lit> as; toDimacs(file, as); }
toDimacs(const char * file,Lit p)477 inline void Solver::toDimacs (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
toDimacs(const char * file,Lit p,Lit q)478 inline void Solver::toDimacs (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
toDimacs(const char * file,Lit p,Lit q,Lit r)479 inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }
480
481
482 //=================================================================================================
483 // Debug etc:
484
485
486 //=================================================================================================
487 } /* CVC4::BVMinisat namespace */
488 } /* CVC4 namespace */
489
490
491 #endif
492