максимальная рекурсивная граница в z3

Question

Я написал тест ниже, чтобы сгенерировать перекрестное произведение двух списков.Есть ли у z3 какая-то максимальная рекурсивная граница?По какой-то причине это может привести к спискам размером 1, но не размером 2. Или, возможно, у меня есть ошибка где-то в моей формализации?

(declare-datatypes ((MyList 1)) ((par (T) ((cons (head T) (tail (MyList T))) (nil)))))
(declare-datatypes (T2) ((Pair (pair (first T2) (second T2)))))

; list functions for lists of ints
(define-fun prepend ( (val (Pair Int)) (l (MyList (Pair Int))) ) (MyList (Pair Int)) (cons val l))

(declare-fun get ( (MyList Int) Int ) Int)
(assert (forall ( (h Int) (t (MyList Int)) (i Int) )
                (ite (<= i 0)
                     (= (get (cons h t) i) h)
                     (= (get (cons h t) i) (get t (- i 1))))))

(declare-fun list_length ( (MyList Int) ) Int)
(assert (= (list_length (as nil (MyList Int))) 0))
(assert (forall ( (val Int) (l (MyList Int)) )
                (= (list_length (cons val l)) (+ 1 (list_length l)))))

(declare-fun tail ( (MyList Int) Int ) (MyList Int))
(assert (forall ( (start Int) (h Int) (t (MyList Int)) )
                (ite (<= start 0)
                     (= (tail (cons h t) start) (cons h t))
                     (= (tail (cons h t) start) (tail t (- start 1))))))
(assert (forall ( (start Int) )
                (= (tail (as nil (MyList Int)) start) (as nil (MyList Int)))))


