Minisat::SimpSolver Class Reference

#include <SimpSolver.h>

Inheritance diagram for Minisat::SimpSolver:

Collaboration diagram for Minisat::SimpSolver:

Data Structures
struct	ClauseDeleted
struct	ElimLt

Public Member Functions
	SimpSolver ()
	~SimpSolver ()
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	substitute (Var v, Lit x)
void	setFrozen (Var v, bool b)
bool	isEliminated (Var v) const
void	freezeVar (Var v)
void	thaw ()
bool	solve (const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)
lbool	solveLimited (const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false)
bool	solve (bool do_simp=true, bool turn_off_simp=false)
bool	solve (Lit p, bool do_simp=true, bool turn_off_simp=false)
bool	solve (Lit p, Lit q, bool do_simp=true, bool turn_off_simp=false)
bool	solve (Lit p, Lit q, Lit r, bool do_simp=true, bool turn_off_simp=false)
bool	eliminate (bool turn_off_elim=false)
virtual void	garbageCollect ()
bool	simplify ()
bool	solve (const vec< Lit > &assumps)
bool	solve ()
bool	solve (Lit p)
bool	solve (Lit p, Lit q)
bool	solve (Lit p, Lit q, Lit r)
lbool	solveLimited (const vec< Lit > &assumps)
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 ()
void	checkGarbage (double gf)
void	checkGarbage ()

Data Fields
int	grow
int	clause_lim
int	subsumption_lim
double	simp_garbage_frac
bool	use_asymm
bool	use_rcheck
bool	use_elim
bool	extend_model
int	merges
int	asymm_lits
int	eliminated_vars
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
lbool	solve_ (bool do_simp=true, bool turn_off_simp=false)
bool	asymm (Var v, CRef cr)
bool	asymmVar (Var v)
void	updateElimHeap (Var v)
void	gatherTouchedClauses ()
bool	merge (const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause)
bool	merge (const Clause &_ps, const Clause &_qs, Var v, int &size)
bool	backwardSubsumptionCheck (bool verbose=false)
bool	eliminateVar (Var v)
void	extendModel ()
void	removeClause (CRef cr)
bool	strengthenClause (CRef cr, Lit l)
bool	implied (const vec< Lit > &c)
void	relocAll (ClauseAllocator &to)
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)
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

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
int	elimorder
bool	use_simplification
Var	max_simp_var
vec< uint32_t >	elimclauses
VMap< char >	touched
OccLists< Var, vec< CRef > , ClauseDeleted >	occurs
LMap< int >	n_occ
Heap< Var, ElimLt >	elim_heap
Queue< CRef >	subsumption_queue
VMap< char >	frozen
vec< Var >	frozen_vars
VMap< char >	eliminated
int	bwdsub_assigns
int	n_touched
CRef	bwdsub_tmpunit
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 33 of file SimpSolver.h.

Constructor & Destructor Documentation

SimpSolver::SimpSolver

(

)

Definition at line 48 of file SimpSolver.cc.

                       :
    grow               (opt_grow)
  , clause_lim         (opt_clause_lim)
  , subsumption_lim    (opt_subsumption_lim)
  , simp_garbage_frac  (opt_simp_garbage_frac)
  , use_asymm          (opt_use_asymm)
  , use_rcheck         (opt_use_rcheck)
  , use_elim           (opt_use_elim)
  , extend_model       (true)
  , merges             (0)
  , asymm_lits         (0)
  , eliminated_vars    (0)
  , elimorder          (1)
  , use_simplification (true)
  , occurs             (ClauseDeleted(ca))
  , elim_heap          (ElimLt(n_occ))
  , bwdsub_assigns     (0)
  , n_touched          (0)
{
    vec<Lit> dummy(1,lit_Undef);
    ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
    bwdsub_tmpunit        = ca.alloc(dummy);
    remove_satisfied      = false;
}

Here is the call graph for this function:

SimpSolver::~SimpSolver

(

)

Definition at line 74 of file SimpSolver.cc.

{
}

Member Function Documentation

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

inlineprotectedinherited

Definition at line 349 of file Solver.h.

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

Here is the call graph for this function:

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

inline

Definition at line 186 of file SimpSolver.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::SimpSolver::addClause ( Lit  p )

inline

Definition at line 188 of file SimpSolver.h.

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

Here is the call graph for this function:

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

inline

Definition at line 189 of file SimpSolver.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::SimpSolver::addClause ( Lit  p, Lit  q, Lit  r  )

inline

Definition at line 190 of file SimpSolver.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::SimpSolver::addClause ( Lit  p, Lit  q, Lit  r, Lit  s  )

inline

Definition at line 191 of file SimpSolver.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 SimpSolver::addClause_

(

vec< Lit > &

ps

)

Definition at line 150 of file SimpSolver.cc.

