Module `Syguslib.Sygus`Source

This module contains definitions that mirror the SyGuS Language Standard Version 2.1, which can be found at https://sygus.org/assets/pdf/SyGuS-IF_2.1.pdf.

Types

Sourceval use_v1 : bool ref

Set to true in order to use SyGuS language v1.

Sourcetype symbol = string

Symbols are just strings.

Sourcetype attribute =

| Attr of symbol
| AttrVal of symbol * string

Sourcetype literal =

| LitNum of int
(*
A numeral literal, which is either the digit 0 or a non-empty sequence of digits that does not being with 0.
*)
| LitDec of float
(*
A decimal number literal, which is syntactically <numeral>.0*<numeral>.
*)
| LitBool of bool
(*
A boolean literal is either true or false.
*)
| LitHex of symbol
(*
A hexadecimal is written with #x followed by a non empty sequence of characters A-F and 0-9
*)
| LitBin of bool list
(*
A hexadecimal is written with #b followed by a non empty sequence of bits
*)
| LitString of symbol
(*
A string literal is any sequence of printable characters delimited by double quotes.
*)

SyGuS literals.

Sourcetype index =

| INum of int
| ISym of symbol

Sourcetype identifier =

| IdSimple of symbol
(*
A simple identifier is a symbol.
*)
| IdIndexed of symbol * index list
(*
An indexed identifier is (_ <symbol> <identifier>)
*)
| IdQual of symbol * sygus_sort
(*
A qualified identifier is (as <symbol> <sort>)
*)

An identifier can be simple, indexed or qualified.

Sourceand sygus_sort =

| SId of identifier
(*
A simple sort with an identifier.
*)
| SApp of identifier * sygus_sort list
(*
A sort applied to arguments.
*)

A sort is either its id, or a sort applied to other sort (polymorphism)

Sourcetype sygus_term =

| SyId of identifier
| SyLit of literal
(*
A literal.
*)
| SyApp of identifier * sygus_term list
(*
A function application.
*)
| SyExists of sorted_var list * sygus_term
(*
An existential quantifier.
*)
| SyForall of sorted_var list * sygus_term
(*
A universal quantifier.
*)
| SyLet of binding list * sygus_term
(*
A let-binding.
*)

The type for sygus terms.

Sourceand sorted_var = symbol * sygus_sort

Sourceand binding = symbol * sygus_term

Sourcetype feature =

| FGrammar
| FFwdDecls
| FRecursion
| FOracles
| FWeights

Sourcetype command =

| CCheckSynth
(*
The (check-synth) command for synthesis.
*)
| CAssume of sygus_term
(*
The assume command.
*)
| CConstraint of sygus_term
(*
The constraint command to define a constraint with a term.
*)
| CChcConstraint of sorted_var list * sygus_term * sygus_term
(*
A command for specifying CHC constraints.
*)
| CDeclareVar of symbol * sygus_sort
(*
The declare command to declare a universally quantified variable.
*)
| CDeclareWeight of symbol * attribute list
(*
Declaration of weight attributes.
*)
| CInvConstraint of symbol * symbol * symbol * symbol
(*
The inv-constraint command to constraint an invariant.
*)
| CSetFeature of feature * bool
(*
The set-feature command.
*)
| CSynthFun of symbol * sorted_var list * sygus_sort * grammar_def option
(*
The synth-fun command to declare a function to synthesize. The grammar is optional.
*)
| CSynthInv of symbol * sorted_var list * grammar_def option
(*
The synth-inv command is a shortcut for synth-fun when the function to be synthesized returns a boolean. It is printed as synth-fun ... Bool if use_v1 is false.
*)
| COptimizeSynth of sygus_term list * attribute list
(*
Command for specifying optimization queries.
*)
| CDeclareDataType of symbol * dt_cons_dec list
(*
A datatype declaration with a name and constructor list.
*)
| CDeclareDataTypes of sygus_sort_decl list * dt_cons_dec list list
(*
A declaration for mutually recursive data types.
*)
| CDeclareSort of symbol * int
(*
A sort declaration
*)
| CDefineFun of symbol * sorted_var list * sygus_sort * sygus_term
(*
A function definition.
*)
| CDefineSort of symbol * sygus_sort
(*
A sort definition (renaming).
*)
| CSetInfo of symbol * literal
(*
Setting some solver option.
*)
| CSetLogic of symbol
(*
Setting the logic used.
*)
| CSetOption of symbol * literal
(*
Setting some solver option.
*)
| COracle of oracle_command
(*
All the oracle commands are grouped under COracle.
*)

