Module Simple_smt

SMT Basics

type sexp = Sexplib.Sexp.t
val atom : string -> sexp
val list : sexp list -> sexp
val is_atom : sexp -> bool
val to_list : sexp -> Sexplib.Sexp.t list option
val app : sexp -> sexp list -> sexp

Apply a function to some arguments.

val app_ : string -> sexp list -> sexp

Apply a function to some arguments

val as_type : sexp -> sexp -> sexp

Type annotation

val let_ : (string * sexp) list -> sexp -> sexp

Let expression

val nat_k : int -> sexp

Non-negative numeric constant.

val nat_zk : Z.t -> sexp

Non-negative numeric constant.

val fam : string -> sexp list -> sexp

Indexed family

val ifam : string -> int list -> sexp

Int-indexed family

val named : string -> sexp -> sexp

Attribute

val allowed_simple_char : char -> bool

Symbols are either simple or quoted (c.f. SMTLIB v2.6 S3.1). This predicate indicates whether a character is allowed in a simple symbol. Note that only ASCII letters are allowed.

val is_simple_symbol : Stdlib.String.t -> bool
val quote_symbol : Stdlib.String.t -> Stdlib.String.t
val symbol : Stdlib.String.t -> sexp

Make an SMT name, quoting if needed. Note that even with quoting the name should not contain pipe (|) or backslash (\)

Booleans

val t_bool : sexp

The type of booleans.

val bool_k : bool -> sexp

Boolean constant

val ite : sexp -> sexp -> sexp -> sexp

If-then-else. This is polymorphic and can be used to construct any term.

val eq : sexp -> sexp -> sexp

Arguments are equal.

val distinct : sexp list -> sexp

All arguments are pairwise different.

val bool_not : sexp -> sexp

Logical negation.

val bool_and : sexp -> sexp -> sexp

Conjunction.

val bool_ands : sexp list -> sexp

Conjunction.

val bool_or : sexp -> sexp -> sexp

Disjunction.

val bool_ors : sexp list -> sexp

Disjunction.

val bool_xor : sexp -> sexp -> sexp

Exclusive-or.

val bool_implies : sexp -> sexp -> sexp

Implication.

Integers and Reals

val t_int : sexp

The type of integers.

val t_real : sexp

The type of reals.

val num_neg : sexp -> sexp

Numeric negation.

val int_k : int -> sexp

Integer constant

val int_zk : Z.t -> sexp

Integer constant

val real_div : sexp -> sexp -> sexp

Division of real numbers.

val real_k : Q.t -> sexp

Real constant.

val num_gt : sexp -> sexp -> sexp

Greater-then for numbers.

val num_lt : sexp -> sexp -> sexp

Less-then for numbers.

val num_geq : sexp -> sexp -> sexp

Greater-than-or-equal-to for numbers.

val num_leq : sexp -> sexp -> sexp

Less-than-or-equal-to for numbers.

val num_add : sexp -> sexp -> sexp

Numeric addition.

val num_sub : sexp -> sexp -> sexp

Numeric subtraction.

val num_mul : sexp -> sexp -> sexp

Numeric multiplication.

val num_abs : sexp -> sexp

Numeric absolute value.

val num_div : sexp -> sexp -> sexp

Numeric division.

val num_mod : sexp -> sexp -> sexp

Numeric modulus.

val num_rem : sexp -> sexp -> sexp

Numeric reminder. Nonstandard.

val num_divisible : sexp -> int -> sexp

Is the number divisible by the given constant?

val real_to_int : sexp -> sexp

Satisfies real_to_int x <= x (i.e., this is like floor)

val int_to_real : sexp -> sexp

Promote an integer to a real.

Bit-vectors

val t_bits : int -> sexp

t_bits w is the type of bit vectors of width w.

val bv_nat_bin : int -> Z.t -> sexp

A bit-vector represented in binary.

  • The number should be non-negative.
  • The number should not exceed the number of bits.
val bv_nat_hex : int -> Z.t -> sexp

A bit-vector represented in hex.

  • The number should be non-negative.
  • The number should not exceed the number of bits.
  • The width should be a multiple of 4.
val bv_neg : sexp -> sexp

Bit vector arithmetic negation.

val bv_bin : int -> Z.t -> sexp

A bit-vector represented in binary. The number should fit in the given number of bits.

val bv_hex : int -> Z.t -> sexp

