40 #ifndef __SAT_SOLVER__
41 #define __SAT_SOLVER__
44 #include <sys/resource.h>
50 #ifndef __SAT_STATUS__
51 #define __SAT_STATUS__
157 vector<pair<int,pair< HookFunPtrT, int> > >
_hooks;
211 vector<CLitPoolElement *> & neg_ht_clauses);
213 vector<CLitPoolElement*> & neg_ht_clauses);
272 _deduction_hook_cookie = cookie; }
289 getrusage(RUSAGE_SELF, &ru);
290 return ( ru.ru_utime.tv_sec*1000 +
291 ru.ru_utime.tv_usec/1000+
292 ru.ru_stime.tv_sec*1000 +
293 ru.ru_stime.tv_usec/1000 );
299 gettimeofday(&tv,&tz);
300 return (tv.tv_sec * 1000 + tv.tv_usec/1000) ;
331 int mem_assignment = 0;
333 mem_assignment += _assignment_stack[i]->capacity() *
sizeof(int);
334 mem_assignment +=
sizeof(vector<int>)* _assignment_stack.size();
335 return mem_dbase + mem_assignment;
341 pair<HookFunPtrT, int> a(fun, interval);
342 _hooks.push_back(pair<
int, pair<HookFunPtrT, int> > (0, a));
346 CHECK (cout <<
"\t\t\t\t\t\tQueueing " << (lit&0x01?
" -":
" +") << (lit>>1) ;
347 cout <<
" because of " << ante_clause <<
endl; );
348 _implication_queue.push(pair<int, ClauseIdx>(lit, ante_clause));
360 cout <<
"Restarting ... " <<
endl;
363 for (
unsigned i=1; i<
variables().size(); ++i) {
366 _last_var_lits_count[0][i] = 0;
367 _last_var_lits_count[1][i] = 0;
374 int solve(
bool allowNewClauses);
381 void dump(ostream & os = cout ) {
float restart_time_incr_incr
bool allow_clause_deletion
void set_var_value_not_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)
void set_min_num_clause_lits_for_delete(int n)
int clause_deletion_interval
void delete_unrelevant_clauses(void)
void set_max_unrelevance(int n)
void verify_integrity(void)
int min_num_clause_lits_for_delete
void dump(ostream &os=cout)
void(* _assignment_hook)(void *, int, int)
int analyze_conflicts(void)
void(* _deduction_hook)(void *)
void unset_var_value(int var)
void set_cls_del_interval(int n)
void set_mem_limit(int s)
void output_current_stats(void)
vector< ClauseIdx > _addedUnitClauses
void RegisterDecisionHook(int(*f)(void *, bool *), void *cookie)
int find_max_clause_dlevel(ClauseIdx cl)
float restart_time_increment
vector< CVariable > & variables(void)
void back_track(int level)
void set_time_limit(float t)
void run_periodic_functions(void)
CSolverParameters _params
int estimate_mem_usage(void)
void * _decision_hook_cookie
CVariable & variable(int idx)
const char * version(void)
void dump_assignment_stack(ostream &os=cout)
int next_restart_backtrack
CVC3::ExprStream & endl(CVC3::ExprStream &os)
Print the end-of-line.
int(* _decision_hook)(void *, bool *)
void * _deduction_hook_cookie
int preprocess(bool allowNewClauses)
void(* _dlevel_hook)(void *, int)
bool allow_multiple_conflict
void set_mem_limit(int n)
vector< ClauseIdx > _conflicts
void enable_cls_deletion(bool allow)
void * _assignment_hook_cookie
queue< pair< int, ClauseIdx > > _implication_queue
int & num_free_variables()
vector< pair< int, int > > _var_order
ClauseIdx add_clause(vector< long > &lits, bool addConflicts=true)
void set_random_seed(int seed)
void dump(ostream &os=cout)
vector< long > _conflict_lits
int max_conflict_clause_length
bool decide_next_branch(void)
int restart_backtrack_incr
int restart_backtrack_incr_incr
void RegisterDLevelHook(void(*f)(void *, int), void *cookie)
void set_var_value_with_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)
int conflict_analysis_method
void mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)
vector< pair< int, pair< HookFunPtrT, int > > > _hooks
bool allow_multiple_conflict_clause
int conflict_analysis_grasp(void)
vector< vector< int > * > _assignment_stack
int add_variables(int new_vars)
void RegisterDeductionHook(void(*f)(void *), void *cookie)
void set_allow_multiple_conflict_clause(bool b=false)
void RegisterAssignmentHook(void(*f)(void *, int, int), void *cookie)
int conflict_analysis_zchaff(void)
void set_randomness(int n)
int current_cpu_time(void)
long total_bubble_move(void)
int current_world_time(void)
void * _dlevel_hook_cookie
void add_hook(HookFunPtrT fun, int interval)
void(* HookFunPtrT)(void *)
void set_var_value(int var, int value, ClauseIdx ante, int dl)
void update_var_stats(void)
vector< int > _last_var_lits_count[2]
void set_allow_multiple_conflict(bool b=false)
void set_preprocess_strategy(int s)
void set_decision_strategy(int s)
int solve(bool allowNewClauses)
void queue_implication(int lit, ClauseIdx ante_clause)
void set_max_conflict_clause_length(int l)