Home
last modified time | relevance | path

Searched refs:fun_solver_t (Results 1 – 11 of 11) sorted by relevance

/dports/math/yices/yices-2.6.2/src/solvers/funs/
H A Dfun_solver.h325 } fun_solver_t; typedef
356 extern void delete_fun_solver(fun_solver_t *solver);
414 extern void fun_solver_start_search(fun_solver_t *solver);
419 extern bool fun_solver_propagate(fun_solver_t *solver);
426 extern fcheck_code_t fun_solver_final_check(fun_solver_t *solver);
442 extern void fun_solver_push(fun_solver_t *solver);
443 extern void fun_solver_pop(fun_solver_t *solver);
444 extern void fun_solver_reset(fun_solver_t *solver);
515 extern void fun_solver_free_model(fun_solver_t *solver);
558 static inline uint32_t fun_solver_num_vars(fun_solver_t *solver) { in fun_solver_num_vars()
[all …]
H A Dfun_solver_printer.h31 extern void print_fsolver_edge(FILE *f, fun_solver_t *solver, uint32_t edge_id);
32 extern void print_fsolver_edges(FILE *f, fun_solver_t *solver);
33 extern void print_fsolver_vars(FILE *f, fun_solver_t *solver);
34 extern void print_fsolver_roots(FILE *f, fun_solver_t *solver);
35 extern void print_fsolver_classes(FILE *f, fun_solver_t *solver);
36 extern void print_fsolver_apps(FILE *f, fun_solver_t *solver);
37 extern void print_fsolver_maps(FILE *f, fun_solver_t *solver);
38 extern void print_fsolver_base_values(FILE *f, fun_solver_t *solver);
39 extern void print_fsolver_diseqs(FILE *f, fun_solver_t *solver);
40 extern void print_fsolver_values(FILE *f, fun_solver_t *solver);
H A Dfun_solver.c1236 static void fun_solver_cleanup(fun_solver_t *solver) { in fun_solver_cleanup()
1750 static bool update_conflicts(fun_solver_t *solver) { in update_conflicts()
1896 void delete_fun_solver(fun_solver_t *solver) { in delete_fun_solver()
1929 void fun_solver_reset(fun_solver_t *solver) { in fun_solver_reset()
1996 void fun_solver_push(fun_solver_t *solver) { in fun_solver_push()
2011 void fun_solver_pop(fun_solver_t *solver) { in fun_solver_pop()
2060 void fun_solver_start_search(fun_solver_t *solver) { in fun_solver_start_search()
2079 bool fun_solver_propagate(fun_solver_t *solver) { in fun_solver_propagate()
2131 void fun_solver_clear(fun_solver_t *solver) { in fun_solver_clear()
3524 void fun_solver_free_model(fun_solver_t *solver) { in fun_solver_free_model()
[all …]
H A Dfun_solver_printer.c35 void print_fsolver_edge(FILE *f, fun_solver_t *solver, uint32_t edge_id) { in print_fsolver_edge()
60 void print_fsolver_edges(FILE *f, fun_solver_t *solver) { in print_fsolver_edges()
75 void print_fsolver_vars(FILE *f, fun_solver_t *solver) { in print_fsolver_vars()
98 void print_fsolver_roots(FILE *f, fun_solver_t *solver) { in print_fsolver_roots()
116 void print_fsolver_classes(FILE *f, fun_solver_t *solver) { in print_fsolver_classes()
141 void print_fsolver_apps(FILE *f, fun_solver_t *solver) { in print_fsolver_apps()
194 void print_fsolver_maps(FILE *f, fun_solver_t *solver) { in print_fsolver_maps()
223 void print_fsolver_base_values(FILE *f, fun_solver_t *solver) { in print_fsolver_base_values()
325 void print_fsolver_values(FILE *f, fun_solver_t *solver) { in print_fsolver_values()
357 void print_fsolver_diseqs(FILE *f, fun_solver_t *solver) { in print_fsolver_diseqs()
/dports/math/yices/yices-2.6.2/src/context/
H A Dcontext_statistics.c194 fun_solver_t *fsolver; in yices_show_statistics()
H A Dcontext_solver.c476 fun_solver_t *fsolver; in context_set_search_parameters()
H A Dcontext.c5301 fun_solver_t *solver; in create_fun_solver()
5305 solver = (fun_solver_t *) safe_malloc(sizeof(fun_solver_t)); in create_fun_solver()
/dports/math/yices/yices-2.6.2/src/frontend/
H A Dyices_smtcomp.c689 fun_solver_t *fsolver; in print_results()
H A Dyices_smt.c1209 fun_solver_t *fsolver; in print_results()
/dports/math/yices/yices-2.6.2/src/frontend/yices/
H A Dyices_reval.c1997 fun_solver_t *fsolver; in yices_showstats_cmd()
/dports/math/yices/yices-2.6.2/src/frontend/smt2/
H A Dsmt2_commands.c1580 static void show_funsolver_stats(int fd, print_buffer_t *b, fun_solver_t *solver) { in show_funsolver_stats()