#include <SimpSolver.h>

Inheritance diagram for Gluco::SimpSolver:

Collaboration diagram for Gluco::SimpSolver:

[legend]

Classes
struct	ClauseDeleted

struct	ElimLt

Public Member Functions
	SimpSolver ()

	~SimpSolver ()

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

void	addVar (Var v)

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

virtual void	garbageCollect ()

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

virtual	~Solver ()

void	sat_solver_set_var_fanin_lit (int, int, int)

void	sat_solver_start_new_round ()

void	sat_solver_mark_cone (int)

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

void	addVar (Var v)

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	printLit (Lit l)

void	printClause (CRef c)

void	printInitialClause (CRef c)

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

int *	getCex () const

void	setIncrementalMode ()

void	initNbInitialVars (int nb)

void	printIncrementalStats ()

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	parsing

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

int	eliminated_clauses

Public Attributes inherited from Gluco::Solver
int	SolverType

void *	pCnfMan

int(*	pCnfFunc )(void p, int, int )

int	nCallConfl

bool	terminate_search_early

int *	pstop

uint64_t	nRuntimeLimit

vec< int >	user_vec

vec< Lit >	user_lits

int	jftr

vec< lbool >	model

vec< Lit >	conflict

int	verbosity

int	verbEveryConflicts

int	showModel

double	K

double	R

double	sizeLBDQueue

double	sizeTrailQueue

int	firstReduceDB

int	incReduceDB

int	specialIncReduceDB

unsigned int	lbLBDFrozenClause

int	lbSizeMinimizingClause

unsigned int	lbLBDMinimizingClause

double	var_decay

double	clause_decay

double	random_var_freq

double	random_seed

int	ccmin_mode

int	phase_saving

bool	rnd_pol

bool	rnd_init_act

double	garbage_frac

FILE *	certifiedOutput

bool	certifiedUNSAT

int64_t	nbRemovedClauses

int64_t	nbReducedClauses

int64_t	nbDL2

int64_t	nbBin

int64_t	nbUn

int64_t	nbReduceDB

int64_t	solves

int64_t	starts

int64_t	decisions

int64_t	rnd_decisions

int64_t	propagations

int64_t	conflicts

int64_t	conflictsRestarts

int64_t	nbstopsrestarts

int64_t	nbstopsrestartssame

int64_t	lastblockatrestart

int64_t	dec_vars

int64_t	clauses_literals

int64_t	learnts_literals

int64_t	max_literals

int64_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 Gluco::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, vec< Lit > &selectors, int &out_btlevel, unsigned int &nblevels, unsigned int &szWithoutSelectors)

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

unsigned int	computeLBD (const vec< Lit > &lits, int end=-1)

unsigned int	computeLBD (const Clause &c)

void	minimisationWithBinaryResolution (vec< Lit > &out_learnt)

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

bool	isSelector (Var v)

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 Gluco::Solver
long	curRestart

int	lastIndexRed

bool	ok

double	cla_inc

vec< double >	activity

double	var_inc

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

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

vec< CRef >	clauses

vec< CRef >	learnts

vec< lbool >	assigns

vec< char >	polarity

vec< char >	decision

vec< Lit >	trail

vec< int >	nbpos

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

vec< unsigned int >	permDiff

ClauseAllocator	ca

int	nbclausesbeforereduce

bqueue< unsigned int >	trailQueue

bqueue< unsigned int >	lbdQueue

float	sumLBD

int	sumAssumptions

vec< char >	seen

vec< Lit >	analyze_stack

vec< Lit >	analyze_toclear

vec< Lit >	add_tmp

unsigned int	MYFLAG

double	max_learnts

double	learntsize_adjust_confl

int	learntsize_adjust_cnt

int64_t	conflict_budget

int64_t	propagation_budget

bool	asynch_interrupt

int	incremental

int	nbVarsInitialFormula

double	totalTime4Sat

double	totalTime4Unsat

int	nbSatCalls

int	nbUnsatCalls

vec< int >	assumptionPositions

vec< int >	initialPositions

