觸發器，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

回答

相關問題