CVC3
2.4.1
|
#include <xchaff_solver.h>
Public Attributes | |
float | time_limit |
int | decision_strategy |
int | preprocess_strategy |
bool | allow_clause_deletion |
int | clause_deletion_interval |
int | max_unrelevance |
int | min_num_clause_lits_for_delete |
int | max_conflict_clause_length |
int | bubble_init_step |
int | verbosity |
int | randomness |
bool | allow_restart |
float | next_restart_time |
float | restart_time_increment |
float | restart_time_incr_incr |
int | next_restart_backtrack |
int | restart_backtrack_incr |
int | restart_backtrack_incr_incr |
int | restart_randomness |
int | base_randomness |
bool | back_track_complete |
int | conflict_analysis_method |
bool | allow_multiple_conflict |
bool | allow_multiple_conflict_clause |
Struct**********************************************************************
Synopsis [Sat solver parameters ]
Description []
SeeAlso []
Definition at line 77 of file xchaff_solver.h.
float CSolverParameters::time_limit |
Definition at line 78 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::set_time_limit(), and CSolver::time_out().
int CSolverParameters::decision_strategy |
Definition at line 80 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::set_decision_strategy().
int CSolverParameters::preprocess_strategy |
Definition at line 81 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::set_preprocess_strategy().
bool CSolverParameters::allow_clause_deletion |
Definition at line 83 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::enable_cls_deletion(), and CSolver::run_periodic_functions().
int CSolverParameters::clause_deletion_interval |
Definition at line 84 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::run_periodic_functions(), and CSolver::set_cls_del_interval().
int CSolverParameters::max_unrelevance |
Definition at line 85 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::delete_unrelevant_clauses(), and CSolver::set_max_unrelevance().
int CSolverParameters::min_num_clause_lits_for_delete |
Definition at line 86 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::delete_unrelevant_clauses(), and CSolver::set_min_num_clause_lits_for_delete().
int CSolverParameters::max_conflict_clause_length |
Definition at line 87 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::delete_unrelevant_clauses(), and CSolver::set_max_conflict_clause_length().
int CSolverParameters::bubble_init_step |
Definition at line 88 of file xchaff_solver.h.
Referenced by CSolver::CSolver().
int CSolverParameters::verbosity |
Definition at line 90 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::preprocess(), CSolver::restart(), and CSolver::run_periodic_functions().
int CSolverParameters::randomness |
Definition at line 91 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::decide_next_branch(), and CSolver::run_periodic_functions().
bool CSolverParameters::allow_restart |
Definition at line 93 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
float CSolverParameters::next_restart_time |
Definition at line 94 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
float CSolverParameters::restart_time_increment |
Definition at line 95 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
float CSolverParameters::restart_time_incr_incr |
Definition at line 96 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
int CSolverParameters::next_restart_backtrack |
Definition at line 97 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
int CSolverParameters::restart_backtrack_incr |
Definition at line 98 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
int CSolverParameters::restart_backtrack_incr_incr |
Definition at line 99 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
int CSolverParameters::restart_randomness |
Definition at line 100 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::run_periodic_functions().
int CSolverParameters::base_randomness |
Definition at line 101 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), CSolver::decide_next_branch(), and CSolver::set_randomness().
bool CSolverParameters::back_track_complete |
Definition at line 103 of file xchaff_solver.h.
Referenced by CSolver::conflict_analysis_zchaff(), CSolver::CSolver(), and CSolver::deduce().
int CSolverParameters::conflict_analysis_method |
Definition at line 104 of file xchaff_solver.h.
bool CSolverParameters::allow_multiple_conflict |
Definition at line 105 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::set_allow_multiple_conflict().
bool CSolverParameters::allow_multiple_conflict_clause |
Definition at line 106 of file xchaff_solver.h.
Referenced by CSolver::CSolver(), and CSolver::set_allow_multiple_conflict_clause().