Expand description
Solver-agnostic bitvector / boolean term types (#553).
BV and Bool wrap ordeal::BvTerm / ordeal::BoolTerm behind the
exact method surface the semantics encoders (wasm_semantics.rs,
arm_semantics.rs) previously used from z3::ast::{BV, Bool} — so the
encoders stay in their native idiom while becoming solver-independent.
Both backends (the default pure-Rust ordeal engine and the optional
feature-gated Z3 differential oracle) consume these terms; see
solver.rs.
§Commutative-operand canonicalization (interim shim)
ordeal 0.4 has no term normalization yet (scoped upstream for ordeal
v0.8.0, pulseengine/ordeal#29): syntactically commuted operands of a
commutative op (a*b vs b*a) can blast to structurally distinct AIGs
and, for Mul, hit a CDCL cliff. Until v0.8.0 lands, the constructors for
the commutative ops (bvadd, bvmul, bvand, bvor, bvxor, and the
Eq/Ne predicates) order their operands by a deterministic structural
key, so both sides of an equivalence query build the same term for the
same commuted expression. This is a pure reordering of arguments to
commutative SMT-LIB operations — semantics are untouched (the Z3 oracle
sees the identical canonicalized query).