Не удается определить рекурсивный тип с массивом в Z3

Question

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

(declare-datatypes() 
    ((Tree 
     (leaf (content Int)) 
     (node (left Tree) (right Tree))))) 

Но я не могу определить следующее. Нужно ли сначала объявить что-то? Или, если это не позволяет, как получить эквивалентное определение (где один конструктор имеет произвольные поля того же типа, индексированные целыми числами)?

(declare-datatypes() 
    ((Tree 
     (leaf (content Int)) 
     (node (children (Array Int Tree)))))) 

Answer 1

Это (четыре года) вопрос очень тесно связан с вашими: "a datatype contains a set in Z3". В ответах на этот вопрос Леонардо де Мора говорит, что это невозможно, и Николай Бьёрнер дает очень подробное объяснение того, как можно обойти ограничение. Возможно, вы знаете, что они написали оригинальную бумагу, представляющую Z3 в 2008 году, см. Z3: An Efficient SMT Solver. Если нам повезет, возможно, один из них проверит, что рекурсивно перемешивающие массивы и типы данных по-прежнему не поддерживаются в Z3.

Кроме того, то, о чем вы просите, очень похоже на пример дерева, представленный под заголовком «Взаимно рекурсивные типы данных» в rise4fun Z3 tutorial, за исключением того, что ваш вопрос использует массив, в то время как в примере на boost4fun используется список. Интересно, можно ли изменить пример с поддержкой list4fun для добавления индекса в каждый узел списка. Что-то вроде этого:

(declare-datatypes() ((Tree leaf (node (value Int) (children TreeList))) 
         (TreeList nil (cons (car Tree) (cdr TreeList) (index Int))))) 
(assert 
    (forall ((treeList TreeList)) 
     (implies 
      (and 
       (distinct treeList nil) 
       (distinct (cdr treeList) nil) 
      ) 
      (= 
       (index (cdr treeList)) 
       (+ 1 (index treeList)) 
      ) 
     ) 
    ) 
) 
(check-sat) 

К сожалению, Z3 дает unsat для этого примера, так что, очевидно, что-то здесь не так.