Записи с Z3

Question

Я довольно внимательно посмотрел документацию и руководства и сам попробовал несколько вещей. Однако решение моих проблем уклоняется от меня.

Это то, что говорит учебник о записях, но мне не ясно, как иметь его удовлетворить мои потребности:

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 
(declare-const p1 (Pair Int Int)) 
(declare-const p2 (Pair Int Int)) 

Ищу синтаксис SMT-Lib2 для объявления записи из 5 полей, 2-х и 3-х уровней.

Я хотел бы иметь массив/набор этих записей.

Кроме того, я искал синтаксис, который я использовал бы для создания оператора $ \ forall $ над некоторым набором записей.

Я старался изо всех сил с предоставленными ресурсами и никуда не денусь.

Спасибо.

Answer 1

Вот как вы можете создать запись с 2 Интсом и 3 BOOLS:

(declare-datatypes() ((R5 (mk-R5 (el1 Int) (el2 Int) (el3 Bool) (el4 Bool) (el5 Bool))))) 

(declare-const r1 R5) 
(declare-const r2 R5) 

(assert (not (= r1 r2))) 

(check-sat) 
(get-model) 

Z3 отвечает:

sat 
(model 
    (define-fun r2() R5 
    (mk-R5 1 0 false false false)) 
    (define-fun r1() R5 
    (mk-R5 0 0 false false false)) 
) 

Надеется, что это будет, чтобы вы начали. Что касается кванторов, то он будет похож на все остальные квантификаторы; Лучше всего задавать конкретные вопросы, чтобы получить лучшие ответы.