CODEWITHSUNDEEP
z3
R4D4
R4D4

Reputation: 1402

Asserting a value if none exist

I am attempting to solve a rather tricky issue with Z3. It's not too relevant, but I am using the .NET bindings along with the latest nightly release of Z3.

I've summarised the problem, but please bear in mind the actual problem is rather more convoluted than this.

In a very brief statement any index of an array may be selected. I then add 1 to it, and the result is stored in any other index of the array. This is repeated as often as desired. At the end of this process an index is selected and we assert that it equals a particular value - and here lies the crux of the matter.

That final assertion will always succeed if the user doesn't assign a value to an index used in the calculation. For example:

(declare-const index1 Int)
(declare-const index2 Int)
(declare-const index3 Int)

;Index2 is assigned a value according to user selections.
(assert (= index2 2))
;Index3 is assigned a value according to user selections.
(assert (= index3 5))   
;User chooses index3 to hold a result. 
(assert (= index3 (+ index1 index2)))

(check-sat)
(get-model)

This problem is satisfiable, and results in index1 having the value 3 (index1 + 2 = 5), but the user has never specified a value for index1 - it's simply implied.

I can't outright assert that index1 should have an initial value of 0, as at runtime, the user may assign index1 a different value.

So, when I select an index from an array, or a selector function of a record, I am wanting to be able to say, this element should be 0, unless it is overwritten. This should then mean the above example would be unsatisfied.

Upvotes: 0

Views: 104

Answers (1)

alias
alias

Reputation: 30475

You can use an array to store the values, and make sure the initial values are 0. At each update, you'd get a new array with that modification:

(declare-const array0 (Array Int Int))
(assert (= array0 ((as const (Array Int Int)) 0)))

(declare-const index1 Int)
(declare-const index2 Int)
(declare-const index3 Int)

;; Index2 is assigned a value according to user selections:
(declare-const array1 (Array Int Int))
(assert (= array1 (store array0 index2 2)))

;; Index3 is assigned a value according to user selections:
(declare-const array2 (Array Int Int))
(assert (= array2 (store array1 index3 5)))

;; final assert:
(assert (= (select array2 index3) (+ (select array2 index1) (select array2 index2))))

The following code would "extract" the relevant values:

(check-sat)
(get-value (index1 index2 index3 (select array2 index1) (select array2 index2) (select array2 index3)))

Note how we used array2 since you had "two" transactions. In general, you'll have arrayN if you have N user-choices. (This is also known as single static assignment form, if you want to read upon that.)

If you try this, z3 will say:

sat
((index1 3)
 (index2 1)
 (index3 1)
 ((select array2 index1) 0)
 ((select array2 index2) 5)
 ((select array2 index3) 5))

Ah, z3 is too smart! It found a model by making sure index2 and index3 are the same. I suspect you intended the indices are distinct. Let's tell z3 that is indeed the case:

(assert (distinct index1 index2 index3))

Now (check-sat) returns:

unsat

Note that this is just one way to approach this problem. You can also keep it simple and get rid of the array by merely keeping track of which indices the user didn't make an assignment for and zero them out explicitly. But I think the array-based method is easier to use in general.

Upvotes: 1

Related Questions