/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/satoko/ |
H A D | solver.c | 46 if (c->size == 2 && lit_value(s, lits[0]) == SATOKO_LIT_FALSE) { in lit_is_removable() 47 assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE); in lit_is_removable() 120 lit_value(s, imp_lit) == SATOKO_LIT_TRUE) { in clause_bin_resolution() 274 assert(lit_value(s, lits[1]) == SATOKO_LIT_TRUE); in solver_analyze() 554 else if (lit_value(s, i->blocker) == SATOKO_LIT_FALSE) in solver_propagate() 569 if (lit_value(s, i->blocker) == SATOKO_LIT_TRUE) { in solver_propagate() 587 if (lits[0] != i->blocker && lit_value(s, lits[0]) == SATOKO_LIT_TRUE) in solver_propagate() 593 if (lit_value(s, lits[k]) != SATOKO_LIT_FALSE) { in solver_propagate() 604 if (lit_value(s, lits[0]) == SATOKO_LIT_FALSE) { in solver_propagate() 669 if (lit_value(s, lit) == SATOKO_LIT_TRUE) { in solver_search() [all …]
|
H A D | solver.h | 178 static inline char lit_value(solver_t *s, unsigned lit) in lit_value() function
|
H A D | solver_api.c | 41 if (lit_value(s, lits[i]) == SATOKO_LIT_TRUE) in clause_is_satisfied() 271 if ((unsigned)lits[i] == lit_compl(prev_lit) || lit_value(s, lits[i]) == SATOKO_LIT_TRUE) in satoko_add_clause()
|
/dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
H A D | new_sat_solver2.h | 1135 static inline bval_t lit_value(const sat_solver_t *solver, literal_t l) { in lit_value() function 1146 return bval_is_undef(lit_value(solver, l)); in lit_is_unassigned() 1162 return true_preferred(lit_value(solver, l)); in lit_prefers_true() 1166 return lit_value(solver, l) == VAL_TRUE; in lit_is_true() 1170 return lit_value(solver, l) == VAL_FALSE; in lit_is_false()
|
H A D | new_sat_solver.h | 1298 static inline bval_t lit_value(const sat_solver_t *solver, literal_t l) { in lit_value() function 1309 return bval_is_undef(lit_value(solver, l)); in lit_is_unassigned() 1325 return true_preferred(lit_value(solver, l)); in lit_prefers_true() 1329 return lit_value(solver, l) == VAL_TRUE; in lit_is_true() 1333 return lit_value(solver, l) == VAL_FALSE; in lit_is_false()
|
H A D | new_sat_solver2.c | 2977 switch (lit_value(solver, l)) { in nsat_base_literal() 3410 switch (lit_value(solver, l)) { in nsat_solver_simplify_and_add_clause() 4156 switch (lit_value(solver, i)) { in simplify_binary_clauses() 4236 switch (lit_value(solver, l)) { in simplify_clause() 4813 switch(lit_value(solver, l)) { in subst_and_simplify_binary_clause() 5600 switch (lit_value(solver, l)) { in pp_visit_clause() 6954 switch (lit_value(solver, l)) { in pp_add_unit_resolvent() 7564 vl = lit_value(solver, l); in propagate_from_literal() 7596 vl = lit_value(solver, l); in propagate_from_literal() 8544 val = lit_value(solver, l); [all …]
|
H A D | new_sat_solver.c | 3353 switch (lit_value(solver, l)) { in nsat_base_literal() 3778 switch (lit_value(solver, l)) { in nsat_solver_simplify_and_add_clause() 4523 switch (lit_value(solver, i)) { in simplify_binary_clauses() 4603 switch (lit_value(solver, l)) { in simplify_clause() 5187 switch(lit_value(solver, l)) { in subst_and_simplify_binary_clause() 5974 switch (lit_value(solver, l)) { in pp_visit_clause() 7836 switch (lit_value(solver, l)) { in pp_add_unit_resolvent() 8523 vl = lit_value(solver, l); in propagate_from_literal() 8552 vl = lit_value(solver, l); in propagate_from_literal() 9866 if (lit_value(solver, a[i]) == VAL_TRUE) { in saved_clause_is_false() [all …]
|
/dports/security/vaultwarden/vaultwarden-1.23.1/cargo-crates/diesel_derives-1.4.1/src/ |
H A D | meta.rs | 177 match *self.lit_value()? { in lit_str_value() 195 match *self.lit_value()? { in int_value() 202 fn lit_value(&self) -> Result<&syn::Lit, Diagnostic> { in lit_value() method
|
/dports/audio/gnome-podcasts/podcasts-c86f7bfdef7692bbf20f315a90450321f6ca9ce7/cargo-crates/diesel_derives-1.4.1/src/ |
H A D | meta.rs | 177 match *self.lit_value()? { in lit_str_value() 195 match *self.lit_value()? { in int_value() 202 fn lit_value(&self) -> Result<&syn::Lit, Diagnostic> { in lit_value() method
|
/dports/math/cvc3/cvc3-2.4.1/src/sat/ |
H A D | xchaff_solver.cpp | 211 int lit_value = literal_value(clause(new_cl).literal(i)); in add_clause() local 213 if (lit_value == 1) { in add_clause() 216 else if (lit_value != 0) { in add_clause() 544 int lit_value = literal_value (cl.literal(i)); in delete_unrelevant_clauses() local 545 if (lit_value == 0 ) ++val_0_lits; in delete_unrelevant_clauses() 546 else if (lit_value == 1) ++val_1_lits; in delete_unrelevant_clauses()
|
/dports/lang/yap/yap-6.2.2/packages/semweb/ |
H A D | sparql_client.pl | 293 lit_value(Content, Value), 306 lit_value([], ''). 307 lit_value([Value], Value).
|
/dports/lang/swi-pl/swipl-8.2.3/packages/semweb/ |
H A D | sparql_client.pl | 483 lit_value(Content, Value), 509 lit_value([], ''). 510 lit_value([Value], Value).
|
/dports/math/yices/yices-2.6.2/src/frontend/ |
H A D | yices_sat_new.c | 302 if (lit_value(&solver, a[i]) == VAL_TRUE) { in clause_is_true() 305 if (lit_value(&solver, a[i]) != VAL_FALSE) { in clause_is_true()
|
/dports/cad/stepcode/stepcode-0.8/test/misc/ |
H A D | select_segfault_210e3.exp | 253 lit_value : LOGICAL;
|
/dports/lang/rust/rustc-1.58.1-src/compiler/rustc_typeck/src/check/ |
H A D | check.rs | 1446 if let rustc_ast::LitKind::Int(lit_value, _int_kind) = &lit.node { in display_discriminant_value() 1447 if evaluated != *lit_value { in display_discriminant_value() 1448 return format!("`{}` (overflowed from `{}`)", evaluated, lit_value); in display_discriminant_value()
|
/dports/cad/stepcode/stepcode-0.8/data/ap235/ |
H A D | AP235_TC_engineering_properties_schema_20110222.exp | 559 lit_value : atom_based_value; 724 lit_value : BINARY; 2194 lit_value : LIST [1:?] OF INTEGER; 2440 lit_value : LOGICAL; 2575 lit_value : maths_enum_atom; 2614 lit_value : LIST OF maths_value; 3552 lit_value : LIST [1:?] OF REAL; 10151 (lit_value : BINARY ) : binary_literal; 10223 (lit_value : INTEGER ) : int_literal; 10274 (lit_value : REAL ) : real_literal; [all …]
|
/dports/cad/stepcode/stepcode-0.8/data/STEPTools_merged_schema/ |
H A D | modified_step_merged_cad_schema.exp.broken | 4750 lit_value : atom_based_value; 5156 lit_value : BINARY; 11314 lit_value : LIST [1:?] OF INTEGER; 12145 lit_value : LOGICAL; 12451 lit_value : maths_enum_atom; 12472 lit_value : LIST [0:?] OF maths_value; 15865 lit_value : LIST [1:?] OF REAL; 29818 (lit_value : BINARY ) : binary_literal; 29901 (lit_value : INTEGER ) : int_literal; 29978 (lit_value : REAL ) : real_literal; [all …]
|
/dports/cad/stepcode/stepcode-0.8/data/cd242/ |
H A D | 242_n2813_mim_lf.exp | 4368 lit_value : atom_based_value; 4794 lit_value : BINARY; 12008 lit_value : LOGICAL; 12458 lit_value : maths_enum_atom; 12484 lit_value : LIST OF maths_value; 28491 lit_value : BINARY 28498 lit_value : BOOLEAN 28595 lit_value : INTEGER 28611 lit_value : LOGICAL 28688 lit_value : REAL [all …]
|
/dports/cad/stepcode/stepcode-0.8/data/wip210e3/ |
H A D | 210e3_v1_47_mim_lf.exp | 7722 lit_value : LOGICAL; 10654 lit_value : LIST [1:?] OF INTEGER; 10660 lit_value : LIST [1:?] OF REAL; 10666 lit_value : atom_based_value; 10672 lit_value : BINARY; 10689 lit_value : maths_enum_atom; 15944 lit_value : LIST OF maths_value; 33021 || literal_number(lit_value) 33033 || literal_number(lit_value) 37449 RETURN (string_literal (lit_value) [all …]
|
/dports/cad/stepcode/stepcode-0.8/data/cd209/ |
H A D | part409cdts_wg3n2617mim_lf.exp | 6129 lit_value : LOGICAL; 6134 lit_value : BINARY; 6139 lit_value : maths_enum_atom; 6144 lit_value : LIST [1:?] OF REAL; 6149 lit_value : LIST [1:?] OF INTEGER; 6154 lit_value : atom_based_value; 6159 lit_value : LIST OF maths_value; 33266 || literal_number(lit_value) 33278 || literal_number(lit_value) 34356 RETURN (string_literal (lit_value) [all …]
|
/dports/devel/tigcc/tigcc-0.96.b8_10/gnu/binutils-2.16.1/bfd/ |
H A D | elf32-xtensa.c | 7570 const literal_value *lit_value, in move_shared_literal() argument 7638 ta_add_literal, target_loc, lit_value, -4); in move_shared_literal()
|
/dports/devel/djgpp-binutils/binutils-2.17/bfd/ |
H A D | elf32-xtensa.c | 7787 const literal_value *lit_value, in move_shared_literal() argument 7855 ta_add_literal, target_loc, lit_value, -4); in move_shared_literal()
|
/dports/math/yices/yices-2.6.2/src/solvers/bv/ |
H A D | new_bit_blaster.c | 496 return lit_value(s->solver, l); in base_value()
|
/dports/devel/arm-elf-binutils/binutils-2.37/bfd/ |
H A D | elf32-xtensa.c | 9314 const literal_value *lit_value, in move_shared_literal() argument 9382 ta_add_literal, target_loc, lit_value, -4); in move_shared_literal()
|
/dports/devel/gnulibiberty/binutils-2.37/bfd/ |
H A D | elf32-xtensa.c | 9314 const literal_value *lit_value, in move_shared_literal() argument 9382 ta_add_literal, target_loc, lit_value, -4); in move_shared_literal()
|