嵌套存儲操作的有效方式

Question

在Most efficient way to represent memory buffers in Z3關於如何使嵌套存儲操作更高效的問題被回答爲可以用選擇替換（嵌套）存儲操作，如(assert (= (select A i1) v1))。但是，我需要商店操作，因爲之前的約束必須用新的約束來替換。

例如：下面的約束模擬以下組件的程序：

mov qword ptr [rax], rbx 
mov rcx, qword ptr [rax] 

我喜歡證明RBX和RCX是相等的，我斷言（= RBX 2 RCX 2！）並期望該模型可以滿足。這工作完美。我斷言（不是（= RBX！2 RCX！2））並且期望模型不能被滿足。當我將以下約束提供給Z3時（例如here），它會給出幾乎即時的答案：UNSAT。但是，如果我在C＃程序中證明了同樣的問題（見下文），則無法推斷UNSAT（在合理的時間內）。

問題：我該如何儘快使C＃程序與SMT2.0程序一樣快？

(declare-fun RAX!0() (_ BitVec 64)) 
(declare-fun RAX!1() (_ BitVec 64)) 
(declare-fun RAX!2() (_ BitVec 64)) 

(declare-fun RBX!0() (_ BitVec 64)) 
(declare-fun RBX!1() (_ BitVec 64)) 
(declare-fun RBX!2() (_ BitVec 64)) 

(declare-fun RCX!0() (_ BitVec 64)) 
(declare-fun RCX!1() (_ BitVec 64)) 
(declare-fun RCX!2() (_ BitVec 64)) 

(declare-fun MEM!0() (Array (_ BitVec 64) (_ BitVec 8))) 
(declare-fun MEM!1() (Array (_ BitVec 64) (_ BitVec 8))) 
(declare-fun MEM!2() (Array (_ BitVec 64) (_ BitVec 8))) 