Additional Inherited Members
Static Protected Member Functions inherited from Gluco::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)
  , eliminated_clauses (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 74 of file SimpSolver.cpp.

75{

76}

Member Function Documentation

◆ addClause() [1/4]

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

inline

Definition at line 183 of file SimpSolver.h.

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

Gluco::SimpSolver::addClause_

bool addClause_(vec< Lit > &ps)

Definition SimpSolver.cpp:138

Gluco::Solver::add_tmp

vec< Lit > add_tmp

Definition Solver.h:276

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addClause() [2/4]

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

inline

Definition at line 185 of file SimpSolver.h.

185{ 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 Gluco::SimpSolver::addClause	(	Lit	p,
		Lit	q )

inline

Definition at line 186 of file SimpSolver.h.

186{ 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 Gluco::SimpSolver::addClause	(	Lit	p,
		Lit	q,
		Lit	r )

inline

Definition at line 187 of file SimpSolver.h.

187{ 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 138 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(!parsing && certifiedUNSAT) {
      for (int i = 0; i < ps.size(); i++)
        fprintf(certifiedOutput, "%i " , (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1) );
      fprintf(certifiedOutput, "0\n");
    }
 
    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 Gluco::SimpSolver::addEmptyClause ( )

inline

Definition at line 184 of file SimpSolver.h.

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

Here is the call graph for this function:

◆ addVar()

void Gluco::SimpSolver::addVar ( Var v )

inline

Definition at line 200 of file SimpSolver.h.

200{ while (v >= nVars()) newVar(); }

Gluco::SimpSolver::newVar

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

Definition SimpSolver.cpp:79

Gluco::Solver::nVars

int nVars() const

Definition Solver.h:426

Here is the call graph for this function:

Here is the caller graph for this function:

◆ asymm()

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

protected

Definition at line 417 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 444 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 350 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 702 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 610 of file SimpSolver.cpp.

{
    //abctime clk = Abc_Clock();
    if (!simplify())
        return false;
    else if (!use_simplification)
        return true;
 
    // Main simplification loop:
    //
 
    int toPerform = clauses.size()<=4800000;
    
    if(!toPerform) {
      printf("c Too many clauses... No preprocessing\n");
    }
 
    while (toPerform && (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] != 0;
                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("c |  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 494 of file SimpSolver.cpp.

{
    int i, j;
    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 (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 (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 (i = 0; i < neg.size(); i++)
            mkElimClause(elimclauses, v, ca[neg[i]]);
        mkElimClause(elimclauses, mkLit(v));
        eliminated_clauses += neg.size();
    }else{
        for (i = 0; i < pos.size(); i++)
            mkElimClause(elimclauses, v, ca[pos[i]]);
        mkElimClause(elimclauses, ~mkLit(v));
        eliminated_clauses += pos.size();
    }
 
 
    // Produce clauses in cross product:
    vec<Lit>& resolvent = add_tmp;
    for (i = 0; i < pos.size(); i++)
        for (j = 0; j < neg.size(); j++)
            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
                return false;
 
    for (i = 0; i < cls.size(); i++)
        removeClause(cls[i]);
 
    // 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 593 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 Gluco::Solver.

Definition at line 741 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 301 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 329 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 Gluco::SimpSolver::isEliminated ( Var v ) const

inline

Definition at line 175 of file SimpSolver.h.

175{ return eliminated.size() > 0 ? eliminated[v] != 0 : 0; }

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 271 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 238 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 79 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:

Here is the caller graph for this function:

◆ relocAll()

void SimpSolver::relocAll ( ClauseAllocator & to )

protected

Definition at line 717 of file SimpSolver.cpp.

{
    int i;
    if (!use_simplification) return;
 
    // All occurs lists:
    //
    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 183 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:

◆ reset()

void SimpSolver::reset ( )

virtual

Reimplemented from Gluco::Solver.

Definition at line 757 of file SimpSolver.cpp.

{
    Solver::reset();
    grow = opt_grow;
    asymm_lits = eliminated_vars = bwdsub_assigns = n_touched = 0;
    elimclauses.clear(false);
    touched.clear(false);
    occurs.clear(false);
    n_occ.clear(false);
    elim_heap.clear(false);
    subsumption_queue.clear(false);
    frozen.clear(false);
    eliminated.clear(false);
    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:

◆ setFrozen()

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

inline

Definition at line 188 of file SimpSolver.h.

188{ 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 Gluco::SimpSolver::solve	(	bool	do_simp = true,
		bool	turn_off_simp = false )

inline

Definition at line 190 of file SimpSolver.h.

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

Gluco::Solver::assumptions

vec< Lit > assumptions

Definition Solver.h:250

Gluco::Solver::solve_

lbool solve_()

Definition Glucose.cpp:1209

Gluco::Solver::budgetOff

void budgetOff()

Definition Solver.h:442

Here is the call graph for this function:

◆ solve() [2/5]

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

inline

Definition at line 194 of file SimpSolver.h.

194 {

195 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 Gluco::SimpSolver::solve	(	Lit	p,
		bool	do_simp = true,
		bool	turn_off_simp = false )

inline

Definition at line 191 of file SimpSolver.h.

191{ 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 Gluco::SimpSolver::solve	(	Lit	p,
		Lit	q,
		bool	do_simp = true,
		bool	turn_off_simp = false )

inline

Definition at line 192 of file SimpSolver.h.

192{ 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 Gluco::SimpSolver::solve	(	Lit	p,
		Lit	q,
		Lit	r,
		bool	do_simp = true,
		bool	turn_off_simp = false )

inline

Definition at line 193 of file SimpSolver.h.

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

inline

Definition at line 197 of file SimpSolver.h.

197 {

198 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 198 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 (certifiedUNSAT) {
      for (int i = 0; i < c.size(); i++)
        if (c[i] != l) fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
      fprintf(certifiedOutput, "0\n");
    }
 
    if (c.size() == 2){
        removeClause(cr);
        c.strengthen(l);
    }else{
        if (certifiedUNSAT) {
          fprintf(certifiedOutput, "d ");
          for (int i = 0; i < c.size(); i++)
            fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) );
          fprintf(certifiedOutput, "0\n");
        }
 
        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 559 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);
        }
 
 
        if (!addClause_(subst_clause))
            return ok = false;
 
       removeClause(cls[i]);
 
   }
 
    return true;
}

Here is the call graph for this function:

◆ updateElimHeap()

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

inlineprotected

Definition at line 176 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 Gluco::SimpSolver::asymm_lits

Definition at line 100 of file SimpSolver.h.

◆ bwdsub_assigns

int Gluco::SimpSolver::bwdsub_assigns

protected

Definition at line 142 of file SimpSolver.h.

◆ bwdsub_tmpunit

CRef Gluco::SimpSolver::bwdsub_tmpunit

protected

Definition at line 147 of file SimpSolver.h.

◆ clause_lim

int Gluco::SimpSolver::clause_lim

Definition at line 88 of file SimpSolver.h.

◆ elim_heap

Heap<ElimLt> Gluco::SimpSolver::elim_heap

protected

Definition at line 138 of file SimpSolver.h.

◆ elimclauses

vec<uint32_t> Gluco::SimpSolver::elimclauses

protected

Definition at line 133 of file SimpSolver.h.

◆ eliminated

vec<char> Gluco::SimpSolver::eliminated

protected

Definition at line 141 of file SimpSolver.h.

◆ eliminated_clauses

int Gluco::SimpSolver::eliminated_clauses

Definition at line 102 of file SimpSolver.h.

◆ eliminated_vars

int Gluco::SimpSolver::eliminated_vars

Definition at line 101 of file SimpSolver.h.

◆ elimorder

int Gluco::SimpSolver::elimorder

protected

Definition at line 131 of file SimpSolver.h.

◆ frozen

vec<char> Gluco::SimpSolver::frozen

protected

Definition at line 140 of file SimpSolver.h.

◆ grow

int Gluco::SimpSolver::grow

Definition at line 87 of file SimpSolver.h.

◆ merges

int Gluco::SimpSolver::merges

Definition at line 99 of file SimpSolver.h.

◆ n_occ

vec<int> Gluco::SimpSolver::n_occ

protected

Definition at line 137 of file SimpSolver.h.

◆ n_touched

int Gluco::SimpSolver::n_touched

protected

Definition at line 143 of file SimpSolver.h.

◆ occurs

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

protected

Definition at line 136 of file SimpSolver.h.

◆ parsing

int Gluco::SimpSolver::parsing

Definition at line 86 of file SimpSolver.h.

◆ simp_garbage_frac

double Gluco::SimpSolver::simp_garbage_frac

Definition at line 91 of file SimpSolver.h.

◆ subsumption_lim

int Gluco::SimpSolver::subsumption_lim

Definition at line 90 of file SimpSolver.h.

◆ subsumption_queue

Queue<CRef> Gluco::SimpSolver::subsumption_queue

protected

Definition at line 139 of file SimpSolver.h.

◆ touched

vec<char> Gluco::SimpSolver::touched

protected

Definition at line 134 of file SimpSolver.h.

◆ use_asymm

bool Gluco::SimpSolver::use_asymm

Definition at line 93 of file SimpSolver.h.

◆ use_elim

bool Gluco::SimpSolver::use_elim

Definition at line 95 of file SimpSolver.h.

◆ use_rcheck

bool Gluco::SimpSolver::use_rcheck

Definition at line 94 of file SimpSolver.h.

◆ use_simplification

bool Gluco::SimpSolver::use_simplification

protected

Definition at line 132 of file SimpSolver.h.

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

src/sat/glucose/SimpSolver.h
src/sat/glucose/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()

◆ addVar()

◆ asymm()

◆ asymmVar()

◆ backwardSubsumptionCheck()

◆ cleanUpClauses()

◆ eliminate()

◆ eliminateVar()

◆ extendModel()

◆ garbageCollect()

◆ gatherTouchedClauses()

◆ implied()

◆ isEliminated()

◆ merge() [1/2]

◆ merge() [2/2]

◆ newVar()

◆ relocAll()

◆ removeClause()

◆ reset()

◆ 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_clauses

◆ eliminated_vars

◆ elimorder

◆ frozen

◆ grow

◆ merges

◆ n_occ

◆ n_touched

◆ occurs

◆ parsing

◆ simp_garbage_frac

◆ subsumption_lim

◆ subsumption_queue

◆ touched

◆ use_asymm

◆ use_elim

◆ use_rcheck

◆ use_simplification