[bitv] Add support for (bvnot) in the solver

This patch adds support for the negation (bvnot) operator in the
bitvector solver.

There are two components to this support:

 - First, the union-find data structure used by the solver is replaced
   with an actual union-find data structure implemented using Tarjan's
   efficient algorithm, rather than using an implementation with sets
   and maps. This is not only more efficient but also simplifies the
   implementation of the second part below.

 - Second, the new union-find data structure is augmented with a link
   between a class representative and the representative of its negated
   class. When merging two classes, their negated classes are merged as
   well (and, in particular, if a class gets forced to all ones or all
   zeroes, its negated classes gets forced to the other bit value). If a
   class is ever merged with its negated class, the problem is
   unsolvable.

Note that this also fixes a bug in the existing solver: previously, it
was possible to make bogus substitutions by asserting an equality
between a constant and a bit-vector term that depends on the constant,
for instance, `(= x (concat ((_ extract 0 0) x) ((_ extract 1 1) x)))`.
This would create the mappings `x -> x[0] @ x[1]` and `x[0] @ x[1] -> x`
in the `repr` table of the union-find, which is obviously incorrect and
confuses Alt-Ergo (see the `coherence` test).

tests/dolmen/bitv/bv2nat_bvneg.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/bv2nat_bvneg.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+
+(declare-const x (_ BitVec 64))
+(assert (distinct (bv2nat (bvneg x)) (mod (+ (bv2nat (bvnot x)) 1) 18446744073709551616)))
+(check-sat)

tests/dolmen/bitv/bv2nat_bvnot.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/bv2nat_bvnot.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+
+(declare-const x (_ BitVec 64))
+(assert (distinct (bv2nat (bvnot x)) (- 18446744073709551615 (bv2nat x))))
+(check-sat)

tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/bv2nat_bvnot_range.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(set-option :produce-models true)
+
+(declare-const x (_ BitVec 64))
+(assert (not (and (<= (bv2nat (bvnot x)) 18446744073709551615) (<= 0 (bv2nat (bvnot x))))))
+(check-sat)

tests/dolmen/bitv/coherence.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/coherence.dolmen.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const x (_ BitVec 2))
+(assert (= x (concat ((_ extract 0 0) x) ((_ extract 1 1) x))))
+(declare-fun f ((_ BitVec 2)) Int)
+(assert (distinct (f x) (f (concat ((_ extract 0 0) x) ((_ extract 1 1) x)))))
+(check-sat)

tests/dolmen/bitv/cyclic.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/cyclic.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 3))
+(assert (= ((_ extract 1 0) x) (bvnot ((_ extract 2 1) x))))
+(assert (= ((_ extract 0 0) x) #b0))
+(assert (distinct x #b010))
+(check-sat)

tests/dolmen/bitv/not-contra.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/not-contra.dolmen.smt2

@@ -0,0 +1,7 @@
+(set-logic BV)
+(set-option :produce-models true)
+
+(declare-const x (_ BitVec 2))
+(assert (= (bvnot x) #b00))
+(assert (= x #b00))
+(check-sat)

tests/dolmen/bitv/notextract.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/notextract.dolmen.smt2

@@ -0,0 +1,8 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 64))
+(declare-const y (_ BitVec 64))
+
+(assert (= ((_ extract 32 16) x) (bvnot ((_ extract 32 16) y))))
+(assert (= ((_ extract 32 0) x) ((_ extract 32 0) y)))
+(check-sat)

tests/dolmen/bitv/notnotx.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/notnotx.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 64))
+(assert (distinct (bvnot (bvnot x)) x))
+(check-sat)

tests/dolmen/bitv/notx.dolmen.expected

@@ -0,0 +1,2 @@
+
+unsat

tests/dolmen/bitv/notx.dolmen.smt2

@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+
+(declare-const x (_ BitVec 64))
+(assert (= (bvnot x) x))
+(check-sat)

tests/models/bitv/not.models.expected

@@ -0,0 +1,5 @@
+
+unknown
+(
+  (define-fun x () (_ BitVec 2) #b11)
+)

tests/models/bitv/not.models.smt2

@@ -0,0 +1,7 @@
+(set-logic BV)
+(set-option :produce-models true)
+
+(declare-const x (_ BitVec 2))
+(assert (= (bvnot x) #b00))
+(check-sat)
+(get-model)