package dolmen_model

You can search for identifiers within the package.

in-package search v0.2.0

dolmen_model
- Dolmen_model
  - Adt
  - Array
  - Bitv
  - Bool
  - Coercion
  - Core
  - Env
  - Eval
  - Fp
  - Fun
  - Int
  - Loop
    
    Make
    
    Parse
    
    State
    
    Typer
    
    Typer_Pipe
  - Model
    
    Cst
    
    S
    
    Var
  - Rat
  - Real
  - Value

Legend:
Library
Module
Module type
Parameter
Class
Class type

type 'a fragment

The type of fragments on which error/warning can occur.

type error

The type of type-checking errors.

type warning

The type of type-checking warnings.

type builtin_symbols

The type of builin symbols for the type-checker.

val ty_state : Dolmen_loop.Typer.ty_state State.key

Key to store the local typechecking state in the global pipeline state.

val check_model : bool State.key

The typechecker needs to know whether we are checking models or not.

val smtlib2_forced_logic : string option State.key

The typechecker needs to know whether we are checking models or not.

val init : 
  ?ty_state:Dolmen_loop.Typer.ty_state ->
  ?smtlib2_forced_logic:string option ->
  State.t ->
  State.t

This signature includes the requirements to instantiate the {Pipes.Make: functor

include Dolmen_loop.Typer_intf.Typer
  with type state := State.t
   and type ty := Dolmen.Std.Expr.ty
   and type ty_var := Dolmen.Std.Expr.ty_var
   and type ty_cst := Dolmen.Std.Expr.ty_cst
   and type term := Dolmen.Std.Expr.term
   and type term_var := Dolmen.Std.Expr.term_var
   and type term_cst := Dolmen.Std.Expr.term_cst
   and type formula := Dolmen.Std.Expr.formula

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

type input = [

| `Logic of Dolmen_loop.Logic.language Dolmen_loop.State.file
| `Response of Dolmen_loop.Response.language Dolmen_loop.State.file

]

val reset : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t

val reset_assertions : State.t -> ?loc:Dolmen.Std.Loc.t -> unit -> State.t

val push : State.t -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> State.t

val pop : State.t -> input:input -> ?loc:Dolmen.Std.Loc.t -> int -> State.t

val set_logic : 
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  string ->
  State.t

val defs : 
  mode:[ `Create_id | `Use_declared_id ] ->
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.defs ->
  State.t
  * [ `Type_def of
        Dolmen.Std.Id.t
        * Dolmen.Std.Expr.ty_cst
        * Dolmen.Std.Expr.ty_var list
        * Dolmen.Std.Expr.ty
    | `Term_def of
      Dolmen.Std.Id.t
      * Dolmen.Std.Expr.term_cst
      * Dolmen.Std.Expr.ty_var list
      * Dolmen.Std.Expr.term_var list
      * Dolmen.Std.Expr.term ]
      list

val decls : 
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Statement.decls ->
  State.t
  * [ `Type_decl of Dolmen.Std.Expr.ty_cst
    | `Term_decl of Dolmen.Std.Expr.term_cst ]
      list

val terms : 
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  State.t * Dolmen.Std.Expr.term list

val formula : 
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  goal:bool ->
  Dolmen.Std.Term.t ->
  State.t * Dolmen.Std.Expr.formula

val formulas : 
  State.t ->
  input:input ->
  ?loc:Dolmen.Std.Loc.t ->
  ?attrs:Dolmen.Std.Term.t list ->
  Dolmen.Std.Term.t list ->
  State.t * Dolmen.Std.Expr.formula list

val report_error : input:input -> State.t -> error -> State.t

Report a typing error by calling the appropriate state function.

val report_warning : input:input -> State.t -> warning -> State.t

Return a typing warning by calling the appropriate state function.

val additional_builtins : builtin_symbols Stdlib.ref

This reference can be modified to parse new builtin symbols. By default no additional builtin symbols are parsed. It is added for all the languages except Dimacs, and iCNF.

val pop_inferred_model_constants : State.t -> Dolmen.Std.Expr.term_cst list

TODO:doc