{
#ifndef NDEBUG
    for (int i = 0; i < ps.size(); i++)
        assert(!isEliminated(var(ps[i])));
#endif

    int nclauses = clauses.size();

    if (use_rcheck && implied(ps))
        return true;

    if (!Solver::addClause_(ps))
        return false;

    if (use_simplification && clauses.size() == nclauses + 1){
        CRef          cr = clauses.last();
        const Clause& c  = ca[cr];

        // NOTE: the clause is added to the queue immediately and then
        // again during 'gatherTouchedClauses()'. If nothing happens
        // in between, it will only be checked once. Otherwise, it may
        // be checked twice unnecessarily. This is an unfortunate
        // consequence of how backward subsumption is used to mimic
        // forward subsumption.
        subsumption_queue.insert(cr);
        for (int i = 0; i < c.size(); i++){
            occurs[var(c[i])].push(cr);
            n_occ[c[i]]++;
            touched[var(c[i])] = 1;
            n_touched++;
            if (elim_heap.inHeap(var(c[i])))
                elim_heap.increase(var(c[i]));
        }
    }

    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool Minisat::SimpSolver::addEmptyClause ( )

inline

Definition at line 187 of file SimpSolver.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  )

protectedinherited

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  )

protectedinherited

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:

bool SimpSolver::asymm ( Var  v, CRef  cr  )

protected

Definition at line 410 of file SimpSolver.cc.

{
    Clause& c = ca[cr];
    assert(decisionLevel() == 0);

    if (c.mark() || satisfied(c)) return true;

    trail_lim.push(trail.size());
    Lit l = lit_Undef;
    for (int i = 0; i < c.size(); i++)
        if (var(c[i]) != v && value(c[i]) != l_False)
            uncheckedEnqueue(~c[i]);
        else
            l = c[i];

    if (propagate() != CRef_Undef){
        cancelUntil(0);
        asymm_lits++;
        if (!strengthenClause(cr, l))
            return false;
    }else
        cancelUntil(0);

    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool SimpSolver::asymmVar ( Var  v )

protected

Definition at line 437 of file SimpSolver.cc.

{
    assert(use_simplification);

    const vec<CRef>& cls = occurs.lookup(v);

    if (value(v) != l_Undef || cls.size() == 0)
        return true;

    for (int i = 0; i < cls.size(); i++)
        if (!asymm(v, cls[i]))
            return false;

    return backwardSubsumptionCheck();
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Solver::attachClause ( CRef  cr )

protectedinherited

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:

bool SimpSolver::backwardSubsumptionCheck ( bool  verbose = false )

protected

Definition at line 343 of file SimpSolver.cc.

{
    int cnt = 0;
    int subsumed = 0;
    int deleted_literals = 0;
    assert(decisionLevel() == 0);

    while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){

        // Empty subsumption queue and return immediately on user-interrupt:
        if (asynch_interrupt){
            subsumption_queue.clear();
            bwdsub_assigns = trail.size();
            break; }

        // Check top-level assignments by creating a dummy clause and placing it in the queue:
        if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
            Lit l = trail[bwdsub_assigns++];
            ca[bwdsub_tmpunit][0] = l;
            ca[bwdsub_tmpunit].calcAbstraction();
            subsumption_queue.insert(bwdsub_tmpunit); }

        CRef    cr = subsumption_queue.peek(); subsumption_queue.pop();
        Clause& c  = ca[cr];

        if (c.mark()) continue;

        if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
            printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);

        assert(c.size() > 1 || value(c[0]) == l_True);    // Unit-clauses should have been propagated before this point.

        // Find best variable to scan:
        Var best = var(c[0]);
        for (int i = 1; i < c.size(); i++)
            if (occurs[var(c[i])].size() < occurs[best].size())
                best = var(c[i]);

        // Search all candidates:
        vec<CRef>& _cs = occurs.lookup(best);
        CRef*       cs = (CRef*)_cs;

        for (int j = 0; j < _cs.size(); j++)
            if (c.mark())
                break;
            else if (!ca[cs[j]].mark() &&  cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
                Lit l = c.subsumes(ca[cs[j]]);

                if (l == lit_Undef)
                    subsumed++, removeClause(cs[j]);
                else if (l != lit_Error){
                    deleted_literals++;

                    if (!strengthenClause(cs[j], ~l))
                        return false;

                    // Did current candidate get deleted from cs? Then check candidate at index j again:
                    if (var(l) == best)
                        j--;
                }
            }
    }

    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::Solver::budgetOff ( )

inlineinherited

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 )

protectedinherited

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 )

inlineinherited

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  )

inlineinherited

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 )

inlineprotectedinherited

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 ( )

inlineprotectedinherited

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

inlineinherited

Definition at line 390 of file Solver.h.

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

