z3 for solving chc datalog rules

[aleksdimovski]

I obtained the out.z3 file below from another tool that contains CHC datalog rules ... How can I run this file using z3 and eventually obtain a model if the result is sat? I tried:
$z3 fp.engine=spacer out.z3, and
$ z3 out.z3,
but no model is returned ... I have z3 version 4.11.2 ...

This is out.z3 file:

(declare-datatypes () ((B ($var ($varAc1 V)) ($and ($andAc2 B) ($andAc3 B)))
(V $v0 $v1 $v2 $v3)))
(declare-var bt1 B)
(declare-var v1 Bool)
(declare-var bt2 B)
(declare-var r1 Bool)
(declare-var v2 Bool)
(declare-var vt V)
(declare-var r Bool)
(declare-var v0 Bool)
(declare-var bt B)
(declare-var result Bool)
(declare-var v3 Bool)
(declare-var r2 Bool)
(declare-var @B__agtt.SynVar1 B)
(declare-var formula B)
(declare-var @B__agtt.SynVar0 B)
(declare-var @V__agtt.SynVar0 V)
(declare-var @B__agtt.SynVar2 B)
(declare-var @V__agtt.SynVar1 V)
(declare-rel B.Sem (B Bool Bool Bool Bool Bool))
(declare-rel V.Sem (V Bool Bool Bool Bool Bool))
(declare-rel realizable ())
(declare-rel @B__agtt.Syn (B))
(declare-rel @V__agtt.Syn (V))
(rule (=> (and (= @B__agtt.SynVar0 ($var @V__agtt.SynVar1)) (@V__agtt.Syn @V__agtt.SynVar1)) (@B__agtt.Syn @B__agtt.SynVar0)))
(rule (=> (and (= @B__agtt.SynVar0 ($and @B__agtt.SynVar1 @B__agtt.SynVar2)) (@B__agtt.Syn @B__agtt.SynVar1) (@B__agtt.Syn @B__agtt.SynVar2)) (@B__agtt.Syn @B__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v2) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v3) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v0) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (= @V__agtt.SynVar0 $v1) (@V__agtt.Syn @V__agtt.SynVar0)))
(rule (=> (and (= bt ($var (as vt V))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as r Bool)) (= (as result Bool) (as r Bool))) (B.Sem (as bt B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= bt ($and (as bt1 B) (as bt2 B))) (B.Sem (as bt1 B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as r1 Bool)) (B.Sem (as bt2 B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as r2 Bool)) (= (as result Bool) (and (as r1 Bool) (as r2 Bool)))) (B.Sem (as bt B) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v0) (= (as result Bool) (as v0 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v1) (= (as result Bool) (as v1 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v2) (= (as result Bool) (as v2 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (= vt $v3) (= (as result Bool) (as v3 Bool))) (V.Sem (as vt V) (as v0 Bool) (as v1 Bool) (as v2 Bool) (as v3 Bool) (as result Bool))))
(rule (=> (and (B.Sem formula false true true false true) (B.Sem formula false true false false false) (B.Sem formula true false true false false)) realizable))
(query realizable)

[levnach]

try adding
(get-model)
as the very last command in your smt file.

[levnach]

It seems that z3 does not terminate in reasonable time on this benchmark. Reopening the issue.

[NikolajBjorner]

spacer invokes several check-sats. There are terms and clauses left over from previous check-sats.
This could be axioms created by the theory of algebraic data-types.
A crude, but workable, way to deal with this is to reset the solver if it exceeds some number of conflicts and reinitialize it with the relevant assertions. Spacer maintains several layers on top of solvers, and this looks like being from a solver pool.

[NikolajBjorner]

z3 7837.smt2 /tr:solver_na2as /v:2 /tr:before_search /tr:asserted_formulas