GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/minisat/core/Solver.h Lines: 108 114 94.7 %
Date: 2021-03-22 Branches: 98 222 44.1 %

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 Minisat_Solver_h
22
#define Minisat_Solver_h
23
24
#include <iosfwd>
25
26
#include "base/check.h"
27
#include "base/output.h"
28
#include "context/context.h"
29
#include "cvc4_private.h"
30
#include "expr/proof_node_manager.h"
31
#include "proof/clause_id.h"
32
#include "prop/minisat/core/SolverTypes.h"
33
#include "prop/minisat/mtl/Alg.h"
34
#include "prop/minisat/mtl/Heap.h"
35
#include "prop/minisat/mtl/Vec.h"
36
#include "prop/minisat/utils/Options.h"
37
#include "prop/sat_proof_manager.h"
38
#include "theory/theory.h"
39
#include "util/resource_manager.h"
40
41
namespace CVC4 {
42
template <class Solver> class TSatProof;
43
44
namespace prop {
45
class PropEngine;
46
class TheoryProxy;
47
}/* CVC4::prop namespace */
48
}/* CVC4 namespace */
49
50
51
namespace CVC4 {
52
namespace Minisat {
53
54
//=================================================================================================
55
// Solver -- the main class:
56
57
class Solver {
58
59
  /** The only two CVC4 entry points to the private solver data */
60
  friend class CVC4::prop::PropEngine;
61
  friend class CVC4::prop::TheoryProxy;
62
  friend class CVC4::prop::SatProofManager;
63
  friend class CVC4::TSatProof<Minisat::Solver>;
64
65
public:
66
  static CRef TCRef_Undef;
67
  static CRef TCRef_Lazy;
68
69
  typedef Var TVar;
70
  typedef Lit TLit;
71
  typedef Clause TClause;
72
  typedef CRef TCRef;
73
  typedef vec<Lit> TLitVec;
74
75
 protected:
76
  /** The pointer to the proxy that provides interfaces to the SMT engine */
77
  CVC4::prop::TheoryProxy* d_proxy;
78
79
  /** The context from the SMT solver */
80
  CVC4::context::Context* d_context;
81
82
  /** The current assertion level (user) */
83
  int assertionLevel;
84
85
  /** Variable representing true */
86
  Var varTrue;
87
88
  /** Variable representing false */
89
  Var varFalse;
90
91
  /** The resolution proof manager */
92
  std::unique_ptr<CVC4::prop::SatProofManager> d_pfManager;
93
94
 public:
95
  /** Returns the current user assertion level */
96
17599
  int getAssertionLevel() const { return assertionLevel; }
97
98
 protected:
99
  /** Do we allow incremental solving */
100
  bool d_enable_incremental;
101
102
  /** Literals propagated by lemmas */
103
  vec<vec<Lit> > lemmas;
104
105
  /** Is the lemma removable */
106
  vec<bool> lemmas_removable;
107
108
  /** Nodes being converted to CNF */
109
  std::vector<CVC4::Node> lemmas_cnf_assertion;
110
111
  /** Do a another check if FULL_EFFORT was the last one */
112
  bool recheck;
113
114
  /** Shrink 'cs' to contain only clauses below given level */
115
  void removeClausesAboveLevel(vec<CRef>& cs, int level);
116
117
  /** True if we are currently solving. */
118
  bool minisat_busy;
119
120
  // Information about registration of variables
121
  struct VarIntroInfo
122
  {
123
    Var d_var;
124
    int d_level;
125
519356
    VarIntroInfo(Var var, int level) : d_var(var), d_level(level) {}
126
  };
127
128
  /** Variables to re-register with theory solvers on backtracks */
129
  vec<VarIntroInfo> variables_to_register;
130
131
  /** Keep only newSize variables */
132
  void resizeVars(int newSize);
133
134
public:
135
136
    // Constructor/Destructor:
137
    //
138
 Solver(CVC4::prop::TheoryProxy* proxy,
139
        CVC4::context::Context* context,
140
        CVC4::context::UserContext* userContext,
141
        ProofNodeManager* pnm,
142
        bool enableIncremental = false);
143
 virtual ~Solver();
144
145
 // Problem specification:
146
 //
147
 Var newVar(bool polarity = true,
148
            bool dvar = true,
149
            bool isTheoryAtom = false,
150
            bool preRegister = false,
151
            bool canErase = true);  // Add a new variable with parameters
152
                                    // specifying variable mode.
153
9027
 Var trueVar() const { return varTrue; }
154
9027
 Var falseVar() const { return varFalse; }
155
156
 /** Retrive the SAT proof manager */
157
 CVC4::prop::SatProofManager* getProofManager();
158
159
 /** Retrive the refutation proof */
160
 std::shared_ptr<ProofNode> getProof();
161
162
 /** Is proof enabled? */
163
 bool isProofEnabled() const;
164
165
 // Less than for literals in a lemma
166
 struct lemma_lt
167
 {
168
   Solver& d_solver;
169
1378522
   lemma_lt(Solver& solver) : d_solver(solver) {}
170
15582826
   bool operator()(Lit x, Lit y)
171
   {
172
15582826
     lbool x_value = d_solver.value(x);
173
15582826
     lbool y_value = d_solver.value(y);
174
     // Two unassigned literals are sorted arbitrarily
175
15582826
     if (x_value == l_Undef && y_value == l_Undef)
176
     {
177
5141744
       return x < y;
178
     }
179
     // Unassigned literals are put to front
180
10441082
     if (x_value == l_Undef) return true;
181
10133090
     if (y_value == l_Undef) return false;
182
     // Literals of the same value are sorted by decreasing levels
183
10028893
     if (x_value == y_value)
184
     {
185
9757003
       return d_solver.trail_index(var(x)) > d_solver.trail_index(var(y));
186
     }
187
     else
188
     {
189
       // True literals go up front
190
271890
       if (x_value == l_True)
191
       {
192
20869
         return true;
193
       }
194
       else
195
       {
196
251021
         return false;
197
       }
198
     }
199
   }
200
 };
201
202
    // CVC4 context push/pop
203
    void          push                     ();
204
    void          pop                      ();
205
206
    /*
207
     * Reset the decisions in the DPLL(T) SAT solver at the current assertion
208
     * level.
209
     */
210
    void resetTrail();
211
    // addClause returns the ClauseId corresponding to the clause added in the
212
    // reference parameter id.
213
    bool    addClause (const vec<Lit>& ps, bool removable, ClauseId& id);  // Add a clause to the solver.
214
    bool    addEmptyClause(bool removable);                                // Add the empty clause, making the solver contradictory.
215
    bool    addClause (Lit p, bool removable, ClauseId& id);               // Add a unit clause to the solver.
216
    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id);        // Add a binary clause to the solver.
217
    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
218
    bool    addClause_(      vec<Lit>& ps, bool removable, ClauseId& id);  // Add a clause to the solver without making superflous internal copy. Will
219
                                                                                 // change the passed vector 'ps'.
220
221
    // Solving:
222
    //
223
    bool    simplify     ();                        // Removes already satisfied clauses.
224
    lbool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
225
    lbool   solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
226
    lbool    solve        ();                        // Search without assumptions.
227
    lbool    solve        (Lit p);                   // Search for a model that respects a single assumption.
228
    lbool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.
229
    lbool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
230
    bool    okay         () const;                  // FALSE means solver is in a conflicting state
231
232
    void toDimacs();
233
    void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
234
    void    toDimacs     (const char *file, const vec<Lit>& assumps);
235
    void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);
236
237
    // Convenience versions of 'toDimacs()':
238
    void    toDimacs     (const char* file);
239
    void    toDimacs     (const char* file, Lit p);
240
    void    toDimacs     (const char* file, Lit p, Lit q);
241
    void    toDimacs     (const char* file, Lit p, Lit q, Lit r);
242
243
    // Variable mode:
244
    //
245
    void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
246
    void    freezePolarity (Var v, bool b); // Declare which polarity the decision heuristic MUST ALWAYS use for a variable. Requires mode 'polarity_user'.
247
    void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
248
249
    // Read state:
250
    //
251
    lbool   value      (Var x) const;       // The current value of a variable.
252
    lbool   value      (Lit p) const;       // The current value of a literal.
253
    lbool   modelValue (Var x) const;       // The value of a variable in the last model. The last call to solve must have been satisfiable.
254
    lbool   modelValue (Lit p) const;       // The value of a literal in the last model. The last call to solve must have been satisfiable.
255
    int     nAssigns   ()      const;       // The current number of assigned literals.
256
    int     nClauses   ()      const;       // The current number of original clauses.
257
    int     nLearnts   ()      const;       // The current number of learnt clauses.
258
    int     nVars      ()      const;       // The current number of variables.
259
    int     nFreeVars  ()      const;
260
    bool    isDecision (Var x) const;       // is the given var a decision?
261
262
    // Debugging SMT explanations
263
    //
264
    bool    properExplanation(Lit l, Lit expl) const; // returns true if expl can be used to explain l---i.e., both assigned and trail_index(expl) < trail_index(l)
265
266
    // Resource contraints:
267
    //
268
    void    setConfBudget(int64_t x);
269
    void    setPropBudget(int64_t x);
270
    void    budgetOff();
271
    void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
272
    void    clearInterrupt();     // Clear interrupt indicator flag.
273
274
    // Memory managment:
275
    //
276
    virtual void garbageCollect();
277
    void    checkGarbage(double gf);
278
    void    checkGarbage();
279
280
    // Extra results: (read-only member variable)
281
    //
282
    vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
283
    vec<Lit> d_conflict;          // If problem is unsatisfiable (possibly under
284
                          // assumptions), this vector represent the final
285
                          // conflict clause expressed in the assumptions.
286
287
    // Mode of operation:
288
    //
289
    int       verbosity;
290
    double    var_decay;
291
    double    clause_decay;
292
    double    random_var_freq;
293
    double    random_seed;
294
    bool      luby_restart;
295
    int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
296
    int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
297
    bool      rnd_pol;            // Use random polarities for branching heuristics.
298
    bool      rnd_init_act;       // Initialize variable activities with a small random value.
299
    double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.
300
301
    int       restart_first;      // The initial restart limit.                                                                (default 100)
302
    double    restart_inc;        // The factor with which the restart limit is multiplied in each restart.                    (default 1.5)
303
    double    learntsize_factor;  // The intitial limit for learnt clauses is a factor of the original clauses.                (default 1 / 3)
304
    double    learntsize_inc;     // The limit for learnt clauses is multiplied with this factor each restart.                 (default 1.1)
305
306
    int       learntsize_adjust_start_confl;
307
    double    learntsize_adjust_inc;
308
309
    // Statistics: (read-only member variable)
310
    //
311
    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, resources_consumed;
312
    uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
313
314
protected:
315
316
    // Helper structures:
317
    //
318
    struct VarData {
319
      // Reason for the literal being in the trail
320
      CRef d_reason;
321
      // Sat level when the literal was added to the trail
322
      int d_level;
323
      // User level when the literal was added to the trail
324
      int d_user_level;
325
      // User level at which this literal was introduced
326
      int d_intro_level;
327
      // The index in the trail
328
      int d_trail_index;
329
330
52648542
      VarData(CRef reason,
331
              int level,
332
              int user_level,
333
              int intro_level,
334
              int trail_index)
335
52648542
          : d_reason(reason),
336
            d_level(level),
337
            d_user_level(user_level),
338
            d_intro_level(intro_level),
339
52648542
            d_trail_index(trail_index)
340
52648542
      {}
341
    };
342
343
    struct Watcher {
344
        CRef cref;
345
        Lit  blocker;
346
209360202
        Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
347
        bool operator==(const Watcher& w) const { return cref == w.cref; }
348
4997739
        bool operator!=(const Watcher& w) const { return cref != w.cref; }
349
    };
350
351
    struct WatcherDeleted
352
    {
353
        const ClauseAllocator& ca;
354
9027
        WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
355
14435245
        bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
356
    };
357
358
    struct VarOrderLt {
359
        const vec<double>&  activity;
360
88886598
        bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
361
9027
        VarOrderLt(const vec<double>&  act) : activity(act) { }
362
    };
363
364
    // Solver state:
365
    //
366
    bool                ok;                 // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
367
    vec<CRef>           clauses_persistent; // List of problem clauses.
368
    vec<CRef>           clauses_removable;  // List of learnt clauses.
369
    double              cla_inc;            // Amount to bump next clause with.
370
    vec<double>         activity;           // A heuristic measurement of the activity of a variable.
371
    double              var_inc;            // Amount to bump next variable with.
372
    OccLists<Lit, vec<Watcher>, WatcherDeleted>
373
                        watches;            // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
374
    vec<lbool>          assigns;            // The current assignments.
375
    vec<int>            assigns_lim;        // The size by levels of the current assignment
376
    vec<char>           polarity;           // The preferred polarity of each variable (bit 0) and whether it's locked (bit 1).
377
    vec<char>           decision;           // Declares if a variable is eligible for selection in the decision heuristic.
378
    vec<int>            flipped;            // Which trail_lim decisions have been flipped in this context.
379
    vec<Lit>            trail;              // Assignment stack; stores all assigments made in the order they were made.
380
    vec<int>            trail_lim;          // Separator indices for different decision levels in 'trail'.
381
    vec<bool>           trail_ok;           // Stack of "whether we're in conflict" flags.
382
    vec<VarData>        vardata;            // Stores reason and level for each variable.
383
    int                 qhead;              // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
384
    int                 simpDB_assigns;     // Number of top-level assignments since last execution of 'simplify()'.
385
    int64_t             simpDB_props;       // Remaining number of propagations that must be made before next execution of 'simplify()'.
386
    vec<Lit>            assumptions;        // Current set of assumptions provided to solve by the user.
387
    Heap<VarOrderLt>    order_heap;         // A priority queue of variables ordered with respect to the variable activity.
388
    double              progress_estimate;  // Set by 'search()'.
389
    bool                remove_satisfied;   // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
390
391
    ClauseAllocator     ca;
392
393
    // CVC4 Stuff
394
    /**
395
     * A vector determining whether each variable represents a theory atom.
396
     * More generally, this value is true for any literal that the theory proxy
397
     * should be notified about when asserted.
398
     */
399
    vec<bool> theory;
400
401
    enum TheoryCheckType {
402
      // Quick check, but don't perform theory reasoning
403
      CHECK_WITHOUT_THEORY,
404
      // Check and perform theory reasoning
405
      CHECK_WITH_THEORY,
406
      // The SAT abstraction of the problem is satisfiable, perform a full theory check
407
      CHECK_FINAL,
408
      // Perform a full theory check even if not done with everything
409
      CHECK_FINAL_FAKE
410
    };
411
412
    // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
413
    // used, exept 'seen' wich is used in several places.
414
    //
415
    vec<char>           seen;
416
    vec<Lit>            analyze_stack;
417
    vec<Lit>            analyze_toclear;
418
    vec<Lit>            add_tmp;
419
420
    double              max_learnts;
421
    double              learntsize_adjust_confl;
422
    int                 learntsize_adjust_cnt;
423
424
    // Resource contraints:
425
    //
426
    int64_t             conflict_budget;    // -1 means no budget.
427
    int64_t             propagation_budget; // -1 means no budget.
428
    bool                asynch_interrupt;
429
430
    // Main internal methods:
431
    //
432
    void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.
433
    Lit      pickBranchLit    ();                                                      // Return the next decision variable.
434
    void     newDecisionLevel ();                                                      // Begins a new decision level.
435
    void     uncheckedEnqueue (Lit p, CRef from = CRef_Undef);                         // Enqueue a literal. Assumes value of literal is undefined.
436
    bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.
437
    bool     theoryConflict;                                                           // Was the last conflict a theory conflict
438
    CRef     propagate        (TheoryCheckType type);                                  // Perform Boolean and Theory. Returns possibly conflicting clause.
439
    CRef     propagateBool    ();                                                      // Perform Boolean propagation. Returns possibly conflicting clause.
440
    void     propagateTheory  ();                                                      // Perform Theory propagation.
441
    void     theoryCheck      (CVC4::theory::Theory::Effort effort);                   // Perform a theory satisfiability check. Adds lemmas.
442
    CRef     updateLemmas     ();                                                      // Add the lemmas, backtraking if necessary and return a conflict if there is one
443
    void     cancelUntil      (int level);                                             // Backtrack until a certain level.
444
    int      analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)