A bit-vector represented in hex .

  • The number should fit in the given number of bits.
  • The width should be a multiple of 4.
val bv_k : int -> Z.t -> sexp

Make a bit-vector literal. Uses hex representation if the size is a multiple of 4, and binary otherwise.

val bv_ult : sexp -> sexp -> sexp

Unsigned less-than on bit-vectors.

val bv_uleq : sexp -> sexp -> sexp

Unsigned less-than-or-equal on bit-vectors.

val bv_slt : sexp -> sexp -> sexp

Signed less-than on bit-vectors.

val bv_sleq : sexp -> sexp -> sexp

Signed less-than-or-equal on bit-vectors.

val bv_concat : sexp -> sexp -> sexp

Bit vector concatenation.

val bv_sign_extend : int -> sexp -> sexp

Extend to the signed equivalent bitvector by the given number of bits.

val bv_zero_extend : int -> sexp -> sexp

Zero extend by the given number of bits.

val bv_extract : int -> int -> sexp -> sexp

bv_extract i j x is a sub-vector of x. i is the larger bit index, j is the smaller one, and indexing is inclusive.

val bv_not : sexp -> sexp

Bitwise negation.

val bv_and : sexp -> sexp -> sexp

Bitwise conjuction.

val bv_or : sexp -> sexp -> sexp

Bitwise disjunction.

val bv_xor : sexp -> sexp -> sexp

Bitwise exclusive or.

val bv_add : sexp -> sexp -> sexp

Addition of bit vectors.

val bv_sub : sexp -> sexp -> sexp

Subtraction of bit vectors.

val bv_mul : sexp -> sexp -> sexp

Multiplication of bit vectors.

val bv_udiv : sexp -> sexp -> sexp

Bit vector unsigned division.

val bv_urem : sexp -> sexp -> sexp

Bit vector unsigned reminder.

val bv_sdiv : sexp -> sexp -> sexp

Bit vector signed division.

val bv_srem : sexp -> sexp -> sexp

Bit vector signed reminder.

val bv_smod : sexp -> sexp -> sexp

Bit vector signed modulus. Nonstandard?

val bv_shl : sexp -> sexp -> sexp

Shift left.

val bv_lshr : sexp -> sexp -> sexp

Logical shift right.

val bv_ashr : sexp -> sexp -> sexp

Arithemti shift right (copies most significant bit).

Arrays

val t_array : sexp -> sexp -> sexp

t_tarray kt vt is the type of arrays with keys kt and values vt

val arr_const : sexp -> sexp -> sexp -> sexp

arr_const kt vt v is an array of type Array kt vt where all elements are v. v should be of type vt.

val arr_select : sexp -> sexp -> sexp

arr_select arr ix is the element stored at index ix of arr.

val arr_store : sexp -> sexp -> sexp -> sexp

arr_store arr ix val is an array that is the same as arr, except at index ix it has val

Sets

type solver_extensions =
  1. | Z3
  2. | CVC5
  3. | Other

Some solvers support theories outside of SMTLIB and, unfortunately, there is no standard for what things are called. We use this flag to decide how to generate terms for those cases.

val t_set : sexp -> sexp

t_set t is the type of sets with elements of type t.

val set_empty : solver_extensions -> sexp -> sexp

set_empty ext t is the empty set with elements of type t

val set_universe : solver_extensions -> sexp -> sexp

set_universe ext t is the universal set with elements of type t

val set_insert : solver_extensions -> sexp -> sexp -> sexp

set_insert ext x xs is a set that has all elements of xs and also x

val set_union : solver_extensions -> sexp -> sexp -> sexp

set_union ext xs ys has all elements from xs and also from ys

val set_intersection : solver_extensions -> sexp -> sexp -> sexp

set_intersection ext xs ys has the elements that are in both xs and ys

val set_difference : solver_extensions -> sexp -> sexp -> sexp

set_difference ext xs ys has the elements of xs that are not in ys

val set_complement : solver_extensions -> sexp -> sexp

set_complement ext xs has all elements that are not in xs

val set_member : solver_extensions -> sexp -> sexp -> sexp

set_member ext x xs is true if x is a member of xs

val set_subset : solver_extensions -> sexp -> sexp -> sexp

set_subset ext xs ys is true if all elements of xs are also in ys

Commands

