Minisat::Solver Class Reference

#include <Solver.h>

Inheritance diagram for Minisat::Solver:

Collaboration diagram for Minisat::Solver:

Data Structures
struct	ShrinkStackElem
struct	VarData
struct	VarOrderLt
struct	Watcher
struct	WatcherDeleted

Public Member Functions
	Solver ()
virtual	~Solver ()
Var	newVar (lbool upol=l_Undef, bool dvar=true)
void	releaseVar (Lit l)
bool	addClause (const vec< Lit > &ps)
bool	addEmptyClause ()
bool	addClause (Lit p)
bool	addClause (Lit p, Lit q)
bool	addClause (Lit p, Lit q, Lit r)
bool	addClause (Lit p, Lit q, Lit r, Lit s)
bool	addClause_ (vec< Lit > &ps)
bool	simplify ()
bool	solve (const vec< Lit > &assumps)
lbool	solveLimited (const vec< Lit > &assumps)
bool	solve ()
bool	solve (Lit p)
bool	solve (Lit p, Lit q)
bool	solve (Lit p, Lit q, Lit r)
bool	okay () const
bool	implies (const vec< Lit > &assumps, vec< Lit > &out)
ClauseIterator	clausesBegin () const
ClauseIterator	clausesEnd () const
TrailIterator	trailBegin () const
TrailIterator	trailEnd () const
void	toDimacs (FILE *f, const vec< Lit > &assumps)
void	toDimacs (const char *file, const vec< Lit > &assumps)
void	toDimacs (FILE *f, Clause &c, vec< Var > &map, Var &max)
void	toDimacs (const char *file)
void	toDimacs (const char *file, Lit p)
void	toDimacs (const char *file, Lit p, Lit q)
void	toDimacs (const char *file, Lit p, Lit q, Lit r)
void	setPolarity (Var v, lbool b)
void	setDecisionVar (Var v, bool b)
lbool	value (Var x) const
lbool	value (Lit p) const
lbool	modelValue (Var x) const
lbool	modelValue (Lit p) const
int	nAssigns () const
int	nClauses () const
int	nLearnts () const
int	nVars () const
int	nFreeVars () const
void	printStats () const
void	setConfBudget (int64_t x)
void	setPropBudget (int64_t x)
void	budgetOff ()
void	interrupt ()
void	clearInterrupt ()
virtual void	garbageCollect ()
void	checkGarbage (double gf)
void	checkGarbage ()

Data Fields
vec< lbool >	model
LSet	conflict
int	verbosity
double	var_decay
double	clause_decay
double	random_var_freq
double	random_seed
bool	luby_restart
int	ccmin_mode
int	phase_saving
bool	rnd_pol
bool	rnd_init_act
double	garbage_frac
int	min_learnts_lim
int	restart_first
double	restart_inc
double	learntsize_factor
double	learntsize_inc
int	learntsize_adjust_start_confl
double	learntsize_adjust_inc
uint64_t	solves
uint64_t	starts
uint64_t	decisions
uint64_t	rnd_decisions
uint64_t	propagations
uint64_t	conflicts
uint64_t	dec_vars
uint64_t	num_clauses
uint64_t	num_learnts
uint64_t	clauses_literals
uint64_t	learnts_literals
uint64_t	max_literals
uint64_t	tot_literals

Protected Member Functions
void	insertVarOrder (Var x)
Lit	pickBranchLit ()
void	newDecisionLevel ()
void	uncheckedEnqueue (Lit p, CRef from=CRef_Undef)
bool	enqueue (Lit p, CRef from=CRef_Undef)
CRef	propagate ()
void	cancelUntil (int level)
void	analyze (CRef confl, vec< Lit > &out_learnt, int &out_btlevel)
void	analyzeFinal (Lit p, LSet &out_conflict)
bool	litRedundant (Lit p)
lbool	search (int nof_conflicts)
lbool	solve_ ()
void	reduceDB ()
void	removeSatisfied (vec< CRef > &cs)
void	rebuildOrderHeap ()
void	varDecayActivity ()
void	varBumpActivity (Var v, double inc)
void	varBumpActivity (Var v)
void	claDecayActivity ()
void	claBumpActivity (Clause &c)
void	attachClause (CRef cr)
void	detachClause (CRef cr, bool strict=false)
void	removeClause (CRef cr)
bool	isRemoved (CRef cr) const
bool	locked (const Clause &c) const
bool	satisfied (const Clause &c) const
int	decisionLevel () const
uint32_t	abstractLevel (Var x) const
CRef	reason (Var x) const
int	level (Var x) const
double	progressEstimate () const
bool	withinBudget () const
void	relocAll (ClauseAllocator &to)

Static Protected Member Functions
static VarData	mkVarData (CRef cr, int l)
static double	drand (double &seed)
static int	irand (double &seed, int size)

Protected Attributes
vec< CRef >	clauses
vec< CRef >	learnts
vec< Lit >	trail
vec< int >	trail_lim
vec< Lit >	assumptions
VMap< double >	activity
VMap< lbool >	assigns
VMap< char >	polarity
VMap< lbool >	user_pol
VMap< char >	decision
VMap< VarData >	vardata
OccLists< Lit, vec< Watcher > , WatcherDeleted, MkIndexLit >	watches
Heap< Var, VarOrderLt >	order_heap
bool	ok
double	cla_inc
double	var_inc
int	qhead
int	simpDB_assigns
int64_t	simpDB_props
double	progress_estimate
bool	remove_satisfied
Var	next_var
ClauseAllocator	ca
vec< Var >	released_vars
vec< Var >	free_vars
VMap< char >	seen
vec< ShrinkStackElem >	analyze_stack
vec< Lit >	analyze_toclear
vec< Lit >	add_tmp
double	max_learnts
double	learntsize_adjust_confl
int	learntsize_adjust_cnt
int64_t	conflict_budget
int64_t	propagation_budget
bool	asynch_interrupt

Detailed Description

Definition at line 37 of file Solver.h.

Constructor & Destructor Documentation

Solver::Solver

(

)

