| abstractLevel(Var x) const | Gluco2::Solver | inlineprotected |
| activity | Gluco2::Solver | protected |
| add_tmp | Gluco2::Solver | protected |
| addClause(const vec< Lit > &ps) | Gluco2::SimpSolver | inline |
| addClause(Lit p) | Gluco2::SimpSolver | inline |
| addClause(Lit p, Lit q) | Gluco2::SimpSolver | inline |
| addClause(Lit p, Lit q, Lit r) | Gluco2::SimpSolver | inline |
| addClause_(vec< Lit > &ps) | Gluco2::SimpSolver | |
| addEmptyClause() | Gluco2::SimpSolver | inline |
| addJwatch(Var host, Var member, int index) | Gluco2::Solver | inlineprotected |
| addVar(Var v) | Gluco2::SimpSolver | inline |
| analyze(CRef confl, vec< Lit > &out_learnt, vec< Lit > &selectors, int &out_btlevel, unsigned int &nblevels, unsigned int &szWithoutSelectors) | Gluco2::Solver | protected |
| analyze_stack | Gluco2::Solver | protected |
| analyze_toclear | Gluco2::Solver | protected |
| analyzeFinal(Lit p, vec< Lit > &out_conflict) | Gluco2::Solver | protected |
| assigns | Gluco2::Solver | protected |
| assumptionPositions | Gluco2::Solver | protected |
| assumptions | Gluco2::Solver | protected |
| asymm(Var v, CRef cr) | Gluco2::SimpSolver | protected |
| asymm_lits | Gluco2::SimpSolver | |
| asymmVar(Var v) | Gluco2::SimpSolver | protected |
| asynch_interrupt | Gluco2::Solver | protected |
| attachClause(CRef cr) | Gluco2::Solver | protected |
| backwardSubsumptionCheck(bool verbose=false) | Gluco2::SimpSolver | protected |
| budgetOff() | Gluco2::Solver | inline |
| bwdsub_assigns | Gluco2::SimpSolver | protected |
| bwdsub_tmpunit | Gluco2::SimpSolver | protected |
| ca | Gluco2::Solver | protected |
| cancelUntil(int level) | Gluco2::Solver | protected |
| castCRef(Lit p) | Gluco2::Solver | inlineprotected |
| ccmin_mode | Gluco2::Solver | |
| certifiedOutput | Gluco2::Solver | |
| certifiedUNSAT | Gluco2::Solver | |
| checkGarbage(double gf) | Gluco2::Solver | inline |
| checkGarbage() | Gluco2::Solver | inline |
| cla_inc | Gluco2::Solver | protected |
| claBumpActivity(Clause &c) | Gluco2::Solver | inlineprotected |
| claDecayActivity() | Gluco2::Solver | inlineprotected |
| clause_decay | Gluco2::Solver | |
| clause_lim | Gluco2::SimpSolver | |
| clauses | Gluco2::Solver | protected |
| clauses_literals | Gluco2::Solver | |
| cleanUpClauses() | Gluco2::SimpSolver | protected |
| clearInterrupt() | Gluco2::Solver | inline |
| computeLBD(const vec< Lit > &lits, int end=-1) | Gluco2::Solver | inlineprotected |
| computeLBD(const Clause &c) | Gluco2::Solver | inlineprotected |
| conflict | Gluco2::Solver | |
| conflict_budget | Gluco2::Solver | protected |
| conflicts | Gluco2::Solver | |
| conflictsRestarts | Gluco2::Solver | |
| CRef2Var(CRef cr) const | Gluco2::Solver | inlineprotected |
| curRestart | Gluco2::Solver | protected |
| dec_vars | Gluco2::Solver | |
| decision | Gluco2::Solver | protected |
| decisionLevel() const | Gluco2::Solver | inlineprotected |
| decisions | Gluco2::Solver | |
| detachClause(CRef cr, bool strict=false) | Gluco2::Solver | protected |
| drand(double &seed) | Gluco2::Solver | inlineprotectedstatic |
| elim_heap | Gluco2::SimpSolver | protected |
| elimclauses | Gluco2::SimpSolver | protected |
| eliminate(bool turn_off_elim=false) | Gluco2::SimpSolver | |
| eliminated | Gluco2::SimpSolver | protected |
| eliminated_clauses | Gluco2::SimpSolver | |
| eliminated_vars | Gluco2::SimpSolver | |
| eliminateVar(Var v) | Gluco2::SimpSolver | protected |
| elimorder | Gluco2::SimpSolver | protected |
| enqueue(Lit p, CRef from=CRef_Undef) | Gluco2::Solver | inlineprotected |
| extendModel() | Gluco2::SimpSolver | protected |
| firstReduceDB | Gluco2::Solver | |
| frozen | Gluco2::SimpSolver | protected |
| garbage_frac | Gluco2::Solver | |
| garbageCollect() | Gluco2::SimpSolver | virtual |
| gateAddJwatch(Var v, int index) | Gluco2::Solver | inlineprotected |
| gateClearJwatch(Var v, int backtrack_level) | Gluco2::Solver | protected |
| gateJustFanin(Var v) const | Gluco2::Solver | inlineprotected |
| gatePropagate(Lit p) | Gluco2::Solver | inlineprotected |
| gatePropagateCheck(Var v, Var t) | Gluco2::Solver | protected |
| gatePropagateCheckFanout(Var v, Lit lfo) | Gluco2::Solver | inlineprotected |
| gatePropagateCheckThis(Var v) | Gluco2::Solver | inlineprotected |
| gatherTouchedClauses() | Gluco2::SimpSolver | protected |
| getCex() const | Gluco2::Solver | inline |
| getConfClause(CRef r) | Gluco2::Solver | inlineprotected |
| getFaninC0(Var v) const | Gluco2::Solver | inlineprotected |
| getFaninC1(Var v) const | Gluco2::Solver | inlineprotected |
| getFaninLit0(Var v) const | Gluco2::Solver | inlineprotected |
| getFaninLit1(Var v) const | Gluco2::Solver | inlineprotected |
| getFaninPlt0(Var v) const | Gluco2::Solver | inlineprotected |
| getFaninPlt1(Var v) const | Gluco2::Solver | inlineprotected |
| getFaninVar0(Var v) const | Gluco2::Solver | inlineprotected |
| getFaninVar1(Var v) const | Gluco2::Solver | inlineprotected |
| grow | Gluco2::SimpSolver | |
| heap_rescale | Gluco2::Solver | protected |
| implied(const vec< Lit > &c) | Gluco2::SimpSolver | protected |
| incReduceDB | Gluco2::Solver | |
| incremental | Gluco2::Solver | protected |
| initialPositions | Gluco2::Solver | protected |
| initNbInitialVars(int nb) | Gluco2::Solver | |
| inplace_sort(Var v) | Gluco2::Solver | inlineprotected |
| insertVarOrder(Var x) | Gluco2::Solver | inlineprotected |
| interpret(Var v, Var t) | Gluco2::Solver | inlineprotected |
| interrupt() | Gluco2::Solver | inline |
| irand(double &seed, int size) | Gluco2::Solver | inlineprotectedstatic |
| isAND(Var v) const | Gluco2::Solver | inlineprotected |
| isEliminated(Var v) const | Gluco2::SimpSolver | inline |
| isGateCRef(CRef cr) const | Gluco2::Solver | inlineprotected |
| isJReason(Var v) const | Gluco2::Solver | inlineprotected |
| isRoundWatch(Var v) const | Gluco2::Solver | inline |
| isSelector(Var v) | Gluco2::Solver | inlineprotected |
| isTwoFanin(Var v) const | Gluco2::Solver | inlineprotected |
| itpc | Gluco2::Solver | protected |
| jftr | Gluco2::Solver | |
| jhead | Gluco2::Solver | protected |
| jheap | Gluco2::Solver | protected |
| jlevel | Gluco2::Solver | protected |
| jnext | Gluco2::Solver | protected |
| justCheck() | Gluco2::Solver | inlineprotected |
| JustModel | Gluco2::Solver | |
| justReset() | Gluco2::Solver | inline |
| justUsage() const | Gluco2::Solver | inline |
| K | Gluco2::Solver | |
| lastblockatrestart | Gluco2::Solver | |
| lastIndexRed | Gluco2::Solver | protected |
| lbdQueue | Gluco2::Solver | protected |
| lbLBDFrozenClause | Gluco2::Solver | |
| lbLBDMinimizingClause | Gluco2::Solver | |
| lbSizeMinimizingClause | Gluco2::Solver | |
| learnts | Gluco2::Solver | protected |
| learnts_literals | Gluco2::Solver | |
| learntsize_adjust_cnt | Gluco2::Solver | protected |
| learntsize_adjust_confl | Gluco2::Solver | protected |
| level(Var x) const | Gluco2::Solver | inline |
| litRedundant(Lit p, uint32_t abstract_levels) | Gluco2::Solver | protected |
| loadJust() | Gluco2::Solver | inlineprotected |
| loadJust_rec(Var v) | Gluco2::Solver | inlineprotected |
| locked(const Clause &c) const | Gluco2::Solver | inlineprotected |
| markApprox(Var v0, Var v1, int nlim) | Gluco2::Solver | inline |
| markCone(Var v) | Gluco2::Solver | inline |
| markTill(Var v0, int nlim) | Gluco2::Solver | inline |
| max_learnts | Gluco2::Solver | protected |
| max_literals | Gluco2::Solver | |
| maxActiveLit(Lit lit0, Lit lit1) const | Gluco2::Solver | inlineprotected |
| merge(const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause) | Gluco2::SimpSolver | protected |
| merge(const Clause &_ps, const Clause &_qs, Var v, int &size) | Gluco2::SimpSolver | protected |
| merges | Gluco2::SimpSolver | |
| minimisationWithBinaryResolution(vec< Lit > &out_learnt) | Gluco2::Solver | protected |
| mkNodeData() | Gluco2::Solver | inlineprotectedstatic |
| mkVarData(CRef cr, int l) | Gluco2::Solver | inlineprotectedstatic |
| model | Gluco2::Solver | |
| modelValue(Var x) const | Gluco2::Solver | inline |
| modelValue(Lit p) const | Gluco2::Solver | inline |
| MYFLAG | Gluco2::Solver | protected |
| n_occ | Gluco2::SimpSolver | protected |
| n_touched | Gluco2::SimpSolver | protected |
| nAssigns() const | Gluco2::Solver | inline |
| nbBin | Gluco2::Solver | |
| nbclausesbeforereduce | Gluco2::Solver | protected |
| nbDL2 | Gluco2::Solver | |
| nbpos | Gluco2::Solver | protected |
| nbReduceDB | Gluco2::Solver | |
| nbReducedClauses | Gluco2::Solver | |
| nbRemovedClauses | Gluco2::Solver | |
| nbSatCalls | Gluco2::Solver | protected |
| nbstopsrestarts | Gluco2::Solver | |
| nbstopsrestartssame | Gluco2::Solver | |
| nbUn | Gluco2::Solver | |
| nbUnsatCalls | Gluco2::Solver | protected |
| nbVarsInitialFormula | Gluco2::Solver | protected |
| nCallConfl | Gluco2::Solver | |
| nClauses() const | Gluco2::Solver | inline |
| newDecisionLevel() | Gluco2::Solver | inlineprotected |
| newVar(bool polarity=true, bool dvar=true) | Gluco2::SimpSolver | |
| nFreeVars() const | Gluco2::Solver | inline |
| nLearnts() const | Gluco2::Solver | inline |
| nRuntimeLimit | Gluco2::Solver | |
| nSkipMark | Gluco2::Solver | protected |
| nVars() const | Gluco2::Solver | inline |
| occurs | Gluco2::SimpSolver | protected |
| ok | Gluco2::Solver | protected |
| okay() const | Gluco2::Solver | inline |
| order_heap | Gluco2::Solver | protected |
| parsing | Gluco2::SimpSolver | |
| pCnfFunc | Gluco2::Solver | |
| pCnfMan | Gluco2::Solver | |
| permDiff | Gluco2::Solver | protected |
| phase_saving | Gluco2::Solver | |
| pickBranchLit() | Gluco2::Solver | protected |
| pickJustLit(int &index) | Gluco2::Solver | inlineprotected |
| polarity | Gluco2::Solver | protected |
| prelocate(int base_var_num) | Gluco2::SimpSolver | inline |
| printClause(CRef c) | Gluco2::Solver | inline |
| printIncrementalStats() | Gluco2::Solver | |
| printInitialClause(CRef c) | Gluco2::Solver | inline |
| printLit(Lit l) | Gluco2::Solver | inline |
| progress_estimate | Gluco2::Solver | protected |
| progressEstimate() const | Gluco2::Solver | protected |
| propagate() | Gluco2::Solver | protected |
| propagation_budget | Gluco2::Solver | protected |
| propagations | Gluco2::Solver | |
| pstop | Gluco2::Solver | |
| pushJustQueue(Var v, int index) | Gluco2::Solver | inlineprotected |
| qhead | Gluco2::Solver | protected |
| R | Gluco2::Solver | |
| random_seed | Gluco2::Solver | |
| random_var_freq | Gluco2::Solver | |
| reason(Var x) const | Gluco2::Solver | inlineprotected |
| rebuildOrderHeap() | Gluco2::Solver | protected |
| reduceDB() | Gluco2::Solver | protected |
| relocAll(ClauseAllocator &to) | Gluco2::SimpSolver | protected |
| remove_satisfied | Gluco2::Solver | protected |
| removeClause(CRef cr) | Gluco2::SimpSolver | protected |
| removeSatisfied(vec< CRef > &cs) | Gluco2::Solver | protected |
| reset() | Gluco2::SimpSolver | virtual |
| ResetJustData(bool fCleanMemory) | Gluco2::Solver | inlineprotected |
| restoreJustQueue(int level) | Gluco2::Solver | protected |
| rnd_decisions | Gluco2::Solver | |
| rnd_init_act | Gluco2::Solver | |
| rnd_pol | Gluco2::Solver | |
| sat_solver_jftr() | Gluco2::Solver | inline |
| sat_solver_mark_cone(int) | Gluco2::Solver | inline |
| sat_solver_reset() | Gluco2::Solver | inline |
| sat_solver_set_jftr(int) | Gluco2::Solver | inline |
| sat_solver_set_var_fanin_lit(int, int, int) | Gluco2::Solver | inline |
| sat_solver_start_new_round() | Gluco2::Solver | inline |
| satisfied(const Clause &c) const | Gluco2::Solver | protected |
| search(int nof_conflicts) | Gluco2::Solver | protected |
| seen | Gluco2::Solver | protected |
| setConfBudget(int64_t x) | Gluco2::Solver | inline |
| setDecisionVar(Var v, bool b, bool use_oheap=true) | Gluco2::Solver | inline |
| setFrozen(Var v, bool b) | Gluco2::SimpSolver | inline |
| setIncrementalMode() | Gluco2::Solver | |
| setItpcSize(int sz) | Gluco2::Solver | inlineprotected |
| setJust(int njftr) | Gluco2::Solver | inline |
| setNewRound() | Gluco2::Solver | inline |
| setPolarity(Var v, bool b) | Gluco2::Solver | inline |
| setPropBudget(int64_t x) | Gluco2::Solver | inline |
| setVarFaninLits(Var v, Lit lit1, Lit lit2) | Gluco2::Solver | inline |
| setVarFaninLits(int v, int lit1, int lit2) | Gluco2::Solver | inline |
| showModel | Gluco2::Solver | |
| simp_garbage_frac | Gluco2::SimpSolver | |
| simpDB_assigns | Gluco2::Solver | protected |
| simpDB_props | Gluco2::Solver | protected |
| simplify() | Gluco2::Solver | |
| SimpSolver() | Gluco2::SimpSolver | |
| sizeLBDQueue | Gluco2::Solver | |
| sizeTrailQueue | Gluco2::Solver | |
| solve(const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false) | Gluco2::SimpSolver | inline |
| solve(bool do_simp=true, bool turn_off_simp=false) | Gluco2::SimpSolver | inline |
| solve(Lit p, bool do_simp=true, bool turn_off_simp=false) | Gluco2::SimpSolver | inline |
| solve(Lit p, Lit q, bool do_simp=true, bool turn_off_simp=false) | Gluco2::SimpSolver | inline |
| solve(Lit p, Lit q, Lit r, bool do_simp=true, bool turn_off_simp=false) | Gluco2::SimpSolver | inline |
| Gluco2::Solver::solve(const vec< Lit > &assumps) | Gluco2::Solver | inline |
| Gluco2::Solver::solve() | Gluco2::Solver | inline |
| Gluco2::Solver::solve(Lit p) | Gluco2::Solver | inline |
| Gluco2::Solver::solve(Lit p, Lit q) | Gluco2::Solver | inline |
| Gluco2::Solver::solve(Lit p, Lit q, Lit r) | Gluco2::Solver | inline |
| solve_(bool do_simp=true, bool turn_off_simp=false) | Gluco2::SimpSolver | protected |
| Gluco2::Solver::solve_() | Gluco2::Solver | protected |
| solveLimited(const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false) | Gluco2::SimpSolver | inline |
| solveLimited(int *lit0, int nlits, bool do_simp=false, bool turn_off_simp=false) | Gluco2::SimpSolver | inline |
| Gluco2::Solver::solveLimited(const vec< Lit > &assumps) | Gluco2::Solver | inline |
| Gluco2::Solver::solveLimited(int *, int nlits) | Gluco2::Solver | inline |
| Solver() | Gluco2::Solver | |
| SolverType | Gluco2::Solver | |
| solves | Gluco2::Solver | |
| specialIncReduceDB | Gluco2::Solver | |
| starts | Gluco2::Solver | |
| strengthenClause(CRef cr, Lit l) | Gluco2::SimpSolver | protected |
| substitute(Var v, Lit x) | Gluco2::SimpSolver | |
| subsumption_lim | Gluco2::SimpSolver | |
| subsumption_queue | Gluco2::SimpSolver | protected |
| sumAssumptions | Gluco2::Solver | protected |
| sumLBD | Gluco2::Solver | protected |
| terminate_search_early | Gluco2::Solver | |
| toDimacs(FILE *f, const vec< Lit > &assumps) | Gluco2::Solver | |
| toDimacs(const char *file, const vec< Lit > &assumps) | Gluco2::Solver | |
| toDimacs(FILE *f, Clause &c, vec< Var > &map, Var &max) | Gluco2::Solver | |
| toDimacs(const char *file) | Gluco2::Solver | inline |
| toDimacs(const char *file, Lit p) | Gluco2::Solver | inline |
| toDimacs(const char *file, Lit p, Lit q) | Gluco2::Solver | inline |
| toDimacs(const char *file, Lit p, Lit q, Lit r) | Gluco2::Solver | inline |
| tot_literals | Gluco2::Solver | |
| totalTime4Sat | Gluco2::Solver | protected |
| totalTime4Unsat | Gluco2::Solver | protected |
| touched | Gluco2::SimpSolver | protected |
| trail | Gluco2::Solver | protected |
| trail_lim | Gluco2::Solver | protected |
| trailQueue | Gluco2::Solver | protected |
| travId | Gluco2::Solver | protected |
| travId_prev | Gluco2::Solver | protected |
| uncheckedEnqueue(Lit p, CRef from=CRef_Undef) | Gluco2::Solver | protected |
| uncheckedEnqueue2(Lit p, CRef from=CRef_Undef) | Gluco2::Solver | inlineprotected |
| updateElimHeap(Var v) | Gluco2::SimpSolver | inlineprotected |
| updateJustActivity(Var v) | Gluco2::Solver | inlineprotected |
| use_asymm | Gluco2::SimpSolver | |
| use_elim | Gluco2::SimpSolver | |
| use_rcheck | Gluco2::SimpSolver | |
| use_simplification | Gluco2::SimpSolver | protected |
| user_lits | Gluco2::Solver | |
| user_vec | Gluco2::Solver | |
| value(Var x) const | Gluco2::Solver | inline |
| value(Lit p) const | Gluco2::Solver | inline |
| Var2CRef(Var v) const | Gluco2::Solver | inlineprotected |
| var2Fanout0 | Gluco2::Solver | protected |
| var2FanoutN | Gluco2::Solver | protected |
| var2NodeData | Gluco2::Solver | protected |
| var2TravId | Gluco2::Solver | protected |
| var_decay | Gluco2::Solver | |
| var_inc | Gluco2::Solver | protected |
| varActivity(int v) const | Gluco2::Solver | inline |
| varBumpActivity(Var v, double inc) | Gluco2::Solver | inlineprotected |
| varBumpActivity(Var v) | Gluco2::Solver | inlineprotected |
| vardata | Gluco2::Solver | protected |
| varDecayActivity() | Gluco2::Solver | inlineprotected |
| varPolarity(int v) | Gluco2::Solver | inline |
| verbEveryConflicts | Gluco2::Solver | |
| verbosity | Gluco2::Solver | |
| vMarked | Gluco2::Solver | protected |
| watches | Gluco2::Solver | protected |
| watchesBin | Gluco2::Solver | protected |
| withinBudget() const | Gluco2::Solver | inlineprotected |
| ~SimpSolver() | Gluco2::SimpSolver | |
| ~Solver() | Gluco2::Solver | virtual |
