CVC3  2.4.1
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
CSolver Class Reference

#include <xchaff_solver.h>

Inheritance diagram for CSolver:
CDatabase

Public Member Functions

 CSolver ()
 
 ~CSolver ()
 
void set_time_limit (float t)
 
void set_mem_limit (int s)
 
void set_decision_strategy (int s)
 
void set_preprocess_strategy (int s)
 
void enable_cls_deletion (bool allow)
 
void set_cls_del_interval (int n)
 
void set_max_unrelevance (int n)
 
void set_min_num_clause_lits_for_delete (int n)
 
void set_max_conflict_clause_length (int l)
 
void set_allow_multiple_conflict (bool b=false)
 
void set_allow_multiple_conflict_clause (bool b=false)
 
void set_randomness (int n)
 
void set_random_seed (int seed)
 
void RegisterDLevelHook (void(*f)(void *, int), void *cookie)
 
void RegisterDecisionHook (int(*f)(void *, bool *), void *cookie)
 
void RegisterAssignmentHook (void(*f)(void *, int, int), void *cookie)
 
void RegisterDeductionHook (void(*f)(void *), void *cookie)
 
int outcome ()
 
int num_decisions ()
 
int & num_free_variables ()
 
int max_dlevel ()
 
int num_implications ()
 
long total_bubble_move (void)
 
const char * version (void)
 
int current_cpu_time (void)
 
int current_world_time (void)
 
float elapsed_cpu_time ()
 
float total_run_time ()
 
float cpu_run_time ()
 
float world_run_time ()
 
int estimate_mem_usage ()
 
int mem_usage (void)
 
int & dlevel ()
 
void add_hook (HookFunPtrT fun, int interval)
 
void queue_implication (int lit, ClauseIdx ante_clause)
 
int add_variables (int new_vars)
 
ClauseIdx add_clause (vector< long > &lits, bool addConflicts=true)
 
void verify_integrity (void)
 
void restart (void)
 
int solve (bool allowNewClauses)
 
int continueCheck ()
 
void dump_assignment_stack (ostream &os=cout)
 
void output_current_stats (void)
 
void dump (ostream &os=cout)
 
- Public Member Functions inherited from CDatabase
 CDatabase ()
 
 ~CDatabase ()
 
void init (void)
 
vector< CVariable > & variables (void)
 
vector< CClause > & clauses (void)
 
CVariablevariable (int idx)
 
CClauseclause (ClauseIdx idx)
 
CDatabaseStatsstats (void)
 
void set_mem_limit (int n)
 
int & init_num_clauses ()
 
int & init_num_literals ()
 
int & num_added_clauses ()
 
int & num_added_literals ()
 
int & num_deleted_clauses ()
 
int & num_deleted_literals ()
 
CLitPoolElementlit_pool_begin (void)
 
CLitPoolElementlit_pool_end (void)
 
void lit_pool_push_back (int value)
 
int lit_pool_size (void)
 
int lit_pool_free_space (void)
 
CLitPoolElementlit_pool (int i)
 
void output_lit_pool_state (void)
 
bool enlarge_lit_pool (void)
 
void compact_lit_pool (void)
 
int estimate_mem_usage (void)
 
int mem_usage (void)
 
void set_variable_number (int n)
 
int add_variable (void)
 
int num_variables (void)
 
int num_clauses (void)
 
int num_literals (void)
 
void mark_clause_deleted (CClause &cl)
 
void mark_var_in_new_cl (int v_idx, int phase)
 
int literal_value (CLitPoolElement l)
 
int find_unit_literal (ClauseIdx cl)
 
bool is_conflict (ClauseIdx cl)
 
bool is_satisfied (ClauseIdx cl)
 
void detail_dump_cl (ClauseIdx cl_idx, ostream &os=cout)
 
void dump (ostream &os=cout)
 

Protected Member Functions

void real_solve (void)
 
