CSolver Member List

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

_addedUnitClausesCSolver [protected]
_assignment_hookCSolver [protected]
_assignment_hook_cookieCSolver [protected]
_assignment_stackCSolver [protected]
_clausesCDatabase [protected]
_conflict_litsCSolver [protected]
_conflictsCSolver [protected]
_decision_hookCSolver [protected]
_decision_hook_cookieCSolver [protected]
_deduction_hookCSolver [protected]
_deduction_hook_cookieCSolver [protected]
_dlevelCSolver [protected]
_dlevel_hookCSolver [protected]
_dlevel_hook_cookieCSolver [protected]
_hooksCSolver [protected]
_implication_queueCSolver [protected]
_last_var_lits_countCSolver [protected]
_lit_pool_end_storageCDatabase [protected]
_lit_pool_finishCDatabase [protected]
_lit_pool_startCDatabase [protected]
_max_score_posCSolver [protected]
_mem_limitCDatabase [protected]
_num_markedCSolver [protected]
_num_var_in_new_clCDatabase [protected]
_paramsCSolver [protected]
_statsCSolver [protected]
_unused_clause_idx_queueCDatabase [protected]
_var_orderCSolver [protected]
_variablesCDatabase [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


Generated on Tue Jul 3 14:35:24 2007 for CVC3 by  doxygen 1.5.1