Searched refs:queue_implication (Results 1 – 2 of 2) sorted by relevance
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | xchaff_solver.cpp | 287 queue_implication(lit, new_cl); in add_clause()
344 queue_implication (other_ht_ptr->s_var(), cl_idx); in set_var_value_with_current_dl()
404 queue_implication (other_ht_ptr->s_var(), cl_idx); in set_var_value_not_current_dl()
702 queue_implication(s_var, NULL_CLAUSE); in decide_next_branch()
735 queue_implication( i+i+1, NULL_CLAUSE); in preprocess()
739 queue_implication( i+i, NULL_CLAUSE); in preprocess()
755 queue_implication(find_unit_literal(i), i); in preprocess()
781 queue_implication(lit, cl); in real_solve()
1003 queue_implication(lit, conflict_cl); in conflict_analysis_zchaff()
|
| H A D | xchaff_solver.h | 345 void queue_implication (int lit, ClauseIdx ante_clause) { in queue_implication() function
|