#include <Solver.h>

Inheritance diagram for Gluco::Solver:

Collaboration diagram for Gluco::Solver:

[legend]

Classes
struct	VarData

struct	VarOrderLt

struct	Watcher

struct	WatcherDeleted

Public Member Functions
	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 ()

virtual void	reset ()

virtual void	garbageCollect ()

void	checkGarbage (double gf)

void	checkGarbage ()

Public Attributes
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
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)

Static Protected Member Functions
static VarData	mkVarData (CRef cr, int l)

static double	drand (double &seed)

static int	irand (double &seed, int size)

Protected Attributes
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

Detailed Description

Definition at line 47 of file Solver.h.

Constructor & Destructor Documentation

◆ Solver()

Solver::Solver ( )

Definition at line 90 of file Glucose.cpp.

               :
 
    // Parameters (user settable):
    //
    SolverType(0)
    , pCnfFunc(NULL)
    , nCallConfl(1000)
    , terminate_search_early(false)
    , pstop(NULL)
    , nRuntimeLimit(0)
 
    , verbosity      (0)
    , verbEveryConflicts(10000)
    , showModel      (0)
    , K              (opt_K)
    , R              (opt_R)
    , sizeLBDQueue   (opt_size_lbd_queue)
    , sizeTrailQueue   (opt_size_trail_queue)
    , firstReduceDB  (opt_first_reduce_db)
    , incReduceDB    (opt_inc_reduce_db)
    , specialIncReduceDB    (opt_spec_inc_reduce_db)
    , lbLBDFrozenClause (opt_lb_lbd_frozen_clause)
    , lbSizeMinimizingClause (opt_lb_size_minimzing_clause)
    , lbLBDMinimizingClause (opt_lb_lbd_minimzing_clause)
  , var_decay        (opt_var_decay)
  , clause_decay     (opt_clause_decay)
  , random_var_freq  (opt_random_var_freq)
  , random_seed      (opt_random_seed)
  , ccmin_mode       (opt_ccmin_mode)
  , phase_saving     (opt_phase_saving)
  , rnd_pol          (false)
  , rnd_init_act     (opt_rnd_init_act)
  , garbage_frac     (opt_garbage_frac)
  , certifiedOutput  (NULL)
  , certifiedUNSAT   (opt_certified_) 
    // Statistics: (formerly in 'SolverStats')
    //
  ,  nbRemovedClauses(0),nbReducedClauses(0), nbDL2(0),nbBin(0),nbUn(0) , nbReduceDB(0)
    , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0),conflicts(0),conflictsRestarts(0),nbstopsrestarts(0),nbstopsrestartssame(0),lastblockatrestart(0)
  , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
    , curRestart(1)
 
  , ok                 (true)
  , cla_inc            (1)
  , var_inc            (1)
  , watches            (WatcherDeleted(ca))
  , watchesBin            (WatcherDeleted(ca))
  , qhead              (0)
  , simpDB_assigns     (-1)
  , simpDB_props       (0)
  , order_heap         (VarOrderLt(activity))
  , progress_estimate  (0)
  , remove_satisfied   (true)
 
    // Resource constraints:
    //
  , conflict_budget    (-1)
  , propagation_budget (-1)
  , asynch_interrupt   (false)
  , incremental(opt_incremental)
  , nbVarsInitialFormula(INT32_MAX)
{
  MYFLAG=0;  
  // Initialize only first time. Useful for incremental solving, useless otherwise
  lbdQueue.initSize(sizeLBDQueue);
  trailQueue.initSize(sizeTrailQueue);
  sumLBD = 0;
  nbclausesbeforereduce = firstReduceDB;
  totalTime4Sat=0;totalTime4Unsat=0;
  nbSatCalls=0;nbUnsatCalls=0;
 
 
  if(certifiedUNSAT) {
    if(!strcmp(opt_certified_file_,"NULL")) {
      certifiedOutput =  fopen("/dev/stdout", "wb");
    } else {
      certifiedOutput =  fopen(opt_certified_file_, "wb");           
    }
    //    fprintf(certifiedOutput,"o proof DRUP\n");
  }
}

Here is the call graph for this function:

◆ ~Solver()

Solver::~Solver ( )

virtual

Definition at line 173 of file Glucose.cpp.

174{

175}

Member Function Documentation

◆ abstractLevel()

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

inlineprotected

Definition at line 418 of file Solver.h.

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

Gluco::Solver::level

int level(Var x) const

Definition Solver.h:369

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addClause() [1/4]

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

inline

Definition at line 402 of file Solver.h.

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

Gluco::Solver::addClause_

bool addClause_(vec< Lit > &ps)

Definition Glucose.cpp:224

Gluco::Solver::add_tmp

vec< Lit > add_tmp

Definition Solver.h:276

Here is the call graph for this function:

◆ addClause() [2/4]

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

inline

Definition at line 404 of file Solver.h.

