О представлении неинтерпретированной функции в Z3 - PullRequest
Новая
       4

О представлении неинтерпретированной функции в Z3

3 голосов
/ 05 января 2012

У меня быстрый вопрос.Я написал простую программу (используя Z3 NET API) и получил вывод следующим образом.

Программа (частичная): 

        Sort[] domain = new Sort[3];
        domain[0] = intT;  
        domain[1] = intT;          
        domain[2] = intT;  
        FPolicy = z3.MkFuncDecl("FPolicy", domain, boolT);      

        Term[] args = new Term[3];
        args[0] = z3.MkNumeral(0, intT);
        args[1] = z3.MkNumeral(1, intT);
        args[2] = z3.MkNumeral(30, intT);
        z3.AssertCnstr(z3.MkApp(FPolicy, args));

        args[1] = z3.MkNumeral(2, intT);
        args[2] = z3.MkNumeral(20, intT);
        z3.AssertCnstr(z3.MkApp(FPolicy, args));

Вывод: 

FPolicy -> {
  0 1 30 -> true
  0 2 20 -> true     
  else -> true
}

Iмне интересно, я мог бы сделать "else -> true" как false (то есть, "else -> false").

Ответы [ 2 ]

4 голосов
/ 05 января 2012

Для проблем без квантификатора Z3 (3.2) выберет для else значение, которое чаще всего встречается в range. Под range здесь я подразумеваю конечный набор значений, которые Z3 присвоил конкретному конечному набору входных значений. В нашем примере только true встречается в range. Таким образом, true выбрано в качестве значения else.

Для задач без квантификаторов (и без массивов), если опция :model-compact true не используется, то значение else не имеет значения. То есть, если формула F выполнима, Z3 создаст модель M. Затем, если мы изменим значение любого else в M, результирующая модель M’ все еще будет моделью для F. Таким образом, вы можете игнорировать else или предполагать, что это то, что вы хотите, ЕСЛИ входная формула F не содержит квантификаторов, F не использует теорию массивов и :model-compact true не используется. Это свойство основано на алгоритмах, реализованных в настоящее время в Z3, и это может измениться в будущем. Напротив, решение, предоставляемое MHS, не зависит от изменений в реализации Z3. В своем кодировании любой решатель SMT (который успешно создает модель) должен будет использовать false в качестве значения функции в каждой точке, не указанной в антецеденте квантификатора.

Другой вариант - использовать оператор default и кодировать вашу проблему с помощью массивов. Когда используется оператор default, мы должны рассматривать массивы как пары: (Actual Array, Default value). Это значение по умолчанию используется для предоставления значения else во время построения модели. Z3 также имеет несколько встроенных аксиом для распространения значений по умолчанию на: store и map операторы. Вот ваша проблема, закодированная с использованием этого подхода: 

(set-option :produce-models true)
(declare-const FPolicy (Array Int Int Int Bool))

(assert (select FPolicy 0 1 30))
(assert (select FPolicy 0 2 20))
(assert (not (default FPolicy)))

(check-sat)
(get-model)
1 голос
/ 05 января 2012

Как насчет следующего ( RiSE4fun link )? 

(set-option :MBQI true)

(declare-fun FPolicy (Int Int Int) Bool)

(assert (forall ((x1 Int) (x2 Int) (x3 Int)) (!
  (implies
    (not
      (or
        (and (= x1 0) (= x2 1) (= x3 30))
        (and (= x1 0) (= x2 2) (= x3 20))))
      (= (FPolicy x1 x2 x3) false))
  :pattern (FPolicy x1 x2 x3))))

(assert (FPolicy 0 1 30))
(assert (FPolicy 0 2 20))

(check-sat)
(get-model)

Преимущество, которое я вижу, заключается в том, что вы можете изменить его так, чтобы FPolicy (0 1 30) == false, не касаясь ограничения forall. Очевидным недостатком является то, что вам в основном приходится упоминать все кортежи аргументов дважды, а созданная модель довольно запутанная.

Я с нетерпением жду лучших решений: -)

...