ClauseIterator Minisat::Solver::clausesEnd ( ) const

inlineinherited

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 ( )

inlineinherited

Definition at line 372 of file Solver.h.

{ asynch_interrupt = false; }

int Minisat::Solver::decisionLevel ( ) const

inlineprotectedinherited

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  )

protectedinherited

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 )

inlinestaticprotectedinherited

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 SimpSolver::eliminate

(

bool

turn_off_elim = false

)

Definition at line 597 of file SimpSolver.cc.

{
    if (!simplify())
        return false;
    else if (!use_simplification)
        return true;

    // Main simplification loop:
    //
    while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){

        gatherTouchedClauses();
        // printf("  ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
        if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && 
            !backwardSubsumptionCheck(true)){
            ok = false; goto cleanup; }

        // Empty elim_heap and return immediately on user-interrupt:
        if (asynch_interrupt){
            assert(bwdsub_assigns == trail.size());
            assert(subsumption_queue.size() == 0);
            assert(n_touched == 0);
            elim_heap.clear();
            goto cleanup; }

        // printf("  ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
        for (int cnt = 0; !elim_heap.empty(); cnt++){
            Var elim = elim_heap.removeMin();
            
            if (asynch_interrupt) break;

            if (isEliminated(elim) || value(elim) != l_Undef) continue;

            if (verbosity >= 2 && cnt % 100 == 0)
                printf("elimination left: %10d\r", elim_heap.size());

            if (use_asymm){
                // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
                bool was_frozen = frozen[elim];
                frozen[elim] = true;
                if (!asymmVar(elim)){
                    ok = false; goto cleanup; }
                frozen[elim] = was_frozen; }

            // At this point, the variable may have been set by assymetric branching, so check it
            // again. Also, don't eliminate frozen variables:
            if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
                ok = false; goto cleanup; }

            checkGarbage(simp_garbage_frac);
        }

        assert(subsumption_queue.size() == 0);
    }
 cleanup:

    // If no more simplification is needed, free all simplification-related data structures:
    if (turn_off_elim){
        touched  .clear(true);
        occurs   .clear(true);
        n_occ    .clear(true);
        elim_heap.clear(true);
        subsumption_queue.clear(true);

        use_simplification    = false;
        remove_satisfied      = true;
        ca.extra_clause_field = false;
        max_simp_var          = nVars();

        // Force full cleanup (this is safe and desirable since it only happens once):
        rebuildOrderHeap();
        garbageCollect();
    }else{
        // Cheaper cleanup:
        checkGarbage();
    }

    if (verbosity >= 1 && elimclauses.size() > 0)
        printf("|  Eliminated clauses:     %10.2f Mb                                      |\n", 
               double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));

    return ok;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool SimpSolver::eliminateVar ( Var  v )

protected

Definition at line 487 of file SimpSolver.cc.

{
    assert(!frozen[v]);
    assert(!isEliminated(v));
    assert(value(v) == l_Undef);

    // Split the occurrences into positive and negative:
    //
    const vec<CRef>& cls = occurs.lookup(v);
    vec<CRef>        pos, neg;
    for (int i = 0; i < cls.size(); i++)
        (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);

    // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
    // clause must exceed the limit on the maximal clause size (if it is set):
    //
    int cnt         = 0;
    int clause_size = 0;

    for (int i = 0; i < pos.size(); i++)
        for (int j = 0; j < neg.size(); j++)
            if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && 
                (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
                return true;

    // Delete and store old clauses:
    eliminated[v] = true;
    setDecisionVar(v, false);
    eliminated_vars++;

    if (pos.size() > neg.size()){
        for (int i = 0; i < neg.size(); i++)
            mkElimClause(elimclauses, v, ca[neg[i]]);
        mkElimClause(elimclauses, mkLit(v));
    }else{
        for (int i = 0; i < pos.size(); i++)
            mkElimClause(elimclauses, v, ca[pos[i]]);
        mkElimClause(elimclauses, ~mkLit(v));
    }

    for (int i = 0; i < cls.size(); i++)
        removeClause(cls[i]); 

    // Produce clauses in cross product:
    vec<Lit>& resolvent = add_tmp;
    for (int i = 0; i < pos.size(); i++)
        for (int j = 0; j < neg.size(); j++)
            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
                return false;

    // Free occurs list for this variable:
    occurs[v].clear(true);
    
    // Free watchers lists for this variable, if possible:
    if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
    if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);

    return backwardSubsumptionCheck();
}

Here is the call graph for this function:

Here is the caller graph for this function:

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

inlineprotectedinherited

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 SimpSolver::extendModel ( )

protected

Definition at line 580 of file SimpSolver.cc.

