package dolmen_model

  1. Overview
  2. Docs
On This Page
  1. Types
include Dolmen_loop.Typer_intf.Types with type state := State.t with type ty := Dolmen.Std.Expr.ty with type ty_var := Dolmen.Std.Expr.ty_var with type ty_cst := Dolmen.Std.Expr.ty_cst with type term := Dolmen.Std.Expr.term with type term_var := Dolmen.Std.Expr.term_var with type term_cst := Dolmen.Std.Expr.term_cst with type formula := Dolmen.Std.Expr.formula
val type_check : bool State.key
val init : type_check:bool -> State.t -> State.t

Types

type +'a stmt = {
  1. id : Dolmen.Std.Id.t;
  2. loc : Dolmen.Std.Loc.t;
  3. contents : 'a;
}

Wrapper around statements. It records implicit type declarations.

type decl = [
  1. | `Type_decl of Dolmen.Std.Expr.ty_cst
  2. | `Term_decl of Dolmen.Std.Expr.term_cst
]

The type of top-level type declarations.

type decls = [
  1. | `Decls of decl list
]

A list of type declarations.

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

type defs = [
  1. | `Defs of def list
]

A list of definitions

type assume = [
  1. | `Hyp of Dolmen.Std.Expr.formula
  2. | `Goal of Dolmen.Std.Expr.formula
  3. | `Clause of Dolmen.Std.Expr.formula list
]

The type of top-level assertion statements

type solve = [
  1. | `Solve of Dolmen.Std.Expr.formula list
]

Top-level solve instruction

type get_info = [
  1. | `Get_info of string
  2. | `Get_option of string
  3. | `Get_proof
  4. | `Get_unsat_core
  5. | `Get_unsat_assumptions
  6. | `Get_model
  7. | `Get_value of Dolmen.Std.Expr.term list
  8. | `Get_assignment
  9. | `Get_assertions
  10. | `Echo of string
  11. | `Plain of Dolmen.Std.Statement.term
]

Various info getters

type set_info = [
  1. | `Set_logic of string
  2. | `Set_info of Dolmen.Std.Statement.term
  3. | `Set_option of Dolmen.Std.Statement.term
]

Info setters

type stack_control = [
  1. | `Pop of int
  2. | `Push of int
  3. | `Reset_assertions
  4. | `Reset
]

Stack control

type exit = [
  1. | `Exit
]

Exit statement

type typechecked = [
  1. | defs
  2. | decls
  3. | assume
  4. | solve
  5. | get_info
  6. | set_info
  7. | stack_control
  8. | exit
]

The type of statements after typechecking

val print : Stdlib.Format.formatter -> typechecked stmt -> unit

Printing funciton for typechecked statements.

val typecheck : State.t -> Dolmen.Std.Statement.t -> State.t * [ `Continue of typechecked stmt | `Done of unit ]

Typechecks a statement.