Definition at line 56 of file Solver.cc.

               :

    // Parameters (user settable):
    //
    verbosity        (0)
  , var_decay        (opt_var_decay)
  , clause_decay     (opt_clause_decay)
  , random_var_freq  (opt_random_var_freq)
  , random_seed      (opt_random_seed)
  , luby_restart     (opt_luby_restart)
  , ccmin_mode       (opt_ccmin_mode)
  , phase_saving     (opt_phase_saving)
  , rnd_pol          (false)
  , rnd_init_act     (opt_rnd_init_act)
  , garbage_frac     (opt_garbage_frac)
  , min_learnts_lim  (opt_min_learnts_lim)
  , restart_first    (opt_restart_first)
  , restart_inc      (opt_restart_inc)

    // Parameters (the rest):
    //
  , learntsize_factor((double)1/(double)3), learntsize_inc(1.1)

    // Parameters (experimental):
    //
  , learntsize_adjust_start_confl (100)
  , learntsize_adjust_inc         (1.5)

    // Statistics: (formerly in 'SolverStats')
    //
  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
  , dec_vars(0), num_clauses(0), num_learnts(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)

  , watches            (WatcherDeleted(ca))
  , order_heap         (VarOrderLt(activity))
  , ok                 (true)
  , cla_inc            (1)
  , var_inc            (1)
  , qhead              (0)
  , simpDB_assigns     (-1)
  , simpDB_props       (0)
  , progress_estimate  (0)
  , remove_satisfied   (true)
  , next_var           (0)

    // Resource constraints:
    //
  , conflict_budget    (-1)
  , propagation_budget (-1)
  , asynch_interrupt   (false)
{}

Solver::~Solver ( )

virtual

Definition at line 109 of file Solver.cc.

{
}

Member Function Documentation

uint32_t Minisat::Solver::abstractLevel ( Var  x ) const

inlineprotected

Definition at line 349 of file Solver.h.

{ return 1 << (level(x) & 31); }

Here is the call graph for this function:

bool Minisat::Solver::addClause ( const vec< Lit > &  ps )

inline

Definition at line 337 of file Solver.h.

{ ps.copyTo(add_tmp); return addClause_(add_tmp); }

Here is the call graph for this function:

Here is the caller graph for this function:

bool Minisat::Solver::addClause ( Lit  p )

inline

Definition at line 339 of file Solver.h.

{ add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }

Here is the call graph for this function:

bool Minisat::Solver::addClause ( Lit  p, Lit  q  )

inline

Definition at line 340 of file Solver.h.

{ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }

Here is the call graph for this function:

bool Minisat::Solver::addClause ( Lit  p, Lit  q, Lit  r  )

inline

Definition at line 341 of file Solver.h.

{ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }

Here is the call graph for this function:

bool Minisat::Solver::addClause ( Lit  p, Lit  q, Lit  r, Lit  s  )

inline

Definition at line 342 of file Solver.h.

{ add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); add_tmp.push(s); return addClause_(add_tmp); }

Here is the call graph for this function:

bool Solver::addClause_

(

vec< Lit > &

ps

)

Definition at line 156 of file Solver.cc.

{
    assert(decisionLevel() == 0);
    if (!ok) return false;

    // Check if clause is satisfied and remove false/duplicate literals:
    sort(ps);
    Lit p; int i, j;
    for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
        if (value(ps[i]) == l_True || ps[i] == ~p)
            return true;
        else if (value(ps[i]) != l_False && ps[i] != p)
            ps[j++] = p = ps[i];
    ps.shrink(i - j);

    if (ps.size() == 0)
        return ok = false;
    else if (ps.size() == 1){
        uncheckedEnqueue(ps[0]);
        return ok = (propagate() == CRef_Undef);
    }else{
        CRef cr = ca.alloc(ps, false);
        clauses.push(cr);
        attachClause(cr);
    }

    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool Minisat::Solver::addEmptyClause ( )

inline

Definition at line 338 of file Solver.h.

{ add_tmp.clear(); return addClause_(add_tmp); }

Here is the call graph for this function:

void Solver::analyze ( CRef  confl, vec< Lit > &  out_learnt, int &  out_btlevel  )

protected

Definition at line 298 of file Solver.cc.

{
    int pathC = 0;
    Lit p     = lit_Undef;

    // Generate conflict clause:
    //
    out_learnt.push();      // (leave room for the asserting literal)
    int index   = trail.size() - 1;

    do{
        assert(confl != CRef_Undef); // (otherwise should be UIP)
        Clause& c = ca[confl];

        if (c.learnt())
            claBumpActivity(c);

        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
            Lit q = c[j];

            if (!seen[var(q)] && level(var(q)) > 0){
                varBumpActivity(var(q));
                seen[var(q)] = 1;
                if (level(var(q)) >= decisionLevel())
                    pathC++;
                else
                    out_learnt.push(q);
            }
        }
        
        // Select next clause to look at:
        while (!seen[var(trail[index--])]);
        p     = trail[index+1];
        confl = reason(var(p));
        seen[var(p)] = 0;
        pathC--;

    }while (pathC > 0);
    out_learnt[0] = ~p;

    // Simplify conflict clause:
    //
    int i, j;
    out_learnt.copyTo(analyze_toclear);
    if (ccmin_mode == 2){
        for (i = j = 1; i < out_learnt.size(); i++)
            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i]))
                out_learnt[j++] = out_learnt[i];
        
    }else if (ccmin_mode == 1){
        for (i = j = 1; i < out_learnt.size(); i++){
            Var x = var(out_learnt[i]);

            if (reason(x) == CRef_Undef)
                out_learnt[j++] = out_learnt[i];
            else{
                Clause& c = ca[reason(var(out_learnt[i]))];
                for (int k = 1; k < c.size(); k++)
                    if (!seen[var(c[k])] && level(var(c[k])) > 0){
                        out_learnt[j++] = out_learnt[i];
                        break; }
            }
        }
    }else
        i = j = out_learnt.size();

    max_literals += out_learnt.size();
    out_learnt.shrink(i - j);
    tot_literals += out_learnt.size();

    // Find correct backtrack level:
    //
    if (out_learnt.size() == 1)
        out_btlevel = 0;
    else{
        int max_i = 1;
        // Find the first literal assigned at the next-highest level:
        for (int i = 2; i < out_learnt.size(); i++)
            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
                max_i = i;
        // Swap-in this literal at index 1:
        Lit p             = out_learnt[max_i];
        out_learnt[max_i] = out_learnt[1];
        out_learnt[1]     = p;
        out_btlevel       = level(var(p));
    }

    for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::analyzeFinal ( Lit  p, LSet &  out_conflict  )

protected

Definition at line 458 of file Solver.cc.

