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     assumptionsSize      ()      const;       // The current number of variables.
 139     int     nFreeVars  ()      const;
 140
 141     inline char valuePhase(Var v) {return polarity[v];}
 142
 143     // Incremental mode
 144     void setIncrementalMode();
 145     void initNbInitialVars(int nb);
 146     void printIncrementalStats();
 147     bool isIncremental();
 148     // Resource contraints:
 149     //
 150     void    setConfBudget(int64_t x);
 151     void    setPropBudget(int64_t x);
 152     void    budgetOff();
 153     void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
 154     void    clearInterrupt();     // Clear interrupt indicator flag.
 155
 156     // Memory managment:
 157     //
 158     virtual void garbageCollect();
 159     void    checkGarbage(double gf);
 160     void    checkGarbage();
 161
 162     // Extra results: (read-only member variable)
 163     //
 164     vec<lbool> model;             // If problem is satisfiable, this vector contains the model (if any).
 165     vec<Lit>   conflict;          // If problem is unsatisfiable (possibly under assumptions),
 166                                   // this vector represent the final conflict clause expressed in the assumptions.
 167
 168     // Mode of operation:
 169     //
 170     int       verbosity;
 171     int       verbEveryConflicts;
 172     int       showModel;
 173
 174     // Constants For restarts
 175     double    K;
 176     double    R;
 177     double    sizeLBDQueue;
 178     double    sizeTrailQueue;
 179
 180     // Constants for reduce DB
 181     int          firstReduceDB;
 182     int          incReduceDB;
 183     int          specialIncReduceDB;
 184     unsigned int lbLBDFrozenClause;
 185
 186     // Constant for reducing clause
 187     int          lbSizeMinimizingClause;
 188     unsigned int lbLBDMinimizingClause;
 189
 190     // Constant for heuristic
 191     double    var_decay;
 192     double    max_var_decay;
 193     double    clause_decay;
 194     double    random_var_freq;
 195     double    random_seed;
 196     int       ccmin_mode;         // Controls conflict clause minimization (0=none, 1=basic, 2=deep).
 197     int       phase_saving;       // Controls the level of phase saving (0=none, 1=limited, 2=full).
 198     bool      rnd_pol;            // Use random polarities for branching heuristics.
 199     bool      rnd_init_act;       // Initialize variable activities with a small random value.
 200
 201     // Constant for Memory managment
 202     double    garbage_frac;       // The fraction of wasted memory allowed before a garbage collection is triggered.
 203
 204     // Certified UNSAT ( Thanks to Marijn Heule)
 205     FILE*               certifiedOutput;
 206     bool                certifiedUNSAT;
 207
 208     // Panic mode.
 209     // Save memory
 210     uint32_t panicModeLastRemoved, panicModeLastRemovedShared;
 211
 212     bool useUnaryWatched;            // Enable unary watched literals
 213     bool promoteOneWatchedClause;    // One watched clauses are promotted to two watched clauses if found empty
 214
 215     // Functions useful for multithread solving
 216     // Useless in the sequential case
 217     // Overide in ParallelSolver
 218     virtual void parallelImportClauseDuringConflictAnalysis(Clause &c,CRef confl);
 219     virtual bool parallelImportClauses(); // true if the empty clause was received
 220     virtual void parallelImportUnaryClauses();
 221     virtual void parallelExportUnaryClause(Lit p);
 222     virtual void parallelExportClauseDuringSearch(Clause &c);
 223     virtual bool parallelJobIsFinished();
 224     virtual bool panicModeIsEnabled();
 225
 226
 227
 228     // Statistics: (read-only member variable)
 229     uint64_t    nbPromoted;          // Number of clauses from unary to binary watch scheme
 230     uint64_t    originalClausesSeen; // Number of original clauses seen
 231     uint64_t    sumDecisionLevels;
 232     //
 233     uint64_t nbRemovedClauses,nbRemovedUnaryWatchedClauses, nbReducedClauses,nbDL2,nbBin,nbUn,nbReduceDB,solves, starts, decisions, rnd_decisions, propagations, conflicts,conflictsRestarts,nbstopsrestarts,nbstopsrestartssame,lastblockatrestart;
 234     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
 235
 236 protected:
 237
 238     long curRestart;
 239     // Helper structures:
 240     //
 241     struct VarData { CRef reason; int level; };
 242     static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
 243
 244     struct Watcher {
 245         CRef cref;
 246         Lit  blocker;
 247         Watcher(CRef cr, Lit p) : cref(cr), blocker(p) {}
 248         bool operator==(const Watcher& w) const { return cref == w.cref; }
 249         bool operator!=(const Watcher& w) const { return cref != w.cref; }
 250 /*        Watcher &operator=(Watcher w) {
 251             this->cref = w.cref;
 252             this->blocker = w.blocker;
 253             return *this;
 254         }
 255 */
 256     };
 257
 258     struct WatcherDeleted
 259     {
 260         const ClauseAllocator& ca;
 261         WatcherDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
 262         bool operator()(const Watcher& w) const { return ca[w.cref].mark() == 1; }
 263     };
 264
 265     struct VarOrderLt {
 266         const vec<double>&  activity;
 267         bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
 268         VarOrderLt(const vec<double>&  act) : activity(act) { }
 269     };
 270
 271
 272     // Solver state:
 273     //
 274     int                lastIndexRed;
 275     bool                ok;               // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
 276     double              cla_inc;          // Amount to bump next clause with.
 277     vec<double>         activity;         // A heuristic measurement of the activity of a variable.
 278     double              var_inc;          // Amount to bump next variable with.
 279     OccLists<Lit, vec<Watcher>, WatcherDeleted>
 280                         watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
 281     OccLists<Lit, vec<Watcher>, WatcherDeleted>
 282                         watchesBin;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
 283     OccLists<Lit, vec<Watcher>, WatcherDeleted>
 284                         unaryWatches;       //  Unary watch scheme (clauses are seen when they become empty
 285     vec<CRef>           clauses;          // List of problem clauses.
 286     vec<CRef>           learnts;          // List of learnt clauses.
 287     vec<CRef>           unaryWatchedClauses;  // List of imported clauses (after the purgatory) // TODO put inside ParallelSolver
 288
 289     vec<lbool>          assigns;          // The current assignments.
 290     vec<char>           polarity;         // The preferred polarity of each variable.
 291     vec<char>           decision;         // Declares if a variable is eligible for selection in the decision heuristic.
 292     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
 293     vec<int>            nbpos;
 294     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
 295     vec<VarData>        vardata;          // Stores reason and level for each variable.
 296     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
 297     int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.
 298     int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
 299     vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
 300     Heap<VarOrderLt>    order_heap;       // A priority queue of variables ordered with respect to the variable activity.
 301     double              progress_estimate;// Set by 'search()'.
 302     bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
 303     bool reduceOnSize;
 304     int  reduceOnSizeSize;                // See XMinisat paper
 305     vec<unsigned int>   permDiff;           // permDiff[var] contains the current conflict number... Used to count the number of  LBD
 306
 307
 308     // UPDATEVARACTIVITY trick (see competition'09 companion paper)
 309     vec<Lit> lastDecisionLevel;
 310
 311     ClauseAllocator     ca;
 312
 313     int nbclausesbeforereduce;            // To know when it is time to reduce clause database
 314
 315     // Used for restart strategies
 316     bqueue<unsigned int> trailQueue,lbdQueue; // Bounded queues for restarts.
 317     float sumLBD; // used to compute the global average of LBD. Restarts...
 318     int sumAssumptions;
 319     CRef lastLearntClause;
 320
 321
 322     // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
 323     // used, exept 'seen' wich is used in several places.
 324     //
 325     vec<char>           seen;
 326     vec<Lit>            analyze_stack;
 327     vec<Lit>            analyze_toclear;
 328     vec<Lit>            add_tmp;
 329     unsigned int  MYFLAG;
 330
 331     // Initial reduceDB strategy
 332     double              max_learnts;
 333     double              learntsize_adjust_confl;
 334     int                 learntsize_adjust_cnt;
 335
 336     // Resource contraints:
 337     //
 338     int64_t             conflict_budget;    // -1 means no budget.
 339     int64_t             propagation_budget; // -1 means no budget.
 340     bool                asynch_interrupt;
 341
 342     // Variables added for incremental mode
 343     int incremental; // Use incremental SAT Solver
 344     int nbVarsInitialFormula; // nb VAR in formula without assumptions (incremental SAT)
 345     double totalTime4Sat,totalTime4Unsat;
 346     int nbSatCalls,nbUnsatCalls;
 347     vec<int> assumptionPositions,initialPositions;
 348
 349
 350     // Main internal methods:
 351     //
 352     void     insertVarOrder   (Var x);                                                 // Insert a variable in the decision order priority queue.
 353     Lit      pickBranchLit    ();                                                      // Return the next decision variable.
 354     void     newDecisionLevel ();                                                      // Begins a new decision level.
 355     void     uncheckedEnqueue (Lit p, CRef from = CRef_Undef);                         // Enqueue a literal. Assumes value of literal is undefined.
 356     bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.
 357     CRef     propagate        ();                                                      // Perform unit propagation. Returns possibly conflicting clause.
 358     CRef     propagateUnaryWatches(Lit p);                                                  // Perform propagation on unary watches of p, can find only conflicts
 359     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
 360     void     analyze          (CRef confl, vec<Lit>& out_learnt, vec<Lit> & selectors, int& out_btlevel,unsigned int &nblevels,unsigned int &szWithoutSelectors);    // (bt = backtrack)
 361     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
 362     bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
 363     lbool    search           (int nof_conflicts);                                     // Search for a given number of conflicts.
 364     virtual lbool    solve_           (bool do_simp = true, bool turn_off_simp = false);                                                      // Main solve method (assumptions given in 'assumptions').
 365     virtual void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
 366     void     removeSatisfied  (vec<CRef>& cs);                                         // Shrink 'cs' to contain only non-satisfied clauses.
 367     void     rebuildOrderHeap ();
 368
 369     // Maintaining Variable/Clause activity:
 370     //
 371     void     varDecayActivity ();                      // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead.
 372     void     varBumpActivity  (Var v, double inc);     // Increase a variable with the current 'bump' value.
 373     void     varBumpActivity  (Var v);                 // Increase a variable with the current 'bump' value.
 374     void     claDecayActivity ();                      // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead.
 375     void     claBumpActivity  (Clause& c);             // Increase a clause with the current 'bump' value.
 376
 377     // Operations on clauses:
 378     //
 379     void     attachClause     (CRef cr);               // Attach a clause to watcher lists.
 380     void     detachClause     (CRef cr, bool strict = false); // Detach a clause to watcher lists.
 381     void     detachClausePurgatory(CRef cr, bool strict = false);
 382     void     attachClausePurgatory(CRef cr);
 383     void     removeClause     (CRef cr, bool inPurgatory = false);               // Detach and free a clause.
 384     bool     locked           (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state.
 385     bool     satisfied        (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state.
 386
 387     unsigned int computeLBD(const vec<Lit> & lits,int end=-1);
 388     unsigned int computeLBD(const Clause &c);
 389     void minimisationWithBinaryResolution(vec<Lit> &out_learnt);
 390
 391     virtual void     relocAll         (ClauseAllocator& to);
 392
 393     // Misc:
 394     //
 395     int      decisionLevel    ()      const; // Gives the current decisionlevel.
 396     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
 397     CRef     reason           (Var x) const;
 398     int      level            (Var x) const;
 399     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
 400     bool     withinBudget     ()      const;
 401     inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
 402
 403     // Static helpers:
 404     //
 405
 406     // Returns a random float 0 <= x < 1. Seed must never be 0.
 407     static inline double drand(double& seed) {
 408         seed *= 1389796;
 409         int q = (int)(seed / 2147483647);
 410         seed -= (double)q * 2147483647;
 411         return seed / 2147483647; }
 412
 413     // Returns a random integer 0 <= x < size. Seed must never be 0.
 414     static inline int irand(double& seed, int size) {
 415         return (int)(drand(seed) * size); }
 416 };
 417
 418
 419 //=================================================================================================
 420 // Implementation of inline methods:
 421
 422 inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
 423 inline int  Solver::level (Var x) const { return vardata[x].level; }
 424
 425 inline void Solver::insertVarOrder(Var x) {
 426     if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
 427
 428 inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
 429 inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
 430 inline void Solver::varBumpActivity(Var v, double inc) {
 431     if ( (activity[v] += inc) > 1e100 ) {
 432         // Rescale:
 433         for (int i = 0; i < nVars(); i++)
 434             activity[i] *= 1e-100;
 435         var_inc *= 1e-100; }
 436
 437     // Update order_heap with respect to new activity:
 438     if (order_heap.inHeap(v))
 439         order_heap.decrease(v); }
 440
 441 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
 442 inline void Solver::claBumpActivity (Clause& c) {
 443         if ( (c.activity() += cla_inc) > 1e20 ) {
 444             // Rescale:
 445             for (int i = 0; i < learnts.size(); i++)
 446                 ca[learnts[i]].activity() *= 1e-20;
 447             cla_inc *= 1e-20; } }
 448
 449 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
 450 inline void Solver::checkGarbage(double gf){
 451     if (ca.wasted() > ca.size() * gf)
 452         garbageCollect(); }
 453
 454 // NOTE: enqueue does not set the ok flag! (only public methods do)
 455 inline bool     Solver::enqueue         (Lit p, CRef from)      { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
 456 inline bool     Solver::addClause       (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
 457 inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(); return addClause_(add_tmp); }
 458 inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
 459 inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
 460 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); }
 461  inline bool     Solver::locked          (const Clause& c) const {
 462    if(c.size()>2)
 463      return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c;
 464    return
 465      (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
 466      ||
 467      (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
 468  }
 469 inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
 470
 471 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 472 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
 473 inline lbool    Solver::value         (Var x) const   { return assigns[x]; }
 474 inline lbool    Solver::value         (Lit p) const   { return assigns[var(p)] ^ sign(p); }
 475 inline lbool    Solver::modelValue    (Var x) const   { return model[x]; }
 476 inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
 477 inline int      Solver::nAssigns      ()      const   { return trail.size(); }
 478 inline int      Solver::nClauses      ()      const   { return clauses.size(); }
 479 inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
 480 inline int      Solver::nVars         ()      const   { return vardata.size(); }
 481 inline int      Solver::assumptionsSize         ()      const   { return assumptions.size(); }
 482 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 483 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
 484 inline void     Solver::setDecisionVar(Var v, bool b)
 485 {
 486     if      ( b && !decision[v]) dec_vars++;
 487     else if (!b &&  decision[v]) dec_vars--;
 488
 489     decision[v] = b;
 490     insertVarOrder(v);
 491 }
 492 inline void     Solver::setConfBudget(int64_t x){ conflict_budget    = conflicts    + x; }
 493 inline void     Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
 494 inline void     Solver::interrupt(){ asynch_interrupt = true; }
 495 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 496 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
 497 inline bool     Solver::withinBudget() const {
 498     return !asynch_interrupt &&
 499            (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
 500            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
 501
 502 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
 503 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or
 504 // all calls to solve must return an 'lbool'. I'm not yet sure which I prefer.
 505 inline bool     Solver::solve         ()                    { budgetOff(); assumptions.clear(); return solve_() == l_True; }
 506 inline bool     Solver::solve         (Lit p)               { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }
 507 inline bool     Solver::solve         (Lit p, Lit q)        { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }
 508 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; }
 509 inline bool     Solver::solve         (const vec<Lit>& assumps){ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }
 510 inline lbool    Solver::solveLimited  (const vec<Lit>& assumps){ assumps.copyTo(assumptions); return solve_(); }
 511 inline bool     Solver::okay          ()      const   { return ok; }
 512
 513 inline void     Solver::toDimacs     (const char* file){ vec<Lit> as; toDimacs(file, as); }
 514 inline void     Solver::toDimacs     (const char* file, Lit p){ vec<Lit> as; as.push(p); toDimacs(file, as); }
 515 inline void     Solver::toDimacs     (const char* file, Lit p, Lit q){ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }
 516 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); }
 517
 518
 519
 520 //=================================================================================================
 521 // Debug etc:
 522
 523
 524 inline void Solver::printLit(Lit l)
 525 {
 526     printf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
 527 }
 528
 529
 530 inline void Solver::printClause(CRef cr)
 531 {
 532   Clause &c = ca[cr];
 533     for (int i = 0; i < c.size(); i++){
 534         printLit(c[i]);
 535         printf(" ");
 536     }
 537 }
 538
 539 inline void Solver::printInitialClause(CRef cr)
 540 {
 541   Clause &c = ca[cr];
 542     for (int i = 0; i < c.size(); i++){
 543       if(!isSelector(var(c[i]))) {
 544         printLit(c[i]);
 545         printf(" ");
 546       }
 547     }
 548 }
 549
 550 //=================================================================================================
 551
 552 struct reduceDB_lt {
 553     ClauseAllocator& ca;
 554
 555     reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {
 556     }
 557
 558     bool operator()(CRef x, CRef y) {
 559
 560         // Main criteria... Like in MiniSat we keep all binary clauses
 561         if (ca[x].size() > 2 && ca[y].size() == 2) return 1;
 562
 563         if (ca[y].size() > 2 && ca[x].size() == 2) return 0;
 564         if (ca[x].size() == 2 && ca[y].size() == 2) return 0;
 565
 566         // Second one  based on literal block distance
 567         if (ca[x].lbd() > ca[y].lbd()) return 1;
 568         if (ca[x].lbd() < ca[y].lbd()) return 0;
 569
 570
 571         // Finally we can use old activity or size, we choose the last one
 572         return ca[x].activity() < ca[y].activity();
 573         //return x->size() < y->size();
 574
 575         //return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
 576     }
 577 };
 578
 579
 580 }
 581
 582
 583 #endif