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-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
. 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