int preprocess (bool allowNewClauses)
 
int deduce (void)
 
bool decide_next_branch (void)
 
int analyze_conflicts (void)
 
int conflict_analysis_grasp (void)
 
int conflict_analysis_zchaff (void)
 
void back_track (int level)
 
void init (void)
 
void mark_vars_at_level (ClauseIdx cl, int var_idx, int dl)
 
int find_max_clause_dlevel (ClauseIdx cl)
 
void set_var_value (int var, int value, ClauseIdx ante, int dl)
 
void set_var_value_not_current_dl (int v, vector< CLitPoolElement * > &neg_ht_clauses)
 
void set_var_value_with_current_dl (int v, vector< CLitPoolElement * > &neg_ht_clauses)
 
void unset_var_value (int var)
 
void run_periodic_functions (void)
 
void update_var_stats (void)
 
bool time_out (void)
 
void delete_unrelevant_clauses (void)
 

Protected Attributes

int _dlevel
 
vector< vector< int > * > _assignment_stack
 
queue< pair< int, ClauseIdx > > _implication_queue
 
CSolverParameters _params
 
CSolverStats _stats
 
vector< pair< int, pair
< HookFunPtrT, int > > > 
_hooks
 
int _max_score_pos
 
vector< int > _last_var_lits_count [2]
 
vector< pair< int, int > > _var_order
 
int _num_marked
 
vector< ClauseIdx_conflicts
 
vector< long > _conflict_lits
 
void(* _dlevel_hook )(void *, int)
 
int(* _decision_hook )(void *, bool *)
 
void(* _assignment_hook )(void *, int, int)
 
void(* _deduction_hook )(void *)
 
void * _dlevel_hook_cookie
 
void * _decision_hook_cookie
 
void * _assignment_hook_cookie
 
void * _deduction_hook_cookie
 
vector< ClauseIdx_addedUnitClauses
 
- Protected Attributes inherited from CDatabase
CDatabaseStats _stats
 
CLitPoolElement_lit_pool_start
 
CLitPoolElement_lit_pool_finish
 
CLitPoolElement_lit_pool_end_storage
 
vector< CVariable_variables
 
vector< CClause_clauses
 
queue< ClauseIdx_unused_clause_idx_queue
 
int _num_var_in_new_cl
 
int _mem_limit
 

Detailed Description

Class**********************************************************************

Synopsis [Sat Solver]

Description [This class contains the process and datastructrues to solve the Sat problem.]

SeeAlso []

Definition at line 148 of file xchaff_solver.h.

Constructor & Destructor Documentation

CSolver::CSolver ( void  )

Definition at line 43 of file xchaff_solver.cpp.

References _assignment_hook, _decision_hook, _deduction_hook, _dlevel, _dlevel_hook, _num_marked, _params, _stats, CSolverParameters::allow_clause_deletion, CSolverParameters::allow_multiple_conflict, CSolverParameters::allow_multiple_conflict_clause, CSolverParameters::allow_restart, CSolverParameters::back_track_complete, CSolverParameters::base_randomness, CSolverParameters::bubble_init_step, CSolverParameters::clause_deletion_interval, CSolverParameters::decision_strategy, dlevel(), CSolverStats::finish_cpu_time, CSolverStats::finish_world_time, CSolverStats::is_mem_out, CSolverStats::is_solver_started, CSolverStats::last_cpu_time, CSolverParameters::max_conflict_clause_length, CSolverStats::max_dlevel, CSolverParameters::max_unrelevance, CSolverParameters::min_num_clause_lits_for_delete, CSolverParameters::next_restart_backtrack, CSolverParameters::next_restart_time, CSolverStats::num_backtracks, CSolverStats::num_decisions, CSolverStats::num_implications, CSolverStats::outcome, CSolverParameters::preprocess_strategy, CSolverParameters::randomness, CSolverParameters::restart_backtrack_incr, CSolverParameters::restart_backtrack_incr_incr, CSolverParameters::restart_randomness, CSolverParameters::restart_time_incr_incr, CSolverParameters::restart_time_increment, CSolverStats::start_cpu_time, CSolverStats::start_world_time, CSolverParameters::time_limit, CSolverStats::total_bubble_move, UNKNOWN, and CSolverParameters::verbosity.

