package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Soteria.Smt

Performance-focused SMT-LIB s-expression and solver interface.

Performance notes:

  • Serialization writes directly into a reused Buffer.t (no pretty-printing, no whole-tree intermediate string).
  • Solver responses are read with a hand-written buffered reader and a recursive-descent parser specialised to the small response grammar, rather than a generic s-expression lexer.
  • The handful of hot response tokens (success, sat, unsat, unknown) are interned, so the check / ack_command round-trips do not allocate a fresh atom.

S-expressions

type sexp =
  1. | Atom of string
  2. | List of sexp list
val atom : string -> sexp
val list : sexp list -> sexp
val is_atom : sexp -> bool
val to_list : sexp -> sexp list option
val write_buf : Buffer.t -> sexp -> unit

Serialize an s-expression into buf, using the minimal whitespace the solver needs (a single space between list elements).

val to_string : sexp -> string
val pp_sexp : Format.formatter -> sexp -> unit
val output_sexp : out_channel -> sexp -> unit

Exceptions

exception UnexpectedSolverResponse of sexp

Buffered reader / response parser

module Reader : sig ... end
module Subprocess = Soteria.Soteria_std.Subprocess
module StrSet : sig ... end
module StrMap : sig ... end

SMT term and command builders

val app : sexp -> sexp list -> sexp
val app_ : string -> sexp list -> sexp
val ($$) : sexp -> sexp list -> sexp
val ($$.) : string -> sexp list -> sexp
val ($) : sexp -> sexp -> sexp
val as_type : sexp -> sexp -> sexp
val nat_k : int -> sexp
val nat_zk : Z.t -> sexp
val fam : string -> sexp list -> sexp
val ifam : string -> int list -> sexp

Booleans

val t_bool : sexp
val s_true : sexp
val s_false : sexp
val bool_k : bool -> sexp
val a_ite : sexp
val a_eq : sexp
val a_distinct : sexp
val a_not : sexp
val a_and : sexp
val a_or : sexp
val ite : sexp -> sexp -> sexp -> sexp
val eq : sexp -> sexp -> sexp
val distinct : sexp list -> sexp
val bool_not : sexp -> sexp
val bool_and : sexp -> sexp -> sexp
val bool_ands : sexp list -> sexp
val bool_or : sexp -> sexp -> sexp
val bool_ors : sexp list -> sexp
val exists : sexp list -> sexp -> sexp

Integers

val t_int : sexp
val a_neg : sexp
val num_neg : sexp -> sexp
val int_k : int -> sexp
val int_zk : Z.t -> sexp
val a_lt : sexp
val a_leq : sexp
val a_add : sexp
val a_sub : sexp
val a_mul : sexp
val a_div : sexp
val a_mod : sexp
val a_rem : sexp
val num_lt : sexp -> sexp -> sexp
val num_leq : sexp -> sexp -> sexp
val num_add : sexp -> sexp -> sexp
val num_sub : sexp -> sexp -> sexp
val num_mul : sexp -> sexp -> sexp
val num_div : sexp -> sexp -> sexp
val num_mod : sexp -> sexp -> sexp
val num_rem : sexp -> sexp -> sexp

Bit-vectors

val t_bits : int -> sexp
val bv_nat_bin : int -> Z.t -> sexp
val bv_nat_hex : int -> Z.t -> sexp
val a_bvneg : sexp
val bv_neg : sexp -> sexp
val bv_bin : int -> Z.t -> sexp
val bv_hex : int -> Z.t -> sexp
val bv_k : int -> Z.t -> sexp
val a_bvult : sexp
val a_bvule : sexp
val a_bvslt : sexp
val a_bvsle : sexp
val a_concat : sexp
val a_bvnot : sexp
val a_bvand : sexp
val a_bvor : sexp
val a_bvxor : sexp
val a_bvadd : sexp
val a_bvsub : sexp
val a_bvmul : sexp
val a_bvudiv : sexp
val a_bvurem : sexp
val a_bvsdiv : sexp
val a_bvsrem : sexp
val a_bvsmod : sexp
val a_bvshl : sexp
val a_bvlshr : sexp
val a_bvashr : sexp
val bv_ult : sexp -> sexp -> sexp
val bv_uleq : sexp -> sexp -> sexp
val bv_slt : sexp -> sexp -> sexp
val bv_sleq : sexp -> sexp -> sexp
val bv_concat : sexp -> sexp -> sexp
val bv_sign_extend : int -> sexp -> sexp
val bv_zero_extend : int -> sexp -> sexp
val bv_extract : int -> int -> sexp -> sexp
val bv_not : sexp -> sexp
val bv_and : sexp -> sexp -> sexp
val bv_or : sexp -> sexp -> sexp
val bv_xor : sexp -> sexp -> sexp
val bv_add : sexp -> sexp -> sexp
val bv_sub : sexp -> sexp -> sexp
val bv_mul : sexp -> sexp -> sexp
val bv_udiv : sexp -> sexp -> sexp
val bv_urem : sexp -> sexp -> sexp
val bv_sdiv : sexp -> sexp -> sexp
val bv_srem : sexp -> sexp -> sexp
val bv_smod : sexp -> sexp -> sexp
val bv_shl : sexp -> sexp -> sexp
val bv_lshr : sexp -> sexp -> sexp
val bv_ashr : sexp -> sexp -> sexp

