/dports/math/yices/yices-2.6.2/src/solvers/cdcl/ |
H A D | smt_core.h | 1060 } smt_core_t; typedef 1163 extern void reset_smt_core(smt_core_t *s); 1197 extern void smt_push(smt_core_t *s); 1208 extern void smt_pop(smt_core_t *s); 1604 extern bool smt_easy_sat(smt_core_t *s); 1671 extern bool base_propagate(smt_core_t *s); 1700 extern void stop_search(smt_core_t *s); 1717 extern void smt_restart(smt_core_t *s); 1798 extern void smt_process(smt_core_t *s); 1881 extern void smt_cleanup(smt_core_t *s); [all …]
|
H A D | smt_core_printer.h | 47 extern void print_unit_clauses(FILE *f, smt_core_t *core); 48 extern void print_binary_clauses(FILE *f, smt_core_t *core); 49 extern void print_problem_clauses(FILE *f, smt_core_t *core); 50 extern void print_learned_clauses(FILE *f, smt_core_t *core); 51 extern void print_clauses(FILE *f, smt_core_t *core); 52 extern void print_all_clauses(FILE *f, smt_core_t *core); 53 extern void print_lemmas(FILE *f, smt_core_t *core); 58 extern void print_boolean_assignment(FILE *f, smt_core_t *core); 59 extern void print_conflict(FILE *f, smt_core_t *core); 60 extern void print_smt_core(FILE *f, smt_core_t *core);
|
H A D | smt_core.c | 54 static void check_heap(smt_core_t *s); 56 static void check_marks(smt_core_t *s); 1670 void reset_smt_core(smt_core_t *s) { in reset_smt_core() 5069 void smt_push(smt_core_t *s) { in smt_push() 5326 void smt_pop(smt_core_t *s) { in smt_pop() 5384 void smt_cleanup(smt_core_t *s) { in smt_cleanup() 5395 void smt_clear(smt_core_t *s) { in smt_clear() 5912 void stop_search(smt_core_t *s) { in stop_search() 5985 void smt_process(smt_core_t *s) { in smt_process() 6039 bool smt_easy_sat(smt_core_t *s) { in smt_easy_sat() [all …]
|
H A D | smt_core_printer.c | 154 void print_unit_clauses(FILE *f, smt_core_t *core) { in print_unit_clauses() 229 void print_binary_clauses(FILE *f, smt_core_t *core) { in print_binary_clauses() 262 void print_problem_clauses(FILE *f, smt_core_t *core) { in print_problem_clauses() 266 void print_learned_clauses(FILE *f, smt_core_t *core) { in print_learned_clauses() 270 void print_clauses(FILE *f, smt_core_t *core) { in print_clauses() 277 void print_all_clauses(FILE *f, smt_core_t *core) { in print_all_clauses() 305 void print_lemmas(FILE *f, smt_core_t *core) { in print_lemmas() 329 void print_boolean_assignment(FILE *f, smt_core_t *core) { in print_boolean_assignment() 348 void print_conflict(FILE *f, smt_core_t *core) { in print_conflict() 385 void print_smt_core(FILE *f, smt_core_t *core) { in print_smt_core()
|
H A D | gates_manager.c | 34 void init_gate_manager(gate_manager_t *m, smt_core_t *core) { in init_gate_manager() 61 static void assert_ordef_clauses(smt_core_t *s, literal_t l, ivector_t *v) { in assert_ordef_clauses() 134 smt_core_t *s; in mk_or_gate() 189 smt_core_t *s; in mk_and_gate() 247 static literal_t assert_xordef2(smt_core_t *s, literal_t l1, literal_t l2) { in assert_xordef2() 271 static literal_t assert_xordef_clauses(smt_core_t *s, ivector_t *v) { in assert_xordef_clauses() 355 smt_core_t *s; in mk_xor_gate() 428 smt_core_t *s; in assert_xor() 495 smt_core_t *s; in mk_ite_aux() 553 smt_core_t *s; in mk_ite_gate() [all …]
|
H A D | delegate.c | 479 static void copy_unit_clauses(delegate_t *d, smt_core_t *core) { in copy_unit_clauses() 495 static void copy_binary_clauses(delegate_t *d, smt_core_t *core) { in copy_binary_clauses() 552 static void copy_problem_clauses(delegate_t *d, smt_core_t *core) { in copy_problem_clauses() 565 static void mark_atom_variables(delegate_t *d, smt_core_t *core) { in mark_atom_variables() 667 static void export_gate_definitions(delegate_t *d, smt_core_t *core) { in export_gate_definitions() 687 smt_status_t solve_with_delegate(delegate_t *d, smt_core_t *core) { in solve_with_delegate() 702 smt_status_t preprocess_with_delegate(delegate_t *d, smt_core_t *core) { in preprocess_with_delegate()
|
H A D | delegate.h | 133 extern smt_status_t solve_with_delegate(delegate_t *delegate, smt_core_t *core); 141 extern smt_status_t preprocess_with_delegate(delegate_t *delegate, smt_core_t *core);
|
H A D | gates_manager.h | 44 smt_core_t *core; 68 extern void init_gate_manager(gate_manager_t *m, smt_core_t *core);
|
/dports/math/yices/yices-2.6.2/src/context/ |
H A D | context_solver.c | 71 static void trace_start(smt_core_t *core) { in trace_start() 79 static void trace_restart(smt_core_t *core) { in trace_restart() 101 static void trace_done(smt_core_t *core) { in trace_done() 473 smt_core_t *core; in context_set_search_parameters() 570 smt_core_t *core; in check_context() 595 smt_core_t *core; in check_context_with_assumptions() 635 smt_core_t *core; in precheck_context() 669 smt_core_t *core; in check_with_delegate() 728 smt_core_t *core; in bitblast_then_export_to_dimacs() 782 smt_core_t *core; in process_then_export_to_dimacs() [all …]
|
H A D | context_statistics.c | 166 smt_core_t *core; in yices_print_presearch_stats() 191 smt_core_t *core; in yices_show_statistics()
|
/dports/math/yices/yices-2.6.2/tests/unit/ |
H A D | test_egraph_base.c | 44 static void init_solver(egraph_t *egraph, smt_core_t *core) { in init_solver() 54 static void delete_solver(egraph_t *egraph, smt_core_t *core) { in delete_solver() 62 static void reset_solver(egraph_t *egraph, smt_core_t *core) { in reset_solver() 70 static void print_solver(egraph_t *egraph, smt_core_t *core) { in print_solver() 88 static void print_solver_details(egraph_t *egraph, smt_core_t *core) { 102 static smt_core_t core;
|
H A D | test_gate_manager.c | 522 smt_core_t *core; in test2() 614 smt_core_t *core; in test3() 672 smt_core_t *core; in check_xor_models() 698 smt_core_t *core; in check_iff_models() 723 smt_core_t *core; in check_ite_models() 749 smt_core_t *core; in check_or_models() 777 smt_core_t *core; in check_and_models() 805 smt_core_t *core; in check_xor2_assertion() 826 smt_core_t *core; in check_xor3_assertion() 848 smt_core_t *core; in check_xor5_assertion() [all …]
|
H A D | test_core3.c | 154 static void init_sat_solver(smt_core_t *core, uint32_t n) { in init_sat_solver() 166 static void sat_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *reduce_threshold, doubl… in sat_search() 203 static void show_progress(smt_core_t *core, in show_progress() 229 static void sat_solve(smt_core_t *core, core_param_t *params, bool verbose) { in sat_solve() 295 static void validate_assignment(smt_core_t *core) { in validate_assignment() 380 static int build_instance(char *filename, smt_core_t *core) { in build_instance() 495 static void print_problem_size(FILE *f, smt_core_t *core, char *filename, double construction_time)… in print_problem_size() 543 static void print_results(smt_core_t *core, double construction_time, double search_time) { in print_results() 590 static smt_core_t solver;
|
H A D | test_core2.c | 146 static void init_sat_solver(smt_core_t *core, uint32_t n) { in init_sat_solver() 157 static void sat_search(smt_core_t *core, uint32_t conflict_bound, uint32_t reduce_threshold) { in sat_search() 188 static void show_progress(smt_core_t *core, in show_progress() 214 static void sat_solve(smt_core_t *core, core_param_t *params, bool verbose) { in sat_solve() 283 static void validate_assignment(smt_core_t *core) { in validate_assignment() 368 static int build_instance(char *filename, smt_core_t *core) { in build_instance() 483 static void print_problem_size(FILE *f, smt_core_t *core, char *filename, double construction_time)… in print_problem_size() 537 static void print_results(smt_core_t *core, double construction_time, double search_time) { in print_results() 584 static smt_core_t solver;
|
H A D | test_core.c | 37 smt_core_t *core; 188 static smt_core_t core;
|
H A D | test_smt_blaster.c | 258 static int32_t smt_core_export(smt_core_t *core, const char *filename) {
|
/dports/math/yices/yices-2.6.2/src/solvers/bv/ |
H A D | dimacs_printer.c | 97 static void dimacs_print_unit_clauses(FILE *f, smt_core_t *core) { in dimacs_print_unit_clauses() 109 static void dimacs_print_binary_clauses(FILE *f, smt_core_t *core) { in dimacs_print_binary_clauses() 142 static void dimacs_print_problem_clauses(FILE *f, smt_core_t *core) { in dimacs_print_problem_clauses() 153 static void dimacs_print_all_clauses(FILE *f, smt_core_t *core) { in dimacs_print_all_clauses() 163 static void dimacs_print_header(FILE *f, smt_core_t *core) { in dimacs_print_header() 176 static void dimacs_print_full_header(FILE *f, smt_core_t *core) { in dimacs_print_full_header() 191 void dimacs_print_core(FILE *f, smt_core_t *core) { in dimacs_print_core() 201 void dimacs_print_full_core(FILE *f, smt_core_t *core) { in dimacs_print_full_core()
|
H A D | dimacs_printer.h | 71 extern void dimacs_print_core(FILE *f, smt_core_t *core); 78 extern void dimacs_print_full_core(FILE *f, smt_core_t *core);
|
H A D | bvsolver_types.h | 286 smt_core_t *core;
|
H A D | bit_blaster.h | 96 smt_core_t *solver; 131 extern void init_bit_blaster(bit_blaster_t *blaster, smt_core_t *solver, remap_table_t *remap);
|
H A D | bvsolver.h | 37 extern void init_bv_solver(bv_solver_t *solver, smt_core_t *core, egraph_t *egraph);
|
/dports/math/yices/yices-2.6.2/src/solvers/simplex/ |
H A D | arith_atomtable.h | 154 smt_core_t *core; 178 extern void init_arith_atomtable(arith_atomtable_t *table, smt_core_t *core);
|
/dports/math/yices/yices-2.6.2/src/solvers/funs/ |
H A D | fun_solver.h | 209 smt_core_t *core; 349 extern void init_fun_solver(fun_solver_t *solver, smt_core_t *core,
|
/dports/math/yices/yices-2.6.2/src/solvers/floyd_warshall/ |
H A D | idl_floyd_warshall.h | 353 smt_core_t *core; 441 extern void init_idl_solver(idl_solver_t *solver, smt_core_t *core, gate_manager_t *gates);
|
H A D | rdl_floyd_warshall.h | 382 smt_core_t *core; 479 extern void init_rdl_solver(rdl_solver_t *solver, smt_core_t *core, gate_manager_t *gates);
|