Как я могу изменить стандартное поведение функций z3? - PullRequest
Новая
       11

Как я могу изменить стандартное поведение функций z3?

0 голосов
/ 03 мая 2018

У меня есть запрос (get-model) для Z3, который возвращает эту функцию: 

(define-fun rules ((x!0 Tree)) Bool
(ite (= x!0 (node "mann" (cons (node "adam" nil) nil))) true
(ite (= x!0 (node "mensch" (cons (node "adam" nil) nil))) true
true)))

При использовании этого кода: 

(declare-datatypes () ((Tree leaf (node (value String) (children TreeList)))
                       (TreeList nil (cons (car Tree) (cdr TreeList)))))
(declare-const list TreeList)
(declare-const fact1 Tree)
(declare-const fact2 Tree)

(assert (not (is-leaf fact1)))
(assert (not (is-leaf fact2)))
(assert (not (= list nil)))

(assert (= (value fact1) "mann"))
(assert (= (value fact2) "adam"))
(assert (= (children fact1) list))

(assert (= fact2 (car list)))


(declare-const list2 TreeList)
(declare-const fact3 Tree)
(declare-const fact4 Tree)

(assert (not (is-leaf fact3)))
(assert (not (is-leaf fact4)))
(assert (not (= list2 nil)))

(assert (= (value fact3) "mensch"))
(assert (= (value fact4) "adam"))
(assert (= (children fact3) list2))

(assert (= fact4 (car list2)))

(declare-fun rules (Tree) Bool)
(assert (= (rules fact1) true))
(assert (=> (rules fact1) (rules fact3)))


(check-sat)
(get-model)

Проблема в том, что мне нужно, чтобы функция «rules» возвращала false, когда аргумент не является одним из деревьев, я утверждал, что правила должны быть истинными, но я не могу найти способ отредактировать последний », иначе «в функции. (get-model), кажется, всегда использует наиболее распространенный ответ функции в качестве ответа, если ни одно из правил не работает, и так как у меня есть только правила для деревьев, которые делают ответ истинным, он также использует true для остальных, но я могу Не используйте функцию таким образом.

1 Ответ

0 голосов
/ 04 мая 2018

Похоже, вы пытаетесь смоделировать Пролог как допущение "замкнутого мира" здесь. Это не то, как работают SMT-решатели: они найдут модель, которая будет отвечать всем требованиям, а все остальное - честная игра. То есть, если вы не хотите, чтобы какое-либо другое значение удовлетворяло вашему rules, вы должны указать это явно.

Возможно, вы захотите взглянуть на моделирование данных, которое кажется ближе к тому, что вы пытаетесь выразить: https://rise4fun.com/z3/tutorialcontent/fixedpoints

...