Smtlib2 (dolmen_loop.Dolmen_loop.Export.Smtlib2)

Parameters

module State : State.S

module Printer : Make_smt2_printer

module Expr : Expr_intf.Export

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

module View : 
  Dolmen_intf.View.TFF.S
    with type ty = Expr.Ty.t
     and type ty_var = Expr.Ty.Var.t
     and type ty_cst = Expr.Ty.Const.t
     and type ty_def = Expr.ty_def
     and type term = Expr.Term.t
     and type term_var = Expr.Term.Var.t
     and type term_cst = Expr.Term.Const.t

module Typer_Types : 
  Typer.Types
    with type ty = Expr.ty
     and type ty_var = Expr.ty_var
     and type ty_cst = Expr.ty_cst
     and type ty_def = Expr.ty_def
     and type term = Expr.term
     and type term_var = Expr.term_var
     and type term_cst = Expr.term_cst
     and type formula = Expr.term

Signature

val split_dec : string -> ([> `Neg | `Pos ] * string * string) option

exception Error of State.t

include module type of struct include Typer_Types end

include Expr_intf.S
  with type ty = Expr.ty
  with type ty_var = Expr.ty_var
  with type ty_cst = Expr.ty_cst
  with type ty_def = Expr.ty_def
  with type term = Expr.term
  with type term_var = Expr.term_var
  with type term_cst = Expr.term_cst
  with type formula = Expr.term

type ty = Expr.ty

type ty_var = Expr.ty_var

type ty_cst = Expr.ty_cst

type ty_def = Expr.ty_def

type term = Expr.term

type term_var = Expr.term_var

type term_cst = Expr.term_cst

type formula = Expr.term

type nonrec +'a stmt = 'a Typer_intf.stmt = {

id : Dolmen.Std.Id.t;
loc : Dolmen.Std.Loc.t;
contents : 'a;
attrs : Dolmen.Std.Term.t list;
implicit : bool;

}

Wrapper around statements. It records implicit type declarations.

type decl = [

| `Implicit_type_var
| `Type_decl of ty_cst * ty_def option
| `Term_decl of term_cst

]

The type of top-level type declarations.

type decls = [

| `Decls of bool * decl list

]

A list of type declarations.

type def = [

| `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty
| `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term
| `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term

]

The type of top-level type definitions. Type definitions are inlined and so can be ignored.

type defs = [

| `Defs of bool * def list

]

A list of definitions

type assume = [

| `Hyp of formula
| `Goal of formula
| `Clause of formula list

]

The type of top-level assertion statements

type solve = [

| `Solve of formula list * formula list
(*
`Solve (hyps, goals) represents a sequent with local hypotheses hyps and local goals goals.
*)

]

Top-level solve instruction

type get_info = [

| `Get_info of Dolmen.Std.Statement.term
| `Get_option of Dolmen.Std.Statement.term
| `Get_proof
| `Get_unsat_core
| `Get_unsat_assumptions
| `Get_model
| `Get_value of term list
| `Get_assignment
| `Get_assertions
| `Echo of string
| `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list

]

Various info getters

type set_info = [

| `Set_logic of string * Dolmen_type.Logic.t
| `Set_info of Dolmen.Std.Statement.term
| `Set_option of Dolmen.Std.Statement.term

]

Info setters

type stack_control = [

| `Pop of int
| `Push of int
| `Reset_assertions
| `Reset

]

Stack control

type exit = [

| `Exit

]

Exit statement

type end_ = [

| `End

]

type typechecked = [

| defs
| decls
| assume
| solve
| get_info
| set_info
| stack_control
| exit
| end_

]

The type of statements after typechecking

module Env : sig ... end

module P : sig ... end

type acc = {

env : Env.t;
fmt : Stdlib.Format.formatter;
close : unit -> unit;

}

val init : close:(unit -> unit) -> Stdlib.Format.formatter -> acc

val pp_stmt : 
  State.t ->
  acc ->
  (Env.t -> Stdlib.Format.formatter -> 'a -> unit) ->
  'a ->
  State.t * acc

val map_decl : 
  [< `Term_decl of 'a | `Type_decl of 'b * View.Ty.Def.t option ] ->
  [> `Left of [> `Term_decl of 'a | `Type_decl of 'b ]
  | `Right of
    'b
    * View.ty_var list
    * (View.term_cst * (View.ty * View.term_cst) list) list ]

val register_simple_decl : 
  Env.t ->
  [< `Term_decl of Expr.term_cst | `Type_decl of Expr.ty_cst ] ->
  Env.t

val register_adt_decl : 
  Env.t ->
  (Expr.ty_cst * 'a * (Expr.term_cst * ('b * Expr.term_cst) list) list) ->
  Env.t

val print_simple_decl : 
  (State.t * acc) ->
  [< `Term_decl of Env.term_cst | `Type_decl of Env.ty_cst ] ->
  State.t * acc

val print_decls : 
  State.t ->
  acc ->
  [< `Implicit_type_var
  | `Term_decl of Env.term_cst
  | `Type_decl of Env.ty_cst * View.Ty.Def.t option ]
    list ->
  'a ->
  State.t * acc

val map_def : 
  State.t ->
  [< `Instanceof of 'a
  | `Term_def of 'b * 'c * 'd * 'e * 'f
  | `Type_alias of 'g * 'h * 'i * 'j ] ->
  [> `Left of 'h * 'i * 'j | `Right of 'c * 'd * 'e * 'f ]

val assert_not_named : Expr.Term.Const.t -> unit

val print_defs : 
  State.t ->
  acc ->
  [< `Instanceof of 'a
  | `Term_def of
    'b * Expr.Term.Const.t * Env.ty_var list * Env.term_var list * Env.term
  | `Type_alias of 'c * Env.ty_cst * Env.ty_var list * Env.ty ]
    list ->
  bool ->
  State.t * acc

val is_not_trivially_false : View.Term.t -> bool

val print_solve_aux : State.t -> acc -> hyps:Env.term list -> State.t * acc

val print_solve : 
  State.t ->
  acc ->
  hyps:Env.term list ->
  goals:View.Term.t list ->
  State.t * acc

val print : 
  State.t ->
  acc ->
  Typer_Types.typechecked Typer_Types.stmt ->
  State.t * acc