在z3中定義有界整數

在Z3中有明確的方法來定義有界整數嗎？在z3中定義有界整數

例如，假設我想定義一個整數變量「x」，它可以從[1,4]中取值。我可以做以下操作（我正在使用Java API）

IntExpr x = ctx.mkIntConst("x"); 
solver.add(ctx.mkGT(x, ctx.mkInt(0))); // (assert (> x 0)) 
solver.add(ctx.mkLT(x, ctx.mkInt(5))); // (assert (< x 5))

但是，我不知道是否有更聰明的方法來做到這一點？一些可以在聲明時自動放置變量的上下限的東西。我列舉了一些枚舉，但我不確定這是否是最佳選擇。

謝謝

來源

2017-06-29 Mohammed

如果他們是兩個冪，只是使用位向量。否則，沒有簡單的方法來做到這一點（即你做對了）。

來源

2017-06-29 22:23:14

不幸的是，沒有一種「好」的方式來模擬這種約束。比特向量走得太遠了，假設你可以使用機器算術（即模塊化），並且你的範圍很好地適應，如前所述。以下是以前的相關討論：Is there an UnsignedIntSort in Z3?。

要正確支持你想要的，你需要謂詞子類型。定理證明者，如PVS和Yices的老版本（1.X系列中的SMTLib變體之前的版本）支持這樣的花式類型，具有不同程度的自動化。如果你需要堅持現代化的SMT解決方案，不幸的是，你別無選擇，只能用很多束縛約束來束縛你的代碼。當然，它會非常快速地變得非常難看，因爲在每次操作之後你都必須檢查邊界並定義上溢/下溢的含義。如果尊重邊界是必不可少的，那麼適當的定理證明可能是更好的選擇。

來源

2017-06-30 05:42:09

謝謝Levent，我唯一擔心的就是搜索空間。添加約束約束條件將有助於Z3修剪大量不相關的解決方案，但這些解決方案仍然存在，並且Z3在某一時刻考慮了這些解決方案。我可能弄錯了，它可能是相同的，但是如果Z3中存在有界整數，那麼可能是這種不相關的解決方案從一開始就不存在。無論如何，我現在會堅持約束約束。 – Mohammed

@Mohammed給變量或它們的組合增加了冗餘*上下限，可以加快搜索速度，即使這些*約束可以從現有的約束條件推斷出來（例如參見[如何計算WCET .... ]（http://dl.acm.org/citation.cfm?id=2597817&dl=ACM&coll=DL&CFID=780316479&CFTOKEN=19429447））。說到這一點，在這種情況下預測* smt *求解器的運行時間就像拋硬幣一樣，有幾個因素起作用，包括正在考慮的問題的結構，布爾部分如何與LAR約束*進行交互。 –

在z3中定義有界整數

回答

相關問題