Enconding a transitive closure in Z3 (routing)

Oct 17, 2016 at 10:36 PM

I would like to encode a routing problem using z3.
So simplifiedt he problem is the following:
  • I have a number of Nodes that are connected with each other by edges
  • Each edge has a weight, that is basically the communication cost
  • I would like to encode the topology only by provindng the cost for the neihbours
  • The cost of should be calculated over a transitive relation, but i m not sure how to encode this.
  • In the example i have a very simple topology consisting of 4 nodes, x, y,z, v and they are connected like: x->y->z->v
so i want z3 to find automatically the cost of communication between x and v, which should be the sum of the edges in between. Is there a elegant way to encode this?

Maybe there is a smarter way to encode such routing problem .. do u have any examples?

Here the start of my encoding:

(declare-sort A)
(declare-const x A)
(declare-const y A)
(declare-const z A)
(declare-const v A)
(declare-fun path (A A) Int)
(assert (= (path x y) 1))
(assert (= (path y z) 2))
(assert (= (path z v) 3))
Oct 26, 2016 at 12:15 PM
This discussion board is not in use anymore as Z3 has moved to GitHub. Could you please try to reproduce the error using the latest master branch source code from GitHub and, if it still exists, submit a new issue in our new issue tracker? Thanks!