| abstractLevel(Var x) const | Gluco::Solver | inlineprotected |
| activity | Gluco::Solver | protected |
| add_tmp | Gluco::Solver | protected |
| addClause(const vec< Lit > &ps) | Gluco::SimpSolver | inline |
| addClause(Lit p) | Gluco::SimpSolver | inline |
| addClause(Lit p, Lit q) | Gluco::SimpSolver | inline |
| addClause(Lit p, Lit q, Lit r) | Gluco::SimpSolver | inline |
| addClause_(vec< Lit > &ps) | Gluco::SimpSolver | |
| addEmptyClause() | Gluco::SimpSolver | inline |
| addVar(Var v) | Gluco::SimpSolver | inline |
| analyze(CRef confl, vec< Lit > &out_learnt, vec< Lit > &selectors, int &out_btlevel, unsigned int &nblevels, unsigned int &szWithoutSelectors) | Gluco::Solver | protected |
| analyze_stack | Gluco::Solver | protected |
| analyze_toclear | Gluco::Solver | protected |
| analyzeFinal(Lit p, vec< Lit > &out_conflict) | Gluco::Solver | protected |
| assigns | Gluco::Solver | protected |
| assumptionPositions | Gluco::Solver | protected |
| assumptions | Gluco::Solver | protected |
| asymm(Var v, CRef cr) | Gluco::SimpSolver | protected |
| asymm_lits | Gluco::SimpSolver | |
| asymmVar(Var v) | Gluco::SimpSolver | protected |
| asynch_interrupt | Gluco::Solver | protected |
| attachClause(CRef cr) | Gluco::Solver | protected |
| backwardSubsumptionCheck(bool verbose=false) | Gluco::SimpSolver | protected |
| budgetOff() | Gluco::Solver | inline |
| bwdsub_assigns | Gluco::SimpSolver | protected |
| bwdsub_tmpunit | Gluco::SimpSolver | protected |
| ca | Gluco::Solver | protected |
| cancelUntil(int level) | Gluco::Solver | protected |
| ccmin_mode | Gluco::Solver | |
| certifiedOutput | Gluco::Solver | |
| certifiedUNSAT | Gluco::Solver | |
| checkGarbage(double gf) | Gluco::Solver | inline |
| checkGarbage() | Gluco::Solver | inline |
| cla_inc | Gluco::Solver | protected |
| claBumpActivity(Clause &c) | Gluco::Solver | inlineprotected |
| claDecayActivity() | Gluco::Solver | inlineprotected |
| clause_decay | Gluco::Solver | |
| clause_lim | Gluco::SimpSolver | |
| clauses | Gluco::Solver | protected |
| clauses_literals | Gluco::Solver | |
| cleanUpClauses() | Gluco::SimpSolver | protected |
| clearInterrupt() | Gluco::Solver | inline |
| computeLBD(const vec< Lit > &lits, int end=-1) | Gluco::Solver | inlineprotected |
| computeLBD(const Clause &c) | Gluco::Solver | inlineprotected |
| conflict | Gluco::Solver | |
| conflict_budget | Gluco::Solver | protected |
| conflicts | Gluco::Solver | |
| conflictsRestarts | Gluco::Solver | |
| curRestart | Gluco::Solver | protected |
| dec_vars | Gluco::Solver | |
| decision | Gluco::Solver | protected |
| decisionLevel() const | Gluco::Solver | inlineprotected |
| decisions | Gluco::Solver | |
| detachClause(CRef cr, bool strict=false) | Gluco::Solver | protected |
| drand(double &seed) | Gluco::Solver | inlineprotectedstatic |
| elim_heap | Gluco::SimpSolver | protected |
| elimclauses | Gluco::SimpSolver | protected |
| eliminate(bool turn_off_elim=false) | Gluco::SimpSolver | |
| eliminated | Gluco::SimpSolver | protected |
| eliminated_clauses | Gluco::SimpSolver | |
| eliminated_vars | Gluco::SimpSolver | |
| eliminateVar(Var v) | Gluco::SimpSolver | protected |
| elimorder | Gluco::SimpSolver | protected |
| enqueue(Lit p, CRef from=CRef_Undef) | Gluco::Solver | inlineprotected |
| extendModel() | Gluco::SimpSolver | protected |
| firstReduceDB | Gluco::Solver | |
| frozen | Gluco::SimpSolver | protected |
| garbage_frac | Gluco::Solver | |
| garbageCollect() | Gluco::SimpSolver | virtual |
| gatherTouchedClauses() | Gluco::SimpSolver | protected |
| getCex() const | Gluco::Solver | inline |
| grow | Gluco::SimpSolver | |
| implied(const vec< Lit > &c) | Gluco::SimpSolver | protected |
| incReduceDB | Gluco::Solver | |
| incremental | Gluco::Solver | protected |
| initialPositions | Gluco::Solver | protected |
| initNbInitialVars(int nb) | Gluco::Solver | |
| insertVarOrder(Var x) | Gluco::Solver | inlineprotected |
| interrupt() | Gluco::Solver | inline |
| irand(double &seed, int size) | Gluco::Solver | inlineprotectedstatic |
| isEliminated(Var v) const | Gluco::SimpSolver | inline |
| isSelector(Var v) | Gluco::Solver | inlineprotected |
| jftr | Gluco::Solver | |
| K | Gluco::Solver | |
| lastblockatrestart | Gluco::Solver | |
| lastIndexRed | Gluco::Solver | protected |
| lbdQueue | Gluco::Solver | protected |
| lbLBDFrozenClause | Gluco::Solver | |
| lbLBDMinimizingClause | Gluco::Solver | |
| lbSizeMinimizingClause | Gluco::Solver | |
| learnts | Gluco::Solver | protected |
| learnts_literals | Gluco::Solver | |
| learntsize_adjust_cnt | Gluco::Solver | protected |
| learntsize_adjust_confl | Gluco::Solver | protected |
| level(Var x) const | Gluco::Solver | inlineprotected |
| litRedundant(Lit p, uint32_t abstract_levels) | Gluco::Solver | protected |
| locked(const Clause &c) const | Gluco::Solver | inlineprotected |
| max_learnts | Gluco::Solver | protected |
| max_literals | Gluco::Solver | |
| merge(const Clause &_ps, const Clause &_qs, Var v, vec< Lit > &out_clause) | Gluco::SimpSolver | protected |
| merge(const Clause &_ps, const Clause &_qs, Var v, int &size) | Gluco::SimpSolver | protected |
| merges | Gluco::SimpSolver | |
| minimisationWithBinaryResolution(vec< Lit > &out_learnt) | Gluco::Solver | protected |
| mkVarData(CRef cr, int l) | Gluco::Solver | inlineprotectedstatic |
| model | Gluco::Solver | |
| modelValue(Var x) const | Gluco::Solver | inline |
| modelValue(Lit p) const | Gluco::Solver | inline |
| MYFLAG | Gluco::Solver | protected |
| n_occ | Gluco::SimpSolver | protected |
| n_touched | Gluco::SimpSolver | protected |
| nAssigns() const | Gluco::Solver | inline |
| nbBin | Gluco::Solver | |
| nbclausesbeforereduce | Gluco::Solver | protected |
| nbDL2 | Gluco::Solver | |
| nbpos | Gluco::Solver | protected |
| nbReduceDB | Gluco::Solver | |
| nbReducedClauses | Gluco::Solver | |
| nbRemovedClauses | Gluco::Solver | |
| nbSatCalls | Gluco::Solver | protected |
| nbstopsrestarts | Gluco::Solver | |
| nbstopsrestartssame | Gluco::Solver | |
| nbUn | Gluco::Solver | |
| nbUnsatCalls | Gluco::Solver | protected |
| nbVarsInitialFormula | Gluco::Solver | protected |
| nCallConfl | Gluco::Solver | |
| nClauses() const | Gluco::Solver | inline |
| newDecisionLevel() | Gluco::Solver | inlineprotected |
| newVar(bool polarity=true, bool dvar=true) | Gluco::SimpSolver | |
| nFreeVars() const | Gluco::Solver | inline |
| nLearnts() const | Gluco::Solver | inline |
| nRuntimeLimit | Gluco::Solver | |
| nVars() const | Gluco::Solver | inline |
| occurs | Gluco::SimpSolver | protected |
| ok | Gluco::Solver | protected |
| okay() const | Gluco::Solver | inline |
| order_heap | Gluco::Solver | protected |
| parsing | Gluco::SimpSolver | |
| pCnfFunc | Gluco::Solver | |
| pCnfMan | Gluco::Solver | |
| permDiff | Gluco::Solver | protected |
| phase_saving | Gluco::Solver | |
| pickBranchLit() | Gluco::Solver | protected |
| polarity | Gluco::Solver | protected |
| printClause(CRef c) | Gluco::Solver | inline |
| printIncrementalStats() | Gluco::Solver | |
| printInitialClause(CRef c) | Gluco::Solver | inline |
| printLit(Lit l) | Gluco::Solver | inline |
| progress_estimate | Gluco::Solver | protected |
| progressEstimate() const | Gluco::Solver | protected |
| propagate() | Gluco::Solver | protected |
| propagation_budget | Gluco::Solver | protected |
| propagations | Gluco::Solver | |
| pstop | Gluco::Solver | |
| qhead | Gluco::Solver | protected |
| R | Gluco::Solver | |
| random_seed | Gluco::Solver | |
| random_var_freq | Gluco::Solver | |
| reason(Var x) const | Gluco::Solver | inlineprotected |
| rebuildOrderHeap() | Gluco::Solver | protected |
| reduceDB() | Gluco::Solver | protected |
| relocAll(ClauseAllocator &to) | Gluco::SimpSolver | protected |
| remove_satisfied | Gluco::Solver | protected |
| removeClause(CRef cr) | Gluco::SimpSolver | protected |
| removeSatisfied(vec< CRef > &cs) | Gluco::Solver | protected |
| reset() | Gluco::SimpSolver | virtual |
| rnd_decisions | Gluco::Solver | |
| rnd_init_act | Gluco::Solver | |
| rnd_pol | Gluco::Solver | |
| sat_solver_mark_cone(int) | Gluco::Solver | inline |
| sat_solver_set_var_fanin_lit(int, int, int) | Gluco::Solver | inline |
| sat_solver_start_new_round() | Gluco::Solver | inline |
| satisfied(const Clause &c) const | Gluco::Solver | protected |
| search(int nof_conflicts) | Gluco::Solver | protected |
| seen | Gluco::Solver | protected |
| setConfBudget(int64_t x) | Gluco::Solver | inline |
| setDecisionVar(Var v, bool b) | Gluco::Solver | inline |
| setFrozen(Var v, bool b) | Gluco::SimpSolver | inline |
| setIncrementalMode() | Gluco::Solver | |
| setPolarity(Var v, bool b) | Gluco::Solver | inline |
| setPropBudget(int64_t x) | Gluco::Solver | inline |
| showModel | Gluco::Solver | |
| simp_garbage_frac | Gluco::SimpSolver | |
| simpDB_assigns | Gluco::Solver | protected |
| simpDB_props | Gluco::Solver | protected |
| simplify() | Gluco::Solver | |
| SimpSolver() | Gluco::SimpSolver | |
| sizeLBDQueue | Gluco::Solver | |
| sizeTrailQueue | Gluco::Solver | |
| solve(const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false) | Gluco::SimpSolver | inline |
| solve(bool do_simp=true, bool turn_off_simp=false) | Gluco::SimpSolver | inline |
| solve(Lit p, bool do_simp=true, bool turn_off_simp=false) | Gluco::SimpSolver | inline |
| solve(Lit p, Lit q, bool do_simp=true, bool turn_off_simp=false) | Gluco::SimpSolver | inline |
| solve(Lit p, Lit q, Lit r, bool do_simp=true, bool turn_off_simp=false) | Gluco::SimpSolver | inline |
| Gluco::Solver::solve(const vec< Lit > &assumps) | Gluco::Solver | inline |
| Gluco::Solver::solve() | Gluco::Solver | inline |
| Gluco::Solver::solve(Lit p) | Gluco::Solver | inline |
| Gluco::Solver::solve(Lit p, Lit q) | Gluco::Solver | inline |
| Gluco::Solver::solve(Lit p, Lit q, Lit r) | Gluco::Solver | inline |
| solve_(bool do_simp=true, bool turn_off_simp=false) | Gluco::SimpSolver | protected |
| Gluco::Solver::solve_() | Gluco::Solver | protected |
| solveLimited(const vec< Lit > &assumps, bool do_simp=true, bool turn_off_simp=false) | Gluco::SimpSolver | inline |
| Gluco::Solver::solveLimited(const vec< Lit > &assumps) | Gluco::Solver | inline |
| Solver() | Gluco::Solver | |
| SolverType | Gluco::Solver | |
| solves | Gluco::Solver | |
| specialIncReduceDB | Gluco::Solver | |
| starts | Gluco::Solver | |
| strengthenClause(CRef cr, Lit l) | Gluco::SimpSolver | protected |
| substitute(Var v, Lit x) | Gluco::SimpSolver | |
| subsumption_lim | Gluco::SimpSolver | |
| subsumption_queue | Gluco::SimpSolver | protected |
| sumAssumptions | Gluco::Solver | protected |
| sumLBD | Gluco::Solver | protected |
| terminate_search_early | Gluco::Solver | |
| toDimacs(FILE *f, const vec< Lit > &assumps) | Gluco::Solver | |
| toDimacs(const char *file, const vec< Lit > &assumps) | Gluco::Solver | |
| toDimacs(FILE *f, Clause &c, vec< Var > &map, Var &max) | Gluco::Solver | |
| toDimacs(const char *file) | Gluco::Solver | inline |
| toDimacs(const char *file, Lit p) | Gluco::Solver | inline |
| toDimacs(const char *file, Lit p, Lit q) | Gluco::Solver | inline |
| toDimacs(const char *file, Lit p, Lit q, Lit r) | Gluco::Solver | inline |
| tot_literals | Gluco::Solver | |
| totalTime4Sat | Gluco::Solver | protected |
| totalTime4Unsat | Gluco::Solver | protected |
| touched | Gluco::SimpSolver | protected |
| trail | Gluco::Solver | protected |
| trail_lim | Gluco::Solver | protected |
| trailQueue | Gluco::Solver | protected |
| uncheckedEnqueue(Lit p, CRef from=CRef_Undef) | Gluco::Solver | protected |
| updateElimHeap(Var v) | Gluco::SimpSolver | inlineprotected |
| use_asymm | Gluco::SimpSolver | |
| use_elim | Gluco::SimpSolver | |
| use_rcheck | Gluco::SimpSolver | |
| use_simplification | Gluco::SimpSolver | protected |
| user_lits | Gluco::Solver | |
| user_vec | Gluco::Solver | |
| value(Var x) const | Gluco::Solver | inline |
| value(Lit p) const | Gluco::Solver | inline |
| var_decay | Gluco::Solver | |
| var_inc | Gluco::Solver | protected |
| varBumpActivity(Var v, double inc) | Gluco::Solver | inlineprotected |
| varBumpActivity(Var v) | Gluco::Solver | inlineprotected |
| vardata | Gluco::Solver | protected |
| varDecayActivity() | Gluco::Solver | inlineprotected |
| verbEveryConflicts | Gluco::Solver | |
| verbosity | Gluco::Solver | |
| watches | Gluco::Solver | protected |
| watchesBin | Gluco::Solver | protected |
| withinBudget() const | Gluco::Solver | inlineprotected |
| ~SimpSolver() | Gluco::SimpSolver | |
| ~Solver() | Gluco::Solver | virtual |
