search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.3k stars 1.48k forks source link

Question about bvadd that has just one argument #6517

Closed depted closed 1 year ago

depted commented 1 year ago

Greetings, I have a question about bvadd.

Recently, I saw a formula written in smtlibv2. The formula is as follows:

(declare-fun b () (_ BitVec 4))
(assert (and (= (bvadd b) b) (distinct b (_ bv0 4))))
(check-sat)

I think that this formula cannot be parsed. Since according to standard of smtlibv2(https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml), bvadd should have two arguments. However, z3 parsed the formula and showed the result 'sat' even though bvadd has just one argument, which is 'b' in the formula. I tried to solve the formula using cvc5 and it gave me a parsing error(BITVECTOR_ADD must have at least 2 children).

Is this situation intended in z3? If so, could I know how to understand the situation?

Thanks for reading :)

NikolajBjorner commented 1 year ago

For z3 you can parse associative/commutative operators with any > 0 arguments in Z3. When they are given 1 argument, they are treated as no-ops. so (* x) is x, (+ x) is x, (bvmul x) is x etc. The meaning of bvadd is idempotent on one argument. The simplifier/pre-processor eliminates this use of bvadd. z3 strives to be able to process SMTLIB2 compliant input, but does not restrict itself to reject input that has unambiguous meaning.