使用数据类型和 forall 在 SMT-LIB 中对小型编程语言进行建模和分析 [英] Modeling a small programming language and analysis in SMT-LIB using datatypes and forall

问题描述

我正在尝试在 SMT-LIB 2 中对一种小型编程语言进行建模.我的意图是表达一些程序分析问题并用Z3解决它们.我想我误解了 forall 声明.这是我的代码片段.

I am trying to model a small programming language in SMT-LIB 2. My intent is to express some program analysis problems and solve them with Z3. I think I am misunderstanding the forall statement though. Here is a snippet of my code.

; 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 barrier.smt2 我得到 unsat 结果.我认为我的分析问题的一个实例是一系列 forall 像上面这样的断言和一系列带有描述输入程序的断言的 const 声明.

When I run z3 -smt2 barriers.smt2 I get unsat as the result. I am thinking that an instance of my analysis problem would be a series of forall assertions like the above and a series of const declarations with assertions that describe the input program.

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

但显然我错误地使用了 forall 表达式，因为我希望 z3 决定该断言有一个令人满意的模型.我错过了什么?

But apparently I am using the forall expression incorrectly because I expected z3 to decide that there was a satisfying model for that assertion. What am I missing?

推荐答案

当你像这样声明一个 datatype 时:

When you declare a datatype like this:

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

您正在生成一个自由"生成的宇宙.这只是说对于笛卡尔积Int x Int x Int x Int 中每个可能元素的Barrier 都有一个值.

you are generating a universe that is "freely" generated. That's just a fancy word for saying there is a value for Barrier for each possible element in the cartesian product Int x Int x Int x Int.

稍后，当你说:

(assert
  (forall ((b1 Barrier) (b2 Barrier))
          (=> (= (group b1) (group b2))
              (= (complete-time b1) (complete-time b2)))))

您正在对 b1 和 b2 的所有可能值进行断言，并且您是说如果组相同，则完成时间必须相同.但是请记住，数据类型是自由生成的，因此 z3 会告诉您 unsat，这意味着通过选择 b1 和 b2 的正确值显然违反了您的断言来自那个笛卡尔积，它有很多违反这个断言的居民对.

you are making an assertion about all possible values of b1 and b2, and you are saying that if groups are the same then completion times must be the same. But remember that datatypes are freely generated so z3 tells you unsat, meaning that your assertion is clearly violated by picking up proper values of b1 and b2 from that cartesian product, which have plenty of inhabitant pairs that violate this assertion.

当然，你想说的是:我只是想让你关注那些满足这个属性的元素.我不关心其他的."但这就是不是你说的.为此，只需将断言转换为函数即可:

What you were trying to say, of course, was: "I just want you to pay attention to those elements that satisfy this property. I don't care about the others." But that's not what you said. To do so, simply turn your assertion to a function:

(define-fun groupCompletesTogether ((b1 Barrier) (b2 Barrier)) Bool
   (=> (= (group b1) (group b2))
       (= (complete-time b1) (complete-time b2))))

然后，将其用作您的含义的假设.这是一个愚蠢的例子:

then, use it as the hypothesis of your implications. Here's a silly example:

(declare-const b00 Barrier)
(declare-const b01 Barrier)

(assert (=> (groupCompletesTogether b00 b01)
            (> (rank b00) (rank b01))))
(check-sat)
(get-model)

打印:

sat
(model
  (define-fun b01 () Barrier
    (barrier 3 0 2437 1797))
  (define-fun b00 () Barrier
    (barrier 2 1 1236 1796))
)

这不是一个特别有趣的模型，但它仍然是正确的.我希望这可以解释这个问题，并使您走上正确的建模之路.您也可以将该谓词与其他事实结合使用，我怀疑在 sat 场景中，这确实是您想要的.所以，你可以说:

This isn't a particularly interesting model, but it is correct nonetheless. I hope this explains the issue and sets you on the right path to model. You can use that predicate in conjunction with other facts as well, and I suspect in a sat scenario, that's really what you want. So, you can say:

(assert (distinct b00 b01))
(assert (and (= (group b00) (group b01))
             (groupCompletesTogether b00 b01)
             (> (rank b00) (rank b01))))

你会得到以下模型:

sat
(model
  (define-fun b01 () Barrier
    (barrier 3 2436 0 1236))
  (define-fun b00 () Barrier
    (barrier 2 2437 0 1236))
)

现在变得更有趣了！

一般来说，虽然 SMTLib 确实支持量词，但您应该尽量远离它们，因为它会使逻辑变得半可判定.一般而言，您只想编写量化公理，就像您为未解释的常量所做的那样.(也就是说，引入一个新的函数/常数，让它不被解释，但要断言它应该满足的普遍量化的公理.)这可以让你对一堆有趣的函数进行建模，尽管量词可以让求解器做出响应 未知，所以如果可以，最好避免使用它们.

In general, while SMTLib does support quantifiers, you should try to stay away from them as much as possible as it renders the logic semi-decidable. And in general, you only want to write quantified axioms like you did for uninterpreted constants. (That is, introduce a new function/constant, let it go uninterpreted, but do assert a universally quantified axiom that it should satisfy.) This can let you model a bunch of interesting functions, though quantifiers can make the solver respond unknown, so they are best avoided if you can.

[旁注:根据经验，当你在一个自由生成的数据类型(比如你的 Barrier)上写一个量化公理时，它要么是微不足道的，要么永远不会被满足，因为宇宙实际上将包含一切可以以这种方式构建.把它想象成 Haskell/ML 等中的数据类型；它只是一个包含所有可能值的容器.]

[Side note: As a rule of thumb, When you write a quantified axiom over a freely-generated datatype (like your Barrier), it'll either be trivially true or will never be satisfied because the universe literally will contain everything that can be constructed in that way. Think of it like a datatype in Haskell/ML etc.; where it's nothing but a container of all possible values.]

这篇关于使用数据类型和 forall 在 SMT-LIB 中对小型编程语言进行建模和分析的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！