Solution soundness on QF_BV formula

[rainoftime]

Hi, for the following formula, boolector 6fce0ac yields sat, but both cvc4 and z3 return unsat

(set-logic QF_BV)
(declare-const x (_ BitVec 8))
(declare-const y (_ BitVec 8))
(declare-const z (_ BitVec 8))
(assert (or (not (= (bvadd x y z) (bvadd (bvadd x y) z)))
            (not (= (bvmul x y z) (bvmul (bvmul x y) z)))
            (not (= (bvand x y z) (bvand (bvand x y) z)))
            (not (= (bvor x y z) (bvor (bvor x y) z)))
            (not (= (bvxor x y z) (bvxor (bvxor x y) z)))
            (not (= (bvxnor x y z) (bvxnor (bvxnor x y) z)))))
(check-sat)

[arminbiere]

Reduces to:

(set-logic QFBV) (declare-const x ( BitVec 1)) (declare-const y ( BitVec 1)) (declare-const z ( BitVec 1)) (assert (distinct (bvxnor x y z) (bvxnor (bvxnor x y) z))) (check-sat)

[arminbiere]

SMT lib is confusing here. Apparently 'bvxnor' was once left associative (which means the reduced formula then should be 'unsat' even though Boolector says 'sat' with all variales true), but this has been removed recently:

See http://smtlib.cs.uiowa.edu/Logics/QF_BV.smt2:

2020-05-20 bvxnor is no longer marked as left associative, as that is inconsistent with its meaning as the negation of bvxor.

However, SMT lib does not really define what multi-arity BV operations do (only binary versions). Here it would make sense to either keep the left-associativity or just define (bvxnor x y z) to be (bvnot (bxor x y z)). That is what Boolector does (just checked the parser).

In Z3 https://github.com/Z3Prover/z3/issues/2408 the same issue occurred, but apparently Nikolaj fixed it by disallowing multiple arity XNOR.

[arminbiere]

I started to check VHDL and Verilog semantics on this. For VHDL 'xnor' I found various references which claim operators (except for 'nor' and 'nand') are associative. In Verilog multiple argument '^~' (xnor) is not precisely defined (but operators are left associative by default), and it also has a (unary) 'xnor' reduction operator (also '^~'), for which I could not find precise semantics. It is supposed to 'xnor' all bits of a bit-vector. Just this definition hints at the natural semantics that 'xnor' is assumed to be associative. So I would actually want to argue that SMTLIB should change its semantics back to 'bvxnor' being left-associative. Note that as binary operator 'bvxnor' is associative, e.g.,

(set-logic QF_BV)
(declare-const x (_ BitVec 1))
(declare-const y (_ BitVec 1))
(declare-const z (_ BitVec 1))
(assert (distinct (bvxnor (bvxnor x y) z) (bvxnor x (bvxnor y z))))
(check-sat)

[arminbiere]

Apparentely @mpreiner removed left associativity of XNOR in Boolector 36b7581e27c3b35129421f3c6f99b2800dda15ec even though the commit message claims the opposite.

[aniemetz]

Operator XNOR was mistakenly marked as :left-associative in SMT-LIB, this has been corrected recently. The behavior for n-ary XNORs is not defined in SMT-LIB now. We should probably not allow n-ary XNORs in order to avoid confusion.

[mpreiner]

This all started with https://github.com/Boolector/boolector/issues/61. Back than quite a few BV solvers disagreed on how to handle this. The commit message on 36b7581 is wrong. It actually changes bvxnor from left-assoc to (bvnot (bvxor ... )).

[mpreiner]

But I agree with @aniemetz, we should drop support for n-ary bvxnor.

[aniemetz]

CVC4 previously still treated bvxnor as left-associative, fixed here: https://github.com/CVC4/CVC4/pull/5138

[aniemetz]

We now reverted back to our previous behavior, where we only allow two operands to bvxnor: https://github.com/Boolector/boolector/commit/1cff6b0bff8a6c783790c864b0b2cafbcaf8302e

[arminbiere]

Still think we should convince the SMTLIB maintainers, to first have multi-argument operators and then make those left-associative (except for NAND and NOR). The point is that the only place where I have seen usage of XNOR was in the context of hardware description languages, where apparently it is left-associative (and in Verilog there is even a reduction operator). I will take this on me.

[arminbiere]

