GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/bvminisat/core/Solver.h Lines: 61 73 83.6 %
Date: 2021-03-23 Branches: 45 86 52.3 %

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