Атрибут битректа на Z3

Question

Я пытаюсь использовать Z3 для решения арифметических уравнений с использованием арифметики битвектора. Мне было интересно, есть ли способ справиться и с реальными числами. Например, если я могу указать константу, отличную от # x1, и вместо этого использовать действительное число.

(set-option :pp.bv-literals false) 
(declare-const x (_ BitVec 4)) 
(declare-const y (_ BitVec 4)) 
(assert (= (bvadd x y) #x1)) 
(check-sat) 
(get-model) 

Answer 1

Да, оба SMT-Lib (и Z3) полностью поддерживают действительные числа: http://smtlib.cs.uiowa.edu/theories-Reals.shtml

Вы можете просто написать свой пример следующим образом:

(declare-const x Real) 
(declare-const y Real) 
(assert (= (+ x y) 1)) 
(check-sat) 
(get-model) 

Вы можете также смешать/матч Int/Real/Bitvector, если все правильно напечатано. Вот пример, показывающий, как использовать Ints и Reals вместе:

(declare-const a Int) 
(declare-const b Int) 
(declare-const c Int) 
(declare-const d Real) 
(declare-const e Real) 
(assert (> e (+ (to_real (+ a b)) 2.0))) 
(assert (= d (+ (to_real c) 0.5))) 
(assert (> a b)) 
(check-sat) 
(get-model) 

Однако, обратите внимание, что преобразование из битовых векторов для целых чисел обычно необработанном. См. Здесь для обсуждения: Z3 int2bv operation