{
    int i, j;
    Lit x;

    for (i = elimclauses.size()-1; i > 0; i -= j){
        for (j = elimclauses[i--]; j > 1; j--, i--)
            if (modelValue(toLit(elimclauses[i])) != l_False)
                goto next;

        x = toLit(elimclauses[i]);
        model[var(x)] = lbool(!sign(x));
    next:;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void Minisat::SimpSolver::freezeVar ( Var  v )

inline

Definition at line 194 of file SimpSolver.h.

                                      {
    if (!frozen[v]){
        frozen[v] = 1;
        frozen_vars.push(v); 
    } }

Here is the call graph for this function:

void SimpSolver::garbageCollect ( )

virtual

Reimplemented from Minisat::Solver.

Definition at line 714 of file SimpSolver.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()); 

    to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
    relocAll(to);
    Solver::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:

void SimpSolver::gatherTouchedClauses ( )

protected

Definition at line 294 of file SimpSolver.cc.

{
    if (n_touched == 0) return;

    int i,j;
    for (i = j = 0; i < subsumption_queue.size(); i++)
        if (ca[subsumption_queue[i]].mark() == 0)
            ca[subsumption_queue[i]].mark(2);

    for (i = 0; i < nVars(); i++)
        if (touched[i]){
            const vec<CRef>& cs = occurs.lookup(i);
            for (j = 0; j < cs.size(); j++)
                if (ca[cs[j]].mark() == 0){
                    subsumption_queue.insert(cs[j]);
                    ca[cs[j]].mark(2);
                }
            touched[i] = 0;
        }

    for (i = 0; i < subsumption_queue.size(); i++)
        if (ca[subsumption_queue[i]].mark() == 2)
            ca[subsumption_queue[i]].mark(0);

    n_touched = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool SimpSolver::implied ( const vec< Lit > &  c )

protected

Definition at line 322 of file SimpSolver.cc.

{
    assert(decisionLevel() == 0);

    trail_lim.push(trail.size());
    for (int i = 0; i < c.size(); i++)
        if (value(c[i]) == l_True){
            cancelUntil(0);
            return true;
        }else if (value(c[i]) != l_False){
            assert(value(c[i]) == l_Undef);
            uncheckedEnqueue(~c[i]);
        }

    bool result = propagate() != CRef_Undef;
    cancelUntil(0);
    return result;
}

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  )

inherited

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 )

inlineprotectedinherited

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 ( )

inlineinherited

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  )

inlinestaticprotectedinherited

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::SimpSolver::isEliminated ( Var  v ) const

inline

Definition at line 178 of file SimpSolver.h.

{ return eliminated[v]; }

Here is the caller graph for this function:

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

inlineprotectedinherited

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

inlineprotectedinherited

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 )

protectedinherited

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

inlineprotectedinherited

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:

bool SimpSolver::merge ( const Clause &  _ps, const Clause &  _qs, Var  v, vec< Lit > &  out_clause  )

protected

Definition at line 232 of file SimpSolver.cc.

