GoSMT
Native typed SMT solving in Go+
goforge.dev/gosmt is a native Go+/Go SMT solver and compatibility project.
It is pinned against Microsoft Z3 4.16.0 for differential testing, but does
not bind to Z3: released artifacts are pure generated Go.
Version 0.171.2 is the current release. The 0.171 line adds a native Z3-API total-allocation benchmark harness; the latest patch consumes the released Go+ stdlib v0.207.0.
Version 0.170 adds native compatibility-result provenance and router scaffolding for an optional compatibility backend:
Solver.Checkresults now include aBackendtag (native,z3, orunknown) so consumers can identify which engine handled each workload.- Solver mode metadata tracks
compatibility,native-only, and portfolio-oriented behavior on the Go+ solver object (SolverModeis now part of the generated API surface). - Inline affine-power normalization now accepts repeated powers up to degree 64, with a full degree-32 public benchmark and model validation.
- The compatibility and runtime tests were expanded with randomized degree-17 through degree-64 affine-power agreements and an additional pinned-Z3 parity test workload.
Version 0.169 adds exact strict and non-strict affine four-square balls and
shells. Finite upper balls enumerate complete four-coordinate affine domains,
lower bounds synthesize exterior witnesses, negation is normalized, and
arbitrary-precision or over-limit domains retain sound models or explicit
unknown. Typed GoSMT, SMT-LIB, and a new 64-case corpus agree with pinned
Z3. The gated workload uses 61.3% fewer allocations and is over 190x faster.
Version 0.168 adds exact affine four-square equations:
(a*x+b)^2+(c*y+d)^2+(e*z+f)^2+(g*w+h)^2=k. This completes the fixed
sum-of-squares ladder with bounded lattice enumeration, four
coefficient-congruence filters, affine non-image and conflict proofs,
disequality escapes, arbitrary-precision witnesses, and explicit over-limit
unknown. Typed GoSMT, SMT-LIB, and a new 64-case corpus agree with pinned
Z3. The gated workload uses 58.6% fewer allocations and is over 200x faster.
Version 0.167 adds exact strict and non-strict affine three-square balls and
shells. Finite upper balls enumerate complete coefficient-congruent
coordinate domains, lower bounds synthesize exterior witnesses, negation is
normalized, and arbitrary-precision or over-limit domains retain sound
models or explicit unknown. Typed GoSMT, SMT-LIB, and a new 64-case corpus
agree with pinned Z3. The gated workload uses 61.2% fewer allocations and is
over 149x faster.
Version 0.166 adds exact affine three-square equations:
(a*x+b)^2+(c*y+d)^2+(e*z+f)^2=k. Bounded lattice-sphere enumeration
retains all three coefficient congruences, proves finite non-images and
conflicting targets, and synthesizes disequality escapes. Arbitrary-precision
representations remain exact while over-limit non-images return explicit
unknown. Typed GoSMT, SMT-LIB, and a new 64-case corpus agree with pinned
Z3. The gated workload uses 57.8% fewer allocations and is over 137x faster.
Version 0.165 adds exact strict and non-strict disks and annuli over
(a*x+b)^2+(c*y+d)^2. Finite upper disks enumerate complete
coefficient-congruent coordinate domains, lower bounds synthesize exterior
witnesses, negation is normalized, and wide or over-limit domains retain
sound models or explicit unknown. Typed GoSMT, SMT-LIB, and a new 64-case
corpus agree with pinned Z3. The gated workload uses 59% fewer allocations
and is over 124x faster.
Version 0.164 adds the first exact mixed-base polynomial fragment:
(a*x+b)^2+(c*y+d)^2=k. Bounded two-square enumeration retains only
coefficient-congruent preimages, proves non-representability and conflicts,
provides injectivity-backed disequality escapes, returns explicit unknown
beyond complete limits, and retains wide exact models. Go+ Add now
preserves the compact structure before Go generation. Typed GoSMT, SMT-LIB,
and a new 64-case corpus agree with pinned Z3. The gated workload uses 54.3%
fewer allocations and is over 180x faster.
Version 0.163 adds exact strict and non-strict bounds for affine powers of
degrees 4 through 16. Odd degrees normalize into signed affine intervals;
even degrees use absolute-value domains with exact lower witnesses,
exhaustive finite upper ranges, negation, arbitrary-precision endpoints, and
explicit large-domain unknown. Typed GoSMT, SMT-LIB execution, and a new
64-case corpus agree with pinned Z3. The gated workload uses 57.7% fewer
allocations and is over 168x faster.
Version 0.162 introduces a reusable exact affine-power abstraction for degrees 4 through 16. Repeated multiplication normalizes independently of tree association, with arbitrary-precision nth roots, odd/even image semantics, coefficient-congruence proofs, conflicting-target detection, and parity-aware disequality escapes. Typed GoSMT, SMT-LIB execution, and a new 64-case corpus agree with pinned Z3. The gated workload uses exactly 50% fewer allocations and is over 210x faster.
Version 0.161 adds exact strict and non-strict affine cube bounds.
Monotonic cube roots and sign-aware floor/ceiling division normalize
(a*x+b)^3 into integer intervals for positive and negative coefficients.
Congruence-empty intervals prove unsatisfiable, small intervals are
exhaustive, and arbitrary-precision endpoints retain exact models. Typed
GoSMT, SMT-LIB execution, and a new 64-case corpus agree with pinned Z3. The
gated workload uses 53.8% fewer allocations and is over 160x faster.
Version 0.160 adds exact affine cube equations and disequalities.
(a*x+b)^3=k uses arbitrary-precision perfect-cube roots and coefficient
congruence to prove image membership. Injectivity supplies complete finite
escape sets for multiple disequalities, and conflicting cube targets prove
unsatisfiable without bounded search. Typed GoSMT, SMT-LIB execution, and a
new 64-case corpus agree with pinned Z3. The gated workload uses exactly 50%
fewer allocations and is over 159x faster.
Version 0.159 adds strict and non-strict bounds over
(a*x+b)*(c*y+d). Factored operands produce coefficient-congruent boundary
witnesses without polynomial expansion, normalize negation, and compose with
complete affine-square domains for finite contradiction proofs. Typed GoSMT,
SMT-LIB execution, and a new 64-case corpus agree with pinned Z3. The gated
workload uses 54.3% fewer allocations and is over 78x faster.
Version 0.158 adds strict and non-strict bounds over (a*x+b)². Exact
factor-space interval enumeration retains only coefficient-congruent variable
preimages, synthesizes lower-bound witnesses, normalizes negation, handles
wide bounds, and preserves explicit large-domain unknown. A new 64-case
corpus agrees with pinned Z3. The gated workload uses 58.3% fewer allocations
and is over 151x faster.
Version 0.157 solves products of one-symbol affine factors without expanding
the polynomial. (a*x+b)*(c*y+d)=k enumerates exact divisors and maps them
back through integer divisibility, covering shifted/scaled models, residue
contradictions, shifted squares, negative coefficients, and wide constants.
A compact GoSMT/std handoff preserves ordinary Add/Sub/ScaleInt/MulInt
syntax. A new 64-case corpus agrees with pinned Z3. The gated workload uses
52% fewer allocations and is over 204x faster.
Version 0.156 adds strict and non-strict bilinear bounds over x*y to bounded
QF_NIA. Positive, negative, negated, and arbitrary-precision intervals
construct exact witnesses; product bounds compose with exhaustive self-square
domains to prove finite contradictions. Ordinary MulInt/Le/Lt syntax,
SMT-LIB execution, and a new 64-case randomized corpus agree with pinned Z3.
The gated interval workload uses 60.9% fewer allocations and is over 166x
faster.
Version 0.155 adds exact strict and non-strict self-square inequalities to the
bounded QF_NIA fragment. Lower bounds synthesize the nearest valid integer;
upper bounds enumerate complete domains of up to 63 integers, enabling exact
interval models and contradiction proofs. Negation, arbitrary-precision
bounds, explicit large-domain unknown, ordinary typed GoSMT comparisons,
and SMT-LIB execution are covered by a new 64-case corpus against pinned Z3.
The gated interval workload uses 61.1% fewer allocations and is over 173x
faster.
Version 0.154 makes bounded QF_NIA disequality search sound by tracking exhaustiveness per symbol instead of treating a finite heuristic candidate set as a proof domain. Finite product exclusions receive deterministic escape models beyond every target, while conflicting equalities and equality/disequality pairs on repeated products prove unsatisfiable directly. The expanded four-way Z3 corpus covers coupled models, square-image impossibility, escape models, and conflicts. The new gated workload uses 64.3% fewer allocations and is over 152x faster.
Version 0.153 adds an exact bounded QF_NIA fragment for constant-target
integer products. Coupled factor graphs, self-square image proofs, exact
models, explicit resource outcomes, typed GoSMT, and SMT-LIB execution are
covered by a 64-case corpus against pinned Z3. The ordinary Go+ API compacts
MulInt/EqInt/And relations without intermediate expression trees. The
gated model workload uses 67.6% fewer allocations and is over 122x faster.
Version 0.152 adds complete finite QF_AUFBV models for symbolic addresses.
Resolved bit-vector addresses now feed back into array interpretations, while
otherwise unconstrained addresses receive deterministic witnesses. The new
dependent-width Go+ BitVecArrayReadAt abstraction retains the address and
selected cell together without materializing a general formula. Typed GoSMT,
SMT-LIB get-value, and a 64-case model corpus agree with pinned Z3. The
model workload uses 57.7% fewer allocations and is over 222x faster.
Version 0.151 adds compact model synthesis for the all-aliased
fp.fma(x,x,x) form. Both roots of x²+x=result are derived across all five
rounding modes, adjacent IEEE values are probed, and only exact
fused-operation witnesses are committed. Binary128, signed zeros, infinities,
NaN payloads, subnormals, typed GoSMT, and both SMT-LIB paths are covered by a
64-case corpus against pinned Z3. Typed execution uses 61.5% fewer allocations
and is over 11,626x faster; streaming uses 93.6% fewer allocations and is over
2.16x faster than the complete parser.
Version 0.144 completes fixed-result fp.min and fp.max model synthesis
for negated atoms. A deterministic alternate IEEE result—+0 unless forbidden,
then +1—is evaluated through the exact kernel and committed only when its bits
differ from the forbidden target. Positive and negated cases now cover every
target, including NaNs, signed zeros, binary128, self operands, and paired
independent atoms. The exact-bit 64-case corpus agrees with pinned Z3. Typed
execution uses 70.6% fewer allocations and is over 392x faster; paired
streaming uses 97.6% fewer allocations and is over 2.76x faster.
Version 0.143 adds exact operand synthesis for positive fixed-result
fp.min and fp.max atoms. The kernel-validated target,target identity
reproduces every IEEE pattern, including NaN payloads, signed zeros,
infinities, binary128 values, and self operands; two independent atoms remain
on the compact path. A new 64-case exact-bit result-image corpus agrees with
pinned Z3. The typed workload uses 5 versus Z3’s 17 allocations and is over
342x faster; paired streaming uses 9 versus 369 allocations and is over 2.71x
faster.
Version 0.142 adds canonical model synthesis for up to two independent unconstrained floating-point order atoms. Strict, non-strict, negated, and self comparisons work across arbitrary formats without constructing a bit-blast graph; shared and mixed systems retain the complete solver path. Binary128, all four order directions, both SMT-LIB executors, and a new 64-case existential corpus agree with pinned Z3. The typed workload uses 5 versus Z3’s 14 allocations and is over 359x faster; paired streaming uses 9 versus 162 allocations and is over 2.33x faster.
Version 0.141 adds exact Real source synthesis for fixed floating-point conversion results. Finite targets use exact rational preimages; signed zero and infinities use rounding-direction-aware witnesses, all committed only after forward validation. NaN and directionally unreachable images are rejected. Binary128, every rounding mode, typed GoSMT, both SMT-LIB paths, and a new 64-case model-valid corpus are covered against pinned Z3. The typed workload uses 6 versus Z3’s 13 allocations and is over 1,377x faster; four-image streaming uses 29 versus 274 allocations and is over 2.73x faster.
Version 0.140 adds exact signed and unsigned bit-vector source synthesis for fixed floating-point conversion results. Integer and extremal candidates are committed only after forward validation; finite nonintegers, NaNs, negative zero, and unsigned negative infinity are proved outside the image. Arbitrary-width sources, binary128, every rounding mode, and a new 64-case corpus agree with pinned Z3. Direct bit-vector model lookup reduces the typed workload to 7 versus Z3’s 14 allocations while remaining over 507x faster; four-image QF_FPBV streaming uses 29 versus 306 allocations and is over 3.05x faster than the complete parser.
Version 0.139 adds exact source synthesis for unconstrained fp.to_sbv and
fp.to_ubv. Fixed result bits are interpreted as their indexed signed or
unsigned integer, nearby FP candidates are constructed, and a source is
committed only when the asserted conversion is defined and matches exactly;
nonimage integers remain unknown. Arbitrary result widths, all five modes,
binary128, and a new 64-case corpus agree with pinned Z3. The typed workload
uses 5 versus Z3’s 14 allocations and is over 619x faster; four-image
streaming execution uses 29 versus 282 allocations and is over 2.85x faster
than the complete parser.
Version 0.138 adds exact source synthesis for unconstrained floating-point format conversion. Fixed targets are reverse-converted under every rounding direction and nearby source candidates are committed only after exact forward validation with the asserted mode; narrowing targets outside the conversion image remain unknown. Widening, narrowing, signed zero, binary128, all five modes, and a new 64-case corpus agree with pinned Z3. The typed workload uses 5 versus Z3’s 14 allocations and is over 666x faster; four-format streaming execution uses 140 versus 420 allocations and is over 2.19x faster than the complete parser.
Version 0.137 adds exact source synthesis for one-term unconstrained
fp.to_real equalities. A solved rational target is rounded to a candidate
and committed only when exact conversion validates it; unrepresentable finite
targets remain unknown. Arbitrary formats, affine coefficients, binary128,
typed GoSMT, and both SMT-LIB paths are covered by a new 64-case corpus against
pinned Z3. The typed workload uses 6 versus Z3’s 12 allocations and is over
528x faster; four-image streaming execution uses 45 versus 284 allocations and
is over 2.07x faster than the complete parser.
Version 0.136 adds exact canonical models for distinct unconstrained fp.rem
operands. Every finite result selects the kernel-validated
rem(result, +infinity) witness across arbitrary formats; infinite result
patterns are proved impossible. A new 64-case result-image corpus validates
the witness with pinned Z3. The typed workload uses 5 versus Z3’s 17
allocations and is over 1.47 million times faster; paired streaming execution
uses 9 versus 198 allocations and is over 2.95x faster than the complete
parser.
Version 0.135 adds exact model synthesis for unconstrained fp.sqrt sources.
Kernel-validated rounded-square and adjacent candidates cover ordinary result
images across arbitrary formats and all five modes; negative nonzero results
are proved impossible, while unsupported compact image points remain unknown.
A new 64-case result-image corpus agrees with pinned Z3. The typed workload
uses 5 versus Z3’s 13 allocations and is over 4,138x faster; paired streaming
execution uses 9 versus 163 allocations and is over 2.24x faster than the
complete parser.
Version 0.134 adds exact canonical models for three distinct unconstrained
fp.fma operands. A fixed ordinary result selects the kernel-validated
fma(result, 1, signed-zero) witness without decomposing the fused operation.
A new 64-case result-image corpus agrees with pinned Z3. The typed workload
uses 5 versus Z3’s 21 allocations and is over 10,600x faster; paired streaming
execution uses 7 versus 146 allocations and is over 2.12x faster than the
complete parser.
Version 0.133 adds exact canonical models for distinct unconstrained fp.div
operands. A fixed ordinary result selects a kernel-validated
result-divided-by-one witness across arbitrary formats and all five rounding
modes. A new 64-case result-image corpus agrees with pinned Z3. The typed
workload uses 5 versus Z3’s 17 allocations and is over 54,000x faster; paired
streaming execution uses 9 versus 200 allocations and is over 2.96x faster
than the complete parser.
Version 0.132 adds exact canonical models for distinct unconstrained fp.mul
operands. A fixed ordinary result selects a kernel-validated result-times-one
witness across arbitrary formats and all five rounding modes. A new 64-case
result-image corpus agrees with pinned Z3. The typed workload uses 5 versus
Z3’s 17 allocations and is over 25,000x faster; paired streaming execution
uses 9 versus 200 allocations and is over 3.00x faster than the complete
parser.
Version 0.131 adds exact canonical models for distinct unconstrained fp.sub
operands. A fixed ordinary result selects a kernel-validated
result-minus-signed-zero witness across arbitrary formats and all five
rounding modes. A new 64-case result-image corpus agrees with pinned Z3. The
typed workload uses 5 versus Z3’s 17 allocations and is over 1,073x faster;
paired streaming execution uses 9 versus 200 allocations and is over 2.70x
faster than the complete parser.
Version 0.130 adds exact canonical models for distinct unconstrained fp.add
operands. A fixed ordinary result selects a kernel-validated
result-plus-signed-zero witness across arbitrary formats and all five rounding
modes. A new 64-case result-image corpus agrees with pinned Z3. The typed
workload uses 5 versus Z3’s 17 allocations and is over 1,154x faster; paired
streaming execution uses 9 versus 200 allocations and is over 2.63x faster
than the complete parser.
Version 0.129 adds exact model synthesis for unconstrained
fp.roundToIntegral sources. Fixed result patterns in the operator’s image
select themselves as canonical preimages, while non-fixed patterns are proved
unsatisfiable across all five rounding modes. A new 64-case unconstrained
corpus agrees with pinned Z3. The typed workload uses 5 versus Z3’s 13
allocations and is over 757x faster; paired streaming execution uses 9 versus
165 allocations and is over 2.58x faster than the complete parser.
Version 0.128 bridges exact fp.to_real expressions into ordinary linear
Real arithmetic. Directly assigned floating-point symbols can now determine
otherwise unconstrained Real symbols, participate in mixed equalities and
order constraints, and produce a single exact combined model. Typed GoSMT and
both general and streaming SMT-LIB paths share the solver-neutral Go+ std
relation. A new 64-case mixed corpus agrees with pinned Z3. Streaming uses 82
versus 348 allocations and is over 2.19x faster; the typed workload uses 10
versus Z3’s 25 allocations and is over 121x faster.
Version 0.127 extends exact fp.to_real into affine arithmetic across directly
assigned floating-point symbols: rational scaling, addition/subtraction,
equality, strict and non-strict order, cancellation, and exact model
evaluation. The fixed-inline relation lives in solver-neutral Go+ std, while
typed GoSMT and both general and streaming SMT-LIB paths retain conversion
metadata through arithmetic. A new 64-case affine corpus agrees with pinned
Z3. Streaming uses 56 versus 365 allocations and is over 2.70x faster; the
typed workload uses 12 versus Z3’s 32 allocations and is over 96x faster.
Version 0.126 adds exact arbitrary-format fp.to_real. Every finite
floating-point value converts to an exact rational without a host
floating-point intermediate; signed zeros map to exact zero, while NaN and
infinity use a stable value permitted by SMT-LIB’s unspecified semantics.
Go+ retains context and format indices, and directly assigned symbols use a
compact relation for equality and model extraction. Separate 160-case ground
and 64-case assigned-symbol corpora agree with pinned Z3. Streaming uses 27
versus 209 allocations and is over 2.22x faster; the paired typed workload
uses 13 versus Z3’s 26 allocations and is over 106x faster.
Version 0.125 completes the SMT-LIB numeric conversion overload family with
exact ((_ to_fp e s) rm Real) conversion. Arbitrary-precision rationals are
rounded directly across all five modes without an intermediate host float.
Go+ retains context and target format as indices; solver-neutral std adds a
compact exact-Real assignment and directly assigned Real-to-FP relation.
Separate 160-case ground and 64-case assigned-symbol corpora agree with pinned
Z3. Streaming uses 29 versus 196 allocations and is over 5.0x faster; the
paired typed workload uses 13 versus Z3’s 27 allocations and is over 89x
faster.
Version 0.124 adds exact floating-point format conversion through
((_ to_fp e s) rm fp). Finite inputs are decoded exactly and rounded once
into arbitrary target formats across all five SMT-LIB modes; signed zero and
infinities are preserved and NaNs receive a stable target representation.
Go+ retains source context and target format as indices, while solver-neutral
std provides inline and arbitrary-width kernels plus compact assigned-symbol
relations. Separate 160-case ground and 64-case assigned-symbol corpora agree
with pinned Z3. Streaming uses 11 versus 193 allocations and is over 2.45x
faster; the paired typed workload uses 11 versus Z3’s 27 allocations and is
over 109x faster.
Version 0.123 adds exact arbitrary-width signed and unsigned bit-vector to
floating-point numeric conversion across all five SMT-LIB rounding modes.
The signed two-argument (_ to_fp e s) overload remains distinct from IEEE
bit-pattern reinterpretation, while (_ to_fp_unsigned e s) covers unsigned
inputs. Go+ retains context, source width, and target format as indices;
solver-neutral std provides inline and arbitrary-width kernels plus compact
assigned-symbol relations. Separate 160-case ground and 64-case
assigned-symbol corpora agree with pinned Z3. Streaming uses 11 versus 186
allocations and is over 2.89x faster; the paired typed workload uses 15 versus
Z3’s 31 allocations and is over 96x faster.
Version 0.122 adds exact arbitrary-width fp.to_ubv and fp.to_sbv across
all five SMT-LIB rounding modes. Go+ retains context, floating-point format,
and result width as indices; solver-neutral std supplies an allocation-free
inline path, arbitrary-width fallback, compact assigned-symbol relations, and
a stable permitted model for unspecified conversions. Separate 160-case
ground and 64-case assigned-symbol corpora agree with pinned Z3. Streaming
uses 9 versus 140 allocations and is over 2.42x faster; the paired typed
workload uses 13 versus Z3’s 29 allocations and is over 112x faster.
Version 0.121 adds exact arbitrary-format fp.rem with the SMT-LIB
nearest-even integer quotient rule. Modular arithmetic handles extreme
exponent gaps without materializing enormous quotients, while signed zero,
NaNs, infinities, and binary128 behavior remain exact. An inline-width path
complements the arbitrary-width implementation. Separate 160-case ground and
64-case assigned-symbol corpora agree with pinned Z3. Streaming uses 11 versus
184 allocations and is over 2.00x faster; the typed workload uses 10 versus
Z3’s 21 allocations and is over 110x faster.
Version 0.120 adds exact arbitrary-format fp.sqrt across all five SMT-LIB
rounding modes. The solver-neutral kernel compares integer squares and exact
midpoints without host floating point, preserving irrational rounding,
subnormals, signed zero, negative-input NaN, infinity, and binary128 behavior.
An allocation-free inline integer-square-root path complements the
arbitrary-width implementation. Separate 160-case ground and 64-case symbolic
corpora agree with pinned Z3. Streaming uses 9 versus 138 allocations and is
over 2.18x faster; the typed workload uses 9 versus Z3’s 18 allocations and
is over 146x faster.
Version 0.119 adds exact arbitrary-format fp.fma across all five SMT-LIB
rounding modes. Product and addend are combined exactly before one final
rounding, including cancellation cases that differ from fp.mul followed by
fp.add. Signed zero, invalid infinite products, opposite infinities,
subnormal results, overflow, and extreme binary128 exponent gaps are covered.
An allocation-free inline fused accumulator complements the arbitrary-width
sticky-bit path. Separate 160-case ground and 64-case symbolic corpora agree
with pinned Z3. Streaming uses 13 versus 236 allocations and is over 2.90x
faster; the typed workload uses 11 versus Z3’s 26 allocations and is over
119x faster.
Version 0.118 adds exact arbitrary-format fp.div across all five SMT-LIB
rounding modes. The quotient core rounds exact integer ratios without host
floating point, covering recurring fractions, signed zero, division by zero,
zero/infinity indeterminacy, gradual underflow, overflow, infinities, and NaNs.
An allocation-free inline-width path complements the arbitrary-width fallback;
typed Go+ retains context and format indices, with compact assigned-symbol
relations. Separate 160-case ground and 64-case symbolic corpora agree with
pinned Z3. Streaming uses 11 versus 185 allocations and is over 2.38x faster;
the typed workload uses 10 versus Z3’s 22 allocations and is over 138x faster.
Version 0.117 adds exact arbitrary-format fp.mul across all five SMT-LIB
rounding modes. The Go+ std implementation covers signed zero, zero times
infinity as NaN, gradual underflow, overflow, infinities, and NaNs, using an
inline-width core with an arbitrary-width fallback. Typed Go+ retains context
and format indices, and assigned symbols use a compact solver relation.
Separate 160-case ground and 64-case symbolic corpora agree with pinned Z3.
Streaming uses 11 versus 185 allocations and is over 2.92x faster; the typed
workload uses 10 versus Z3’s 21 allocations and is over 150x faster.
Version 0.116 adds exact arbitrary-format fp.sub across all five SMT-LIB
rounding modes. Subtraction shares the proven addition normalization core
while preserving cancellation and signed-zero rules, gradual underflow,
overflow, extreme exponent gaps, infinities, and NaNs. Typed Go+ retains
context and format indices, and assigned symbols use a distinct compact std
relation. Separate 160-case ground and 64-case symbolic corpora agree with
pinned Z3. Streaming uses 11 versus 185 allocations and is over 2.77x faster;
the typed workload uses 10 versus Z3’s 21 allocations and is over 148x faster.
Version 0.115 adds exact arbitrary-format fp.add across all five SMT-LIB
rounding modes. It covers ties, gradual underflow, overflow, cancellation
sign, extreme exponent gaps, infinities, and NaNs, with an allocation-free
inline-width core and arbitrary-width fallback in Go+ std. Typed Go+ retains
context and format indices; assigned symbols use a compact solver relation.
Separate 160-case ground and 64-case symbolic wire corpora agree with pinned
Z3. Streaming uses 11 versus 185 allocations and is over 2.95x faster; the
typed workload uses 10 versus Z3’s 21 allocations and is over 156x faster.
Version 0.114 adds native (fp sign exponent significand) construction and
all five indexed SMT-LIB special values: positive and negative zero, positive
and negative infinity, and NaN. Go+ retains the context and computes the
result format as [exponentBits, trailingBits+1]; solver-neutral std supports
ground and arbitrary-term construction, including binary128. A new 64-case
wire corpus agrees with pinned Z3. Streaming execution uses 9 allocations
versus the complete parser’s 267 and is over 8.71x faster; the typed workload
uses 4 versus Z3’s 19 allocations and is over 195x faster.
Version 0.113 adds exact fp.abs, fp.neg, fp.min, and fp.max to
SMT-LIB QF_FP execution. Reusable Go+ std constructors lower unary operations
over arbitrary bit-vector terms, while compact direct-symbol min/max relations
retain the complete general fallback. A new 64-case wire corpus agrees with
pinned Z3 across NaNs, signed zeros, infinities, and subnormals. Streaming
fp.min uses 11 allocations versus the complete parser’s 269 (95.9% fewer)
and is over 2.98x faster; the typed workload uses 10 versus Z3’s 22
allocations and is over 153x faster.
Version 0.112 exposes fp.eq, fp.lt, fp.leq, fp.gt, and fp.geq
through complete and streaming SMT-LIB execution, backed by reusable
arbitrary-term equality/order constructors in Go+ std. Ground, direct-symbol,
negated, reversed, and nested-ground cases preserve NaN, signed-zero,
infinity, and subnormal semantics. A 64-case wire corpus agrees with pinned
Z3. The streaming ordering workload uses 11 allocations versus the complete
parser’s 163 (93.3% fewer) and is over 2.58x faster; the typed workload retains
10 versus Z3’s 20 allocations and over 150x throughput.
Version 0.111 exposes all seven floating-point classification predicates through both complete and streaming SMT-LIB execution, backed by a new solver-neutral arbitrary-term predicate constructor in Go+ std. Ground, assigned-symbol, negated, and nested-ground expressions are covered, and a separate 64-case wire corpus agrees with pinned Z3. The streaming classification workload uses 9 allocations versus the general parser’s 115 (92.2% fewer) and is more than 2.14x faster. The typed NaN workload retains exactly 50% fewer allocations than Z3 and a greater than 369x advantage.
Version 0.110 replaces throwaway S-expression construction for the supported QF_FP fragment with fixed-inline streaming command and symbol storage, while retaining transparent fallback to the complete parser. The official parse/sort/lower/solve workload drops from 140 to 9 allocations (93.6% fewer) and from 8.602–8.719 us to 3.275–3.353 us (over 2.56x faster). Comments, reversed equalities, long rounding-mode names, structured errors, arbitrary-format fallback, and streaming/general semantic equivalence remain covered.
Version 0.109 establishes the first SMT-LIB QF_FP execution path: indexed
floating-point sorts, exact IEEE bit-vector reinterpretation, short and long
rounding-mode literals, and ground or assigned-symbol fp.roundToIntegral.
A separate 64-case SMT-LIB corpus agrees with pinned Z3 across all five modes.
Ill-sorted formats, conversions, modes, and operands produce structured
execution errors. The underlying typed operation retains its independent
9-versus-19 allocation gate and more than 175x throughput advantage.
Version 0.108 adds exhaustive Go+ values for all five SMT-LIB rounding modes
and exact arbitrary-format fp.roundToIntegral. Ground and assigned-symbol
symbolic paths cover ties, directed rounding, signed zero, infinities, NaNs,
and derived rounded models. A separate 64-case corpus across RNE, RNA, RTP,
RTN, and RTZ agrees with pinned Z3. The official workload uses 9 allocations
versus Z3’s 19 (52.6% fewer) and is more than 175 times faster. Broader
unconstrained symbolic rounding, rounded arithmetic, conversions, SMT-LIB FP
execution, and general QF_FP/QF_FPBV solving remain explicitly planned.
Version 0.106 adds exact arbitrary-format ground and symbolic fp.min and
fp.max. A sole NaN selects the numeric operand; the implementation makes
deterministic SMT-LIB-permitted choices for two NaN payloads and signed zeros.
Solver-neutral std provides compact assigned-symbol validation, nested
bit-vector conditional fallback, and derived model evaluation. A separate
64-case symbolic corpus agrees with pinned Z3. The official fp.min workload
uses 10 allocations versus Z3’s 22 (54.5% fewer) and is more than 156 times
faster. Rounding modes, rounded arithmetic, conversions, SMT-LIB FP execution,
and general QF_FP/QF_FPBV solving remain explicitly planned.
Version 0.105 adds exact ground and symbolic fp.lt, fp.leq, fp.gt, and
fp.geq. Ordered comparison handles signed zeros, infinities, subnormals, and
unordered NaNs at arbitrary valid formats while Go+ preserves context and
format indices. Solver-neutral std uses a compact assigned-symbol relation
with a complete bit-blasted fallback. A separate 64-case symbolic corpus
agrees with pinned Z3. The official cold workload uses 10 allocations versus
Z3’s 20 and is more than 159 times faster. Rounding modes, rounded arithmetic,
conversions, SMT-LIB FP execution, and general QF_FP/QF_FPBV solving remain
explicitly planned.
Version 0.104 adds exact ground and symbolic fp.abs and fp.neg.
Arbitrary-format values preserve every non-sign bit, including NaN payloads;
Go+ retains context, exponent width, significand width, and the computed IEEE
bit-vector width through both operations. A separate 64-case symbolic corpus
agrees with pinned Z3. The official unary workload uses 7 allocations versus
Z3’s 18 (61.1% fewer) and is more than 201 times faster. Rounding modes,
rounded arithmetic, conversions, SMT-LIB FP execution, and general
QF_FP/QF_FPBV solving remain explicitly planned.
Version 0.103 extends the floating-point foundation to symbolic QF_FPBV
classification. Go+ retains context, exponent width, significand width, and
the computed e+s IEEE bit-vector width. Symbolic constants support all seven
classification predicates, exact fp.eq, and exact model-bit extraction.
Separate 64-case classification and 64-case equality corpora agree with pinned
Z3. Solver-neutral compact std relations also correct interior bit-vector
extract source-width retention and synthesize canonical classification models.
The symbolic NaN workload uses 5 allocations versus Z3’s 10 and is more than
324 times faster. Rounding modes, FP arithmetic, conversions, SMT-LIB FP
execution, and general QF_FP/QF_FPBV solving remain explicitly planned.
Version 0.102 adds a ground floating-point foundation. Exact arbitrary-format
IEEE/SMT-LIB bit patterns retain exponent width, significand width, and solver
context as Go+ indices; mixed formats and contexts are rejected during
generation. Classification covers NaN, infinity, zero, subnormal, normal,
positive, and negative values, while fp.eq handles signed zeros and NaNs
exactly. Seventy-four deterministic binary32 patterns, four equality cases,
and a binary128 round trip are covered. The official-API cold workload uses 4
allocations versus Z3’s 17 (76.5% fewer) and is more than 223 times faster.
Symbolic FP arithmetic and QF_FP/QF_FPBV solving remain explicitly planned.
Version 0.101 extends rational-scaled coercions to two-symbol affine integer
terms such as to_real(x)+to_real(y)+r. The std compact relation retains both
coefficients, the exact offset, Euclidean divisor, and negated remainder
semantics without materializing a general solver problem. A separate 64-case
corpus agrees with pinned Z3; the cold workload uses 18 allocations versus
Z3’s 38 (52.6% fewer) and is more than 111 times faster.
Version 0.100 extends exact rational scaling across supported affine
coerced-integer expressions with rational offsets. to_int and is_int
lower to Euclidean div and mod over one coefficient-plus-offset integer
numerator, including signed offsets and negative coefficients. A separate
64-case corpus agrees with pinned Z3; the cold affine workload uses 9
allocations versus Z3’s 28 (67.9% fewer) and is more than 154 times faster.
Version 0.99 exactly lowers rational scaling of coerced integers:
to_int((p/q)*to_real(x)) becomes Euclidean div(p*x,q), while is_int
becomes mod(p*x,q)=0, including negative coefficients and floor behavior.
Scaled-dividend and negated-remainder relations stay compact. A separate
64-case corpus agrees with pinned Z3; the non-integral cold workload uses 12
allocations versus Z3’s 25 (52% fewer) and is more than 154 times faster.
Version 0.98 lowers equality and ordering between supported affine integer-real expressions into exact LIA residual bounds. Fractional equality is false; strict and non-strict order use exact integer rounding. A separate 64-case corpus agrees with pinned Z3. The cold affine-equality workload uses 5 allocations versus Z3’s 12 and remains more than 360 times faster.
Version 0.97 normalizes affine coerced-integer expressions with exact rational
offsets, addition/subtraction, and integral scaling. to_int(n+r) becomes
n+floor(r), while is_int(n+r) depends exactly on the offset. It also adds
context-indexed AndPair for allocation-free two-term short-circuiting. A
64-case corpus agrees with pinned Z3; the cold affine workload uses 4
allocations versus Z3’s 12 and runs more than 486 times faster.
Version 0.96 adds the exact universal symbolic laws
to_int(to_real(x)) = x and is_int(to_real(x)). Go+ std and the
context-indexed façade eliminate both round trips before solving. A dedicated
64-case corpus agrees with pinned Z3. The cold contradiction workload uses 4
allocations versus Z3’s 12 and runs more than 430 times faster.
Version 0.95 adds exact direct symbolic to_real equality and order against
another coerced integer or an exact rational constant. Fractional bounds lower
with correct floor/ceiling semantics, while broader mixed expressions remain
explicitly unknown. A separate 64-case corpus agrees with pinned Z3. The
three-equality cold workload uses 8 allocations versus Z3’s 21 and runs more
than 225 times faster.
Version 0.94 adds exact arbitrary-precision ground Int/Real coercions:
context-indexed Go+ ToReal, floor-correct ToIntReal, and exact
IsIntReal, together with SMT-LIB to_real, to_int, and is_int.
Symbolic coercions remain explicitly unknown. A 64-case corpus agrees with
pinned Z3; construction uses 1 allocation versus Z3’s 4 and runs more than
2 times faster.
Version 0.93 adds ternary Real × Real × Real -> Real functions with
context-indexed Go+ arity, affine purification, exact rational-bound
aggregation, SMT-LIB execution, and fixed-point LRA/EUF congruence. The cold
workload uses 16 allocations versus Z3’s 34 and runs about 54 times faster.
Version 0.92 adds unary Real -> Bool and binary Real × Real -> Bool
predicates with context-indexed Go+ signatures, affine-argument purification,
SMT-LIB execution, and fixed-point LRA/EUF equality exchange. Their cold
workloads use 11 allocations versus Z3’s 22 and 25 while running more than
170 times faster.
Version 0.91 adds exact integer-valued conditional terms around unary EUF
applications in the context-indexed Go+ API and SMT-LIB ite. The compact
QF_UFLIA workload uses 13 allocations versus Z3’s 34 and runs more than 160
times faster on the recorded Apple M5 Max cold benchmark.
Typed by construction
The solver-neutral foundation lives in goforge.dev/goplus/std/smt and
goforge.dev/goplus/std/smtlib. Go+ indices preserve context identities,
bit-vector widths, uninterpreted-function signatures, datatype declaration
identities/cardinalities, and array index/element sorts. Incorrect widths and
sorts are rejected while generating ordinary Go.
Version 0.40 includes Boolean SAT, integer difference logic, general exact
linear integer arithmetic, exact linear real arithmetic, typed unary and binary
EUF, finite, arbitrary-arity same-sort recursive, scalar-product, and mixed-sort
recursive QF_DT, arbitrary-width bit vectors,
BV/Int conversions, integer arrays, and
width-indexed bit-vector arrays with finite extensional models and normalized
store chains. Shared equality exchange covers Real/EUF, IDL/integer arrays,
and BV/bit-vector arrays. Unsupported theories return unknown rather than
being approximated.
Evidence
Deterministic SMT-LIB corpora are checked against pinned Z3 4.16.0. Every official-API benchmark treats throughput and visible Go allocation count as independent gates. The release covers 768 deterministic array and mixed-theory oracle cases and 12 array performance gates. The exact and symbolic QF_AUFBV paths, for example, use 4 and 5 allocations compared with Z3’s 16 and 23, while remaining more than 1,000 times faster on the recorded Apple M5 Max cold workloads.
Small Boolean CNF and typed ground-EUF systems use compact solver-neutral representations from Go+ std. Disjoint choice-group CNF—covering one-hot allocation, graph coloring, and finite scheduling—uses a fixed-bitset solver. The hard 7-into-6 workload takes 326.05–326.89 µs and 23 allocations versus Z3’s 2.962–3.068 ms and 1,078. Every recorded pre-string official-API workload clears both the 2x throughput and 50% allocation-reduction gates independently. The string workload now clears them too: it is about 360 times faster and uses 9 allocations versus Z3’s 31 visible Go allocations.
Finite enumeration datatypes add nullary constructors, recognizers,
equality/disequality, exhaustion detection, exact model values, and SMT-LIB
declare-datatype execution. A 64-system deterministic corpus agrees with
pinned Z3. The cold model workload uses 11 allocations versus Z3’s 31 and
remains more than 550 times faster.
Recursive datatypes add context-, declaration-, and arity-indexed constructor
witnesses. Constructor arguments use vec.Vec and selectors require
vec.Fin[arity], making wrong arity and out-of-bounds fields generation-time
errors. The solver provides constructor disjointness, per-field injectivity,
graph acyclicity across every edge, exact n-ary models, and recursive SMT-LIB
declarations. Separate 64-system unary-depth, binary-branching, and
ternary-branching corpora agree with pinned Z3. The n-ary cold constructor,
selector, recognizer, and model workload uses 20 allocations versus Z3’s 40
and runs about 300 times faster. Version 0.13 added type-level mixed field
signatures, context-indexed argument HLists, sort-refining selector cursors,
Bool/Int/Real/bit-vector/Self fields, exact recognizer-only models, and general
SMT-LIB product constructors. Its mixed cold model workload uses 19
allocations versus Z3’s 41 and runs about 226 times faster at the median.
Version 0.14 adds mutually recursive datatype declaration groups, typed
cross-datatype references, productivity validation, and cross-declaration
acyclicity through SMT-LIB declare-datatypes. Its Tree/Forest cold workload
uses 22 allocations versus Z3’s 58 and runs about 146 times faster at the
median.
Version 0.15 adds unary parametric par families with distinct lazy concrete
instantiations, qualified constructors, indexed recognizers, nested
instantiation, exact scalar selector values, and exhaustive scalar match.
Its PList Int cold model workload uses 19 allocations versus Z3’s 41 and
runs about 172 times faster at the median.
Version 0.16 adds typed and SMT-LIB update-field: owning constructors are
rebuilt, other constructors are preserved, symbolic recognizer-only values
remain exact, and wrong replacement sorts are rejected during Go+ generation.
The cold update workload uses 14 allocations versus Z3’s 35 and runs about
330 times faster at the median.
Version 0.17 couples datatype constructor coloring with scalar branch solving,
so an exhaustive scalar match can select the constructor of an otherwise
unconstrained value. It retains constructor schemas for exact selected-field
and datatype model extraction, and the expanded 64-case corpus agrees with
pinned Z3.
Version 0.18 extends exhaustive matches to bit-vector and datatype-valued
results. Datatype branch equalities enumerate constructor choices soundly and
retain exact selected models. Its cold datatype-valued match workload uses 18
allocations versus Z3’s 46 and runs about 300 times faster at the median.
Version 0.19 adds arity-checked multi-parameter families, identity-distinct
instantiations, regular recursion, nested substituted fields, and exact mixed
models. Its cold Pair Int Bool workload uses 14 allocations versus Z3’s 37
and runs about 300 times faster at the median. Mutually parametric groups
arrive in Version 0.20: families are monomorphized jointly across cross-family
cycles, differing arities are supported, and productivity is validated before
installation. The cold Tree Int/Forest Int workload uses 21 allocations
versus Z3’s 57 and runs about 200 times faster at the median.
Version 0.21 adds bounded complete Boolean QF_DT branching for disjunction,
implication, equivalence, Boolean equality and ITE, nested negation, and
distinct. Its fully model-validating cold workload uses 19 allocations
versus Z3’s 47 and runs about 200 times faster at the median.
Version 0.22 adds context-indexed GoSMT strings and SMT-LIB String,
str.++, str.len, str.contains, str.prefixof, and str.suffixof, with
Unicode code-point length and exact model values. Go+ std also gains
element-sort-indexed generic sequence empty/unit/concat/length constructors.
A 64-system QF_SLIA corpus agrees with pinned Z3. The native std workload takes
6 allocations and 0.684–0.708 µs; the public API workload takes 28 allocations
and 3.615–3.670 µs versus Z3’s 31 visible Go allocations and 1.029–1.093 ms.
Throughput is green and façade allocation reduction remains the next gate.
Version 0.23 replaces that red façade path with compact inline string terms
and relation systems. The same fully model-validating workload falls from 28
to 9 allocations and 2.894–2.927 µs, versus Z3’s 31 visible Go allocations and
1.044–1.097 ms: 71.0% fewer allocations and about 360 times faster. Constant
concatenation canonicalization also reduces the std core to 3 allocations and
0.645–0.671 µs.
Version 0.24 adds typed and SMT-LIB str.at, str.substr, str.indexof, and
first-occurrence str.replace, plus Z3-compatible \u{…} and \uXXXX
Unicode escapes. The expanded 64-system QF_SLIA corpus agrees with pinned Z3.
Constant folding cuts the fully model-validating indexed workload from 35 to
11 allocations and 3.575–3.605 µs, versus Z3’s 39 visible Go allocations and
0.983–1.049 ms: 71.8% fewer allocations and about 285 times faster.
Version 0.25 adds first/all replacement, arbitrary-precision string/integer
round trips, code-point conversion over SMT-LIB’s full 0..0x2ffff character
domain, surrogate-preserving WTF-8 escapes, and ASCII digit recognition. The
expanded 64-system corpus agrees with pinned Z3 across invalid, negative,
empty, surrogate, and arbitrary-precision cases. Its conversion workload uses
8 allocations and 1.224–1.233 µs versus Z3’s 18 visible Go allocations and
0.978–1.061 ms: 55.6% fewer allocations and about 800 times faster.
Version 0.26 adds an element-sort-indexed regular-language AST to Go+ std,
context-indexed GoSMT regex construction, and SMT-LIB regex membership,
literal/range/empty/full/all-character languages, concat/union/intersection/
difference/complement, star/plus/optional, and indexed exact or bounded
repetition. A separate 64-system QF_S corpus agrees with pinned Z3. Compact
literal-regex construction uses 5 allocations and 1.021–1.026 µs versus Z3’s
10 visible Go allocations and 0.941–1.029 ms: exactly 50.0% fewer allocations
and about 950 times faster.
Version 0.27 adds constructive symbolic regular-language models and exact
contradiction proofs for equality-forced strings. An inline postfix regex
program keeps literal/range/concat/loop languages value-resident through
construction and synthesis. A separate 64-system symbolic QF_S corpus agrees
with pinned Z3. The fully model-validating symbolic workload uses 9
allocations and 1.897–1.938 µs versus Z3’s 20 visible Go allocations and
2.807–2.903 ms: 55.0% fewer allocations and about 1,480 times faster.
Version 0.28 solves conjunctive positive and negative regular-language
constraints over the same symbolic string, synthesizes shared witnesses, and
proves incompatible singleton intersections unsatisfiable. Direct fixed-bitset
evaluation avoids expanding inline regex programs into heap ASTs. A separate
64-system interacting QF_S corpus agrees with pinned Z3. Its fully
model-validating workload uses 13 allocations and 4.658–4.701 µs versus Z3’s
27 visible Go allocations and 1.239–1.353 ms: 51.9% fewer allocations and
about 275 times faster.
Version 0.29 adds bounded non-conjunctive Boolean regex models and constructive
single-unknown literal-prefix/suffix word equations. Separate 64-case corpora
for both features agree with pinned Z3. Inline postfix Boolean formulas use
6 allocations and 3.902–3.910 µs versus Z3’s 30 allocations and
1.018–1.072 ms; word equations use 6 allocations and 1.575–1.586 µs versus
Z3’s 17 allocations and 0.979–1.059 ms.
Version 0.30 adds constructive word equations over as many as four distinct
symbols separated by unique nonempty literal delimiters, including interaction
with additional equalities. A separate 64-case four-symbol corpus agrees with
pinned Z3. The fully model-validating cold workload uses 6 allocations and
1.728–1.755 µs versus Z3’s 23 allocations and 1.951–2.042 ms.
Version 0.31 adds deterministic standalone models for adjacent-symbol and
multiply delimited bounded equations while keeping conjunction propagation
restricted to uniquely forced splits. A separate 64-case corpus agrees with
pinned Z3. The canonical adjacent-symbol workload uses 6 allocations and
1.698–1.714 µs versus Z3’s 20 allocations and 1.195–1.264 ms.
Version 0.32 replaces greedy canonical splitting with exhaustive bounded
Unicode-boundary search and adds repeated-symbol equations such as
x ++ "-" ++ x = "go-go". A separate 64-case corpus agrees with pinned Z3,
and a 4,096-state limit returns unknown instead of approximating. The cold
workload uses 6 allocations and 1.711–1.740 µs versus Z3’s 16 allocations and
2.711–2.820 ms.
Version 0.33 combines ambiguous bounded equations exactly with ground symbol
assignments, including alternative-split models and contradiction proofs. A
separate 64-case corpus agrees with pinned Z3. The interacting cold workload
uses 8 allocations and 3.354–3.359 µs versus Z3’s 27 allocations and
0.987–1.084 ms.
Version 0.34 combines bounded word equations with exact str.len equalities,
using Unicode code-point lengths to prune model search and prove impossible
lengths contradictory. A separate 64-case corpus agrees with pinned Z3. The
fully model-validating cold workload uses 10 allocations and 3.351–3.366 µs
versus Z3’s 26 allocations and 1.518–1.584 ms: 61.5% fewer allocations and
more than 450 times faster.
Version 0.35 adds lower and upper str.len bounds in either operand order,
merges them independently of assertion order, and prunes bounded word-equation
search by Unicode code-point count. Compact public order relations reduce the
first implementation from 18 allocations to 13. Pinned Z3 uses 29 allocations
and 1.673–1.752 ms versus GoSMT’s 4.395–4.413 µs: 55.2% fewer allocations and
more than 379 times faster.
Version 0.36 solves as many as four bounded ground-target word equations with
one shared model and 4,096-state limit. Global backtracking revisits an earlier
equation’s locally valid split when a later equation rejects it. A separate
64-case corpus agrees with pinned Z3. The shared-equation workload uses
8 allocations and 3.716–3.732 µs versus Z3’s 32 allocations and
1.710–1.763 ms: 75.0% fewer allocations and more than 458 times faster.
Version 0.37 couples positive and negative regular-language memberships to the
same bounded word-equation search, pruning invalid splits before accepting a
global model. Compact Boolean-regex predicates participate in final model
validation. A separate 64-case corpus agrees with pinned Z3. The cold workload
uses 9 allocations and 4.177–4.193 µs versus Z3’s 29 allocations and
1.270–1.360 ms: 69.0% fewer allocations and more than 302 times faster.
Version 0.38 evaluates general bounded Boolean-regex predicates inside global
word-equation search, so false or, nested not, implication, equivalence,
equality, and ITE candidates resume split backtracking. A separate 64-case
corpus agrees with pinned Z3. The non-singleton range workload uses
13 allocations and 5.504–5.516 µs versus Z3’s 32 allocations and
1.423–1.496 ms: 59.4% fewer allocations and more than 257 times faster.
Version 0.39 adds string equality/disequality predicates and Boolean choices
over them to the same global word-equation validation. For
x ++ y = "ab" with x != "", it rejects the canonical empty split and
continues to x = "a", y = "b". A separate 64-case corpus agrees with
pinned Z3. The workload uses 9 allocations and 4.513–4.560 µs versus Z3’s
25 allocations and 1.289–1.354 ms: 64.0% fewer allocations and more than
282 times faster.
Version 0.40 adds contains, prefix, suffix, and digit predicates to global
word-equation backtracking. The cold workload requires both
contains(x,"b") and prefixof("a",x) under x ++ y = "abc", selecting
x = "ab" and y = "c". A separate 64-case corpus agrees with pinned Z3.
It uses 13 allocations and 6.425–6.457 µs versus Z3’s 26 allocations and
1.852–1.916 ms: exactly 50.0% fewer allocations and more than 286 times
faster.
Version 0.41 doubles the exact bounded word-equation system capacity to eight
ground-target equations and sixteen inline conjuncts while retaining one
shared 4,096-state search limit. A separate 64-case eight-equation corpus
agrees with pinned Z3. The cold workload uses 15 allocations and
12.196–12.216 µs versus Z3’s 62 allocations and 2.992–3.069 ms: 75.8% fewer
allocations and more than 244 times faster.
Version 0.42 removes the fixed equation and conjunct count ceilings: eight
equations and sixteen conjuncts remain inline, then exact overflow storage
continues under the same global 4,096-state limit. A separate 64-case
twelve-equation corpus agrees with pinned Z3. The cold workload uses
20 allocations and 15.280–15.290 µs versus Z3’s 84 allocations and
3.035–3.130 ms: 76.2% fewer allocations and more than 198 times faster.
Version 0.43 removes the four-entry ceilings for length, regex, and general
string-predicate constraints while retaining inline storage for common
systems. The GoSMT façade now lowers one-symbol prefix/suffix concatenation
equalities directly into shared word equations, and std length evaluation
counts SMT code points without allocating rune slices. A separate 64-case
mixed overflow corpus agrees with pinned Z3. The cold five-length/five-regex
workload uses 28 allocations and 13.801–13.824 µs versus Z3’s 60 allocations
and 1.403–1.527 ms: 53.3% fewer allocations and more than 101 times faster.
Version 0.44 adds compact relational string-length equality, strict order, and
non-strict order between bound string expressions, including Boolean nesting
during word-equation backtracking and Unicode code-point semantics. A separate
64-case corpus agrees with pinned Z3. The cold equality workload uses
9 allocations and 5.142–5.167 µs versus Z3’s 24 allocations and
2.325–2.436 ms: 62.5% fewer allocations and more than 449 times faster.
Version 0.45 adds exact affine string-length expressions over n-ary addition,
subtraction, and arbitrary-precision constant scaling, including Boolean
combinations during word-equation backtracking. A separate 64-case corpus
agrees with pinned Z3. The cold subtraction workload uses 14 allocations and
4.720–4.738 µs versus Z3’s 28 allocations and 2.452–2.498 ms: exactly
50.0% fewer allocations and more than 517 times faster.
Version 0.46 couples str.indexof, exact arbitrary-precision str.to_int,
and str.to_code integer predicates to globally backtracked word equations,
including affine combinations. A separate 64-case corpus agrees with pinned
Z3. Allocation-free Unicode/WTF-8 index scanning reduces the cold index
workload from 21 allocations to 12; it uses 12 allocations and
5.075–5.080 µs versus Z3’s 27 allocations and 2.725–2.811 ms: 55.6% fewer
allocations and more than 536 times faster.
Version 0.47 couples derived-string equalities over str.at, str.substr,
str.replace, str.replace_all, str.from_int, and str.from_code to the
same global word-equation search. Allocation-free Unicode/WTF-8 boundary
scanning preserves malformed-input semantics. A separate 64-case supported
corpus agrees with pinned Z3; str.replace_all, for which Z3 returns
unknown in QF_SLIA, has direct semantic coverage. The cold substring
workload uses 12 allocations and 5.879–5.897 µs versus Z3’s 29 allocations
and 1.813–1.866 ms: 58.6% fewer allocations and more than 307 times faster.
Version 0.48 adds exact ground Seq Int construction, equality/disequality,
length arithmetic, Boolean composition, and model evaluation. Go+ retains the
element sort in std and the context identity in GoSMT; the first eight values
stay inline before exact overflow. A separate 64-case corpus agrees with
pinned Z3. The cold sequence workload uses 12 allocations and
3.176–3.193 µs versus Z3’s 30 allocations and 0.955–1.039 ms: 60.0% fewer
allocations and more than 299 times faster.
Version 0.49 completes the common ground integer-sequence operator layer with
indexed at/extract, contains, prefix, suffix, index-of, and first
replacement, including empty and out-of-range behavior. A separate 64-case
operator corpus agrees with pinned Z3. The combined cold operator workload
uses 23 allocations and 5.969–5.978 µs versus Z3’s 53 allocations and
0.927–1.061 ms: 56.6% fewer allocations and more than 155 times faster.
Version 0.50 adds generic sequence constants and exact ground-assigned
Seq Int models across derived operators and temporary assumptions.
Conflicting assignments are unsatisfiable and underconstrained sequences
remain explicit unknown. A separate 64-case corpus agrees with pinned Z3.
The cold symbolic workload uses 22 allocations and 6.247–6.337 µs versus
Z3’s 48 allocations and 1.049–1.109 ms: 54.2% fewer allocations and more than
165 times faster.
Version 0.51 constructs deterministic exact Seq Int witnesses for positive
conjunctive contains, prefix, and suffix constraints. It merges compatible
boundaries, proves incompatible prefixes or suffixes unsatisfiable, supports
multiple symbols, and preserves unknown outside the supported fragment. A
separate 64-case corpus agrees with pinned Z3. The cold witness workload uses
16 allocations and 5.099–5.112 µs versus Z3’s 34 allocations and
5.635–5.769 ms: 52.9% fewer allocations and more than 1,102 times faster.
Version 0.52 couples symbolic Seq Int witnesses to exact ground lengths.
Bounded placement/backtracking handles overlapping prefix and suffix
requirements, containment offsets, deterministic zero filling, and exact
negative, conflicting, or too-short proofs. A separate 64-case corpus agrees
with pinned Z3. The cold exact-length workload uses 18 allocations and
5.722–5.792 µs versus Z3’s 37 allocations and 3.601–3.744 ms: 51.4% fewer
allocations and more than 621 times faster.
Version 0.53 adds strict and non-strict ground lower/upper length bounds.
Admissible lengths share the bounded placement budget, and contradictory
bounds are proved independently of assertion order. A separate 64-case corpus
agrees with pinned Z3. The cold relational-length workload uses 20 allocations
and 6.882–6.897 µs versus Z3’s 41 allocations and 4.140–4.292 ms: 51.2% fewer
allocations and more than 600 times faster.
Version 0.54 adds single-symbol affine sequence lengths with exact addition,
subtraction, arbitrary-precision constant scaling, divisibility proofs,
coefficient-sign reversal, integer floor/ceiling bounds, and cancellation. A
separate 64-case corpus agrees with pinned Z3. The cold affine workload uses
25 allocations and 7.394–7.411 µs versus Z3’s 50 allocations and
4.123–4.288 ms: exactly 50% fewer allocations and more than 556 times faster.
Version 0.55 adds compact positive sequence-symbol equality classes.
Assignments, constructive and length constraints, assumptions, derived
evaluation, and exact models propagate across aliases, while conflicting alias
assignments are unsatisfiable. A separate 64-case corpus agrees with pinned Z3.
The cold equality-class model workload uses 29 allocations and
8.840–8.850 µs versus Z3’s 60 allocations and 4.217–4.391 ms: 51.7% fewer
allocations and more than 476 times faster.
Version 0.56 adds exact affine equations across two distinct symbolic sequence
lengths. The solver canonicalizes aliases, jointly searches one bounded
length, derives its partner by exact division, satisfies each symbol’s
constructive requirements, and commits both models atomically. A separate
64-case corpus agrees with pinned Z3. The cold paired-model workload uses 19
allocations and 5.282–5.295 µs versus Z3’s 46 allocations and 1.400–1.446 ms:
58.7% fewer allocations and more than 264 times faster.
Version 0.57 extends exact affine sequence-length equations to three canonical
symbols. Constructive boundaries prune bounded recursive search, the final
length is derived by exact division, coefficient-GCD conflicts are proved
without search, aliases canonicalize before solving, and all three witnesses
commit atomically. A separate 64-case corpus agrees with pinned Z3. The cold
three-model workload uses 24 allocations and 6.566–6.589 µs versus Z3’s 56
allocations and 1.450–1.503 ms: 57.1% fewer allocations and more than 220
times faster.
Version 0.58 adds one strict or non-strict affine inequality across two or
three canonical sequence lengths. Sign-correct integer division handles
positive and negative coefficients, constructive minima prune infeasible
partial assignments, equality relations solve first regardless of assertion
order, and exact witnesses satisfy local sequence requirements. Multiple
simultaneous multi-symbol inequalities return unknown rather than risking an
unsound answer. A separate 64-case corpus agrees with pinned Z3. The cold
bounded-model workload uses 24 allocations and 6.818–6.903 µs versus Z3’s 56
allocations and 1.432–1.490 ms: 57.1% fewer allocations and more than 207
times faster.
Version 0.59 jointly solves multiple affine equalities and inequalities over
as many as three canonical sequence roots. One bounded global search prunes
partial assignments against every attainable relation interval, intersects
final exact values with sign-correct inequality bounds, satisfies local
constructive requirements, and commits all models atomically. A separate
64-case interacting corpus agrees with pinned Z3. The cold relation-system
workload uses 32 allocations and 8.737–8.753 µs versus Z3’s 72 allocations and
1.680–1.735 ms: 55.6% fewer allocations and more than 191 times faster.
Version 0.60 extends exact and interacting affine sequence-length systems to
four canonical roots while retaining fixed inline coefficients, bounded global
search, interval pruning, final exact/bound intersection, constructive
requirements, and atomic models. Five-root systems explicitly return
unknown. A separate 64-case corpus agrees with pinned Z3. The cold
four-model workload uses 38 allocations and 10.786–10.884 µs versus Z3’s 90
allocations and 1.836–1.896 ms: 57.8% fewer allocations and more than 168
times faster.
Version 0.61 aligns affine relation and global-search capacity with the
existing eight-entry inline sequence-value and alias design. Exact and
interacting systems now support as many as eight canonical roots; nine-root
systems retain the explicit bounded unknown contract. A separate five-root
64-case corpus agrees with pinned Z3, while the prior four-root allocation
count remains unchanged. The cold five-model workload uses 45 allocations and
13.553–13.704 µs versus Z3’s 109 allocations and 2.006–2.078 ms: 58.7% fewer
allocations and more than 146 times faster.
Version 0.62 adds bounded positive Boolean and/or solving for symbolic
integer-sequence constraints. Nested disjunctions expand under a 4,096-branch
limit, alternatives are tried left to right, exact models are validated, and
all-unsatisfiable alternatives are proved without approximating unsupported
negation. A separate 64-case corpus agrees with pinned Z3. The cold fallback
workload uses 20 allocations and 6.129–6.166 µs versus Z3’s 44 allocations and
2.547–2.598 ms: 54.5% fewer allocations and more than 413 times faster.
Version 0.63 extends bounded symbolic integer-sequence formulas through nested
negation, implication, equivalence, and Boolean if. Negated affine length
equality and order lower to exact positive relations, while unsupported
negated equality/content predicates retain the explicit unknown contract. A
separate 64-case corpus agrees with pinned Z3. The cold negated-bound workload
uses 24 allocations and 9.663–9.673 µs versus Z3’s 49 allocations and
30.461–31.105 ms: 51.0% fewer allocations and more than 3,149 times faster.
Version 0.64 adds constructive symbolic integer-sequence disequality against
finite ground values. Exclusions discriminate genuinely free elements,
backtrack fully fixed containment placements, prove exhaustive conflicts, and
share the existing 4,096-resource contract. A separate 64-case corpus agrees
with pinned Z3. The cold exact-model workload uses 19 allocations and
7.037–7.057 µs versus Z3’s 44 allocations and 2.848–2.973 ms: 56.8% fewer
allocations and more than 403 times faster.
Version 0.65 adds exact negated ground contains, prefix, and suffix constraints
for symbolic integer sequences. Free positions use an integer absent from every
forbidden pattern; fixed violations backtrack through positive containment
placements and length choices, and empty-pattern contradictions are proved
directly. A separate 64-case corpus agrees with pinned Z3. The cold
placement-backtracking workload uses 19 allocations and 10.017–10.024 µs
versus Z3’s 41 allocations and 22.600–23.112 ms: 53.7% fewer allocations and
more than 2,254 times faster.
Version 0.66 adds exact pairwise disequality between symbolic integer
sequences, including aliases, assigned/free pairs, and coupled affine-length
backtracking. Candidate construction excludes already committed neighboring
models and retries lengths when a distinct value cannot be built. A separate
64-case corpus agrees with pinned Z3. The cold coupled-length workload uses 21
allocations and 10.445–10.490 µs versus Z3’s 44 allocations and
2.603–2.701 ms: 52.3% fewer allocations and more than 248 times faster.
Version 0.67 adds exact negated contains, prefix, and suffix predicates whose
pattern is a distinct symbolic integer sequence. Acyclic dependencies construct
nonempty patterns before dependent values, participate in affine-length
backtracking, and support assigned targets through exact pattern-side
requirements; cyclic dependencies remain explicit unknown. A separate
64-case corpus agrees with pinned Z3. The cold coupled-prefix workload uses 21
allocations and 11.677–12.116 µs versus Z3’s 44 allocations and
2.633–2.727 ms: 52.3% fewer allocations and more than 217 times faster.
Version 0.68 closes cyclic dependencies between symbolic negated contains,
prefix, and suffix predicates. When dependency ordering cycles, the later root
receives both value-side and pattern-side exact constraints against earlier
models, including coupled affine-length backtracking. GoSMT also retains
generic Boolean-atom polarity without eagerly materializing a negation node. A
separate 64-case cyclic corpus agrees with pinned Z3. The cold coupled-prefix
cycle uses 21 allocations and 11.919–12.008 µs versus Z3’s 44 allocations and
21.909–22.457 ms: 52.3% fewer allocations and more than 1,824 times faster.
Version 0.69 raises exact affine integer-sequence systems from eight to sixteen
canonical roots. Normalization, aliases, requirements, candidate search, and
models share the new capacity; equality interval pruning proves impossible
totals early, while direct symbol-model lookup avoids rebuilding façade
expressions. Seventeen-root systems retain an explicit bounded unknown
contract. A separate nine-root 64-case corpus agrees with pinned Z3. The cold
nine-model workload uses 56 allocations and 36.201–36.594 µs versus Z3’s 173
allocations and 3.221–3.305 ms: 67.6% fewer allocations and more than 88 times
faster.
Version 0.70 removes the sixteen-root semantic cutoff. The first sixteen
canonical roots remain allocation-stable inline; larger affine systems use
exact overflow normalization, dynamically sized global-search vectors,
bidirectional symbolic-pattern constraints, and atomic overflow models under
the existing 4,096-resource contract. A separate seventeen-root 64-case corpus
agrees with pinned Z3. The cold seventeen-model workload uses 117 allocations
and 91.043–91.578 µs versus Z3’s 317 allocations and 5.597–5.703 ms: 63.1%
fewer allocations and more than 61 times faster.
Version 0.71 adds exact standalone positive equalities for ground-index
str.at and str.substr over direct symbolic strings. Overlapping
requirements reduce to shared code-point placements and lower/upper length
bounds, producing canonical models and exact contradictions without a
bounding word equation. Compact GoSMT indexed terms preserve the common path
through std solving. The cold substring-and-model workload uses 7 allocations
and 3.424–3.467 µs versus Z3’s 15 allocations and 1.820–1.970 ms: 53.3% fewer
allocations and more than 524 times faster.
Version 0.72 republishes the same verified solver against the immediately
available immutable std v0.103 artifact after the public module services
cached an early lookup of std v0.102. No solver semantics or benchmark results
changed.
Version 0.73 adds exact standalone inversion of first-replacement equalities
with a direct symbolic input and ground source, replacement, and target. The
finite preimage covers unchanged strings, empty source/replacement,
replacement-aligned reconstruction, Unicode boundaries, ambiguity, and
intersection across multiple constraints under the 4,096-resource contract.
The cold replacement-and-model workload uses 7 allocations and
3.389–3.432 µs versus Z3’s 14 allocations and 1.204–1.305 ms: exactly 50%
fewer allocations and more than 350 times faster.
Version 0.74 composes finite first-replacement preimages with ground-index
str.at and str.substr equalities over the same direct symbol. Every
replacement candidate is filtered, so a compatible model is selected or
unsatisfiability is proved only after exhaustive rejection. The cold mixed
workload uses 8 allocations and 4.632–4.633 µs versus Z3’s 21 allocations and
1.388–1.471 ms: 61.9% fewer allocations and more than 299 times faster.
Version 0.75 extends exhaustive first-replacement candidates through the
bounded same-symbol string predicate language: equality/disequality,
contains/prefix/suffix/digit/regex, length/index/conversion arithmetic, and
supported Boolean forms. Foreign unbound symbols remain explicit unknown.
The cold replacement-plus-contains workload uses 8 allocations and
4.980–5.008 µs versus Z3’s 18 allocations and 1.329–1.410 ms: 55.6% fewer
allocations and more than 265 times faster.
Version 0.84.1 adds SMT-LIB 2.7 str.replace_re and str.replace_re_all to
Go+ std and exposes context-indexed GoSMT constructors. Single replacement
uses the shortest leftmost match, including an empty match; replace-all scans
left to right over shortest non-empty matches. Pinned Z3 4.16.0 reports
unknown for the same ground formulas, while GoSMT decides them exactly. The
cold assertion-and-model workload uses 8 allocations and 4.023–4.064 µs
versus Z3’s 17 visible Go allocations and 1.327–1.438 ms: 52.9% fewer
allocations and more than 326 times faster.
Version 0.85.0 adds core code-point lexicographic str.< and reflexive
str.<= to Go+ std, context-indexed GoSMT, and chainable SMT-LIB execution.
Compact symbolic solving constructs ordered models, intersects literal
lower/upper bounds, and proves reflexive, boundary, and mixed strict/non-strict
cycle contradictions. The fully model-validating cold workload uses 9
allocations and 5.101–5.160 µs versus Z3’s 20 visible Go allocations and
25.89–26.51 ms: 55.0% fewer allocations and more than 5,017 times faster.
Version 0.86.0 adds checked singleton-character construction to Go+ std and
context-indexed GoSMT, plus strict SMT-LIB execution for (_ char #xH) across
the complete 0..0x2ffff domain. The 64-case corpus covers encoding boundaries,
surrogate-preserving WTF-8, supplementary characters, leading zeros, and mixed
hex case against pinned Z3. Construction uses 1 allocation and about 25 ns
versus Z3’s 2 visible Go allocations and about 503 ns: exactly 50% fewer
allocations and more than 20 times faster.
Version 0.87.0 adds Go+-indexed unary Int -> Int and binary
Int × Int -> Int uninterpreted functions to std and the context-indexed
GoSMT façade, with SMT-LIB QF_UFLIA, exact integer arguments, ground
congruence, and direct integer-symbol equality exchange. A 64-case corpus
agrees with pinned Z3, and cross-context applications fail during Go+
generation. The binary cold workload uses 10 allocations and
4.42–4.48 µs versus Z3’s 22 visible Go allocations and 0.95–1.05 ms: 54.5%
fewer allocations and more than 212 times faster.
Version 0.88.0 adds shared QF_UFLIA purification and fixed-point equality
exchange between EUF and linear integer arithmetic. Reciprocal inequalities
can now establish application congruence; unary and binary applications can
participate in affine constraints, including affine arguments; and
application equality propagates back into LIA. The 64-case randomized corpus
agrees with pinned Z3. The shared equality workload uses 9 allocations and
3.692–3.702 µs versus Z3’s 23 allocations and 0.997–1.132 ms. The purified
binary arithmetic workload uses 7 allocations and 3.539–3.759 µs versus Z3’s
23 allocations and 0.880–1.034 ms. Both clear the independent allocation gate
and are more than 234 times faster at conservative endpoints.
Version 0.89.0 extends the indexed QF_UFLIA surface with ternary
Int × Int × Int -> Int functions across Go+ std, the context-indexed GoSMT
façade, and SMT-LIB execution. All three argument sorts and solver context are
checked before Go generation. Ground congruence, affine arguments, application
purification, and fixed-point EUF/LIA exchange are covered by the mixed-arity
64-case pinned-Z3 corpus. Retaining all three argument identities in the
compact path reduced the cold workload from 32 allocations to 7 versus Z3’s
26; it runs in 4.138–4.190 µs versus 0.898–1.062 ms, over 214 times faster at
conservative endpoints.
Version 0.90.0 adds mixed-signature unary Int -> Bool and binary
Int × Int -> Bool predicates across Go+ std, GoSMT, and SMT-LIB. Predicate
argument sorts, result sort, and solver context are checked before Go
generation. Affine arguments are purified and LIA-implied equality drives EUF
predicate congruence. A 64-case unary/binary predicate corpus agrees with
pinned Z3. The unary cold workload uses 9 allocations and 4.100–4.147 µs
versus Z3’s 23 allocations and 1.014–1.182 ms. Binary uses 9 allocations and
3.955–4.005 µs versus 25 allocations and 0.889–1.071 ms. Both clear their
independent allocation gates and are over 221 times faster conservatively.
The QF_LIA foundation adds arbitrary-precision affine coefficients, exact
branch-and-bound integrality, bounded Boolean structure over arithmetic atoms,
finite resource limits, exact model extraction, and ordinary SMT-LIB integer
multiplication, comparisons, distinct, and nonzero constant-divisor
Euclidean div/mod. Its deterministic 288-system conjunctive, Boolean, and
signed-dividend/signed-divisor corpus agrees with pinned Z3 and validates every
satisfiable model.
The cold exact-equation model workload uses 6 allocations versus Z3’s 15 and
runs more than 1,500 times faster on the recorded Apple M5 Max runs. The
general two-row model workload fell from 104 allocations to 13 versus Z3’s 28,
while remaining more than 250 times faster.
The Boolean disjunction+disequality model workload uses 7 allocations versus
Z3’s 20 and remains more than 175 times faster.
The signed Euclidean div/mod model workload uses 8 allocations versus Z3’s 23
and remains more than 750 times faster.
The source repository contains the complete compatibility matrix, performance ledger, pinned oracle tests, and roadmap. This is a foundation release, not a claim of complete Z3 compatibility.