CODEWITHSUNDEEP
z3
Patrick Spettel
Patrick Spettel

Reputation: 730

How do I define for example a plus function on integers in Z3 using the .NET API?

Using the Z3 .NET API I'm trying to do something similar as the following example which I have taken from the 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)

How do I define the + function such that I can use it in MkMap?

Upvotes: 1

Views: 315

Answers (1)

Taylor T. Johnson
Taylor T. Johnson

Reputation: 2884

MkMap expects a function declaration, so you need to get a reference to the + function declaration, which you can do by using MkAdd and getting a reference to its function declaration with .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);

Upvotes: 1

Related Questions