404{ 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::Solver::addClause	(	Lit	p,
		Lit	q )

inline

Definition at line 405 of file Solver.h.

405{ 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::Solver::addClause	(	Lit	p,
		Lit	q,
		Lit	r )

inline

Definition at line 406 of file Solver.h.

406{ 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 Solver::addClause_ ( vec< Lit > & ps )

Definition at line 224 of file Glucose.cpp.

{
    assert(decisionLevel() == 0);
    if (!ok) return false;
 
    if ( 0 ) {
        for ( int i = 0; i < ps.size(); i++ )
            printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
        printf( "\n" );
    }
 
    // Check if clause is satisfied and remove false/duplicate literals:
    sort(ps);
 
    vec<Lit>    oc;
    oc.clear();
 
    Lit p; int i, j, flag = 0;
    if(certifiedUNSAT) {
      for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
        oc.push(ps[i]);
        if (value(ps[i]) == l_True || ps[i] == ~p || value(ps[i]) == l_False)
          flag = 1;
      }
    }
 
    for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
      if (value(ps[i]) == l_True || ps[i] == ~p)
        return true;
      else if (value(ps[i]) != l_False && ps[i] != p)
        ps[j++] = p = ps[i];
    ps.shrink(i - j);
 
    if ( 0 ) {
        for ( int i = 0; i < ps.size(); i++ )
            printf( "%s%d ", (toInt(ps[i]) & 1) ? "-":"", toInt(ps[i]) >> 1 );
        printf( "\n" );
    }
    
    if (flag && (certifiedUNSAT)) {
      for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
        fprintf(certifiedOutput, "%i ", (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1));
      fprintf(certifiedOutput, "0\n");
 
      fprintf(certifiedOutput, "d ");
      for (i = j = 0, p = lit_Undef; i < oc.size(); i++)
        fprintf(certifiedOutput, "%i ", (var(oc[i]) + 1) * (-2 * sign(oc[i]) + 1));
      fprintf(certifiedOutput, "0\n");
    }
 
    if (ps.size() == 0)
        return ok = false;
    else if (ps.size() == 1){
        uncheckedEnqueue(ps[0]);
        return ok = (propagate() == CRef_Undef);
    }else{
        CRef cr = ca.alloc(ps, false);
        clauses.push(cr);
        attachClause(cr);
    }
 
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addEmptyClause()

bool Gluco::Solver::addEmptyClause ( )

inline

Definition at line 403 of file Solver.h.

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

Here is the call graph for this function:

◆ addVar()

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

inline

Definition at line 464 of file Solver.h.

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

Gluco::Solver::nVars

int nVars() const

Definition Solver.h:426

Gluco::Solver::newVar

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

Definition Glucose.cpp:202

Here is the call graph for this function:

◆ analyze()

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

protected

Definition at line 529 of file Glucose.cpp.

{
    int pathC = 0;
    Lit p     = lit_Undef;
 
    // Generate conflict clause:
    //
    out_learnt.push();      // (leave room for the asserting literal)
    int index   = trail.size() - 1;
 
    do{
        assert(confl != CRef_Undef); // (otherwise should be UIP)
        Clause& c = ca[confl];
 
        // Special case for binary clauses
        // The first one has to be SAT
        if( p != lit_Undef && c.size()==2 && value(c[0])==l_False) {
          
          assert(value(c[1])==l_True);
          Lit tmp = c[0];
          c[0] =  c[1], c[1] = tmp;
        }
        
        if (c.learnt()) 
            claBumpActivity(c);
 
#ifdef DYNAMICNBLEVEL               
        // DYNAMIC NBLEVEL trick (see competition'09 companion paper)
        if(c.learnt()  && c.lbd()>2) { 
          unsigned int nblevels = computeLBD(c);
          if(nblevels+1<c.lbd() ) { // improve the LBD
            if(c.lbd()<=lbLBDFrozenClause) {
              c.setCanBeDel(false); 
            }
            // seems to be interesting : keep it for the next round
            c.setLBD(nblevels); // Update it
          }
        }
#endif
 
 
        for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
            Lit q = c[j];
 
            if (!seen[var(q)] && level(var(q)) > 0){
              if(!isSelector(var(q)))
                varBumpActivity(var(q));
              seen[var(q)] = 1;
              if (level(var(q)) >= decisionLevel()) {
                pathC++;
#ifdef UPDATEVARACTIVITY
                // UPDATEVARACTIVITY trick (see competition'09 companion paper)
                if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)  && ca[reason(var(q))].learnt()) 
                  lastDecisionLevel.push(q);
#endif
                
              } else {
                if(isSelector(var(q))) {
                  assert(value(q) == l_False);
                  selectors.push(q);
                } else 
                  out_learnt.push(q);
              }
            }
        }
        
        // Select next clause to look at:
        while (!seen[var(trail[index--])]);
        p     = trail[index+1];
        confl = reason(var(p));
        seen[var(p)] = 0;
        pathC--;
 
    }while (pathC > 0);
    out_learnt[0] = ~p;
 
    // Simplify conflict clause:
    //
    int i, j;
 
    for(i = 0;i<selectors.size();i++)  
      out_learnt.push(selectors[i]);       
 
    out_learnt.copyTo_(analyze_toclear);
    if (ccmin_mode == 2){
        uint32_t abstract_level = 0;
        for (i = 1; i < out_learnt.size(); i++)
            abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
 
        for (i = j = 1; i < out_learnt.size(); i++)
            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
                out_learnt[j++] = out_learnt[i];
        
    }else if (ccmin_mode == 1){
        for (i = j = 1; i < out_learnt.size(); i++){
            Var x = var(out_learnt[i]);
 
            if (reason(x) == CRef_Undef)
                out_learnt[j++] = out_learnt[i];
            else{
                Clause& c = ca[reason(var(out_learnt[i]))];
                // Thanks to Siert Wieringa for this bug fix!
                for (int k = ((c.size()==2) ? 0:1); k < c.size(); k++)
                    if (!seen[var(c[k])] && level(var(c[k])) > 0){
                        out_learnt[j++] = out_learnt[i];
                        break; }
            }
        }
    }else
        i = j = out_learnt.size();
 
    max_literals += out_learnt.size();
    out_learnt.shrink(i - j);
    tot_literals += out_learnt.size();
 
 
    /* ***************************************
      Minimisation with binary clauses of the asserting clause
      First of all : we look for small clauses
      Then, we reduce clauses with small LBD.
      Otherwise, this can be useless
     */
    if(!incremental && out_learnt.size()<=lbSizeMinimizingClause) {
      minimisationWithBinaryResolution(out_learnt);
    }
    // Find correct backtrack level:
    //
    if (out_learnt.size() == 1)
        out_btlevel = 0;
    else{
        int max_i = 1;
        // Find the first literal assigned at the next-highest level:
        for (int i = 2; i < out_learnt.size(); i++)
            if (level(var(out_learnt[i])) > level(var(out_learnt[max_i])))
                max_i = i;
        // Swap-in this literal at index 1:
        Lit p             = out_learnt[max_i];
        out_learnt[max_i] = out_learnt[1];
        out_learnt[1]     = p;
        out_btlevel       = level(var(p));
    }
 
 
    // Compute the size of the clause without selectors (incremental mode)
    if(incremental) {
      szWithoutSelectors = 0;
      for(int i=0;i<out_learnt.size();i++) {
        if(!isSelector(var((out_learnt[i])))) szWithoutSelectors++; 
        else if(i>0) break;
      }
    } else 
      szWithoutSelectors = out_learnt.size();
    
    // Compute LBD
    lbd = computeLBD(out_learnt,out_learnt.size()-selectors.size());
 
  
#ifdef UPDATEVARACTIVITY
  // UPDATEVARACTIVITY trick (see competition'09 companion paper)
  if(lastDecisionLevel.size()>0) {
    for(int i = 0;i<lastDecisionLevel.size();i++) {
      if(ca[reason(var(lastDecisionLevel[i]))].lbd()<lbd)
        varBumpActivity(var(lastDecisionLevel[i]));
    }
    lastDecisionLevel.clear();
  } 
#endif      
 
 
 
  for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
  for(j = 0 ; j<selectors.size() ; j++) seen[var(selectors[j])] = 0;  
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ analyzeFinal()

void Solver::analyzeFinal	(	Lit	p,
		vec< Lit > &	out_conflict )

protected

Definition at line 749 of file Glucose.cpp.

{
    out_conflict.clear();
    out_conflict.push(p);
 
    if (decisionLevel() == 0)
        return;
 
    seen[var(p)] = 1;
 
    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
        Var x = var(trail[i]);
        if (seen[x]){
            if (reason(x) == CRef_Undef){
                assert(level(x) > 0);
                out_conflict.push(~trail[i]);
            }else{
                Clause& c = ca[reason(x)];
                //                for (int j = 1; j < c.size(); j++) Minisat (glucose 2.0) loop 
                // Bug in case of assumptions due to special data structures for Binary.
                // Many thanks to Sam Bayless (sbayless@cs.ubc.ca) for discover this bug.
                for (int j = ((c.size()==2) ? 0:1); j < c.size(); j++)
                    if (level(var(c[j])) > 0)
                        seen[var(c[j])] = 1;
            }  
 
            seen[x] = 0;
        }
    }
 
    seen[var(p)] = 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ attachClause()

void Solver::attachClause ( CRef cr )

protected

Definition at line 289 of file Glucose.cpp.

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

Here is the caller graph for this function:

◆ budgetOff()

void Gluco::Solver::budgetOff ( )

inline

Definition at line 442 of file Solver.h.

442{ conflict_budget = propagation_budget = -1; }

Here is the caller graph for this function:

◆ cancelUntil()

void Solver::cancelUntil ( int level )

protected

Definition at line 471 of file Glucose.cpp.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkGarbage() [1/2]

void Gluco::Solver::checkGarbage ( void )

inline

Definition at line 395 of file Solver.h.

395{ checkGarbage(garbage_frac); }

Gluco::Solver::checkGarbage

void checkGarbage()

Definition Solver.h:395

Here is the call graph for this function:

Here is the caller graph for this function:

◆ checkGarbage() [2/2]

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

inline

Definition at line 396 of file Solver.h.

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

Here is the call graph for this function:

◆ claBumpActivity()

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

inlineprotected

Definition at line 388 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ claDecayActivity()

void Gluco::Solver::claDecayActivity ( )

inlineprotected

Definition at line 387 of file Solver.h.

387{ cla_inc *= (1 / clause_decay); }

Here is the caller graph for this function:

◆ clearInterrupt()

void Gluco::Solver::clearInterrupt ( )

inline

Definition at line 441 of file Solver.h.

441{ asynch_interrupt = false; }

◆ computeLBD() [1/2]

unsigned int Solver::computeLBD ( const Clause & c )

inlineprotected

Definition at line 397 of file Glucose.cpp.

                                                      {
  int nblevels = 0;
  MYFLAG++;
 
  if(incremental) { // ----------------- INCREMENTAL MODE
     int nbDone = 0;
    for(int i=0;i<c.size();i++) {
      if(nbDone>=c.sizeWithoutSelectors()) break;
      if(isSelector(var(c[i]))) continue;
      nbDone++;
      int l = level(var(c[i]));
      if (permDiff[l] != MYFLAG) {
        permDiff[l] = MYFLAG;
        nblevels++;
      }
    }
  } else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ
    for(int i=0;i<c.size();i++) {
      int l = level(var(c[i]));
      if (permDiff[l] != MYFLAG) {
        permDiff[l] = MYFLAG;
        nblevels++;
      }
    }
  }
  return nblevels;
}

Here is the call graph for this function:

◆ computeLBD() [2/2]

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

inlineprotected

Definition at line 367 of file Glucose.cpp.

                                                                    {
  int nblevels = 0;
  MYFLAG++;
 
  if(incremental) { // ----------------- INCREMENTAL MODE
    if(end==-1) end = lits.size();
    unsigned int nbDone = 0;
    for(int i=0;i<lits.size();i++) {
      if(nbDone>=end) break;
      if(isSelector(var(lits[i]))) continue;
      nbDone++;
      int l = level(var(lits[i]));
      if (permDiff[l] != MYFLAG) {
        permDiff[l] = MYFLAG;
        nblevels++;
      }
    }
  } else { // -------- DEFAULT MODE. NOT A LOT OF DIFFERENCES... BUT EASIER TO READ
    for(int i=0;i<lits.size();i++) {
      int l = level(var(lits[i]));
      if (permDiff[l] != MYFLAG) {
        permDiff[l] = MYFLAG;
        nblevels++;
      }
    }
  }
 
  return nblevels;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ decisionLevel()

int Gluco::Solver::decisionLevel ( ) const

inlineprotected

Definition at line 417 of file Solver.h.

417{ return trail_lim.size(); }

Here is the caller graph for this function:

◆ detachClause()

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

protected

Definition at line 306 of file Glucose.cpp.

                                              {
    const Clause& c = ca[cr];
    
    assert(c.size() > 1);
    if(c.size()==2) {
      if (strict){
        remove(watchesBin[~c[0]], Watcher(cr, c[1]));
        remove(watchesBin[~c[1]], Watcher(cr, c[0]));
      }else{
        // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
        watchesBin.smudge(~c[0]);
        watchesBin.smudge(~c[1]);
      }
    } else {
      if (strict){
        remove(watches[~c[0]], Watcher(cr, c[1]));
        remove(watches[~c[1]], Watcher(cr, c[0]));
      }else{
        // Lazy detaching: (NOTE! Must clean all watcher lists before garbage collecting this clause)
        watches.smudge(~c[0]);
        watches.smudge(~c[1]);
      }
    }
    if (c.learnt()) learnts_literals -= c.size();
    else            clauses_literals -= c.size(); }

Here is the caller graph for this function:

◆ drand()

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

inlinestaticprotected

Definition at line 353 of file Solver.h.

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

Here is the caller graph for this function:

◆ enqueue()

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

inlineprotected

Definition at line 401 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ garbageCollect()

void Solver::garbageCollect ( )

virtual

Reimplemented in Gluco::SimpSolver.

Definition at line 1427 of file Glucose.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()); 
 
    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:

◆ getCex()

int * Gluco::Solver::getCex ( ) const

inline

Definition at line 428 of file Solver.h.

428{ return NULL; }

◆ initNbInitialVars()

void Solver::initNbInitialVars ( int nb )

Definition at line 190 of file Glucose.cpp.

                                     {
  nbVarsInitialFormula = nb;
}

◆ insertVarOrder()

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

inlineprotected

Definition at line 371 of file Solver.h.

