Можно ли получить достоверную информацию о диапазоне при использовании ограничения SMT с Z3

Question

Таким образом, в основном я пытаюсь решить следующее ограничение SMT с помощью общего решателя ограничений, такого как Z3:

>>> from z3 import *
>>> a = BitVec("a", 32)
>>> b = BitVec("b", 32)
>>> c1 = (a + 32) & (b & 0xff)
>>> c2 = (b & 0xff)
>>> s = Solver()
>>> s.add(c1 == c2)
>>> s.check()
sat
>>> s.model()
[b = 0, a = 4294967199]

Обратите внимание, что очевидно, что ограничение должно быть sat всякий раз, когда b попадает в диапазон[0x00000000, 0xffffff00].

Итак, вот мой вопрос: возможно ли вообще для решателя SMT, как Z3, предоставить информацию о «диапазоне» выполнимого ограничения?Благодаря.

Answer 1

Ответ, предоставленный Левент Эркок , действителен в целом и, в большинстве практических случаев, он является единственным, который стоит рассмотреть.

Однако, технически говоря, этоне проблема, которая полностью недостижима для OMT решателей, по крайней мере, когда рассматриваемая область значений является конечной и, возможно, small .В этом случае можно просто перечислить все возможные значения в постановке задачи.Естественно, не следует ожидать, что этот подход будет очень хорошо масштабироваться.

---

Пример.

Цель этой модели - найти наибольший интервал delta, содержится в [low, upp], так что для всех значений внутри интервала выполняется определенное логическое свойство Prop.

Файл: test.smt2

(set-option :produce-models true)

(declare-fun low () (_ BitVec 4))
(declare-fun upp () (_ BitVec 4))
(declare-fun delta () (_ BitVec 4))

(declare-fun Prop () Bool)

(assert (bvule low upp))
(assert (= delta (bvadd upp (bvneg low) (_ bv1 4))))

; Put in relation a domain value with the desired Property
(assert (=> (and (bvule low (_ bv0 4)) (bvule (_ bv0 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv1 4)) (bvule (_ bv1 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv2 4)) (bvule (_ bv2 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv3 4)) (bvule (_ bv3 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv4 4)) (bvule (_ bv4 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv5 4)) (bvule (_ bv5 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv6 4)) (bvule (_ bv6 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv7 4)) (bvule (_ bv7 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv8 4)) (bvule (_ bv8 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv9 4)) (bvule (_ bv9 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv10 4)) (bvule (_ bv10 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv11 4)) (bvule (_ bv11 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv12 4)) (bvule (_ bv12 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv13 4)) (bvule (_ bv13 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv14 4)) (bvule (_ bv14 4) upp)) Prop))
(assert (=> (and (bvule low (_ bv15 4)) (bvule (_ bv15 4) upp)) Prop))

; These are just to make the solution "interesting"
; Your problem should already entail some values bvX for
; which Prop is false
(assert (=> (and (bvule low (_ bv5 4)) (bvule (_ bv5 4) upp)) (not Prop)))
(assert (=> (and (bvule low (_ bv6 4)) (bvule (_ bv6 4) upp)) (not Prop)))
(assert (=> (and (bvule low (_ bv13 4)) (bvule (_ bv13 4) upp)) (not Prop)))

(maximize delta)

(check-sat)
(get-objectives)
(get-model)

Краткое объяснение.Цель целевой функции - максимизировать размер интервала [low, upp], который измеряется delta.Наибольшее значение delta равно 2^N, что соответствует интервалу [0, 2^N - 1].

. Ограничение:

(assert (=> (and (bvule low (_ bv0 4)) (bvule (_ bv0 4) upp)) Prop))

говорит о том, что если содержится значение bv0в текущем интервале [low, upp] свойство Prop должно храниться.

Ограничение:

(assert (=> (and (bvule low (_ bv5 4)) (bvule (_ bv5 4) upp)) (not Prop)))

говорит о том, что для значения bv5 свойство Prop не выполняется.То же самое для bv6 и bv13.Эти ограничения только для того, чтобы сделать решение интересным.Ваша проблема должна уже содержать некоторые значения bvX, для которых свойство Prop не может быть true .

Оптимальное решение соответствует требуемому значению:

~$ time ./optimathsat test.smt2 
sat

(objectives
 (delta (_ bv6 4))
)
( (low (_ bv7 4))
  (upp (_ bv12 4))
  (delta (_ bv6 4))
  (Prop true) )

real    0m0,042s
user    0m0,029s
sys     0m0,013s

Естественно, эту же формулу можно также решить с помощью z3.

Answer 2

Если вы запрашиваете действительный «самый широкий» диапазон значений, чтобы ваше свойство было удовлетворено для всех чисел в этом диапазоне, это было бы количественной проблемой оптимизации.(Кроме того, то, что означает «самый широкий» в этом контексте, трудно выразить.) В настоящее время ни z3, ни какой-либо другой SMT-решатель, о котором я знаю, к сожалению, не могут решить такие проблемы.

Однако, если выища минимальные и максимальные значения b, которые будут храниться в вашем имуществе, тогда вы можете использовать класс Optimize для этого:

from z3 import *

a = BitVec("a", 32)
b = BitVec("b", 32)
c1 = (a + 32) & (b & 0xff)
c2 = (b & 0xff)

s = Optimize()
s.add(c1 == c2)

min_b = s.minimize(b)
max_b = s.maximize(b)
s.set('priority', 'box')
s.check()

print "min b = %s" % format(min_b.value().as_long(), '#x')
print "max b = %s" % format(max_b.value().as_long(), '#x')

Это печатает:

min b = 0x0
max b = 0xffffffff

[В сторону: максимальное значение b отличается от того, что вы предсказывали.Но то, что говорит z3, выглядит хорошо для меня: если вы выберете a как 0x7fffffdf, тогда a+32 будет 0x7fffffff, что составляет все 1 с;и, таким образом, c1 и c2 будут эквивалентны для любого значения b.Так что ничто здесь действительно не ограничивает b в любом случае.Возможно, вы имели в виду другое ограничение?]

Но, что более важно, обратите внимание, что это не означает, что ваше свойство будет истинным для всех значений b в этом диапазоне: все этоговорят, что из всех значений b, которые удовлетворяют вашей собственности, это минимальные и максимальные значения, которые b может принять(В данном конкретном случае оказывается, что все значения в этом диапазоне удовлетворяют его, но мы сами это сделали.) Например, если вы добавите ограничение, что b равно , а не 5,вы все равно получите эти границы.Надеюсь, это понятно!