package syguslib-utils

  1. Overview
  2. Docs

Module Syguslib.ParserSource

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.

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.

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.

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.

Convert a s-expression into a feature Sygus.feature. Raises ParseError if the s-expression is not one of the predefined features.

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.

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

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.

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.

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.

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.

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.

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

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.

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.

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

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

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

OCaml

Innovation. Community. Security.