(assert (= RAX!1 RAX!0)) 
(assert (= RBX!1 RBX!0)) 
(assert (= RCX!1 RCX!0)) 
(assert (let ((a!1 (store (store (store MEM!0 RAX!0 ((_ extract 7 0) RBX!0)) 
         (bvadd #x0000000000000001 RAX!0) 
         ((_ extract 15 8) RBX!0)) 
        (bvadd #x0000000000000002 RAX!0) 
        ((_ extract 23 16) RBX!0)))) 
(let ((a!2 (store (store (store a!1 
           (bvadd #x0000000000000003 RAX!0) 
           ((_ extract 31 24) RBX!0)) 
         (bvadd #x0000000000000004 RAX!0) 
         ((_ extract 39 32) RBX!0)) 
        (bvadd #x0000000000000005 RAX!0) 
        ((_ extract 47 40) RBX!0)))) 
    (= MEM!1 
    (store (store a!2 
        (bvadd #x0000000000000006 RAX!0) 
        ((_ extract 55 48) RBX!0)) 
      (bvadd #x0000000000000007 RAX!0) 
      ((_ extract 63 56) RBX!0)))))) 
(assert (= RAX!2 RAX!1)) 
(assert (= RBX!2 RBX!1)) 
(assert (= RCX!2 
    (concat (select MEM!1 (bvadd #x0000000000000007 RAX!1)) 
      (select MEM!1 (bvadd #x0000000000000006 RAX!1)) 
      (select MEM!1 (bvadd #x0000000000000005 RAX!1)) 
      (select MEM!1 (bvadd #x0000000000000004 RAX!1)) 
      (select MEM!1 (bvadd #x0000000000000003 RAX!1)) 
      (select MEM!1 (bvadd #x0000000000000002 RAX!1)) 
      (select MEM!1 (bvadd #x0000000000000001 RAX!1)) 
      (select MEM!1 RAX!1)))) 
(assert (= MEM!2 MEM!1)) 
(assert (not (= RBX!2 RCX!2))) 

C＃代碼：

Dictionary<string, string> settings = new Dictionary<string, string> 
{ 
    { "unsat-core", "false" }, // enable generation of unsat cores 
    { "model", "false" },   // enable model generation 
    { "proof", "false" },   // enable proof generation 
    { "timeout", "60000" }  // 60000=1min 
}; 
Context ctx = new Context(settings); 

Solver solver = ctx.MkSolver(ctx.MkTactic("qfbv")); 
BitVecExpr rax0 = ctx.MkBVConst("RAX!0", 64); 
BitVecExpr rax1 = ctx.MkBVConst("RAX!1", 64); 
BitVecExpr rax2 = ctx.MkBVConst("RAX!2", 64); 

BitVecExpr rbx0 = ctx.MkBVConst("RBX!0", 64); 
BitVecExpr rbx1 = ctx.MkBVConst("RBX!1", 64); 
BitVecExpr rbx2 = ctx.MkBVConst("RBX!2", 64); 

BitVecExpr rcx0 = ctx.MkBVConst("RCX!0", 64); 
BitVecExpr rcx1 = ctx.MkBVConst("RCX!1", 64); 
BitVecExpr rcx2 = ctx.MkBVConst("RCX!2", 64); 

ArrayExpr mem0 = ctx.MkArrayConst("MEM!0", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); 
ArrayExpr mem1 = ctx.MkArrayConst("MEM!1", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); 
ArrayExpr mem2 = ctx.MkArrayConst("MEM!2", ctx.MkBitVecSort(64), ctx.MkBitVecSort(8)); 

solver.Assert(ctx.MkEq(rax1, rax0)); 
solver.Assert(ctx.MkEq(rbx1, rbx0)); 
solver.Assert(ctx.MkEq(rcx1, rcx0)); 
ArrayExpr memX0 = ctx.MkStore(mem0, ctx.MkBVAdd(ctx.MkBV(0, 64), rax0), ctx.MkExtract((1 * 8) - 1, 0 * 8, rbx0)); 
ArrayExpr memX1 = ctx.MkStore(memX0, ctx.MkBVAdd(ctx.MkBV(1, 64), rax0), ctx.MkExtract((2 * 8) - 1, 1 * 8, rbx0)); 
ArrayExpr memX2 = ctx.MkStore(memX1, ctx.MkBVAdd(ctx.MkBV(2, 64), rax0), ctx.MkExtract((3 * 8) - 1, 2 * 8, rbx0)); 
ArrayExpr memX3 = ctx.MkStore(memX2, ctx.MkBVAdd(ctx.MkBV(3, 64), rax0), ctx.MkExtract((4 * 8) - 1, 3 * 8, rbx0)); 
ArrayExpr memX4 = ctx.MkStore(memX3, ctx.MkBVAdd(ctx.MkBV(4, 64), rax0), ctx.MkExtract((5 * 8) - 1, 4 * 8, rbx0)); 
ArrayExpr memX5 = ctx.MkStore(memX4, ctx.MkBVAdd(ctx.MkBV(5, 64), rax0), ctx.MkExtract((6 * 8) - 1, 5 * 8, rbx0)); 
ArrayExpr memX6 = ctx.MkStore(memX5, ctx.MkBVAdd(ctx.MkBV(6, 64), rax0), ctx.MkExtract((7 * 8) - 1, 6 * 8, rbx0)); 
memX7 = ctx.MkStore(memX6, ctx.MkBVAdd(ctx.MkBV(7, 64), rax0), ctx.MkExtract((8 * 8) - 1, 7 * 8, rbx0)); 
solver.Assert(ctx.MkEq(mem1, memX7).Simplify() as BoolExpr); 

solver.Assert(ctx.MkEq(rax2, rax1)); 
solver.Assert(ctx.MkEq(rbx2, rbx1)); 
BitVecExpr y0 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(0, 64), rax1)) as BitVecExpr; 
BitVecExpr y1 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(1, 64), rax1)) as BitVecExpr; 
BitVecExpr y2 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(2, 64), rax1)) as BitVecExpr; 
BitVecExpr y3 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(3, 64), rax1)) as BitVecExpr; 
BitVecExpr y4 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(4, 64), rax1)) as BitVecExpr; 
BitVecExpr y5 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(5, 64), rax1)) as BitVecExpr; 
BitVecExpr y6 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(6, 64), rax1)) as BitVecExpr; 
BitVecExpr y7 = ctx.MkSelect(mem1, ctx.MkBVAdd(ctx.MkBV(7, 64), rax1)) as BitVecExpr; 
BitVecExpr y = ctx.MkConcat(y7, ctx.MkConcat(y6, ctx.MkConcat(y5, ctx.MkConcat(y4, ctx.MkConcat(y3, ctx.MkConcat(y2, ctx.MkConcat(y1, y0))))))); 
solver.Assert(ctx.MkEq(rcx2, y).Simplify() as BoolExpr); 
solver.Assert(ctx.MkEq(mem2, mem1)); 

Status status_Neg = solver.Check(ctx.MkNot(ctx.MkEq(rbx2, rcx2))); 
Console.WriteLine("Status Neg = "+status_Neg); // Go on holiday... 

Answer 1

我沒有辦法運行C＃程序與它玩，很遺憾。但我注意到，你不得不Simplify電話：

solver.Assert(ctx.MkEq(mem1, memX7).Simplify() as BoolExpr); 

我很好奇，爲什麼你需要的電話嗎？也許這是罪魁禍首？

要嘗試的另一件事是使用未解釋的函數來表示內存，而不是Array s。用友通常更容易處理，並且他們提供了與我個人經驗大致相同的抽象。

查看C＃接口作爲SMT-Lib生成的內容可能是一個好主意，以查看翻譯是否與您認爲的翻譯顯着不同。我想你可以用下面的函數來做到這一點：https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/AST.cs#L195