{
    out_conflict.clear();
    out_conflict.insert(p);

    if (decisionLevel() == 0)
        return;

    seen[var(p)] = 1;

    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
        Var x = var(trail[i]);
        if (seen[x]){
            if (reason(x) == CRef_Undef){
                assert(level(x) > 0);
                out_conflict.insert(~trail[i]);
            }else{
                Clause& c = ca[reason(x)];
                for (int j = 1; j < c.size(); j++)
                    if (level(var(c[j])) > 0)
                        seen[var(c[j])] = 1;
            }
            seen[x] = 0;
        }
    }

    seen[var(p)] = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::attachClause ( CRef  cr )

protected

Definition at line 186 of file Solver.cc.

                                {
    const Clause& c = ca[cr];
    assert(c.size() > 1);
    watches[~c[0]].push(Watcher(cr, c[1]));
    watches[~c[1]].push(Watcher(cr, c[0]));
    if (c.learnt()) num_learnts++, learnts_literals += c.size();
    else            num_clauses++, clauses_literals += c.size();
}

Here is the caller graph for this function:

void Minisat::Solver::budgetOff ( )

inline

Definition at line 373 of file Solver.h.

{ conflict_budget = propagation_budget = -1; }

Here is the caller graph for this function:

void Solver::cancelUntil ( int  level )

protected

Definition at line 233 of file Solver.cc.

                                  {
    if (decisionLevel() > level){
        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
            Var      x  = var(trail[c]);
            assigns [x] = l_Undef;
            if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last()))
                polarity[x] = sign(trail[c]);
            insertVarOrder(x); }
        qhead = trail_lim[level];
        trail.shrink(trail.size() - trail_lim[level]);
        trail_lim.shrink(trail_lim.size() - level);
    } }

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::Solver::checkGarbage ( double  gf )

inline

Definition at line 331 of file Solver.h.

                                         {
    if (ca.wasted() > ca.size() * gf)
        garbageCollect(); }

Here is the call graph for this function:

void Minisat::Solver::checkGarbage ( void  )

inline

Definition at line 330 of file Solver.h.

{ return checkGarbage(garbage_frac); }

Here is the caller graph for this function:

void Minisat::Solver::claBumpActivity ( Clause &  c )

inlineprotected

Definition at line 323 of file Solver.h.

                                              {
        if ( (c.activity() += cla_inc) > 1e20 ) {
            // Rescale:
            for (int i = 0; i < learnts.size(); i++)
                ca[learnts[i]].activity() *= 1e-20;
            cla_inc *= 1e-20; } }

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::Solver::claDecayActivity ( )

inlineprotected

Definition at line 322 of file Solver.h.

{ cla_inc *= (1 / clause_decay); }

Here is the caller graph for this function:

ClauseIterator Minisat::Solver::clausesBegin ( ) const

inline

Definition at line 390 of file Solver.h.

{ return ClauseIterator(ca, &clauses[0]); }

ClauseIterator Minisat::Solver::clausesEnd ( ) const

inline

Definition at line 391 of file Solver.h.

{ return ClauseIterator(ca, &clauses[clauses.size()]); }

Here is the call graph for this function:

void Minisat::Solver::clearInterrupt ( )

inline

Definition at line 372 of file Solver.h.

{ asynch_interrupt = false; }

int Minisat::Solver::decisionLevel ( ) const

inlineprotected

Definition at line 348 of file Solver.h.

{ return trail_lim.size(); }

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::detachClause ( CRef  cr, bool  strict = false  )

protected

Definition at line 196 of file Solver.cc.

                                             {
    const Clause& c = ca[cr];
    assert(c.size() > 1);
    
    // Strict or lazy detaching:
    if (strict){
        remove(watches[~c[0]], Watcher(cr, c[1]));
        remove(watches[~c[1]], Watcher(cr, c[0]));
    }else{
        watches.smudge(~c[0]);
        watches.smudge(~c[1]);
    }

    if (c.learnt()) num_learnts--, learnts_literals -= c.size();
    else            num_clauses--, clauses_literals -= c.size();
}

Here is the caller graph for this function:

static double Minisat::Solver::drand ( double &  seed )

inlinestaticprotected

Definition at line 288 of file Solver.h.

                                             {
        seed *= 1389796;
        int q = (int)(seed / 2147483647);
        seed -= (double)q * 2147483647;
        return seed / 2147483647; }

Here is the caller graph for this function:

bool Minisat::Solver::enqueue ( Lit  p, CRef  from = CRef_Undef  )

inlineprotected

Definition at line 336 of file Solver.h.

