Gluco2::Solver Class Reference

#include <Solver.h>

Inheritance diagram for Gluco2::Solver:

Collaboration diagram for Gluco2::Solver:

Classes
struct	JustKey
struct	JustOrderLt2
struct	NodeData
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)
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 ()
virtual void	reset ()
virtual void	garbageCollect ()
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	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
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 ()

Static Protected Member Functions
static VarData	mkVarData (CRef cr, int l)
static double	drand (double &seed)
static int	irand (double &seed, int size)
static NodeData	mkNodeData ()

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

Detailed Description

Definition at line 49 of file Solver.h.

Constructor & Destructor Documentation

Solver()

Solver::Solver

(

)

Definition at line 91 of file Glucose2.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)
 
  #ifdef CGLUCOSE_EXP
  //, jheap         (JustOrderLt(this))
  , jheap         (JustOrderLt2(this))
  #endif
{
  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");
  }
 
  #ifdef CGLUCOSE_EXP
  jhead= 0;
  jftr = 0;
  travId = 0;
  travId_prev = 0;
 
  // allocate space for clause interpretation 
  vec<Lit> tmp; tmp.growTo(3); 
  itpc = ca.alloc(tmp);
  ca[itpc].shrink( ca[itpc].size() );
 
  nSkipMark = 0;
  #endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

~Solver()

Solver::~Solver ( )

virtual

Definition at line 194 of file Glucose2.cpp.

{
}

Member Function Documentation

abstractLevel()

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

inlineprotected

Definition at line 561 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

addClause() [1/4]

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

inline

Definition at line 532 of file Solver.h.

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

Here is the call graph for this function:

addClause() [2/4]

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

inline

Definition at line 534 of file Solver.h.

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

Here is the call graph for this function:

addClause() [3/4]

bool Gluco2::Solver::addClause ( Lit p, Lit q )

inline

Definition at line 535 of file Solver.h.

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

inline

Definition at line 536 of file Solver.h.

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

Here is the call graph for this function:

addClause_()

bool Solver::addClause_

(

vec< Lit > &

ps

)

Definition at line 268 of file Glucose2.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 Gluco2::Solver::addEmptyClause ( )

inline

Definition at line 533 of file Solver.h.

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

Here is the call graph for this function:

addJwatch()

void Gluco2::Solver::addJwatch ( Var host, Var member, int index )

inlineprotected

Definition at line 159 of file CGlucoseCore.h.

                                                              {
    assert(level(host) >= level(member));
    jnext[index] = jlevel[level(host)];
    jlevel[level(host)] = index;
}

Here is the call graph for this function:

Here is the caller graph for this function:

addVar()

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

inline

Definition at line 607 of file Solver.h.

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

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 604 of file Glucose2.cpp.

{
    //double clk = Abc_Clock();
    heap_rescale = 0;
 
    int pathC = 0;
    Lit p     = lit_Undef;
 
    // Generate conflict clause:
    //
    out_learnt.push();      // (leave room for the asserting literal)
    int index   = trail.size() - 1;
    
    analyze_toclear.shrink_( analyze_toclear.size() );
    do{
        assert(confl != CRef_Undef); // (otherwise should be UIP)
 
        #ifdef CGLUCOSE_EXP
        Clause& c = ca[ lit_Undef != p ? castCRef(p): getConfClause(confl) ];
        #else
        Clause& c = ca[confl];
        #endif
 
        // 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];
            bool fBump = 0;
 
            if (!seen[var(q)] && level(var(q)) > 0){
                if(!isSelector(var(q))){
                    fBump = 1;
                    varBumpActivity(var(q));
                }
                seen[var(q)] = 1;
                if (level(var(q)) >= decisionLevel()) {
                    if( fBump )
                        analyze_toclear.push(q);
                    pathC++;
                    #ifdef UPDATEVARACTIVITY
                    // UPDATEVARACTIVITY trick (see competition'09 companion paper)
                    #ifdef CGLUCOSE_EXP
                    if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)  
                    && ! isGateCRef(reason(var(q))) && ca[reason(var(q))].learnt())
                        lastDecisionLevel.push(q);
                    #else
                    if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)  && ca[reason(var(q))].learnt()) 
                        lastDecisionLevel.push(q);
                    #endif
                    #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]);       
 
 
    #ifdef CGLUCOSE_EXP
    for(i = 0;i<out_learnt.size();i++)  
        analyze_toclear.push(out_learnt[i]);
    #else
    out_learnt.copyTo_(analyze_toclear);
    #endif
    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{
                #ifdef CGLUCOSE_EXP
                Clause& c = ca[castCRef(out_learnt[i])];
                #else
                Clause& c = ca[reason(var(out_learnt[i]))];
                #endif
                // 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++) {
            Lit t = lastDecisionLevel[i];
            //assert( ca[reason(var(t))].learnt() );
            if(ca[reason(var(t))].lbd()<lbd)
                varBumpActivity(var(t));
        }
        lastDecisionLevel.shrink_( lastDecisionLevel.size() );
    } 
#endif
 
 
    if( justUsage() ){
        if( heap_rescale )
        {
            for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;
 
            analyze_toclear.shrink_( analyze_toclear.size() );
            for (j = 0; j < jheap.size(); j++){
                Var x = jheap[j];
                if( var2NodeData[x].now )
                    analyze_toclear.push(mkLit(x));
            }
            for (j = 0; j < analyze_toclear.size(); j++){
                Var x = var(analyze_toclear[j]);
//                jdata[x].act_fanin = activity[getFaninVar0(x)] > activity[getFaninVar1(x)]? activity[getFaninVar0(x)]: activity[getFaninVar1(x)];
//                jheap.update(x);
                if( activity[getFaninVar1(x)] > activity[getFaninVar0(x)] )
                    jheap.update( JustKey( activity[getFaninVar1(x)], x, jheap.data_attr(x) ) );
                else
                    jheap.update( JustKey( activity[getFaninVar0(x)], x, jheap.data_attr(x) ) );
            }
 
        } else {
 
            for (j = 0; j < analyze_toclear.size(); j++)
            {
                seen[var(analyze_toclear[j])] = 0;
                updateJustActivity(var(analyze_toclear[j]));
            }
        }
    } else
        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 888 of file Glucose2.cpp.

{
    out_conflict.shrink_( out_conflict.size() );
    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{
              #ifdef CGLUCOSE_EXP
                Clause& c = ca[castCRef(trail[i])];
              #else
                Clause& c = ca[reason(x)];
              #endif
                //                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 333 of file Glucose2.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 Gluco2::Solver::budgetOff ( )

inline

Definition at line 585 of file Solver.h.

{ conflict_budget = propagation_budget = -1; }

Here is the caller graph for this function:

cancelUntil()

void Solver::cancelUntil ( int level )

protected

Definition at line 515 of file Glucose2.cpp.

                                  {
    if (decisionLevel() > level){
 
        #ifdef CGLUCOSE_EXP
        if( 0 < justUsage() ){
 
            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]);
                //gateClearJwatch(x, level);
 
                var2NodeData[x].now = false;
            }
            for (int l = decisionLevel(); l > level; l -- ){
                int q = jlevel[l], k;
                jlevel[l] = -1;
                while( -1 != q ){
                    k = jnext[q];
                    jnext[q] = -1;
                    Var v = var(trail[q]);
                    if( Solver::level(v) <= level ){
                        pushJustQueue(v,q);
                    }
                    q = k;
                }
            }
        } else 
        #endif
            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);
            }
 
        jhead = 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:

castCRef()

CRef Gluco2::Solver::castCRef ( Lit p )

inlineprotected

Definition at line 541 of file CGlucoseCore.h.

                                   {
    CRef cr = reason( var(p) );
    if( CRef_Undef == cr )
        return cr;
    if( ! isGateCRef(cr) )
        return cr;
    Var v = CRef2Var(cr);
    return interpret(v,var(p));
}

Here is the call graph for this function:

Here is the caller graph for this function:

checkGarbage() [1/2]

void Gluco2::Solver::checkGarbage ( void )

inline

Definition at line 525 of file Solver.h.

{ checkGarbage(garbage_frac); }

Here is the call graph for this function:

Here is the caller graph for this function:

checkGarbage() [2/2]

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

inline

Definition at line 526 of file Solver.h.

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

Here is the call graph for this function:

claBumpActivity()

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

inlineprotected

Definition at line 518 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 Gluco2::Solver::claDecayActivity ( )

inlineprotected

Definition at line 517 of file Solver.h.

{ cla_inc *= (1 / clause_decay); }

Here is the caller graph for this function:

clearInterrupt()

void Gluco2::Solver::clearInterrupt ( )

inline

Definition at line 584 of file Solver.h.

{ asynch_interrupt = false; }

computeLBD() [1/2]

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

inlineprotected

Definition at line 441 of file Glucose2.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 411 of file Glucose2.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:

CRef2Var()

Var Gluco2::Solver::CRef2Var ( CRef cr ) const

