glucose-syrup/core/Solver.h

   1 /***************************************************************************************[Solver.h]
   2  Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon
   3                                 CRIL - Univ. Artois, France
   4                                 LRI  - Univ. Paris Sud, France (2009-2013)
   5                                 Labri - Univ. Bordeaux, France
   6
   7  Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
   8                                 CRIL - Univ. Artois, France
   9                                 Labri - Univ. Bordeaux, France
  10
  11 Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of
  12 Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it
  13 is based on. (see below).
  14
  15 Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
  16 version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
  17 without restriction, including the rights to use, copy, modify, merge, publish, distribute,
  18 sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is
  19 furnished to do so, subject to the following conditions:
  20
  21 - The above and below copyrights notices and this permission notice shall be included in all
  22 copies or substantial portions of the Software;
  23 - The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
  24 be used in any competitive event (sat competitions/evaluations) without the express permission of
  25 the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
  26 using Glucose Parallel as an embedded SAT engine (single core or not).
  27
  28
  29 --------------- Original Minisat Copyrights
  30
  31 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  32 Copyright (c) 2007-2010, Niklas Sorensson
  33
  34 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
  35 associated documentation files (the "Software"), to deal in the Software without restriction,
  36 including without limitation the rights to use, copy, modify, merge, publish, distribute,
  37 sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
  38 furnished to do so, subject to the following conditions:
  39
  40 The above copyright notice and this permission notice shall be included in all copies or
  41 substantial portions of the Software.
  42
  43 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
  44 NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
  45 NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
  46 DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
  47 OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
  48  **************************************************************************************************/
  49
  50 #ifndef Glucose_Solver_h
  51 #define Glucose_Solver_h
  52
  53 #include "mtl/Heap.h"
  54 #include "mtl/Alg.h"
  55 #include "utils/Options.h"
  56 #include "core/SolverTypes.h"
  57 #include "core/BoundedQueue.h"
  58 #include "core/Constants.h"
  59 #include "mtl/Clone.h"
  60
  61
  62 namespace Glucose {
  63
  64 //=================================================================================================
  65 // Solver -- the main class:
  66
  67 class Solver : public Clone {
  68
  69     friend class SolverConfiguration;
  70
  71 public:
  72
  73     // Constructor/Destructor:
  74     //
  75     Solver();
  76     Solver(const  Solver &s);
  77
  78     virtual ~Solver();
  79
  80     /**
  81      * Clone function
  82      */
  83     virtual Clone* clone() const {
  84         return  new Solver(*this);
  85     }
  86
  87     // Problem specification:
  88     //
  89     virtual Var     newVar    (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode.
  90     bool    addClause (const vec<Lit>& ps);                     // Add a clause to the solver.
  91     bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
  92     bool    addClause (Lit p);                                  // Add a unit clause to the solver.
  93     bool    addClause (Lit p, Lit q);                           // Add a binary clause to the solver.
  94     bool    addClause (Lit p, Lit q, Lit r);                    // Add a ternary clause to the solver.
  95     virtual bool    addClause_(      vec<Lit>& ps);                     // Add a clause to the solver without making superflous internal copy. Will
  96                                                                 // change the passed vector 'ps'.
  97
  98     // Solving:
  99     //
 100     bool    simplify     ();                        // Removes already satisfied clauses.
 101     bool    solve        (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions.
 102     lbool   solveLimited (const vec<Lit>& assumps); // Search for a model that respects a given set of assumptions (With resource constraints).
 103     bool    solve        ();                        // Search without assumptions.
 104     bool    solve        (Lit p);                   // Search for a model that respects a single assumption.
 105     bool    solve        (Lit p, Lit q);            // Search for a model that respects two assumptions.
 106     bool    solve        (Lit p, Lit q, Lit r);     // Search for a model that respects three assumptions.
 107     bool    okay         () const;                  // FALSE means solver is in a conflicting state
 108
 109        // Convenience versions of 'toDimacs()':
 110     void    toDimacs     (FILE* f, const vec<Lit>& assumps);            // Write CNF to file in DIMACS-format.
 111     void    toDimacs     (const char *file, const vec<Lit>& assumps);
 112     void    toDimacs     (FILE* f, Clause& c, vec<Var>& map, Var& max);
 113     void    toDimacs     (const char* file);
 114     void    toDimacs     (const char* file, Lit p);
 115     void    toDimacs     (const char* file, Lit p, Lit q);
 116     void    toDimacs     (const char* file, Lit p, Lit q, Lit r);
 117
 118     // Display clauses and literals
 119     void printLit(Lit l);
 120     void printClause(CRef c);
 121     void printInitialClause(CRef c);
 122
 123     // Variable mode:
 124     //
 125     void    setPolarity    (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
 126     void    setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
 127
 128     // Read state:
 129     //
 130     lbool   value      (Var x) const;       // The current value of a variable.
 131     lbool   value      (Lit p) const;       // The current value of a literal.
 132     lbool   modelValue (Var x) const;       // The value of a variable in the last model. The last call to solve must have been satisfiable.
 133     lbool   modelValue (Lit p) const;       // The value of a literal in the last model. The last call to solve must have been satisfiable.
 134     int     nAssigns   ()      const;       // The current number of assigned literals.
 135     int     nClauses   ()      const;       // The current number of original clauses.
 136     int     nLearnts   ()      const;       // The current number of learnt clauses.
 137     int     nVars      ()      const;       // The current number of variables.
 138     int     nFreeVars  ()      const;
 139
 140     inline char valuePhase(Var v) {return polarity[v];}
 141
 142     // Incremental mode
 143     void setIncrementalMode();
 144     void initNbInitialVars(int nb);
 145     void printIncrementalStats();
 146     bool isIncremental();
 147     // Resource contraints:
 148     //
 149     void    setConfBudget(int64_t x);
 150     void    setPropBudget(int64_t x);
 151     void    budgetOff();
 152     void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
 153     void    clearInterrupt();     // Clear interrupt indicator flag.
 154
 155     // Memory managment:
 156     //
 157     virtual void garbageCollect();
 158     void    checkGarbage(double gf);
 159     void    checkGarbage();
 160
 161     // Extra results: (read-only member variable)
 162     //
 163     vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
 164     vec<Lit>   conflict;          // If problem is unsatisfiable (possibly under assumptions),
 165                                   // this vector represent the final conflict clause expressed in the assumptions.
 166
 167     // Mode of operation:
 168     //
 169     int       verbosity;
 170     int       verbEveryConflicts;
 171     int       showModel;
 172
 173     // Constants For restarts
 174     double    K;
 175     double    R;
 176     double    sizeLBDQueue;
 177     double    sizeTrailQueue;
 178
 179     // Constants for reduce DB
 180     int          firstReduceDB;
 181     int          incReduceDB;
 182     int          specialIncReduceDB;
 183     unsigned int lbLBDFrozenClause;
 184
 185     // Constant for reducing clause
 186     int          lbSizeMinimizingClause;
 187     unsigned int lbLBDMinimizingClause;
 188
 189     // Constant for heuristic
 190     double    var_decay;
 191     double    max_var_decay;
 192     double    clause_decay;
 193     double    random_var_freq;
 194     double    random_seed;
 195     int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
 196     int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
 197     bool      rnd_pol;            // Use random polarities for branching heuristics.
 198     bool      rnd_init_act;       // Initialize variable activities with a small random value.
 199
 200     // Constant for Memory managment
 201     double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.
 202
 203     // Certified UNSAT ( Thanks to Marijn Heule)
 204     FILE*               certifiedOutput;
 205     bool                certifiedUNSAT;
 206
 207     // Panic mode.
 208     // Save memory
 209     uint32_t panicModeLastRemoved, panicModeLastRemovedShared;
 210
 211     bool useUnaryWatched;            // Enable unary watched literals
 212     bool promoteOneWatchedClause;    // One watched clauses are promotted to two watched clauses if found empty
 213
 214     // Functions useful for multithread solving
 215     // Useless in the sequential case
 216     // Overide in ParallelSolver
 217     virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl);
 218     virtual bool parallelImportClauses(); // true if the empty clause was received
 219     virtual void parallelImportUnaryClauses();
 220     virtual void parallelExportUnaryClause(Lit p);
 221     virtual void parallelExportClauseDuringSearch(Clause &c);
 222     virtual bool parallelJobIsFinished();
 223     virtual bool panicModeIsEnabled();
 224
 225
 226
 227     // Statistics: (read-only member variable)
 228     uint64_t    nbPromoted;          // Number of clauses from unary to binary watch scheme
 229     uint64_t    originalClausesSeen; // Number of original clauses seen
 230     uint64_t    sumDecisionLevels;
 231     //
 232     uint64_t nbRemovedClauses,nbRemovedUnaryWatchedClauses, nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart;
 233     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
 234
 235 protected:
 236
 237     long curRestart;
 238     // Helper structures:
 239     //
 240     struct VarData { CRef reason; int level; };
 241     static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
 242
 243     struct Watcher {
 244         CRef cref;
 245         Lit  blocker;
 246         Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
 247         bool operator==(const Watcher& w) const { return cref == w.cref; }
 248         bool operator!=(const Watcher& w) const { return cref != w.cref; }
 249 /*        Watcher &operator=(Watcher w) {
 250             this->cref = w.cref;
 251             this->blocker = w.blocker;
 252             return *this;
 253         }
 254 */
 255     };
 256
 257     struct WatcherDeleted
 258     {
 259         const ClauseAllocator& ca;
 260         WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
 261         bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
 262     };
 263
 264     struct VarOrderLt {
 265         const vec<double>&  activity;
 266         bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
 267         VarOrderLt(const vec<double>&  act) : activity(act) { }
 268     };
 269
 270
 271     // Solver state:
 272     //
 273     int                lastIndexRed;
 274     bool                ok;               // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
 275     double              cla_inc;          // Amount to bump next clause with.
 276     vec<double>         activity;         // A heuristic measurement of the activity of a variable.
 277     double              var_inc;          // Amount to bump next variable with.
 278     OccLists<Lit, vec<Watcher>, WatcherDeleted>
 279                         watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
 280     OccLists<Lit, vec<Watcher>, WatcherDeleted>
 281                         watchesBin;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
 282     OccLists<Lit, vec<Watcher>, WatcherDeleted>
 283                         unaryWatches;       //  Unary watch scheme (clauses are seen when they become empty
 284     vec<CRef>           clauses;          // List of problem clauses.
 285     vec<CRef>           learnts;          // List of learnt clauses.
 286     vec<CRef>           unaryWatchedClauses;  // List of imported clauses (after the purgatory) // TODO put inside ParallelSolver
 287
 288     vec<lbool>          assigns;          // The current assignments.
 289     vec<char>           polarity;         // The preferred polarity of each variable.
 290     vec<char>           decision;         // Declares if a variable is eligible for selection in the decision heuristic.
 291     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
 292     vec<int>            nbpos;
 293     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
 294     vec<VarData>        vardata;          // Stores reason and level for each variable.
 295     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
 296     int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.
 297     int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
 298     vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
 299     Heap<VarOrderLt>    order_heap;       // A priority queue of variables ordered with respect to the variable activity.
 300     double              progress_estimate;// Set by 'search()'.
 301     bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
 302     bool reduceOnSize;
 303     int  reduceOnSizeSize;                // See XMinisat paper
 304     vec<unsigned int>   permDiff;           // permDiff[var] contains the current conflict number... Used to count the number of  LBD
 305
 306
 307     // UPDATEVARACTIVITY trick (see competition'09 companion paper)
 308     vec<Lit> lastDecisionLevel;
 309
 310     ClauseAllocator     ca;
 311
 312     int nbclausesbeforereduce;            // To know when it is time to reduce clause database
 313
 314     // Used for restart strategies
 315     bqueue<unsigned int> trailQueue,lbdQueue; // Bounded queues for restarts.
 316     float sumLBD; // used to compute the global average of LBD. Restarts...
 317     int sumAssumptions;
 318     CRef lastLearntClause;
 319
 320
 321     // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
 322     // used, exept 'seen' wich is used in several places.
 323     //
 324     vec<char>           seen;
 325     vec<Lit>            analyze_stack;
 326     vec<Lit>            analyze_toclear;
 327     vec<Lit>            add_tmp;
 328     unsigned int  MYFLAG;
 329
 330     // Initial reduceDB strategy
 331     double              max_learnts;
 332     double              learntsize_adjust_confl;
 333     int                 learntsize_adjust_cnt;
 334
 335     // Resource contraints:
 336     //
 337     int64_t             conflict_budget;    // -1 means no budget.
 338     int64_t             propagation_budget; // -1 means no budget.
 339     bool                asynch_interrupt;
 340
 341     // Variables added for incremental mode
 342     int incremental; // Use incremental SAT Solver
 343     int nbVarsInitialFormula; // nb VAR in formula without assumptions (incremental SAT)
 344     double totalTime4Sat,totalTime4Unsat;
 345     int nbSatCalls,nbUnsatCalls;
 346     vec<int> assumptionPositions,initialPositions;
 347
 348
 349     // Main internal methods:
 350     //
 351     void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.
 352     Lit      pickBranchLit    ();                                                      // Return the next decision variable.
 353     void     newDecisionLevel ();                                                      // Begins a new decision level.
 354     void     uncheckedEnqueue (Lit p, CRef from = CRef_Undef);                         // Enqueue a literal. Assumes value of literal is undefined.
 355     bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.
 356     CRef     propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
 357     CRef     propagateUnaryWatches(Lit p);                                                  // Perform propagation on unary watches of p, can find only conflicts
 358     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
 359     void     analyze          (CRef confl, vec<Lit>& out_learnt, vec<Lit> & selectors, int& out_btlevel,unsigned int &nblevels,unsigned int &szWithoutSelectors);    // (bt = backtrack)
 360     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
 361     bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
 362     lbool    search           (int nof_conflicts);                                     // Search for a given number of conflicts.
 363     virtual lbool    solve_           (bool do_simp = true, bool turn_off_simp = false);                                                      // Main solve method (assumptions given in 'assumptions').
 364     virtual void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
 365     void     removeSatisfied  (vec<CRef>& cs);                                         // Shrink 'cs' to contain only non-satisfied clauses.
 366     void     rebuildOrderHeap ();
 367
 368     // Maintaining Variable/Clause activity:
 369     //
 370     void     varDecayActivity ();                      // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
 371     void     varBumpActivity  (Var v, double inc);     // Increase a variable with the current 'bump' value.
 372     void     varBumpActivity  (Var v);                 // Increase a variable with the current 'bump' value.
 373     void     claDecayActivity ();                      // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
 374     void     claBumpActivity  (Clause& c);             // Increase a clause with the current 'bump' value.
 375
 376     // Operations on clauses:
 377     //
 378     void     attachClause     (CRef cr);               // Attach a clause to watcher lists.
 379     void     detachClause     (CRef cr, bool strict = false); // Detach a clause to watcher lists.
 380     void     detachClausePurgatory(CRef cr, bool strict = false);
 381     void     attachClausePurgatory(CRef cr);
 382     void     removeClause     (CRef cr, bool inPurgatory = false);               // Detach and free a clause.
 383     bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
 384     bool     satisfied        (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
 385
 386     unsigned int computeLBD(const vec<Lit> & lits,int end=-1);
 387     unsigned int computeLBD(const Clause &c);
 388     void minimisationWithBinaryResolution(vec<Lit> &out_learnt);
 389
 390     virtual void     relocAll         (ClauseAllocator& to);
 391
 392     // Misc:
 393     //
 394     int      decisionLevel    ()      const; // Gives the current decisionlevel.
 395     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
 396     CRef     reason           (Var x) const;
 397     int      level            (Var x) const;
 398     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 399     bool     withinBudget     ()      const;
 400     inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
 401
 402     // Static helpers:
 403     //
 404
 405     // Returns a random float 0 <= x < 1. Seed must never be 0.
 406     static inline double drand(double& seed) {
 407         seed *= 1389796;
 408         int q = (int)(seed / 2147483647);
 409         seed -= (double)q * 2147483647;
 410         return seed / 2147483647; }
 411
 412     // Returns a random integer 0 <= x < size. Seed must never be 0.
 413     static inline int irand(double& seed, int size) {
 414         return (int)(drand(seed) * size); }
 415 };
 416
 417
 418 //=================================================================================================
 419 // Implementation of inline methods:
 420
 421 inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
 422 inline int  Solver::level (Var x) const { return vardata[x].level; }
 423
 424 inline void Solver::insertVarOrder(Var x) {
 425     if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
 426
 427 inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
 428 inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
 429 inline void Solver::varBumpActivity(Var v, double inc) {
 430     if ( (activity[v] += inc) > 1e100 ) {
 431         // Rescale:
 432         for (int i = 0; i < nVars(); i++)
 433             activity[i] *= 1e-100;
 434         var_inc *= 1e-100; }
 435
 436     // Update order_heap with respect to new activity:
 437     if (order_heap.inHeap(v))
 438         order_heap.decrease(v); }
 439
 440 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
 441 inline void Solver::claBumpActivity (Clause& c) {
 442         if ( (c.activity() += cla_inc) > 1e20 ) {
 443             // Rescale:
 444             for (int i = 0; i < learnts.size(); i++)
 445                 ca[learnts[i]].activity() *= 1e-20;
 446             cla_inc *= 1e-20; } }
 447
 448 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
 449 inline void Solver::checkGarbage(double gf){
 450     if (ca.wasted() > ca.size() * gf)
 451         garbageCollect(); }
 452
 453 // NOTE: enqueue does not set the ok flag! (only public methods do)
 454 inline bool     Solver::enqueue         (Lit p, CRef from)      { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
 455 inline bool     Solver::addClause       (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
 456 inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(); return addClause_(add_tmp); }
 457 inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
 458 inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
 459 inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
 460  inline bool     Solver::locked          (const Clause& c) const {
 461    if(c.size()>2)
 462      return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c;
 463    return
 464      (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
 465      ||
 466      (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
 467  }
 468 inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
 469
 470 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 471 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
 472 inline lbool    Solver::value         (Var x) const   { return assigns[x]; }
 473 inline lbool    Solver::value         (Lit p) const   { return assigns[var(p)] ^ sign(p); }
 474 inline lbool    Solver::modelValue    (Var x) const   { return model[x]; }
 475 inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
 476 inline int      Solver::nAssigns      ()      const   { return trail.size(); }
 477 inline int      Solver::nClauses      ()      const   { return clauses.size(); }
 478 inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
 479 inline int      Solver::nVars         ()      const   { return vardata.size(); }
 480 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 481 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 482 inline void     Solver::setDecisionVar(Var v, bool b)
 483 {
 484     if      ( b && !decision[v]) dec_vars++;
 485     else if (!b &&  decision[v]) dec_vars--;
 486
 487     decision[v] = b;
 488     insertVarOrder(v);
 489 }
 490 inline void     Solver::setConfBudget(int64_t x){ conflict_budget    = conflicts    + x; }
 491 inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
 492 inline void     Solver::interrupt(){ asynch_interrupt = true; }
 493 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 494 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
 495 inline bool     Solver::withinBudget() const {
 496     return !asynch_interrupt &&
 497            (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
 498            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
 499
 500 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
 501 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
 502 // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
 503 inline bool     Solver::solve         ()                    { budgetOff(); assumptions.clear(); return solve_() == l_True; }
 504 inline bool     Solver::solve         (Lit p)               { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
 505 inline bool     Solver::solve         (Lit p, Lit q)        { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
 506 inline bool     Solver::solve         (Lit p, Lit q, Lit r) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }
 507 inline bool     Solver::solve         (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
 508 inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
 509 inline bool     Solver::okay          ()      const   { return ok; }
 510
 511 inline void     Solver::toDimacs     (const char* file){ vec<Lit> as; toDimacs(file, as); }
 512 inline void     Solver::toDimacs     (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
 513 inline void     Solver::toDimacs     (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
 514 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); }
 515
 516
 517
 518 //=================================================================================================
 519 // Debug etc:
 520
 521
 522 inline void Solver::printLit(Lit l)
 523 {
 524     printf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
 525 }
 526
 527
 528 inline void Solver::printClause(CRef cr)
 529 {
 530   Clause &c = ca[cr];
 531     for (int i = 0; i < c.size(); i++){
 532         printLit(c[i]);
 533         printf(" ");
 534     }
 535 }
 536
 537 inline void Solver::printInitialClause(CRef cr)
 538 {
 539   Clause &c = ca[cr];
 540     for (int i = 0; i < c.size(); i++){
 541       if(!isSelector(var(c[i]))) {
 542         printLit(c[i]);
 543         printf(" ");
 544       }
 545     }
 546 }
 547
 548 //=================================================================================================
 549
 550 struct reduceDB_lt {
 551     ClauseAllocator& ca;
 552
 553     reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {
 554     }
 555
 556     bool operator()(CRef x, CRef y) {
 557
 558         // Main criteria... Like in MiniSat we keep all binary clauses
 559         if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
 560
 561         if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
 562         if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
 563
 564         // Second one  based on literal block distance
 565         if (ca[x].lbd() > ca[y].lbd()) return 1;
 566         if (ca[x].lbd() < ca[y].lbd()) return 0;
 567
 568
 569         // Finally we can use old activity or size, we choose the last one
 570         return ca[x].activity() < ca[y].activity();
 571         //return x->size() < y->size();
 572
 573         //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
 574     }
 575 };
 576
 577
 578 }
 579
 580
 581 #endif