#include <SimpSolver.h>

Inheritance diagram for Minisat::SimpSolver:

Collaboration diagram for Minisat::SimpSolver:

[legend]

Classes
struct	ClauseDeleted

struct	ElimLt

Public Member Functions
	SimpSolver ()

	~SimpSolver ()

Var	newVar (bool polarity=true, bool dvar=true)

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_ (vec< Lit > &ps)

bool	substitute (Var v, Lit x)

void	setFrozen (Var v, bool b)

bool	isEliminated (Var v) const

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

Public Member Functions inherited from Minisat::Solver
	Solver ()

virtual	~Solver ()

Var	newVar (bool polarity=true, bool dvar=true)

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

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, bool 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	setConfBudget (int64_t x)

void	setPropBudget (int64_t x)

void	budgetOff ()

void	interrupt ()

void	clearInterrupt ()

void	checkGarbage (double gf)

void	checkGarbage ()

Public Attributes
int	grow

int	clause_lim

int	subsumption_lim

double	simp_garbage_frac

bool	use_asymm

bool	use_rcheck

bool	use_elim

int	merges

int	asymm_lits

int	eliminated_vars

Public Attributes inherited from Minisat::Solver
vec< lbool >	model

vec< Lit >	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	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	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)

void	cleanUpClauses ()

bool	implied (const vec< Lit > &c)

void	relocAll (ClauseAllocator &to)

Protected Member Functions inherited from Minisat::Solver
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, vec< Lit > &out_conflict)

bool	litRedundant (Lit p, uint32_t abstract_levels)

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	locked (const Clause &c) const

bool	satisfied (const Clause &c) const

void	relocAll (ClauseAllocator &to)

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

Protected Attributes
int	elimorder

bool	use_simplification

vec< uint32_t >	elimclauses

vec< char >	touched

OccLists< Var, vec< CRef >, ClauseDeleted >	occurs

vec< int >	n_occ

Heap< ElimLt >	elim_heap

Queue< CRef >	subsumption_queue

vec< char >	frozen

vec< char >	eliminated

int	bwdsub_assigns

int	n_touched

CRef	bwdsub_tmpunit

Protected Attributes inherited from Minisat::Solver
bool	ok

vec< CRef >	clauses

vec< CRef >	learnts

double	cla_inc

vec< double >	activity

double	var_inc

OccLists< Lit, vec< Watcher >, WatcherDeleted >	watches

vec< lbool >	assigns

vec< char >	polarity

vec< char >	decision

vec< Lit >	trail

vec< int >	trail_lim

vec< VarData >	vardata

int	qhead

int	simpDB_assigns

int64_t	simpDB_props

vec< Lit >	assumptions

Heap< VarOrderLt >	order_heap

double	progress_estimate

bool	remove_satisfied

ClauseAllocator	ca

vec< char >	seen

vec< Lit >	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

Additional Inherited Members
Static Protected Member Functions inherited from Minisat::Solver
static VarData	mkVarData (CRef cr, int l)

static double	drand (double &seed)

static int	irand (double &seed, int size)

Detailed Description

Definition at line 34 of file SimpSolver.h.

Constructor & Destructor Documentation

◆ SimpSolver()

SimpSolver::SimpSolver ( )

Definition at line 48 of file SimpSolver.cpp.

                       :
    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)
  , 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;
}

◆ ~SimpSolver()

SimpSolver::~SimpSolver ( )

Definition at line 73 of file SimpSolver.cpp.

74{

75}

Member Function Documentation

◆ addClause() [1/4]

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

inline

Definition at line 178 of file SimpSolver.h.

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

Minisat::SimpSolver::addClause_

bool addClause_(vec< Lit > &ps)

Definition SimpSolver.cpp:137

Minisat::Solver::add_tmp

vec< Lit > add_tmp

Definition Solver.h:202

Here is the call graph for this function:

◆ addClause() [2/4]

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

inline