445
    void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
446
    bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()') - true if p is redundant
447
    lbool    search           (int nof_conflicts);                                     // Search for a given number of conflicts.
448
    lbool    solve_           ();                                                      // Main solve method (assumptions given in 'assumptions').
449
    void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
450
    void     removeSatisfied  (vec<CRef>& cs);                                         // Shrink 'cs' to contain only non-satisfied clauses.
451
    void     rebuildOrderHeap ();
452
453
    // Maintaining Variable/Clause activity:
454
    //
455
    void     varDecayActivity ();                      // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
456
    void     varBumpActivity  (Var v, double inc);     // Increase a variable with the current 'bump' value.
457
    void     varBumpActivity  (Var v);                 // Increase a variable with the current 'bump' value.
458
    void     claDecayActivity ();                      // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
459
    void     claBumpActivity  (Clause& c);             // Increase a clause with the current 'bump' value.
460
461
    // Operations on clauses:
462
    //
463
    void     attachClause     (CRef cr);               // Attach a clause to watcher lists.
464
    void     detachClause     (CRef cr, bool strict = false); // Detach a clause to watcher lists.
465
    void     removeClause     (CRef cr);               // Detach and free a clause.
466
    bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
467
    bool     satisfied        (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
468
469
    void     relocAll         (ClauseAllocator& to);
470
471
    // Misc:
472
    //
473
    int      decisionLevel    ()      const; // Gives the current decisionlevel.
474
    uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
475
    CRef     reason           (Var x); // Get the reason of the variable (non const as it might create the explanation on the fly)
476
    bool     hasReasonClause  (Var x) const; // Does the variable have a reason
477
    bool     isPropagated     (Var x) const; // Does the variable have a propagated variables
478
    bool     isPropagatedBy   (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C
479
480
    int      level            (Var x) const;
481
    int      user_level       (Var x) const; // User level at which this variable was asserted
482
    int      intro_level      (Var x) const; // User level at which this variable was created
483
    int      trail_index      (Var x) const; // Index in the trail
484
    double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
485
public:
486
    bool     withinBudget     (uint64_t amount)      const;
487
    bool withinBudget(ResourceManager::Resource r) const;
488
489
   protected:
490
    // Static helpers:
491
    //
492
493
    // Returns a random float 0 <= x < 1. Seed must never be 0.
494
1883287
    static inline double drand(double& seed) {
495
1883287
        seed *= 1389796;
496
1883287
        int q = (int)(seed / 2147483647);
497
1883287
        seed -= (double)q * 2147483647;
498
1883287
        return seed / 2147483647; }
499
500
    // Returns a random integer 0 <= x < size. Seed must never be 0.
501
    static inline int irand(double& seed, int size) {
502
        return (int)(drand(seed) * size); }
503
504
};
505
506
507
508
//=================================================================================================
509
// Implementation of inline methods:
510
511
224618
inline bool Solver::hasReasonClause(Var x) const
512
{
513
224618
  return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy;
514
}
515
516
inline bool Solver::isPropagated(Var x) const
517
{
518
  return vardata[x].d_reason != CRef_Undef;
519
}
520
521
428435
inline bool Solver::isPropagatedBy(Var x, const Clause& c) const
522
{
523
744228
  return vardata[x].d_reason != CRef_Undef && vardata[x].d_reason != CRef_Lazy
524
732009
         && ca.lea(vardata[var(c[0])].d_reason) == &c;
525
}
526
527
209424
inline bool Solver::isDecision(Var x) const
528
{
529
418848
  Debug("minisat") << "var " << x << " is a decision iff "
530
418848
                   << (vardata[x].d_reason == CRef_Undef) << " && " << level(x)
531
209424
                   << " > 0" << std::endl;
532
209424
  return vardata[x].d_reason == CRef_Undef && level(x) > 0;
533
}
534
535
115088909
inline int Solver::level(Var x) const
536
{
537
115088909
  Assert(x < vardata.size());
538
115088909
  return vardata[x].d_level;
539
}
540
541
4328184
inline int Solver::user_level(Var x) const
542
{
543
4328184
  Assert(x < vardata.size());
544
4328184
  return vardata[x].d_user_level;
545
}
546
547
60924269
inline int Solver::intro_level(Var x) const
548
{
549
60924269
  Assert(x < vardata.size());
550
60924269
  return vardata[x].d_intro_level;
551
}
552
553
20434683
inline int Solver::trail_index(Var x) const
554
{
555
20434683
  Assert(x < vardata.size());
556
20434683
  return vardata[x].d_trail_index;
557
}
558
559
52211880
inline void Solver::insertVarOrder(Var x) {
560
52211880
  Assert(x < vardata.size());
561
52211880
  if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x);
562
52211880
}
563
564
260110
inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
565
14251469
inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
566
14251469
inline void Solver::varBumpActivity(Var v, double inc) {
567
14251469
    if ( (activity[v] += inc) > 1e100 ) {
568
        // Rescale:
569
31144
        for (int i = 0; i < nVars(); i++)
570
31123
            activity[i] *= 1e-100;
571
21
        var_inc *= 1e-100; }
572
573
    // Update order_heap with respect to new activity:
574
14251469
    if (order_heap.inHeap(v))
575
10147614
        order_heap.decrease(v); }