CSolver::~CSolver ( )

Member Function Documentation

void CSolver::real_solve ( void  )
protected
int CSolver::preprocess ( bool  allowNewClauses)
protected
int CSolver::deduce ( void  )
protected
bool CSolver::decide_next_branch ( void  )
protected
int CSolver::analyze_conflicts ( void  )
protected

Definition at line 912 of file xchaff_solver.cpp.

References conflict_analysis_zchaff().

Referenced by real_solve().

int CSolver::conflict_analysis_grasp ( void  )
protected
int CSolver::conflict_analysis_zchaff ( void  )
protected
void CSolver::back_track ( int  level)
protected
void CSolver::init ( void  )
protected
void CSolver::mark_vars_at_level ( ClauseIdx  cl,
int  var_idx,
int  dl 
)
protected
int CSolver::find_max_clause_dlevel ( ClauseIdx  cl)
protected
void CSolver::set_var_value ( int  var,
int  value,
ClauseIdx  ante,
int  dl 
)
protected
void CSolver::set_var_value_not_current_dl ( int  v,
vector< CLitPoolElement * > &  neg_ht_clauses 
)
protected
void CSolver::set_var_value_with_current_dl ( int  v,
vector< CLitPoolElement * > &  neg_ht_clauses 
)
protected
void CSolver::unset_var_value ( int  var)
protected
void CSolver::run_periodic_functions ( void  )
protected
void CSolver::update_var_stats ( void  )
protected
bool CSolver::time_out ( void  )
protected
void CSolver::delete_unrelevant_clauses ( void  )
protected
void CSolver::set_time_limit ( float  t)
inline

Definition at line 228 of file xchaff_solver.h.

References _params, and CSolverParameters::time_limit.

Referenced by Xchaff::SetBudget().

void CSolver::set_mem_limit ( int  s)
inline

Definition at line 230 of file xchaff_solver.h.

References CDatabase::set_mem_limit().

Referenced by Xchaff::SetMemLimit().

void CSolver::set_decision_strategy ( int  s)
inline

Definition at line 233 of file xchaff_solver.h.

References _params, and CSolverParameters::decision_strategy.

void CSolver::set_preprocess_strategy ( int  s)
inline

Definition at line 235 of file xchaff_solver.h.

References _params, and CSolverParameters::preprocess_strategy.

void CSolver::enable_cls_deletion ( bool  allow)
inline
void CSolver::set_cls_del_interval ( int  n)
inline

Definition at line 239 of file xchaff_solver.h.

References _params, and CSolverParameters::clause_deletion_interval.

void CSolver::set_max_unrelevance ( int  n)
inline

Definition at line 241 of file xchaff_solver.h.

References _params, and CSolverParameters::max_unrelevance.

void CSolver::set_min_num_clause_lits_for_delete ( int  n)
inline

Definition at line 243 of file xchaff_solver.h.

References _params, and CSolverParameters::min_num_clause_lits_for_delete.

void CSolver::set_max_conflict_clause_length ( int  l)
inline

Definition at line 245 of file xchaff_solver.h.

References _params, and CSolverParameters::max_conflict_clause_length.

void CSolver::set_allow_multiple_conflict ( bool  b = false)
inline

Definition at line 247 of file xchaff_solver.h.

References _params, and CSolverParameters::allow_multiple_conflict.

void CSolver::set_allow_multiple_conflict_clause ( bool  b = false)
inline

Definition at line 250 of file xchaff_solver.h.

References _params, and CSolverParameters::allow_multiple_conflict_clause.

