Странные результаты с квантифицированной формулой

Question

Я получаю некоторые странные результаты, когда я использую квантификатор ForAll. Моя цель состоит в том, чтобы ограничить интерпретацию функции Foo к следующему:

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

Так что, если я утверждаю выше в контексте, я должен вернуться к интерпретации для Foo, который по существу эквивалентный приведенному выше. Однако я этого не делаю. То, что я получаю, это что-то вроде

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

И я понятия не имею, почему. Код, я использую ниже (доступ к Z3 через .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 

где getZ3Id преобразует заданную строку в соответствующую константу в Enum

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

И satisfy является:

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

Модель возвращает интерпретацию для foo, которая возвращает C1 независимо от того, что

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

Может ли кто-нибудь указать, где я ошибаюсь? спасибо PS Также в чем разница между двумя вызовами API для MkForAll - один принимает сортировки и имена, а другой принимает «связанные константы»?

---

Вот моя дальнейшая проблема: Если я определить

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

и изменить тело е

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) 

где

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

формула Z3 выглядит разумно

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

еще нет ответа Z3 Неиспользуемый. Можешь мне сказать почему?

Answer 1

Проблема - это абстракция квантора. Он не абстрагирует переменные, которые вы планируете использовать.

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

вместо этого должен быть:

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

Предпосылка, что Z3 предоставляет два различных способа для вас, чтобы определить количество переменных.

Вариант 1: вы можете абстрагировать константы, которые появляются в формулах. Вы должны передать массив этих констант в абстракцию квантора. Это версия, которую использует моя коррекция.

Вариант 2: вы можете абстрагироваться от дебрюинских индексов, которые выглядят бесплатно в формуле. Затем вы можете использовать перегрузку ctx.MkForall, которую вы использовали в вашем примере. Но для этого требуется, чтобы всякий раз, когда вы ссылаетесь на связанную переменную, вы используете связанный индекс (что-то созданное с помощью ctx.MkBound).