This library defines the semiring abstraction used throughout SWAL and provides all concrete implementations.
Algebra.Semiring defines Algebra.Semiring.T, the module type every semiring must satisfy. It bundles the carrier type, the semiring operations (⊕ and ⊗) with their identities, and the SMT sub-module that lifts those operations into Smtml expressions. Every functor in the Encoding and Learner libraries is parameterized over a value of type (module Algebra.Semiring.T).
Algebra.Bool — Boolean semiring ({false, true}, ∨, ∧). Used by the residual NFA benchmarks. Encoded in QF_BV.Algebra.Nat — Natural-number semiring (ℕ, +, ×), optionally bounded. Nat.get (Some b) returns the bounded variant {0,…,b}. Encoded in QF_NIA.Algebra.Rat — Rational-number semiring (ℚ, +, ×). Represented as integer (numerator, denominator) pairs in SMT. Encoded in QF_NIA.Algebra.Prob — Probabilistic semiring (0,1∩ℚ, min(·+·,1), ×). Like Algebra.Rat but with domain constraint num ≤ den. Encoded in QF_NIA.Algebra.Bottleneck — Bottleneck semiring ({-∞}∪ℤ∪{+∞}, max, min). Uses integer sentinel encoding. Encoded in QF_LIA.Algebra.Tropical_lia — Tropical semiring ({∞}∪ℕ, min, +), bounded or unbounded, encoded in QF_LIA.Algebra.Tropical_bv — Bounded tropical semiring, encoded as bitvectors in QF_BV for faster solving.Algebra.Matrix — Dense matrix algebra parameterized over any semiring. Used internally by Automata.WFA and Learner.Angluin.Implement Algebra.Semiring.T (in particular its SMT sub-module) and add a get function following the pattern of Algebra.Nat or Algebra.Tropical_lia. Register the new semiring in Lang.Lang by adding a variant to Lang.t and a case in Lang.get.