package syguslib-utils

  1. Overview
  2. Docs

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.

Main entry points

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.

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

Useful auxiliary functions.

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.

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.

Convert a s-expression into a grammar description.

Convert a s-expression into a grammar definition.

OCaml

Innovation. Community. Security.