void CSolver::set_randomness ( int  n)
inline

Definition at line 253 of file xchaff_solver.h.

References _params, and CSolverParameters::base_randomness.

Referenced by Xchaff::SetRandomness().

void CSolver::set_random_seed ( int  seed)
inline

Definition at line 256 of file xchaff_solver.h.

References current_world_time().

Referenced by Xchaff::SetRandSeed().

void CSolver::RegisterDLevelHook ( void(*)(void *, int)  f,
void *  cookie 
)
inline

Definition at line 264 of file xchaff_solver.h.

References _dlevel_hook, and _dlevel_hook_cookie.

Referenced by Xchaff::RegisterDLevelHook().

void CSolver::RegisterDecisionHook ( int(*)(void *, bool *)  f,
void *  cookie 
)
inline

Definition at line 266 of file xchaff_solver.h.

References _decision_hook, and _decision_hook_cookie.

Referenced by Xchaff::RegisterDecisionHook().

void CSolver::RegisterAssignmentHook ( void(*)(void *, int, int)  f,
void *  cookie 
)
inline

Definition at line 268 of file xchaff_solver.h.

References _assignment_hook, and _assignment_hook_cookie.

Referenced by Xchaff::RegisterAssignmentHook().

void CSolver::RegisterDeductionHook ( void(*)(void *)  f,
void *  cookie 
)
inline

Definition at line 270 of file xchaff_solver.h.

References _deduction_hook, and _deduction_hook_cookie.

Referenced by Xchaff::RegisterDeductionHook().

int CSolver::outcome ( )
inline

Definition at line 274 of file xchaff_solver.h.

References _stats, and CSolverStats::outcome.

int CSolver::num_decisions ( )
inline

Definition at line 275 of file xchaff_solver.h.

References _stats, and CSolverStats::num_decisions.

Referenced by Xchaff::GetNumDecisions().

int& CSolver::num_free_variables ( )
inline
int CSolver::max_dlevel ( )
inline

Definition at line 279 of file xchaff_solver.h.

References _stats, and CSolverStats::max_dlevel.

Referenced by conflict_analysis_zchaff(), and Xchaff::GetMaxDLevel().

int CSolver::num_implications ( )
inline

Definition at line 280 of file xchaff_solver.h.

References _stats, and CSolverStats::num_implications.

Referenced by Xchaff::GetNumImplications().

long CSolver::total_bubble_move ( void  )
inline

Definition at line 281 of file xchaff_solver.h.

References _stats, and CSolverStats::total_bubble_move.

const char* CSolver::version ( void  )
inline

Definition at line 283 of file xchaff_solver.h.

int CSolver::current_cpu_time ( void  )
inline
int CSolver::current_world_time ( void  )
inline

Definition at line 296 of file xchaff_solver.h.

Referenced by continueCheck(), init(), set_random_seed(), and solve().

float CSolver::elapsed_cpu_time ( )
inline

Definition at line 303 of file xchaff_solver.h.

References _stats, current_cpu_time(), and CSolverStats::last_cpu_time.

float CSolver::total_run_time ( )
inline
float CSolver::cpu_run_time ( )
inline
float CSolver::world_run_time ( )
inline
int CSolver::estimate_mem_usage ( void  )
inline

Definition at line 326 of file xchaff_solver.h.

References CDatabase::estimate_mem_usage().

Referenced by Xchaff::GetMemUsed().

int CSolver::mem_usage ( void  )
inline
int& CSolver::dlevel ( void  )
inline
void CSolver::add_hook ( HookFunPtrT  fun,
int  interval 
)
inline

Definition at line 340 of file xchaff_solver.h.

References _hooks.

void CSolver::queue_implication ( int  lit,
ClauseIdx  ante_clause 
)
inline
int CSolver::add_variables ( int  new_vars)
ClauseIdx CSolver::add_clause ( vector< long > &  lits,
bool  addConflicts = true 
)
void CSolver::verify_integrity ( void  )