inlineprotected

Definition at line 422 of file Solver.h.

{ return cr & ~(1<<(sizeof(CRef)*8-1)); }

Here is the caller graph for this function:

decisionLevel()

int Gluco2::Solver::decisionLevel ( ) const

inlineprotected

Definition at line 560 of file Solver.h.

{ 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 350 of file Glucose2.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 Gluco2::Solver::drand ( double & seed )

inlinestaticprotected

Definition at line 358 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 Gluco2::Solver::enqueue ( Lit p, CRef from = CRef_Undef )

inlineprotected

Definition at line 531 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

garbageCollect()

void Solver::garbageCollect ( )

virtual

Reimplemented in Gluco2::SimpSolver.

Definition at line 1648 of file Glucose2.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:

gateAddJwatch()

void Gluco2::Solver::gateAddJwatch ( Var v, int index )

inlineprotected

Definition at line 118 of file CGlucoseCore.h.

                                                {
    assert(v < nVars());
    assert(isJReason(v));
 
    lbool val0, val1;
    Var var0, var1;
    var0 = getFaninVar0(v);
    var1 = getFaninVar1(v);
    val0 = value(getFaninLit0(v));
    val1 = value(getFaninLit1(v));
 
    assert( !isAND(v) ||  l_False == val0 || l_False == val1  );
    assert(  isAND(v) || (l_Undef != val0 && l_Undef != val1) );
 
    if( (val0 == l_False && val1 == l_False) || !isAND(v) ){
        addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v, index);
        return;
    }
 
    addJwatch(l_False == val0? var0: var1, v, index);
 
    return;
}

Here is the call graph for this function:

Here is the caller graph for this function:

gateClearJwatch()

void Gluco2::Solver::gateClearJwatch ( Var v, int backtrack_level )

protected

gateJustFanin()

Lit Gluco2::Solver::gateJustFanin ( Var v ) const

inlineprotected

