| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
| H A D | AbcGlucose.cpp | 78 int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits) in glucose_solver_addclause()
100 int glucose_solver_solve(Gluco::SimpSolver* S, int * plits, int nlits) in glucose_solver_solve()
155 int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits) in bmcg_sat_solver_addclause()
165 int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits) in bmcg_sat_solver_solve()
253 int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ) in bmcg_sat_solver_minimize_assumptions()
345 int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits) in glucose_solver_addclause()
367 int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits) in glucose_solver_solve()
417 int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits) in bmcg_sat_solver_addclause()
427 int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits) in bmcg_sat_solver_solve()
515 int bmcg_sat_solver_minimize_assumptions( bmcg_sat_solver * s, int * plits, int nlits, int pivot ) in bmcg_sat_solver_minimize_assumptions()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/satoko/ |
| H A D | solver_api.c | 347 int satoko_solve_assumptions(solver_t *s, int * plits, int nlits) in satoko_solve_assumptions()
364 int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim) in satoko_solve_assumptions_limit()
372 int satoko_minimize_assumptions(satoko_t * s, int * plits, int nlits, int nconflim) in satoko_minimize_assumptions()
|
| /dports/math/vampire/vampire-4.5.1/Inferences/ |
| H A D | TautologyDeletionISE.cpp | 43 static DArray<Literal*> nlits(32); // array of negative literals in simplify() local
|
| /dports/math/yices/yices-2.6.2/tests/unit/ |
| H A D | test_remap_table.c | 131 uint32_t nlits; member
|
| /dports/math/picosat/picosat-965/ |
| H A D | picosat.c | 44 /* By default we 'detach satisfied (large) clauses', e.g. NDSC undefined.
|
| /dports/misc/otter/otter-3.3f/source/ |
| H A D | resolve.c | 807 int m, i, nlits, j, nuc_pos; in ur_res() local
|
| /dports/cad/nvc/nvc-r1.5.3/src/ |
| H A D | common.c | 384 const int nlits = type_enum_literals(base); in parse_value() local
|
| H A D | simp.c | 326 const int nlits = type_enum_literals(type); in simp_attr_ref() local
|
| H A D | bounds.c | 697 unsigned nlits, low, high; in bounds_check_case() local
|
| H A D | sem.c | 590 const int nlits = type_enum_literals(type); in scope_import_decls() local
1323 const int nlits = type_enum_literals(type); in sem_declare() local
4750 const int nlits = type_enum_literals(elem); in sem_is_character_array() local
4779 const int nlits = type_enum_literals(elem); in sem_check_string_literal() local
5149 const unsigned nlits = type_enum_literals(index_type); in sem_check_aggregate() local
|
| H A D | lower.c | 2670 const int nlits = type_enum_literals(base); in lower_image_map() local
|
| /dports/devel/plan9port/plan9port-1f098efb7370a0b28306d10681e21883fb1c1507/src/libflate/ |
| H A D | deflate.c | 214 static ulong nlits; variable
|
| /dports/math/SCIP/scip-7.0.3/src/scip/ |
| H A D | conflict.c | 5312 int nlits; in conflictCreateReconvergenceConss() local
5475 int nlits; in conflictAnalyze() local
5590 int nlits; in conflictAnalyze() local
|
| /dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
| H A D | smt_core.h | 957 uint32_t nlits; // Number of literals = twice the number of variables member
|
| H A D | smt_core.c | 5178 uint32_t i, m, nlits; in restore_clauses() local
|
| /dports/math/z3/z3-z3-4.8.13/src/smt/ |
| H A D | theory_pb.cpp | 2058 uint_set nlits; in validate_assign() local
|
| /dports/math/py-z3-solver/z3-z3-4.8.10/src/smt/ |
| H A D | theory_pb.cpp | 2058 uint_set nlits; in validate_assign() local
|
| /dports/cad/nvc/nvc-r1.5.3/src/rt/ |
| H A D | rtkern.c | 1407 int nlits; in rt_memo_resolution_fn() local
|