Правило содержит исключение бесконечных сортировок с IntSort

Question

Я новичок в Datalog и двигатель Datalog в Z3. Я пробую некоторые примеры, используя Python API Z3. Это небольшой пример, который я пробую. Я ожидаю использовать аналогичные конструкции (целые числа) для реальной проблемы, которую я попытаюсь решить позже.

from z3 import *

fp = Fixedpoint()
fp.set(engine='datalog')
fp.set('datalog.generate_explanations', True)


valid = Function('valid', IntSort(),  BoolSort())
fp.register_relation(valid)
five=IntVal(5)
fp.fact(valid(five))
print fp.query(valid(five))
print fp.get_answer()

Это приводит к следующей ошибке:

  File "trial3.py", line 12, in <module>
    print fp.query(valid(five))
  File "/opt/z3/bin/python/z3/z3.py", line 6596, in query
    r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
  File "/opt/z3/bin/python/z3/z3core.py", line 3827, in Z3_fixedpoint_query
    _elems.Check(a0)
  File "/opt/z3/bin/python/z3/z3core.py", line 1328, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: Rule contains infinite sorts in rule <null>:
valid(5).

Я пытался заменить IntSort в приведенном выше примере с BitVecSortи проблема уходит.

from z3 import *

fp = Fixedpoint()
fp.set(engine='datalog')
fp.set('datalog.generate_explanations', True)


valid = Function('valid', BitVecSort(3),  BoolSort())
fp.register_relation(valid)
five=BitVecVal(5, BitVecSort(3))
fp.fact(valid(five))
print fp.query(valid(five))
print fp.get_answer()

Это фундаментальное ограничение? Каковы последствия производительности, если я использую большой BitVecSort вместо IntSort?