Module S.SMT

Lifts the semiring into SMT expressions via Smtml.

Two distinct abstract types, sym and exp, keep decision variables (symbols introduced by mk) separate from general expressions (which may be constants or compound terms). exp_of_s injects a symbol into the expression type when an expression is required.

type sym

An SMT decision variable representing an unknown semiring element.

type exp

An SMT expression representing a (possibly symbolic) semiring value.

val logic : Smtml.Logic.t

The SMT logic that is sound and complete for this semiring. Used to instantiate the solver with the tightest possible theory, e.g. QF_BV for Boolean / bounded tropical (bitvector encoding), QF_LIA for tropical / bottleneck, QF_NIA for Nat / Rat / Prob.

val eval : Smtml.Model.t -> sym -> t

eval model sym reads the value assigned to sym in a satisfying model and converts it back to a concrete semiring element.

val exp_of_t : t -> exp

exp_of_t v embeds a concrete value as a constant SMT expression.

val exp_of_s : sym -> exp

exp_of_s sym injects a decision variable into the expression type.

val mk : Base.string -> sym * Smtml.Expr.t Base.list

mk label allocates a fresh SMT decision variable named label and returns it together with any domain-restriction constraints required to keep the variable within the semiring's carrier set. For example, Nat's mk emits sym >= 0 (and sym <= bound when bounded); Rat's mk emits den > 0; Tropical/Bottleneck emit range guards for the sentinel infinity value.

val add : exp -> exp -> exp

SMT-level semiring addition: add e1 e2 returns an expression computing e1 ⊕ e2 symbolically.

val mul : exp -> exp -> exp

SMT-level semiring multiplication: mul e1 e2 returns an expression computing e1 ⊗ e2 symbolically.

val ge : exp -> exp -> Smtml.Expr.t

ge e1 e2 produces the SMT constraint e1 ≥ e2 in the order induced by the semiring (not used in the core encoding, available for auxiliary constraints).

val eq : exp -> exp -> Smtml.Expr.t

eq e1 e2 produces the SMT constraint e1 = e2. This is the primary equality atom used in both the naive and gen encodings to pin symbolic expressions to observed membership values.