Page
Library
Module
Module type
Parameter
Class
Class type
Source
Syguslib.Parser
SourceThis module defines function to convert from s-expressions to sygus.
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.
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.
Parse a file using the s-epxression based parser.
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.
Convert a list of s-expressions into a prgram, which is a list of commands. Raises ParseError
if parsing one of the commands fails.
Translate a s-expression returned by a solver to a Sygus.solver_response
.
Convert a s-expression into a symbol. Raises ParseError
if the s-expression is not a atom.
Convert a s-expression into a feature Sygus.feature
. Raises ParseError
if the s-expression is not one of the predefined features.
Convert a s-expression into an index. Sygus.index
. Raises ParseError
if the s-expression is not an index.
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).
Convert a s-expression into a sort Sygus.sygus_sort
. Raises ParseError
if the s-expression is not a valid sort.
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.
Convert a string into a literal Sygus.literal
. Raises ParseError
if the s-expression is not a 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.
Convert a s-expression into a term Sygus.sygus_term
. Raises ParseError
if the s-expression is not a term.
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).
Convert a s-expression into a sort declaration Sygus.sygus_sort_decl
.
Convert a s-expression into a datatype constructor declaration Sygus.dt_cons_dec
.
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.
Convert a s-expression into a grammar definition.