Parametric Bit-Vector Lab

Visualize Bit-Vector operations with symbolic width k.

Elimination Rule

This operator is eliminated by rewriting it into Addition and Bitwise AND.

Algorithm 1: Function ADM

Recursively constructs admissibility constraints.

Match Expression e	Constraint
x (PBV variable)	Bw(e) > 0
z (Int constant)	True (⊤)
to-pbv(k, t)	Bw(e) > 0 ∧ ADM(t)
\|t\|	ADM(t)
t[i:j]	0 ≤ j ≤ i < Bw(t) ∧ ADM(t)
ext_z(n, t)	n ≥ 0 ∧ ADM(t)
ext_s(n, t)	n ≥ 0 ∧ ADM(t)
t1 ∘ t2	ADM(t1) ∧ ADM(t2)
ite_PBV(t1, t2, t3)	Bw(t2) ≈ Bw(t3) ∧ ⋀ ADM(t_i)
Other Binary Ops (x ⋄ y)	Bw(t1) ≈ Bw(t2) ∧ ADM(t1) ∧ ADM(t2)

Algorithm 2: Function Bw

Computes the bit-width of PBV-terms.

Match Expression e	Width
x (PBV variable)	\|x\|
to-pbv(k, t)	k
t[i:j]	i - j + 1
ext_z(n, t)	Bw(t) + n
ext_s(n, t)	Bw(t) + n
t1 ∘ t2	Bw(t1) + Bw(t2)
ite_PBV(t1, t2, t3)	Bw(t2)
Other Ops (⋄(t1...tn))	Bw(t1)

Algorithm 3: Translation Function TRANS

Translates PBV formulas to Integer Arithmetic.

                function TRANS(φ)

                  return CONV(φ) ∧ RANGE(φ) ∧ ADM(φ)

Function CONV (Conversion Table)

PBV Term	Integer Arithmetic (IA)

Algorithm 4: Function RANGE

Recursively constructs size and range constraints.

                function RANGE(e)

                  match e:

x (PBV variable)	→ 0 ≤ χ(x) < pow₂(κ(x))
\|t\|	→ e ≈ Bw(t) ∧ RANGE(t)
z (Int constant)	→ ⊤
•(t₁...t_n)	→ ⋀_i=1ⁿ RANGE(t_i)

Parametric Bit-Vector Theory Signatures

Table 1: Signature Σ_IA (Integer Arithmetic)

Symbol	SMT-LIB Syntax	Arity
≈_Int, ≉_Int	=, distinct	Int × Int → Bool
0, 1, 2, ...	0, 1, 2, ...	Int
+, -, ·, div, mod	+, -, *, div, mod	Int × Int → Int
≤, ≥, <, >	<=, >=, <, >	Int × Int → Bool

Table 2: Signatures Σ_PBV and Σ_IA(pow₂, &^ℕ)

Σ_PBV = Σ_IA + the following operators

Symbol	SMT-LIB Syntax	Arity
≈_PBV, ≉_PBV	=, distinct	PBV × PBV → Bool
<_u, >_u, <_s, >_s	bvult, bvugt, bvslt, bvsgt	PBV × PBV → Bool
≤_u, ≥_u, ≤_s, ≥_s	bvule, bvuge, bvsle, bvsge	PBV × PBV → Bool
~, -^B	bvnot, bvneg	PBV → PBV
&, \|, ⊕	bvand, bvor, bvxor	PBV × PBV → PBV
<<, >>, >>_a	bvshl, bvlshr, bvashr	PBV × PBV → PBV
+^B, -^B	bvadd, bvsub	PBV × PBV → PBV
·^B, mod^B, div^B	bvmul, bvurem, bvudiv	PBV × PBV → PBV
_[_ : _]	pextract	PBV × Int × Int → PBV
∘	concat	PBV × PBV → PBV
ext_z	pzero_extend	Int × PBV → PBV
ext_s	psign_extend	Int × PBV → PBV
\|_\|	bvsize	PBV → Int
to-pbv	int_to_pbv	Int × Int → PBV

Σ_IA(pow₂, &^ℕ) = Σ_IA + the following operators

Symbol	SMT-LIB Syntax	Arity
&^ℕ	piand	Int × Int × Int → Int
pow₂	pow2	Int → Int

Performance Evaluation

Main Results (Table 6)

Configurations (Table 5)

Benchmark	#	BASELINE	EAGER	PBV (Ours)	VBS
alive	200	71	93	107	124
ic	180	43	58	77	81
rewrite	2006	658	1221	1331	1382
syrew	1500	558	720	912	951
lemmas	70	12	14	23	23
icfb	46	1	9	12	12
mut	9441	669	1084	4863	4915
TOTAL	13443	2012	3199	7325	7488
sat		0	0	3641	3641
unsat		2012	3199	3684	3847
unique		24	57	4222	4303
time [s]		709k	634k	375k	355k

Key Insights:

PBV Dominance: Configuration PBV solves 7,325 instances, more than 3.5x the Baseline (2,012) and 2x the Eager approach (3,199).
Speed: On common instances, PBV is more than 18x faster than the Eager approach (375k seconds vs 634k seconds).
Unsat Performance: PBV excels at finding UNSAT results (3,684 vs 2,012 for Baseline).
Satisfiability: Baseline and Eager solve 0 satisfiable instances due to quantifier overhead. PBV solves 3,641.

Feature	BASELINE	EAGER	PBV
Target Theory	T_IA(pow2, &^ℕ, \|^ℕ, ⊕^ℕ)	T_IA(pow2, &^ℕ)	T_IA(pow2_★, &_★^ℕ)
Multiple Bit-widths	✕	✓	✓
Lazy pow2	✕	✕	✓
Lazy &	✕	✕	✓
\|-elimination	✕	✓	✓
⊕-elimination	✕	✓	✓
>> without mod	✕	✓	✓
New lemmas for &	✕	✓	✓
New lemmas for pow2	✕	✓	✓
No redundant axioms	✕	✓	✓
RW_B	✕	✓	✓
mod-reduction	✕	✓	✓

System Architecture

Click any component to see its internal logic (tables/algorithms).

φ₀

→

RW_B

φ₁ →

TRANS

smt-switch

→ φ₂ →

SOLVE_★

pow₂-solver

&^ℕ-solver

cvc5

PBV Formula x ∘ y

Integer Translation x · 2^k + y

Range Constraints

Admissibility Constraints

−

Operator

Parametric Width (k) 4

Value X 2

Value Y 3

Left Click: Rotate | Right Click: Pan | Scroll: Zoom