Printer (dolmen_loop.Dolmen_loop.Export.Smtlib2.Printer)

Parameters

module Env : Dolmen_intf.Env.Print with type name := Dolmen_std.Name.t

module S : Dolmen_intf.View.Sexpr.S with type id := Dolmen_std.Id.t

module V : 
  Dolmen_intf.View.TFF.S
    with type ty = Env.ty
     and type ty_var = Env.ty_var
     and type ty_cst = Env.ty_cst
     and type term = Env.term
     and type term_var = Env.term_var
     and type term_cst = Env.term_cst

Signature

Env

val add_named : Env.t -> Env.term_cst -> Env.term -> Env.t

Add a `:named` definition to the env.

val set_split_dec : 
  Env.t ->
  (string -> ([ `Pos | `Neg ] * string * string) option) ->
  Env.t

Set a splitting function for decimals.

Helpers

val match_prop_literal : 
  Env.term ->
  [ `Cst of Env.term_cst | `Neg of Env.term_cst | `Not_a_prop_literal ]

Match against prop literals.

Types and terms

val ty : Env.t -> Stdlib.Format.formatter -> Env.ty -> unit

Printer for types

val term : Env.t -> Stdlib.Format.formatter -> Env.term -> unit

Printer for terms

Statements

val echo : Env.t -> Stdlib.Format.formatter -> string -> unit

val set_logic : Env.t -> Stdlib.Format.formatter -> string -> unit

Print a set-logic statement.

val set_info : Env.t -> Stdlib.Format.formatter -> S.t -> unit

val set_option : Env.t -> Stdlib.Format.formatter -> S.t -> unit

val get_info : Env.t -> Stdlib.Format.formatter -> S.t -> unit

val get_option : Env.t -> Stdlib.Format.formatter -> S.t -> unit

val get_value : Env.t -> Stdlib.Format.formatter -> Env.term list -> unit

val pop : Env.t -> Stdlib.Format.formatter -> int -> unit

pop fmt n prints a statement that pops `n` levels.

raises Cannot_print
if the provided level is non-positive

val push : Env.t -> Stdlib.Format.formatter -> int -> unit

push fmt n prints a statement that pushes `n` levels.

raises Cannot_print
if the provided level is non-positive

val declare_sort : Env.t -> Stdlib.Format.formatter -> Env.ty_cst -> unit

Declare a sort, i.e. a type constant.

val declare_datatype : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.ty_cst
   * Env.ty_var list
   * (Env.term_cst * (Env.ty * Env.term_cst) list) list) ->
  unit

Declare a single datatype.

val declare_datatypes : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.ty_cst
   * Env.ty_var list
   * (Env.term_cst * (Env.ty * Env.term_cst) list) list)
    list ->
  unit

Declare multiple mutually recursive datatypes.

val declare_fun : Env.t -> Stdlib.Format.formatter -> Env.term_cst -> unit

Declare a function, i.e. a term constant. This will use either the `declare-fun` or the `declare-const` statement depending on the actualy type of the function.

val define_sort : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.ty_cst * Env.ty_var list * Env.ty) ->
  unit

val define_fun : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.term_cst * Env.ty_var list * Env.term_var list * Env.term) ->
  unit

val define_fun_rec : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.term_cst * Env.ty_var list * Env.term_var list * Env.term) ->
  unit

val define_funs_rec : 
  Env.t ->
  Stdlib.Format.formatter ->
  (Env.term_cst * Env.ty_var list * Env.term_var list * Env.term) list ->
  unit

val assert_ : Env.t -> Stdlib.Format.formatter -> Env.term -> unit

val check_sat : Env.t -> Stdlib.Format.formatter -> unit -> unit

val check_sat_assuming : 
  Env.t ->
  Stdlib.Format.formatter ->
  Env.term list ->
  unit

val reset : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `reset` statement.

val reset_assertions : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `reset-assertion` statement.

val get_unsat_core : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `get-unsat-core` statement.

val get_unsat_assumptions : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `get-unsat-assumptions` statement.

val get_proof : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `get-proof` statement.

val get_model : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `get-model` statement.

val get_assertions : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `get-assertions` statement.

val get_assignment : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print a `get-assignment` statement.

val exit : Env.t -> Stdlib.Format.formatter -> unit -> unit

Print an `exit` statement.