ネストされた店舗運営を効率化する方法についての質問が1がのように選択して（ネスト）ストア操作に置き換えることができると答えている

Question

Most efficient way to represent memory buffers in Z3で巣ストア・オペレーションへの効率的な方法：(assert (= (select A i1) v1))。ただし、以前の制約を新しい制約に置き換える必要があるため、ストア操作が必要です。例えば

：以下の制約は、次のアセンブリプログラムシミュレーション：私はRBXとRCXが等しいことを証明したいと

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

を、私は（！= 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秒の、メモリを表現するための未解釈の機能を使用することです。 UFの方が処理がはるかに簡単で、私の個人的な経験ではほぼ同じ抽象化を提供します。

翻訳はあなたはそれが可能だろうと思ったものよりも著しく異なっているかどうかを確認するために、C＃のインターフェイスは、SMT-Libのようにして生成するものを見て、良いアイデアかもしれません。 https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/AST.cs#L195