BTW, unary usage also make sense (since I think Verilog's reduction operators work on single bit bit-vectors). Then XOR is like a copy operator (buffer) while XNOR is a NOT.

[alemuller]

VHDL-2008 also supports unary operator for and, or, nand, nor, xor and xnor. Those logical reduction operators are only defined for one-dimensional array type.

The package ieee.std_logic_1164 implements the unary xor operation as:

function "xor" (l : STD_ULOGIC_VECTOR) return STD_ULOGIC is
  variable result : STD_ULOGIC := '0';
begin
  for i in l'reverse_range loop
    result := xor_table (l(i), result);
  end loop;
  return result;
end function "xor";

Note, the array ranges can be in upward direction (0 to 3) or downward direction (3 downto 0). The common pratice is to declare one-dimension array type in downward direction (3 downto 0), and arrays of types in upward direction (x is array(0 to 3) of bit(3 downto 0)).

The loop statement from the library code for a one-dimensional array with range (3 downto 0) could be written as:

for i in 0 to 3 loop
    result := xor_table (l(i), result);
end for;

The xor_table defines binary xor operation over binary numbers and metavalues.

The behavior of VHDL-2008 reductions operators are defined at IEEE Std 1076-2008 9.2.2.

[arminbiere]

And more importantly the 'std_logic_1164' implementation of VHDL has:

 function "xnor" (l : STD_ULOGIC; r : STD_ULOGIC) return UX01 is
  begin
    return not_table(xor_table(l, r));
  end function "xnor";

So that is exactly what the current SMT standard says. Also check out this UNSAT formula:

(set-logic QF_BV)
(declare-fun a () (_ BitVec 1))
(declare-fun b () (_ BitVec 1))
(declare-fun c () (_ BitVec 1))
(assert 
  (or
    (distinct (bvxnor a ((bvxnor b c))) (bvxnor (bvxnor a b) c))
    (distinct (not (bvxor a ((bvxnor b c)))) (bvxnor (bvxnor a b) c))
    (distinct (not (bvxor a ((not (bvxor b c))))) (bvxnor (bvxnor a b) c))
    (distinct (bvxor a ((bvxor b c))) (bvxnor (bvxnor a b) c))
  )
)
(check-sat)

So I think we need to get XNOR back to be left-associative in the SMTLIB.

[aniemetz]

@barrettcw @tinelli what's your opinion on this?

[aniemetz]

@arminbiere VHDL the code you posted is not left-associative. What you posted is what Boolector implemented until I reverted to the old behavior where we only allow 2 operands.

[aniemetz]

@arminbiere did you mean to say that we could revert back to our previous behavior of n-ary bvxor since this is exactly what VHDL implements?

[arminbiere]

Yes, the VHDL code for "xnor" is only binary, but the other "xor" code from @alemuller is for reduction and thus could be considered associated. But once more in Verilog it is said to be left-associative and has a reduction operator built in the language (which requires associativity and commutativity similar to 'bvor' and 'bvand') and further even works with one argument (single bits). So yes, the semantics implemented in Boolector before Mathias (tried to) remove the left-associative is what I think should be in SMTLIB, maybe extended to the unary case as well ...

[aniemetz]

Mathias didn't "try to remove left-assiociativity" for bvxnor, before his commit (which had a misleading and incorrect commit message) it was binary only. He introduced the n-ary case as implemented in the VHDL code above.

[arminbiere]

BTW, the semantics would be even sound if '^~' (xnor in Verilog) and '^' (xor in Verilog) have the same operator precedence:

a ^~ b ^ c ^~ d ^ e

has 2 '~' which cancel. In essence count the number XNORs say N and then replace them all by XOR. If N is odd you need to either negate the whole term or just one variable or XOR with '1'. If N is even then replacing by XOR is enough.

Armin

P.S. Further equality on the Boolean level is the same as 'iff' as 'XNOR' and all have the semantics discussed above even though for SMTLIB "(= a b c)" is problematic, because it does not match the interpretation in Mathemtical texts "(a = b) & (b = c)".

[aniemetz]

So, to summarize, Armin suggests to revert back to our previous n-ary behavior, and to convince the SMT-LIB maintainers to define the n-ary behavior for bvxnor as we had it implemented. @mpreiner you ok with this?

[mpreiner]

Sounds good. That means:

(bvxor a b c d) == (bvxor (bvxor (bvxor a b) c) d)
(bvxnor a b c d) == (bvnot (bvxor a b c d)) == (bvnot (bvxor (bvxor (bvxor a b) c) d)

?

[arminbiere]

And with the normalization I just explained:

(bvxnor a b c) == (bvxor a b c)

but automatically ...

[aniemetz]

@arminbiere I do not understand what you mean.

[aniemetz]

Sounds good. That means:

(bvxor a b c d) == (bvxor (bvxor (bvxor a b) c) d)
(bvxnor a b c d) == (bvnot (bvxor a b c d)) == (bvnot (bvxor (bvxor (bvxor a b) c) d)

?

That would be my understanding, yes.

[arminbiere]

The fix of Mathias parsed

(bxnor a b c)

as

(bvnot (bvxor a b c))

but this is bogus. XNOR is only the negation of XOR for arity 2.

[aniemetz]

So you want it to be left-associative, then? I think we'll just stick to having bvxnor binary to avoid confusion.

[arminbiere]

With automatic I mean:

(bxnor a b c) = (bxnor (bvxnor a b) c) = (bvnot (bvxor (bvnot (bxor a b)) c))

Now if you have XOR normalization somewhere in rewriting the two negations cancel:

(bvxor a b c)

[arminbiere]

@aniemetz yes left-associative as it was before the fix by Mathias ...

[aniemetz]

@arminbiere it was binary before. And that's what it is now. So we're all good then.

[arminbiere]

Sorry no, as I explained in lengthy detail, XNOR only occurs in HDL, and there it is multi-argument, so why not in SMTLIB? So I want it to be multi-argument (even unary makes sense) and then left-associative.

[aniemetz]

Yes, but it was not n-ary before Mathias' commit. We simply didn't support it.

[aniemetz]

I'll leave it up to the SMT-LIB maintainers to decide if it should be left-associative. For now we'll leave it as it is (= binary).

[arminbiere]

I think Boolector parsed multi-argument XNOR in a left-associative way before the commit (except that the assertion might have failed where now in line 2031 also XNOR is allowed) 36b7581

[arminbiere]

Ah and in line 2797 there is the change from fun to left_assoc. Yes, this also has to go in (and was not before the fix of Mathias). These two lines should be changed, but the 'is_xnor' code in ...left_assoc removed.

[mpreiner]

commit 83618821d37f136fa6bdda045997268b322ac55a (before my "fix") does not parse multi-argument bvxnor:

(set-logic QF_BV)

(declare-const a (_ BitVec 8))
(declare-const b (_ BitVec 8))
(declare-const c (_ BitVec 8))
(declare-const d (_ BitVec 8))

(assert (distinct (bvxnor a b c d) (bvxor a b c d)))
(check-sat)

$ bin/boolector test.smt2
boolector: test.smt2:8:20: 'bvxnor' has 2 arguments too much

bvxor are parsed left associative.

[aniemetz]

That's what I was saying.

[alemuller]

(bvxor a b c d) == (bvxor (bvxor (bvxor a b) c) d) (bvxnor a b c d) == (bvnot (bvxor a b c d)) == (bvnot (bvxor (bvxor (bvxor a b) c) d)

I'm not sure if that's how VHDL behaves with the usual convention (downwards range).

assume vec = "abcd";

assert vec(0) = 'd';
assert vec(1) = 'c';
assert vec(2) = 'b';
assert vec(3) = 'a';

Therefore, unrolling the loop from the code I posted earlier:

result := xor_table ('d', '0');
result := xor_table ('c', xor_table ('d', '0'));
result := xor_table ('b', xor_table ('c', xor_table ('d', '0'));
result := xor_table ('a', xor_table ('b', xor_table ('c', xor_table ('d', '0')));

But, it is also possible to declare the array with upward range, but that's not the common practice.

Also. In VHDL all logical operators have the same precedence.

---

Just made another test.

I used ghdl --synth, the vhdl front-end to yosys, to see how it deals with a unary xor.

o <= xor(i);

Is converted into:

o <= i(0) xor i(1) xor i(2) xor i(3);

Using a vhdl parser that i'm working on I made the syntax tree:

(logical_expression (logical_expression (logical_expression (i0) (i1)) (i2)) (i3))))))))
(logical_expression (logical_expression (logical_expression (d) (c)) (b)) (a))))))))

[arminbiere]

@aniemetz @mpreiner your commit consisted of two things, first it added multi-argument support for XNOR (for that actually only the last changed line is necessary and maybe the first one to avoid an assertion failure) but then it added a second part (> 10 lines) with this boolean flag 'is_xnor', which in my view is bogus, that is inconsistent with XNOR being associative. I bet you squashed several commits. Anyhow, if you are serious about having consistent source you should remove those (> 10) lines with the 'is_xnor' flag, or better just support multi-argument XNOR (only the first and last line of the commit), which in my view is the better option.

[mpreiner]

In this case no squash was made ;-)

We'll keep the current behavior (binary bvxnor) until the SMT-LIB standard changes. Otherwise, we keep getting fuzz testing issues reported on disagreeing solvers that do not adhere to the standard.