Definition at line 18 of file CGlucoseCore.h.

                                             {
    assert(v < nVars());
    assert(isJReason(v));
 
 
    lbool val0, val1;
    val0 = value(getFaninLit0(v));
    val1 = value(getFaninLit1(v));
 
    if(isAND(v)){
        // should be handled by conflict analysis before entering here
        assert( value(v) != l_False || l_True  != val0 || l_True  != val1 );
 
        if(val0 == l_False || val1 == l_False)
            return lit_Undef;
 
        // branch 
        if(val0 == l_True)
            return ~getFaninLit1(v);
        if(val1 == l_True)
            return ~getFaninLit0(v);
 
        //assert( jdata[v].act_fanin == activity[getFaninVar0(v)] || jdata[v].act_fanin == activity[getFaninVar1(v)] );
        //assert( jdata[v].act_fanin == (jdata[v].adir? activity[getFaninVar1(v)]: activity[getFaninVar0(v)]) );
        return maxActiveLit( ~getFaninLit0(v), ~getFaninLit1(v) );
        //return jdata[v].adir? ~getFaninLit1(v): ~getFaninLit0(v);
    } else { // xor scope
        // should be handled by conflict analysis before entering here
        assert( value(v) == l_Undef || value(v) != l_False || val0 == val1 );
 
        // both are assigned
        if( l_Undef != val0 && l_Undef != val1 )
            return lit_Undef;
 
        // should be handled by propagation before entering here
        assert( l_Undef == val0 && l_Undef == val1 );
        return maxActiveLit( getFaninPlt0(v), getFaninPlt1(v) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

gatePropagate()

CRef Gluco2::Solver::gatePropagate ( Lit p )

inlineprotected

Definition at line 279 of file CGlucoseCore.h.

                                        {
    CRef confl = CRef_Undef, stats;
    if( justUsage() < 2 )
        return CRef_Undef;
 
    if( ! isRoundWatch(var(p)) )
        return CRef_Undef;
 
    if( ! isTwoFanin( var(p) ) )
        goto check_fanout;
 
 
    // check fanin consistency 
    if( CRef_Undef != (stats = gatePropagateCheckThis( var(p) )) ){
        confl = stats;
        if( l_True == value(var(p)) )
            return confl;
    }
 
    // check fanout consistency
check_fanout:
    assert( var(p) < var2Fanout0.size() );
 
    if( ! var2NodeData[var(p)].sort )
        inplace_sort(var(p));
 
    int nFanout = 0;
    for( Lit lfo = var2Fanout0[ var(p) ]; nFanout < var2NodeData[var(p)].sort; lfo = var2FanoutN[ toInt(lfo) ], nFanout ++ )
    {
        if( CRef_Undef != (stats = gatePropagateCheckFanout( var(p), lfo )) ){
            confl = stats;
            if( l_True == value(var(lfo)) )
                return confl;
        }
    }
 
    return confl;
}

Here is the call graph for this function:

Here is the caller graph for this function:

gatePropagateCheck()

CRef Gluco2::Solver::gatePropagateCheck ( Var v, Var t )

protected

gatePropagateCheckFanout()

CRef Gluco2::Solver::gatePropagateCheckFanout ( Var v, Lit lfo )

inlineprotected

Definition at line 318 of file CGlucoseCore.h.

                                                            {
    Lit faninLit = sign(lfo)? getFaninLit1(var(lfo)): getFaninLit0(var(lfo));
    assert( var(faninLit) == v );
    if( isAND(var(lfo)) ){
        if( l_False == value(faninLit) )
        {
            if( l_False == value(var(lfo)) )
                return CRef_Undef;
 
            if( l_True == value(var(lfo)) )
                return Var2CRef(var(lfo));
            
            var2NodeData[var(lfo)].dir = sign(lfo);
            uncheckedEnqueue2(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
        } else {
            assert( l_True == value(faninLit) );
 
            if( l_True == value(var(lfo)) )
                return CRef_Undef;
            
            // check value of the other fanin 
            Lit faninLitP = sign(lfo)? getFaninLit0(var(lfo)): getFaninLit1(var(lfo));
            if( l_False == value(var(lfo)) ){
                
                if( l_False == value(faninLitP) )
                    return CRef_Undef;
 
                if( l_True == value(faninLitP) )
                    return Var2CRef(var(lfo));
 
                uncheckedEnqueue2( ~faninLitP, Var2CRef( var(lfo) ) );
            }
            else
            if( l_True == value(faninLitP) )
                uncheckedEnqueue2( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
        }
    } else { // xor scope
        // check value of the other fanin 
        Lit faninLitP = sign(lfo)? getFaninLit0(var(lfo)): getFaninLit1(var(lfo));
 
        lbool val0, val1, valo;
        val0 = value(faninLit );
        val1 = value(faninLitP);
        valo = value(var(lfo));
 
        if( l_Undef == val1 && l_Undef == valo )
            return CRef_Undef;
        else
        if( l_Undef == val1 )
            uncheckedEnqueue2( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
        else
        if( l_Undef == valo )
            uncheckedEnqueue2( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
        else
        if( l_False  == (valo ^ (val0 == val1)) )
            return Var2CRef(var(lfo));
 
    }
    
    return CRef_Undef;
}

Here is the call graph for this function:

Here is the caller graph for this function:

gatePropagateCheckThis()

CRef Gluco2::Solver::gatePropagateCheckThis ( Var v )

inlineprotected

Definition at line 380 of file CGlucoseCore.h.

                                                 {
    CRef confl = CRef_Undef;
    if( isAND(v) ){
        if( l_False == value(v) ){
            if( l_True == value(getFaninLit0(v)) && l_True == value(getFaninLit1(v)) )
                return Var2CRef(v);
 
            if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
                return CRef_Undef;
 
            if( l_True == value(getFaninLit0(v)) )
                uncheckedEnqueue2(~getFaninLit1( v ), Var2CRef( v ) );
            if( l_True == value(getFaninLit1(v)) )
                uncheckedEnqueue2(~getFaninLit0( v ), Var2CRef( v ) );
        } else {
            assert( l_True == value(v) );
            if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
                confl = Var2CRef(v);
 
            if( l_Undef == value( getFaninLit0( v )) )
                uncheckedEnqueue2( getFaninLit0( v ), Var2CRef( v ) );
 
            if( l_Undef == value( getFaninLit1( v )) )
                uncheckedEnqueue2( getFaninLit1( v ), Var2CRef( v ) );
 
        }
    } else { // xor scope
        lbool val0, val1, valo;
        val0 = value(getFaninLit0(v));
        val1 = value(getFaninLit1(v));
        valo = value(v);
        if( l_Undef == val0 && l_Undef == val1 )
            return CRef_Undef;
        if( l_Undef == val0 )
            uncheckedEnqueue2(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
        else
        if( l_Undef == val1 )
            uncheckedEnqueue2(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
        else
        if( l_False == (valo ^ (val0 == val1)) )
            return Var2CRef(v);
    }
 
    return confl;
}

Here is the call graph for this function:

Here is the caller graph for this function:

getCex()

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

inline

Definition at line 571 of file Solver.h.

{ return (int*) &JustModel[0]; }

getConfClause()

CRef Gluco2::Solver::getConfClause ( CRef r )

inlineprotected

Definition at line 426 of file CGlucoseCore.h.

                                         {
    if( !isGateCRef(r) )
        return r;
    Var v = CRef2Var(r);
    assert( isTwoFanin(v) );
 
    if(isAND(v)){
        if( l_False == value(v) ){
            setItpcSize(3);
            Clause& c = ca[itpc];
            c[0] = mkLit(v);
            c[1] = ~getFaninLit0( v );
            c[2] = ~getFaninLit1( v );
        } else {
            setItpcSize(2);
            Clause& c = ca[itpc];
            c[0] = ~mkLit(v);
 
            lbool val0 = value(getFaninLit0(v));
            lbool val1 = value(getFaninLit1(v));
 
            if( l_False == val0 && l_False == val1 )
                c[1] = level(getFaninVar0(v)) < level(getFaninVar1(v))? getFaninLit0( v ): getFaninLit1( v );
            else
            if( l_False == val0 )
                c[1] = getFaninLit0( v );
            else
                c[1] = getFaninLit1( v );
        }
    } else { // xor scope
        setItpcSize(3);
        Clause& c = ca[itpc];
        c[0] = mkLit(v, l_True == value(v));
        c[1] = mkLit(getFaninVar0(v), l_True == value(getFaninVar0(v)));
        c[2] = mkLit(getFaninVar1(v), l_True == value(getFaninVar1(v)));
    }
    
 
    return itpc;
}

Here is the call graph for this function:

Here is the caller graph for this function:

getFaninC0()

bool Gluco2::Solver::getFaninC0 ( Var v ) const

inlineprotected

Definition at line 391 of file Solver.h.

{ return sign(getFaninLit0(v)); }

Here is the call graph for this function:

Here is the caller graph for this function:

getFaninC1()

bool Gluco2::Solver::getFaninC1 ( Var v ) const

inlineprotected

Definition at line 392 of file Solver.h.

{ return sign(getFaninLit1(v)); }

Here is the call graph for this function:

Here is the caller graph for this function:

getFaninLit0()

Lit Gluco2::Solver::getFaninLit0 ( Var v ) const

inlineprotected

Definition at line 389 of file Solver.h.

{ return var2NodeData[ v ].lit0; }

Here is the caller graph for this function:

getFaninLit1()

Lit Gluco2::Solver::getFaninLit1 ( Var v ) const

inlineprotected

Definition at line 390 of file Solver.h.

{ return var2NodeData[ v ].lit1; }

Here is the caller graph for this function:

getFaninPlt0()

Lit Gluco2::Solver::getFaninPlt0 ( Var v ) const

inlineprotected

Definition at line 395 of file Solver.h.

{ return mkLit(getFaninVar0(v), 1 == polarity[getFaninVar0(v)]); }

Here is the call graph for this function:

Here is the caller graph for this function:

getFaninPlt1()

Lit Gluco2::Solver::getFaninPlt1 ( Var v ) const

inlineprotected

Definition at line 396 of file Solver.h.

{ return mkLit(getFaninVar1(v), 1 == polarity[getFaninVar1(v)]); }

Here is the call graph for this function:

Here is the caller graph for this function:

getFaninVar0()

Var Gluco2::Solver::getFaninVar0 ( Var v ) const

inlineprotected

Definition at line 393 of file Solver.h.

{ return  var(getFaninLit0(v)); }

Here is the call graph for this function:

Here is the caller graph for this function:

getFaninVar1()

Var Gluco2::Solver::getFaninVar1 ( Var v ) const

inlineprotected

Definition at line 394 of file Solver.h.

{ return  var(getFaninLit1(v)); }

Here is the call graph for this function:

Here is the caller graph for this function:

initNbInitialVars()

void Solver::initNbInitialVars

(

int

nb

)

Definition at line 211 of file Glucose2.cpp.

                                     {
  nbVarsInitialFormula = nb;
}

inplace_sort()

void Gluco2::Solver::inplace_sort ( Var v )

inlineprotected

Definition at line 565 of file CGlucoseCore.h.

                                       {
    Lit w, next, prev;
    prev= var2Fanout0[v];
 
    if( toLit(~0) == prev ) return;
 
    if( isRoundWatch(var(prev)) )
        var2NodeData[v].sort ++ ;
 
    if( toLit(~0) == (w = var2FanoutN[toInt(prev)]) )
        return;
 
    while( toLit(~0) != w ){
        next = var2FanoutN[toInt(w)];
        if( isRoundWatch(var(w)) )
            var2NodeData[v].sort ++ ;
        if( isRoundWatch(var(w)) && !isRoundWatch(var(prev)) ){
            var2FanoutN[toInt(w)] = var2Fanout0[v];
            var2Fanout0[v] = w;
            var2FanoutN[toInt(prev)] = next;
        } else 
            prev = w;
        w = next;
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

insertVarOrder()

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

inlineprotected

Definition at line 494 of file Solver.h.

                                        {
    #ifdef CGLUCOSE_EXP
    if (!justUsage() && !order_heap.inHeap(x) && decision[x]) order_heap.insert(x); 
    #else
    if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); 
    #endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

interpret()

CRef Gluco2::Solver::interpret ( Var v, Var t )

inlineprotected

Definition at line 473 of file CGlucoseCore.h.

{ // get gate-clause on implication graph
    assert( isTwoFanin(v) );
 
    lbool val0, val1, valo;
    Var var0, var1;
    var0 = getFaninVar0( v );
    var1 = getFaninVar1( v );
    val0 = value(var0);
    val1 = value(var1);
    valo = value( v );
 
    // phased values
    if(l_Undef != val0) val0 = val0 ^ getFaninC0( v );
    if(l_Undef != val1) val1 = val1 ^ getFaninC1( v );
 
 
    if( isAND(v) ){
        if( v == t ){ // tracing output 
            if( l_False == valo ){
                setItpcSize(2);
                Clause& c = ca[itpc];
                c[0] = ~mkLit(v);
 
                c[1] = var2NodeData[v].dir ? getFaninLit1( v ): getFaninLit0( v );
            } else {
                setItpcSize(3);
                Clause& c = ca[itpc];
                c[0] = mkLit(v);
                c[1] = ~getFaninLit0( v );
                c[2] = ~getFaninLit1( v );
            }
        } else {
            assert( t == var0 || t == var1 );
            if( l_False == valo ){
                setItpcSize(3);
                Clause& c = ca[itpc];
                c[0] = ~getFaninLit0( v );
                c[1] = ~getFaninLit1( v );
                c[2] = mkLit(v);
                if( t == var1 )
                    c[1].x ^= c[0].x, c[0].x ^= c[1].x, c[1].x ^= c[0].x;
            } else {
                setItpcSize(2);
                Clause& c = ca[itpc];
                c[0] =  t == var0? getFaninLit0( v ): getFaninLit1( v );
                c[1] = ~mkLit(v);
            }
        }
    } else { // xor scope
        setItpcSize(3);
        Clause& c = ca[itpc];
        if( v == t ){
            c[0] = mkLit(v, l_False == value(v));
            c[1] = mkLit(var0, l_True == value(var0));
            c[2] = mkLit(var1, l_True == value(var1));
        } else {
            if( t == var0)
                c[0] = mkLit(var0, l_False == value(var0)), c[1] = mkLit(var1, l_True  == value(var1));
            else
                c[1] = mkLit(var0, l_True  == value(var0)), c[0] = mkLit(var1, l_False == value(var1));
            c[2] = mkLit(v, l_True == value(v));
        }
    }
 
    return itpc;
}

Here is the call graph for this function:

Here is the caller graph for this function:

interrupt()

void Gluco2::Solver::interrupt ( )

inline

Definition at line 583 of file Solver.h.

{ asynch_interrupt = true; }

irand()

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

inlinestaticprotected

Definition at line 365 of file Solver.h.

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

Here is the call graph for this function:

Here is the caller graph for this function:

isAND()

bool Gluco2::Solver::isAND ( Var v ) const

inlineprotected

Definition at line 387 of file Solver.h.

{ return getFaninVar0(v) < getFaninVar1(v); }

Here is the call graph for this function:

Here is the caller graph for this function:

isGateCRef()

bool Gluco2::Solver::isGateCRef ( CRef cr ) const

inlineprotected

Definition at line 423 of file Solver.h.

{ return CRef_Undef != cr && 0 != (cr & (1<<(sizeof(CRef)*8-1))); }

Here is the caller graph for this function:

isJReason()

bool Gluco2::Solver::isJReason ( Var v ) const

inlineprotected

Definition at line 388 of file Solver.h.

{ return isTwoFanin(v) && ( l_False == value(v) || (!isAND(v) && l_Undef != value(v)) ); }

Here is the call graph for this function:

Here is the caller graph for this function:

isRoundWatch()

bool Gluco2::Solver::isRoundWatch ( Var v ) const

inline

Definition at line 473 of file Solver.h.

{ return travId==var2TravId[v]; }

Here is the caller graph for this function:

isSelector()

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

inlineprotected

Definition at line 352 of file Solver.h.

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

Here is the caller graph for this function:

isTwoFanin()

bool Gluco2::Solver::isTwoFanin ( Var v ) const

inlineprotected

Definition at line 268 of file CGlucoseCore.h.

                                            {
    Lit lit0 = var2NodeData[ v ].lit0;
    Lit lit1 = var2NodeData[ v ].lit1;
    assert( toLit(~0) == lit0 || var(lit0) < nVars() );
    assert( toLit(~0) == lit1 || var(lit1) < nVars() );
    lit0.x = lit1.x = 0; // suppress the warning - alanmi
    return toLit(~0) != var2NodeData[ v ].lit0 && toLit(~0) != var2NodeData[ v ].lit1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

justCheck()

void Gluco2::Solver::justCheck ( )

inlineprotected

Definition at line 169 of file CGlucoseCore.h.

                             {
    Lit lit;
    int i, nJustFail = 0;
    for(i=0; i<trail.size(); i++){
        Var      x  = var(trail[i]);
        if( ! isRoundWatch(x) )
            continue;
        if( !isJReason(x) )
            continue;
        if( lit_Undef != (lit = gateJustFanin(x)) ){
            printf("\t%8d is not justified (value=%d, level=%3d)\n", x, l_True == value(x)? 1: 0, vardata[x].level), nJustFail ++ ;
 
            assert(false);
        }
    }
    if( nJustFail )
        printf("%d just-fails\n", nJustFail);
}

Here is the call graph for this function:

justReset()

void Gluco2::Solver::justReset ( )

inline

Definition at line 474 of file Solver.h.

{ jftr = 0; reset(); }

Here is the call graph for this function:

Here is the caller graph for this function:

justUsage()

int Gluco2::Solver::justUsage ( ) const

inline

Definition at line 16 of file CGlucoseCore.h.

{ return jftr; }

Here is the caller graph for this function:

level()

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

inline

Definition at line 492 of file Solver.h.

{ return vardata[x].level; }

Here is the caller graph for this function:

litRedundant()

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

protected

Definition at line 841 of file Glucose2.cpp.

{
    analyze_stack.shrink_( analyze_stack.size() ); analyze_stack.push(p);
    int top = analyze_toclear.size();
    while (analyze_stack.size() > 0){
        assert(reason(var(analyze_stack.last())) != CRef_Undef);
        #ifdef CGLUCOSE_EXP
        Clause& c = ca[castCRef(analyze_stack.last())]; analyze_stack.pop();
        #else
        Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
        #endif
        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:

loadJust()

void Gluco2::Solver::loadJust ( )

inlineprotected

Definition at line 681 of file CGlucoseCore.h.

                            {
    int i;
    travId ++ ;
    JustModel.shrink_(JustModel.size());
    vMarked.shrink_(vMarked.size());
    JustModel.push(toLit(0));
    for(i = 0; i < assumptions.size(); i ++)
        loadJust_rec( var(assumptions[i]) );
    JustModel[0] = toLit( JustModel.size()-1 );
    travId -- ;
    for(i = 0; i < vMarked.size(); i ++)
        var2TravId[ vMarked[i] ] = travId;
}

Here is the call graph for this function:

Here is the caller graph for this function:

loadJust_rec()

void Gluco2::Solver::loadJust_rec ( Var v )

inlineprotected

Definition at line 666 of file CGlucoseCore.h.

                                       {
    //assert( value(v) != l_Undef );
    if( var2TravId[v] == travId || value(v) == l_Undef )
        return;
    assert( var2TravId[v] == travId-1 );
    var2TravId[v] = travId;
    vMarked.push(v);
 
    if( !isTwoFanin(v) ){
        JustModel.push( mkLit( v, value(v) == l_False ) );
        return;
    }
    loadJust_rec( getFaninVar0(v) );
    loadJust_rec( getFaninVar1(v) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

locked()

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

inlineprotected

Definition at line 537 of file Solver.h.

                                                              { 
   #ifdef CGLUCOSE_EXP
 
    if(c.size()>2) 
     return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && !isGateCRef(reason(var(c[0]))) && ca.lea(reason(var(c[0]))) == &c; 
   return 
     (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && !isGateCRef(reason(var(c[0]))) && ca.lea(reason(var(c[0]))) == &c)
     || 
     (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && !isGateCRef(reason(var(c[1]))) && ca.lea(reason(var(c[1]))) == &c);
 
   #else
   
   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);
 
   #endif
 }

Here is the call graph for this function:

Here is the caller graph for this function:

markApprox()

void Gluco2::Solver::markApprox ( Var v0, Var v1, int nlim )

inline

Definition at line 634 of file CGlucoseCore.h.

                                                        {
    int i;
    if( travId <= 1 || nSkipMark>=4 || 0 == nlim )
        goto finalize;
 
    vMarked.shrink_( vMarked.size() );
    travId ++ ; // travId = t+1
    assert(travId>1);
 
    markTill(v0, nlim);
    if( vMarked.size() >= nlim )
        goto finalize;
 
    markTill(v1, nlim);
    if( vMarked.size() >= nlim )
        goto finalize;
 
    travId -- ; // travId = t
    for(i = 0; i < vMarked.size(); i ++){
        var2TravId  [ vMarked[i] ]      = travId;   // set new nodes to time t 
        var2NodeData[ vMarked[i] ].sort = 0;
    }
    nSkipMark ++ ;
    return;
finalize:
 
    travId ++ ;
    nSkipMark = 0;
    markCone(v0);
    markCone(v1);
}

Here is the call graph for this function:

markCone()

void Gluco2::Solver::markCone ( Var v )

inline

Definition at line 551 of file CGlucoseCore.h.

                                   {
    if( var2TravId[v] >= travId )
        return;
    var2TravId[v] = travId;
    var2NodeData[v].sort = 0;
    Var var0, var1;
    var0 = getFaninVar0(v);
    var1 = getFaninVar1(v);
    if( !isTwoFanin(v) )
        return;
    markCone( var0 );
    markCone( var1 );
}

Here is the call graph for this function:

Here is the caller graph for this function:

markTill()

void Gluco2::Solver::markTill ( Var v0, int nlim )

inline

Definition at line 617 of file CGlucoseCore.h.

                                             {
    if( var2TravId[v] == travId )
        return;
 
    vMarked.push(v);
    
    if( vMarked.size() >= nlim )
        return;
    if( var2TravId[v] == travId-1 || !isTwoFanin(v) )
        goto finalize;
 
    markTill( getFaninVar0(v), nlim );
    markTill( getFaninVar1(v), nlim );
finalize:
    var2TravId[v] = travId;
}

Here is the call graph for this function:

Here is the caller graph for this function:

maxActiveLit()

Lit Gluco2::Solver::maxActiveLit ( Lit lit0, Lit lit1 ) const

inlineprotected

Definition at line 397 of file Solver.h.

{ return activity[var(lit0)] < activity[var(lit1)]? lit1: lit0; }

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 473 of file Glucose2.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:

mkNodeData()

static NodeData Gluco2::Solver::mkNodeData ( )

inlinestaticprotected

Definition at line 378 of file Solver.h.

{ NodeData w; w.lit0 = toLit(~0); w.lit1 = toLit(~0); w.sort = 0; w.dir = 0; w.now = 0; return w; }

Here is the call graph for this function:

Here is the caller graph for this function:

mkVarData()

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

inlinestaticprotected

Definition at line 208 of file Solver.h.

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

Here is the caller graph for this function:

modelValue() [1/2]

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

inline

Definition at line 565 of file Solver.h.

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

Here is the call graph for this function:

modelValue() [2/2]

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

inline

Definition at line 564 of file Solver.h.

{ return model[x]; }

Here is the caller graph for this function:

nAssigns()

int Gluco2::Solver::nAssigns ( ) const

inline

Definition at line 566 of file Solver.h.

{ return trail.size(); }

Here is the caller graph for this function:

nClauses()

int Gluco2::Solver::nClauses ( ) const

inline

Definition at line 567 of file Solver.h.

{ return clauses.size(); }

Here is the caller graph for this function:

newDecisionLevel()

void Gluco2::Solver::newDecisionLevel ( )

inlineprotected

Definition at line 558 of file Solver.h.

{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 223 of file Glucose2.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);
    
 
    #ifdef CGLUCOSE_EXP
    //jreason  .capacity(v+1);
    if( justUsage() ){
        //jdata    .push(mkJustData(false));
        //jwatch   .push(mkJustWatch());
 
        jlevel   .push(-1);
        jnext    .push(-1);
 
        var2FanoutN.growTo( nVars()<<1, toLit(~0));
        //var2FanoutP.growTo( nVars()<<1, toLit(~0));
        var2Fanout0.growTo( nVars(), toLit(~0));
        var2NodeData.growTo( nVars(), mkNodeData());
        var2TravId .growTo( nVars(), 0);
 
        setDecisionVar(v, dvar, false);
    } else 
        setDecisionVar(v, dvar);
    #else
    setDecisionVar(v, dvar);
    #endif
 
    return v;
}

Here is the call graph for this function:

Here is the caller graph for this function:

nFreeVars()

int Gluco2::Solver::nFreeVars ( ) const

inline

Definition at line 570 of file Solver.h.

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

nLearnts()

int Gluco2::Solver::nLearnts ( ) const

inline

Definition at line 568 of file Solver.h.

{ return learnts.size(); }

Here is the caller graph for this function:

nVars()

int Gluco2::Solver::nVars ( ) const

inline

Definition at line 569 of file Solver.h.

{ return vardata.size(); }

Here is the caller graph for this function:

okay()

bool Gluco2::Solver::okay ( ) const

inline

Definition at line 600 of file Solver.h.

{ return ok; }

pickBranchLit()

Lit Solver::pickBranchLit ( )

protected

Definition at line 565 of file Glucose2.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:

pickJustLit()

Lit Gluco2::Solver::pickJustLit ( int & index )

inlineprotected

Definition at line 90 of file CGlucoseCore.h.

                                          {
    Var next = var_Undef;
    Lit jlit = lit_Undef;
 
    for( ; jhead < trail.size() ; jhead++ ){
        Var x = var(trail[jhead]);
        if( !decisionLevel() && !isRoundWatch(x) ) continue;
        if( isJReason(x) && l_Undef == value( getFaninVar0(x) ) && l_Undef == value( getFaninVar1(x) ) )
            pushJustQueue(x,jhead);
    }
 
    while( ! jheap.empty() ){
        next = jheap.removeMin(index);
        if( ! var2NodeData[next].now )
            continue; 
 
        assert(isJReason(next));
        if( lit_Undef != (jlit = gateJustFanin(next)) ){
            //assert( jheap.prev.key() == activity[getFaninVar0(next)] || jheap.prev.key() == activity[getFaninVar1(next)] );
            break;
        }
        gateAddJwatch(next,index);
    }
 
    return jlit;
}

Here is the call graph for this function:

Here is the caller graph for this function:

prelocate()

void Gluco2::Solver::prelocate ( int var_num )

inline

Definition at line 591 of file CGlucoseCore.h.

                                               {
    if( justUsage() ){
        var2FanoutN .prelocate( base_var_num << 1 );
        var2Fanout0 .prelocate( base_var_num );
        var2NodeData.prelocate( base_var_num );
        var2TravId  .prelocate( base_var_num );
        jheap       .prelocate( base_var_num );
        jlevel      .prelocate( base_var_num );
        jnext       .prelocate( base_var_num );
    }
    watches    .prelocate( base_var_num << 1 );
    watchesBin .prelocate( base_var_num << 1 );
 
    decision   .prelocate( base_var_num );
    trail      .prelocate( base_var_num );
    assigns    .prelocate( base_var_num );
    vardata    .prelocate( base_var_num );
    activity   .prelocate( base_var_num );
 
 
    seen       .prelocate( base_var_num );
    permDiff   .prelocate( base_var_num );
    polarity   .prelocate( base_var_num );
}

Here is the call graph for this function:

Here is the caller graph for this function:

printClause()

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

inline

Definition at line 632 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 1368 of file Glucose2.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 Gluco2::Solver::printInitialClause ( CRef c )

inline

Definition at line 641 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 Gluco2::Solver::printLit ( Lit l )

inline

Definition at line 626 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 1354 of file Glucose2.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 947 of file Glucose2.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++;
 
        #ifdef CGLUCOSE_EXP
        if( 2 <= justUsage() ){
            CRef stats;
            if( CRef_Undef != (stats = gatePropagate(p)) ){
                confl = stats;
                if( l_True == value(var(p)) ) return confl;
            }
        }
        #endif
 
        // 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:

pushJustQueue()

void Gluco2::Solver::pushJustQueue ( Var v, int index )

inlineprotected

Definition at line 60 of file CGlucoseCore.h.

                                                 {
    assert(v < nVars());
    assert(isJReason(v));
 
    if( ! isRoundWatch(v) )\
        return;
 
    var2NodeData[v].now = true;
 
 
    if( activity[getFaninVar1(v)] > activity[getFaninVar0(v)] )
        jheap.update( JustKey( activity[getFaninVar1(v)], v, index ) );
    else
        jheap.update( JustKey( activity[getFaninVar0(v)], v, index ) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

reason()

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

inlineprotected

Definition at line 491 of file Solver.h.

{ return vardata[x].reason; }

Here is the caller graph for this function:

rebuildOrderHeap()

void Solver::rebuildOrderHeap ( )

protected

Definition at line 1141 of file Glucose2.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 1095 of file Glucose2.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 1597 of file Glucose2.cpp.

{
    #ifdef CGLUCOSE_EXP
    if( CRef_Undef != itpc ){
      setItpcSize(3);
      ca.reloc(itpc, to);
    }
    #endif
    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]);
 
        #ifdef CGLUCOSE_EXP
        if( isGateCRef(reason(v)) )
          continue;
        #endif
        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 377 of file Glucose2.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 1127 of file Glucose2.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 Gluco2::SimpSolver.

Definition at line 1661 of file Glucose2.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   .shrink_(model   .size());
    conflict.shrink_(conflict.size());
    activity.shrink_(activity.size());
    assigns .shrink_(assigns .size());
    polarity.shrink_(polarity.size());
    //forceUNSAT.clear(false);
    decision   .shrink_(decision   .size());
    trail      .shrink_(trail      .size());
    trail_lim  .shrink_(trail_lim  .size());
    vardata    .shrink_(vardata    .size());
    assumptions.shrink_(assumptions.size());
    nbpos      .shrink_(nbpos      .size());
    permDiff   .shrink_(permDiff   .size());
    #ifdef UPDATEVARACTIVITY
    lastDecisionLevel.shrink_(lastDecisionLevel.size());
    #endif
    ca.clear();
    seen           .shrink_(seen.size());
    analyze_stack  .shrink_(analyze_stack  .size());
    analyze_toclear.shrink_(analyze_toclear.size());
    add_tmp.clear(false);
    assumptionPositions.clear(false);
    initialPositions.clear(false);
 
    #ifdef CGLUCOSE_EXP
 
    ResetJustData(false);
 
    //jwatch.shrink_(jwatch.size());
    //jdata .shrink_(jdata .size());
 
    jhead  = 0;
    travId = 0;
    travId_prev = 0;
    var2TravId   .shrink_(var2TravId.size());
    JustModel    .shrink_(JustModel .size());
    jlevel       .shrink_(jlevel.size());
    jnext        .shrink_(jnext.size());
 
    //var2FaninLits.shrink_(var2FaninLits.size());
    var2NodeData .shrink_(var2NodeData .size());
    var2Fanout0  .shrink_(var2Fanout0  .size());
    var2FanoutN  .shrink_(var2FanoutN  .size());
    //var2FanoutP.clear(false);
    if( CRef_Undef != itpc ){
        itpc = CRef_Undef;       // clause allocator has been cleared, do not worry 
        // allocate space for clause interpretation 
        vec<Lit> tmp; tmp.growTo(3); 
        itpc = ca.alloc(tmp);
        ca[itpc].shrink( ca[itpc].size() );
    }
 
    vMarked.shrink_( vMarked.size() );
    nSkipMark = 0;
    #endif
}

Here is the call graph for this function:

Here is the caller graph for this function:

ResetJustData()

void Gluco2::Solver::ResetJustData ( bool fCleanMemory )

inlineprotected

Definition at line 85 of file CGlucoseCore.h.

                                                  {
    jhead = 0;
    jheap .clear_( fCleanMemory );
}

Here is the caller graph for this function:

restoreJustQueue()

void Gluco2::Solver::restoreJustQueue ( int level )

protected

Here is the call graph for this function:

sat_solver_jftr()

int Gluco2::Solver::sat_solver_jftr ( )

inline

Definition at line 613 of file Solver.h.

{ return jftr; }

sat_solver_mark_cone()

void Gluco2::Solver::sat_solver_mark_cone ( int v )

inline

Definition at line 611 of file Solver.h.

{ markCone(v); }

Here is the call graph for this function:

sat_solver_reset()

void Gluco2::Solver::sat_solver_reset ( )

inline

Definition at line 614 of file Solver.h.

{ justReset();  }

Here is the call graph for this function:

sat_solver_set_jftr()

void Gluco2::Solver::sat_solver_set_jftr ( int njftr )

inline

Definition at line 612 of file Solver.h.

{ setJust(njftr); }

Here is the call graph for this function:

sat_solver_set_var_fanin_lit()

void Gluco2::Solver::sat_solver_set_var_fanin_lit ( int v, int lit0, int lit1 )

inline

Definition at line 609 of file Solver.h.

{ setVarFaninLits( Var(v), toLit(lit0), toLit(lit1) ); }

Here is the call graph for this function:

sat_solver_start_new_round()

void Gluco2::Solver::sat_solver_start_new_round ( )

inline

Definition at line 610 of file Solver.h.

{ setNewRound(); }

Here is the call graph for this function:

satisfied()

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

protected

Definition at line 396 of file Glucose2.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 1201 of file Glucose2.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();
 
        // exact conflict limit
        if ( !withinBudget() && confl != CRef_Undef ) {
          lbdQueue.fastclear();
          cancelUntil(0);
          return l_Undef; }
 
        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.shrink_( learnt_clause.size() );
            selectors    .shrink_( selectors.size() );
            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)
            {
                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;
                }
            }
 
            #ifdef CGLUCOSE_EXP
            // pick from JustQueue
 
            if (0 < justUsage())
            if ( next == lit_Undef ){
                int index = -1;
                decisions++;
                next = pickJustLit( index );
                if(next == lit_Undef)
                    return l_True;
                //addJwatch(var(next), j_reason);
                jnext[index] = jlevel[decisionLevel()+1];
                jlevel[decisionLevel()+1] = index;
            }
            #endif
 
            if (next == lit_Undef){
                // New variable decision:
                decisions++;
                next = pickBranchLit();
 
                if (next == lit_Undef){
                  // Model found:
                  return l_True;
                }
            }
 
            // Increase decision level and enqueue 'next'
            newDecisionLevel();
            uncheckedEnqueue(next);
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

setConfBudget()

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

inline

Definition at line 581 of file Solver.h.

{ conflict_budget    = conflicts    + x; }

setDecisionVar()

void Gluco2::Solver::setDecisionVar ( Var v, bool b, bool use_oheap = true )

inline

Definition at line 573 of file Solver.h.

{ 
    if      ( b && !decision[v]) dec_vars++;
    else if (!b &&  decision[v]) dec_vars--;
 
    decision[v] = b;
    if( use_oheap ) 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 206 of file Glucose2.cpp.

                                {
  incremental = true;
}

Here is the caller graph for this function:

setItpcSize()

void Gluco2::Solver::setItpcSize ( int sz )

inlineprotected

Definition at line 467 of file CGlucoseCore.h.

                                       {
    assert( 3 >= sz );
    assert( CRef_Undef != itpc );
    ca[itpc].header.size = sz;
}

Here is the caller graph for this function:

setJust()

void Gluco2::Solver::setJust ( int njftr )

inline

Definition at line 472 of file Solver.h.

{ jftr = njftr; }

Here is the caller graph for this function:

setNewRound()

void Gluco2::Solver::setNewRound ( )

inline

Definition at line 470 of file Solver.h.

{ travId ++ ; }

Here is the caller graph for this function:

setPolarity()

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

inline

Definition at line 572 of file Solver.h.

{ polarity[v] = b; }

setPropBudget()

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

inline

Definition at line 582 of file Solver.h.

{ propagation_budget = propagations + x; }

setVarFaninLits() [1/2]

void Gluco2::Solver::setVarFaninLits ( int v, int lit1, int lit2 )

inline

Definition at line 467 of file Solver.h.

{ setVarFaninLits( Var(v), toLit(lit1), toLit(lit2) ); }

Here is the call graph for this function:

Here is the caller graph for this function:

setVarFaninLits() [2/2]

void Gluco2::Solver::setVarFaninLits ( Var v, Lit lit1, Lit lit2 )

inline

inline void Solver::delVarFaninLits( Var v ){ if( toLit(~0) != getFaninLit0(v) ){ if( toLit(~0) == var2FanoutP[ (v<<1) + 0 ] ){ head of linked-list Lit root = mkLit(getFaninVar0(v)); Lit next = var2FanoutN[ (v<<1) + 0 ]; if( toLit(~0) != next ){ assert( var2Fanout0[ toInt(root) ] == toLit((v<<1) + 0) ); assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 0) ); var2Fanout0[ getFaninVar0(v) ] = next; var2FanoutP[ toInt(next) ] = toLit(~0); } } else { Lit prev = var2FanoutP[ (v<<1) + 0 ]; Lit next = var2FanoutN[ (v<<1) + 0 ]; if( toLit(~0) != next ){ assert( var2FanoutN[ toInt(prev) ] == toLit((v<<1) + 0) ); assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 0) ); var2FanoutN[ toInt(prev) ] = next; var2FanoutP[ toInt(next) ] = prev; } } }

if( toLit(~0) != getFaninLit1(v) ){
    if( toLit(~0) == var2FanoutP[ (v<<1) + 1 ] ){

head of linked-list Lit root = mkLit(getFaninVar1(v)); Lit next = var2FanoutN[ (v<<1) + 1 ]; if( toLit(~0) != next ){ assert( var2Fanout0[ toInt(root) ] == toLit((v<<1) + 1) ); assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 1) ); var2Fanout0[ getFaninVar1(v) ] = next; var2FanoutP[ toInt(next) ] = toLit(~0); } } else { Lit prev = var2FanoutP[ (v<<1) + 1 ]; Lit next = var2FanoutN[ (v<<1) + 1 ]; if( toLit(~0) != next ){ assert( var2FanoutN[ toInt(prev) ] == toLit((v<<1) + 1) ); assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 1) ); var2FanoutN[ toInt(prev) ] = next; var2FanoutP[ toInt(next) ] = prev; } } }

var2FanoutP [ (v<<1) + 0 ] = toLit(~0); var2FanoutP [ (v<<1) + 1 ] = toLit(~0); var2FanoutN [ (v<<1) + 0 ] = toLit(~0); var2FanoutN [ (v<<1) + 1 ] = toLit(~0); var2FaninLits[ (v<<1) + 0 ] = toLit(~0); var2FaninLits[ (v<<1) + 1 ] = toLit(~0); }

Definition at line 244 of file CGlucoseCore.h.

                                                              {
    assert( var(lit1) != var(lit2) );
    int mincap = var(lit1) < var(lit2)? var(lit2): var(lit1);
    mincap = (v < mincap? mincap: v) + 1;
 
    var2NodeData[ v ].lit0 = lit1;
    var2NodeData[ v ].lit1 = lit2;
 
 
    assert( toLit(~0) != lit1 && toLit(~0) != lit2 );
 
    var2FanoutN[ (v<<1) + 0 ] = var2Fanout0[ var(lit1) ];
    var2FanoutN[ (v<<1) + 1 ] = var2Fanout0[ var(lit2) ];
    var2Fanout0[ var(lit1) ] = toLit( (v<<1) + 0 );
    var2Fanout0[ var(lit2) ] = toLit( (v<<1) + 1 );
 
    //if( toLit(~0) != var2FanoutN[ (v<<1) + 0 ] )
    //  var2FanoutP[ toInt(var2FanoutN[ (v<<1) + 0 ]) ] = toLit((v<<1) + 0);
 
    //if( toLit(~0) != var2FanoutN[ (v<<1) + 1 ] )
    //  var2FanoutP[ toInt(var2FanoutN[ (v<<1) + 1 ]) ] = toLit((v<<1) + 1);
}

Here is the call graph for this function:

Here is the caller graph for this function:

simplify()

bool Solver::simplify

(

)

Definition at line 1159 of file Glucose2.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();
 
    #ifdef CGLUCOSE_EXP
    if( !justUsage() )
    #endif
        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 Gluco2::Solver::solve ( )

inline

Definition at line 594 of file Solver.h.

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

Here is the call graph for this function:

solve() [2/5]

bool Gluco2::Solver::solve ( const vec< Lit > & assumps )

inline

Definition at line 598 of file Solver.h.

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

Here is the call graph for this function:

solve() [3/5]

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

inline

Definition at line 595 of file Solver.h.

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

Here is the call graph for this function:

solve() [4/5]

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

inline

Definition at line 596 of file Solver.h.

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

Here is the call graph for this function:

solve() [5/5]

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

inline

Definition at line 597 of file Solver.h.

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

Here is the call graph for this function:

solve_()

lbool Solver::solve_ ( )

protected

Definition at line 1391 of file Glucose2.cpp.

{
 
    #ifdef CGLUCOSE_EXP
    ResetJustData(false);
    #endif
 
    if(incremental && certifiedUNSAT) {
        printf("Can not use incremental and certified unsat in the same time\n");
        exit(-1);
    }
 
    conflict.shrink_(conflict.size());
    if (!ok){
      travId_prev = travId;
      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 |          | pol-inconsist\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){
 
        if( justUsage() ){
            if( nSkipMark ){
                loadJust();
            } else {
                JustModel.shrink_(JustModel.size());
                assert(jheap.empty());
                //JustModel.growTo(nVars());
                int i = 0, j = 0;
                JustModel.push(toLit(0));
                for (; i < trail.size(); i++) 
                    if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
                        JustModel.push(trail[i]), j++;
                JustModel[0] = toLit(j);
            }
            
        } else {
            // Extend & copy model:
            model.shrink_(model.size());
            model.growTo(nVars());
            for (int i = 0; i < trail.size(); i++) model[ var(trail[i]) ] = value(var(trail[i]));
        }
    }else if (status == l_False && conflict.size() == 0)
        ok = false;
 
    //#ifdef CGLUCOSE_EXP
    //if(status == l_True && 0 < justUsage())
    //  justCheck();
    //#endif
 
    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
 
    travId_prev = travId;
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

solveLimited() [1/2]

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

inline

Definition at line 599 of file Solver.h.

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

Here is the call graph for this function:

solveLimited() [2/2]

int Gluco2::Solver::solveLimited ( int * lit0, int nlits )

inline

Definition at line 615 of file Solver.h.

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

Here is the call graph for this function:

toDimacs() [1/7]

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

inline

Definition at line 602 of file Solver.h.

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

Here is the call graph for this function:

toDimacs() [2/7]

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

Definition at line 1542 of file Glucose2.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 Gluco2::Solver::toDimacs ( const char * file, Lit p )

inline

Definition at line 603 of file Solver.h.

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

Here is the call graph for this function:

toDimacs() [4/7]

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

inline

Definition at line 604 of file Solver.h.

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

Here is the call graph for this function:

toDimacs() [5/7]

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

inline

Definition at line 605 of file Solver.h.

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

Here is the call graph for this function:

toDimacs() [6/7]

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

Definition at line 1531 of file Glucose2.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 1552 of file Glucose2.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 925 of file Glucose2.cpp.

{
    if( justUsage() && !isRoundWatch(var(p)) )
        return;
    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:

uncheckedEnqueue2()

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

inlineprotected

Definition at line 76 of file CGlucoseCore.h.

{
    //assert( isRoundWatch(var(p)) ); // inplace sorting guarantee this 
    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:

updateJustActivity()

void Gluco2::Solver::updateJustActivity ( Var v )

inlineprotected

Definition at line 142 of file CGlucoseCore.h.

                                             {
    if( ! var2NodeData[v].sort )
        inplace_sort(v);
 
    int nFanout = 0;
    for(Lit lfo = var2Fanout0[ v ]; nFanout < var2NodeData[v].sort; lfo = var2FanoutN[ toInt(lfo) ], nFanout ++ ){
        Var x = var(lfo);
        if( var2NodeData[x].now && jheap.inHeap(x) ){
            if( activity[getFaninVar1(x)] > activity[getFaninVar0(x)] )
                jheap.update( JustKey( activity[getFaninVar1(x)], x, jheap.data_attr(x) ) );
            else
                jheap.update( JustKey( activity[getFaninVar0(x)], x, jheap.data_attr(x) ) );
        }
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

value() [1/2]

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

inline

Definition at line 563 of file Solver.h.

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

Here is the call graph for this function:

value() [2/2]

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

inline

Definition at line 562 of file Solver.h.

{ return assigns[x]; }

Here is the caller graph for this function:

Var2CRef()

CRef Gluco2::Solver::Var2CRef ( Var v ) const

inlineprotected

Definition at line 421 of file Solver.h.

{ return v  |  (1<<(sizeof(CRef)*8-1)); }

Here is the caller graph for this function:

varActivity()

double Gluco2::Solver::varActivity ( int v ) const

inline

Definition at line 478 of file Solver.h.

{ return activity[v];}

varBumpActivity() [1/2]

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

inlineprotected

Definition at line 503 of file Solver.h.

{ varBumpActivity(v, var_inc); }

Here is the call graph for this function:

varBumpActivity() [2/2]

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

inlineprotected

Definition at line 504 of file Solver.h.

                                                     {
    if ( (activity[v] += inc) > 1e100 ) {
        heap_rescale = 1;
        // 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 (!justUsage() && 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 Gluco2::Solver::varDecayActivity ( )

inlineprotected

Definition at line 502 of file Solver.h.

{ var_inc *= (1 / var_decay); }

Here is the caller graph for this function:

varPolarity()

int Gluco2::Solver::varPolarity ( int v )

inline

Definition at line 480 of file Solver.h.

{ return polarity[v]? 1: 0;}

withinBudget()

bool Gluco2::Solver::withinBudget ( ) const

inlineprotected

Definition at line 586 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> Gluco2::Solver::activity

protected

Definition at line 237 of file Solver.h.

add_tmp

vec<Lit> Gluco2::Solver::add_tmp

protected

Definition at line 282 of file Solver.h.

analyze_stack

vec<Lit> Gluco2::Solver::analyze_stack

protected

Definition at line 280 of file Solver.h.

analyze_toclear

vec<Lit> Gluco2::Solver::analyze_toclear

protected

Definition at line 281 of file Solver.h.

assigns

vec<lbool> Gluco2::Solver::assigns

protected

Definition at line 246 of file Solver.h.

assumptionPositions

vec<int> Gluco2::Solver::assumptionPositions

protected

Definition at line 302 of file Solver.h.

assumptions

vec<Lit> Gluco2::Solver::assumptions

protected

Definition at line 256 of file Solver.h.

asynch_interrupt

bool Gluco2::Solver::asynch_interrupt

protected

Definition at line 294 of file Solver.h.

ca

ClauseAllocator Gluco2::Solver::ca

protected

Definition at line 267 of file Solver.h.

ccmin_mode

int Gluco2::Solver::ccmin_mode

Definition at line 187 of file Solver.h.

certifiedOutput

FILE* Gluco2::Solver::certifiedOutput

Definition at line 194 of file Solver.h.

certifiedUNSAT

bool Gluco2::Solver::certifiedUNSAT

Definition at line 195 of file Solver.h.

cla_inc

double Gluco2::Solver::cla_inc

protected

Definition at line 236 of file Solver.h.

clause_decay

double Gluco2::Solver::clause_decay

Definition at line 184 of file Solver.h.

clauses

vec<CRef> Gluco2::Solver::clauses

protected

Definition at line 243 of file Solver.h.

clauses_literals

int64_t Gluco2::Solver::clauses_literals

Definition at line 201 of file Solver.h.

conflict

vec<Lit> Gluco2::Solver::conflict

Definition at line 159 of file Solver.h.

conflict_budget

int64_t Gluco2::Solver::conflict_budget

protected

Definition at line 292 of file Solver.h.

conflicts

int64_t Gluco2::Solver::conflicts

Definition at line 200 of file Solver.h.

conflictsRestarts

int64_t Gluco2::Solver::conflictsRestarts

Definition at line 200 of file Solver.h.

curRestart

long Gluco2::Solver::curRestart

protected

Definition at line 204 of file Solver.h.

dec_vars

int64_t Gluco2::Solver::dec_vars

Definition at line 201 of file Solver.h.

decision

vec<char> Gluco2::Solver::decision

protected

Definition at line 248 of file Solver.h.

decisions

int64_t Gluco2::Solver::decisions

Definition at line 200 of file Solver.h.

firstReduceDB

int Gluco2::Solver::firstReduceDB

Definition at line 174 of file Solver.h.

garbage_frac

double Gluco2::Solver::garbage_frac

Definition at line 191 of file Solver.h.

heap_rescale

bool Gluco2::Solver::heap_rescale

protected

Definition at line 372 of file Solver.h.

incReduceDB

int Gluco2::Solver::incReduceDB

Definition at line 175 of file Solver.h.

incremental

int Gluco2::Solver::incremental

protected

Definition at line 298 of file Solver.h.

initialPositions

vec<int> Gluco2::Solver::initialPositions

protected

Definition at line 302 of file Solver.h.

itpc

CRef Gluco2::Solver::itpc

protected

Definition at line 383 of file Solver.h.

jftr

int Gluco2::Solver::jftr

Definition at line 70 of file Solver.h.

jhead

int Gluco2::Solver::jhead

protected

Definition at line 428 of file Solver.h.

jheap

Heap2<JustOrderLt2, JustKey> Gluco2::Solver::jheap

protected

Definition at line 453 of file Solver.h.

jlevel

vec<int> Gluco2::Solver::jlevel

protected

Definition at line 454 of file Solver.h.

jnext

vec<int> Gluco2::Solver::jnext

protected

Definition at line 455 of file Solver.h.

JustModel

vec<Lit> Gluco2::Solver::JustModel

Definition at line 481 of file Solver.h.

K

double Gluco2::Solver::K

Definition at line 168 of file Solver.h.

lastblockatrestart

int64_t Gluco2::Solver::lastblockatrestart

Definition at line 200 of file Solver.h.

lastIndexRed

int Gluco2::Solver::lastIndexRed

protected

Definition at line 234 of file Solver.h.

lbdQueue

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

protected

Definition at line 271 of file Solver.h.

lbLBDFrozenClause

unsigned int Gluco2::Solver::lbLBDFrozenClause

Definition at line 177 of file Solver.h.

lbLBDMinimizingClause

unsigned int Gluco2::Solver::lbLBDMinimizingClause

Definition at line 181 of file Solver.h.

lbSizeMinimizingClause

int Gluco2::Solver::lbSizeMinimizingClause

Definition at line 180 of file Solver.h.

learnts

vec<CRef> Gluco2::Solver::learnts

protected

Definition at line 244 of file Solver.h.

learnts_literals

int64_t Gluco2::Solver::learnts_literals

Definition at line 201 of file Solver.h.

learntsize_adjust_cnt

int Gluco2::Solver::learntsize_adjust_cnt

protected

Definition at line 288 of file Solver.h.

learntsize_adjust_confl

double Gluco2::Solver::learntsize_adjust_confl

protected

Definition at line 287 of file Solver.h.

max_learnts

double Gluco2::Solver::max_learnts

protected

Definition at line 286 of file Solver.h.

max_literals

int64_t Gluco2::Solver::max_literals

Definition at line 201 of file Solver.h.

model

vec<lbool> Gluco2::Solver::model

Definition at line 158 of file Solver.h.

MYFLAG

unsigned int Gluco2::Solver::MYFLAG

protected

Definition at line 283 of file Solver.h.

nbBin

int64_t Gluco2::Solver::nbBin

Definition at line 200 of file Solver.h.

nbclausesbeforereduce

int Gluco2::Solver::nbclausesbeforereduce

protected

Definition at line 269 of file Solver.h.

nbDL2

int64_t Gluco2::Solver::nbDL2

Definition at line 200 of file Solver.h.

nbpos

vec<int> Gluco2::Solver::nbpos

protected

Definition at line 250 of file Solver.h.

nbReduceDB

int64_t Gluco2::Solver::nbReduceDB

Definition at line 200 of file Solver.h.

nbReducedClauses

int64_t Gluco2::Solver::nbReducedClauses

Definition at line 200 of file Solver.h.

nbRemovedClauses

int64_t Gluco2::Solver::nbRemovedClauses

Definition at line 200 of file Solver.h.

nbSatCalls

int Gluco2::Solver::nbSatCalls

protected

Definition at line 301 of file Solver.h.

nbstopsrestarts

int64_t Gluco2::Solver::nbstopsrestarts

Definition at line 200 of file Solver.h.

nbstopsrestartssame

int64_t Gluco2::Solver::nbstopsrestartssame

Definition at line 200 of file Solver.h.

nbUn

int64_t Gluco2::Solver::nbUn

Definition at line 200 of file Solver.h.

nbUnsatCalls

int Gluco2::Solver::nbUnsatCalls

protected

Definition at line 301 of file Solver.h.

nbVarsInitialFormula

int Gluco2::Solver::nbVarsInitialFormula

protected

Definition at line 299 of file Solver.h.

nCallConfl

int Gluco2::Solver::nCallConfl

Definition at line 62 of file Solver.h.

nRuntimeLimit

uint64_t Gluco2::Solver::nRuntimeLimit

Definition at line 65 of file Solver.h.

nSkipMark

int Gluco2::Solver::nSkipMark

protected

Definition at line 457 of file Solver.h.

ok

bool Gluco2::Solver::ok

protected

Definition at line 235 of file Solver.h.

order_heap

Heap<VarOrderLt> Gluco2::Solver::order_heap

protected

Definition at line 257 of file Solver.h.

pCnfFunc

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

Definition at line 61 of file Solver.h.

pCnfMan

void* Gluco2::Solver::pCnfMan

Definition at line 60 of file Solver.h.

permDiff

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

protected

Definition at line 260 of file Solver.h.

phase_saving

int Gluco2::Solver::phase_saving

Definition at line 188 of file Solver.h.

polarity

vec<char> Gluco2::Solver::polarity

protected

Definition at line 247 of file Solver.h.

progress_estimate

double Gluco2::Solver::progress_estimate

protected

Definition at line 258 of file Solver.h.

propagation_budget

int64_t Gluco2::Solver::propagation_budget

protected

Definition at line 293 of file Solver.h.

propagations

int64_t Gluco2::Solver::propagations

Definition at line 200 of file Solver.h.

pstop

int* Gluco2::Solver::pstop

Definition at line 64 of file Solver.h.

qhead

int Gluco2::Solver::qhead

protected

Definition at line 253 of file Solver.h.

R

double Gluco2::Solver::R

Definition at line 169 of file Solver.h.

random_seed

double Gluco2::Solver::random_seed

Definition at line 186 of file Solver.h.

random_var_freq

double Gluco2::Solver::random_var_freq

Definition at line 185 of file Solver.h.

remove_satisfied

bool Gluco2::Solver::remove_satisfied

protected

Definition at line 259 of file Solver.h.

rnd_decisions

int64_t Gluco2::Solver::rnd_decisions

Definition at line 200 of file Solver.h.

rnd_init_act

bool Gluco2::Solver::rnd_init_act

Definition at line 190 of file Solver.h.

rnd_pol

bool Gluco2::Solver::rnd_pol

Definition at line 189 of file Solver.h.

seen

vec<char> Gluco2::Solver::seen

protected

Definition at line 279 of file Solver.h.

showModel

int Gluco2::Solver::showModel

Definition at line 166 of file Solver.h.

simpDB_assigns

int Gluco2::Solver::simpDB_assigns

protected

Definition at line 254 of file Solver.h.

simpDB_props

int64_t Gluco2::Solver::simpDB_props

protected

Definition at line 255 of file Solver.h.

sizeLBDQueue

double Gluco2::Solver::sizeLBDQueue

Definition at line 170 of file Solver.h.

sizeTrailQueue

double Gluco2::Solver::sizeTrailQueue

Definition at line 171 of file Solver.h.

SolverType

int Gluco2::Solver::SolverType

Definition at line 52 of file Solver.h.

solves

int64_t Gluco2::Solver::solves

Definition at line 200 of file Solver.h.

specialIncReduceDB

int Gluco2::Solver::specialIncReduceDB

Definition at line 176 of file Solver.h.

starts

int64_t Gluco2::Solver::starts

Definition at line 200 of file Solver.h.

sumAssumptions

int Gluco2::Solver::sumAssumptions

protected

Definition at line 273 of file Solver.h.

sumLBD

float Gluco2::Solver::sumLBD

protected

Definition at line 272 of file Solver.h.

terminate_search_early

bool Gluco2::Solver::terminate_search_early

Definition at line 63 of file Solver.h.

tot_literals

int64_t Gluco2::Solver::tot_literals

Definition at line 201 of file Solver.h.

totalTime4Sat

double Gluco2::Solver::totalTime4Sat

protected

Definition at line 300 of file Solver.h.

totalTime4Unsat

double Gluco2::Solver::totalTime4Unsat

protected

Definition at line 300 of file Solver.h.

trail

vec<Lit> Gluco2::Solver::trail

protected

Definition at line 249 of file Solver.h.

trail_lim

vec<int> Gluco2::Solver::trail_lim

protected

Definition at line 251 of file Solver.h.

trailQueue

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

protected

Definition at line 271 of file Solver.h.

travId

unsigned Gluco2::Solver::travId

protected

Definition at line 425 of file Solver.h.

travId_prev

unsigned Gluco2::Solver::travId_prev

protected

Definition at line 425 of file Solver.h.

user_lits

vec<Lit> Gluco2::Solver::user_lits

Definition at line 67 of file Solver.h.

user_vec

vec<int> Gluco2::Solver::user_vec

Definition at line 66 of file Solver.h.

var2Fanout0

vec<Lit> Gluco2::Solver::var2Fanout0

protected

Definition at line 382 of file Solver.h.

var2FanoutN

vec<Lit> Gluco2::Solver::var2FanoutN

protected

Definition at line 382 of file Solver.h.

var2NodeData

vec<NodeData> Gluco2::Solver::var2NodeData

protected

Definition at line 379 of file Solver.h.

var2TravId

vec<unsigned> Gluco2::Solver::var2TravId

protected

Definition at line 381 of file Solver.h.

var_decay

double Gluco2::Solver::var_decay

Definition at line 183 of file Solver.h.

var_inc

double Gluco2::Solver::var_inc

protected

Definition at line 238 of file Solver.h.

vardata

vec<VarData> Gluco2::Solver::vardata

protected

Definition at line 252 of file Solver.h.

verbEveryConflicts

int Gluco2::Solver::verbEveryConflicts

Definition at line 165 of file Solver.h.

verbosity

int Gluco2::Solver::verbosity

Definition at line 164 of file Solver.h.

vMarked

vec<Var> Gluco2::Solver::vMarked

protected

Definition at line 460 of file Solver.h.

watches

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

protected

Definition at line 240 of file Solver.h.

watchesBin

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

protected

Definition at line 242 of file Solver.h.

---

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

• src/sat/glucose2/Solver.h
• src/sat/glucose2/CGlucoseCore.h
• src/sat/glucose2/Glucose2.cpp