Definition at line 180 of file SimpSolver.h.

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

p

Cube * p

Definition exorList.c:222

Here is the call graph for this function:

◆ addClause() [3/4]

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

inline

Definition at line 181 of file SimpSolver.h.

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

Here is the call graph for this function:

◆ addClause() [4/4]

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

inline

Definition at line 182 of file SimpSolver.h.

182{ 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:

◆ addClause_()

bool SimpSolver::addClause_ ( vec< Lit > & ps )

Definition at line 137 of file SimpSolver.cpp.

{
#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[toInt(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:

◆ addEmptyClause()

bool Minisat::SimpSolver::addEmptyClause ( )

inline

Definition at line 179 of file SimpSolver.h.

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

Here is the call graph for this function:

◆ asymm()

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

protected

Definition at line 400 of file SimpSolver.cpp.

{
    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:

◆ asymmVar()

bool SimpSolver::asymmVar ( Var v )

protected

Definition at line 427 of file SimpSolver.cpp.

{
    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:

◆ backwardSubsumptionCheck()

bool SimpSolver::backwardSubsumptionCheck ( bool verbose = false )

protected

Definition at line 333 of file SimpSolver.cpp.

{
    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:

◆ cleanUpClauses()

void SimpSolver::cleanUpClauses ( )

protected

Definition at line 673 of file SimpSolver.cpp.

{
    occurs.cleanAll();
    int i,j;
    for (i = j = 0; i < clauses.size(); i++)
        if (ca[clauses[i]].mark() == 0)
            clauses[j++] = clauses[i];
    clauses.shrink(i - j);
}

Here is the caller graph for this function:

◆ eliminate()

bool SimpSolver::eliminate ( bool turn_off_elim = false )

Definition at line 588 of file SimpSolver.cpp.

{
    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;
 
        // Force full cleanup (this is safe and desirable since it only happens once):
        rebuildOrderHeap();
        garbageCollect();
    }else{
        // Cheaper cleanup:
        cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
        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:

◆ eliminateVar()

bool SimpSolver::eliminateVar ( Var v )

protected

Definition at line 477 of file SimpSolver.cpp.

{
    assert(!frozen[v]);
    assert(!isEliminated(v));
    assert(value(v) == l_Undef);
    int i;
 
    // Split the occurrences into positive and negative:
    //
    const vec<CRef>& cls = occurs.lookup(v);
    vec<CRef>        pos, neg;
    for (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 (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 (i = 0; i < cls.size(); i++)
        removeClause(cls[i]); 
 
    // Produce clauses in cross product:
    vec<Lit>& resolvent = add_tmp;
    for (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:

◆ extendModel()

void SimpSolver::extendModel ( )

protected

Definition at line 571 of file SimpSolver.cpp.

{
    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:

◆ garbageCollect()

void SimpSolver::garbageCollect ( )

virtual

Reimplemented from Minisat::Solver.

Definition at line 712 of file SimpSolver.cpp.

{
    // 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()); 
 
    cleanUpClauses();
    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:

◆ gatherTouchedClauses()

void SimpSolver::gatherTouchedClauses ( )

protected

Definition at line 284 of file SimpSolver.cpp.

{
    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 < touched.size(); 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:

◆ implied()

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

protected

Definition at line 312 of file SimpSolver.cpp.

{
    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 false;
        }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:

◆ isEliminated()

bool Minisat::SimpSolver::isEliminated ( Var v ) const

inline

Definition at line 170 of file SimpSolver.h.

170{ return eliminated[v]; }

Here is the caller graph for this function:

◆ merge() [1/2]

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

protected

Definition at line 253 of file SimpSolver.cpp.

{
    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:

◆ merge() [2/2]

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

protected

Definition at line 219 of file SimpSolver.cpp.

{
    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;
    int i, j;
 
    for (i = 0; i < qs.size(); i++){
        if (var(qs[i]) != v){
            for (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 (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:

◆ newVar()

Var SimpSolver::newVar	(	bool	polarity = true,
		bool	dvar = true )

Definition at line 78 of file SimpSolver.cpp.

                                           {
    Var v = Solver::newVar(sign, dvar);
 
    frozen    .push((char)false);
    eliminated.push((char)false);
 
    if (use_simplification){
        n_occ     .push(0);
        n_occ     .push(0);
        occurs    .init(v);
        touched   .push(0);
        elim_heap .insert(v);
    }
    return v; }

Here is the call graph for this function:

◆ relocAll()

void SimpSolver::relocAll ( ClauseAllocator & to )

protected

Definition at line 688 of file SimpSolver.cpp.

{
    if (!use_simplification) return;
 
    // All occurs lists:
    //
    int i;
    for (i = 0; i < nVars(); i++){
        vec<CRef>& cs = occurs[i];
        for (int j = 0; j < cs.size(); j++)
            ca.reloc(cs[j], to);
    }
 
    // Subsumption queue:
    //
    for (i = 0; i < subsumption_queue.size(); i++)
        ca.reloc(subsumption_queue[i], to);
 
    // Temporary clause:
    //
    ca.reloc(bwdsub_tmpunit, to);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeClause()

void SimpSolver::removeClause ( CRef cr )

protected

Definition at line 177 of file SimpSolver.cpp.

{
    const Clause& c = ca[cr];
 
    if (use_simplification)
        for (int i = 0; i < c.size(); i++){
            n_occ[toInt(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:

◆ setFrozen()

void Minisat::SimpSolver::setFrozen	(	Var	v,
		bool	b )

inline

Definition at line 183 of file SimpSolver.h.

183{ 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:

◆ solve() [1/5]

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

inline

Definition at line 185 of file SimpSolver.h.

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

Minisat::Solver::budgetOff

void budgetOff()

Definition Solver.h:344

Minisat::Solver::solve_

lbool solve_()

Definition Solver.cpp:753

Minisat::Solver::assumptions

vec< Lit > assumptions

Definition Solver.h:189

Here is the call graph for this function:

◆ solve() [2/5]

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

inline

Definition at line 189 of file SimpSolver.h.

189 {

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

Here is the call graph for this function:

◆ solve() [3/5]

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

inline

Definition at line 186 of file SimpSolver.h.

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

Here is the call graph for this function:

◆ solve() [4/5]

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

inline

Definition at line 187 of file SimpSolver.h.

187{ 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:

◆ solve() [5/5]

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

inline

Definition at line 188 of file SimpSolver.h.

188{ 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:

◆ solve_()

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

protected

Definition at line 95 of file SimpSolver.cpp.

{
    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)
        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:

◆ solveLimited()

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

inline

Definition at line 192 of file SimpSolver.h.

192 {

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

Here is the call graph for this function:

◆ strengthenClause()

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

protected

Definition at line 192 of file SimpSolver.cpp.

{
    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[toInt(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:

◆ substitute()

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

Definition at line 539 of file SimpSolver.cpp.

{
    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:

◆ updateElimHeap()

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

inlineprotected

Definition at line 171 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:

Member Data Documentation

◆ asymm_lits

int Minisat::SimpSolver::asymm_lits

Definition at line 97 of file SimpSolver.h.

◆ bwdsub_assigns

int Minisat::SimpSolver::bwdsub_assigns

protected

Definition at line 138 of file SimpSolver.h.

◆ bwdsub_tmpunit

CRef Minisat::SimpSolver::bwdsub_tmpunit

protected

Definition at line 143 of file SimpSolver.h.

◆ clause_lim

int Minisat::SimpSolver::clause_lim

Definition at line 85 of file SimpSolver.h.

◆ elim_heap

Heap<ElimLt> Minisat::SimpSolver::elim_heap

protected

Definition at line 134 of file SimpSolver.h.

◆ elimclauses

vec<uint32_t> Minisat::SimpSolver::elimclauses

protected

Definition at line 129 of file SimpSolver.h.

◆ eliminated

vec<char> Minisat::SimpSolver::eliminated

protected

Definition at line 137 of file SimpSolver.h.

◆ eliminated_vars

int Minisat::SimpSolver::eliminated_vars

Definition at line 98 of file SimpSolver.h.

◆ elimorder

int Minisat::SimpSolver::elimorder

protected

Definition at line 127 of file SimpSolver.h.

◆ frozen

vec<char> Minisat::SimpSolver::frozen

protected

Definition at line 136 of file SimpSolver.h.

◆ grow

int Minisat::SimpSolver::grow

Definition at line 84 of file SimpSolver.h.

◆ merges

int Minisat::SimpSolver::merges

Definition at line 96 of file SimpSolver.h.

◆ n_occ

vec<int> Minisat::SimpSolver::n_occ

protected

Definition at line 133 of file SimpSolver.h.

◆ n_touched

int Minisat::SimpSolver::n_touched

protected

Definition at line 139 of file SimpSolver.h.

◆ occurs

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

protected

Definition at line 132 of file SimpSolver.h.

◆ simp_garbage_frac

double Minisat::SimpSolver::simp_garbage_frac

Definition at line 88 of file SimpSolver.h.

◆ subsumption_lim

int Minisat::SimpSolver::subsumption_lim

Definition at line 87 of file SimpSolver.h.

◆ subsumption_queue

Queue<CRef> Minisat::SimpSolver::subsumption_queue

protected

Definition at line 135 of file SimpSolver.h.

◆ touched

vec<char> Minisat::SimpSolver::touched

protected

Definition at line 130 of file SimpSolver.h.

◆ use_asymm

bool Minisat::SimpSolver::use_asymm

Definition at line 90 of file SimpSolver.h.

◆ use_elim

bool Minisat::SimpSolver::use_elim

Definition at line 92 of file SimpSolver.h.

◆ use_rcheck

bool Minisat::SimpSolver::use_rcheck

Definition at line 91 of file SimpSolver.h.

◆ use_simplification

bool Minisat::SimpSolver::use_simplification

protected

Definition at line 128 of file SimpSolver.h.

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

src/sat/bsat2/SimpSolver.h
src/sat/bsat2/SimpSolver.cpp

Classes

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ SimpSolver()

◆ ~SimpSolver()

Member Function Documentation

◆ addClause() [1/4]

◆ addClause() [2/4]

◆ addClause() [3/4]

◆ addClause() [4/4]

◆ addClause_()

◆ addEmptyClause()

◆ asymm()

◆ asymmVar()

◆ backwardSubsumptionCheck()

◆ cleanUpClauses()

◆ eliminate()

◆ eliminateVar()

◆ extendModel()

◆ garbageCollect()

◆ gatherTouchedClauses()

◆ implied()

◆ isEliminated()

◆ merge() [1/2]

◆ merge() [2/2]

◆ newVar()

◆ relocAll()

◆ removeClause()

◆ setFrozen()

◆ solve() [1/5]

◆ solve() [2/5]

◆ solve() [3/5]

◆ solve() [4/5]

◆ solve() [5/5]

◆ solve_()

◆ solveLimited()

◆ strengthenClause()

◆ substitute()

◆ updateElimHeap()

Member Data Documentation

◆ asymm_lits

◆ bwdsub_assigns

◆ bwdsub_tmpunit

◆ clause_lim

◆ elim_heap

◆ elimclauses

◆ eliminated

◆ eliminated_vars

◆ elimorder

◆ frozen

◆ grow

◆ merges

◆ n_occ

◆ n_touched

◆ occurs

◆ simp_garbage_frac

◆ subsumption_lim

◆ subsumption_queue

◆ touched

◆ use_asymm

◆ use_elim

◆ use_rcheck

◆ use_simplification