在 smtlib 中定义列表 concat

Question

我基于 Haskell 定义了我自己的 list 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

Answer 2

alias 提出了有效的观点，但我不完全同意的最终结论“不要使用 SMT 求解器进行量化或递归定义的推理”。最后，这取决于您需要推理哪种属性，需要哪种答案（是 unsat/unknown OK，还是您需要 unsat/sat 和模型？），以及您做了多少工作愿意投资:-)

例如，Dafny 和 Viper 等基于 SMT 的程序验证器可以快速验证以下关于列表的断言：

assert [4] + [] == [4]; // holds
assert [4,1] + [1,4] == [4,1,1,4]; // holds
assert [4] + [1] == [1,4]; // fails

这两种工具都可以在线使用，但网站速度很慢，而且不太可靠。您可以找到Dafny example here 和Viper example here。

这是 Viper 生成的相关 SMT 代码：

(set-option :auto_config false) ; Usually a good idea
(set-option :smt.mbqi false)

;; The following definitions are an excerpt of Viper's sequence axiomatisation,
;; which is based on Dafny's sequence axiomatisation.
;; See also:
;;   https://github.com/dafny-lang/dafny
;;   http://viper.ethz.ch

(declare-sort Seq<Int>) ;; Monomorphised sort of integer sequences

(declare-const Seq_empty Seq<Int>)
(declare-fun Seq_length (Seq<Int>) Int)
(declare-fun Seq_singleton (Int) Seq<Int>)
(declare-fun Seq_index (Seq<Int> Int) Int)
(declare-fun Seq_append (Seq<Int> Seq<Int>) Seq<Int>)
(declare-fun Seq_equal (Seq<Int> Seq<Int>) Bool)

(assert (forall ((s Seq<Int>)) (!
  (<= 0 (Seq_length s))
  :pattern ((Seq_length s))
  )))

(assert (= (Seq_length (as Seq_empty  Seq<Int>)) 0))

(assert (forall ((s1 Seq<Int>) (s2 Seq<Int>)) (!
  (implies
    (and
      (not (= s1 (as Seq_empty  Seq<Int>)))
      (not (= s2 (as Seq_empty  Seq<Int>))))
    (= (Seq_length (Seq_append s1 s2)) (+ (Seq_length s1) (Seq_length s2))))
  :pattern ((Seq_length (Seq_append s1 s2)))
  )))

(assert (forall ((s Seq<Int>)) (!
  (= (Seq_append (as Seq_empty  Seq<Int>) s) s)
  :pattern ((Seq_append (as Seq_empty  Seq<Int>) s))
  )))

(assert (forall ((s Seq<Int>)) (!
  (= (Seq_append s (as Seq_empty  Seq<Int>)) s)
  :pattern ((Seq_append s (as Seq_empty  Seq<Int>)))
  )))

(assert (forall ((s1 Seq<Int>) (s2 Seq<Int>) (i Int)) (!
  (implies
    (and
      (not (= s1 (as Seq_empty  Seq<Int>)))
      (not (= s2 (as Seq_empty  Seq<Int>))))
    (ite
      (< i (Seq_length s1))
      (= (Seq_index (Seq_append s1 s2) i) (Seq_index s1 i))
      (= (Seq_index (Seq_append s1 s2) i) (Seq_index s2 (- i (Seq_length s1))))))
  :pattern ((Seq_index (Seq_append s1 s2) i))
  :pattern ((Seq_index s1 i) (Seq_append s1 s2))
  )))

(assert (forall ((s1 Seq<Int>) (s2 Seq<Int>)) (!
  (=
    (Seq_equal s1 s2)
    (and
      (= (Seq_length s1) (Seq_length s2))
      (forall ((i Int)) (!
        (implies
          (and (<= 0 i) (< i (Seq_length s1)))
          (= (Seq_index s1 i) (Seq_index s2 i)))
        :pattern ((Seq_index s1 i))
        :pattern ((Seq_index s2 i))
        ))))
  :pattern ((Seq_equal s1 s2))
  )))

(assert (forall ((s1 Seq<Int>) (s2 Seq<Int>)) (!
  (implies (Seq_equal s1 s2) (= s1 s2))
  :pattern ((Seq_equal s1 s2))
  )))

; ------------------------------------------------------------

; assert Seq(4) ++ Seq[Int]() == Seq(4)
(push)
(assert (not 
  (Seq_equal
    (Seq_append (Seq_singleton 4) Seq_empty)
    (Seq_singleton 4))))
(check-sat) ; unsat -- good!
(pop)

; assert Seq(4, 1) ++ Seq(1, 4) == Seq(4, 1, 1, 4)
(push)
(assert (not 
  (Seq_equal
    (Seq_append
      (Seq_append (Seq_singleton 4) (Seq_singleton 1))
      (Seq_append (Seq_singleton 1) (Seq_singleton 4)))
    (Seq_append
      (Seq_append
        (Seq_append (Seq_singleton 4) (Seq_singleton 1))
        (Seq_singleton 1))
      (Seq_singleton 4)))))
(check-sat) ; unsat -- good!
(pop)

; assert Seq(4) ++ Seq(1) == Seq(1, 4)
(push)
(assert (not (Seq_equal
  (Seq_append (Seq_singleton 4) (Seq_singleton 1))
  (Seq_append (Seq_singleton 1) (Seq_singleton 4)))))
(check-sat) ; unknown -- OK, since property doesn't hold
(pop)