Searched refs:_conflict_lits (Results 1 – 2 of 2) sorted by relevance
906 _conflict_lits.push_back((*itr).s_var()); in mark_vars_at_level()930 while (_conflict_lits.size()) { in conflict_analysis_zchaff()931 CVariable & var = variable(_conflict_lits.back() >> 1); in conflict_analysis_zchaff()932 _conflict_lits.pop_back(); in conflict_analysis_zchaff()954 _conflict_lits.push_back(assigned^0x1); // add this assignment's reverse, e.g. UIP in conflict_analysis_zchaff()955 int conflict_cl = add_clause(_conflict_lits, false); in conflict_analysis_zchaff()962 _conflict_lits.pop_back(); // remove for continue use of _conflict_lits in conflict_analysis_zchaff()1009 while (_conflict_lits.size()) { in conflict_analysis_zchaff()1010 CVariable & var = variable(_conflict_lits.back() >> 1); in conflict_analysis_zchaff()1011 _conflict_lits.pop_back(); in conflict_analysis_zchaff()
167 vector<long> _conflict_lits; //used when constructing conflict clauses variable