0

I'm trying to use Z3 to solve arithmetic equations using bitvector arithmetic. I was wondering if there is a way to handle also Real numbers. For example if I can specify a constant different from #x1 and use real number instead.

(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)
marco
  • 51
  • 3

1 Answers1

0

Yes, both SMT-Lib (and Z3) fully support real numbers: http://smtlib.cs.uiowa.edu/theories-Reals.shtml

You can simply write your example as follows:

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

You can also mix/match Int/Real/Bitvector, so long as everything is properly typed. Here's an example showing how to use Ints and Reals together:

(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)

However, note that conversion from bit-vectors to integers is usually uninterpreted. See here for a discussion: Z3 int2bv operation

Community
  • 1
  • 1
alias
  • 28,120
  • 2
  • 23
  • 40
  • Thank you for your response. What You've said is right, anyway with 'Real' I cannot use bitwise operations, but I must use bit vectors. – marco Dec 20 '15 at 13:50
  • Mixing/matching of types are allowed too; so long as everything is properly typed. See the updated answer. – alias Dec 20 '15 at 23:45
  • http://stackoverflow.com/questions/16841212/z3-convert-between-fp-and-bitvector may be relevant. – jpe Dec 21 '15 at 18:42