104 for (
unsigned i=0; i<
variables().size(); ++i)
132 for (
unsigned i=0; i<
_hooks.size(); ++i) {
133 pair<int,pair<HookFunPtrT, int> > & hook =
_hooks[i];
135 hook.first += hook.second.second;
136 hook.second.first((
void *)
this);
150 for (
unsigned i=0; i<
variables().size(); ++i)
163 int num_vars = old_num_vars + new_vars;
168 for (
int i=old_num_vars; i<num_vars; ++i) {
181 int n_lits = lits.size();
201 bool satisfied =
false, is_unit =
false,
is_conflict =
false;
203 for (
int i=0; i< n_lits; ++i){
204 int var_idx = lits[i]>>1;
205 if ((
unsigned)var_idx >=
variables().size()) {
208 int var_sign = lits[i]&0x1;
213 if (lit_value == 1) {
216 else if (lit_value != 0) {
221 is_unit = !satisfied && (num_unknown == 1);
225 if (
clause(new_cl).num_lits() > 1) {
227 int max_idx = -1, max_dl = -1;
231 for (i=0; i< sz; ++i) {
253 other_ht_idx = max_idx;
255 max_idx = -1; max_dl = -1;
256 for (i=sz-1; i>=0; --i) {
257 if (i==other_ht_idx )
continue;
298 assert (value == 0 || value == 1);
301 CHECK (cout <<
"Setting\t" << (value>0?
"+":
"-") << v
302 <<
" at " << dl <<
" because " << ante<<
endl;);
313 vector<CLitPoolElement *> & ht_ptrs = var.
ht_ptr(value);
326 for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin(); itr != ht_ptrs.end(); ++itr) {
332 if (ptr->val() <= 0) {
334 cl_idx = - ptr->
val();
343 else if ( the_value != 1)
355 int sign = ptr->var_sign();
360 *itr = ht_ptrs.back();
371 CLitPoolElement * ht_ptr, * other_ht_ptr = NULL, * ptr, * max_ptr = NULL;
374 for (vector <CLitPoolElement *>::iterator itr = ht_ptrs.begin();
375 itr != ht_ptrs.end(); ++itr) {
382 if (ptr->val() <= 0) {
384 cl_idx = - ptr->
val();
392 int sign = max_ptr->var_sign();
395 max_ptr->set_ht(dir);
396 *itr = ht_ptrs.back();
403 else if ( the_value != 1)
419 int v1 = ptr->var_index();
420 int sign = ptr->var_sign();
425 *itr = ht_ptrs.back();
453 for (
int i=0, sz=
clause(cl).num_lits(); i<sz; ++i) {
464 cout <<
"Assignment Stack: ";
465 for (
int i=0; i<=
dlevel(); ++i) {
469 cout <<
"(" <<i <<
":";
473 cout <<
") " <<
endl;
482 for (
int i=0, sz=
clause(cl).num_lits(); i<sz; ++i)
491 for (
int i=0, sz=
clause(cl).num_lits(); i<sz; ++i)
501 for (
int i=0, sz=
clause(cl).num_lits(); i<sz; ++i) {
530 cout <<
"Forced to reduce unrelevance in clause deletion. " <<
endl;
539 itr !=
clauses().end(); ++itr) {
542 int val_0_lits = 0, val_1_lits = 0, unknown_lits = 0;
543 for (
int i=0; i< cl.
num_lits(); ++i) {
545 if (lit_value == 0 ) ++val_0_lits;
546 else if (lit_value == 1) ++val_1_lits;
551 CHECK (cout <<
"Deleting Unrelevant clause: " << cl <<
endl;);
555 (unknown_lits+val_1_lits > 1) ) {
558 CHECK (cout <<
"Deleting too large clause: " << cl <<
endl;);
567 for (vector<CVariable>::iterator itr =
variables().begin();
569 for (
int i=0; i<2; ++i) {
571 vector<CLitPoolElement *> & ht_ptr = (*itr).ht_ptr(i);
572 for (vector<CLitPoolElement *>::iterator my_itr = ht_ptr.begin();
573 my_itr != ht_ptr.end(); ++my_itr) {
574 if ( (*my_itr)->val() <= 0) {
575 *my_itr = ht_ptr.back();
595 const pair<int, int> & v2)
597 if (v1.second > v2.second)
return true;
603 for(
unsigned i=1; i<
variables().size(); ++i) {
629 int s_var = 0, s_var2;
632 unsigned i, var_idx, sign;
648 int skip =random()%(1+randomness);
659 s_var = var_idx + var_idx + sign;
663 if (s_var < 2) done =
true;
699 CHECK (cout <<
"**Decision at Level " <<
dlevel() ;
700 cout <<
": " << s_var <<
"\te.g. " << (s_var&0x1?
"-":
" ") ;
701 cout <<(s_var>>1) <<
endl; );
709 if (!allowNewClauses) {
711 for (
int i=1, sz=
variables().size(); i<sz; ++i) {
714 un_used.push_back(i);
721 cout << un_used.size()<<
" Variables are defined but not used " <<
endl;
723 for (
unsigned i=0; i< un_used.size(); ++i)
724 cout << un_used[i] <<
" ";
729 vector<int> uni_phased;
730 for (
int i=1, sz=
variables().size(); i<sz; ++i) {
736 uni_phased.push_back(-i);
740 uni_phased.push_back(i);
744 cout << uni_phased.size()<<
" Variables only appear in one phase." <<
endl;
746 for (
unsigned i=0; i< uni_phased.size(); ++i)
747 cout << uni_phased[i] <<
" ";
832 CHECK (cout <<
"Back track to " << blevel <<
" ,currently in "<<
dlevel() <<
" level" <<
endl;);
835 assert(blevel <=
dlevel());
836 for (
int i=
dlevel(); i>= blevel; --i) {
838 for (
int j=assignments.size()-1 ; j>=0; --j)
857 int variable_index = literal>>1;
868 the_var = &(
variables()[variable_index]);
872 else if (the_var->
value() == (literal&0x1) ) {
893 int v = (*itr).var_index();
923 vector<ClauseIdx> added_conflict_clauses;
924 for (
int i=0, sz=
_conflicts.size(); i<sz; ++i) {
937 bool first_time =
true;
938 bool prev_is_uip =
false;
942 for (
int j = assignments.size() - 1; j >= 0; --j ) {
943 int assigned = assignments[j];
951 (prev_is_uip ==
false))
953 assert (
variable(assigned>>1).in_new_cl()==-1);
956 if (conflict_cl < 0 ) {
963 added_conflict_clauses.push_back(conflict_cl);
966 cout <<
"**Add Clause " <<conflict_cl<<
" : "<<
clause(conflict_cl) <<
endl;
972 else prev_is_uip =
false;
989 for (
unsigned i=0; i< added_conflict_clauses.size(); ++i) {
990 ClauseIdx cl = added_conflict_clauses[i];
999 for (
int i=0, sz=added_conflict_clauses.size(); i<sz; ++i) {
1000 conflict_cl = added_conflict_clauses[i];
1016 CHECK(cout <<
"Conflict Analasis: conflict at level: " << back_level;
1017 cout <<
" Assertion Clause is " << conflict_cl<<
endl; );
float restart_time_incr_incr
int find_unit_literal(ClauseIdx cl)
int literal_value(CLitPoolElement l)
bool allow_clause_deletion
void set_antecedence(ClauseIdx ante)
int lit_pool_free_space(void)
void set_var_value_not_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)
void mark_clause_deleted(CClause &cl)
int clause_deletion_interval
void delete_unrelevant_clauses(void)
void verify_integrity(void)
int min_num_clause_lits_for_delete
vector< CClause > _clauses
vector< CClause > & clauses(void)
void(* _assignment_hook)(void *, int, int)
int analyze_conflicts(void)
void(* _deduction_hook)(void *)
void unset_var_value(int var)
vector< ClauseIdx > _addedUnitClauses
bool is_conflict(ClauseIdx cl)
int find_max_clause_dlevel(ClauseIdx cl)
void set_in_new_cl(int phase)
void lit_pool_push_back(int value)
CLitPoolElement & literal(int idx)
float restart_time_increment
vector< CVariable > & variables(void)
void back_track(int level)
void init(CLitPoolElement *head, int num_lits)
void run_periodic_functions(void)
CSolverParameters _params
int & var_score_pos(void)
queue< ClauseIdx > _unused_clause_idx_queue
void * _decision_hook_cookie
CVariable & variable(int idx)
CLitPoolElement * lit_pool_end(void)
vector< CLitPoolElement * > & ht_ptr(int i)
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
ClauseIdx get_antecedence(void)
int preprocess(bool allowNewClauses)
void(* _dlevel_hook)(void *, int)
bool allow_multiple_conflict
vector< ClauseIdx > _conflicts
void * _assignment_hook_cookie
queue< pair< int, ClauseIdx > > _implication_queue
int & num_free_variables()
int & num_deleted_literals()
CLitPoolElement * literals(void)
vector< pair< int, int > > _var_order
bool compare_var_stat(const pair< int, int > &v1, const pair< int, int > &v2)
ClauseIdx add_clause(vector< long > &lits, bool addConflicts=true)
bool enlarge_lit_pool(void)
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 set_var_value_with_current_dl(int v, vector< CLitPoolElement * > &neg_ht_clauses)
void mark_vars_at_level(ClauseIdx cl, int var_idx, int dl)
vector< pair< int, pair< HookFunPtrT, int > > > _hooks
bool allow_multiple_conflict_clause
vector< vector< int > * > _assignment_stack
int add_variables(int new_vars)
int conflict_analysis_zchaff(void)
int current_cpu_time(void)
int current_world_time(void)
void * _dlevel_hook_cookie
bool is_satisfied(ClauseIdx cl)
void set_var_value(int var, int value, ClauseIdx ante, int dl)
void update_var_stats(void)
vector< int > _last_var_lits_count[2]
CClause & clause(ClauseIdx idx)
int solve(bool allowNewClauses)
vector< CVariable > _variables
void queue_implication(int lit, ClauseIdx ante_clause)
int & num_deleted_clauses()