{
    merges++;
    out_clause.clear();

    bool  ps_smallest = _ps.size() < _qs.size();
    const Clause& ps  =  ps_smallest ? _qs : _ps;
    const Clause& qs  =  ps_smallest ? _ps : _qs;

    for (int i = 0; i < qs.size(); i++){
        if (var(qs[i]) != v){
            for (int j = 0; j < ps.size(); j++)
                if (var(ps[j]) == var(qs[i])){
                    if (ps[j] == ~qs[i])
                        return false;
                    else
                        goto next;
                }
            out_clause.push(qs[i]);
        }
        next:;
    }

    for (int i = 0; i < ps.size(); i++)
        if (var(ps[i]) != v)
            out_clause.push(ps[i]);

    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool SimpSolver::merge ( const Clause &  _ps, const Clause &  _qs, Var  v, int &  size  )

protected

Definition at line 264 of file SimpSolver.cc.

{
    merges++;

    bool  ps_smallest = _ps.size() < _qs.size();
    const Clause& ps  =  ps_smallest ? _qs : _ps;
    const Clause& qs  =  ps_smallest ? _ps : _qs;
    const Lit*  __ps  = (const Lit*)ps;
    const Lit*  __qs  = (const Lit*)qs;

    size = ps.size()-1;

    for (int i = 0; i < qs.size(); i++){
        if (var(__qs[i]) != v){
            for (int j = 0; j < ps.size(); j++)
                if (var(__ps[j]) == var(__qs[i])){
                    if (__ps[j] == ~__qs[i])
                        return false;
                    else
                        goto next;
                }
            size++;
        }
        next:;
    }

    return true;
}

Here is the call graph for this function:

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

inlinestaticprotectedinherited

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

inlineinherited

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

inlineinherited

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

inlineinherited

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

inlineinherited

Definition at line 355 of file Solver.h.

{ return num_clauses; }

Here is the caller graph for this function:

void Minisat::Solver::newDecisionLevel ( )

inlineprotectedinherited

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 SimpSolver::newVar	(	lbool	upol = l_Undef,
		bool	dvar = true
	)

Definition at line 79 of file SimpSolver.cc.

                                            {
    Var v = Solver::newVar(upol, dvar);

    frozen    .insert(v, (char)false);
    eliminated.insert(v, (char)false);

    if (use_simplification){
        n_occ     .insert( mkLit(v), 0);
        n_occ     .insert(~mkLit(v), 0);
        occurs    .init  (v);
        touched   .insert(v, 0);
        elim_heap .insert(v);
    }
    return v; }

Here is the call graph for this function:

Here is the caller graph for this function:

int Minisat::Solver::nFreeVars ( ) const

inlineinherited

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

inlineinherited

Definition at line 356 of file Solver.h.

{ return num_learnts; }

Here is the caller graph for this function:

int Minisat::Solver::nVars ( ) const

inlineinherited

Definition at line 357 of file Solver.h.

{ return next_var; }

Here is the caller graph for this function:

bool Minisat::Solver::okay ( ) const

inlineinherited

Definition at line 388 of file Solver.h.

{ return ok; }

Lit Solver::pickBranchLit ( )

protectedinherited

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

inherited

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

protectedinherited

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 ( )

protectedinherited

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

inlineprotectedinherited

Definition at line 303 of file Solver.h.

{ return vardata[x].reason; }

Here is the caller graph for this function:

void Solver::rebuildOrderHeap ( )

protectedinherited

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 ( )

protectedinherited

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 SimpSolver::releaseVar

(

Lit

l

)

Definition at line 95 of file SimpSolver.cc.

{
    assert(!isEliminated(var(l)));
    if (!use_simplification && var(l) >= max_simp_var)
        // Note: Guarantees that no references to this variable is
        // left in model extension datastructure. Could be improved!
        Solver::releaseVar(l);
    else
        // Otherwise, don't allow variable to be reused.
        Solver::addClause(l);
}

Here is the call graph for this function:

void SimpSolver::relocAll ( ClauseAllocator &  to )

protected

Definition at line 686 of file SimpSolver.cc.

{
    if (!use_simplification) return;

    // All occurs lists:
    //
    for (int i = 0; i < nVars(); i++){
        occurs.clean(i);
        vec<CRef>& cs = occurs[i];
        for (int j = 0; j < cs.size(); j++)
            ca.reloc(cs[j], to);
    }

    // Subsumption queue:
    //
    for (int i = subsumption_queue.size(); i > 0; i--){
        CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
        if (ca[cr].mark()) continue;
        ca.reloc(cr, to);
        subsumption_queue.insert(cr);
    }
        
    // Temporary clause:
    //
    ca.reloc(bwdsub_tmpunit, to);
}

Here is the call graph for this function:

Here is the caller graph for this function:

void SimpSolver::removeClause ( CRef  cr )

protected

Definition at line 190 of file SimpSolver.cc.

{
    const Clause& c = ca[cr];

    if (use_simplification)
        for (int i = 0; i < c.size(); i++){
            n_occ[c[i]]--;
            updateElimHeap(var(c[i]));
            occurs.smudge(var(c[i]));
        }

    Solver::removeClause(cr);
}

Here is the call graph for this function:

Here is the caller graph for this function:

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

protectedinherited

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

protectedinherited

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 )

protectedinherited

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 )

inlineinherited

Definition at line 369 of file Solver.h.

{ conflict_budget    = conflicts    + x; }

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

inlineinherited

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::SimpSolver::setFrozen ( Var  v, bool  b  )

inline

Definition at line 192 of file SimpSolver.h.

{ frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(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  )

inlineinherited

Definition at line 360 of file Solver.h.

{ user_pol[v] = b; }

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

inlineinherited

Definition at line 370 of file Solver.h.

{ propagation_budget = propagations + x; }

bool Solver::simplify ( )

inherited

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 )

inlineinherited

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 ( )

inlineinherited

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 )

inlineinherited

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::SimpSolver::solve ( const vec< Lit > &  assumps, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 213 of file SimpSolver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

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

inlineinherited

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  )

inlineinherited

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:

