Как объявить предикаты для битовых векторов произвольного размера в z3? - PullRequest
Новая
       15

Как объявить предикаты для битовых векторов произвольного размера в z3?

0 голосов
/ 03 мая 2019

Я столкнулся с проблемой при попытке определить некоторые правила для битовых векторов в z3.Если я пытаюсь решить следующий файл с z3 

(declare-rel FunnyFun ((_ BitVec 64)))
(declare-var A (_ BitVec 64))
(declare-var B (_ BitVec 64))
(rule (=> (= B (bvadd A #x0000000000000001))
    (FunnyFun B)))

(declare-rel q1 ())

(rule (=> (FunnyFun #x0000000000000001) q1))

(query q1)

, я получаю ошибку 

(error "query failed: Rule contains infinite sorts in rule <null>:
FunnyFun(#0) :- 
 (= (:var 0) (bvadd (:var 1) #x0000000000000001)).
")

Как ни странно, z3 мгновенно дает ожидаемый результат (sat) при использовании битов меньшей ширины: 

(declare-rel FunnyFun ((_ BitVec 60)))
(declare-var A (_ BitVec 60))
(declare-var B (_ BitVec 60))
(rule (=> (= B (bvadd A #x000000000000001))
    (FunnyFun B)))

(declare-rel q1 ())

(rule (=> (FunnyFun #x000000000000001) q1))

(query q1)

Это ошибка или мне не хватает некоторых ограничений (я предполагал, что BitVec может иметь произвольную битовую ширину)?

Я пробовал другую версию z3 (4.6.0, 4.8.3 и4.8.5) и все они показали это поведение.

1 Ответ

0 голосов
/ 05 мая 2019

Это ограничение предусмотрено дизайном.Смотрите здесь: https://github.com/Z3Prover/z3/issues/1698

...