CODEWITHSUNDEEP
z3smt
Jivan
Jivan

Reputation: 23068

Partially interpreted Const in z3

In z3, one can declare a fully-uninterpreted const like so:

(declare-const x Int)

Similarly, one can define a fully-interpreted one like this:

(define-fun y () Int 3)
; y == 3

Given an algebraic datatype, one can have a fully interpreted tuple like the following:

(declare-datatypes () ((Item (mk-item (size Int) (weight Int)))))
(define-fun z () Item (mk-item 3 4))
; z == Item(size=3, weight=4)

... Or a non-interpreted one like below:

(declare-const i1 (Item Int Int))

Now is it possible to have a partially-interpreted data type, so that, based on the previous example, weight would be fixed for each item and size could vary?

; (bad syntax, but I hope you get the idea)
; in this case the size is varying, but weight is fixed to 5
(declare-const i2 (Item Int 5))

Upvotes: 1

Views: 87

Answers (1)

alias
alias

Reputation: 30428

You should simply declare it with declare-fun and assert an equality for the portions that you know:

(declare-datatypes () ((Item (mk-item (size Int) (weight Int)))))

(declare-fun x () Item)
(assert (= (weight x) 5))

(check-sat)
(get-model)

This produces:

sat
(model
  (define-fun x () Item
    (mk-item 0 5))
)

Upvotes: 2

Related Questions