bool Minisat::SimpSolver::solve ( bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 209 of file SimpSolver.h.

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

Here is the call graph for this function:

bool Minisat::SimpSolver::solve ( Lit  p, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 210 of file SimpSolver.h.

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

Here is the call graph for this function:

bool Minisat::SimpSolver::solve ( Lit  p, Lit  q, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 211 of file SimpSolver.h.

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

Here is the call graph for this function:

bool Minisat::SimpSolver::solve ( Lit  p, Lit  q, Lit  r, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 212 of file SimpSolver.h.

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

Here is the call graph for this function:

lbool SimpSolver::solve_ ( bool  do_simp = true, bool  turn_off_simp = false  )

protected

Definition at line 108 of file SimpSolver.cc.

{
    vec<Var> extra_frozen;
    lbool    result = l_True;

    do_simp &= use_simplification;

    if (do_simp){
        // Assumptions must be temporarily frozen to run variable elimination:
        for (int i = 0; i < assumptions.size(); i++){
            Var v = var(assumptions[i]);

            // If an assumption has been eliminated, remember it.
            assert(!isEliminated(v));

            if (!frozen[v]){
                // Freeze and store.
                setFrozen(v, true);
                extra_frozen.push(v);
            } }

        result = lbool(eliminate(turn_off_simp));
    }

    if (result == l_True)
        result = Solver::solve_();
    else if (verbosity >= 1)
        printf("===============================================================================\n");

    if (result == l_True && extend_model)
        extendModel();

    if (do_simp)
        // Unfreeze the assumptions that were frozen:
        for (int i = 0; i < extra_frozen.size(); i++)
            setFrozen(extra_frozen[i], false);

    return result;
}

Here is the call graph for this function:

lbool Solver::solve_ ( )

protectedinherited

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 )

inlineinherited

Definition at line 387 of file Solver.h.

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

Here is the call graph for this function:

lbool Minisat::SimpSolver::solveLimited ( const vec< Lit > &  assumps, bool  do_simp = true, bool  turn_off_simp = false  )

inline

Definition at line 216 of file SimpSolver.h.

                                                                                               { 
    assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }

Here is the call graph for this function:

bool SimpSolver::strengthenClause ( CRef  cr, Lit  l  )

protected

Definition at line 205 of file SimpSolver.cc.

{
    Clause& c = ca[cr];
    assert(decisionLevel() == 0);
    assert(use_simplification);

    // FIX: this is too inefficient but would be nice to have (properly implemented)
    // if (!find(subsumption_queue, &c))
    subsumption_queue.insert(cr);

    if (c.size() == 2){
        removeClause(cr);
        c.strengthen(l);
    }else{
        detachClause(cr, true);
        c.strengthen(l);
        attachClause(cr);
        remove(occurs[var(l)], cr);
        n_occ[l]--;
        updateElimHeap(var(l));
    }

    return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

bool SimpSolver::substitute	(	Var	v,
		Lit	x
	)

Definition at line 548 of file SimpSolver.cc.

{
    assert(!frozen[v]);
    assert(!isEliminated(v));
    assert(value(v) == l_Undef);

    if (!ok) return false;

    eliminated[v] = true;
    setDecisionVar(v, false);
    const vec<CRef>& cls = occurs.lookup(v);
    
    vec<Lit>& subst_clause = add_tmp;
    for (int i = 0; i < cls.size(); i++){
        Clause& c = ca[cls[i]];

        subst_clause.clear();
        for (int j = 0; j < c.size(); j++){
            Lit p = c[j];
            subst_clause.push(var(p) == v ? x ^ sign(p) : p);
        }

        removeClause(cls[i]);

        if (!addClause_(subst_clause))
            return ok = false;
    }

    return true;
}

Here is the call graph for this function:

void Minisat::SimpSolver::thaw ( )

inline

Definition at line 200 of file SimpSolver.h.

                            {
    for (int i = 0; i < frozen_vars.size(); i++){
        Var v = frozen_vars[i];
        frozen[v] = 0;
        if (use_simplification)
            updateElimHeap(v);
    }
    frozen_vars.clear(); }

Here is the call graph for this function:

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

inherited

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  )

inherited

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  )

inherited

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 )

inlineinherited

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  )

inlineinherited

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  )

inlineinherited

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  )

inlineinherited

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

inlineinherited

Definition at line 392 of file Solver.h.

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

TrailIterator Minisat::Solver::trailEnd ( ) const

inlineinherited

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  )

protectedinherited

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:

void Minisat::SimpSolver::updateElimHeap ( Var  v )

inlineprotected

Definition at line 179 of file SimpSolver.h.

                                            {
    assert(use_simplification);
    // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
    if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
        elim_heap.update(v); }

Here is the call graph for this function:

Here is the caller graph for this function:

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

inlineinherited

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

inlineinherited

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  )

inlineprotectedinherited

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 )

inlineprotectedinherited

Definition at line 310 of file Solver.h.

{ varBumpActivity(v, var_inc); }

Here is the call graph for this function:

void Minisat::Solver::varDecayActivity ( )

inlineprotectedinherited

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

inlineprotectedinherited

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

protectedinherited

Definition at line 196 of file Solver.h.

vec<Lit> Minisat::Solver::add_tmp

protectedinherited

Definition at line 227 of file Solver.h.

vec<ShrinkStackElem> Minisat::Solver::analyze_stack

protectedinherited

Definition at line 225 of file Solver.h.