The SyGuS commands

Sourceand oracle_command =

| OAssume of sorted_var list * sorted_var list * sygus_term * symbol
(*
Asert an oracle assumption.
*)
| OConstraint of sorted_var list * sorted_var list * sygus_term * symbol
(*
Assert and oracle constraint.
*)
| ODeclareFun of symbol * sygus_sort list * sygus_sort * symbol
(*
Declare an oracle functional symbol.
*)
| OConstraintIO of symbol * symbol
(*
Declare an input-output oracle.
*)
| OConstraintCex of symbol * symbol
(*
Declare a counterexample witness oracle.
*)
| OConstraintMem of symbol * symbol
(*
Declare a membership-query oracle.
*)
| OConstraintPosw of symbol * symbol
(*
Declare a positive witness oracle.
*)
| OConstraintNegw of symbol * symbol
(*
Declare a negative witness oracle.
*)
| OCorrectness of symbol * symbol
(*
Declare a correctness oracle.
*)
| OCorrectnessCex of symbol * symbol
(*
Declare a correctness oracle with counterexamples.
*)

A different type is used to separate the oracle commands.

Sourceand sygus_sort_decl = symbol * int

A sort declaration is a name with an integer index.

Sourceand dt_cons_dec = symbol * sorted_var list

A datatype constructor with a name and named arguments.

Sourceand grammar_def = (sorted_var * grouped_rule_list) list

A grammar definition is a list of non-terminals together with their production rule. In SyGuS v2, the definition is printed by first declaring the non-terminals and then printing the rules. The first symbol is always assumed to be the start symbol.

Sourceand grouped_rule_list = sygus_gsterm list

Sourceand sygus_gsterm =

| GConstant of sygus_sort
(*
A constant stands for any constant of a given sort.
*)
| GTerm of sygus_term
(*
A grammar term stands for a SyGuS term, which may contain non-terminals of the grammar.
*)
| GVar of sygus_sort
(*
A grammar var stands for any variable of a given sort.
*)

A grammar term in SyGuS.

Sourcetype program = command list

A program in SyGuS is a list of commands.

Sourceval special_chars : char list

The special characters that may not be used as identifiers (symbols).

Sourceval reserved_words : symbol list

A list of reserved symbols, that may not be used as symbols.

Sourceval digits : char list

Sourceval valid_ident : symbol -> bool

Returns true if the string is a valid identifier in SyGuS.

Sourceval has_standard_extension : string -> bool

Checks that a filename has the standard extension (.sl)

Sourceval char_to_bool : char -> bool

Solver specific types.

Sourcetype solver_response =

| RSuccess of (symbol * sorted_var list * sygus_sort * sygus_term) list
(*
A successful response comes with a list of implementations for the functions to synthesize.
*)
| RInfeasible
(*
A response indicating that the problem has no solution.
*)
| RFail
(*
A response indicating that the solver failed.
*)
| RUnknown
(*
A response indicating that the solver could not find a solution, with no guarantee about the feasibility of the problem.
*)

The types of responses a solver can give.

Sourceval is_sat : solver_response -> bool

Returns true is the solver response is successful.

Sourceval is_failed : solver_response -> bool

Returns true if the solver response indicates failure.

Sourceval is_infeasible : solver_response -> bool

Returns true if the solver response indicates the problem is is infeasible

package syguslib-utils

Module Syguslib.SygusSource

Types

Solver specific types.

Module `Syguslib.Sygus`Source