Как запустить журнал данных в Z3 с помощью командной строки

Я пытаюсь запустить файл журнала данных (test.dl, с http://rise4fun.com/Z3/tutorialcontent/fixedpoints#h21), как показано ниже в Z3 (версия: 4.3.2).

(set-option :fixedpoint.engine datalog)
(define-sort s () (_ BitVec 3))
(declare-rel edge (s s))
(declare-rel path (s s))
(declare-var a s)
(declare-var b s)
(declare-var c s)

(rule (=> (edge a b) (path a b)))
(rule (=> (and (path a b) (path b c)) (path a c)))

(rule (edge #b001 #b010))
(rule (edge #b001 #b011))
(rule (edge #b010 #b100))

(query (path #b001 #b100))
(query (path #b011 #b100))
(query (path #b001 b)
  :print-answer true)

Используйте команду z3 test.dl, но есть сообщение об ошибке: введите здесь описание изображения

Может кто-нибудь помочь, как запустить файл журнала данных?

Спасибо.


z3 datalog
person Community    schedule 05.12.2015    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Входной формат для этого файла — SMT2, а не Datalog. Несмотря на то, что вы хотите запустить модуль Datalog, файл не в формате Datalog, поэтому синтаксический анализатор выдает ошибку, которую вы видите.

Запуск Z3 с помощью команды z3 -smt2 test.dl прошел успешно, так как это вынуждает Z3 использовать анализатор SMT2, а не Datalog. В качестве альтернативы можно переименовать файл в test.smt2 и запустить z3 test.smt2.

Обе команды произвели то, что я считаю ожидаемым результатом sat unsat sat (or (= (:var 0) #b011) (= (:var 0) #b010) (= (:var 0) #b100))

person mtrberzi    schedule 06.12.2015