#include <SimpSolver.h>

Inheritance diagram for Gluco2::SimpSolver:

Collaboration diagram for Gluco2::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)

int	solveLimited (int *lit0, int nlits, bool do_simp=false, 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)

void	prelocate (int base_var_num)

virtual void	reset ()

virtual void	garbageCollect ()

Public Member Functions inherited from Gluco2::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)

void	sat_solver_set_jftr (int)

int	sat_solver_jftr ()

void	sat_solver_reset ()

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, bool use_oheap=true)

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

int	level (Var x) 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 ()

void	markTill (Var v0, int nlim)

void	markApprox (Var v0, Var v1, int nlim)

void	prelocate (int var_num)

void	setVarFaninLits (Var v, Lit lit1, Lit lit2)

void	setVarFaninLits (int v, int lit1, int lit2)

void	setNewRound ()

void	markCone (Var v)

void	setJust (int njftr)

bool	isRoundWatch (Var v) const

void	justReset ()

double	varActivity (int v) const

int	varPolarity (int v)

int	justUsage () const

int	solveLimited (int *, int nlits)

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

vec< Lit >	JustModel

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

double	progressEstimate () const

bool	withinBudget () const

bool	isSelector (Var v)

void	uncheckedEnqueue2 (Lit p, CRef from=CRef_Undef)

void	addJwatch (Var host, Var member, int index)

void	inplace_sort (Var v)

bool	isTwoFanin (Var v) const

bool	isAND (Var v) const

bool	isJReason (Var v) const

Lit	getFaninLit0 (Var v) const

Lit	getFaninLit1 (Var v) const

bool	getFaninC0 (Var v) const

bool	getFaninC1 (Var v) const

Var	getFaninVar0 (Var v) const

Var	getFaninVar1 (Var v) const

Lit	getFaninPlt0 (Var v) const

Lit	getFaninPlt1 (Var v) const

Lit	maxActiveLit (Lit lit0, Lit lit1) const

Lit	gateJustFanin (Var v) const

void	gateAddJwatch (Var v, int index)

CRef	gatePropagateCheck (Var v, Var t)

CRef	gatePropagateCheckThis (Var v)

CRef	gatePropagateCheckFanout (Var v, Lit lfo)

void	setItpcSize (int sz)

void	updateJustActivity (Var v)

void	ResetJustData (bool fCleanMemory)

Lit	pickJustLit (int &index)

void	justCheck ()

void	pushJustQueue (Var v, int index)

void	restoreJustQueue (int level)

void	gateClearJwatch (Var v, int backtrack_level)

CRef	gatePropagate (Lit p)

CRef	interpret (Var v, Var t)

CRef	castCRef (Lit p)

CRef	getConfClause (CRef r)

CRef	Var2CRef (Var v) const

Var	CRef2Var (CRef cr) const

bool	isGateCRef (CRef cr) const

void	loadJust_rec (Var v)

void	loadJust ()

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

bool	heap_rescale

vec< NodeData >	var2NodeData

vec< unsigned >	var2TravId

vec< Lit >	var2Fanout0

vec< Lit >	var2FanoutN

CRef	itpc

unsigned	travId_prev

unsigned	travId

int	jhead

Heap2< JustOrderLt2, JustKey >	jheap

vec< int >	jlevel

vec< int >	jnext

int	nSkipMark

vec< Var >	vMarked

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

static double	drand (double &seed)

static int	irand (double &seed, int size)

static NodeData	mkNodeData ()

Detailed Description

Definition at line 36 of file SimpSolver.h.

Constructor & Destructor Documentation

◆ SimpSolver()

SimpSolver::SimpSolver ( )

Definition at line 48 of file SimpSolver2.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;
    parsing               = 0;
}

◆ ~SimpSolver()

SimpSolver::~SimpSolver ( )

Definition at line 75 of file SimpSolver2.cpp.

76{

77}

Member Function Documentation

◆ addClause() [1/4]

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

inline

