, including all inherited members.
| _addedUnitClauses | CSolver | [protected] |
| _assignment_hook | CSolver | [protected] |
| _assignment_hook_cookie | CSolver | [protected] |
| _assignment_stack | CSolver | [protected] |
| _clauses | CDatabase | [protected] |
| _conflict_lits | CSolver | [protected] |
| _conflicts | CSolver | [protected] |
| _decision_hook | CSolver | [protected] |
| _decision_hook_cookie | CSolver | [protected] |
| _deduction_hook | CSolver | [protected] |
| _deduction_hook_cookie | CSolver | [protected] |
| _dlevel | CSolver | [protected] |
| _dlevel_hook | CSolver | [protected] |
| _dlevel_hook_cookie | CSolver | [protected] |
| _hooks | CSolver | [protected] |
| _implication_queue | CSolver | [protected] |
| _last_var_lits_count | CSolver | [protected] |
| _lit_pool_end_storage | CDatabase | [protected] |
| _lit_pool_finish | CDatabase | [protected] |
| _lit_pool_start | CDatabase | [protected] |
| _max_score_pos | CSolver | [protected] |
| _mem_limit | CDatabase | [protected] |
| _num_marked | CSolver | [protected] |
| _num_var_in_new_cl | CDatabase | [protected] |
| _params | CSolver | [protected] |
| _stats | CSolver | [protected] |
| _unused_clause_idx_queue | CDatabase | [protected] |
| _var_order | CSolver | [protected] |
| _variables | CDatabase | [protected] |
| add_clause(vector< long > &lits, bool addConflicts=true) | CSolver | |
| add_hook(HookFunPtrT fun, int interval) | CSolver | [inline] |
| add_variable(void) | CDatabase | [inline] |
| add_variables(int new_vars) | CSolver | |
| analyze_conflicts(void) | CSolver | [protected] |
| back_track(int level) | CSolver | [protected] |
| CDatabase() | CDatabase | |
| clause(ClauseIdx idx) | CDatabase | [inline] |
| clauses(void) | CDatabase | [inline] |
| compact_lit_pool(void) | CDatabase | |
| conflict_analysis_grasp(void) | CSolver | [protected] |
| conflict_analysis_zchaff(void) | CSolver | [protected] |
| continueCheck() | CSolver | |
| cpu_run_time() | CSolver | [inline] |
| CSolver() | CSolver | |
| current_cpu_time(void) | CSolver | [inline] |
| current_world_time(void) | CSolver | [inline] |
| decide_next_branch(void) | CSolver | [protected] |
| deduce(void) | CSolver | [protected] |
| delete_unrelevant_clauses(void) | CSolver | [protected] |
| detail_dump_cl(ClauseIdx cl_idx, ostream &os=cout) | CDatabase | |
| dlevel() | CSolver | [inline] |
| dump(ostream &os=cout) | CSolver | [inline] |
| dump_assignment_stack(ostream &os=cout) | CSolver | |
| elapsed_cpu_time() | CSolver | [inline] |
| enable_cls_deletion(bool allow) | CSolver | [inline] |
| enlarge_lit_pool(void) | CDatabase | |
| estimate_mem_usage() | CSolver | [inline] |
| find_max_clause_dlevel(ClauseIdx cl) | CSolver | [protected] |
| find_unit_literal(ClauseIdx cl) | CDatabase | |
| init(void) | CSolver | [protected] |
| init_num_clauses() | CDatabase | [inline] |
| init_num_literals() | CDatabase | [inline] |
| is_conflict(ClauseIdx cl) | CDatabase | |
| is_satisfied(ClauseIdx cl) | CDatabase | |
| lit_pool(int i) | CDatabase | [inline] |
| lit_pool_begin(void) | CDatabase | [inline] |
| lit_pool_end(void) | CDatabase | [inline] |
| lit_pool_free_space(void) | CDatabase | [inline] |
| lit_pool_push_back(int value) | CDatabase | [inline] |
| lit_pool_size(void) | CDatabase | [inline] |
| literal_value(CLitPoolElement l) | CDatabase | [inline] |
| mark_clause_deleted(CClause &cl) | CDatabase | [inline] |
| mark_var_in_new_cl(int v_idx, int phase) | CDatabase | [inline] |
| mark_vars_at_level(ClauseIdx cl, int var_idx, int dl) | CSolver | [protected] |
| max_dlevel() | CSolver | [inline] |
| mem_usage(void) | CSolver | [inline] |
| num_added_clauses() | CDatabase | [inline] |
| num_added_literals() | CDatabase | [inline] |
| num_clauses(void) | CDatabase | [inline] |
| num_decisions() | CSolver | [inline] |
| num_deleted_clauses() | CDatabase | [inline] |
| num_deleted_literals() | CDatabase | [inline] |
| num_free_variables() | CSolver | [inline] |
| num_implications() | CSolver | [inline] |
| num_literals(void) | CDatabase | [inline] |
| num_variables(void) | CDatabase | [inline] |
| outcome() | CSolver | [inline] |
| output_current_stats(void) | CSolver | |
| output_lit_pool_state(void) | CDatabase | |
| preprocess(bool allowNewClauses) | CSolver | [protected] |
| queue_implication(int lit, ClauseIdx ante_clause) | CSolver | [inline] |
| real_solve(void) | CSolver | [protected] |
| RegisterAssignmentHook(void(*f)(void *, int, int), void *cookie) | CSolver | [inline] |
| RegisterDecisionHook(int(*f)(void *, bool *), void *cookie) | CSolver | [inline] |
| RegisterDeductionHook(void(*f)(void *), void *cookie) | CSolver | [inline] |
| RegisterDLevelHook(void(*f)(void *, int), void *cookie) | CSolver | [inline] |
| restart(void) | CSolver | [inline] |
| run_periodic_functions(void) | CSolver | [protected] |
| set_allow_multiple_conflict(bool b=false) | CSolver | [inline] |
| set_allow_multiple_conflict_clause(bool b=false) | CSolver | [inline] |
| set_cls_del_interval(int n) | CSolver | [inline] |
| set_decision_strategy(int s) | CSolver | [inline] |
| set_max_conflict_clause_length(int l) | CSolver | [inline] |
| set_max_unrelevance(int n) | CSolver | [inline] |
| set_mem_limit(int s) | CSolver | [inline] |
| set_min_num_clause_lits_for_delete(int n) | CSolver | [inline] |
| set_preprocess_strategy(int s) | CSolver | [inline] |
| set_random_seed(int seed) | CSolver | [inline] |
| set_randomness(int n) | CSolver | [inline] |
| set_time_limit(float t) | CSolver | [inline] |
| set_var_value(int var, int value, ClauseIdx ante, int dl) | CSolver | [protected] |
| set_var_value_not_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses) | CSolver | [protected] |
| set_var_value_with_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses) | CSolver | [protected] |
| set_variable_number(int n) | CDatabase | [inline] |
| solve(bool allowNewClauses) | CSolver | |
| stats(void) | CDatabase | [inline] |
| time_out(void) | CSolver | [protected] |
| total_bubble_move(void) | CSolver | [inline] |
| total_run_time() | CSolver | [inline] |
| unset_var_value(int var) | CSolver | [protected] |
| update_var_stats(void) | CSolver | [protected] |
| variable(int idx) | CDatabase | [inline] |
| variables(void) | CDatabase | [inline] |
| verify_integrity(void) | CSolver | |
| version(void) | CSolver | [inline] |
| world_run_time() | CSolver | [inline] |
| ~CDatabase() | CDatabase | [inline] |
| ~CSolver() | CSolver | |
