Library
Module
Module type
Parameter
Class
Class type
This module defines function to convert from s-expressions to sygus.
exception ParseError of Sexplib.Sexp.t * Base.string
An exception raised during the s-expression based parsing method. The s-expression should be the expression causing the exception to be raise, and the string is an informative message as to why parsing failed.
exception NonConforming of Sygus.command * Base.string
An exception raise during parsing when an input does not conform to the new v2.1 standard (e.g. and input of v1). This exception contains the command resulting from parsing the input.
val sexp_parse : Base.string -> Sygus.program
Parse a file using the s-epxression based parser.
val command_of_sexp : Sexplib.Sexp.t -> Sygus.command
Convert a s-expression into a command Sygus.command
. Raises ParseError
if the s-expression is not a command. Raises NonConforming
is the s-expression is not a SyGuS v2 command, byt may be a SyGuS v1 command.
val program_of_sexp_list : Sexplib.Sexp.t Base.list -> Sygus.program
Convert a list of s-expressions into a prgram, which is a list of commands. Raises ParseError
if parsing one of the commands fails.
val reponse_of_sexps : Sexplib.Sexp.t Base.list -> Sygus.solver_response
Translate a s-expression returned by a solver to a Sygus.solver_response
.
val symbol_of_sexp : Sexplib.Sexp.t -> Base.string
Convert a s-expression into a symbol. Raises ParseError
if the s-expression is not a atom.
val feature_of_sexp :
Sexplib.Sexp.t ->
(Sygus.feature, Base.string) Base.Result.t
Convert a s-expression into a feature Sygus.feature
. Raises ParseError
if the s-expression is not one of the predefined features.
val index_of_sexp : Sexplib.Sexp.t -> Sygus.index
Convert a s-expression into an index. Sygus.index
. Raises ParseError
if the s-expression is not an index.
val identifier_of_sexp : Sexplib.Sexp.t -> Sygus.identifier
Convert a s-expression into an identifier Sygus.identifier
. Raises ParseError
if the s-expression is not an identifier (either an indexed identifier or a simple identifier).
val sygus_sort_of_sexp : Sexplib.Sexp.t -> Sygus.sygus_sort
Convert a s-expression into a sort Sygus.sygus_sort
. Raises ParseError
if the s-expression is not a valid sort.
val sorted_var_of_sexp : Sexplib.Sexp.t -> Sygus.sorted_var
Convert a s-expression into a sorted var Sygus.sorted_var
. Raises ParseError
if the s-expression is not a sorted var, which is a pair of a symbol and a sort.
val literal_of_string : Base.string -> Sygus.literal
Convert a string into a literal Sygus.literal
. Raises ParseError
if the s-expression is not a literal.
val literal_of_sexp : Sexplib.Sexp.t -> Sygus.literal
Convert a s-expression into a literal Sygus.feature
. Raises ParseError
if the s-expression is not an atom, and if the string in the atom is not a literal.
val sygus_term_of_sexp : Sexplib.Sexp.t -> Sygus.sygus_term
Convert a s-expression into a term Sygus.sygus_term
. Raises ParseError
if the s-expression is not a term.
val binding_of_sexp : Sexplib.Sexp.t -> Sygus.binding
Convert a s-expression into a binding Sygus.binding
. Raises ParseError
if the s-expression is not a pair of and identifier and a term (a binding).
val sygus_sort_decl_of_sexp : Sexplib.Sexp.t -> Sygus.sygus_sort_decl
Convert a s-expression into a sort declaration Sygus.sygus_sort_decl
.
val dt_cons_dec_of_sexp : Sexplib.Sexp.t -> Sygus.dt_cons_dec
Convert a s-expression into a datatype constructor declaration Sygus.dt_cons_dec
.
val sygus_gsterm_of_sexp : Sexplib.Sexp.t -> Sygus.sygus_gsterm
Convert a s-expression into a grammar term Sygus.sygus_gsterm
.
val pre_grouped_rule_of_sexp :
Sexplib0.Sexp.t ->
Base.string * Sygus.sygus_sort * Sygus.sygus_gsterm Base.list
Convert a s-expression into a grammar description.
val grammar_def_of_sexps :
Sexplib.Sexp.t Base.option ->
Sexplib.Sexp.t ->
Sygus.grammar_def
Convert a s-expression into a grammar definition.