sig
module type Id = Ast_smtlib.Id
module type Term = Ast_smtlib.Term
module type Statement = Ast_smtlib.Statement
module Make :
functor
(L : ParseLocation.S) (I : Id) (T : sig
type t
val const : ?loc:L.t -> I.t -> t
val int : ?loc:L.t -> string -> t
val real :
?loc:L.t -> string -> t
val hexa :
?loc:L.t -> string -> t
val binary :
?loc:L.t -> string -> t
val colon :
?loc:L.t -> t -> t -> t
val apply :
?loc:L.t -> t -> t list -> t
val letin :
?loc:L.t -> t list -> t -> t
val forall :
?loc:L.t -> t list -> t -> t
val exists :
?loc:L.t -> t list -> t -> t
val sexpr :
?loc:L.t -> t list -> t
val annot :
?loc:L.t -> t -> t list -> t
end) (S : sig
type t
val pop :
?loc:L.t -> int -> t
val push :
?loc:L.t -> int -> t
val assert_ :
?loc:L.t -> T.t -> t
val check_sat :
?loc:L.t -> unit -> t
val set_logic :
?loc:L.t ->
string -> t
val get_info :
?loc:L.t ->
string -> t
val set_info :
?loc:L.t ->
string * T.t option ->
t
val get_option :
?loc:L.t ->
string -> t
val set_option :
?loc:L.t ->
string * T.t option ->
t
val type_decl :
?loc:L.t ->
I.t -> int -> t
val type_def :
?loc:L.t ->
I.t ->
I.t list -> T.t -> t
val fun_decl :
?loc:L.t ->
I.t ->
T.t list -> T.t -> t
val fun_def :
?loc:L.t ->
I.t ->
T.t list ->
T.t -> T.t -> t
val get_proof :
?loc:L.t -> unit -> t
val get_unsat_core :
?loc:L.t -> unit -> t
val get_value :
?loc:L.t ->
T.t list -> t
val get_assignment :
?loc:L.t -> unit -> t
val get_assertions :
?loc:L.t -> unit -> t
val exit :
?loc:L.t -> unit -> t
end) ->
sig
type token
type statement = S.t
module Lexer :
sig exception Error val token : Lexing.lexbuf -> token end
module Parser :
sig
exception Error
val file :
(Lexing.lexbuf -> token) -> Lexing.lexbuf -> statement list
val input :
(Lexing.lexbuf -> token) -> Lexing.lexbuf -> statement option
module MenhirInterpreter :
sig
type token = token
type env
type production
type 'a checkpoint = private
InputNeeded of env
| Shifting of env * env * bool
| AboutToReduce of env * production
| HandlingError of env
| Accepted of 'a
| Rejected
val offer :
'a checkpoint ->
token * Lexing.position * Lexing.position -> 'a checkpoint
val resume : 'a checkpoint -> 'a checkpoint
type supplier =
unit -> token * Lexing.position * Lexing.position
val lexer_lexbuf_to_supplier :
(Lexing.lexbuf -> token) -> Lexing.lexbuf -> supplier
val loop : supplier -> 'a checkpoint -> 'a
val loop_handle :
('a -> 'answer) ->
('a checkpoint -> 'answer) ->
supplier -> 'a checkpoint -> 'answer
val loop_handle_undo :
('a -> 'answer) ->
('a checkpoint -> 'a checkpoint -> 'answer) ->
supplier -> 'a checkpoint -> 'answer
val loop_test :
(env -> 'accu -> 'accu) -> 'a checkpoint -> 'accu -> 'accu
val acceptable :
'a checkpoint -> token -> Lexing.position -> bool
type 'a lr1state
val number : 'a lr1state -> int
type element =
Element : 'a lr1state * 'a * Lexing.position *
Lexing.position -> element
type stack = element MenhirLib.General.stream
val stack : env -> stack
val positions : env -> Lexing.position * Lexing.position
val has_default_reduction : env -> bool
end
module Incremental :
sig
val input :
Lexing.position ->
statement option MenhirInterpreter.checkpoint
end
end
val find : ?dir:string -> string -> string option
val parse_file : string -> statement list
val parse_input :
[ `File of string | `Stdin ] -> unit -> statement option
end
end