package alt-ergo-lib

  1. Overview
  2. Docs
package alt-ergo-lib
Legend:
Library
Module
Module type
Parameter
Class
Class type
type env = Typer.env
val type_check : bool State.key
val init : type_check:bool -> State.t -> State.t
type !'a stmt = {
  1. id : Dolmen.Std.Id.t;
  2. loc : Dolmen.Std.Loc.t;
  3. contents : 'a;
  4. attrs : Dolmen.Std.Term.t list;
}
type decl = [
  1. | `Term_decl of DStd.Expr.term_cst
  2. | `Type_decl of DStd.Expr.ty_cst * DStd.Expr.ty_def option
]
type decls = [
  1. | `Decls of decl list
]
type defs = [
  1. | `Defs of def list
]
type assume = [
  1. | `Clause of DStd.Expr.formula list
  2. | `Goal of DStd.Expr.formula
  3. | `Hyp of DStd.Expr.formula
]
type solve = [
  1. | `Solve of DStd.Expr.formula list * DStd.Expr.formula list
]
type get_info = [
  1. | `Echo of string
  2. | `Get_assertions
  3. | `Get_assignment
  4. | `Get_info of string
  5. | `Get_model
  6. | `Get_option of string
  7. | `Get_proof
  8. | `Get_unsat_assumptions
  9. | `Get_unsat_core
  10. | `Get_value of DStd.Expr.term list
  11. | `Plain of Dolmen.Std.Statement.term
]
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 typechecked = [
  1. | `Clause of DStd.Expr.formula list
  2. | `Decls of decl list
  3. | `Defs of def list
  4. | `Echo of string
  5. | `Exit
  6. | `Get_assertions
  7. | `Get_assignment
  8. | `Get_info of string
  9. | `Get_model
  10. | `Get_option of string
  11. | `Get_proof
  12. | `Get_unsat_assumptions
  13. | `Get_unsat_core
  14. | `Get_value of DStd.Expr.term list
  15. | `Goal of DStd.Expr.formula
  16. | `Hyp of DStd.Expr.formula
  17. | `Plain of Dolmen.Std.Statement.term
  18. | `Pop of int
  19. | `Push of int
  20. | `Reset
  21. | `Reset_assertions
  22. | `Set_info of Dolmen.Std.Statement.term
  23. | `Set_logic of string * Dolmen_type.Logic.t
  24. | `Set_option of Dolmen.Std.Statement.term
  25. | `Solve of DStd.Expr.formula list * DStd.Expr.formula list
]
val print : Stdlib.Format.formatter -> typechecked stmt -> unit
val typecheck : State.t -> Dolmen.Std.Statement.t -> State.t * [ `Continue of typechecked stmt | `Done of unit ]