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

【问题标题】：How do I define for example a plus function on integers in Z3 using the .NET API?例如，如何使用 .NET API 定义 Z3 中整数的加号函数？
【发布时间】：2013-10-11 07:32:21
【问题描述】：

使用 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 中使用它？

【问题讨论】：

标签： z3

【解决方案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);

【讨论】：