Module MoxiInput

type error =
  1. | UnexpectedChar of Lib.position * char
  2. | SyntaxError of Lib.position
  3. | TypeError of MoxiTypeChecker.error
  4. | Unsupported of Lib.position * string
    (*

    A well-sorted construct that kmoxi does not translate

    *)
val pp_print_error : Stdlib.Format.formatter -> error -> unit

Print an error as file:line:column: error: message

type system_check = TransSys.t SubSystem.t
type encoding = {
  1. current_state : bool;
    (*

    Every condition is over the current state: it holds in the transition from a state, which the property reads, so a counterexample has a last state that is not part of the witness

    *)
  2. flags : bool;
    (*

    The query has several conditions, each recorded by a flag of whether it has held, which a trail does not show

    *)
}

How the reachability conditions of a query are encoded in its property, which a trail of the query depends on

type check = {
  1. systems : system_check list;
  2. queries : (string * encoding) list;
}

The systems of a check-system command, one per group of its queries with the same assumptions and initiality condition, and the names of the queries with how each is encoded, in the order of the script. Each query is a property of the system of its group, named after the query.

val check_file : string -> (unit, error) Stdlib.result

Parse and type check the script in a file, without translating it

val moxi_name_of_uf : UfSymbol.t -> string option

The MoXI name of a function defined with define-fun, given the symbol it is translated to, which has a fresh name

val call_name : TransSys.t -> TransSys.instance -> string

The name of a subsystem call, given the caller and the instance of the call. Raises Failure if the call has no name, which every call kmoxi builds has.

val of_file : string -> (check list * string option, error) Stdlib.result

Parse, type check and translate the script in a file into the checks of its check-system commands, in the order of the script, and the logic set with set-logic, if any

val subsystems_of_checks : check list -> system_check list

The systems of checks