CSolver Member List

This is the complete list of members for CSolver, 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< int > &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

---