Definition at line 198 of file SimpSolver.h.

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

Gluco2::SimpSolver::addClause_

bool addClause_(vec< Lit > &ps)

Definition SimpSolver2.cpp:139

Gluco2::Solver::add_tmp

vec< Lit > add_tmp

Definition Solver.h:282

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addClause() [2/4]

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

inline

Definition at line 200 of file SimpSolver.h.

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

inline

Definition at line 201 of file SimpSolver.h.

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

inline

Definition at line 202 of file SimpSolver.h.

202{ 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 139 of file SimpSolver2.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 Gluco2::SimpSolver::addEmptyClause ( )

inline

Definition at line 199 of file SimpSolver.h.

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

Here is the call graph for this function:

◆ addVar()

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

inline

Definition at line 223 of file SimpSolver.h.

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

Gluco2::SimpSolver::newVar

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

Definition SimpSolver2.cpp:80

Gluco2::Solver::nVars

int nVars() const

Definition Solver.h:569

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 418 of file SimpSolver2.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 445 of file SimpSolver2.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 351 of file SimpSolver2.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 703 of file SimpSolver2.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 611 of file SimpSolver2.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 495 of file SimpSolver2.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 594 of file SimpSolver2.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 Gluco2::Solver.

Definition at line 742 of file SimpSolver2.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 302 of file SimpSolver2.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 330 of file SimpSolver2.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 Gluco2::SimpSolver::isEliminated ( Var v ) const

inline

Definition at line 190 of file SimpSolver.h.

190{ 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 272 of file SimpSolver2.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 239 of file SimpSolver2.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 80 of file SimpSolver2.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:

◆ prelocate()

void Gluco2::SimpSolver::prelocate ( int base_var_num )

inline

Definition at line 71 of file SimpSolver.h.

                                       {
        Solver::prelocate(base_var_num);
        frozen    .prelocate( base_var_num );
        eliminated.prelocate( base_var_num );
 
        if (use_simplification){
            n_occ     .prelocate( base_var_num << 1 );
            occurs    .prelocate( base_var_num );
            touched   .prelocate( base_var_num );
            elim_heap .prelocate( base_var_num );
        }
    }

Here is the call graph for this function:

◆ relocAll()

void SimpSolver::relocAll ( ClauseAllocator & to )

protected

Definition at line 718 of file SimpSolver2.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 184 of file SimpSolver2.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 Gluco2::Solver.

Definition at line 758 of file SimpSolver2.cpp.

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

Here is the call graph for this function:

◆ setFrozen()

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

inline

Definition at line 203 of file SimpSolver.h.

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

inline

Definition at line 205 of file SimpSolver.h.

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

Gluco2::Solver::budgetOff

void budgetOff()

Definition Solver.h:585

Gluco2::Solver::solve_

lbool solve_()

Definition Glucose2.cpp:1391

Gluco2::Solver::assumptions

vec< Lit > assumptions

Definition Solver.h:256

Here is the call graph for this function:

◆ solve() [2/5]

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

inline

Definition at line 209 of file SimpSolver.h.

209 {

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

inline

Definition at line 206 of file SimpSolver.h.

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

inline

Definition at line 207 of file SimpSolver.h.

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

inline

Definition at line 208 of file SimpSolver.h.

208{ 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 97 of file SimpSolver2.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() [1/2]

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

inline

Definition at line 212 of file SimpSolver.h.

212 {

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

Here is the call graph for this function:

◆ solveLimited() [2/2]

int Gluco2::SimpSolver::solveLimited	(	int *	lit0,
		int	nlits,
		bool	do_simp = false,
		bool	turn_off_simp = false )

inline

Definition at line 215 of file SimpSolver.h.

                                                                                          {
    assumptions.clear();
    for(int i = 0; i < nlits; i ++)
        assumptions.push(toLit(lit0[i]));
    lbool res = solve_(do_simp, turn_off_simp);
    return res == l_True ? 1 : (res == l_False ? -1 : 0);
}

Here is the call graph for this function:

◆ strengthenClause()

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

protected

Definition at line 199 of file SimpSolver2.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 560 of file SimpSolver2.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 Gluco2::SimpSolver::updateElimHeap ( Var v )

inlineprotected

Definition at line 191 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 Gluco2::SimpSolver::asymm_lits

Definition at line 115 of file SimpSolver.h.

◆ bwdsub_assigns

int Gluco2::SimpSolver::bwdsub_assigns

protected

Definition at line 157 of file SimpSolver.h.

◆ bwdsub_tmpunit

CRef Gluco2::SimpSolver::bwdsub_tmpunit

protected

Definition at line 162 of file SimpSolver.h.

◆ clause_lim

int Gluco2::SimpSolver::clause_lim

Definition at line 103 of file SimpSolver.h.

◆ elim_heap

Heap<ElimLt> Gluco2::SimpSolver::elim_heap

protected

Definition at line 153 of file SimpSolver.h.

◆ elimclauses

vec<uint32_t> Gluco2::SimpSolver::elimclauses

protected

Definition at line 148 of file SimpSolver.h.

◆ eliminated

vec<char> Gluco2::SimpSolver::eliminated

protected

Definition at line 156 of file SimpSolver.h.

◆ eliminated_clauses

int Gluco2::SimpSolver::eliminated_clauses

Definition at line 117 of file SimpSolver.h.

◆ eliminated_vars

int Gluco2::SimpSolver::eliminated_vars

Definition at line 116 of file SimpSolver.h.

◆ elimorder

int Gluco2::SimpSolver::elimorder

protected

Definition at line 146 of file SimpSolver.h.

◆ frozen

vec<char> Gluco2::SimpSolver::frozen

protected

Definition at line 155 of file SimpSolver.h.

◆ grow

int Gluco2::SimpSolver::grow

Definition at line 102 of file SimpSolver.h.

◆ merges

int Gluco2::SimpSolver::merges

Definition at line 114 of file SimpSolver.h.

◆ n_occ

vec<int> Gluco2::SimpSolver::n_occ

protected

Definition at line 152 of file SimpSolver.h.

◆ n_touched

int Gluco2::SimpSolver::n_touched

protected

Definition at line 158 of file SimpSolver.h.

◆ occurs

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

protected

Definition at line 151 of file SimpSolver.h.

◆ parsing

int Gluco2::SimpSolver::parsing

Definition at line 101 of file SimpSolver.h.

◆ simp_garbage_frac

double Gluco2::SimpSolver::simp_garbage_frac

Definition at line 106 of file SimpSolver.h.

◆ subsumption_lim

int Gluco2::SimpSolver::subsumption_lim

Definition at line 105 of file SimpSolver.h.

◆ subsumption_queue

Queue<CRef> Gluco2::SimpSolver::subsumption_queue

protected

Definition at line 154 of file SimpSolver.h.

◆ touched

vec<char> Gluco2::SimpSolver::touched

protected

Definition at line 149 of file SimpSolver.h.

◆ use_asymm

bool Gluco2::SimpSolver::use_asymm

Definition at line 108 of file SimpSolver.h.

◆ use_elim

bool Gluco2::SimpSolver::use_elim

Definition at line 110 of file SimpSolver.h.

◆ use_rcheck

bool Gluco2::SimpSolver::use_rcheck

Definition at line 109 of file SimpSolver.h.

◆ use_simplification

bool Gluco2::SimpSolver::use_simplification

protected

Definition at line 147 of file SimpSolver.h.

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

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

◆ prelocate()

◆ relocAll()

◆ removeClause()

◆ reset()

◆ setFrozen()

◆ solve() [1/5]

◆ solve() [2/5]

◆ solve() [3/5]

◆ solve() [4/5]

◆ solve() [5/5]

◆ solve_()

◆ solveLimited() [1/2]

◆ solveLimited() [2/2]

◆ 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