触发器，Z3中的#in

我的问题来自large Boogie file。我会在这里解释相关的部分。触发器，Z3中的#in

对于有7个字段tID, stype, bal, acc, mbal, mval, val的消息，我声明一个新类型Msg。这些字段在Boogie中声明为函数。然后我声明了72个Msg常量M1, ..., M72及其相应的字段值。你可以看到下面的例子：

type Msg; 
const unique M1: Msg; 

function tID (Msg) returns (int); 
function stype (Msg) returns (Str); 
function bal (Msg) returns (int); 
function acc (Msg) returns (Proc); 
function mbal (Msg) returns (int); 
function mval (Msg) returns (Val); 
function val (Msg) returns (Val); 

axiom (tID (M1) == 1); 
axiom (stype (M1) == s1a); 
axiom (bal (M1) == 1); 
axiom (acc (M1) == ProcNull); 
axiom (mbal (M1) == -2); 
axiom (mval (M1) == ValNull); 
axiom (val (M1) == ValNull);

其中Proc, Str一些类型和s1a, ProcNull, ValNull是一些常量。然后我宣布一个公理，它说当两个信息m1, m2相等当且仅当m1, m2的每个字段。这个公理使用触发器MsgComp(m1, m2)。

function MsgComp(m1, m2: Msg): bool { true } 
axiom (forall m1, m2: Msg :: {MsgComp(m1, m2)} 
    m1 == m2 <==> 
    (tID(m1) == tID(m2) && stype(m1) == stype(m2) && 
    acc(m1) == acc(m2) && bal(m1) == bal(m2) && 
    mbal(m1) == mbal(m2) && mval(m1) == mval(m2) && 
    val(m1) == val(m2)));

然后，我声明一个新变量m和分配任意值到它的电场，使得m等于M1或M2。我没有明确地说m == M1 || m == M2，但我们可以用上面的公理证明这个断言（786行）。

assert (MsgComp(cMsg, M1) && MsgComp(cMsg, M2) && (cMsg == M1 || cMsg == M2));

但是，如果我要检查是否m是M1, ..., M72之一，布吉显示相应的声明可能不成立。

assert (MsgComp(cMsg, M1) && ... && MsgComp(cMsg, M72) && (cMsg == M1 || ... || cMsg == M72));

我发现如果我检查最多32个常量的断言，布吉可以验证它。为什么Boogie或Z3不能用更多的常量来验证它？

来源

2017-08-29 Thanh Hai Tran

在我的机器上，即使对于两个常量，检查也不会成功。

我能得到两张支票将它们变更为以下形式

assert MsgComp(cMsg, M1) && MsgComp(cMsg, M2) ==> (cMsg == M1 || cMsg == M2);

（注意中间的&&已更改为==>）

这也适用于通过与72值的断言。

我不知道为什么这个改变很重要。看起来在触发事件发生之前，这些连词被忽略或简化了。

来源

2017-08-29 16:00:07

AFAIK，SMTLib连词不是短路的，因此可以并行处理。这可以解释为什么触发器'MsgComp（...）'不一定在原始编码中可用，而是在你的编码中。 –

触发器，Z3中的#in

回答

相关问题