Strange results with quantified formula

Question

I am getting some strange results when I use the ForAll quantifier. My goal is to restrict the interpretation of a function foo to the following:

\Ax,y. foo(x,y)= if x=A && y=B then C1 else C2

So if i assert the above into a context I should get back an interpretation for foo which essentially equivalent to the above. However I do not. What i get back is something like

foo(x,y)= if x=A && y=B then C1 else C1

And I have no idea why. The code I am using is below (accessing Z3 via the .net API)

let ctx = new Context()
let Sort1 = ctx.MkEnumSort("S1", [|"A";"AA"|])
let Sort2 = ctx.MkEnumSort("S2", [|"B"|])
let Sort3 = ctx.MkEnumSort("S3", [|"C1";"C2"|]) 
let s1 = ctx.MkSymbol "s1"
let s2 = ctx.MkSymbol "s2"
let types = [|Sort1:>Sort; Sort2:>Sort |]
let names = [|s1:>Symbol ; s2:>Symbol|]
let vars = [| ctx.MkConst(names.[0],types.[0]);ctx.MkConst(names.[1],types.[1])|]

let FDecl = ctx.MkFuncDecl("foo", [|Sort1:>Sort;Sort2:>Sort|], Sort3) 
let f_body = ctx.MkITE(ctx.MkAnd(ctx.MkEq(vars.[0],getZ3Id("A",Sort1)), 
                                 ctx.MkEq(vars.[1], getZ3Id("B",Sort2))),
                       getZ3Id("C1",Sort3), 
                       getZ3Id("C2",Sort3)) 
let f_app = FDecl.Apply vars //ctx.MkApp(FDecl, vars)
let body = ctx.MkEq(f_app, f_body)

let std_weight = uint32 1
let form = ctx.MkForall(types, names, body, std_weight, null, null, null, null) 
           :> BoolExpr
let s = ctx.MkSolver() 
satisfy s [|form|]
s.Model

where getZ3Id converts the given string to the corresponding constant in the Enum

let getZ3Id (id,sort:EnumSort) = 
  let matchingConst zconst = zconst.ToString().Equals(id)
  Array.find matchingConst sort.Consts

And satisfy is:

let satisfy (s:Solver) formula =
    s.Assert (formula)
    let res = s.Check() 
    assert (res = Status.SATISFIABLE)
    s.Model

The model returns an interpretation for foo that returns C1 no matter what

(define-fun foo ((x!1 S1) (x!2 S2)) S3
  (ite (and (= x!1 A) (= x!2 B)) C1
    C1))

Could someone point out where I'm going wrong? thanks PS Also what is the difference between the two API calls to MkForAll - one takes sorts and names and other takes "bound constants"?

Here is my further problem: If i define

let set1 = Set.map (fun (p:string)-> ctx.MkConst(p,Sort3)) 
                   (new Set<string>(["C1"]))

and change the body of f

let f_body = ctx.MkITE(ctx.MkAnd(ctx.MkEq(vars.[0],getZ3Id("A",Sort1))), 
                                 ctx.MkEq(vars.[1], getZ3Id("B",Sort2))),
                       mkZ3Set ctx set1,
                       ctx.MkEmptySet Sort3)

where

let mkZ3Set (ctx:Context) exprs sort =
  Set.fold (fun xs x-> ctx.MkSetAdd(xs,x)) (ctx.MkEmptySet(sort)) exprs

The Z3 formula looks reasonable

form= (forall ((s1 S1))
  (= (foo s1)
     (ite (and (= s1 A))
          (store ((as const (Array S3 Bool)) false) C1 true)
          ((as const (Array S3 Bool)) false))))

yet Z3 returns Unsatisfiable. Can you tell me why?

OK thanks. But I now have a further problem. If i change the return type of Foo to be a Set of Sort3 rather than Sort3 and change the constraint to return some set, it becomes unsatisfiable, and again I am not sure why. Unf. S/O doesnt allow you do much formatting in the reply box so I've "answered my own q". Please take a look there — N.S.
I was about to clarify that Z3 does not return Unsatisfiable but Unknown. After poking around a bit, I think my problem may have something to do with MBQI and that it needs to be turned on. However I do not know how to do that via the API. (It doesnt help that the main Z3 documentation page is down as are the links to some of the classes such as STATUS. I have filed a bug report at codeplex). The user guide describes how to turn it on only for SMTLIB interface — N.S.

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2013-04-12T04:50:58

The problem is the quantifier abstraction. It does not abstract the variables you intend.

 let form = ctx.MkForall(types, names, body, std_weight, null, null, null, null) 
       :> BoolExpr

should instead be:

 let form = ctx.MkForall(vars, body, std_weight, null, null, null, null) 
       :> BoolExpr

The background is that Z3 exposes two different ways for you to quantify variables.

Option 1: you can abstract constants that appear in formulas. You should pass an array of those constants to the quantifier abstraction. This is the version my correction uses.

Option 2: you can abstract de-Brujin indices that appear free in a formula. You can then use the overload of ctx.MkForall that you used in your example. But it requires that whenever you refer to a bound variable, you use a bound index (something created using ctx.MkBound).

Strange results with quantified formula

1 Answers