1 /* 2 * This file is part of the Yices SMT Solver. 3 * Copyright (C) 2017 SRI International. 4 * 5 * Yices is free software: you can redistribute it and/or modify 6 * it under the terms of the GNU General Public License as published by 7 * the Free Software Foundation, either version 3 of the License, or 8 * (at your option) any later version. 9 * 10 * Yices is distributed in the hope that it will be useful, 11 * but WITHOUT ANY WARRANTY; without even the implied warranty of 12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 13 * GNU General Public License for more details. 14 * 15 * You should have received a copy of the GNU General Public License 16 * along with Yices. If not, see <http://www.gnu.org/licenses/>. 17 */ 18 19 /* 20 * PRINTER FOR THE RDL FLOYD-WARSHALL SOLVER 21 */ 22 23 #ifndef __RDL_FW_PRINTER_H 24 #define __RDL_FW_PRINTER_H 25 26 #include <stdio.h> 27 28 #include "solvers/floyd_warshall/rdl_floyd_warshall.h" 29 30 31 /* 32 * Name of vertex x 33 */ 34 extern void print_rdl_vertex(FILE *f, int32_t x); 35 36 /* 37 * RDL constant c (q + k.delta) 38 */ 39 extern void print_rdl_const(FILE *f, rdl_const_t *c); 40 41 /* 42 * Value of vertex x in the graph 43 * - this prints distance[0, x] as the value 44 * - of ??? if there's no path from 0 to x 45 */ 46 extern void print_rdl_vertex_value(FILE *f, rdl_solver_t *rdl, int32_t x); 47 48 /* 49 * Atom in format: [<boolvar> := (x - y <= const)] 50 */ 51 extern void print_rdl_atom(FILE *f, rdl_atom_t *atom); 52 extern void print_rdl_atoms(FILE *f, rdl_solver_t *rdl); 53 54 55 /* 56 * Difference logic triple (x - y + d) 57 * - x and y are vertices 58 */ 59 extern void print_rdl_triple(FILE *f, dl_triple_t *triple); 60 61 62 /* 63 * Variable triples: in the format u := (x - y + d) 64 * - x and y are vertices 65 * - u is a theory variable 66 */ 67 extern void print_rdl_var_name(FILE *f, thvar_t u); 68 extern void print_rdl_var_def(FILE *f, rdl_solver_t *solver, thvar_t u); 69 extern void print_rdl_var_table(FILE *f, rdl_solver_t *solver); 70 71 72 /* 73 * Edges 74 */ 75 extern void print_rdl_axioms(FILE *f, rdl_solver_t *solver); 76 extern void print_rdl_edges(FILE *f, rdl_solver_t *solver); 77 78 79 80 #endif 81