get_cover_delta() returning "'operation is not supported for datalog' when using pdr

[HalleyYoung]

When calling f.get_cover_delta(1, rel) in z3py, I get the above error, even when I've set the fixpoint solver to pdr. Suggestions?

Code:

from z3 import *

fp = Fixedpoint()

fp.set(engine='pdr')

s = BitVecSort(3)
edge = Function('edge', s, s, BoolSort())
path = Function('path', s, s, BoolSort())
edge_ = Function("edge_", s, s, BoolSort())
f = Function("f", s, s, s, BoolSort())
a = Const('a',s)
b = Const('b',s)
c = Const('c',s)

fp.register_relation(path,edge)
fp.register_relation(f, path)
fp.register_relation(f,edge)
fp.register_relation(edge_, f)
fp.register_relation(edge_, path)
fp.declare_var(a,b,c)
fp.rule(path(a,b), edge(a,b))


fp.rule(edge_(a,b), [path(a,b), Not(f(a,b,c))])
fp.rule(f(a,b,c), And(path(a,c), edge(c,b)))

v1 = BitVecVal(1,s)
v2 = BitVecVal(2,s)
v3 = BitVecVal(3,s)
v4 = BitVecVal(4,s)
v = BitVec("s", s)
fp.fact(path(v1,v2))
fp.fact(edge(v1,v3))
fp.fact(edge(v2,v4))

print(fp.query(edge_), "yes we can reach v2 from v1 using only an edge")
print(fp.get_cover_delta(1, edge_)

[NikolajBjorner]

@agurfinkel - is this feature used?

[agurfinkel]

@NikolajBjorner yes

@HalleyYoung there is no pdr engine. get_cover_delta is only supported by spacer engine.
However, spacer engine does not allow for negative predicates in the rules.

[NikolajBjorner]

It now complains about the configuration issue

[HalleyYoung]

@agurfinkel @NikolajBjorner thank you so much for your help in better understanding Z3's limitations, I really appreciate it!