How to run datalog in Z3 using commad line

Question

I try to run datalog file (test.dl, from http://rise4fun.com/Z3/tutorialcontent/fixedpoints#h21) as following in Z3 (version: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)

Use the command z3 test.dl, but there is erorr msg:

Can someone help how to run the datalog file?

Thanks.

mtrberzi mtrberzi · Accepted Answer · 2015-12-06T02:10:25

The input format for this file is SMT2, not Datalog. Even though you want to run the Datalog engine, the file isn't in Datalog format and so the parser gives you the error that you see.

Running Z3 with the command z3 -smt2 test.dl was successful, as this forces Z3 to use the SMT2 parser and not the Datalog one. Alternatively, renaming the file to test.smt2 and running z3 test.smt2 works.

Both commands produced what I believe is the expected output sat unsat sat (or (= (:var 0) #b011) (= (:var 0) #b010) (= (:var 0) #b100))

How to run datalog in Z3 using commad line

1 Answers