Home
last modified time | relevance | path

Searched refs:lit1 (Results 1 – 25 of 327) sorted by relevance

12345678910>>...14

/dports/lang/racket/racket-8.3/share/pkgs/datalog/tests/private/
H A Dvariant.rkt19 (test-not-false "same" (variant? (make-literal #f 'lit1 empty) (make-literal #f 'lit1 empty)))
21 (test-not-false "same" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1)))
22 (make-literal #f 'lit1 (list (make-constant #f 'k1)))))
23 (test-false "dif con" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1)))
24 (make-literal #f 'lit1 (list (make-constant #f 'k2)))))
25 (test-false "dif var/con" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v1)))
29 (test-not-false "same" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v1)))
30 (make-literal #f 'lit1 (list (make-variable #f 'v1)))))
37 (test-false "mt" (mem-literal (make-literal #f 'lit1 empty) empty))
38 …(test-not-false "in" (mem-literal (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty…
[all …]
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/
H A Ddatasync.cpp148 lit1 = solver->map_to_with_bva(lit1); in clear_set_binary_values()
149 lit1 = solver->varReplacer->get_lit_replaced_with_outer(lit1); in clear_set_binary_values()
150 lit1 = solver->map_outer_to_inter(lit1); in clear_set_binary_values()
194 lit1 = solver->map_to_with_bva(lit1); in syncBinFromOthers()
195 lit1 = solver->varReplacer->get_lit_replaced_with_outer(lit1); in syncBinFromOthers()
196 lit1 = solver->map_outer_to_inter(lit1); in syncBinFromOthers()
281 assert(lit1 < lit2); in addOneBinToOthers()
382 lit1 = solver->map_inter_to_outer(lit1); in signalNewBinClause()
383 lit1 = map_outside_without_bva(lit1); in signalNewBinClause()
541 lit1 = solver->varReplacer->get_lit_replaced_with_outer(lit1); in sync_mpi_unit()
[all …]
H A Dgatefinder.h41 lit1(_lit1) in OrGate()
46 if (lit1 > lit2) in OrGate()
47 std::swap(lit1, lit2); in OrGate()
54 && lit1 == other.lit1
60 return std::array<Lit, 2>{{lit1, lit2}}; in getLits()
64 Lit lit1; variable
78 if (a.lit1 != b.lit1) { in operator()
79 return (a.lit1 < b.lit1); in operator()
93 << " lits: " << gate.lit1 << ", " << gate.lit2
163 void add_gate_if_not_already_inside(Lit rhs, Lit lit1, Lit lit2);
[all …]
H A Dvarreplacer.cpp376 , Lit lit1 in updateBin() argument
382 if (lit1 == lit2) { in updateBin()
394 if (lit1 == ~lit2) in updateBin()
484 if (get_lit_replaced_with_fast(lit1) != lit1) { in replaceImplicit()
485 lit1 = get_lit_replaced_with_fast(lit1); in replaceImplicit()
796 << add << lit1 in handleAlreadyReplaced()
819 const Lit lit1 in replace_vars_already_set() argument
848 const Lit lit1 in handleOneSet() argument
954 table[lit1.var()] = lit2 ^ lit1.sign(); in update_table_and_reversetable()
967 setAllThatPointsHereTo(lit1.var(), lit2 ^ lit1.sign()); in update_table_and_reversetable()
[all …]
H A Dbva.h77 lit1 = a;
84 lit1 = a;
91 return lit1 == other.lit1 && lit2 == other.lit2;
97 h = lit1.toInt(); in hash()
111 Lit lit1; member
125 if (lits.lit1 != other.lits.lit1)
126 return lits.lit1 < other.lits.lit1;
H A Dwatchalgos.h59 , const Lit lit1 in removeWBin() argument
63 watch_subarray ws = wsFull[lit1]; in removeWBin()
80 , const Lit lit1 in removeWBin_change_order() argument
84 watch_subarray ws = wsFull[lit1]; in removeWBin_change_order()
99 , const Lit lit1 in removeWBin_except_marked() argument
103 watch_subarray ws = wsFull[lit1]; in removeWBin_except_marked()
126 , const Lit lit1 in findWatchedOfBin() argument
130 watch_subarray_const ws = wsFull[lit1]; in findWatchedOfBin()
142 , const Lit lit1 in findWatchedOfBin() argument
146 watch_subarray ws = wsFull[lit1]; in findWatchedOfBin()
H A Dsolvertypes.h180 lit1(_lit1) in BinaryClause()
184 if (lit1 > lit2) std::swap(lit1, lit2); in BinaryClause()
189 if (lit1 < other.lit1) return true;
190 if (lit1 > other.lit1) return false;
199 return (lit1 == other.lit1
206 return lit1; in getLit1()
220 Lit lit1;
653 Lit& lit1 in orderLits() argument
657 if (lit1 > lit3) in orderLits()
660 if (lit1 > lit2) in orderLits()
[all …]
/dports/math/cryptominisat/cryptominisat-5.8.0/src/
H A Ddatasync.cpp148 lit1 = solver->map_to_with_bva(lit1); in clear_set_binary_values()
149 lit1 = solver->varReplacer->get_lit_replaced_with_outer(lit1); in clear_set_binary_values()
150 lit1 = solver->map_outer_to_inter(lit1); in clear_set_binary_values()
194 lit1 = solver->map_to_with_bva(lit1); in syncBinFromOthers()
195 lit1 = solver->varReplacer->get_lit_replaced_with_outer(lit1); in syncBinFromOthers()
196 lit1 = solver->map_outer_to_inter(lit1); in syncBinFromOthers()
281 assert(lit1 < lit2); in addOneBinToOthers()
382 lit1 = solver->map_inter_to_outer(lit1); in signalNewBinClause()
383 lit1 = map_outside_without_bva(lit1); in signalNewBinClause()
541 lit1 = solver->varReplacer->get_lit_replaced_with_outer(lit1); in sync_mpi_unit()
[all …]
H A Dgatefinder.h41 lit1(_lit1) in OrGate()
46 if (lit1 > lit2) in OrGate()
47 std::swap(lit1, lit2); in OrGate()
54 && lit1 == other.lit1
60 return std::array<Lit, 2>{{lit1, lit2}}; in getLits()
64 Lit lit1; variable
78 if (a.lit1 != b.lit1) { in operator()
79 return (a.lit1 < b.lit1); in operator()
93 << " lits: " << gate.lit1 << ", " << gate.lit2
163 void add_gate_if_not_already_inside(Lit rhs, Lit lit1, Lit lit2);
[all …]
H A Dvarreplacer.cpp376 , Lit lit1 in updateBin() argument
382 if (lit1 == lit2) { in updateBin()
394 if (lit1 == ~lit2) in updateBin()
484 if (get_lit_replaced_with_fast(lit1) != lit1) { in replaceImplicit()
485 lit1 = get_lit_replaced_with_fast(lit1); in replaceImplicit()
796 << add << lit1 in handleAlreadyReplaced()
819 const Lit lit1 in replace_vars_already_set() argument
848 const Lit lit1 in handleOneSet() argument
954 table[lit1.var()] = lit2 ^ lit1.sign(); in update_table_and_reversetable()
967 setAllThatPointsHereTo(lit1.var(), lit2 ^ lit1.sign()); in update_table_and_reversetable()
[all …]
H A Dbva.h77 lit1 = a;
84 lit1 = a;
91 return lit1 == other.lit1 && lit2 == other.lit2;
97 h = lit1.toInt(); in hash()
111 Lit lit1; member
125 if (lits.lit1 != other.lits.lit1)
126 return lits.lit1 < other.lits.lit1;
H A Dwatchalgos.h59 , const Lit lit1 in removeWBin() argument
63 watch_subarray ws = wsFull[lit1]; in removeWBin()
80 , const Lit lit1 in removeWBin_change_order() argument
84 watch_subarray ws = wsFull[lit1]; in removeWBin_change_order()
99 , const Lit lit1 in removeWBin_except_marked() argument
103 watch_subarray ws = wsFull[lit1]; in removeWBin_except_marked()
126 , const Lit lit1 in findWatchedOfBin() argument
130 watch_subarray_const ws = wsFull[lit1]; in findWatchedOfBin()
142 , const Lit lit1 in findWatchedOfBin() argument
146 watch_subarray ws = wsFull[lit1]; in findWatchedOfBin()
H A Dsolvertypes.h180 lit1(_lit1) in BinaryClause()
184 if (lit1 > lit2) std::swap(lit1, lit2); in BinaryClause()
189 if (lit1 < other.lit1) return true;
190 if (lit1 > other.lit1) return false;
199 return (lit1 == other.lit1
206 return lit1; in getLit1()
220 Lit lit1;
653 Lit& lit1 in orderLits() argument
657 if (lit1 > lit3) in orderLits()
660 if (lit1 > lit2) in orderLits()
[all …]
/dports/lang/racket/racket-8.3/share/pkgs/datalog/tests/
H A Dast.rkt11 (define lit1-srcloc (list ast.rkt #f #f 3000 3))
64 …test-not-false "lit" (literal-equal? (make-literal #f 'lit1 empty) (make-literal lit1-srcloc 'lit1…
66 … (make-literal lit1-srcloc 'lit1 (list (make-variable #f 'sym1)))))
68 … (make-literal lit1-srcloc 'lit1 (list (make-variable sym1-srcloc 'sym1)))))
69 …(test-false "lit" (literal-equal? (make-literal #f 'lit1 empty) (make-literal lit1-srcloc 'lit2 em…
70 …t-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1))) (make-litera…
78 … "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 e…
79 … (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))))
82 (test-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) empty)
84 … "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 e…
[all …]
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/mpi/
H A DDataSync.cpp299 Lit lit1 = ~Lit::toLit(wsLit); in syncToMPI() local
305 assert(lit1 == binSet[i].lit1); in syncToMPI()
327 assert(triSet[i].lit1 == lit1); in syncToMPI()
364 lit1 = solver.varReplacer->getReplaceTable()[lit1.var()] ^ lit1.sign(); in shareBinData()
398 if (lit1.toInt() > lit2.toInt()) std::swap(lit1, lit2); in signalNewBinClause()
414 lits[0] = lit1; in signalNewTriClause()
432 lit1 = solver.varReplacer->getReplaceTable()[lit1.var()] ^ lit1.sign(); in shareTriData()
458 assert(solver.varReplacer->getReplaceTable()[lit1.var()].var() == lit1.var()); in syncTriFromOthers()
508 tmp[0] = lit1; in syncTriFromOthers()
537 assert(lit1 < lit2); in addOneTriToOthers()
[all …]
/dports/math/cryptominisat/cryptominisat-5.8.0/src/mpi/
H A DDataSync.cpp299 Lit lit1 = ~Lit::toLit(wsLit); in syncToMPI() local
305 assert(lit1 == binSet[i].lit1); in syncToMPI()
327 assert(triSet[i].lit1 == lit1); in syncToMPI()
364 lit1 = solver.varReplacer->getReplaceTable()[lit1.var()] ^ lit1.sign(); in shareBinData()
398 if (lit1.toInt() > lit2.toInt()) std::swap(lit1, lit2); in signalNewBinClause()
414 lits[0] = lit1; in signalNewTriClause()
432 lit1 = solver.varReplacer->getReplaceTable()[lit1.var()] ^ lit1.sign(); in shareTriData()
458 assert(solver.varReplacer->getReplaceTable()[lit1.var()].var() == lit1.var()); in syncTriFromOthers()
508 tmp[0] = lit1; in syncTriFromOthers()
537 assert(lit1 < lit2); in addOneTriToOthers()
[all …]
/dports/devel/py-mypy/mypy-0.910/mypy/test/
H A Dtesttypes.py301 lit1 = fx.lit1
319 assert_true(is_subtype(lit1, lit1))
468 self.assert_simplified_union([fx.lit1, fx.lit1], fx.lit1)
759 lit1 = self.fx.lit1
763 self.assert_join(lit1, lit1, lit1)
987 lit1 = self.fx.lit1
991 self.assert_meet(lit1, lit1, lit1)
992 self.assert_meet(lit1, a, lit1)
995 self.assert_meet(UnionType([lit1, lit2]), lit1, lit1)
1047 lit1 = self.fx.lit1
[all …]
/dports/cad/nvc/nvc-r1.5.3/test/
H A Dtest_value.c45 tree_t lit1 = tree_new(T_ENUM_LIT); in START_TEST() local
46 tree_set_ident(lit1, ident_new("'x'")); in START_TEST()
54 type_enum_add_literal(t, lit1); in START_TEST()
76 tree_t lit1 = tree_new(T_ENUM_LIT); in START_TEST() local
77 tree_set_ident(lit1, ident_new("A")); in START_TEST()
78 tree_set_type(lit1, t); in START_TEST()
88 type_enum_add_literal(t, lit1); in START_TEST()
96 .left = make_ref(lit1), in START_TEST()
/dports/devel/boost-docs/boost_1_72_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit1 = L"Hello"; in BOOST_AUTO_TEST_CASE() local
51 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE()
53 BOOST_CHECK(std::wcscmp(lit1.c_str(), lit2.c_str()) == 0); in BOOST_AUTO_TEST_CASE()
58 logging::string_literal lit1 = logging::str_literal("Wow!"); in BOOST_AUTO_TEST_CASE() local
59 BOOST_CHECK(std::strcmp(lit1.c_str(), "Wow!") == 0); in BOOST_AUTO_TEST_CASE()
186 logging::string_literal lit1 = "yo-ho-ho"; in BOOST_AUTO_TEST_CASE() local
189 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
190 BOOST_CHECK_EQUAL(lit1, "hello"); in BOOST_AUTO_TEST_CASE()
193 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
195 BOOST_CHECK_EQUAL(lit1, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
/dports/devel/boost-python-libs/boost_1_72_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit1 = L"Hello"; in BOOST_AUTO_TEST_CASE() local
51 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE()
53 BOOST_CHECK(std::wcscmp(lit1.c_str(), lit2.c_str()) == 0); in BOOST_AUTO_TEST_CASE()
58 logging::string_literal lit1 = logging::str_literal("Wow!"); in BOOST_AUTO_TEST_CASE() local
59 BOOST_CHECK(std::strcmp(lit1.c_str(), "Wow!") == 0); in BOOST_AUTO_TEST_CASE()
186 logging::string_literal lit1 = "yo-ho-ho"; in BOOST_AUTO_TEST_CASE() local
189 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
190 BOOST_CHECK_EQUAL(lit1, "hello"); in BOOST_AUTO_TEST_CASE()
193 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
195 BOOST_CHECK_EQUAL(lit1, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
/dports/databases/percona57-pam-for-mysql/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp49 logging::wstring_literal lit1 = L"Hello"; in BOOST_AUTO_TEST_CASE() local
50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE()
52 BOOST_CHECK(std::wcscmp(lit1.c_str(), lit2.c_str()) == 0); in BOOST_AUTO_TEST_CASE()
57 logging::string_literal lit1 = logging::str_literal("Wow!"); in BOOST_AUTO_TEST_CASE() local
58 BOOST_CHECK(std::strcmp(lit1.c_str(), "Wow!") == 0); in BOOST_AUTO_TEST_CASE()
184 logging::string_literal lit1 = "yo-ho-ho"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
188 BOOST_CHECK_EQUAL(lit1, "hello"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
193 BOOST_CHECK_EQUAL(lit1, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
/dports/databases/percona57-server/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp49 logging::wstring_literal lit1 = L"Hello"; in BOOST_AUTO_TEST_CASE() local
50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE()
52 BOOST_CHECK(std::wcscmp(lit1.c_str(), lit2.c_str()) == 0); in BOOST_AUTO_TEST_CASE()
57 logging::string_literal lit1 = logging::str_literal("Wow!"); in BOOST_AUTO_TEST_CASE() local
58 BOOST_CHECK(std::strcmp(lit1.c_str(), "Wow!") == 0); in BOOST_AUTO_TEST_CASE()
184 logging::string_literal lit1 = "yo-ho-ho"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
188 BOOST_CHECK_EQUAL(lit1, "hello"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
193 BOOST_CHECK_EQUAL(lit1, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
/dports/databases/xtrabackup/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp49 logging::wstring_literal lit1 = L"Hello"; in BOOST_AUTO_TEST_CASE() local
50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE()
52 BOOST_CHECK(std::wcscmp(lit1.c_str(), lit2.c_str()) == 0); in BOOST_AUTO_TEST_CASE()
57 logging::string_literal lit1 = logging::str_literal("Wow!"); in BOOST_AUTO_TEST_CASE() local
58 BOOST_CHECK(std::strcmp(lit1.c_str(), "Wow!") == 0); in BOOST_AUTO_TEST_CASE()
184 logging::string_literal lit1 = "yo-ho-ho"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
188 BOOST_CHECK_EQUAL(lit1, "hello"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
193 BOOST_CHECK_EQUAL(lit1, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
/dports/databases/percona57-client/boost_1_59_0/libs/log/test/run/
H A Dutil_string_literal.cpp49 logging::wstring_literal lit1 = L"Hello"; in BOOST_AUTO_TEST_CASE() local
50 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE()
52 BOOST_CHECK(std::wcscmp(lit1.c_str(), lit2.c_str()) == 0); in BOOST_AUTO_TEST_CASE()
57 logging::string_literal lit1 = logging::str_literal("Wow!"); in BOOST_AUTO_TEST_CASE() local
58 BOOST_CHECK(std::strcmp(lit1.c_str(), "Wow!") == 0); in BOOST_AUTO_TEST_CASE()
184 logging::string_literal lit1 = "yo-ho-ho"; in BOOST_AUTO_TEST_CASE() local
187 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
188 BOOST_CHECK_EQUAL(lit1, "hello"); in BOOST_AUTO_TEST_CASE()
191 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
193 BOOST_CHECK_EQUAL(lit1, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()
/dports/devel/boost-libs/boost_1_72_0/libs/log/test/run/
H A Dutil_string_literal.cpp50 logging::wstring_literal lit1 = L"Hello"; in BOOST_AUTO_TEST_CASE() local
51 logging::wstring_literal lit2 = lit1; in BOOST_AUTO_TEST_CASE()
53 BOOST_CHECK(std::wcscmp(lit1.c_str(), lit2.c_str()) == 0); in BOOST_AUTO_TEST_CASE()
58 logging::string_literal lit1 = logging::str_literal("Wow!"); in BOOST_AUTO_TEST_CASE() local
59 BOOST_CHECK(std::strcmp(lit1.c_str(), "Wow!") == 0); in BOOST_AUTO_TEST_CASE()
186 logging::string_literal lit1 = "yo-ho-ho"; in BOOST_AUTO_TEST_CASE() local
189 lit1.swap(lit2); in BOOST_AUTO_TEST_CASE()
190 BOOST_CHECK_EQUAL(lit1, "hello"); in BOOST_AUTO_TEST_CASE()
193 swap(lit1, lit2); in BOOST_AUTO_TEST_CASE()
195 BOOST_CHECK_EQUAL(lit1, "yo-ho-ho"); in BOOST_AUTO_TEST_CASE()

12345678910>>...14