CODEWITHSUNDEEP
arraysz3smtquantifiers
user8616916
user8616916

Reputation: 73

z3 with quantifiers and arrays, along with corresponding C code for Seahorn

The below program returns unsat when ran on z3.

(assert ( forall ( (y (Array Int Int)) ) 
   (= (select y 1) 0) 
))
(check-sat)

I don't get, what does the line "forall" actually mean; Does it mean, for all arrays - Int y [Int], is there a possibility of y[1] == 0 ? If yes, then SAT, else UNSAT ? Why is z3 returning unsat, when I run the above code ?

Here's the C code that I wrote for Seahorn, corresponding to the above smt2 file.

#include "seahorn/seahorn.h"
extern int nd();

int main(void){

int n = nd();

assume(n>0);

int y[n]; 

for(int i = 0; i < n; i++)
{
    sassert(y[1]=0);        
}

}

I converted the C code to smt2 file using Seahorn and then formatted it using format.py, from CHC Comp 2020, and then ran z3 on the formatted file which gives - unsat.

Although, the answer of both the files is same, I don't think, this is correct code. The original smt2 file says "Forall array y", whereas, my c code says, "for all elements in an array y". How do I write the correct c code for this problem?

[Please note: I referred z3's tutorial, but still, am not clear]

Upvotes: 0

Views: 201

Answers (1)

alias
alias

Reputation: 30475

The meaning of this assertion:

(assert ( forall ( (y (Array Int Int)) ) 
   (= (select y 1) 0) 
))

is: For all arrays y indexed by integers and containing integers, the element in position 1 is always 0.

And clearly that is unsatisfiable. There are many arrays where the element in position 1 is not 0, so your quantified assertion fails and you get unsat as the answer.

Note that any universally quantified axiom over arrays is bound to be unsatisfiable unless it states something trivial: What property can you write that is true for all such arrays? There aren't many.

It's hard to guess what you're trying to do, but in general what you want to say is I have an array, and I know that its first element is 0. If that's the case, use an existential. Any variable declared at the top-level in an SMTLib query is assumed to be existential. Like this:

(declare-fun A () (Array Int Int))

; assert first element of `A` is `0`
(assert (= (select A 1) 0))

; .. now add other constraints, etc.

This approach essentially tells z3 to consider all arrays A such that they have a 0 in their 1st position; and is typical of what software verification tasks usually involve. (Where that constraint will stem from the "initialization" part of your program.)

Upvotes: 2

Related Questions