vec<Lit> Minisat::Solver::analyze_toclear

protectedinherited

Definition at line 226 of file Solver.h.

VMap<lbool> Minisat::Solver::assigns

protectedinherited

Definition at line 197 of file Solver.h.

vec<Lit> Minisat::Solver::assumptions

protectedinherited

Definition at line 194 of file Solver.h.

int Minisat::SimpSolver::asymm_lits

Definition at line 104 of file SimpSolver.h.

bool Minisat::Solver::asynch_interrupt

protectedinherited

Definition at line 237 of file Solver.h.

int Minisat::SimpSolver::bwdsub_assigns

protected

Definition at line 147 of file SimpSolver.h.

CRef Minisat::SimpSolver::bwdsub_tmpunit

protected

Definition at line 152 of file SimpSolver.h.

ClauseAllocator Minisat::Solver::ca

protectedinherited

Definition at line 216 of file Solver.h.

int Minisat::Solver::ccmin_mode

inherited

Definition at line 134 of file Solver.h.

double Minisat::Solver::cla_inc

protectedinherited

Definition at line 208 of file Solver.h.

double Minisat::Solver::clause_decay

inherited

Definition at line 130 of file Solver.h.

int Minisat::SimpSolver::clause_lim

Definition at line 91 of file SimpSolver.h.

vec<CRef> Minisat::Solver::clauses

protectedinherited

Definition at line 190 of file Solver.h.

uint64_t Minisat::Solver::clauses_literals

inherited

Definition at line 152 of file Solver.h.

LSet Minisat::Solver::conflict

inherited

Definition at line 123 of file Solver.h.

int64_t Minisat::Solver::conflict_budget

protectedinherited

Definition at line 235 of file Solver.h.

uint64_t Minisat::Solver::conflicts

inherited

Definition at line 151 of file Solver.h.

uint64_t Minisat::Solver::dec_vars

inherited

Definition at line 152 of file Solver.h.

VMap<char> Minisat::Solver::decision

protectedinherited

Definition at line 200 of file Solver.h.

uint64_t Minisat::Solver::decisions

inherited

Definition at line 151 of file Solver.h.

Heap<Var,ElimLt> Minisat::SimpSolver::elim_heap

protected

Definition at line 142 of file SimpSolver.h.

vec<uint32_t> Minisat::SimpSolver::elimclauses

protected

Definition at line 137 of file SimpSolver.h.

VMap<char> Minisat::SimpSolver::eliminated

protected

Definition at line 146 of file SimpSolver.h.

int Minisat::SimpSolver::eliminated_vars

Definition at line 105 of file SimpSolver.h.

int Minisat::SimpSolver::elimorder

protected

Definition at line 134 of file SimpSolver.h.

bool Minisat::SimpSolver::extend_model

Definition at line 99 of file SimpSolver.h.

vec<Var> Minisat::Solver::free_vars

protectedinherited

Definition at line 219 of file Solver.h.

VMap<char> Minisat::SimpSolver::frozen

protected

Definition at line 144 of file SimpSolver.h.

vec<Var> Minisat::SimpSolver::frozen_vars

protected

Definition at line 145 of file SimpSolver.h.

double Minisat::Solver::garbage_frac

inherited

Definition at line 138 of file Solver.h.

int Minisat::SimpSolver::grow

Definition at line 90 of file SimpSolver.h.

vec<CRef> Minisat::Solver::learnts

protectedinherited

Definition at line 191 of file Solver.h.

uint64_t Minisat::Solver::learnts_literals

inherited

Definition at line 152 of file Solver.h.

int Minisat::Solver::learntsize_adjust_cnt

protectedinherited

Definition at line 231 of file Solver.h.

double Minisat::Solver::learntsize_adjust_confl

protectedinherited

Definition at line 230 of file Solver.h.

double Minisat::Solver::learntsize_adjust_inc

inherited

Definition at line 147 of file Solver.h.

int Minisat::Solver::learntsize_adjust_start_confl

inherited

Definition at line 146 of file Solver.h.

double Minisat::Solver::learntsize_factor

inherited

Definition at line 143 of file Solver.h.

double Minisat::Solver::learntsize_inc

inherited

Definition at line 144 of file Solver.h.

bool Minisat::Solver::luby_restart

inherited

Definition at line 133 of file Solver.h.

double Minisat::Solver::max_learnts

protectedinherited

Definition at line 229 of file Solver.h.

uint64_t Minisat::Solver::max_literals

inherited

Definition at line 152 of file Solver.h.

Var Minisat::SimpSolver::max_simp_var

protected

Definition at line 136 of file SimpSolver.h.

int Minisat::SimpSolver::merges

Definition at line 103 of file SimpSolver.h.

int Minisat::Solver::min_learnts_lim

inherited

Definition at line 139 of file Solver.h.

