Module `Syguslib.Parser`Source

This module defines function to convert from s-expressions to sygus.

Sourceexception 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.

Sourceexception 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.

Main entry points

Sourceval sexp_parse : Base.string -> Sygus.program

Parse a file using the s-epxression based parser.

raises ParseError

Sourceval 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.

raises ParseError

raises NonConforming

Sourceval 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.

raises ParseError

raises NonConforming

Sourceval reponse_of_sexps : Sexplib.Sexp.t Base.list -> Sygus.solver_response

Translate a s-expression returned by a solver to a Sygus.solver_response.

Useful auxiliary functions.

Sourceval 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.

raises ParseError

Source

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.

raises ParseError

Sourceval 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.

raises ParseError

Sourceval 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).

raises ParseError

Sourceval 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.

raises ParseError

Sourceval 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.

raises ParseError

Sourceval 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.

raises ParseError

Sourceval 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.

raises ParseError

Sourceval 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.

raises ParseError

Sourceval 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).

raises ParseError

Sourceval sygus_sort_decl_of_sexp : Sexplib.Sexp.t -> Sygus.sygus_sort_decl

Convert a s-expression into a sort declaration Sygus.sygus_sort_decl.

raises ParseError

Sourceval 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.

raises ParseError

Sourceval sygus_gsterm_of_sexp : Sexplib.Sexp.t -> Sygus.sygus_gsterm

Convert a s-expression into a grammar term Sygus.sygus_gsterm.

raises ParseError

Source

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.

raises ParseError

Source

val grammar_def_of_sexps : 
  Sexplib.Sexp.t Base.option ->
  Sexplib.Sexp.t ->
  Sygus.grammar_def

Convert a s-expression into a grammar definition.

raises ParseError

package syguslib-utils

Module Syguslib.ParserSource

Main entry points

Useful auxiliary functions.

Module `Syguslib.Parser`Source