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 * INCREMENTAL FORM OF THE FLOYD-WARSHALL ALGORITHM FOR INTEGER DIFFERENCE LOGIC.
21 */
22
23 /*
24 * This solver is for integer difference logic only. It cannot be
25 * attached to the egraph.
26 *
27 * WARNING: All path length computations are done using signed 32bit
28 * integers. There's some check for this now (not very precise).
29 */
30
31 /*
32 * Graph representation
33 * - edges are stored in a stack (added and removed in FIFO order)
34 * - each edge has source and destination vertices and an integer cost
35 * - edges are indexed from 0 to n-1
36 * - edge 0 is not really an edge. It's used as a mark.
37 *
38 * Matrix:
39 * - for each pair of vertices (x, y), we maintain the distance from x to y and
40 * edge index M[x,y].id
41 * - for each vertex x, M[x, x].id = 0 and M[x, x].dist = 0
42 * - if there's no path from x to y, we set M[x, y] = null_edge (-1)
43 * - if there's a path from x to y then M[x, y].id is an index between 1 and n-1
44 * Invariant: a
45 * - if M[x, y].id = i and edge i is from u to v then
46 * 0 <= M[x, u].id < i and 0 <= M[u, y].id < i
47 *
48 * - Based on this, we can define the path from x to y represented by M
49 * path(x, y) =
50 * if x = y then empty-path
51 * else (concat path(x, u) i path(v, y))
52 * where i = M[x, y].id and that edge is from u to v.
53 *
54 * this recursion is well-founded by the Main invariant,
55 *
56 * Then the length of path(x, y) can also be computed recursively:
57 * len(x, y) = if x = y then 0 else len(x, u) + c(i) + len(v, y)
58 * where i = M[x, y].m_edge_id and edge i has cost c(i) and goes from u to v.
59 *
60 * That length is stored in M[x, y].dist
61 *
62 * - The data structure is constructed so that path(x, y) is a shortest
63 * path from x to y in the current graph.
64 * M[x, y].m_val is then the distance from x to y.
65 *
66 * The graph encodes the constraints asserted so far:
67 * - an edge from x to y of cost d encodes the assertion (x - y <= d)
68 * - if there's a path of length D from x to y, then the assertions imply (x - y <= D)
69 */
70
71
72 #ifndef __IDL_FLOYD_WARSHALL_H
73 #define __IDL_FLOYD_WARSHALL_H
74
75 #include <stdint.h>
76 #include <stdbool.h>
77 #include <stddef.h>
78 #include <setjmp.h>
79
80 #include "context/context_types.h"
81 #include "solvers/cdcl/smt_core.h"
82 #include "solvers/floyd_warshall/dl_vartable.h"
83 #include "terms/poly_buffer.h"
84 #include "utils/arena.h"
85 #include "utils/bitvectors.h"
86 #include "utils/int_hash_tables.h"
87 #include "utils/int_vectors.h"
88
89
90 /***********
91 * GRAPH *
92 **********/
93
94 /*
95 * Edge indices = signed 32 bit integers
96 * - null_idl_edge = -1 is a marker
97 * Vertex index = signed 32 bit integers
98 * - null_idl_vertex = -1
99 */
100 enum {
101 null_idl_edge = -1,
102 null_idl_vertex = -1,
103 };
104
105
106 /*
107 * Edge descriptor:
108 * - the cost is used only by the debugging function valid_idl_graph
109 */
110 typedef struct idl_edge_s {
111 int32_t source;
112 int32_t target;
113 #ifndef NDEBUG
114 int32_t cost;
115 #endif
116 } idl_edge_t;
117
118
119 /*
120 * Stack of edges + a literal for each edge
121 * - for edge i: lit[i] == true_literal if i was asserted as an axiom
122 * - otherwise lit[i] = a literal l in the smt_core, such that l is true
123 * and l is attached to an idl atom
124 */
125 typedef struct edge_stack_s {
126 uint32_t size;
127 uint32_t top;
128 idl_edge_t *data;
129 literal_t *lit;
130 } edge_stack_t;
131
132 #define DEFAULT_IDL_EDGE_STACK_SIZE 100
133 #define MAX_IDL_EDGE_STACK_SIZE (UINT32_MAX/sizeof(idl_edge_t))
134
135
136 /*
137 * Cell in the matrix
138 */
139 typedef struct idl_cell_s {
140 int32_t id; // edge index
141 int32_t dist;
142 } idl_cell_t;
143
144
145 /*
146 * Matrix:
147 * - data is an array of (size * size) cells
148 * - the matrix itself is stored in data[0 ... dim*dim-1]
149 */
150 typedef struct idl_matrix_s {
151 uint32_t size;
152 uint32_t dim;
153 idl_cell_t *data;
154 } idl_matrix_t;
155
156
157 /*
158 * Maximal dimension: we want (dim * x + y) to fit a 32bit unsigned integer
159 * where 0 <= x < dim and 0 <= y < dim
160 */
161 #define MAX_IDL_MATRIX_DIMENSION 65535
162
163
164 /*
165 * Stack for restoring cells in the matrix
166 */
167 typedef struct saved_cell_s {
168 uint32_t index; // cell index: M[x, y] has index (nvertices * x + y)
169 idl_cell_t saved; // content to restore
170 } saved_cell_t;
171
172 typedef struct cell_stack_s {
173 uint32_t size;
174 uint32_t top;
175 saved_cell_t *data;
176 } cell_stack_t;
177
178
179 #define DEFAULT_IDL_CELL_STACK_SIZE 100
180 #define MAX_IDL_CELL_STACK_SIZE (UINT32_MAX/sizeof(saved_cell_t))
181
182
183 /*
184 * Graph
185 */
186 typedef struct idl_graph_s {
187 idl_matrix_t matrix;
188 edge_stack_t edges;
189 cell_stack_t cstack;
190 ivector_t buffer;
191 } idl_graph_t;
192
193
194
195 /***********
196 * ATOMS *
197 **********/
198
199 /*
200 * Each atom has an index i (in the global atom table)
201 * - the atom includes <source vertex, target vertex, cost, boolean variable>
202 * - if atom->boolvar = v then the atom index is attached to v in the smt_core
203 * (Hack: this is done by converting the int32_t index to void*).
204 */
205 typedef struct idl_atom_s {
206 int32_t source;
207 int32_t target;
208 int32_t cost;
209 bvar_t boolvar;
210 } idl_atom_t;
211
212
213 /*
214 * Conversion from atom index to void* (and back)
215 * TODO: add a 2bit tag to make this consistent with the egraph
216 * tagging of atoms??
217 */
index2atom(int32_t i)218 static inline void *index2atom(int32_t i) {
219 return (void *) ((size_t) i);
220 }
221
atom2index(void * a)222 static inline int32_t atom2index(void *a) {
223 return (int32_t) ((size_t) a);
224 }
225
226
227 /*
228 * Record for doubly-linked list of free atoms
229 */
230 typedef struct idl_listelem_s {
231 int32_t pre;
232 int32_t next;
233 } idl_listelem_t;
234
235
236 /*
237 * Atom table: current set of atoms have indices between 0 and natoms-1
238 * For theory propagation, we maintain a list of free atoms
239 * (all atoms not assigned a truth value yet)
240 * - size = size of the atoms array
241 * - mark = one bit per atom
242 * mark = 1 means that the atom is assigned (present in the atom stack)
243 * mark = 0 means that the atom is unassigned (present in the free list)
244 * - free_list is an array of n+1 list elements, indexed from -1 to n-1
245 */
246 typedef struct idl_atbl_s {
247 uint32_t size;
248 uint32_t natoms;
249 idl_atom_t *atoms;
250 idl_listelem_t *free_list;
251 byte_t *mark;
252 } idl_atbl_t;
253
254
255 /*
256 * Atom stack & propagation queue:
257 * - for all assigned atom, the queue contains its index + a sign bit
258 * - this follows our usual encoding of index+sign in 32bit:
259 * sign bit = lowest order bit of data[k]
260 * if sign bit = 0, then atom k is true
261 * if sign bit = 1, then atom k is false
262 * - every atom in the stack has its mark bit set to 1 in the atom table
263 * - the propagation queue consists of the atoms in
264 * data[prop_ptr ... top -1]
265 */
266 typedef struct idl_astack_s {
267 uint32_t size;
268 uint32_t top;
269 uint32_t prop_ptr;
270 int32_t *data;
271 } idl_astack_t;
272
273
274
275 #define DEFAULT_IDL_ATBL_SIZE 100
276 #define MAX_IDL_ATBL_SIZE (UINT32_MAX/sizeof(idl_atom_t))
277
278 #define DEFAULT_IDL_ASTACK_SIZE 100
279 #define MAX_IDL_ASTACK_SIZE (UINT32_MAX/sizeof(int32_t))
280
281
282 /*
283 * Maximal number of atoms: same as MAX_IDL_ATBL_SIZE
284 * (so any atom index fits in 30 bits).
285 */
286 #define MAX_IDL_ATOMS MAX_IDL_ATBL_SIZE
287
288
289
290 /****************
291 * UNDO STACK *
292 ***************/
293
294 /*
295 * For backtracking: on entry to each decision level k we store:
296 * - edge_id = id of the first edge of level k
297 * for level 0, edge_id must be -1.
298 * for level k>0, edge_id is the number of edges in the graph
299 * when the level k was entered.
300 * - top of cell stack, top of atom stack
301 */
302 typedef struct idl_undo_record_s {
303 int32_t edge_id;
304 uint32_t nsaved;
305 uint32_t natoms;
306 } idl_undo_record_t;
307
308 typedef struct idl_undo_stack_s {
309 uint32_t size;
310 uint32_t top;
311 idl_undo_record_t *data;
312 } idl_undo_stack_t;
313
314 #define DEFAULT_IDL_UNDO_STACK_SIZE 100
315 #define MAX_IDL_UNDO_STACK_SIZE (UINT32_MAX/sizeof(idl_undo_record_t))
316
317
318
319
320 /******************
321 * PUSH/POP STACK *
322 *****************/
323
324 /*
325 * For each base level, we keep the number of vertices and atoms
326 * on entry to that level.
327 */
328 typedef struct idl_trail_s {
329 uint32_t nvertices;
330 uint32_t natoms;
331 } idl_trail_t;
332
333 typedef struct idl_trail_stack_s {
334 uint32_t size;
335 uint32_t top;
336 idl_trail_t *data;
337 } idl_trail_stack_t;
338
339 #define DEFAULT_IDL_TRAIL_SIZE 20
340 #define MAX_IDL_TRAIL_SIZE (UINT32_MAX/sizeof(idl_trail_t))
341
342
343
344
345 /***************************
346 * FLOYD-WARHSALL SOLVER *
347 **************************/
348
349 typedef struct idl_solver_s {
350 /*
351 * Attached smt core + gate manager
352 */
353 smt_core_t *core;
354 gate_manager_t *gate_manager;
355
356 /*
357 * Base level and decision level (same interpretation as in smt_core)
358 */
359 uint32_t base_level;
360 uint32_t decision_level;
361
362 /*
363 * Unsat flag: set to true if the asserted axioms are inconsistent
364 */
365 bool unsat_before_search;
366
367 /*
368 * Variable table
369 * - every variable (used by the context) is mapped to a
370 * difference logic triple (x - y + c) where x and y are vertices
371 * in the graph.
372 */
373 dl_vartable_t vtbl;
374
375 /*
376 * Graph
377 */
378 uint32_t nvertices; // number of vertices
379 int32_t zero_vertex; // index of zero vertex or null
380 idl_graph_t graph;
381
382 /*
383 * Atom table and stack
384 */
385 idl_atbl_t atoms;
386 idl_astack_t astack;
387
388 /*
389 * Backtracking stack
390 */
391 idl_undo_stack_t stack;
392
393 /*
394 * Push/pop stack
395 */
396 idl_trail_stack_t trail_stack;
397
398 /*
399 * Auxiliary buffers and data structures
400 */
401 int_htbl_t htbl; // for hash-consing of atoms
402 arena_t arena; // for storing explanations of implied atoms
403 ivector_t expl_buffer; // for constructing explanations
404 ivector_t aux_vector; // general-purpose vector
405
406 dl_triple_t triple; // for variable construction
407 poly_buffer_t buffer; // for internal polynomial operations
408
409 /*
410 * Variable assignment: allocated when needed in build_model
411 */
412 int32_t *value;
413
414 /*
415 * Jump buffer for exception handling during internalization
416 */
417 jmp_buf *env;
418 } idl_solver_t;
419
420
421
422 /*
423 * Maximal number of vertices: same as maximal matrix dimension
424 */
425 #define MAX_IDL_VERTICES MAX_IDL_MATRIX_DIMENSION
426
427 #define DEFAULT_IDL_BUFFER_SIZE 20
428
429
430
431
432 /*********************
433 * MAIN OPERATIONS *
434 ********************/
435
436 /*
437 * Initialize an idl solver
438 * - core = the attached smt-core object
439 * - gates = the attached gate manager
440 */
441 extern void init_idl_solver(idl_solver_t *solver, smt_core_t *core, gate_manager_t *gates);
442
443
444 /*
445 * Attach a jump buffer for internalization exception
446 */
447 extern void idl_solver_init_jmpbuf(idl_solver_t *solver, jmp_buf *buffer);
448
449
450 /*
451 * Delete: free all allocated memory
452 */
453 extern void delete_idl_solver(idl_solver_t *solver);
454
455
456 /*
457 * Get interface descriptors to attach solver to a core
458 */
459 extern th_ctrl_interface_t *idl_ctrl_interface(idl_solver_t *solver);
460 extern th_smt_interface_t *idl_smt_interface(idl_solver_t *solver);
461
462
463 /*
464 * Get interface descriptor for the internalization functions.
465 */
466 extern arith_interface_t *idl_arith_interface(idl_solver_t *solver);
467
468
469
470
471 /******************************
472 * VERTEX AND ATOM CREATION *
473 *****************************/
474
475 /*
476 * Create a new theory variable = a new vertex
477 * - return null_idl_vertex if there are too many vertices
478 */
479 extern int32_t idl_new_vertex(idl_solver_t *solver);
480
481
482 /*
483 * Return the zero_vertex (create it if needed)
484 * - return null_idl_vertex if the vertex can't be created
485 * (i.e. too many vertices)
486 */
487 extern int32_t idl_zero_vertex(idl_solver_t *solver);
488
489
490 /*
491 * Create the atom (x - y <= d) and return the corresponding literal
492 * - x and y must be vertices in the solver
493 * - if x - y <= d simplifies to true or false (given the current graph)
494 * return true_literal or false_literal
495 */
496 extern literal_t idl_make_atom(idl_solver_t *solver, int32_t x, int32_t y, int32_t d);
497
498
499 /*
500 * Assert (x - y <= d) as an axiom
501 * - x and y must be vertices in solver
502 * - the solver must be at base level (i.e., solver->decision_level == solver->base_level)
503 *
504 * - this adds an edge from x to y with cost d to the graph
505 * - if the edge causes a conflict, then solver->unsat_before_search is set to true
506 */
507 extern void idl_add_axiom_edge(idl_solver_t *solver, int32_t x, int32_t y, int32_t d);
508
509
510 /*
511 * Assert (x - y == d) as an axiom:
512 * - add edge x ---> y with cost d (x - y <= d)
513 * and edge y ---> x with cost -d (y - x <= -d)
514 */
515 extern void idl_add_axiom_eq(idl_solver_t *solver, int32_t x, int32_t y, int32_t d);
516
517
518
519
520
521 /*******************************
522 * INTERNALIZATION FUNCTIONS *
523 ******************************/
524
525 /*
526 * These functions are used by the context to convert terms to
527 * variables and literals. They form the arith_interface descriptor.
528 */
529
530 /*
531 * Create a new theory variable
532 * - is_int indicates whether the variable should be an integer,
533 * so it should always be true for this solver.
534 * - raise exception NOT_IDL if is_int is false
535 * - raise exception TOO_MANY_VARS if we can't create a new vertex
536 * for that variable
537 */
538 extern thvar_t idl_create_var(idl_solver_t *solver, bool is_int);
539
540
541 /*
542 * Create a variable that represents the constant q
543 * - raise an exception if q is not an integer
544 */
545 extern thvar_t idl_create_const(idl_solver_t *solver, rational_t *q);
546
547
548 /*
549 * Create a variable for a polynomial p, with variables defined by map:
550 * - p is of the form a_0 t_0 + ... + a_n t_n where t_0, ..., t_n
551 * are arithmetic terms.
552 * - map[i] is the theory variable x_i for t_i
553 * (with map[0] = null_thvar if t_0 is const_idx)
554 * - the function constructs a variable equal to a_0 x_0 + ... + a_n x_n
555 *
556 * - fails if a_0 x_0 + ... + a_n x_n is not an IDL polynomial
557 * (i.e., not of the form x - y + c)
558 */
559 extern thvar_t idl_create_poly(idl_solver_t *solver, polynomial_t *p, thvar_t *map);
560
561
562 /*
563 * Internalization for a product: always fails with NOT_IDL exception
564 */
565 extern thvar_t idl_create_pprod(idl_solver_t *solver, pprod_t *p, thvar_t *map);
566
567
568 /*
569 * Create the atom x = 0
570 */
571 extern literal_t idl_create_eq_atom(idl_solver_t *solver, thvar_t x);
572
573
574 /*
575 * Create the atom x >= 0
576 */
577 extern literal_t idl_create_ge_atom(idl_solver_t *solver, thvar_t x);
578
579
580 /*
581 * Create the atom p = 0
582 * - map is used as in create_poly
583 * - fails if p is not of the form (x - y + c)
584 */
585 extern literal_t idl_create_poly_eq_atom(idl_solver_t *solver, polynomial_t *p, thvar_t *map);
586
587
588 /*
589 * Create the atom p >= 0
590 * - map is used as in create_poly
591 * - fails if p is not of the form (x - y + c)
592 */
593 extern literal_t idl_create_poly_ge_atom(idl_solver_t *solver, polynomial_t *p, thvar_t *map);
594
595
596 /*
597 * Create the atom (x = y)
598 */
599 extern literal_t idl_create_vareq_atom(idl_solver_t *solver, thvar_t x, thvar_t y);
600
601
602 /*
603 * Assert the top-level constraint (x == 0) or (x != 0)
604 * - if tt is true: assert x == 0
605 * - if tt is false: assert x != 0
606 */
607 extern void idl_assert_eq_axiom(idl_solver_t *solver, thvar_t x, bool tt);
608
609
610 /*
611 * Assert the top-level constraint (x >= 0) or (x < 0)
612 * - if tt is true: assert (x >= 0)
613 * - if tt is false: assert (x < 0)
614 */
615 extern void idl_assert_ge_axiom(idl_solver_t *solver, thvar_t x, bool tt);
616
617
618 /*
619 * Assert the top-level constraint (p == 0) or (p != 0)
620 * - map is as in create_poly
621 * - if tt is true: assert p == 0
622 * - if tt is false: assert p != 0
623 * - fails if p is not of the form (x - y + c)
624 */
625 extern void idl_assert_poly_eq_axiom(idl_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt);
626
627
628 /*
629 * Assert the top-level constraint (p >= 0) or (p < 0)
630 * - map is as in create_poly
631 * - if tt is true: assert (p >= 0)
632 * - if tt is false: assert (p < 0)
633 * - fails if p is not of the form (x - y + c)
634 */
635 extern void idl_assert_poly_ge_axiom(idl_solver_t *solver, polynomial_t *p, thvar_t *map, bool tt);
636
637
638 /*
639 * Assert (x == y) or (x != y)
640 * - if tt is true: assert (x == y)
641 * - if tt is false: assert (x != y)
642 */
643 extern void idl_assert_vareq_axiom(idl_solver_t *solver, thvar_t x, thvar_t y, bool tt);
644
645
646 /*
647 * Assert (c ==> x == y)
648 */
649 extern void idl_assert_cond_vareq_axiom(idl_solver_t *solver, literal_t c, thvar_t x, thvar_t y);
650
651
652 /*
653 * Assert (c[0] \/ ... \/ c[n-1] \/ x == y)
654 */
655 extern void idl_assert_clause_vareq_axiom(idl_solver_t *solver, uint32_t n, literal_t *c, thvar_t x, thvar_t y);
656
657
658
659
660 /**********************
661 * SOLVER FUNCTIONS *
662 *********************/
663
664 /*
665 * These functions are used by the core. They form the th_ctrl and
666 * th_smt interfaces.
667 */
668
669 /*
670 * Start the search
671 */
672 extern void idl_start_search(idl_solver_t *solver);
673
674
675 /*
676 * Increase the decision level/backtrack
677 */
678 extern void idl_increase_decision_level(idl_solver_t *solver);
679 extern void idl_backtrack(idl_solver_t *solver, uint32_t back_level);
680
681
682 /*
683 * Push/pop/reset
684 */
685 extern void idl_push(idl_solver_t *solver);
686 extern void idl_pop(idl_solver_t *solver);
687 extern void idl_reset(idl_solver_t *solver);
688
689
690 /*
691 * Push an assertion into the queue
692 * - atom is the index of an idl_atom with boolean variable v
693 * - l is either pos_lit(v) or neg_lit(v)
694 * - if l == pos_lit(v), the atom is asserted true, otherwise it's false
695 * - return false if a conflict is detected
696 * return true otherwise
697 */
698 extern bool idl_assert_atom(idl_solver_t *solver, void *atom, literal_t l);
699
700
701 /*
702 * Propagate: process the assertion queue
703 * - return false if a conflict is detected
704 * - return true otherwise.
705 */
706 extern bool idl_propagate(idl_solver_t *solver);
707
708
709 /*
710 * Support for theory-branching heuristic
711 * - evaluate atom attached to l in the current model
712 * - the result is either l or (not l)
713 * - if atom is true, return pos_lit(var_of(l))
714 * - if atom is false, return neg_lit(var_of(l))
715 */
716 extern literal_t idl_select_polarity(idl_solver_t *solver, void *atom, literal_t l);
717
718
719 /*
720 * Final check: do nothing and return SAT
721 */
722 extern fcheck_code_t idl_final_check(idl_solver_t *solver);
723
724
725 /*
726 * Explain why literal l is true.
727 * - l is a literal set true by solver in the core (via implied_literal)
728 * - expl is the explanation object given to implied_literal,
729 * (expl is an array of literals terminated by null_literal).
730 * - expl must be expanded into a conjunction of literals l_0 ... l_k
731 * such that (l_0 and ... and l_k) implies l
732 * - literals l_0 ... l_k that must be stored into v
733 */
734 extern void idl_expand_explanation(idl_solver_t *solver, literal_t l, literal_t *expl, ivector_t *v);
735
736
737
738
739
740 /************************
741 * MODEL CONSTRUCTION *
742 ***********************/
743
744 /*
745 * Build a model: assign an integer value to all vertices
746 * - the zero vertex has value 0 (if it exists)
747 * - the solver must be in a consistent state
748 * - the mapping is stored internally in solver->value
749 */
750 extern void idl_build_model(idl_solver_t *solver);
751
752
753 /*
754 * Value of vertex x in the model
755 */
idl_vertex_value(idl_solver_t * solver,int32_t x)756 static inline int32_t idl_vertex_value(idl_solver_t *solver, int32_t x) {
757 assert(solver->value != NULL && 0 <= x && x < solver->nvertices);
758 return solver->value[x];
759 }
760
761
762 /*
763 * Value of variable v in the model
764 * - copy the value in rational q and return true
765 */
766 extern bool idl_value_in_model(idl_solver_t *solver, thvar_t v, rational_t *q);
767
768
769 /*
770 * Free the model
771 */
772 extern void idl_free_model(idl_solver_t *solver);
773
774
775
776 /*****************
777 * STATISTICS *
778 ****************/
779
780 // we don't maintain any search statistics
idl_num_vars(idl_solver_t * solver)781 static inline uint32_t idl_num_vars(idl_solver_t *solver) {
782 return solver->vtbl.nvars;
783 }
784
idl_num_atoms(idl_solver_t * solver)785 static inline uint32_t idl_num_atoms(idl_solver_t *solver) {
786 return solver->atoms.natoms;
787 }
788
idl_num_vertices(idl_solver_t * solver)789 static inline uint32_t idl_num_vertices(idl_solver_t *solver) {
790 return solver->nvertices;
791 }
792
793
794
795 #endif /* __IDL_FLOYD_WARSHALL_H */
796