Lines Matching refs:get_wlist
67 … CTRACE("sat_ter_watch_bug", !contains_watched(s.get_wlist(~c[0]), c[1], c[2]), tout << c << "\n"; in check_clause()
69 s.display_watch_list(tout, s.get_wlist(~c[0])); in check_clause()
71 VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2])); in check_clause()
72 VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2])); in check_clause()
73 VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1])); in check_clause()
97 VERIFY(contains_watched(s.get_wlist(~c[0]), c, s.get_offset(c))); in check_clause()
98 VERIFY(contains_watched(s.get_wlist(~c[1]), c, s.get_offset(c))); in check_clause()
145 VERIFY(s.get_wlist(literal(v, false)).empty()); in check_bool_vars()
146 VERIFY(s.get_wlist(literal(v, true)).empty()); in check_bool_vars()
153 return check_watches(l, s.get_wlist(~l)); in check_watches()
161 … CTRACE("sat_watched_bug", !s.get_wlist(~(w.get_literal())).contains(watched(l, w.is_learned())), in check_watches()
168 s.display_watch_list(tout, s.get_wlist(~(w.get_literal()))); in check_watches()
170 VERIFY(find_binary_watch(s.get_wlist(~(w.get_literal())), l)); in check_watches()