{ return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::garbageCollect ( )

virtual

Reimplemented in Minisat::SimpSolver.

Definition at line 1057 of file Solver.cc.

{
    // Initialize the next region to a size corresponding to the estimated utilization degree. This
    // is not precise but should avoid some unnecessary reallocations for the new region:
    ClauseAllocator to(ca.size() - ca.wasted()); 

    relocAll(to);
    if (verbosity >= 2)
        printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
               ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
    to.moveTo(ca);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool Solver::implies	(	const vec< Lit > &	assumps,
		vec< Lit > &	out
	)

Definition at line 889 of file Solver.cc.

{
    trail_lim.push(trail.size());
    for (int i = 0; i < assumps.size(); i++){
        Lit a = assumps[i];

        if (value(a) == l_False){
            cancelUntil(0);
            return false;
        }else if (value(a) == l_Undef)
            uncheckedEnqueue(a);
    }

    unsigned trail_before = trail.size();
    bool     ret          = true;
    if (propagate() == CRef_Undef){
        out.clear();
        for (int j = trail_before; j < trail.size(); j++)
            out.push(trail[j]);
    }else
        ret = false;
    
    cancelUntil(0);
    return ret;
}

Here is the call graph for this function:

void Minisat::Solver::insertVarOrder ( Var  x )

inlineprotected

Definition at line 306 of file Solver.h.

                                        {
    if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }

Here is the caller graph for this function:

void Minisat::Solver::interrupt ( )

inline

Definition at line 371 of file Solver.h.

{ asynch_interrupt = true; }

Here is the caller graph for this function:

static int Minisat::Solver::irand ( double &  seed, int  size  )

inlinestaticprotected

Definition at line 295 of file Solver.h.

                                                    {
        return (int)(drand(seed) * size); }

Here is the call graph for this function:

Here is the caller graph for this function:

bool Minisat::Solver::isRemoved ( CRef  cr ) const

inlineprotected

Definition at line 344 of file Solver.h.

{ return ca[cr].mark() == 1; }

Here is the caller graph for this function:

int Minisat::Solver::level ( Var  x ) const

inlineprotected

Definition at line 304 of file Solver.h.

{ return vardata[x].level; }

Here is the caller graph for this function:

bool Solver::litRedundant ( Lit  p )

protected

Definition at line 390 of file Solver.cc.

{
    enum { seen_undef = 0, seen_source = 1, seen_removable = 2, seen_failed = 3 };
    assert(seen[var(p)] == seen_undef || seen[var(p)] == seen_source);
    assert(reason(var(p)) != CRef_Undef);

    Clause*               c     = &ca[reason(var(p))];
    vec<ShrinkStackElem>& stack = analyze_stack;
    stack.clear();

    for (uint32_t i = 1; ; i++){
        if (i < (uint32_t)c->size()){
            // Checking 'p'-parents 'l':
            Lit l = (*c)[i];
            
            // Variable at level 0 or previously removable:
            if (level(var(l)) == 0 || seen[var(l)] == seen_source || seen[var(l)] == seen_removable){
                continue; }
            
            // Check variable can not be removed for some local reason:
            if (reason(var(l)) == CRef_Undef || seen[var(l)] == seen_failed){
                stack.push(ShrinkStackElem(0, p));
                for (int i = 0; i < stack.size(); i++)
                    if (seen[var(stack[i].l)] == seen_undef){
                        seen[var(stack[i].l)] = seen_failed;
                        analyze_toclear.push(stack[i].l);
                    }
                    
                return false;
            }

            // Recursively check 'l':
            stack.push(ShrinkStackElem(i, p));
            i  = 0;
            p  = l;
            c  = &ca[reason(var(p))];
        }else{
            // Finished with current element 'p' and reason 'c':
            if (seen[var(p)] == seen_undef){
                seen[var(p)] = seen_removable;
                analyze_toclear.push(p);
            }

            // Terminate with success if stack is empty:
            if (stack.size() == 0) break;
            
            // Continue with top element on stack:
            i  = stack.last().i;
            p  = stack.last().l;
            c  = &ca[reason(var(p))];

            stack.pop();
        }
    }

    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool Minisat::Solver::locked ( const Clause &  c ) const

inlineprotected

Definition at line 345 of file Solver.h.

{ return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }

Here is the call graph for this function:

Here is the caller graph for this function:

static VarData Minisat::Solver::mkVarData ( CRef  cr, int  l  )

inlinestaticprotected

Definition at line 159 of file Solver.h.

{ VarData d = {cr, l}; return d; }

Here is the caller graph for this function:

lbool Minisat::Solver::modelValue ( Var  x ) const

inline

Definition at line 352 of file Solver.h.

{ return model[x]; }

Here is the caller graph for this function:

lbool Minisat::Solver::modelValue ( Lit  p ) const

inline

Definition at line 353 of file Solver.h.

{ return model[var(p)] ^ sign(p); }

Here is the call graph for this function:

int Minisat::Solver::nAssigns ( ) const

inline

Definition at line 354 of file Solver.h.

{ return trail.size(); }

Here is the call graph for this function:

Here is the caller graph for this function:

int Minisat::Solver::nClauses ( ) const

inline

Definition at line 355 of file Solver.h.

{ return num_clauses; }

Here is the caller graph for this function:

void Minisat::Solver::newDecisionLevel ( )

inlineprotected

Definition at line 346 of file Solver.h.

{ trail_lim.push(trail.size()); }

Here is the call graph for this function:

Here is the caller graph for this function:

Var Solver::newVar	(	lbool	upol = l_Undef,
		bool	dvar = true
	)

Definition at line 121 of file Solver.cc.

{
    Var v;
    if (free_vars.size() > 0){
        v = free_vars.last();
        free_vars.pop();
    }else
        v = next_var++;

    watches  .init(mkLit(v, false));
    watches  .init(mkLit(v, true ));
    assigns  .insert(v, l_Undef);
    vardata  .insert(v, mkVarData(CRef_Undef, 0));
    activity .insert(v, rnd_init_act ? drand(random_seed) * 0.00001 : 0);
    seen     .insert(v, 0);
    polarity .insert(v, true);
    user_pol .insert(v, upol);
    decision .reserve(v);
    trail    .capacity(v+1);
    setDecisionVar(v, dvar);
    return v;
}

Here is the call graph for this function:

Here is the caller graph for this function:

int Minisat::Solver::nFreeVars ( ) const

inline

Definition at line 359 of file Solver.h.

{ return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }

Here is the call graph for this function:

int Minisat::Solver::nLearnts ( ) const

inline

Definition at line 356 of file Solver.h.

{ return num_learnts; }

Here is the caller graph for this function:

int Minisat::Solver::nVars ( ) const

inline

Definition at line 357 of file Solver.h.

{ return next_var; }

Here is the caller graph for this function:

bool Minisat::Solver::okay ( ) const

inline

Definition at line 388 of file Solver.h.

{ return ok; }

Lit Solver::pickBranchLit ( )

protected

Definition at line 251 of file Solver.cc.

{
    Var next = var_Undef;

    // Random decision:
    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
        next = order_heap[irand(random_seed,order_heap.size())];
        if (value(next) == l_Undef && decision[next])
            rnd_decisions++; }

    // Activity based decision:
    while (next == var_Undef || value(next) != l_Undef || !decision[next])
        if (order_heap.empty()){
            next = var_Undef;
            break;
        }else
            next = order_heap.removeMin();

    // Choose polarity based on different polarity modes (global or per-variable):
    if (next == var_Undef)
        return lit_Undef;
    else if (user_pol[next] != l_Undef)
        return mkLit(next, user_pol[next] == l_True);
    else if (rnd_pol)
        return mkLit(next, drand(random_seed) < 0.5);
    else
        return mkLit(next, polarity[next]);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::printStats

(

)

const

Definition at line 993 of file Solver.cc.

{
    double cpu_time = cpuTime();
    double mem_used = memUsedPeak();
    printf("restarts              : %" PRIu64 "\n", starts);
    printf("conflicts             : %-12" PRIu64 "   (%.0f /sec)\n", conflicts   , conflicts   /cpu_time);
    printf("decisions             : %-12" PRIu64 "   (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions   /cpu_time);
    printf("propagations          : %-12" PRIu64 "   (%.0f /sec)\n", propagations, propagations/cpu_time);
    printf("conflict literals     : %-12" PRIu64 "   (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals);
    if (mem_used != 0) printf("Memory used           : %.2f MB\n", mem_used);
    printf("CPU time              : %g s\n", cpu_time);
}

Here is the call graph for this function:

double Solver::progressEstimate ( ) const

protected

Definition at line 798 of file Solver.cc.

{
    double  progress = 0;
    double  F = 1.0 / nVars();

    for (int i = 0; i <= decisionLevel(); i++){
        int beg = i == 0 ? 0 : trail_lim[i - 1];
        int end = i == decisionLevel() ? trail.size() : trail_lim[i];
        progress += pow(F, i) * (end - beg);
    }

    return progress / nVars();
}

Here is the call graph for this function:

Here is the caller graph for this function:

CRef Solver::propagate ( )

protected

Definition at line 508 of file Solver.cc.

{
    CRef    confl     = CRef_Undef;
    int     num_props = 0;

    while (qhead < trail.size()){
        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
        vec<Watcher>&  ws  = watches.lookup(p);
        Watcher        *i, *j, *end;
        num_props++;

        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
            // Try to avoid inspecting the clause:
            Lit blocker = i->blocker;
            if (value(blocker) == l_True){
                *j++ = *i++; continue; }

            // Make sure the false literal is data[1]:
            CRef     cr        = i->cref;
            Clause&  c         = ca[cr];
            Lit      false_lit = ~p;
            if (c[0] == false_lit)
                c[0] = c[1], c[1] = false_lit;
            assert(c[1] == false_lit);
            i++;

            // If 0th watch is true, then clause is already satisfied.
            Lit     first = c[0];
            Watcher w     = Watcher(cr, first);
            if (first != blocker && value(first) == l_True){
                *j++ = w; continue; }

            // Look for new watch:
            for (int k = 2; k < c.size(); k++)
                if (value(c[k]) != l_False){
                    c[1] = c[k]; c[k] = false_lit;
                    watches[~c[1]].push(w);
                    goto NextClause; }

            // Did not find watch -- clause is unit under assignment:
            *j++ = w;
            if (value(first) == l_False){
                confl = cr;
                qhead = trail.size();
                // Copy the remaining watches:
                while (i < end)
                    *j++ = *i++;
            }else
                uncheckedEnqueue(first, cr);

        NextClause:;
        }
        ws.shrink(i - j);
    }
    propagations += num_props;
    simpDB_props -= num_props;

    return confl;
}

Here is the call graph for this function:

Here is the caller graph for this function:

CRef Minisat::Solver::reason ( Var  x ) const

inlineprotected

Definition at line 303 of file Solver.h.

{ return vardata[x].reason; }

Here is the caller graph for this function:

void Solver::rebuildOrderHeap ( )

protected

Definition at line 625 of file Solver.cc.

{
    vec<Var> vs;
    for (Var v = 0; v < nVars(); v++)
        if (decision[v] && value(v) == l_Undef)
            vs.push(v);
    order_heap.build(vs);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::reduceDB ( )

protected

Definition at line 583 of file Solver.cc.

{
    int     i, j;
    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity

    sort(learnts, reduceDB_lt(ca));
    // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
    // and clauses with activity smaller than 'extra_lim':
    for (i = j = 0; i < learnts.size(); i++){
        Clause& c = ca[learnts[i]];
        if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
            removeClause(learnts[i]);
        else
            learnts[j++] = learnts[i];
    }
    learnts.shrink(i - j);
    checkGarbage();
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::releaseVar

(

Lit

l

)

Definition at line 147 of file Solver.cc.

{
    if (value(l) == l_Undef){
        addClause(l);
        released_vars.push(var(l));
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::relocAll ( ClauseAllocator &  to )

protected

Definition at line 1010 of file Solver.cc.

{
    // All watchers:
    //
    watches.cleanAll();
    for (int v = 0; v < nVars(); v++)
        for (int s = 0; s < 2; s++){
            Lit p = mkLit(v, s);
            vec<Watcher>& ws = watches[p];
            for (int j = 0; j < ws.size(); j++)
                ca.reloc(ws[j].cref, to);
        }

    // All reasons:
    //
    for (int i = 0; i < trail.size(); i++){
        Var v = var(trail[i]);

        // Note: it is not safe to call 'locked()' on a relocated clause. This is why we keep
        // 'dangling' reasons here. It is safe and does not hurt.
        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)]))){
            assert(!isRemoved(reason(v)));
            ca.reloc(vardata[v].reason, to);
        }
    }

    // All learnt:
    //
    int i, j;
    for (i = j = 0; i < learnts.size(); i++)
        if (!isRemoved(learnts[i])){
            ca.reloc(learnts[i], to);
            learnts[j++] = learnts[i];
        }
    learnts.shrink(i - j);

    // All original:
    //
    for (i = j = 0; i < clauses.size(); i++)
        if (!isRemoved(clauses[i])){
            ca.reloc(clauses[i], to);
            clauses[j++] = clauses[i];
        }
    clauses.shrink(i - j);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::removeClause ( CRef  cr )

protected

Definition at line 214 of file Solver.cc.

                                 {
    Clause& c = ca[cr];
    detachClause(cr);
    // Don't leave pointers to free'd memory!
    if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
    c.mark(1); 
    ca.free(cr);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::removeSatisfied ( vec< CRef > &  cs )

protected

Definition at line 603 of file Solver.cc.

{
    int i, j;
    for (i = j = 0; i < cs.size(); i++){
        Clause& c = ca[cs[i]];
        if (satisfied(c))
            removeClause(cs[i]);
        else{
            // Trim clause:
            assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef);
            for (int k = 2; k < c.size(); k++)
                if (value(c[k]) == l_False){
                    c[k--] = c[c.size()-1];
                    c.pop();
                }
            cs[j++] = cs[i];
        }
    }
    cs.shrink(i - j);
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool Solver::satisfied ( const Clause &  c ) const

protected

Definition at line 224 of file Solver.cc.

                                            {
    for (int i = 0; i < c.size(); i++)
        if (value(c[i]) == l_True)
            return true;
    return false; }

Here is the call graph for this function:

Here is the caller graph for this function:

lbool Solver::search ( int  nof_conflicts )

protected

Definition at line 704 of file Solver.cc.

{
    assert(ok);
    int         backtrack_level;
    int         conflictC = 0;
    vec<Lit>    learnt_clause;
    starts++;

    for (;;){
        CRef confl = propagate();
        if (confl != CRef_Undef){
            // CONFLICT
            conflicts++; conflictC++;
            if (decisionLevel() == 0) return l_False;

            learnt_clause.clear();
            analyze(confl, learnt_clause, backtrack_level);
            cancelUntil(backtrack_level);

            if (learnt_clause.size() == 1){
                uncheckedEnqueue(learnt_clause[0]);
            }else{
                CRef cr = ca.alloc(learnt_clause, true);
                learnts.push(cr);
                attachClause(cr);
                claBumpActivity(ca[cr]);
                uncheckedEnqueue(learnt_clause[0], cr);
            }

            varDecayActivity();
            claDecayActivity();

            if (--learntsize_adjust_cnt == 0){
                learntsize_adjust_confl *= learntsize_adjust_inc;
                learntsize_adjust_cnt    = (int)learntsize_adjust_confl;
                max_learnts             *= learntsize_inc;

                if (verbosity >= 1)
                    printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", 
                           (int)conflicts, 
                           (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
                           (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
            }

        }else{
            // NO CONFLICT
            if ((nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){
                // Reached bound on number of conflicts:
                progress_estimate = progressEstimate();
                cancelUntil(0);
                return l_Undef; }

            // Simplify the set of problem clauses:
            if (decisionLevel() == 0 && !simplify())
                return l_False;

            if (learnts.size()-nAssigns() >= max_learnts)
                // Reduce the set of learnt clauses:
                reduceDB();

            Lit next = lit_Undef;
            while (decisionLevel() < assumptions.size()){
                // Perform user provided assumption:
                Lit p = assumptions[decisionLevel()];
                if (value(p) == l_True){
                    // Dummy decision level:
                    newDecisionLevel();
                }else if (value(p) == l_False){
                    analyzeFinal(~p, conflict);
                    return l_False;
                }else{
                    next = p;
                    break;
                }
            }

            if (next == lit_Undef){
                // New variable decision:
                decisions++;
                next = pickBranchLit();

                if (next == lit_Undef)
                    // Model found:
                    return l_True;
            }

            // Increase decision level and enqueue 'next'
            newDecisionLevel();
            uncheckedEnqueue(next);
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::Solver::setConfBudget ( int64_t  x )

inline

Definition at line 369 of file Solver.h.

{ conflict_budget    = conflicts    + x; }

void Minisat::Solver::setDecisionVar ( Var  v, bool  b  )

inline

Definition at line 361 of file Solver.h.

{ 
    if      ( b && !decision[v]) dec_vars++;
    else if (!b &&  decision[v]) dec_vars--;

    decision[v] = b;
    insertVarOrder(v);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::Solver::setPolarity ( Var  v, lbool  b  )

inline

Definition at line 360 of file Solver.h.

{ user_pol[v] = b; }

void Minisat::Solver::setPropBudget ( int64_t  x )

inline

Definition at line 370 of file Solver.h.

{ propagation_budget = propagations + x; }

bool Solver::simplify

(

)

Definition at line 643 of file Solver.cc.

{
    assert(decisionLevel() == 0);

    if (!ok || propagate() != CRef_Undef)
        return ok = false;

    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
        return true;

    // Remove satisfied clauses:
    removeSatisfied(learnts);
    if (remove_satisfied){       // Can be turned off.
        removeSatisfied(clauses);

        // TODO: what todo in if 'remove_satisfied' is false?

        // Remove all released variables from the trail:
        for (int i = 0; i < released_vars.size(); i++){
            assert(seen[released_vars[i]] == 0);
            seen[released_vars[i]] = 1;
        }

        int i, j;
        for (i = j = 0; i < trail.size(); i++)
            if (seen[var(trail[i])] == 0)
                trail[j++] = trail[i];
        trail.shrink(i - j);
        //printf("trail.size()= %d, qhead = %d\n", trail.size(), qhead);
        qhead = trail.size();

        for (int i = 0; i < released_vars.size(); i++)
            seen[released_vars[i]] = 0;

        // Released variables are now ready to be reused:
        append(released_vars, free_vars);
        released_vars.clear();
    }
    checkGarbage();
    rebuildOrderHeap();

    simpDB_assigns = nAssigns();
    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)

    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool Minisat::Solver::solve ( const vec< Lit > &  assumps )

inline

Definition at line 386 of file Solver.h.

{ budgetOff(); assumps.copyTo(assumptions); return solve_() == l_True; }

Here is the call graph for this function:

bool Minisat::Solver::solve ( )

inline

Definition at line 382 of file Solver.h.

{ budgetOff(); assumptions.clear(); return solve_() == l_True; }

Here is the call graph for this function:

bool Minisat::Solver::solve ( Lit  p )

inline

Definition at line 383 of file Solver.h.

{ budgetOff(); assumptions.clear(); assumptions.push(p); return solve_() == l_True; }

Here is the call graph for this function:

bool Minisat::Solver::solve ( Lit  p, Lit  q  )

inline

Definition at line 384 of file Solver.h.

{ budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_() == l_True; }

Here is the call graph for this function:

bool Minisat::Solver::solve ( Lit  p, Lit  q, Lit  r  )

inline

Definition at line 385 of file Solver.h.

{ budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_() == l_True; }

Here is the call graph for this function:

lbool Solver::solve_ ( )

protected

Definition at line 841 of file Solver.cc.

{
    model.clear();
    conflict.clear();
    if (!ok) return l_False;

    solves++;

    max_learnts = nClauses() * learntsize_factor;
    if (max_learnts < min_learnts_lim)
        max_learnts = min_learnts_lim;

    learntsize_adjust_confl   = learntsize_adjust_start_confl;
    learntsize_adjust_cnt     = (int)learntsize_adjust_confl;
    lbool   status            = l_Undef;

    if (verbosity >= 1){
        printf("============================[ Search Statistics ]==============================\n");
        printf("| Conflicts |          ORIGINAL         |          LEARNT          | Progress |\n");
        printf("|           |    Vars  Clauses Literals |    Limit  Clauses Lit/Cl |          |\n");
        printf("===============================================================================\n");
    }

    // Search:
    int curr_restarts = 0;
    while (status == l_Undef){
        double rest_base = luby_restart ? luby(restart_inc, curr_restarts) : pow(restart_inc, curr_restarts);
        status = search(rest_base * restart_first);
        if (!withinBudget()) break;
        curr_restarts++;
    }

    if (verbosity >= 1)
        printf("===============================================================================\n");


    if (status == l_True){
        // Extend & copy model:
        model.growTo(nVars());
        for (int i = 0; i < nVars(); i++) model[i] = value(i);
    }else if (status == l_False && conflict.size() == 0)
        ok = false;

    cancelUntil(0);
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

lbool Minisat::Solver::solveLimited ( const vec< Lit > &  assumps )

inline

Definition at line 387 of file Solver.h.

{ assumps.copyTo(assumptions); return solve_(); }

Here is the call graph for this function:

void Solver::toDimacs	(	FILE *	f,
		const vec< Lit > &	assumps
	)

Definition at line 951 of file Solver.cc.

{
    // Handle case when solver is in contradictory state:
    if (!ok){
        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
        return; }

    vec<Var> map; Var max = 0;

    // Cannot use removeClauses here because it is not safe
    // to deallocate them at this point. Could be improved.
    int cnt = 0;
    for (int i = 0; i < clauses.size(); i++)
        if (!satisfied(ca[clauses[i]]))
            cnt++;
        
    for (int i = 0; i < clauses.size(); i++)
        if (!satisfied(ca[clauses[i]])){
            Clause& c = ca[clauses[i]];
            for (int j = 0; j < c.size(); j++)
                if (value(c[j]) != l_False)
                    mapVar(var(c[j]), map, max);
        }

    // Assumptions are added as unit clauses:
    cnt += assumps.size();

    fprintf(f, "p cnf %d %d\n", max, cnt);

    for (int i = 0; i < assumps.size(); i++){
        assert(value(assumps[i]) != l_False);
        fprintf(f, "%s%d 0\n", sign(assumps[i]) ? "-" : "", mapVar(var(assumps[i]), map, max)+1);
    }

    for (int i = 0; i < clauses.size(); i++)
        toDimacs(f, ca[clauses[i]], map, max);

    if (verbosity > 0)
        printf("Wrote DIMACS with %d variables and %d clauses.\n", max, cnt);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::toDimacs	(	const char *	file,
		const vec< Lit > &	assumps
	)

Definition at line 941 of file Solver.cc.

{
    FILE* f = fopen(file, "wr");
    if (f == NULL)
        fprintf(stderr, "could not open file %s\n", file), exit(1);
    toDimacs(f, assumps);
    fclose(f);
}

Here is the call graph for this function:

void Solver::toDimacs	(	FILE *	f,
		Clause &	c,
		vec< Var > &	map,
		Var &	max
	)

Definition at line 930 of file Solver.cc.

{
    if (satisfied(c)) return;

    for (int i = 0; i < c.size(); i++)
        if (value(c[i]) != l_False)
            fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", mapVar(var(c[i]), map, max)+1);
    fprintf(f, "0\n");
}

Here is the call graph for this function:

void Minisat::Solver::toDimacs ( const char *  file )

inline

Definition at line 396 of file Solver.h.

{ vec<Lit> as; toDimacs(file, as); }

Here is the call graph for this function:

void Minisat::Solver::toDimacs ( const char *  file, Lit  p  )

inline

Definition at line 397 of file Solver.h.

{ vec<Lit> as; as.push(p); toDimacs(file, as); }

Here is the call graph for this function:

void Minisat::Solver::toDimacs ( const char *  file, Lit  p, Lit  q  )

inline

Definition at line 398 of file Solver.h.

{ vec<Lit> as; as.push(p); as.push(q); toDimacs(file, as); }

Here is the call graph for this function:

void Minisat::Solver::toDimacs ( const char *  file, Lit  p, Lit  q, Lit  r  )

inline

Definition at line 399 of file Solver.h.

{ vec<Lit> as; as.push(p); as.push(q); as.push(r); toDimacs(file, as); }

Here is the call graph for this function:

TrailIterator Minisat::Solver::trailBegin ( ) const

inline

Definition at line 392 of file Solver.h.

{ return TrailIterator(&trail[0]); }

TrailIterator Minisat::Solver::trailEnd ( ) const

inline

Definition at line 393 of file Solver.h.

                                                 { 
    return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); }

Here is the call graph for this function:

void Solver::uncheckedEnqueue ( Lit  p, CRef  from = CRef_Undef  )

protected

Definition at line 488 of file Solver.cc.

{
    assert(value(p) == l_Undef);
    assigns[var(p)] = lbool(!sign(p));
    vardata[var(p)] = mkVarData(from, decisionLevel());
    trail.push_(p);
}

Here is the call graph for this function:

Here is the caller graph for this function:

lbool Minisat::Solver::value ( Var  x ) const

inline

Definition at line 350 of file Solver.h.

{ return assigns[x]; }

Here is the caller graph for this function:

lbool Minisat::Solver::value ( Lit  p ) const

inline

Definition at line 351 of file Solver.h.

{ return assigns[var(p)] ^ sign(p); }

Here is the call graph for this function:

void Minisat::Solver::varBumpActivity ( Var  v, double  inc  )

inlineprotected

Definition at line 311 of file Solver.h.

                                                     {
    if ( (activity[v] += inc) > 1e100 ) {
        // Rescale:
        for (int i = 0; i < nVars(); i++)
            activity[i] *= 1e-100;
        var_inc *= 1e-100; }

    // Update order_heap with respect to new activity:
    if (order_heap.inHeap(v))
        order_heap.decrease(v); }

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::Solver::varBumpActivity ( Var  v )

inlineprotected

Definition at line 310 of file Solver.h.

{ varBumpActivity(v, var_inc); }

Here is the call graph for this function:

void Minisat::Solver::varDecayActivity ( )

inlineprotected

Definition at line 309 of file Solver.h.

{ var_inc *= (1 / var_decay); }

Here is the caller graph for this function:

bool Minisat::Solver::withinBudget ( ) const

inlineprotected

Definition at line 374 of file Solver.h.

                                           {
    return !asynch_interrupt &&
           (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
           (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }

Here is the caller graph for this function:

Field Documentation

VMap<double> Minisat::Solver::activity

protected

Definition at line 196 of file Solver.h.

vec<Lit> Minisat::Solver::add_tmp

protected

Definition at line 227 of file Solver.h.

vec<ShrinkStackElem> Minisat::Solver::analyze_stack

protected

Definition at line 225 of file Solver.h.

vec<Lit> Minisat::Solver::analyze_toclear

protected

Definition at line 226 of file Solver.h.

VMap<lbool> Minisat::Solver::assigns

protected

Definition at line 197 of file Solver.h.

vec<Lit> Minisat::Solver::assumptions

protected

Definition at line 194 of file Solver.h.

bool Minisat::Solver::asynch_interrupt

protected

Definition at line 237 of file Solver.h.

ClauseAllocator Minisat::Solver::ca

protected

Definition at line 216 of file Solver.h.

int Minisat::Solver::ccmin_mode

Definition at line 134 of file Solver.h.

double Minisat::Solver::cla_inc

protected

Definition at line 208 of file Solver.h.

double Minisat::Solver::clause_decay

Definition at line 130 of file Solver.h.

vec<CRef> Minisat::Solver::clauses

protected

Definition at line 190 of file Solver.h.

uint64_t Minisat::Solver::clauses_literals

Definition at line 152 of file Solver.h.

LSet Minisat::Solver::conflict

Definition at line 123 of file Solver.h.

int64_t Minisat::Solver::conflict_budget

protected

Definition at line 235 of file Solver.h.

uint64_t Minisat::Solver::conflicts

Definition at line 151 of file Solver.h.

uint64_t Minisat::Solver::dec_vars

Definition at line 152 of file Solver.h.

VMap<char> Minisat::Solver::decision

protected

Definition at line 200 of file Solver.h.

uint64_t Minisat::Solver::decisions

Definition at line 151 of file Solver.h.

vec<Var> Minisat::Solver::free_vars

protected

Definition at line 219 of file Solver.h.

double Minisat::Solver::garbage_frac

Definition at line 138 of file Solver.h.

vec<CRef> Minisat::Solver::learnts

protected

Definition at line 191 of file Solver.h.

uint64_t Minisat::Solver::learnts_literals

Definition at line 152 of file Solver.h.

int Minisat::Solver::learntsize_adjust_cnt

protected

Definition at line 231 of file Solver.h.

double Minisat::Solver::learntsize_adjust_confl

protected

Definition at line 230 of file Solver.h.

double Minisat::Solver::learntsize_adjust_inc

Definition at line 147 of file Solver.h.

int Minisat::Solver::learntsize_adjust_start_confl

Definition at line 146 of file Solver.h.

double Minisat::Solver::learntsize_factor

Definition at line 143 of file Solver.h.

double Minisat::Solver::learntsize_inc

Definition at line 144 of file Solver.h.

bool Minisat::Solver::luby_restart

Definition at line 133 of file Solver.h.

double Minisat::Solver::max_learnts

protected

Definition at line 229 of file Solver.h.

uint64_t Minisat::Solver::max_literals

Definition at line 152 of file Solver.h.

int Minisat::Solver::min_learnts_lim

Definition at line 139 of file Solver.h.

vec<lbool> Minisat::Solver::model

Definition at line 122 of file Solver.h.

Var Minisat::Solver::next_var

protected

Definition at line 215 of file Solver.h.

uint64_t Minisat::Solver::num_clauses

Definition at line 152 of file Solver.h.

uint64_t Minisat::Solver::num_learnts

Definition at line 152 of file Solver.h.

bool Minisat::Solver::ok

protected

Definition at line 207 of file Solver.h.

Heap<Var,VarOrderLt> Minisat::Solver::order_heap

protected

Definition at line 205 of file Solver.h.

int Minisat::Solver::phase_saving

Definition at line 135 of file Solver.h.

VMap<char> Minisat::Solver::polarity

protected

Definition at line 198 of file Solver.h.

double Minisat::Solver::progress_estimate

protected

Definition at line 213 of file Solver.h.

int64_t Minisat::Solver::propagation_budget

protected

Definition at line 236 of file Solver.h.

uint64_t Minisat::Solver::propagations

Definition at line 151 of file Solver.h.

int Minisat::Solver::qhead

protected

Definition at line 210 of file Solver.h.

double Minisat::Solver::random_seed

Definition at line 132 of file Solver.h.

double Minisat::Solver::random_var_freq

Definition at line 131 of file Solver.h.

vec<Var> Minisat::Solver::released_vars

protected

Definition at line 218 of file Solver.h.

bool Minisat::Solver::remove_satisfied

protected

Definition at line 214 of file Solver.h.

int Minisat::Solver::restart_first

Definition at line 141 of file Solver.h.

double Minisat::Solver::restart_inc

Definition at line 142 of file Solver.h.

uint64_t Minisat::Solver::rnd_decisions

Definition at line 151 of file Solver.h.

bool Minisat::Solver::rnd_init_act

Definition at line 137 of file Solver.h.

bool Minisat::Solver::rnd_pol

Definition at line 136 of file Solver.h.

VMap<char> Minisat::Solver::seen

protected

Definition at line 224 of file Solver.h.

int Minisat::Solver::simpDB_assigns

protected

Definition at line 211 of file Solver.h.

int64_t Minisat::Solver::simpDB_props

protected

Definition at line 212 of file Solver.h.

uint64_t Minisat::Solver::solves

Definition at line 151 of file Solver.h.

uint64_t Minisat::Solver::starts

Definition at line 151 of file Solver.h.

uint64_t Minisat::Solver::tot_literals

Definition at line 152 of file Solver.h.

vec<Lit> Minisat::Solver::trail

protected

Definition at line 192 of file Solver.h.

vec<int> Minisat::Solver::trail_lim

protected

Definition at line 193 of file Solver.h.

VMap<lbool> Minisat::Solver::user_pol

protected

Definition at line 199 of file Solver.h.

double Minisat::Solver::var_decay

Definition at line 129 of file Solver.h.

double Minisat::Solver::var_inc

protected

Definition at line 209 of file Solver.h.

VMap<VarData> Minisat::Solver::vardata

protected

Definition at line 201 of file Solver.h.

int Minisat::Solver::verbosity

Definition at line 128 of file Solver.h.

OccLists<Lit, vec<Watcher>, WatcherDeleted, MkIndexLit> Minisat::Solver::watches

protected

Definition at line 203 of file Solver.h.

---

The documentation for this class was generated from the following files:

• Solver.h
• Solver.cc