vec<lbool> Minisat::Solver::model

inherited

Definition at line 122 of file Solver.h.

LMap<int> Minisat::SimpSolver::n_occ

protected

Definition at line 141 of file SimpSolver.h.

int Minisat::SimpSolver::n_touched

protected

Definition at line 148 of file SimpSolver.h.

Var Minisat::Solver::next_var

protectedinherited

Definition at line 215 of file Solver.h.

uint64_t Minisat::Solver::num_clauses

inherited

Definition at line 152 of file Solver.h.

uint64_t Minisat::Solver::num_learnts

inherited

Definition at line 152 of file Solver.h.

OccLists<Var, vec<CRef>, ClauseDeleted> Minisat::SimpSolver::occurs

protected

Definition at line 140 of file SimpSolver.h.

bool Minisat::Solver::ok

protectedinherited

Definition at line 207 of file Solver.h.

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

protectedinherited

Definition at line 205 of file Solver.h.

int Minisat::Solver::phase_saving

inherited

Definition at line 135 of file Solver.h.

VMap<char> Minisat::Solver::polarity

protectedinherited

Definition at line 198 of file Solver.h.

double Minisat::Solver::progress_estimate

protectedinherited

Definition at line 213 of file Solver.h.

int64_t Minisat::Solver::propagation_budget

protectedinherited

Definition at line 236 of file Solver.h.

uint64_t Minisat::Solver::propagations

inherited

Definition at line 151 of file Solver.h.

int Minisat::Solver::qhead

protectedinherited

Definition at line 210 of file Solver.h.

double Minisat::Solver::random_seed

inherited

Definition at line 132 of file Solver.h.

double Minisat::Solver::random_var_freq

inherited

Definition at line 131 of file Solver.h.

vec<Var> Minisat::Solver::released_vars

protectedinherited

Definition at line 218 of file Solver.h.

bool Minisat::Solver::remove_satisfied

protectedinherited

Definition at line 214 of file Solver.h.

int Minisat::Solver::restart_first

inherited

Definition at line 141 of file Solver.h.

double Minisat::Solver::restart_inc

inherited

Definition at line 142 of file Solver.h.

uint64_t Minisat::Solver::rnd_decisions

inherited

Definition at line 151 of file Solver.h.

bool Minisat::Solver::rnd_init_act

inherited

Definition at line 137 of file Solver.h.

bool Minisat::Solver::rnd_pol

inherited

Definition at line 136 of file Solver.h.

VMap<char> Minisat::Solver::seen

protectedinherited

Definition at line 224 of file Solver.h.

double Minisat::SimpSolver::simp_garbage_frac

Definition at line 94 of file SimpSolver.h.

int Minisat::Solver::simpDB_assigns

protectedinherited

Definition at line 211 of file Solver.h.

int64_t Minisat::Solver::simpDB_props

protectedinherited

Definition at line 212 of file Solver.h.

uint64_t Minisat::Solver::solves

inherited

Definition at line 151 of file Solver.h.

uint64_t Minisat::Solver::starts

inherited

Definition at line 151 of file Solver.h.

int Minisat::SimpSolver::subsumption_lim

Definition at line 93 of file SimpSolver.h.

Queue<CRef> Minisat::SimpSolver::subsumption_queue

protected

Definition at line 143 of file SimpSolver.h.

uint64_t Minisat::Solver::tot_literals

inherited

Definition at line 152 of file Solver.h.

VMap<char> Minisat::SimpSolver::touched

protected

Definition at line 138 of file SimpSolver.h.

vec<Lit> Minisat::Solver::trail

protectedinherited

Definition at line 192 of file Solver.h.

vec<int> Minisat::Solver::trail_lim

protectedinherited

Definition at line 193 of file Solver.h.

bool Minisat::SimpSolver::use_asymm

Definition at line 96 of file SimpSolver.h.

bool Minisat::SimpSolver::use_elim

Definition at line 98 of file SimpSolver.h.

bool Minisat::SimpSolver::use_rcheck

Definition at line 97 of file SimpSolver.h.

bool Minisat::SimpSolver::use_simplification

protected

Definition at line 135 of file SimpSolver.h.

VMap<lbool> Minisat::Solver::user_pol

protectedinherited

Definition at line 199 of file Solver.h.

double Minisat::Solver::var_decay

inherited

Definition at line 129 of file Solver.h.

double Minisat::Solver::var_inc

protectedinherited

Definition at line 209 of file Solver.h.

VMap<VarData> Minisat::Solver::vardata

protectedinherited

Definition at line 201 of file Solver.h.

int Minisat::Solver::verbosity

inherited

Definition at line 128 of file Solver.h.

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

protectedinherited

Definition at line 203 of file Solver.h.

---

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

• SimpSolver.h
• SimpSolver.cc