Z3 QBVF вопросы

Question

По итогам предыдущего обсуждения: Z3: извлечение значений экзистенциальной модели

Есть ли разница между:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))

И

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))

Что касается Z3?То есть я все равно получу решатель QBVF для последнего автоматически?

Кроме того, после экспериментов я обнаружил, что если я выдаю:

(eval (sx #x8000))

После вызова (check-sat), он работаетхорошо (что здорово).Что было бы лучше, если бы я мог также сказать:

(eval (sx (get-value (y))))

Увы, для этого запроса Z3 жалуется, что это invalid function application.Есть ли способ использовать функцию eval таким образом?

Спасибо!

Answer 1

Сценарии

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))

и

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))

не эквивалентны.Второе фактически равнозначно

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (exists ((y (_ BitVec 16))) (bvuge y (sx y))))

Что касается команды eval, вы можете ссылаться на любую неинтерпретированную константу и символ функции.Таким образом, вы можете написать:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))
(check-sat)
(eval (sx y))

Команда (eval (sx y)) не будет работать для первого скрипта, поскольку y является универсальной переменной.