Частично интерпретируемый Const в z3

В z3 можно объявить полностью неинтерпретируемый const следующим образом:

(declare-const x Int)

Точно так же можно определить полностью интерпретируемый следующим образом:

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

Учитывая алгебраический тип данных, можно получить полностью интерпретируемый кортеж, подобный следующему:

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

... Или неинтерпретируемый, как показано ниже:

(declare-const i1 (Item Int Int))

Теперь возможно иметь частично интерпретируемый тип данных, чтобы, основываясь на предыдущем примере, weight было бы фиксированным для каждого элемента, а size могло бы различаться?

; (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))

z3 smt
person Jivan    schedule 26.11.2017    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Вы должны просто объявить это с помощью declare-fun и подтвердить равенство для частей, которые вы знаете:

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

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

(check-sat)
(get-model)

Это производит:

sat
(model
  (define-fun x () Item
    (mk-item 0 5))
)
person alias    schedule 27.11.2017