最大递归必将在Z3

问题描述 投票：0回答：1

我写了下面的基准来生成两个列表的交叉产品。 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)
z3 smt
1个回答
0
投票

这实在是不正确的谈论在SMT求解器的背景下，“约束最大递归”。我可以看到你的倾向，称呼其为这样的;因为你希望它只会尽可能展开的定义是必要的。但是，这根本就不是一个SMT求解器是如何工作的。

在一般情况下，当你有一个递归函数它引起了一套量化的公理。 （您可以在http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 63页的翻译。）所以，你可能会认为是一个“功能”，实际上是一种短手写一堆量化公理。

请注意，您也有自己的量化公理，而所有的这些约束扎堆求解器去上班。不幸的是，这使得所述逻辑半可判定的;这意味着没有决策程序。 （A决策程序是一个永远终止，答案正确。）从理论上说，如果事情是不正确的，这意味着它总能找到一个“证明”，如果它最终会存在，但可以无限循环。然而，在实践中，这通常意味着它会循环足够在这两种情况下足够长的时间，要么你的耐心和您的计算机的内存会用完第一。

有迹象表明，与量词处理算法（如宏观发现和电子匹配）。但是，这些都是不完整的，在我的经验很脆。您也可以尝试通过提供量词实例化模式帮助Z3，在这里看到：https://rise4fun.com/z3/tutorialcontent/guide#h28。但是，该技术既不好用，也不在实践中扩展。

长话短说，SMT求解器只是不适合与量词的推理。和递归定义暗示量化。有既有理论限制，他们可以做什么，也实际考虑可用性，性能和诚实回报率投资：如果你想推理递归函数和递归数据类型，SMT求解器可以说是只是不正确工具。相反，使用定理-证明如HOL，伊莎贝尔，Coq的，阿格达，精益;等，它们被设计成具有这样的结构的工作。 （大多数这些工具可以自动调用SMT-求解代您办理简化的目标，所以你得到两全其美的。）

我希望这个解释是明确的。经验法则是，推理递归函数需要感应和电感证明需要必要的不变量的发明。 SMT求解器不能拿出你所需要的不变量，他们也允许你指定什么这些变量是，即使你愿意为他们提供。但是定理证明可以帮助你的状态并证明这些不变量;并且应当优选用于这样的问题。

最新问题
© www.soinside.com 2019 - 2024. All rights reserved.