z3 - 例如，如何使用 .NET API 定义 Z3 中整数的加号函数？

Question

使用Z3 .NET API，我正在尝试执行类似于以下示例的操作，该示例取自Z3 指南：

(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);