371 {

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

Gluco::Solver::decision

vec< char > decision

Definition Solver.h:242

Here is the caller graph for this function:

◆ interrupt()

void Gluco::Solver::interrupt ( )

inline

Definition at line 440 of file Solver.h.

440{ asynch_interrupt = true; }

◆ irand()

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

inlinestaticprotected

Definition at line 360 of file Solver.h.

360 {

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

Gluco::Solver::drand

static double drand(double &seed)

Definition Solver.h:353

NewBdd::size

unsigned long long size

Definition giaNewBdd.h:39

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isSelector()

bool Gluco::Solver::isSelector ( Var v )

inlineprotected

Definition at line 347 of file Solver.h.

347{return (incremental && v>nbVarsInitialFormula);}

Here is the caller graph for this function:

◆ level()

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

inlineprotected

Definition at line 369 of file Solver.h.

369{ return vardata[x].level; }

Gluco::Solver::vardata

vec< VarData > vardata

Definition Solver.h:246

Here is the caller graph for this function:

◆ litRedundant()

bool Solver::litRedundant	(	Lit	p,
		uint32_t	abstract_levels )

protected

Definition at line 706 of file Glucose.cpp.

{
    analyze_stack.clear(); analyze_stack.push(p);
    int top = analyze_toclear.size();
    while (analyze_stack.size() > 0){
        assert(reason(var(analyze_stack.last())) != CRef_Undef);
        Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
        if(c.size()==2 && value(c[0])==l_False) {
          assert(value(c[1])==l_True);
          Lit tmp = c[0];
          c[0] =  c[1], c[1] = tmp;
        }
 
        for (int i = 1; i < c.size(); i++){
            Lit p  = c[i];
            if (!seen[var(p)] && level(var(p)) > 0){
                if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
                    seen[var(p)] = 1;
                    analyze_stack.push(p);
                    analyze_toclear.push(p);
                }else{
                    for (int j = top; j < analyze_toclear.size(); j++)
                        seen[var(analyze_toclear[j])] = 0;
                    analyze_toclear.shrink(analyze_toclear.size() - top);
                    return false;
                }
            }
        }
    }
 
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ locked()

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

inlineprotected

Definition at line 407 of file Solver.h.

                                                              { 
   if(c.size()>2) 
     return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; 
   return 
     (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
     || 
     (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
 }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ minimisationWithBinaryResolution()

void Solver::minimisationWithBinaryResolution ( vec< Lit > & out_learnt )

protected

Definition at line 429 of file Glucose.cpp.

                                                                  {
  
  // Find the LBD measure                                                                                                         
  unsigned int lbd = computeLBD(out_learnt);
  Lit p = ~out_learnt[0];
  
  if(lbd<=lbLBDMinimizingClause){
    MYFLAG++;
    
    for(int i = 1;i<out_learnt.size();i++) {
      permDiff[var(out_learnt[i])] = MYFLAG;
    }
 
    vec<Watcher>&  wbin  = watchesBin[p];
    int nb = 0;
    for(int k = 0;k<wbin.size();k++) {
      Lit imp = wbin[k].blocker;
      if(permDiff[var(imp)]==MYFLAG && value(imp)==l_True) {
        nb++;
        permDiff[var(imp)]= MYFLAG-1;
      }
      }
    int l = out_learnt.size()-1;
    if(nb>0) {
      nbReducedClauses++;
      for(int i = 1;i<out_learnt.size()-nb;i++) {
        if(permDiff[var(out_learnt[i])]!=MYFLAG) {
          Lit p = out_learnt[l];
          out_learnt[l] = out_learnt[i];
          out_learnt[i] = p;
          l--;i--;
        }
      }
      
      out_learnt.shrink(nb);
      
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ mkVarData()

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

inlinestaticprotected

Definition at line 202 of file Solver.h.

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

Gluco::Solver::VarData

Definition Solver.h:201

Here is the caller graph for this function:

◆ modelValue() [1/2]

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

inline

Definition at line 422 of file Solver.h.

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

Gluco::Solver::model

vec< lbool > model

Definition Solver.h:152

Here is the call graph for this function:

◆ modelValue() [2/2]

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

inline

Definition at line 421 of file Solver.h.

421{ return model[x]; }

Here is the caller graph for this function:

◆ nAssigns()

int Gluco::Solver::nAssigns ( ) const

inline

Definition at line 423 of file Solver.h.

423{ return trail.size(); }

Here is the caller graph for this function:

◆ nClauses()

int Gluco::Solver::nClauses ( ) const

inline

Definition at line 424 of file Solver.h.

424{ return clauses.size(); }

Here is the caller graph for this function:

◆ newDecisionLevel()

void Gluco::Solver::newDecisionLevel ( )

inlineprotected

Definition at line 415 of file Solver.h.

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

Here is the caller graph for this function:

◆ newVar()

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

Definition at line 202 of file Glucose.cpp.

{
    int v = nVars();
    watches  .init(mkLit(v, false));
    watches  .init(mkLit(v, true ));
    watchesBin  .init(mkLit(v, false));
    watchesBin  .init(mkLit(v, true ));
    assigns  .push(l_Undef);
    vardata  .push(mkVarData(CRef_Undef, 0));
    //activity .push(0);
    activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
    seen     .push(0);
    permDiff .push(0);
    polarity .push(sign);
    decision .push();
    trail    .capacity(v+1);
    setDecisionVar(v, dvar);
    return v;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ nFreeVars()

int Gluco::Solver::nFreeVars ( ) const

inline

Definition at line 427 of file Solver.h.

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

◆ nLearnts()

int Gluco::Solver::nLearnts ( ) const

inline

Definition at line 425 of file Solver.h.

425{ return learnts.size(); }

Here is the caller graph for this function:

◆ nVars()

int Gluco::Solver::nVars ( ) const

inline

Definition at line 426 of file Solver.h.

426{ return vardata.size(); }

Here is the caller graph for this function:

◆ okay()

bool Gluco::Solver::okay ( ) const

inline

Definition at line 457 of file Solver.h.

457{ return ok; }

◆ pickBranchLit()

Lit Solver::pickBranchLit ( )

protected

Definition at line 490 of file Glucose.cpp.

{
    Var next = var_Undef;
 
    // Random decision:
    if (drand(random_seed) < random_var_freq && !order_heap.empty()){
        next = order_heap[irand(random_seed,order_heap.size())];
        if (value(next) == l_Undef && decision[next])
            rnd_decisions++; }
 
    // Activity based decision:
    while (next == var_Undef || value(next) != l_Undef || !decision[next])
        if (order_heap.empty()){
            next = var_Undef;
            break;
        }else
            next = order_heap.removeMin();
    
    return next == var_Undef ? lit_Undef : mkLit(next, rnd_pol ? drand(random_seed) < 0.5 : (polarity[next] != 0));
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ printClause()

void Gluco::Solver::printClause ( CRef c )

inline

Definition at line 480 of file Solver.h.

{
  Clause &c = ca[cr];
    for (int i = 0; i < c.size(); i++){
        printLit(c[i]);
        printf(" ");
    }
}

Here is the call graph for this function:

◆ printIncrementalStats()

void Solver::printIncrementalStats ( )

Definition at line 1186 of file Glucose.cpp.

                                   {
 
  printf("c---------- Glucose Stats -------------------------\n");
  printf("c restarts              : %ld\n", starts);
  printf("c nb ReduceDB           : %ld\n", nbReduceDB);
  printf("c nb removed Clauses    : %ld\n", nbRemovedClauses);
  printf("c nb learnts DL2        : %ld\n", nbDL2);
  printf("c nb learnts size 2     : %ld\n", nbBin);
  printf("c nb learnts size 1     : %ld\n", nbUn);
 
  printf("c conflicts             : %ld\n", conflicts);
  printf("c decisions             : %ld\n", decisions);
  printf("c propagations          : %ld\n", propagations);
 
  printf("c SAT Calls             : %d in %g seconds\n", nbSatCalls,   totalTime4Sat);
  printf("c UNSAT Calls           : %d in %g seconds\n", nbUnsatCalls, totalTime4Unsat);
  printf("c--------------------------------------------------\n");
 
 
}

◆ printInitialClause()

void Gluco::Solver::printInitialClause ( CRef c )

inline

Definition at line 489 of file Solver.h.

{
  Clause &c = ca[cr];
    for (int i = 0; i < c.size(); i++){
      if(!isSelector(var(c[i]))) {
    printLit(c[i]);
        printf(" ");
      }
    }
}

Here is the call graph for this function:

◆ printLit()

void Gluco::Solver::printLit ( Lit l )

inline

Definition at line 474 of file Solver.h.

{
    printf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ progressEstimate()

double Solver::progressEstimate ( ) const

protected

Definition at line 1172 of file Glucose.cpp.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ propagate()

CRef Solver::propagate ( )

protected

Definition at line 803 of file Glucose.cpp.

{
    CRef    confl     = CRef_Undef;
    int     num_props = 0;
    watches.cleanAll();
    watchesBin.cleanAll();
    while (qhead < trail.size()){
        Lit            p   = trail[qhead++];     // 'p' is enqueued fact to propagate.
        vec<Watcher>&  ws  = watches[p];
        Watcher        *i, *j, *end;
        num_props++;
        
        // First, Propagate binary clauses 
        vec<Watcher>&  wbin  = watchesBin[p];
        for(int k = 0;k<wbin.size();k++) {
          Lit imp = wbin[k].blocker;
          if(value(imp) == l_False) {
            return wbin[k].cref;
          }
          if(value(imp) == l_Undef) {
            uncheckedEnqueue(imp,wbin[k].cref);
          }
        }
 
        for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
            // Try to avoid inspecting the clause:
            Lit blocker = i->blocker;
            if (value(blocker) == l_True){
                *j++ = *i++; continue; }
 
            // Make sure the false literal is data[1]:
            CRef     cr        = i->cref;
            Clause&  c         = ca[cr];
            Lit      false_lit = ~p;
            if (c[0] == false_lit)
                c[0] = c[1], c[1] = false_lit;
            assert(c[1] == false_lit);
            i++;
 
            // If 0th watch is true, then clause is already satisfied.
            Lit     first = c[0];
            Watcher w     = Watcher(cr, first);
            if (first != blocker && value(first) == l_True){
              *j++ = w; continue; }
 
            // Look for new watch:
            if(incremental) { // ----------------- INCREMENTAL MODE
              int choosenPos = -1;
              for (int k = 2; k < c.size(); k++) {
                
                if (value(c[k]) != l_False){
                  if(decisionLevel()>assumptions.size()) {
                    choosenPos = k;
                    break;
                  } else {
                    choosenPos = k;
                    
                    if(value(c[k])==l_True || !isSelector(var(c[k]))) {
                      break;
                    }
                  }
 
                }
              }
              if(choosenPos!=-1) {
                c[1] = c[choosenPos]; c[choosenPos] = false_lit;
                watches[~c[1]].push(w);
                goto NextClause; }
            } else {  // ----------------- DEFAULT  MODE (NOT INCREMENTAL)
              for (int k = 2; k < c.size(); k++) {
                
                if (value(c[k]) != l_False){
                  c[1] = c[k]; c[k] = false_lit;
                  watches[~c[1]].push(w);
                  goto NextClause; }
              }
            }
 
            // Did not find watch -- clause is unit under assignment:
            *j++ = w;
            if (value(first) == l_False){
                confl = cr;
                qhead = trail.size();
                // Copy the remaining watches:
                while (i < end)
                    *j++ = *i++;
            }else {
                uncheckedEnqueue(first, cr);
          
                
            }
        NextClause:;
        }
        ws.shrink(i - j);
    }
    propagations += num_props;
    simpDB_props -= num_props;
    
    return confl;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reason()

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

inlineprotected

Definition at line 368 of file Solver.h.

368{ return vardata[x].reason; }

Here is the caller graph for this function:

◆ rebuildOrderHeap()

void Solver::rebuildOrderHeap ( )

protected

Definition at line 981 of file Glucose.cpp.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reduceDB()

void Solver::reduceDB ( )

protected

Definition at line 935 of file Glucose.cpp.

{ 
  int i, j;
  nbReduceDB++;
  sort(learnts, reduceDB_lt(ca));
 
  // We have a lot of "good" clauses, it is difficult to compare them. Keep more !
  if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd()<=3) nbclausesbeforereduce +=specialIncReduceDB; 
  // Useless :-)
  if(ca[learnts.last()].lbd()<=5)  nbclausesbeforereduce +=specialIncReduceDB;   
  
  // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
  // Keep clauses which seem to be usefull (their lbd was reduce during this sequence)
 
  int limit = learnts.size() / 2;
  for (i = j = 0; i < learnts.size(); i++){
    Clause& c = ca[learnts[i]];
    if (c.lbd()>2 && c.size() > 2 && c.canBeDel() &&  !locked(c) && (i < limit)) {
      removeClause(learnts[i]);
      nbRemovedClauses++;
    }
    else {
      if(!c.canBeDel()) limit++; //we keep c, so we can delete an other clause
      c.setCanBeDel(true);       // At the next step, c can be delete
      learnts[j++] = learnts[i];
    }
  }
  learnts.shrink(i - j);
  checkGarbage();
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ relocAll()

void Solver::relocAll ( ClauseAllocator & to )

protected

Definition at line 1386 of file Glucose.cpp.

{
    int v, s, i, j;
    // All watchers:
    //
    // for (int i = 0; i < watches.size(); i++)
    watches.cleanAll();
    watchesBin.cleanAll();
    for (v = 0; v < nVars(); v++)
        for (s = 0; s < 2; s++){
            Lit p = mkLit(v, s != 0);
            // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
            vec<Watcher>& ws = watches[p];
            for (j = 0; j < ws.size(); j++)
                ca.reloc(ws[j].cref, to);
            vec<Watcher>& ws2 = watchesBin[p];
            for (j = 0; j < ws2.size(); j++)
                ca.reloc(ws2[j].cref, to);
        }
 
    // All reasons:
    //
    for (i = 0; i < trail.size(); i++){
        Var v = var(trail[i]);
 
        if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
            ca.reloc(vardata[v].reason, to);
    }
 
    // All learnt:
    //
    for (i = 0; i < learnts.size(); i++)
        ca.reloc(learnts[i], to);
 
    // All original:
    //
    for (i = 0; i < clauses.size(); i++)
        ca.reloc(clauses[i], to);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeClause()

void Solver::removeClause ( CRef cr )

protected

Definition at line 333 of file Glucose.cpp.

                                 {
 
  Clause& c = ca[cr];
 
  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);
  // Don't leave pointers to free'd memory!
  if (locked(c)) vardata[var(c[0])].reason = CRef_Undef;
  c.mark(1);
  ca.free_(cr);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ removeSatisfied()

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

protected

Definition at line 967 of file Glucose.cpp.

{
    int i, j;
    for (i = j = 0; i < cs.size(); i++){
        Clause& c = ca[cs[i]];
        if (satisfied(c)) 
            removeClause(cs[i]);
        else
            cs[j++] = cs[i];
    }
    cs.shrink(i - j);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ reset()

void Solver::reset ( )

virtual

Reimplemented in Gluco::SimpSolver.

Definition at line 1440 of file Glucose.cpp.

{
    // Reset everything
    ok = true;
    K = (double)opt_K;
    R = (double)opt_R;
    firstReduceDB = opt_first_reduce_db;
    var_decay = (double)opt_var_decay;
    //max_var_decay = opt_max_var_decay;
    solves = starts = decisions = propagations = conflicts = conflictsRestarts = 0;
    curRestart = 1;
    cla_inc = var_inc = 1;
    watches.clear(false); // We don't free the memory, new calls should be of the same size order.
    watchesBin.clear(false); 
    //unaryWatches.clear(false);
    qhead = 0;
    simpDB_assigns = -1;
    simpDB_props = 0;
    order_heap.clear(false);
    progress_estimate = 0;
    //lastLearntClause = CRef_Undef;
    conflict_budget = -1;
    propagation_budget = -1;
    nbVarsInitialFormula = INT32_MAX;
    totalTime4Sat = 0.;
    totalTime4Unsat = 0.;
    nbSatCalls = nbUnsatCalls = 0;
    MYFLAG = 0;
    lbdQueue.clear(false);
    lbdQueue.initSize(sizeLBDQueue);
    trailQueue.clear(false);
    trailQueue.initSize(sizeTrailQueue);
    sumLBD = 0;
    nbclausesbeforereduce = firstReduceDB;
    //stats.clear();
    //stats.growTo(coreStatsSize, 0);
    clauses.clear(false);
    learnts.clear(false);
    //permanentLearnts.clear(false);
    //unaryWatchedClauses.clear(false);
    model.clear(false);
    conflict.clear(false);
    activity.clear(false);
    assigns.clear(false);
    polarity.clear(false);
    //forceUNSAT.clear(false);
    decision.clear(false);
    trail.clear(false);
    nbpos.clear(false);
    trail_lim.clear(false);
    vardata.clear(false);
    assumptions.clear(false);
    permDiff.clear(false);
    lastDecisionLevel.clear(false);
    ca.clear();
    seen.clear(false);
    analyze_stack.clear(false);
    analyze_toclear.clear(false);
    add_tmp.clear(false);
    assumptionPositions.clear(false);
    initialPositions.clear(false);
}

Here is the caller graph for this function:

◆ sat_solver_mark_cone()

void Gluco::Solver::sat_solver_mark_cone ( int var )

inline

Definition at line 468 of file Solver.h.

468{}

Here is the call graph for this function:

◆ sat_solver_set_var_fanin_lit()

void Gluco::Solver::sat_solver_set_var_fanin_lit	(	int	var,
		int	lit0,
		int	lit1 )

inline

Definition at line 466 of file Solver.h.

466{}

Here is the call graph for this function:

◆ sat_solver_start_new_round()

void Gluco::Solver::sat_solver_start_new_round ( )

inline

Definition at line 467 of file Solver.h.

467{}

◆ satisfied()

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

protected

Definition at line 352 of file Glucose.cpp.

                                            {
  if(incremental)  // Check clauses with many selectors is too time consuming
    return (value(c[0]) == l_True) || (value(c[1]) == l_True);
 
  // Default mode.
    for (int i = 0; i < c.size(); i++)
        if (value(c[i]) == l_True)
            return true;
    return false; 
}

Here is the caller graph for this function:

◆ search()

lbool Solver::search ( int nof_conflicts )

protected

Definition at line 1038 of file Glucose.cpp.

{
    assert(ok);
    int         backtrack_level;
    int         conflictC = 0;
    vec<Lit>    learnt_clause,selectors;
    unsigned int nblevels,szWoutSelectors;
    bool blocked=false;
    starts++;
    for (;;){
        CRef confl = propagate();
        if (confl != CRef_Undef){
            // CONFLICT
          conflicts++; conflictC++;conflictsRestarts++;
          if(conflicts%5000==0 && var_decay<0.95)
            var_decay += 0.01;
 
          if (verbosity >= 1 && conflicts%verbEveryConflicts==0){
            printf("c | %8d   %7d    %5d | %7d %8d %8d | %5d %8d   %6d %8d | %6.3f %% |\n", 
                   (int)starts,(int)nbstopsrestarts, (int)(conflicts/starts), 
                   (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
                   (int)nbReduceDB, nLearnts(), (int)nbDL2,(int)nbRemovedClauses, progressEstimate()*100);
          }
          if (decisionLevel() == 0) {
            return l_False;
            
          }
 
          trailQueue.push(trail.size());
          // BLOCK RESTART (CP 2012 paper)
          if( conflictsRestarts>LOWER_BOUND_FOR_BLOCKING_RESTART && lbdQueue.isvalid()  && trail.size()>R*trailQueue.getavg()) {
            lbdQueue.fastclear();
            nbstopsrestarts++;
            if(!blocked) {lastblockatrestart=starts;nbstopsrestartssame++;blocked=true;}
          }
 
            learnt_clause.clear();
            selectors.clear();
            analyze(confl, learnt_clause, selectors,backtrack_level,nblevels,szWoutSelectors);
 
            lbdQueue.push(nblevels);
            sumLBD += nblevels;
 
            cancelUntil(backtrack_level);
 
            if (certifiedUNSAT) {
              for (int i = 0; i < learnt_clause.size(); i++)
                fprintf(certifiedOutput, "%i " , (var(learnt_clause[i]) + 1) *
                            (-2 * sign(learnt_clause[i]) + 1) );
              fprintf(certifiedOutput, "0\n");
            }
 
            if (learnt_clause.size() == 1){
              uncheckedEnqueue(learnt_clause[0]);nbUn++;
            }else{
                CRef cr = ca.alloc(learnt_clause, true);
                ca[cr].setLBD(nblevels); 
                ca[cr].setSizeWithoutSelectors(szWoutSelectors);
                if(nblevels<=2) nbDL2++; // stats
                if(ca[cr].size()==2) nbBin++; // stats
                learnts.push(cr);
                attachClause(cr);
 
                claBumpActivity(ca[cr]);
                uncheckedEnqueue(learnt_clause[0], cr);
            }
            varDecayActivity();
            claDecayActivity();
 
           
        }else{
 
          // Our dynamic restart, see the SAT09 competition compagnion paper 
          if ( (conflictsRestarts && lbdQueue.isvalid() && lbdQueue.getavg()*K > sumLBD/conflictsRestarts) || (pstop && *pstop) ) {
            lbdQueue.fastclear();
            progress_estimate = progressEstimate();
            int bt = 0;
            if(incremental) { // DO NOT BACKTRACK UNTIL 0.. USELESS
              bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
            }
            cancelUntil(bt);
            return l_Undef; 
          }
 
           // Simplify the set of problem clauses:
          if (decisionLevel() == 0 && !simplify()) {
            return l_False;
          }
            // Perform clause database reduction !
            if(conflicts>=curRestart* nbclausesbeforereduce && learnts.size()>0) 
              {
                  
                assert(learnts.size()>0);
                curRestart = (conflicts/ nbclausesbeforereduce)+1;
                reduceDB();
                nbclausesbeforereduce += incReduceDB;
              }
 
            Lit next = lit_Undef;
            while (decisionLevel() < assumptions.size()){
                // Perform user provided assumption:
                Lit p = assumptions[decisionLevel()];
                if (value(p) == l_True){
                    // Dummy decision level:
                    newDecisionLevel();
                }else if (value(p) == l_False){
                    analyzeFinal(~p, conflict);
                    return l_False;
                }else{
                    next = p;
                    break;
                }
            }
 
            if (next == lit_Undef){
                // New variable decision:
                decisions++;
                next = pickBranchLit();
 
                if (next == lit_Undef){
                  //printf("c last restart ## conflicts  :  %d %d \n",conflictC,decisionLevel());
                  // Model found:
                  return l_True;
                }
            }
 
            // Increase decision level and enqueue 'next'
            newDecisionLevel();
            uncheckedEnqueue(next);
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setConfBudget()

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

inline

Definition at line 438 of file Solver.h.

438{ conflict_budget = conflicts + x; }

◆ setDecisionVar()

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

inline

Definition at line 430 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setIncrementalMode()

void Solver::setIncrementalMode ( )

Definition at line 185 of file Glucose.cpp.

                                {
  incremental = true;
}

Here is the caller graph for this function:

◆ setPolarity()

void Gluco::Solver::setPolarity	(	Var	v,
		bool	b )

inline

Definition at line 429 of file Solver.h.

429{ polarity[v] = b; }

◆ setPropBudget()

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

inline

Definition at line 439 of file Solver.h.

439{ propagation_budget = propagations + x; }

◆ simplify()

bool Solver::simplify ( )

Definition at line 999 of file Glucose.cpp.

{
    assert(decisionLevel() == 0);
 
    if (!ok || propagate() != CRef_Undef)
        return ok = false;
 
    if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
        return true;
 
    // Remove satisfied clauses:
    removeSatisfied(learnts);
    if (remove_satisfied)        // Can be turned off.
        removeSatisfied(clauses);
 
    checkGarbage();
 
    rebuildOrderHeap();
 
    simpDB_assigns = nAssigns();
    simpDB_props   = clauses_literals + learnts_literals;   // (shouldn't depend on stats really, but it will do for now)
 
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ solve() [1/5]

bool Gluco::Solver::solve ( )

inline

Definition at line 451 of file Solver.h.

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

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::Solver::solve ( const vec< Lit > & assumps )

inline

Definition at line 455 of file Solver.h.

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

Here is the call graph for this function:

◆ solve() [3/5]

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

inline

Definition at line 452 of file Solver.h.

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

Here is the call graph for this function:

◆ solve() [4/5]

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

inline

Definition at line 453 of file Solver.h.

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

Here is the call graph for this function:

◆ solve() [5/5]

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

inline

Definition at line 454 of file Solver.h.

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

Here is the call graph for this function:

◆ solve_()

lbool Solver::solve_ ( )

protected

Definition at line 1209 of file Glucose.cpp.

{
 
  if(incremental && certifiedUNSAT) {
    printf("Can not use incremental and certified unsat in the same time\n");
    exit(-1);
  }
    model.clear();
    conflict.clear();
    if (!ok) return l_False;
    double curTime = cpuTime();
 
    
    solves++;
            
 
    
    lbool   status        = l_Undef;
    if(!incremental && verbosity>=1) {
      printf("c ========================================[ MAGIC CONSTANTS ]==============================================\n");
      printf("c | Constants are supposed to work well together :-)                                                      |\n");
      printf("c | however, if you find better choices, please let us known...                                           |\n");
      printf("c |-------------------------------------------------------------------------------------------------------|\n");
    printf("c |                                |                                |                                     |\n"); 
    printf("c | - Restarts:                    | - Reduce Clause DB:            | - Minimize Asserting:               |\n");
    printf("c |   * LBD Queue    : %6d      |   * First     : %6d         |    * size < %3d                     |\n",lbdQueue.maxSize(),nbclausesbeforereduce,lbSizeMinimizingClause);
    printf("c |   * Trail  Queue : %6d      |   * Inc       : %6d         |    * lbd  < %3d                     |\n",trailQueue.maxSize(),incReduceDB,lbLBDMinimizingClause);
    printf("c |   * K            : %6.2f      |   * Special   : %6d         |                                     |\n",K,specialIncReduceDB);
    printf("c |   * R            : %6.2f      |   * Protected :  (lbd)< %2d     |                                     |\n",R,lbLBDFrozenClause);
    printf("c |                                |                                |                                     |\n"); 
printf("c ==================================[ Search Statistics (every %6d conflicts) ]=========================\n",verbEveryConflicts);
      printf("c |                                                                                                       |\n"); 
 
      printf("c |          RESTARTS           |          ORIGINAL         |              LEARNT              | Progress |\n");
      printf("c |       NB   Blocked  Avg Cfc |    Vars  Clauses Literals |   Red   Learnts    LBD2  Removed |          |\n");
      printf("c =========================================================================================================\n");
    }
 
    // Search:
    int curr_restarts = 0;
    while (status == l_Undef){
      status = search(0); // the parameter is useless in glucose, kept to allow modifications
        if (!withinBudget() || terminate_search_early || (pstop && *pstop)) break;
        if (nRuntimeLimit && Abc_Clock() > nRuntimeLimit)                   break;
        curr_restarts++;
    }
 
    if (!incremental && verbosity >= 1)
      printf("c =========================================================================================================\n");
 
 
    if (certifiedUNSAT){ // Want certified output
      if (status == l_False)
        fprintf(certifiedOutput, "0\n");
      fclose(certifiedOutput);
    }
 
 
    if (status == l_True){
        // Extend & copy model:
        model.growTo(nVars());
        for (int i = 0; i < nVars(); i++) model[i] = value(i);
    }else if (status == l_False && conflict.size() == 0)
        ok = false;
 
    cancelUntil(0);
 
    double finalTime = cpuTime();
    if(status==l_True) {
      nbSatCalls++; 
      totalTime4Sat +=(finalTime-curTime);
    }
    if(status==l_False) {
      nbUnsatCalls++; 
      totalTime4Unsat +=(finalTime-curTime);
    }
 
    // ABC callback
    if (pCnfFunc && !terminate_search_early) {// hack to avoid calling callback twise if the solver was terminated early
        int * pCex = NULL;
        int message = (status == l_True ? 1 : status == l_False ? 0 : -1);
        if (status == l_True) {
            pCex = new int[nVars()];
            for (int i = 0; i < nVars(); i++)
                pCex[i] = (model[i] == l_True);
        }
        
        int callback_result = pCnfFunc(pCnfMan, message, pCex);
        assert(callback_result == 0);
    }
    else if (pCnfFunc)
        terminate_search_early = false; // for next run
 
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ solveLimited()

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

inline

Definition at line 456 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [1/7]

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

inline

Definition at line 459 of file Solver.h.

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

Gluco::Solver::toDimacs

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

Definition Glucose.cpp:1341

file

struct file file

Definition file.h:21

Here is the call graph for this function:

◆ toDimacs() [2/7]

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

Definition at line 1331 of file Glucose.cpp.

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

Here is the call graph for this function:

◆ toDimacs() [3/7]

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

inline

Definition at line 460 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [4/7]

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

inline

Definition at line 461 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [5/7]

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

inline

Definition at line 462 of file Solver.h.

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

Here is the call graph for this function:

◆ toDimacs() [6/7]

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

Definition at line 1320 of file Glucose.cpp.

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

Here is the call graph for this function:

◆ toDimacs() [7/7]

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

Definition at line 1341 of file Glucose.cpp.

{
    // Handle case when solver is in contradictory state:
    if (!ok){
        fprintf(f, "p cnf 1 2\n1 0\n-1 0\n");
        return; }
 
    vec<Var> map; Var max = 0;
 
    // Cannot use removeClauses here because it is not safe
    // to deallocate them at this point. Could be improved.
    int i, cnt = 0;
    for (i = 0; i < clauses.size(); i++)
        if (!satisfied(ca[clauses[i]]))
            cnt++;
        
    for (i = 0; i < clauses.size(); i++)
        if (!satisfied(ca[clauses[i]])){
            Clause& c = ca[clauses[i]];
            for (int j = 0; j < c.size(); j++)
                if (value(c[j]) != l_False)
                    mapVar(var(c[j]), map, max);
        }
 
    // Assumptions are added as unit clauses:
    cnt += assumptions.size();
 
    fprintf(f, "p cnf %d %d\n", max, cnt);
 
    for (i = 0; i < assumptions.size(); i++){
        assert(value(assumptions[i]) != l_False);
        fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
    }
 
    for (i = 0; i < clauses.size(); i++)
        toDimacs(f, ca[clauses[i]], map, max);
 
    if (verbosity > 0)
        printf("Wrote %d clauses with %d variables.\n", cnt, max);
}

Here is the call graph for this function:

Here is the caller graph for this function:

◆ uncheckedEnqueue()

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

protected

Definition at line 783 of file Glucose.cpp.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ value() [1/2]

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

inline

Definition at line 420 of file Solver.h.

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

Here is the call graph for this function:

◆ value() [2/2]

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

inline

Definition at line 419 of file Solver.h.

419{ return assigns[x]; }

Here is the caller graph for this function:

◆ varBumpActivity() [1/2]

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

inlineprotected

Definition at line 375 of file Solver.h.

375{ varBumpActivity(v, var_inc); }

Here is the call graph for this function:

◆ varBumpActivity() [2/2]

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

inlineprotected

Definition at line 376 of file Solver.h.

                                                     {
    if ( (activity[v] += inc) > 1e100 ) {
        // Rescale:
        for (int i = 0; i < nVars(); i++)
            activity[i] *= 1e-100;
        var_inc *= 1e-100; }
 
    // Update order_heap with respect to new activity:
    if (order_heap.inHeap(v))
        order_heap.decrease(v); }

Here is the call graph for this function:

Here is the caller graph for this function:

◆ varDecayActivity()

void Gluco::Solver::varDecayActivity ( )

inlineprotected

Definition at line 374 of file Solver.h.

374{ var_inc *= (1 / var_decay); }

Here is the caller graph for this function:

◆ withinBudget()

bool Gluco::Solver::withinBudget ( ) const

inlineprotected

Definition at line 443 of file Solver.h.

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

Here is the caller graph for this function:

Member Data Documentation

◆ activity

vec<double> Gluco::Solver::activity

protected

Definition at line 231 of file Solver.h.

◆ add_tmp

vec<Lit> Gluco::Solver::add_tmp

protected

Definition at line 276 of file Solver.h.

◆ analyze_stack

vec<Lit> Gluco::Solver::analyze_stack

protected

Definition at line 274 of file Solver.h.

◆ analyze_toclear

vec<Lit> Gluco::Solver::analyze_toclear

protected

Definition at line 275 of file Solver.h.

◆ assigns

vec<lbool> Gluco::Solver::assigns

protected

Definition at line 240 of file Solver.h.

◆ assumptionPositions

vec<int> Gluco::Solver::assumptionPositions

protected

Definition at line 296 of file Solver.h.

◆ assumptions

vec<Lit> Gluco::Solver::assumptions

protected

Definition at line 250 of file Solver.h.

◆ asynch_interrupt

bool Gluco::Solver::asynch_interrupt

protected

Definition at line 288 of file Solver.h.

◆ ca

ClauseAllocator Gluco::Solver::ca

protected

Definition at line 261 of file Solver.h.

◆ ccmin_mode

int Gluco::Solver::ccmin_mode

Definition at line 181 of file Solver.h.

◆ certifiedOutput

FILE* Gluco::Solver::certifiedOutput

Definition at line 188 of file Solver.h.

◆ certifiedUNSAT

bool Gluco::Solver::certifiedUNSAT

Definition at line 189 of file Solver.h.

◆ cla_inc

double Gluco::Solver::cla_inc

protected

Definition at line 230 of file Solver.h.

◆ clause_decay

double Gluco::Solver::clause_decay

Definition at line 178 of file Solver.h.

◆ clauses

vec<CRef> Gluco::Solver::clauses

protected

Definition at line 237 of file Solver.h.

◆ clauses_literals

int64_t Gluco::Solver::clauses_literals

Definition at line 195 of file Solver.h.

◆ conflict

vec<Lit> Gluco::Solver::conflict

Definition at line 153 of file Solver.h.

◆ conflict_budget

int64_t Gluco::Solver::conflict_budget

protected

Definition at line 286 of file Solver.h.

◆ conflicts

int64_t Gluco::Solver::conflicts

Definition at line 194 of file Solver.h.

◆ conflictsRestarts

int64_t Gluco::Solver::conflictsRestarts

Definition at line 194 of file Solver.h.

◆ curRestart

long Gluco::Solver::curRestart

protected

Definition at line 198 of file Solver.h.

◆ dec_vars

int64_t Gluco::Solver::dec_vars

Definition at line 195 of file Solver.h.

◆ decision

vec<char> Gluco::Solver::decision

protected

Definition at line 242 of file Solver.h.

◆ decisions

int64_t Gluco::Solver::decisions

Definition at line 194 of file Solver.h.

◆ firstReduceDB

int Gluco::Solver::firstReduceDB

Definition at line 168 of file Solver.h.

◆ garbage_frac

double Gluco::Solver::garbage_frac

Definition at line 185 of file Solver.h.

◆ incReduceDB

int Gluco::Solver::incReduceDB

Definition at line 169 of file Solver.h.

◆ incremental

int Gluco::Solver::incremental

protected

Definition at line 292 of file Solver.h.

◆ initialPositions

vec<int> Gluco::Solver::initialPositions

protected

Definition at line 296 of file Solver.h.

◆ jftr

int Gluco::Solver::jftr

Definition at line 68 of file Solver.h.

◆ K

double Gluco::Solver::K

Definition at line 162 of file Solver.h.

◆ lastblockatrestart

int64_t Gluco::Solver::lastblockatrestart

Definition at line 194 of file Solver.h.

◆ lastIndexRed

int Gluco::Solver::lastIndexRed

protected

Definition at line 228 of file Solver.h.

◆ lbdQueue

bqueue<unsigned int> Gluco::Solver::lbdQueue

protected

Definition at line 265 of file Solver.h.

◆ lbLBDFrozenClause

unsigned int Gluco::Solver::lbLBDFrozenClause

Definition at line 171 of file Solver.h.

◆ lbLBDMinimizingClause

unsigned int Gluco::Solver::lbLBDMinimizingClause

Definition at line 175 of file Solver.h.

◆ lbSizeMinimizingClause

int Gluco::Solver::lbSizeMinimizingClause

Definition at line 174 of file Solver.h.

◆ learnts

vec<CRef> Gluco::Solver::learnts

protected

Definition at line 238 of file Solver.h.

◆ learnts_literals

int64_t Gluco::Solver::learnts_literals

Definition at line 195 of file Solver.h.

◆ learntsize_adjust_cnt

int Gluco::Solver::learntsize_adjust_cnt

protected

Definition at line 282 of file Solver.h.

◆ learntsize_adjust_confl

double Gluco::Solver::learntsize_adjust_confl

protected

Definition at line 281 of file Solver.h.

◆ max_learnts

double Gluco::Solver::max_learnts

protected

Definition at line 280 of file Solver.h.

◆ max_literals

int64_t Gluco::Solver::max_literals

Definition at line 195 of file Solver.h.

◆ model

vec<lbool> Gluco::Solver::model

Definition at line 152 of file Solver.h.

◆ MYFLAG

unsigned int Gluco::Solver::MYFLAG

protected

Definition at line 277 of file Solver.h.

◆ nbBin

int64_t Gluco::Solver::nbBin

Definition at line 194 of file Solver.h.

◆ nbclausesbeforereduce

int Gluco::Solver::nbclausesbeforereduce

protected

Definition at line 263 of file Solver.h.

◆ nbDL2

int64_t Gluco::Solver::nbDL2

Definition at line 194 of file Solver.h.

◆ nbpos

vec<int> Gluco::Solver::nbpos

protected

Definition at line 244 of file Solver.h.

◆ nbReduceDB

int64_t Gluco::Solver::nbReduceDB

Definition at line 194 of file Solver.h.

◆ nbReducedClauses

int64_t Gluco::Solver::nbReducedClauses

Definition at line 194 of file Solver.h.

◆ nbRemovedClauses

int64_t Gluco::Solver::nbRemovedClauses

Definition at line 194 of file Solver.h.

◆ nbSatCalls

int Gluco::Solver::nbSatCalls

protected

Definition at line 295 of file Solver.h.

◆ nbstopsrestarts

int64_t Gluco::Solver::nbstopsrestarts

Definition at line 194 of file Solver.h.

◆ nbstopsrestartssame

int64_t Gluco::Solver::nbstopsrestartssame

Definition at line 194 of file Solver.h.

◆ nbUn

int64_t Gluco::Solver::nbUn

Definition at line 194 of file Solver.h.

◆ nbUnsatCalls

int Gluco::Solver::nbUnsatCalls

protected

Definition at line 295 of file Solver.h.

◆ nbVarsInitialFormula

int Gluco::Solver::nbVarsInitialFormula

protected

Definition at line 293 of file Solver.h.

◆ nCallConfl

int Gluco::Solver::nCallConfl

Definition at line 60 of file Solver.h.

◆ nRuntimeLimit

uint64_t Gluco::Solver::nRuntimeLimit

Definition at line 63 of file Solver.h.

◆ ok

bool Gluco::Solver::ok

protected

Definition at line 229 of file Solver.h.

◆ order_heap

Heap<VarOrderLt> Gluco::Solver::order_heap

protected

Definition at line 251 of file Solver.h.

◆ pCnfFunc

int(* Gluco::Solver::pCnfFunc) (void *p, int, int *)

Definition at line 59 of file Solver.h.

◆ pCnfMan

void* Gluco::Solver::pCnfMan

Definition at line 58 of file Solver.h.

◆ permDiff

vec<unsigned int> Gluco::Solver::permDiff

protected

Definition at line 254 of file Solver.h.

◆ phase_saving

int Gluco::Solver::phase_saving

Definition at line 182 of file Solver.h.

◆ polarity

vec<char> Gluco::Solver::polarity

protected

Definition at line 241 of file Solver.h.

◆ progress_estimate

double Gluco::Solver::progress_estimate

protected

Definition at line 252 of file Solver.h.

◆ propagation_budget

int64_t Gluco::Solver::propagation_budget

protected

Definition at line 287 of file Solver.h.

◆ propagations

int64_t Gluco::Solver::propagations

Definition at line 194 of file Solver.h.

◆ pstop

int* Gluco::Solver::pstop

Definition at line 62 of file Solver.h.

◆ qhead

int Gluco::Solver::qhead

protected

Definition at line 247 of file Solver.h.

◆ R

double Gluco::Solver::R

Definition at line 163 of file Solver.h.

◆ random_seed

double Gluco::Solver::random_seed

Definition at line 180 of file Solver.h.

◆ random_var_freq

double Gluco::Solver::random_var_freq

Definition at line 179 of file Solver.h.

◆ remove_satisfied

bool Gluco::Solver::remove_satisfied

protected

Definition at line 253 of file Solver.h.

◆ rnd_decisions

int64_t Gluco::Solver::rnd_decisions

Definition at line 194 of file Solver.h.

◆ rnd_init_act

bool Gluco::Solver::rnd_init_act

Definition at line 184 of file Solver.h.

◆ rnd_pol

bool Gluco::Solver::rnd_pol

Definition at line 183 of file Solver.h.

◆ seen

vec<char> Gluco::Solver::seen

protected

Definition at line 273 of file Solver.h.

◆ showModel

int Gluco::Solver::showModel

Definition at line 160 of file Solver.h.

◆ simpDB_assigns

int Gluco::Solver::simpDB_assigns

protected

Definition at line 248 of file Solver.h.

◆ simpDB_props

int64_t Gluco::Solver::simpDB_props

protected

Definition at line 249 of file Solver.h.

◆ sizeLBDQueue

double Gluco::Solver::sizeLBDQueue

Definition at line 164 of file Solver.h.

◆ sizeTrailQueue

double Gluco::Solver::sizeTrailQueue

Definition at line 165 of file Solver.h.

◆ SolverType

int Gluco::Solver::SolverType

Definition at line 50 of file Solver.h.

◆ solves

int64_t Gluco::Solver::solves

Definition at line 194 of file Solver.h.

◆ specialIncReduceDB

int Gluco::Solver::specialIncReduceDB

Definition at line 170 of file Solver.h.

◆ starts

int64_t Gluco::Solver::starts

Definition at line 194 of file Solver.h.

◆ sumAssumptions

int Gluco::Solver::sumAssumptions

protected

Definition at line 267 of file Solver.h.

◆ sumLBD

float Gluco::Solver::sumLBD

protected

Definition at line 266 of file Solver.h.

◆ terminate_search_early

bool Gluco::Solver::terminate_search_early

Definition at line 61 of file Solver.h.

◆ tot_literals

int64_t Gluco::Solver::tot_literals

Definition at line 195 of file Solver.h.

◆ totalTime4Sat

double Gluco::Solver::totalTime4Sat

protected

Definition at line 294 of file Solver.h.

◆ totalTime4Unsat

double Gluco::Solver::totalTime4Unsat

protected

Definition at line 294 of file Solver.h.

◆ trail

vec<Lit> Gluco::Solver::trail

protected

Definition at line 243 of file Solver.h.

◆ trail_lim

vec<int> Gluco::Solver::trail_lim

protected

Definition at line 245 of file Solver.h.

◆ trailQueue

bqueue<unsigned int> Gluco::Solver::trailQueue

protected

Definition at line 265 of file Solver.h.

◆ user_lits

vec<Lit> Gluco::Solver::user_lits

Definition at line 65 of file Solver.h.

◆ user_vec

vec<int> Gluco::Solver::user_vec

Definition at line 64 of file Solver.h.

◆ var_decay

double Gluco::Solver::var_decay

Definition at line 177 of file Solver.h.

◆ var_inc

double Gluco::Solver::var_inc

protected

Definition at line 232 of file Solver.h.

◆ vardata

vec<VarData> Gluco::Solver::vardata

protected

Definition at line 246 of file Solver.h.

◆ verbEveryConflicts

int Gluco::Solver::verbEveryConflicts

Definition at line 159 of file Solver.h.

◆ verbosity

int Gluco::Solver::verbosity

Definition at line 158 of file Solver.h.

◆ watches

OccLists<Lit, vec<Watcher>, WatcherDeleted> Gluco::Solver::watches

protected

Definition at line 234 of file Solver.h.

◆ watchesBin

OccLists<Lit, vec<Watcher>, WatcherDeleted> Gluco::Solver::watchesBin

protected

Definition at line 236 of file Solver.h.

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

src/sat/glucose/Solver.h
src/sat/glucose/Glucose.cpp

Classes

Public Member Functions

Public Attributes

Protected Member Functions

Static Protected Member Functions

Protected Attributes

Detailed Description

Constructor & Destructor Documentation

◆ Solver()

◆ ~Solver()

Member Function Documentation

◆ abstractLevel()

◆ addClause() [1/4]

◆ addClause() [2/4]

◆ addClause() [3/4]

◆ addClause() [4/4]

◆ addClause_()

◆ addEmptyClause()

◆ addVar()

◆ analyze()

◆ analyzeFinal()

◆ attachClause()

◆ budgetOff()

◆ cancelUntil()

◆ checkGarbage() [1/2]

◆ checkGarbage() [2/2]

◆ claBumpActivity()

◆ claDecayActivity()

◆ clearInterrupt()

◆ computeLBD() [1/2]

◆ computeLBD() [2/2]

◆ decisionLevel()

◆ detachClause()

◆ drand()

◆ enqueue()

◆ garbageCollect()

◆ getCex()

◆ initNbInitialVars()

◆ insertVarOrder()

◆ interrupt()

◆ irand()

◆ isSelector()

◆ level()

◆ litRedundant()

◆ locked()

◆ minimisationWithBinaryResolution()

◆ mkVarData()

◆ modelValue() [1/2]

◆ modelValue() [2/2]

◆ nAssigns()

◆ nClauses()

◆ newDecisionLevel()

◆ newVar()

◆ nFreeVars()

◆ nLearnts()

◆ nVars()

◆ okay()

◆ pickBranchLit()

◆ printClause()

◆ printIncrementalStats()

◆ printInitialClause()

◆ printLit()

◆ progressEstimate()

◆ propagate()

◆ reason()

◆ rebuildOrderHeap()

◆ reduceDB()

◆ relocAll()

◆ removeClause()

◆ removeSatisfied()

◆ reset()

◆ sat_solver_mark_cone()

◆ sat_solver_set_var_fanin_lit()

◆ sat_solver_start_new_round()

◆ satisfied()

◆ search()

◆ setConfBudget()

◆ setDecisionVar()

◆ setIncrementalMode()

◆ setPolarity()