Home
last modified time | relevance | path

Searched refs:lit2 (Results 1 – 25 of 581) sorted by relevance

12345678910>>...24

/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/
H A Dgatefinder.h42 , lit2(_lit2) in OrGate()
46 if (lit1 > lit2) in OrGate()
55 && lit2 == other.lit2
65 Lit lit2; variable
82 if (a.lit2 != b.lit2) { in operator()
83 return (a.lit2 < b.lit2); in operator()
176 , const Lit lit2
269 lit2(_lit2) in TriToUnlink()
274 const Lit lit2; member
280 if (lit2 != other.lit2)
[all …]
H A Dwatchalgos.h60 , const Lit lit2 in removeWBin() argument
67 || i->lit2() != lit2 in removeWBin()
81 , const Lit lit2 in removeWBin_change_order() argument
88 || i->lit2() != lit2 in removeWBin_change_order()
100 , const Lit lit2 in removeWBin_except_marked() argument
107 || i->lit2() != lit2 in removeWBin_except_marked()
127 , const Lit lit2 in findWatchedOfBin() argument
132 if (i->isBin() && i->lit2() == lit2 && i->red() == red) in findWatchedOfBin()
143 , const Lit lit2 in findWatchedOfBin() argument
148 if (i->isBin() && i->lit2() == lit2 && i->red() == red) in findWatchedOfBin()
H A Dvarreplacer.cpp377 , Lit lit2 in updateBin() argument
382 if (lit1 == lit2) { in updateBin()
394 if (lit1 == ~lit2) in updateBin()
416 << add << lit1 << lit2 in updateBin()
492 if (get_lit_replaced_with_fast(lit2) != lit2) { in replaceImplicit()
493 lit2 = get_lit_replaced_with_fast(lit2); in replaceImplicit()
850 , const Lit lit2 in handleOneSet() argument
911 << add << ~lit1 << lit2 in replace()
917 << add << lit1 << ~lit2 in replace()
961 table[lit2.var()] = lit1 ^ lit2.sign(); in update_table_and_reversetable()
[all …]
H A Dsolvertypes.h181 , lit2(_lit2) in BinaryClause()
184 if (lit1 > lit2) std::swap(lit1, lit2); in BinaryClause()
192 if (lit2 < other.lit2) return true;
193 if (lit2 > other.lit2) return false;
200 && lit2 == other.lit2
211 return lit2; in getLit2()
221 Lit lit2; variable
654 , Lit& lit2 in orderLits() argument
660 if (lit1 > lit2) in orderLits()
663 if (lit2 > lit3) in orderLits()
[all …]
H A Dpropengine.h206 , Lit lit2
213 removeWBin(watches, lit1, lit2, red);
216 removeWBin(watches, lit2, lit1, red);
229 , const Lit lit2
235 , const Lit lit2
509 , const Lit lit2 in attach_bin_clause() argument
517 assert(lit1.var() != lit2.var()); in attach_bin_clause()
520 assert(value(lit2) == l_Undef || value(lit2) == l_False); in attach_bin_clause()
524 assert(varData[lit2.var()].removed == Removed::none); in attach_bin_clause()
527 watches[lit1].push(Watched(lit2, red)); in attach_bin_clause()
[all …]
H A Dbva.h85 lit2 = b;
91 return lit1 == other.lit1 && lit2 == other.lit2;
99 if (lit2 == lit_Undef) in hash()
102 h = h*31 + lit2.toInt(); in hash()
112 Lit lit2; member
128 return lits.lit2 < other.lits.lit2;
H A Dcardfinder.cpp61 bool CardFinder::find_connector(Lit lit1, Lit lit2) const in find_connector()
67 std::swap(lit1, lit2); in find_connector()
75 if (x.lit2() == lit2) in find_connector()
110 l = ws.lit2(); in find_two_product_atmost1()
112 if (ws.lit2() < l) { in find_two_product_atmost1()
113 l = ws.lit2(); in find_two_product_atmost1()
124 Lit c = ws.lit2(); in find_two_product_atmost1()
148 seen[ws3.lit2().toInt()] = 1; in find_two_product_atmost1()
157 Lit conn_lit = ws3.lit2(); in find_two_product_atmost1()
176 seen[ws3.lit2().toInt()] = 0; in find_two_product_atmost1()
[all …]
/dports/math/cryptominisat/cryptominisat-5.8.0/src/
H A Dgatefinder.h42 , lit2(_lit2) in OrGate()
46 if (lit1 > lit2) in OrGate()
55 && lit2 == other.lit2
65 Lit lit2; variable
82 if (a.lit2 != b.lit2) { in operator()
83 return (a.lit2 < b.lit2); in operator()
176 , const Lit lit2
269 lit2(_lit2) in TriToUnlink()
274 const Lit lit2; member
280 if (lit2 != other.lit2)
[all …]
H A Dwatchalgos.h60 , const Lit lit2 in removeWBin() argument
67 || i->lit2() != lit2 in removeWBin()
81 , const Lit lit2 in removeWBin_change_order() argument
88 || i->lit2() != lit2 in removeWBin_change_order()
100 , const Lit lit2 in removeWBin_except_marked() argument
107 || i->lit2() != lit2 in removeWBin_except_marked()
127 , const Lit lit2 in findWatchedOfBin() argument
132 if (i->isBin() && i->lit2() == lit2 && i->red() == red) in findWatchedOfBin()
143 , const Lit lit2 in findWatchedOfBin() argument
148 if (i->isBin() && i->lit2() == lit2 && i->red() == red) in findWatchedOfBin()
H A Dvarreplacer.cpp377 , Lit lit2 in updateBin() argument
382 if (lit1 == lit2) { in updateBin()
394 if (lit1 == ~lit2) in updateBin()
416 << add << lit1 << lit2 in updateBin()
492 if (get_lit_replaced_with_fast(lit2) != lit2) { in replaceImplicit()
493 lit2 = get_lit_replaced_with_fast(lit2); in replaceImplicit()
850 , const Lit lit2 in handleOneSet() argument
911 << add << ~lit1 << lit2 in replace()
917 << add << lit1 << ~lit2 in replace()
961 table[lit2.var()] = lit1 ^ lit2.sign(); in update_table_and_reversetable()
[all …]
H A Dsolvertypes.h181 , lit2(_lit2) in BinaryClause()
184 if (lit1 > lit2) std::swap(lit1, lit2); in BinaryClause()
192 if (lit2 < other.lit2) return true;
193 if (lit2 > other.lit2) return false;
200 && lit2 == other.lit2
211 return lit2; in getLit2()
221 Lit lit2; variable
654 , Lit& lit2 in orderLits() argument
660 if (lit1 > lit2) in orderLits()
663 if (lit2 > lit3) in orderLits()
[all …]
H A Dpropengine.h206 , Lit lit2
213 removeWBin(watches, lit1, lit2, red);
216 removeWBin(watches, lit2, lit1, red);
229 , const Lit lit2
235 , const Lit lit2
509 , const Lit lit2 in attach_bin_clause() argument
517 assert(lit1.var() != lit2.var()); in attach_bin_clause()
520 assert(value(lit2) == l_Undef || value(lit2) == l_False); in attach_bin_clause()
524 assert(varData[lit2.var()].removed == Removed::none); in attach_bin_clause()
527 watches[lit1].push(Watched(lit2, red)); in attach_bin_clause()
[all …]
H A Dbva.h85 lit2 = b;
91 return lit1 == other.lit1 && lit2 == other.lit2;
99 if (lit2 == lit_Undef) in hash()
102 h = h*31 + lit2.toInt(); in hash()
112 Lit lit2; member
128 return lits.lit2 < other.lits.lit2;
/dports/devel/boost-docs/boost_1_72_0/libs/log/test/run/
H A Dutil_string_literal.cpp51 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
116 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
117 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
118 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
121 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
187 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
189 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
191 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
193 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/devel/boost-python-libs/boost_1_72_0/libs/log/test/run/
H A Dutil_string_literal.cpp51 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
116 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
117 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
118 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
121 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
187 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
189 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
191 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
193 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/databases/percona57-pam-for-mysql/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
114 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
115 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
116 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
117 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
185 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
189 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/databases/percona57-server/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
114 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
115 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
116 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
117 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
185 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
189 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/databases/xtrabackup/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
114 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
115 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
116 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
117 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
185 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
189 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/databases/percona57-client/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
114 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
115 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
116 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
117 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
185 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
189 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/devel/boost-libs/boost_1_72_0/libs/log/test/run/
H A Dutil_string_literal.cpp51 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
116 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
117 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
118 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
121 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
187 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
189 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
191 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
193 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/databases/mysqlwsrep57-server/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
114 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
115 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
116 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
117 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
185 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
189 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/devel/hyperscan/boost_1_75_0/libs/log/test/run/
H A Dutil_string_literal.cpp51 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE() local
116 logging::string_literal lit2 = "Yo!"; in BOOST_AUTO_TEST_CASE() local
117 BOOST_CHECK(lit != lit2); in BOOST_AUTO_TEST_CASE()
118 lit2 = "abcdefg"; in BOOST_AUTO_TEST_CASE()
119 BOOST_CHECK(lit == lit2); in BOOST_AUTO_TEST_CASE()
121 BOOST_CHECK(lit.compare(lit2) == 0); in BOOST_AUTO_TEST_CASE()
187 logging::string_literal lit2 = "hello"; in BOOST_AUTO_TEST_CASE() local
189 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
191 BOOST_CHECK_EQUAL(lit2, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
193 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
[all …]
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/mpi/
H A DDataSync.cpp398 if (lit1.toInt() > lit2.toInt()) std::swap(lit1, lit2); in signalNewBinClause()
415 lits[1] = lit2; in signalNewTriClause()
469 Lit lit2 = solver.varReplacer->getReplaceTable()[cl.lit2.var()] ^ cl.lit2.sign(); in syncTriFromOthers() local
509 tmp[1] = lit2; in syncTriFromOthers()
537 assert(lit1 < lit2); in addOneTriToOthers()
538 assert(lit2 < lit3); in addOneTriToOthers()
539 assert(lit1.var() != lit2.var()); in addOneTriToOthers()
540 assert(lit2.var() != lit3.var()); in addOneTriToOthers()
544 if (it->lit2 == lit2 in addOneTriToOthers()
570 Lit otherLit = bins[i].lit2; in syncBinFromOthers()
[all …]
/dports/math/cryptominisat/cryptominisat-5.8.0/src/mpi/
H A DDataSync.cpp398 if (lit1.toInt() > lit2.toInt()) std::swap(lit1, lit2); in signalNewBinClause()
415 lits[1] = lit2; in signalNewTriClause()
469 Lit lit2 = solver.varReplacer->getReplaceTable()[cl.lit2.var()] ^ cl.lit2.sign(); in syncTriFromOthers() local
509 tmp[1] = lit2; in syncTriFromOthers()
537 assert(lit1 < lit2); in addOneTriToOthers()
538 assert(lit2 < lit3); in addOneTriToOthers()
539 assert(lit1.var() != lit2.var()); in addOneTriToOthers()
540 assert(lit2.var() != lit3.var()); in addOneTriToOthers()
544 if (it->lit2 == lit2 in addOneTriToOthers()
570 Lit otherLit = bins[i].lit2; in syncBinFromOthers()
[all …]
/dports/cad/nvc/nvc-r1.5.3/test/
H A Dtest_value.c48 tree_t lit2 = tree_new(T_ENUM_LIT); in START_TEST() local
49 tree_set_ident(lit2, ident_new("HELLO")); in START_TEST()
55 type_enum_add_literal(t, lit2); in START_TEST()
80 tree_t lit2 = tree_new(T_ENUM_LIT); in START_TEST() local
81 tree_set_ident(lit2, ident_new("B")); in START_TEST()
82 tree_set_type(lit2, t); in START_TEST()
89 type_enum_add_literal(t, lit2); in START_TEST()
97 .right = make_ref(lit2) in START_TEST()

12345678910>>...24