如何在Z3中使用.NET API定義整數的加號函數？

Question

使用Z3 .NET API我想，如下面的例子我從Z3 Guide採取了類似的東西：

(define-sort A() (Array Int Int Int)) 
(define-fun bag-union ((x A) (y A)) A 
    ((_ map (+ (Int Int) Int)) x y)) 
(declare-const s1 A) 
(declare-const s2 A) 
(declare-const s3 A) 
(assert (= s3 (bag-union s1 s2))) 
(assert (= (select s1 0 0) 5)) 
(assert (= (select s2 0 0) 3)) 
(assert (= (select s2 1 2) 4)) 
(check-sat) 
(get-model) 

如何定義的+功能，這樣我可以用它在MkMap？

Answer 1

MkMap需要一個函數聲明，所以你需要使用MkAdd並獲得與.FuncDecl參考其函數聲明才能到+函數聲明，你可以做一個參考：

Context z3 = new Context(); 
Sort twoInt = z3.MkTupleSort(z3.MkSymbol("twoInt"), new Symbol[] { z3.MkSymbol("a"), z3.MkSymbol("b") }, new Sort[] { z3.IntSort, z3.IntSort }); 
Sort A = z3.MkArraySort(twoInt, z3.IntSort); 
ArrayExpr x = z3.MkArrayConst("x", twoInt, z3.IntSort); 
ArrayExpr y = z3.MkArrayConst("y", twoInt, z3.IntSort); 
ArrayExpr map = z3.MkMap(z3.MkAdd(z3.MkIntConst("a"), z3.MkIntConst("b")).FuncDecl, x, y);