Home
last modified time | relevance | path

Searched refs:get_wlist (Results 1 – 25 of 44) sorted by relevance

12

/dports/math/z3/z3-z3-4.8.13/src/sat/
H A Dsat_integrity_checker.cpp69 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()
168 s.display_watch_list(tout, s.get_wlist(~(w.get_literal()))); in check_watches()
[all …]
H A Dsat_probing.cpp155 if (nullptr == find_binary_watch(s.get_wlist(lit), l) || in process_core()
156 nullptr == find_binary_watch(s.get_wlist(~l), ~lit)) { in process_core()
170 unsigned sz = s.get_wlist(~l).size(); in process_core()
172 watch_list& wlist = s.get_wlist(~l); in process_core()
H A Dsat_elim_vars.cpp126 for (watched const& w : simp.get_wlist(~pos_l)) { in elim_var()
132 for (watched const& w : simp.get_wlist(~neg_l)) { in elim_var()
297 watch_list& wl = simp.get_wlist(lit); in mark_literals()
321 watch_list& wl = simp.get_wlist(~lit); in make_clauses()
H A Dsat_simplifier.cpp74 watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } in get_wlist() function in sat::simplifier
76 watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); } in get_wlist() function in sat::simplifier
774 mark_as_not_learned_core(get_wlist(~l1), l2); in mark_as_not_learned()
775 mark_as_not_learned_core(get_wlist(~l2), l1); in mark_as_not_learned()
1106 for (watched & w : s.get_wlist(l)) { in resolution_intersection()
1171 for (watched & w : s.get_wlist(l)) { in check_abce_tautology()
1511 watch_list & wlist = s.get_wlist(~l); in process_cce_binary()
1645 watch_list & wlist = s.get_wlist(l); in all_tautology()
1730 watch_list const & wlist = get_wlist(~l); in num_nonlearned_bin()
1791 watch_list & wlist = get_wlist(~l); in collect_clauses()
[all …]
H A Dsat_gc.cpp430 auto& wl1 = get_wlist(lit); in gc_vars()
431 for (auto w : get_wlist(lit)) { in gc_vars()
445 auto& wl2 = get_wlist(~lit); in gc_vars()
593 auto& wl = get_wlist((~lit).index());
H A Dsat_simplifier.h177 watch_list & get_wlist(literal l);
178 watch_list const & get_wlist(literal l) const;
H A Dsat_xor_finder.cpp86 for (watched const & w : s.get_wlist(l)) { in extract_xor()
95 for (watched const & w : s.get_wlist(l)) { in extract_xor()
H A Dsat_lut_finder.cpp93 for (watched const & w : s.get_wlist(l)) { in check_lut()
102 for (watched const & w : s.get_wlist(l)) { in check_lut()
H A Dsat_big.cpp40 for (watched const& w : s.get_wlist(l_idx)) { in init()
206 s.get_wlist(~v).erase(watched(~u, w.is_learned())); in reduce_tr()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/
H A Dsat_integrity_checker.cpp69 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()
168 s.display_watch_list(tout, s.get_wlist(~(w.get_literal()))); in check_watches()
[all …]
H A Dsat_probing.cpp155 if (nullptr == find_binary_watch(s.get_wlist(lit), l) || in process_core()
156 nullptr == find_binary_watch(s.get_wlist(~l), ~lit)) { in process_core()
170 unsigned sz = s.get_wlist(~l).size(); in process_core()
172 watch_list& wlist = s.get_wlist(~l); in process_core()
H A Dsat_elim_vars.cpp126 for (watched const& w : simp.get_wlist(~pos_l)) { in elim_var()
132 for (watched const& w : simp.get_wlist(~neg_l)) { in elim_var()
297 watch_list& wl = simp.get_wlist(lit); in mark_literals()
321 watch_list& wl = simp.get_wlist(~lit); in make_clauses()
H A Dsat_simplifier.cpp74 watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); } in get_wlist() function in sat::simplifier
76 watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); } in get_wlist() function in sat::simplifier
773 mark_as_not_learned_core(get_wlist(~l1), l2); in mark_as_not_learned()
774 mark_as_not_learned_core(get_wlist(~l2), l1); in mark_as_not_learned()
1105 for (watched & w : s.get_wlist(l)) { in resolution_intersection()
1170 for (watched & w : s.get_wlist(l)) { in check_abce_tautology()
1510 watch_list & wlist = s.get_wlist(~l); in process_cce_binary()
1644 watch_list & wlist = s.get_wlist(l); in all_tautology()
1729 watch_list const & wlist = get_wlist(~l); in num_nonlearned_bin()
1790 watch_list & wlist = get_wlist(~l); in collect_clauses()
[all …]
H A Dsat_gc.cpp430 auto& wl1 = get_wlist(lit); in gc_vars()
431 for (auto w : get_wlist(lit)) { in gc_vars()
445 auto& wl2 = get_wlist(~lit); in gc_vars()
593 auto& wl = get_wlist((~lit).index());
H A Dsat_simplifier.h171 watch_list & get_wlist(literal l);
172 watch_list const & get_wlist(literal l) const;
H A Dsat_lut_finder.cpp93 for (watched const & w : s.get_wlist(l)) { in check_lut()
102 for (watched const & w : s.get_wlist(l)) { in check_lut()
H A Dsat_xor_finder.cpp86 for (watched const & w : s.get_wlist(l)) { in extract_xor()
95 for (watched const & w : s.get_wlist(l)) { in extract_xor()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/smt/
H A Dba_constraint.cpp34 return s.get_wlist(~lit).contains(sat::watched(cindex())); in is_watched()
39 s.get_wlist(~lit).erase(w); in unwatch_literal()
47 s.get_wlist(~lit).push_back(w); in watch_literal()
H A Dba_solver_interface.h44 virtual sat::watch_list& get_wlist(literal l) = 0;
45 virtual sat::watch_list const& get_wlist(literal l) const = 0;
H A Dba_solver.h296 …inline watch_list& get_wlist(literal l) override { return m_lookahead ? m_lookahead->get_wlist(l) … in get_wlist() function
297 …line watch_list const& get_wlist(literal l) const override { return m_lookahead ? m_lookahead->get… in get_wlist() function
H A Dxor_solver.cpp102 for (auto const & w : get_wlist(lits[0])) { in add_xor_def()
354 for (watched w : get_wlist(lit)) { in merge_xor()
357 for (watched w : get_wlist(~lit)) { in merge_xor()
/dports/math/z3/z3-z3-4.8.13/src/sat/smt/
H A Dpb_constraint.cpp34 return s.get_wlist(~lit).contains(sat::watched(cindex())); in is_watched()
39 s.get_wlist(~lit).erase(w); in unwatch_literal()
47 s.get_wlist(~lit).push_back(w); in watch_literal()
H A Dpb_solver_interface.h45 virtual sat::watch_list& get_wlist(literal l) = 0;
46 virtual sat::watch_list const& get_wlist(literal l) const = 0;
H A Dpb_solver.h274 …inline sat::watch_list& get_wlist(literal l) override { return m_lookahead ? m_lookahead->get_wlis… in get_wlist() function
275 …at:: watch_list const& get_wlist(literal l) const override { return m_lookahead ? m_lookahead->get… in get_wlist() function
H A Dxor_solver.d102 for (auto const & w : get_wlist(lits[0])) { in add_xor_def()
354 for (watched w : get_wlist(lit)) { in merge_xor()
357 for (watched w : get_wlist(~lit)) { in merge_xor()

12