Search code examples
z3smtquantifiersbitvectorfirst-order-logic

Defining Rules for Bit Vectors in SMT2

I have switched from using Int to Bit Vectors in SMT. However, the logic QF_BV does not allow the use of any quantifiers in your script, and I need to define FOL rules. I know how to eliminate existential quantifiers, but universal quantifiers? How to do that?

Imagine a code like that:

(set-logic QF_AUFBV)

(define-sort Index () (_ BitVec 3))

(declare-fun P (Index) Bool)

(assert (forall ((i Index)) (= (P (bvadd i #b001)) (not (P i)) ) ) )
Solution

  • Strictly speaking, you're out-of-luck. According to http://smtlib.cs.uiowa.edu/logics.shtml, there's no logic that contains quantifiers and bit-vectors at the same time.

    Having said that, most solvers will allow non-standard combinations. Simply leave out the set-logic command, and you might get lucky. For instance, Z3 takes your query just fine without the set-logic part; I just tried..