Home
last modified time | relevance | path

Searched refs:lit_value (Results 1 – 25 of 39) sorted by relevance

12

/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/satoko/
H A Dsolver.c46 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 Dsolver.h178 static inline char lit_value(solver_t *s, unsigned lit) in lit_value() function
H A Dsolver_api.c41 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 Dnew_sat_solver2.h1135 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 Dnew_sat_solver.h1298 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 Dnew_sat_solver2.c2977 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 Dnew_sat_solver.c3353 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 Dmeta.rs177 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 Dmeta.rs177 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 Dxchaff_solver.cpp211 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 Dsparql_client.pl293 lit_value(Content, Value),
306 lit_value([], '').
307 lit_value([Value], Value).
/dports/lang/swi-pl/swipl-8.2.3/packages/semweb/
H A Dsparql_client.pl483 lit_value(Content, Value),
509 lit_value([], '').
510 lit_value([Value], Value).
/dports/math/yices/yices-2.6.2/src/frontend/
H A Dyices_sat_new.c302 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 Dselect_segfault_210e3.exp253 lit_value : LOGICAL;
/dports/lang/rust/rustc-1.58.1-src/compiler/rustc_typeck/src/check/
H A Dcheck.rs1446 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 DAP235_TC_engineering_properties_schema_20110222.exp559 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 Dmodified_step_merged_cad_schema.exp.broken4750 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 D242_n2813_mim_lf.exp4368 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 D210e3_v1_47_mim_lf.exp7722 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 Dpart409cdts_wg3n2617mim_lf.exp6129 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 Delf32-xtensa.c7570 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 Delf32-xtensa.c7787 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 Dnew_bit_blaster.c496 return lit_value(s->solver, l); in base_value()
/dports/devel/arm-elf-binutils/binutils-2.37/bfd/
H A Delf32-xtensa.c9314 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 Delf32-xtensa.c9314 const literal_value *lit_value, in move_shared_literal() argument
9382 ta_add_literal, target_loc, lit_value, -4); in move_shared_literal()

12