CODEWITHSUNDEEP
z3
yollo
yollo

Reputation: 41

Encoding self-dependent relations in Z3

I was wondering if there is an easy way to represented the following dependencies in Z3:

x = 0
y = x + 1
y = y + 10

Thanks!

Upvotes: 1

Views: 43

Answers (1)

alias
alias

Reputation: 30428

y = y + 10 is always unsatisfiable. I'm guessing you intend these to model a series of assignments, as in an imperative programming language? In that case, you should convert it to static single assignment form (https://en.wikipedia.org/wiki/Static_single_assignment_form). That is, model it as follows:

x0 = 1
y0 = x0 + 1
y1 = y0 + 10

Upvotes: 1

Related Questions