Home
last modified time | relevance | path

Searched refs:get_literal (Results 1 – 25 of 232) sorted by relevance

12345678910

/dports/math/z3/z3-z3-4.8.13/src/sat/
H A Dsat_cleaner.cpp57 tout << ~to_literal(l_idx) << " " << it2->get_literal() << "\n"; in cleanup_watches()
58 … tout << s.value(~to_literal(l_idx)) << " " << s.value(it2->get_literal()) << "\n"; in cleanup_watches()
59 … tout << s.was_eliminated(it2->get_literal()) << " " << s.inconsistent() << "\n";); in cleanup_watches()
60 … SASSERT(s.value(it2->get_literal()) == l_true || s.value(it2->get_literal()) == l_undef); in cleanup_watches()
61 if (s.value(it2->get_literal()) == l_undef) { in cleanup_watches()
65 …CE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";); in cleanup_watches()
H A Dsat_watched.cpp45 if (w.is_binary_clause() && w.get_literal() == l) return &w; in find_binary_watch()
52 if (w.is_binary_clause() && w.get_literal() == l) return &w; in find_binary_watch()
62 if (it->is_binary_clause() && it->get_literal() == l && !found) { in erase_binary_watch()
117 out << w.get_literal(); in display_watch_list()
H A Dsat_xor_finder.cpp87 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in extract_xor()
88 if (extract_xor(parity, c, ~l, w.get_literal())) { in extract_xor()
96 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in extract_xor()
97 if (extract_xor(parity, c, ~l, w.get_literal())) { in extract_xor()
H A Dsat_lut_finder.cpp94 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in check_lut()
95 if (extract_lut(~l, w.get_literal())) { in check_lut()
103 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in check_lut()
104 if (extract_lut(~l, w.get_literal())) { in check_lut()
H A Dsat_integrity_checker.cpp160 VERIFY(!s.was_eliminated(w.get_literal().var())); in check_watches()
161 … CTRACE("sat_watched_bug", !s.get_wlist(~(w.get_literal())).contains(watched(l, w.is_learned())), in check_watches()
162 tout << "l: " << l << " l2: " << w.get_literal() << "\n"; in check_watches()
164 tout << " was_eliminated2: " << s.was_eliminated(w.get_literal().var()); 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()
H A Dsat_justification.h46 literal get_literal() const { SASSERT(is_binary_clause()); return to_literal(val1()); } in get_literal() function
66 out << "binary " << j.get_literal();
/dports/math/py-z3-solver/z3-z3-4.8.10/src/sat/
H A Dsat_cleaner.cpp57 tout << ~to_literal(l_idx) << " " << it2->get_literal() << "\n"; in cleanup_watches()
58 … tout << s.value(~to_literal(l_idx)) << " " << s.value(it2->get_literal()) << "\n"; in cleanup_watches()
59 … tout << s.was_eliminated(it2->get_literal()) << " " << s.inconsistent() << "\n";); in cleanup_watches()
60 … SASSERT(s.value(it2->get_literal()) == l_true || s.value(it2->get_literal()) == l_undef); in cleanup_watches()
61 if (s.value(it2->get_literal()) == l_undef) { in cleanup_watches()
65 …CE("cleanup_bug", tout << "keeping: " << ~to_literal(l_idx) << " " << it2->get_literal() << "\n";); in cleanup_watches()
H A Dsat_watched.cpp45 if (w.is_binary_clause() && w.get_literal() == l) return &w; in find_binary_watch()
52 if (w.is_binary_clause() && w.get_literal() == l) return &w; in find_binary_watch()
62 if (it->is_binary_clause() && it->get_literal() == l && !found) { in erase_binary_watch()
117 out << w.get_literal(); in display_watch_list()
H A Dsat_lut_finder.cpp94 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in check_lut()
95 if (extract_lut(~l, w.get_literal())) { in check_lut()
103 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in check_lut()
104 if (extract_lut(~l, w.get_literal())) { in check_lut()
H A Dsat_xor_finder.cpp87 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in extract_xor()
88 if (extract_xor(parity, c, ~l, w.get_literal())) { in extract_xor()
96 …if (w.is_binary_clause() && s.is_visited(w.get_literal().var()) && w.get_literal().index() < l.ind… in extract_xor()
97 if (extract_xor(parity, c, ~l, w.get_literal())) { in extract_xor()
H A Dsat_integrity_checker.cpp160 VERIFY(!s.was_eliminated(w.get_literal().var())); in check_watches()
161 … CTRACE("sat_watched_bug", !s.get_wlist(~(w.get_literal())).contains(watched(l, w.is_learned())), in check_watches()
162 tout << "l: " << l << " l2: " << w.get_literal() << "\n"; in check_watches()
164 tout << " was_eliminated2: " << s.was_eliminated(w.get_literal().var()); 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()
/dports/math/z3/z3-z3-4.8.13/src/smt/
H A Dsmt_conflict_resolution.cpp125 m_antecedents->push_back(js.get_literal()); in eq_justification2literals()
852 …TRACE("proof_gen_bug", tout << js.get_literal() << "\n"; m_ctx.display_literal_info(tout, js.get_l… in get_proof()
988 SASSERT(l == false_literal || l == cls->get_literal(0) || l == cls->get_literal(1)); in get_proof()
990 if (cls->get_literal(0) == l) { in get_proof()
994 SASSERT(l == cls->get_literal(1)); in get_proof()
1101 if (cls->get_literal(0) == l) { in visit_b_justification()
1105 SASSERT(cls->get_literal(1) == l); in visit_b_justification()
1112 SASSERT(cls->get_literal(i) != l); in visit_b_justification()
1150 if (get_proof(js.get_literal()) == nullptr) in visit_trans_proof()
1420 SASSERT(cls->get_literal(0) == consequent || cls->get_literal(1) == consequent); in mk_unsat_core()
[all …]
H A Dsmt_internalizer.cpp273 literal cl = get_literal(c); in internalize_assertion()
274 literal tl = get_literal(t); in internalize_assertion()
275 literal el = get_literal(e); in internalize_assertion()
297 literal l = get_literal(n); in assert_default()
469 literal l_def = get_literal(def); in internalize_distinct()
842 literal c_lit = get_literal(c); in internalize_ite_term()
1081 return ~get_literal(n); in get_literal()
1637 literal l = get_literal(n); in mk_and_cnstr()
1651 literal l = get_literal(n); in mk_or_cnstr()
1665 literal l = get_literal(n); in mk_iff_cnstr()
[all …]
H A Dsmt_context_inv.cpp33 SASSERT(is_watching_clause(~cls->get_literal(0), cls)); in check_clause()
34 SASSERT(is_watching_clause(~cls->get_literal(1), cls)); in check_clause()
60 SASSERT(l == cls->get_literal(0) || l == cls->get_literal(1)); in check_watch_list()
345 literal l = cls->get_literal(0); in validate_justification()
347 l = cls->get_literal(1); in validate_justification()
/dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/
H A Dsmt_conflict_resolution.cpp125 m_antecedents->push_back(js.get_literal()); in eq_justification2literals()
849 …TRACE("proof_gen_bug", tout << js.get_literal() << "\n"; m_ctx.display_literal_info(tout, js.get_l… in get_proof()
985 SASSERT(l == false_literal || l == cls->get_literal(0) || l == cls->get_literal(1)); in get_proof()
987 if (cls->get_literal(0) == l) { in get_proof()
991 SASSERT(l == cls->get_literal(1)); in get_proof()
1098 if (cls->get_literal(0) == l) { in visit_b_justification()
1102 SASSERT(cls->get_literal(1) == l); in visit_b_justification()
1109 SASSERT(cls->get_literal(i) != l); in visit_b_justification()
1147 if (get_proof(js.get_literal()) == nullptr) in visit_trans_proof()
1418 SASSERT(cls->get_literal(0) == consequent || cls->get_literal(1) == consequent); in mk_unsat_core()
[all …]
H A Dsmt_internalizer.cpp273 literal cl = get_literal(c); in internalize_assertion()
274 literal tl = get_literal(t); in internalize_assertion()
275 literal el = get_literal(e); in internalize_assertion()
297 literal l = get_literal(n); in assert_default()
468 literal l_def = get_literal(def); in internalize_distinct()
836 literal c_lit = get_literal(c); in internalize_ite_term()
1075 return ~get_literal(n); in get_literal()
1631 literal l = get_literal(n); in mk_and_cnstr()
1645 literal l = get_literal(n); in mk_or_cnstr()
1659 literal l = get_literal(n); in mk_iff_cnstr()
[all …]
H A Dsmt_context_inv.cpp33 SASSERT(is_watching_clause(~cls->get_literal(0), cls)); in check_clause()
34 SASSERT(is_watching_clause(~cls->get_literal(1), cls)); in check_clause()
60 SASSERT(l == cls->get_literal(0) || l == cls->get_literal(1)); in check_watch_list()
345 literal l = cls->get_literal(0); in validate_justification()
347 l = cls->get_literal(1); in validate_justification()
/dports/databases/xtrabackup/percona-xtrabackup-2.4.21/rapid/unittest/gunit/xplugin/
H A Dinsert_statement_builder_t.cc79 inline std::string get_literal(const std::string& name) in get_literal() function
87 return "field {" + get_literal(name) + "}"; in get_field()
112 *row.Add() << get_literal("one"); in TEST_F()
121 *row.Add() << get_literal("one"); in TEST_F()
130 *row.Add() << get_literal("one"); in TEST_F()
131 *row.Add() << get_literal("two"); in TEST_F()
/dports/databases/percona57-server/percona-server-5.7.36-39/rapid/unittest/gunit/xplugin/
H A Dinsert_statement_builder_t.cc79 inline std::string get_literal(const std::string& name) in get_literal() function
87 return "field {" + get_literal(name) + "}"; in get_field()
112 *row.Add() << get_literal("one"); in TEST_F()
121 *row.Add() << get_literal("one"); in TEST_F()
130 *row.Add() << get_literal("one"); in TEST_F()
131 *row.Add() << get_literal("two"); in TEST_F()
/dports/databases/mysqlwsrep57-server/mysql-wsrep-wsrep_5.7.35-25.27/rapid/unittest/gunit/xplugin/
H A Dinsert_statement_builder_t.cc79 inline std::string get_literal(const std::string& name) in get_literal() function
87 return "field {" + get_literal(name) + "}"; in get_field()
112 *row.Add() << get_literal("one"); in TEST_F()
121 *row.Add() << get_literal("one"); in TEST_F()
130 *row.Add() << get_literal("one"); in TEST_F()
131 *row.Add() << get_literal("two"); in TEST_F()
/dports/databases/percona57-client/percona-server-5.7.36-39/rapid/unittest/gunit/xplugin/
H A Dinsert_statement_builder_t.cc79 inline std::string get_literal(const std::string& name) in get_literal() function
87 return "field {" + get_literal(name) + "}"; in get_field()
112 *row.Add() << get_literal("one"); in TEST_F()
121 *row.Add() << get_literal("one"); in TEST_F()
130 *row.Add() << get_literal("one"); in TEST_F()
131 *row.Add() << get_literal("two"); in TEST_F()
/dports/databases/mysql57-client/mysql-5.7.36/rapid/unittest/gunit/xplugin/
H A Dinsert_statement_builder_t.cc79 inline std::string get_literal(const std::string& name) in get_literal() function
87 return "field {" + get_literal(name) + "}"; in get_field()
112 *row.Add() << get_literal("one"); in TEST_F()
121 *row.Add() << get_literal("one"); in TEST_F()
130 *row.Add() << get_literal("one"); in TEST_F()
131 *row.Add() << get_literal("two"); in TEST_F()
/dports/databases/percona57-pam-for-mysql/percona-server-5.7.36-39/rapid/unittest/gunit/xplugin/
H A Dinsert_statement_builder_t.cc79 inline std::string get_literal(const std::string& name) in get_literal() function
87 return "field {" + get_literal(name) + "}"; in get_field()
112 *row.Add() << get_literal("one"); in TEST_F()
121 *row.Add() << get_literal("one"); in TEST_F()
130 *row.Add() << get_literal("one"); in TEST_F()
131 *row.Add() << get_literal("two"); in TEST_F()
/dports/math/clingo/clingo-5.5.1/libclingo/tests/
H A Dpropagator.cc474 literal_t get_literal(PropagateInit &init, char const *name) { in get_literal() function
752 auto a = get_literal(init, "a"); in __anon8c6883b40802()
768 auto a = get_literal(init, "a"); in __anon8c6883b40902()
784 auto a = get_literal(init, "a"); in __anon8c6883b40a02()
785 auto b = get_literal(init, "b"); in __anon8c6883b40a02()
803 auto a = get_literal(init, "a"); in __anon8c6883b40b02()
804 auto b = get_literal(init, "b"); in __anon8c6883b40b02()
820 init.add_minimize(get_literal(init, "a"), 1, 0); in __anon8c6883b40c02()
821 init.add_minimize(get_literal(init, "b"), 1, 0); in __anon8c6883b40c02()
822 init.add_minimize(get_literal(init, "c"), 1, 0); in __anon8c6883b40c02()
[all …]
/dports/misc/otter/otter-3.3f/source/
H A Dresolve.c59 new = get_literal(); in build_hyper()
75 new = get_literal(); in build_hyper()
109 new = get_literal(); in build_hyper()
421 l1 = get_literal(); in hyper_res()
482 l1 = get_literal(); in hyper_res()
519 l1 = get_literal(); in hyper_res()
625 l1 = get_literal(); in neg_hyper_res()
723 l1 = get_literal(); in neg_hyper_res()
828 l1 = get_literal(); in ur_res()
914 l1 = get_literal(); in ur_res()
[all …]

12345678910