CVC3
CSolver Member List

This is the complete list of members for CSolver, including all inherited members.

_addedUnitClausesCSolverprotected
_assignment_hookCSolverprotected
_assignment_hook_cookieCSolverprotected
_assignment_stackCSolverprotected
_clausesCDatabaseprotected
_conflict_litsCSolverprotected
_conflictsCSolverprotected
_decision_hookCSolverprotected
_decision_hook_cookieCSolverprotected
_deduction_hookCSolverprotected
_deduction_hook_cookieCSolverprotected
_dlevelCSolverprotected
_dlevel_hookCSolverprotected
_dlevel_hook_cookieCSolverprotected
_hooksCSolverprotected
_implication_queueCSolverprotected
_last_var_lits_countCSolverprotected
_lit_pool_end_storageCDatabaseprotected
_lit_pool_finishCDatabaseprotected
_lit_pool_startCDatabaseprotected
_max_score_posCSolverprotected
_mem_limitCDatabaseprotected
_num_markedCSolverprotected
_num_var_in_new_clCDatabaseprotected
_paramsCSolverprotected
_statsCSolverprotected
_unused_clause_idx_queueCDatabaseprotected
_var_orderCSolverprotected
_variablesCDatabaseprotected
add_clause(vector< long > &lits, bool addConflicts=true)CSolver
add_hook(HookFunPtrT fun, int interval)CSolverinline
add_variable(void)CDatabaseinline
add_variables(int new_vars)CSolver
analyze_conflicts(void)CSolverprotected
back_track(int level)CSolverprotected
CDatabase()CDatabase
clause(ClauseIdx idx)CDatabaseinline
clauses(void)CDatabaseinline
compact_lit_pool(void)CDatabase
conflict_analysis_grasp(void)CSolverprotected
conflict_analysis_zchaff(void)CSolverprotected
continueCheck()CSolver
cpu_run_time()CSolverinline
CSolver()CSolver
current_cpu_time(void)CSolverinline
current_world_time(void)CSolverinline
decide_next_branch(void)CSolverprotected
deduce(void)CSolverprotected
delete_unrelevant_clauses(void)CSolverprotected
detail_dump_cl(ClauseIdx cl_idx, ostream &os=cout)CDatabase
dlevel()CSolverinline
dump(ostream &os=cout)CSolverinline
dump_assignment_stack(ostream &os=cout)CSolver
elapsed_cpu_time()CSolverinline
enable_cls_deletion(bool allow)CSolverinline
enlarge_lit_pool(void)CDatabase
estimate_mem_usage()CSolverinline
find_max_clause_dlevel(ClauseIdx cl)CSolverprotected
find_unit_literal(ClauseIdx cl)CDatabase
init(void)CSolverprotected
init_num_clauses()CDatabaseinline
init_num_literals()CDatabaseinline
is_conflict(ClauseIdx cl)CDatabase
is_satisfied(ClauseIdx cl)CDatabase
lit_pool(int i)CDatabaseinline
lit_pool_begin(void)CDatabaseinline
lit_pool_end(void)CDatabaseinline
lit_pool_free_space(void)CDatabaseinline
lit_pool_push_back(int value)CDatabaseinline
lit_pool_size(void)CDatabaseinline
literal_value(CLitPoolElement l)CDatabaseinline
mark_clause_deleted(CClause &cl)CDatabaseinline
mark_var_in_new_cl(int v_idx, int phase)CDatabaseinline
mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)CSolverprotected
max_dlevel()CSolverinline
mem_usage(void)CSolverinline
num_added_clauses()CDatabaseinline
num_added_literals()CDatabaseinline
num_clauses(void)CDatabaseinline
num_decisions()CSolverinline
num_deleted_clauses()CDatabaseinline
num_deleted_literals()CDatabaseinline
num_free_variables()CSolverinline
num_implications()CSolverinline
num_literals(void)CDatabaseinline
num_variables(void)CDatabaseinline
outcome()CSolverinline
output_current_stats(void)CSolver
output_lit_pool_state(void)CDatabase
preprocess(bool allowNewClauses)CSolverprotected
queue_implication(int lit, ClauseIdx ante_clause)CSolverinline
real_solve(void)CSolverprotected
RegisterAssignmentHook(void(*f)(void *, int, int), void *cookie)CSolverinline
RegisterDecisionHook(int(*f)(void *, bool *), void *cookie)CSolverinline
RegisterDeductionHook(void(*f)(void *), void *cookie)CSolverinline
RegisterDLevelHook(void(*f)(void *, int), void *cookie)CSolverinline
restart(void)CSolverinline
run_periodic_functions(void)CSolverprotected
set_allow_multiple_conflict(bool b=false)CSolverinline
set_allow_multiple_conflict_clause(bool b=false)CSolverinline
set_cls_del_interval(int n)CSolverinline
set_decision_strategy(int s)CSolverinline
set_max_conflict_clause_length(int l)CSolverinline
set_max_unrelevance(int n)CSolverinline
set_mem_limit(int s)CSolverinline
set_min_num_clause_lits_for_delete(int n)CSolverinline
set_preprocess_strategy(int s)CSolverinline
set_random_seed(int seed)CSolverinline
set_randomness(int n)CSolverinline
set_time_limit(float t)CSolverinline
set_var_value(int var, int value, ClauseIdx ante, int dl)CSolverprotected
set_var_value_not_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)CSolverprotected
set_var_value_with_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)CSolverprotected
set_variable_number(int n)CDatabaseinline
solve(bool allowNewClauses)CSolver
stats(void)CDatabaseinline
time_out(void)CSolverprotected
total_bubble_move(void)CSolverinline
total_run_time()CSolverinline
unset_var_value(int var)CSolverprotected
update_var_stats(void)CSolverprotected
variable(int idx)CDatabaseinline
variables(void)CDatabaseinline
verify_integrity(void)CSolver
version(void)CSolverinline
world_run_time()CSolverinline
~CDatabase()CDatabaseinline
~CSolver()CSolver