が部分的にZ3でZ3

Question

でのConstを解釈、一方がそうのような完全に解釈constを宣言することができ：考える

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

：

(declare-const x Int) 

同様に、一つはこのような完全解釈いずれかを定義することができ代数的データ型の場合、次のような完全に解釈されたタプルを持つことができます。

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

Answer 1

あなたは、単にdeclare-funでそれを宣言し、あなたが知っている部分について平等を主張する必要があります。

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

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

(check-sat) 
(get-model) 

これが生成します。

​​ を