About solving Horn clauses

[panda2134]

To my knowledge Z3 has 2 CHC solvers embedded -- datalog and spacer.
As they employ different output formats, how can I specify the usage of one of them explicitly in my SMTLIB2 code? Or is this only available through Z3's C++ interface?

Another question is about the usage of datalog. I know that when using :print-answer with datalog, Z3 tries to output every solution satisfying the given query (connected with logical or). Its output is like this:

sat
(or (and (= (:var 0) #b101) (= (:var 1) #b110))
    (and (= (:var 0) #b001) (= (:var 1) #b000))
    (and (= (:var 0) #b010) (= (:var 1) #b000))
    (and (= (:var 0) #b011) (= (:var 1) #b000))
    (and (= (:var 0) #b100) (= (:var 1) #b000))
    (and (= (:var 0) #b101) (= (:var 1) #b000))
    (and (= (:var 0) #b110) (= (:var 1) #b000))
    (and (= (:var 0) #b111) (= (:var 1) #b000))

However, in my usecase I only need exactly 1 solution, because producing every solution is too slow. How can this be achieved when using datalog?

[hgvk94]

Enable spacer engine using command line argument "fp.engine=spacer". To give this in the SMT file, use smt2 command
(set-option :fp.engine spacer)

To use datalog, change spacer to datalog

[panda2134]

Thank you a lot, but my second question remains unanswered. I wonder if github allows selecting multiple answers..?