使用数据类型和forall在SMT-LIB中建模小型编程语言并进行分析

Question

我正在尝试在SMT-LIB 2中为小型编程语言建模。我的目的是表达一些程序分析问题，并使用Z3解决它们。我想我虽然误解了forall语句。这是我的代码的片段。

; barriers.smt2

(declare-datatype Barrier ((barrier (proc Int) (rank Int) (group Int) (complete-time Int))))

; barriers in the same group complete at the same time
(assert
  (forall ((b1 Barrier) (b2 Barrier))
          (=> (= (group b1) (group b2))
              (= (complete-time b1) (complete-time b2)))))
(check-sat)

[运行z3 -smt2 barriers.smt2时，我得到的是unsat。我认为我的分析问题的一个实例将是像上面的一系列forall断言，以及一系列带有描述输入程序的断言的const声明。

(declare-const b00 Barrier)
(assert (= (proc b00) 0))
(assert (= (rank b00) 0))
...

但是显然我没有正确使用forall表达式，因为我希望z3可以确定该断言有令人满意的模型。我想念什么？

Answer 1

(declare-sort Barrier 0)
(declare-fun proc (Barrier) Int)
(declare-fun rank (Barrier) Int)
(declare-fun group (Barrier) Int)
(declare-fun complete-time (Barrier) Int)

然后坐下forall断言。我仍然很乐意解释为什么此更改有所作为。