Definition at line 886 of file xchaff_solver.cpp.

Referenced by back_track(), deduce(), and set_var_value().

void CSolver::restart ( void  )
inline
int CSolver::solve ( bool  allowNewClauses)
int CSolver::continueCheck ( )
void CSolver::dump_assignment_stack ( ostream &  os = cout)
void CSolver::output_current_stats ( void  )
void CSolver::dump ( ostream &  os = cout)
inline

Member Data Documentation

int CSolver::_dlevel
protected

Definition at line 151 of file xchaff_solver.h.

Referenced by CSolver(), and dlevel().

vector<vector<int> *> CSolver::_assignment_stack
protected
queue<pair<int,ClauseIdx> > CSolver::_implication_queue
protected
CSolverParameters CSolver::_params
protected
CSolverStats CSolver::_stats
protected
vector<pair<int,pair< HookFunPtrT, int> > > CSolver::_hooks
protected

Definition at line 157 of file xchaff_solver.h.

Referenced by add_hook(), and run_periodic_functions().

int CSolver::_max_score_pos
protected

Definition at line 160 of file xchaff_solver.h.

Referenced by decide_next_branch(), unset_var_value(), and update_var_stats().

vector<int> CSolver::_last_var_lits_count[2]
protected

Definition at line 161 of file xchaff_solver.h.

Referenced by add_variables(), init(), restart(), and update_var_stats().

vector<pair<int,int> > CSolver::_var_order
protected

Definition at line 162 of file xchaff_solver.h.

Referenced by add_variables(), decide_next_branch(), init(), and update_var_stats().

int CSolver::_num_marked
protected

Definition at line 165 of file xchaff_solver.h.

Referenced by conflict_analysis_zchaff(), CSolver(), and mark_vars_at_level().

vector<ClauseIdx> CSolver::_conflicts
protected
vector<long> CSolver::_conflict_lits
protected

Definition at line 167 of file xchaff_solver.h.

Referenced by conflict_analysis_zchaff(), and mark_vars_at_level().

void(* CSolver::_dlevel_hook)(void *, int)
protected

Definition at line 170 of file xchaff_solver.h.

Referenced by back_track(), CSolver(), decide_next_branch(), RegisterDLevelHook(), and solve().

int(* CSolver::_decision_hook)(void *, bool *)
protected

Definition at line 171 of file xchaff_solver.h.

Referenced by CSolver(), decide_next_branch(), and RegisterDecisionHook().

void(* CSolver::_assignment_hook)(void *, int, int)
protected

Definition at line 172 of file xchaff_solver.h.

Referenced by CSolver(), RegisterAssignmentHook(), set_var_value(), and unset_var_value().

void(* CSolver::_deduction_hook)(void *)
protected

Definition at line 173 of file xchaff_solver.h.

Referenced by CSolver(), deduce(), and RegisterDeductionHook().

void* CSolver::_dlevel_hook_cookie
protected

Definition at line 174 of file xchaff_solver.h.

Referenced by back_track(), decide_next_branch(), RegisterDLevelHook(), and solve().

void* CSolver::_decision_hook_cookie
protected

Definition at line 175 of file xchaff_solver.h.

Referenced by decide_next_branch(), and RegisterDecisionHook().

void* CSolver::_assignment_hook_cookie
protected

Definition at line 176 of file xchaff_solver.h.

Referenced by RegisterAssignmentHook(), set_var_value(), and unset_var_value().

void* CSolver::_deduction_hook_cookie
protected

Definition at line 177 of file xchaff_solver.h.

Referenced by deduce(), and RegisterDeductionHook().

vector<ClauseIdx> CSolver::_addedUnitClauses
protected

Definition at line 180 of file xchaff_solver.h.

Referenced by add_clause(), and real_solve().


The documentation for this class was generated from the following files: