Home
last modified time | relevance | path

Searched refs:smt_core_t (Results 1 – 25 of 50) sorted by relevance

12

/dports/math/yices/yices-2.6.2/src/solvers/cdcl/
H A Dsmt_core.h1060 } 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 Dsmt_core_printer.h47 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 Dsmt_core.c54 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 Dsmt_core_printer.c154 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 Dgates_manager.c34 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 Ddelegate.c479 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 Ddelegate.h133 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 Dgates_manager.h44 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 Dcontext_solver.c71 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 Dcontext_statistics.c166 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 Dtest_egraph_base.c44 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 Dtest_gate_manager.c522 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 Dtest_core3.c154 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 Dtest_core2.c146 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 Dtest_core.c37 smt_core_t *core;
188 static smt_core_t core;
H A Dtest_smt_blaster.c258 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 Ddimacs_printer.c97 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 Ddimacs_printer.h71 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 Dbvsolver_types.h286 smt_core_t *core;
H A Dbit_blaster.h96 smt_core_t *solver;
131 extern void init_bit_blaster(bit_blaster_t *blaster, smt_core_t *solver, remap_table_t *remap);
H A Dbvsolver.h37 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 Darith_atomtable.h154 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 Dfun_solver.h209 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 Didl_floyd_warshall.h353 smt_core_t *core;
441 extern void init_idl_solver(idl_solver_t *solver, smt_core_t *core, gate_manager_t *gates);
H A Drdl_floyd_warshall.h382 smt_core_t *core;
479 extern void init_rdl_solver(rdl_solver_t *solver, smt_core_t *core, gate_manager_t *gates);

12