Rounding modes

module RoundingMode : sig ... end

Floating-point

val float_shape : int -> int list
val t_f16 : sexp
val t_f32 : sexp
val t_f64 : sexp
val t_f128 : sexp
val f32_k : float -> sexp
val f64_k : float -> sexp
val f128_k : float -> sexp
val f16_k : float -> sexp
val fp_abs : sexp -> sexp
val fp_eq : sexp -> sexp -> sexp
val fp_leq : sexp -> sexp -> sexp
val fp_lt : sexp -> sexp -> sexp
val fp_add : sexp -> sexp -> sexp
val fp_sub : sexp -> sexp -> sexp
val fp_mul : sexp -> sexp -> sexp
val fp_div : sexp -> sexp -> sexp
val fp_rem : sexp -> sexp -> sexp
val fp_is : fpclass -> sexp -> sexp
val fp_round : RoundingMode.t -> sexp -> sexp

Float/bit-vector conversions

val float_of_bv : int -> sexp -> sexp
val float_of_ubv : RoundingMode.t -> int -> sexp -> sexp
val float_of_sbv : RoundingMode.t -> int -> sexp -> sexp
val ubv_of_float : RoundingMode.t -> int -> sexp -> sexp
val sbv_of_float : RoundingMode.t -> int -> sexp -> sexp

Int/bit-vector conversions

val int_of_bv : bool -> sexp -> sexp
val bv_of_int : int -> sexp -> sexp

Bit-vector overflow predicates

val bv_nego : sexp -> sexp
val bv_uaddo : sexp -> sexp -> sexp
val bv_saddo : sexp -> sexp -> sexp
val bv_usubo : sexp -> sexp -> sexp
val bv_ssubo : sexp -> sexp -> sexp
val bv_umulo : sexp -> sexp -> sexp
val bv_smulo : sexp -> sexp -> sexp

Sequences

val t_seq : sexp
val seq_singl : sexp -> sexp
val seq_concat : sexp list -> sexp

Commands

val simple_command : string list -> sexp
val set_option : string -> string -> sexp
val push : int -> sexp
val pop : int -> sexp
val declare_fun : string -> sexp list -> sexp -> sexp
val declare : string -> sexp -> sexp
type con_field = string * sexp
val declare_datatype : string -> string list -> (string * con_field list) list -> sexp
val assume : sexp -> sexp
val reset : sexp

Solver

type solver_extensions =
  1. | Z3
  2. | CVC5
  3. | Other
type solver_log = {
  1. send : (unit -> string) -> unit;
    (*

    We sent this to the solver.

    *)
  2. receive : (unit -> string) -> unit;
    (*

    We got this from the solver.

    *)
  3. stop : unit -> unit;
    (*

    Cleanup when done.

    *)
}
type solver_config = {
  1. exe : string;
  2. opts : string list;
  3. exts : solver_extensions;
  4. log : solver_log;
}
type solver = {
  1. ack_command : sexp -> sexp;
    (*

    Send a command and synchronously wait for its response. Any fire-and-forget commands sent earlier with command are flushed (their acknowledgements drained) first, so the response read here lines up with this command's own query. Used for the commands whose answer we actually need (check-sat, get-model).

    *)
  2. command : sexp -> unit;
    (*

    Send a command without waiting for its acknowledgement. The solver still runs in :print-success true mode, so each such command still produces exactly one success (or error) line; those are drained in one batch by the next ack_command. This turns the long chain of synchronous round-trips (declare / assert / push / pop / reset that precedes every check-sat) into pipelined writes.

    *)
  3. stop : unit -> unit;
  4. force_stop : unit -> unit;
  5. config : solver_config;
}

Acknowledged commands and checking

val ack_command : solver -> sexp -> unit

Send a command and verify the solver acknowledged it with success.

This goes through ack_command, so it is synchronous: prefer command on the hot path where the acknowledgement can be deferred.

val command : solver -> sexp -> unit

Send a command without waiting for its acknowledgement; see command.

type result =
  1. | Unsat
  2. | Unknown
  3. | Sat
val show_result : result -> Ppx_deriving_runtime.string
val s_check_sat : sexp
val check : solver -> result

Models

val s_get_model : sexp
val get_model : solver -> sexp

Creating solvers

val drain_threshold : int
val new_solver : solver_config -> solver

Solver configurations

val quiet_log : solver_log
val printf_log : solver_log
val cvc5 : solver_config
val z3 : solver_config