; same list functions but for lists of int pairs -- 
; would be great if there is a way to avoid redefining all these again :(
(declare-fun list_get_pair ( (MyList (Pair Int)) Int ) (Pair Int))
(assert (forall ( (h (Pair Int)) (t (MyList (Pair Int))) (i Int) )
                (ite (<= i 0)
                     (= (list_get_pair (cons h t) i) h)
                     (= (list_get_pair (cons h t) i) (list_get_pair t (- i 1))))))

(declare-fun list_length_pair ( (MyList (Pair Int)) ) Int)
(assert (= (list_length_pair (as nil (MyList (Pair Int)))) 0))
(assert (forall ( (val (Pair Int)) (l (MyList (Pair Int))) )
                (= (list_length_pair (cons val l)) (+ 1 (list_length_pair l)))))

(declare-fun tail_pair ( (MyList (Pair Int)) Int ) (MyList (Pair Int)))
(assert (forall ( (start Int) (h (Pair Int)) (t (MyList (Pair Int))) )
                (ite (<= start 0)
                     (= (tail_pair (cons h t) start) (cons h t))
                     (= (tail_pair (cons h t) start) (tail_pair t (- start 1))))))
(assert (forall ( (start Int) )
                (= (tail_pair (as nil (MyList (Pair Int))) start) (as nil (MyList (Pair Int))))))

(declare-fun concat ( (MyList (Pair Int)) (MyList (Pair Int)) ) (MyList (Pair Int)))
(assert (forall ((xs (MyList (Pair Int))) (ys (MyList (Pair Int))))
            (ite (= (as nil (MyList (Pair Int))) xs)
                 (= (concat xs ys) ys)
                 (= (concat xs ys) (prepend (list_get_pair xs 0) (concat (tail_pair xs 1) ys))))))                 

(assert (forall ((xs (MyList (Pair Int))) (ys (MyList (Pair Int))))
            (=> (= (as nil (MyList (Pair Int))) ys)
                (= (concat xs ys) xs))))

; two functions defined using recursive construct                
(define-funs-rec
(
(cross_helper ((i Int) (ys (MyList Int))) (MyList (Pair Int)))
(cross ((xs (MyList Int)) (ys (MyList Int))) (MyList (Pair Int)))
)
(
; cross_helper - given e and [a, b, c] return [(e,a), (e,b), (e,c)]
(ite (= ys (as nil (MyList Int))) (as nil (MyList (Pair Int)))
     (prepend (pair i (get ys 0)) (cross_helper i (tail ys 1))))


; cross - given [a, b] and [c, d] return [(a,c), (a,d), (b,c) (b,d)]
(ite (= xs (as nil (MyList Int))) (as nil (MyList (Pair Int)))
     (concat (cross_helper (get xs 0) ys) (cross (tail xs 1) ys)))
))


(declare-const in1 (MyList Int)) (declare-const in2 (MyList Int))
(declare-const i Int) (declare-const j Int)
(declare-const in11 Int) (declare-const in12 Int) 
(declare-const in21 Int) (declare-const in22 Int)


; this works
; cross([in11], [in21, in22]) = ([in11, in21], [in11, in22])
(push)
(assert (= in1 (cons in11 (as nil (MyList Int)))))
(assert (= in2 (cons in21 (cons in22 (as nil (MyList Int))))))

(assert (not (= (cross in1 in2) (cons (pair in11 in21) (cons (pair in11 in22)                               
                                                            (as nil (MyList (Pair Int))))))))
(check-sat) (pop)

; but this doesn't work
; cross([in11, in12], [in21, in22]) = ([in11, in21], [in11, in22], [in12, in21], [in12, in22])
(push)
(assert (= in1 (cons in11 (cons in22 (as nil (MyList Int))))))
(assert (= in2 (cons in21 (cons in22 (as nil (MyList Int))))))

(assert (not (= (cross in1 in2) (cons (pair in11 in21) (cons (pair in11 in22)
                               (cons (pair in12 in21) (cons (pair in12 in22)
                                                            (as nil (MyList (Pair Int))))))))))
(check-sat) (pop)

Answer 1

Неверно говорить о «максимальной рекурсивной границе» в контексте решателя SMT.Я вижу вашу склонность называть это так;как вы надеетесь, это просто развернет определения по мере необходимости.Но это просто не то, как работает SMT-решатель.

В общем, когда у вас есть рекурсивная функция, она индуцирует набор количественных аксиом.(Вы можете найти перевод на странице 63 из http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf.) Итак, то, что вы можете рассматривать как «функцию», на самом деле является сокращением для написания набора количественных аксиом.

Обратите внимание, что вытакже есть ваши собственные количественные аксиомы, и все эти ограничения собираются вместе, и решатель начинает работать. К сожалению, это делает логику полуразрешимой; это означает, что процедуры принятия решения не существует. (Процедура принятия решений - это процедура, которая всегда завершается и отвечает правильно.) Теоретически это означает, что он всегда может найти «доказательство», если оно существует в конце концов, но может зацикливаться бесконечно, если что-то не так. Однако на практике это обычно означает, что в обоих случаях цикл будет достаточно продолжительным,Ваше терпение или память вашего компьютера истощатся первыми.

Существуют алгоритмы (такие как поиск макросов и электронное сопоставление), которые имеют дело с квантификаторами, но все они обязательно неполные, и, по моему опыту, довольно хрупкие.Вы также можете попытаться помочь z3, предоставив шаблоны для квантификатора i.nstantiation, см. здесь: https://rise4fun.com/z3/tutorialcontent/guide#h28. Но метод не прост в использовании и не масштабируется на практике.

Короче говоря, решатели SMT просто не годятся для рассуждений с квантификаторами.А рекурсивные определения подразумевают количественную оценку.Существуют как теоретические ограничения на то, что они могут сделать, так и практические соображения относительно удобства использования, производительности и честного возврата инвестиций: если вы хотите рассуждать о рекурсивных функциях и рекурсивных типах данных, решатели SMT, возможно, просто не подходятинструмент.Вместо этого используйте доказательство теорем, таких как HOL, Изабель, Coq, Agda, Lean;и т. д., которые предназначены для работы с такими конструкциями.(Большинство из этих инструментов могут автоматически вызывать SMT-решатель от вашего имени для упрощенных целей; поэтому вы получаете лучшее из обоих миров.)

Надеюсь, это объяснение понятно.Практическое правило состоит в том, что рассуждение о рекурсивных функциях требует индукции, а индуктивные доказательства требуют изобретения необходимых инвариантов.Решатели SMT не могут придумать для вас требуемые инварианты и не позволяют вам указать, что это за инварианты, даже если вы готовы их предоставить.Но доказатели теорем могут помочь вам сформулировать и доказать эти инварианты;и должен быть предпочтительным для таких проблем.