CODEWITHSUNDEEP
z3smt
hodophile
hodophile

Reputation: 367

While loop for Z3 or Smt2

How to convert a simple while loop(c- code) to smt2 language or z3? For ex :

int x,a;
while(x > 10 && x < 100){
    a = x + a;
    x++;
}

Upvotes: 9

Views: 3310

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

The input language to an SMT solver is first-order logic (with theories) and as such has no notion of computational operations such as loops.

You can

  • either use a loop invariant to encode an arbitrary loop iteration (and the pre- and post-state of the loop) and prove your relevant properties with respect to that arbitrary iteration, which is what deductive program verifiers such as Boogie, Dafny or Viper do

  • or, if the number of iterations is statically known, you unroll the loop and basically use single static assignment form to encode the different unrollings

For your loop, the latter would look as follows (not using proper SMT syntax here because I'm lazy):

declare x0, a0 // initial values
declare a1, x1 // values after first unrolling
x0 > 10 && x0 < 100 ==> a1 == a0 + x0 && x1 == x0 + 1
declare a2, x2 // values after second unrolling
x1 > 10 && x1 < 100 ==> a2 == a1 + x1 && x2 == x1 + 1
...

Upvotes: 7

Related Questions