The S-Expressions in this section define commands to the SMT solver. These can be sent to solver using ack_command.

val simple_command : string list -> sexp

A command made out of just atoms.

val set_option : string -> string -> sexp

set_option opt val sets option opt to value val.

val set_logic : string -> sexp

Set the logic to use.

val push : int -> sexp

Push a new scope.

val pop : int -> sexp

Pop a scope.

val declare_sort : string -> int -> sexp

declare_sort name arity declares a type name, which expect arity type parameters.

val declare_fun : string -> sexp list -> sexp -> sexp

declare_fun name param_types result_type declareas a function expecting arguments with types param_types and computes a value of type result_type.

val declare : string -> sexp -> sexp

declare name type declares a constant name of type type.

val define_fun : string -> (string * sexp) list -> sexp -> sexp -> sexp

define_fun name params result_type definition defines a function called name, with the given parameters (name, type), that computes a value of result_type, using definition.

val define : string -> sexp -> sexp -> sexp

define name type definition defines a constant name, of type type defined as definition.

type con_field = string * sexp

The fields of an ADT constructor: (field_name, field_type)

val declare_datatype : string -> string list -> (string * con_field list) list -> sexp

declare_datatype name type_params cons define an ADT called name with type parameters type_params and constructors cons. Each constructor is of the form (name, fields).

type pat =
  1. | PVar of string
  2. | PCon of string * string list
val match_datatype : sexp -> (pat * sexp) list -> sexp
val is_con : string -> sexp -> sexp

is_con c e is true if e is an expression constructed with c

val assume : sexp -> sexp

Add an assertion to the current scope.

Solver

type solver_log = {
  1. send : string -> unit;
    (*

    We sent this to the solver.

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

    We got this from the solver.

    *)
}
type solver_config = {
  1. exe : string;
  2. opts : string list;
  3. exts : solver_extensions;
  4. log : solver_log;
}
type solver = {
  1. command : sexp -> sexp;
  2. stop : unit -> Unix.process_status;
  3. force_stop : unit -> Unix.process_status;
  4. config : solver_config;
}

A connection to a solver

exception UnexpectedSolverResponse of sexp
val ack_command : solver -> sexp -> unit

Issue a command and wait for it to succeed. Throws UnexpectedSolverResponse

type result =
  1. | Unsat
  2. | Unknown
  3. | Sat
val pp_result : Ppx_deriving_runtime.Format.formatter -> result -> Ppx_deriving_runtime.unit
val show_result : result -> Ppx_deriving_runtime.string
val check : solver -> result

Check if the current set of assumptions are consistent. Throws UnexpectedSolverResponse.

Decoding Results

val get_model : solver -> sexp

Get all definitions currently in scope. Only valid after a Sat result. See also model_eval.

val get_exprs : solver -> sexp list -> sexp list

Get the values of some s-expressions. Only valid after a Sat result. Throws UnexpectedSolverResponse.

val get_expr : solver -> sexp -> sexp

Evalute the given expression in the current context. Only valid after a Sat result. Throws UnexpectedSolverResponse.

val to_bool : sexp -> bool

Try to decode an s-expression as a boolean Throws UnexpectedSolverResponse.

val to_bits : int -> bool -> sexp -> Z.t

Try to decode an s-expression as a bitvector of the given width. The 2nd argument indicates if the number is signed. Throws UnexpectedSolverResponse.

val to_z : sexp -> Z.t

Try to decode an s-expression as an integer. Throws UnexpectedSolverResponse.

val to_q : sexp -> Q.t

Try to decode an s-expression as a rational number. Throws UnexpectedSolverResponse.

val to_con : sexp -> string * sexp list

Try to decode an s-expression as constructor with field values. Throws UnexpectedSolverResponse.

Creating Solvers

val new_solver : solver_config -> solver
type model_evaluator = {
  1. eval : (string * (string * sexp) list * sexp * sexp) list -> sexp -> sexp;
    (*

    First define some local variables, then evaluate the expression

    *)
  2. stop : unit -> Unix.process_status;
  3. force_stop : unit -> Unix.process_status;
}

A connection to a solver, specialized for evaluting in the context of a model

Model Evaluation

val model_eval : solver_config -> sexp -> model_evaluator

Solver Configurations

val quiet_log : solver_log
val printf_log : 'a -> solver_log
val cvc5 : solver_config
val z3 : solver_config