Module Make.Smtlib2_7

val split_dec : string -> ([> `Neg | `Pos ] * string * string) option
exception Error of State.t
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 = {
  1. id : Dolmen.Std.Id.t;
  2. loc : Dolmen.Std.Loc.t;
  3. contents : 'a;
  4. attrs : Dolmen.Std.Term.t list;
  5. implicit : bool;
}
type decl = [
  1. | `Implicit_type_var
  2. | `Term_decl of term_cst
  3. | `Type_decl of ty_cst * ty_def option
]
type decls = [
  1. | `Decls of bool * decl list
]
type def = [
  1. | `Instanceof of Dolmen.Std.Id.t * term_cst * ty list * ty_var list * term_var list * term
  2. | `Term_def of Dolmen.Std.Id.t * term_cst * ty_var list * term_var list * term
  3. | `Type_alias of Dolmen.Std.Id.t * ty_cst * ty_var list * ty
]
type defs = [
  1. | `Defs of bool * def list
]
type assume = [
  1. | `Clause of formula list
  2. | `Goal of formula
  3. | `Hyp of formula
]
type solve = [
  1. | `Solve of formula list * formula list
]
type get_info = [
  1. | `Echo of string
  2. | `Get_assertions
  3. | `Get_assignment
  4. | `Get_info of Dolmen.Std.Statement.term
  5. | `Get_model
  6. | `Get_option of Dolmen.Std.Statement.term
  7. | `Get_proof
  8. | `Get_unsat_assumptions
  9. | `Get_unsat_core
  10. | `Get_value of term list
  11. | `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list
]
type set_info = [
  1. | `Set_info of Dolmen.Std.Statement.term
  2. | `Set_logic of string * Dolmen_type.Logic.t
  3. | `Set_option of Dolmen.Std.Statement.term
]
type stack_control = [
  1. | `Pop of int
  2. | `Push of int
  3. | `Reset
  4. | `Reset_assertions
]
type exit = [
  1. | `Exit
]
type end_ = [
  1. | `End
]
type typechecked = [
  1. | `Clause of formula list
  2. | `Decls of bool * decl list
  3. | `Defs of bool * def list
  4. | `Echo of string
  5. | `End
  6. | `Exit
  7. | `Get_assertions
  8. | `Get_assignment
  9. | `Get_info of Dolmen.Std.Statement.term
  10. | `Get_model
  11. | `Get_option of Dolmen.Std.Statement.term
  12. | `Get_proof
  13. | `Get_unsat_assumptions
  14. | `Get_unsat_core
  15. | `Get_value of term list
  16. | `Goal of formula
  17. | `Hyp of formula
  18. | `Other of Dolmen.Std.Id.t * Dolmen.Std.Statement.term list
  19. | `Pop of int
  20. | `Push of int
  21. | `Reset
  22. | `Reset_assertions
  23. | `Set_info of Dolmen.Std.Statement.term
  24. | `Set_logic of string * Dolmen_type.Logic.t
  25. | `Set_option of Dolmen.Std.Statement.term
  26. | `Solve of formula list * formula list
]
module Env : sig ... end
module P : sig ... end
type acc = Smtlib2(State)(Dolmen.Smtlib2.Script.V2_7.Print.Make)(Expr)(Sexpr)(View)(Typer_Types).acc = {
  1. env : Env.t;
  2. fmt : Stdlib.Format.formatter;
  3. 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