576
577
260110
inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
578
1965210
inline void Solver::claBumpActivity (Clause& c) {
579
1965210
        if ( (c.activity() += cla_inc) > 1e20 ) {
580
            // Rescale:
581
41321
            for (int i = 0; i < clauses_removable.size(); i++)
582
41320
                ca[clauses_removable[i]].activity() *= 1e-20;
583
1
            cla_inc *= 1e-20; } }
584
585
31693
inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
586
144890
inline void Solver::checkGarbage(double gf){
587
144890
    if (ca.wasted() > ca.size() * gf)
588
3102
        garbageCollect(); }
589
590
// NOTE: enqueue does not set the ok flag! (only public methods do)
591
9156
inline bool     Solver::enqueue         (Lit p, CRef from)      { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
592
79083
inline bool     Solver::addClause       (const vec<Lit>& ps, bool removable, ClauseId& id)
593
79083
                                                                { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
594
inline bool     Solver::addEmptyClause  (bool removable)        { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, removable, tmp); }
595
inline bool     Solver::addClause       (Lit p, bool removable, ClauseId& id)
596
                                                                { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
597
inline bool     Solver::addClause       (Lit p, Lit q, bool removable, ClauseId& id)
598
                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
599
inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
600
                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
601
1471902
inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
602
2492803
inline void Solver::newDecisionLevel()
603
{
604
2492803
  trail_lim.push(trail.size());
605
2492803
  flipped.push(false);
606
2492803
  d_context->push();
607
2492803
}
608
609
75571694
inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
610
21843374
inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
611
9453140
inline lbool Solver::value(Var x) const
612
{
613
9453140
  Assert(x < nVars());
614
9453140
  return assigns[x];
615
}
616
1367836298
inline lbool Solver::value(Lit p) const
617
{
618
1367836298
  Assert(var(p) < nVars());
619
1367836298
  return assigns[var(p)] ^ sign(p);
620
}
621
inline lbool    Solver::modelValue    (Var x) const   { return model[x]; }
622
50418
inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
623
2616508
inline int      Solver::nAssigns      ()      const   { return trail.size(); }
624
10608
inline int      Solver::nClauses      ()      const   { return clauses_persistent.size(); }
625
inline int      Solver::nLearnts      ()      const   { return clauses_removable.size(); }
626
1441511313
inline int      Solver::nVars         ()      const   { return vardata.size(); }
627
inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
628
inline bool     Solver::properExplanation(Lit l, Lit expl) const { return value(l) == l_True && value(expl) == l_True && trail_index(var(expl)) < trail_index(var(l)); }
629
inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
630
82860
inline void     Solver::freezePolarity(Var v, bool b) { polarity[v] = int(b) | 0x2; }
631
827462
inline void     Solver::setDecisionVar(Var v, bool b)
632
{
633
827462
    if      ( b && !decision[v] ) dec_vars++;
634
37088
    else if (!b &&  decision[v] ) dec_vars--;
635
636
827462
    decision[v] = b;
637
827462
    insertVarOrder(v);
638
827462
}
639
640
inline void     Solver::setConfBudget(int64_t x){ conflict_budget    = conflicts    + x; }
641
inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
642
inline void     Solver::interrupt(){ asynch_interrupt = true; }
643
12396
inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
644
24834
inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
645
646
inline lbool     Solver::solve         ()                    { budgetOff(); assumptions.clear(); return solve_(); }
647
inline lbool     Solver::solve         (Lit p)               { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(); }
648
inline lbool     Solver::solve         (Lit p, Lit q)        { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(); }
649
inline lbool     Solver::solve         (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(); }
650
inline lbool     Solver::solve         (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_(); }
651
inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
652
2039268
inline bool     Solver::okay          ()      const   { return ok; }
653
654
inline void     Solver::toDimacs     () { vec<Lit> as; toDimacs(stdout, as); }
655
inline void     Solver::toDimacs     (const char* file){ vec<Lit> as; toDimacs(file, as); }
656
inline void     Solver::toDimacs     (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
657
inline void     Solver::toDimacs     (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
658
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); }
659
660
661
662
//=================================================================================================
663
// Debug etc:
664
665
666
//=================================================================================================
667
} /* CVC4::Minisat namespace */
668
} /* CVC4 namespace */
669
670
#endif