Слишком много возможных конфигураций в z3 с использованием scala ^ z3 - PullRequest
Новая
       15

Слишком много возможных конфигураций в z3 с использованием scala ^ z3

0 голосов
/ 09 декабря 2011

Это в основном логическая проблема, я думаю ...

Я использую эту формулу smtlib: 

(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Bool)
(assert (xor (and a (xor b c)) d))

Что является термином этой структуры (по моему мнению, по крайней мере): 

    XOR
    | |
  AND d
  | |
  a XOR
    | |
    b c

Мое предположение: набор результатов будет выглядеть следующим образом: 

{ab, ac, d}

Но это с использованием scala ^ z3 ctx.checkAndGetAllModels (): 

{ab, d, ac, ad, abcd}

Почему там реклама и abcd?Можно ли получить только те результаты, которые я ожидал?

1 Ответ

3 голосов
/ 09 декабря 2011

Использование Scala (без Z3), чтобы показать, что на самом деле есть больше решений для ограничения: 

val tf = Seq(true, false)
val allValid =
  for(a <- tf; b <- tf; c <- tf; d <- tf; 
      if((a && (b ^ c)) ^ d)) yield (
    (if(a) "a" else "") + (if(b) "b" else "") +
    (if(c) "c" else "") + (if(d) "d" else ""))

allValid.mkString("{ ", ", ", " }")

Печать: 

{ abcd, ab, ac, ad, bcd, bd, cd, d }

Итак, если я что-то упускаю, вопрос в том, почему он не находит все решения? Теперь вот ответ на этот вопрос. (Оповещение о спойлере: "getAllModels" на самом деле не получает все модели.) Сначала давайте воспроизведем то, что вы наблюдали: 

import z3.scala._
val ctx = new Z3Context("MODEL" -> true)
val a = ctx.mkFreshConst("a", ctx.mkBoolSort)
val b = ctx.mkFreshConst("b", ctx.mkBoolSort)
val c = ctx.mkFreshConst("c", ctx.mkBoolSort)
val d = ctx.mkFreshConst("d", ctx.mkBoolSort)
val cstr0 = ctx.mkXor(b, c)
val cstr1 = ctx.mkAnd(a, cstr0)
val cstr2 = ctx.mkXor(cstr1, d)
ctx.assertCnstr(cstr2)

Теперь, если я бегу: ctx.checkAndGetAllModels.foreach(println(_)), я получаю: 

d!3 -> false
a!0 -> true
c!2 -> false
b!1 -> true

d!3 -> true    // this model is problematic
a!0 -> false

d!3 -> false
a!0 -> true
c!2 -> true
b!1 -> false

d!3 -> true
a!0 -> true
c!2 -> false
b!1 -> false

d!3 -> true
a!0 -> true
c!2 -> true
b!1 -> true

Теперь проблема в том, что вторая модель является неполной моделью. Z3 может вернуть его, потому что, какими бы ни были значения для b и c, ограничение выполнено (b и c являются не заботящимися переменными). Текущая реализация checkAndGetAllModels просто отрицает модель, чтобы предотвратить повторение; в этом случае он запросит другую модель, такую, что (not (and d (not a))). Это предотвратит возвращение всех других моделей с этими двумя значениями. В некотором смысле неполная модель фактически представляет четыре действительные завершенные модели.

Кстати, если вы используете DSL ScalaZ3 с функцией findAll, то все модели будут завершены со значениями по умолчанию, если они неполные (и до того, как они будут использованы для вычисления следующий). В контексте DSL мы можем сделать это, потому что мы знаем множество переменных, которые появляются в формуле. В этом случае сложнее угадать, как модель должна быть завершена. Один из вариантов - ScalaZ3 запомнить, какие переменные использовались. Лучшим решением было бы для Z3 иметь возможность всегда возвращать значения для переменных, не имеющих значения, или, возможно, просто перечислять все значения, не заботящиеся в модели.

...