Module Problem

module Problem: sig .. end

Top-Level Statements (with locations)

type metadata = ProblemMetadata.t

type loc = Location.t

type id = ID.t

type 'a printer = Format.formatter -> 'a -> unit

type 'a to_sexp = 'a -> Sexp_lib.t

type 'a or_error = ('a, string) CCResult.t

Problem: a Set of Statements + Signature

type ('t, 'ty) t = private {

	`statements : ('t, 'ty) Statement.t CCVector.ro_vector;`
	`metadata : metadata;`

}

val make : meta:metadata ->
       ('t, 'ty) Statement.t CCVector.ro_vector -> ('t, 'ty) t

Build a problem from statements

val of_list : meta:metadata -> ('t, 'ty) Statement.t list -> ('t, 'ty) t

val statements : ('t, 'ty) t -> ('t, 'ty) Statement.t CCVector.ro_vector

val metadata : ('a, 'b) t -> metadata

val update_meta : ('t, 'ty) t ->
       (metadata -> metadata) -> ('t, 'ty) t

val add_sat_means_unknown : bool -> ('t, 'ty) t -> ('t, 'ty) t

val set_sat_means_unknown : ('t, 'ty) t -> ('t, 'ty) t

val add_unsat_means_unknown : bool -> ('t, 'ty) t -> ('t, 'ty) t

val set_unsat_means_unknown : ('t, 'ty) t -> ('t, 'ty) t

val iter_statements : f:(('t, 'ty) Statement.t -> unit) -> ('t, 'ty) t -> unit

val map_statements : f:(('t, 'ty) Statement.t -> ('t2, 'ty2) Statement.t) ->
       ('t, 'ty) t -> ('t2, 'ty2) t

val fold_map_statements : f:('acc -> ('t, 'ty) Statement.t -> 'acc * ('t2, 'ty2) Statement.t) ->
       x:'acc -> ('t, 'ty) t -> 'acc * ('t2, 'ty2) t

val flat_map_statements : f:(('t, 'ty) Statement.t -> ('t2, 'ty2) Statement.t list) ->
       ('t, 'ty) t -> ('t2, 'ty2) t

Map each statement to a list of statements, and flatten the result into a new problem

val map : term:('a -> 'b) ->
       ty:('tya -> 'tyb) -> ('a, 'tya) t -> ('b, 'tyb) t

val map_with : ?before:(unit -> ('b, 'tyb) Statement.t list) ->
       ?after:(unit -> ('b, 'tyb) Statement.t list) ->
       term:('a -> 'b) ->
       ty:('tya -> 'tyb) -> ('a, 'tya) t -> ('b, 'tyb) t

map_with ~add ~term ~ty pb is similar to map ~term ~ty pb, but after processing each statement st, after () and before() are called, and the statements they return are added respectively before or after the translation of st.

module Print (P1 : TermInner.PRINT)  (P2 : TermInner.PRINT) : sig .. end

Printer for a problem

module Convert (T1 : TermInner.REPR)  (T2 : TermInner.BUILD) : sig .. end

Convert the term representations

exception IllFormed of string

Ill-formed problem

val goal : ('t, 'a) t -> 't

goal pb returns the unique goal of pb, or fails. A problem that doesn't have a single goal is ill-formed
Raises IllFormed if the problem doesn't have exactly one goal

val signature : ?init:'ty Signature.t -> ('a, 'ty) t -> 'ty Signature.t

Gather the signature of every declared symbol
Raises IllFormed if some symbol is declared twice

init : initial signature, if any

val env : ?init:('t, 'ty) Env.t -> ('t, 'ty) t -> ('t, 'ty) Env.t

Build an environment defining/declaring every symbol of the problem.
Raises IllFormed if some declarations/definitions do not agree

init : initial env, if any

Result

module Res: sig .. end