On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
package syguslib-utils
On This Page
Legend:
Library
Module
Module type
Parameter
Class
Class type
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.stringAn 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.stringAn 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.
Main entry points
val sexp_parse : Base.string -> Sygus.programParse a file using the s-epxression based parser.
val command_of_sexp : Sexplib.Sexp.t -> Sygus.commandConvert 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.programConvert 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_responseTranslate a s-expression returned by a solver to a Sygus.solver_response.
Useful auxiliary functions.
val symbol_of_sexp : Sexplib.Sexp.t -> Base.stringConvert 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.tConvert 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.indexConvert 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.identifierConvert 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_sortConvert 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_varConvert 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.literalConvert 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.literalConvert 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_termConvert 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.bindingConvert 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_declConvert a s-expression into a sort declaration Sygus.sygus_sort_decl.
val dt_cons_dec_of_sexp : Sexplib.Sexp.t -> Sygus.dt_cons_decConvert a s-expression into a datatype constructor declaration Sygus.dt_cons_dec.
val sygus_gsterm_of_sexp : Sexplib.Sexp.t -> Sygus.sygus_gstermConvert 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.listConvert a s-expression into a grammar description.
val grammar_def_of_sexps :
Sexplib.Sexp.t Base.option ->
Sexplib.Sexp.t ->
Sygus.grammar_defConvert a s-expression into a grammar definition.
On This Page