在smtlib中定义列表concat

Question

我基于Haskell定义了自己的列表concat版本，如下所示：

(declare-datatypes ((MyList 1))
                   ((par (T) ((cons (head T) (tail (MyList T))) (nil)))))
(declare-fun my-concat ( (MyList T1) (MyList T1) ) (MyList T1))
(assert (forall ((xs (MyList T1)) (ys (MyList T1)) (x T1))
            (ite (= (as nil (MyList T1)) xs)
                 (= (my-concat xs ys) ys)
                 (= (my-concat (cons x xs) ys) (cons x (my-concat xs ys))))))

我想知道为什么z3无法推理以下内容？

(assert (not (= (my-concat (cons 4 (as nil (MyList Int))) (as nil (MyList Int))) 
                (cons 4 (as nil (MyList Int))))))
(check-sat) ; runs forever

Answer 1

加载文件

如果我按照您给的程序将程序加载到z3，它会显示：

(error "line 3 column 33: Parsing function declaration. Expecting sort list '(': unknown sort 'T1'")
(error "line 4 column 29: invalid sorted variables: unknown sort 'T1'")
(error "line 8 column 79: unknown function/constant my-concat")

这是因为您不能在SMTLib中定义“多态”函数。在用户级别，仅允许完全单态函数。 （尽管SMTLib内部确实提供了多态常量，但用户无法实际创建任何多态常量。）

所以，我不确定您如何加载该文件。

单态化

看起来您无论如何都只关心整数列表，所以让我们修改程序以处理整数列表。此过程称为单态化，通常在您到达SMT求解器之前由某些前端工具自动完成，具体取决于您正在使用的框架。这只是一种说法，可以创建所有多态实例使用单类型的常量。 （自从您提到Haskell以来，我就提出，虽然通常可以进行单态化，但这并不总是可行的：可能会有太多的变体生成它，因此不切实际。此外，如果您具有多态递归，那么单态化就不会工作。但这暂时是题外话。）

如果我将您的程序仅变形为Int，则会得到：

(declare-datatypes ((MyList 1))
                   ((par (T) ((cons (head T) (tail (MyList T))) (nil)))))
(declare-fun my-concat ( (MyList Int) (MyList Int) ) (MyList Int))
(assert (forall ((xs (MyList Int)) (ys (MyList Int)) (x Int))
            (ite (= (as nil (MyList Int)) xs)
                 (= (my-concat xs ys) ys)
                 (= (my-concat (cons x xs) ys) (cons x (my-concat xs ys))))))
(assert (not (= (my-concat (cons 4 (as nil (MyList Int))) (as nil (MyList Int)))
                (cons 4 (as nil (MyList Int))))))
(check-sat)
(get-info :reason-unknown)

当我在上面运行z3时，我得到：

unknown
(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)")

所以，它根本不会像您提到的那样循环；但是您的文件并没有真正加载。因此，也许您也正在处理文件中的其他内容，但这是当前问题的题外话。

但是它仍然不能证明它！

当然，您想要unsat这个简单的公式！但是z3表示它很难处理。未知的原因是“不完整的量词”。这是什么意思？

简而言之，SMTLib本质上是多种一阶公式的逻辑。对于该逻辑的无量词片段，求解器是“完整的”。但是添加量词会使逻辑变得不可确定。这意味着，如果您提供足够的资源，并且在发挥智能启发法的作用，则求解器最终会说出sat表示可满足的公式，但是如果给出unsat则可能会永远循环。 （它可能会很幸运，也说unsat，但很可能会循环播放。）

上面的情况有充分的理由，但是请记住，这与z3无关：带量词的一阶逻辑是半确定的。 （这里是开始阅读的好地方：https://en.wikipedia.org/wiki/Decidability_(logic)#Semidecidability）

然而，在实践中通常会发生的是，求解器甚至不会回答sat，只会像上面z3那样放弃并说unknown。一般而言，量词根本超出了SMT求解器的能力范围。您可以尝试使用模式（针对量词和模式触发器的搜索堆栈溢出），但这通常是徒劳的，因为使用模式和触发器非常棘手，并且可能非常脆弱。

您有什么行动方法：

老实说，这是“放弃”是很好的建议的情况之一。 SMT求解器只是不适合解决此类问题。使用定理证明者，例如Isabelle，ACL2，Coq，HOL，HOL-Light，Lean等，您可以在其中表达量词和递归函数并进行推理。他们是为这种事情而建造的。不要期望您的SMT求解器能够处理这类查询。这不是正确的匹配。

还是，我有什么可以做的吗？

您可以尝试使用SMTLib的递归函数定义工具。您会写：

(declare-datatypes ((MyList 1))
                   ((par (T) ((cons (head T) (tail (MyList T))) (nil)))))

(define-fun-rec my-concat ((xs (MyList Int)) (ys (MyList Int))) (MyList Int)
    (ite (= (as nil (MyList Int)) xs)
         ys
         (cons (head xs) (my-concat (tail xs) ys))))

(assert (not (= (my-concat (cons 4 (as nil (MyList Int))) (as nil (MyList Int)))
                (cons 4 (as nil (MyList Int))))))
(check-sat)

请注意define-fun-rec构造，该构造允许递归定义。瞧，我们得到：

unsat

但是这确实不是意味着z3将能够证明有关此concat函数的任意定理。如果尝试任何需要感应的操作，它将放弃（说unknown）或永远循环。当然，随着功能的改进，在z3或其他SMT求解器中可能会提供类似归纳法的证明，但这确实超出了它们的设计意图。因此，请谨慎使用。

您可以在http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf的第4.2.3节中阅读有关递归定义的更多信息>

总结

请勿将SMT求解器用于具有量化或递归定义的推理。他们只是没有必要的能力来处理此类问题，而且他们不太可能到达那里。对于这些任务，请使用适当的定理证明者。请注意，大多数定理证明者都使用SMT求解器作为基本策略，因此您可以两全其美：可以做一些手动工作来指导归纳证明，并让证明者使用SMT求解器来处理大多数目标。自动为您服务。以下是一篇不错的文章，可帮助您开始详细操作：https://people.mpi-inf.mpg.de/~jblanche/jar-smt.pdf