Semgus.Parser
2.1.0
See the version list below for details.
dotnet add package Semgus.Parser --version 2.1.0
NuGet\Install-Package Semgus.Parser -Version 2.1.0
<PackageReference Include="Semgus.Parser" Version="2.1.0" />
paket add Semgus.Parser --version 2.1.0
#r "nuget: Semgus.Parser, 2.1.0"
// Install Semgus.Parser as a Cake Addin
#addin nuget:?package=Semgus.Parser&version=2.1.0
// Install Semgus.Parser as a Cake Tool
#tool nuget:?package=Semgus.Parser&version=2.1.0
SemGuS Parser
A C# parsing library for SemGuS problems. We also provide a standalone tool for verifying and converting SemGuS files. Find the latest release and binaries on the Releases page.
Features
- Parses SemGuS problems from SMT-LIB2 source files
- Displays constrained Horn clauses (CHCs) and other problem data in a human-inspectable format
- Converts SMT-LIB2 SemGuS problems into JSON for consumption by other tools
- Allows programatic access via a C# API
Examples
To verify the syntax of a problem file and display details in a human-inspectable format, run:
semgus-parser <input.sem>
To convert a problem file to JSON, run:
semgus-parser --format json --mode batch --output <output.json> -- <input.sem>
Caveats and Considerations
This project is under active development and does not yet support all SMT-LIB2 features. The following theories are currently supported:
- Core
- Ints
- Strings (except regular expressions)
- Bit vectors
New additions:
- Indexed identifiers, e.g.
(_ move up)
- Bit vectors (partial support; only theory functions supported for now)
- Converting SyGuS problems to CHCs on the fly (beta)
- Declarative S-expression output format (beta). Use
--format sexpr
Unsupported SMT-LIB2 features include:
- Parametric sorts
- Theory functions annotated with
:left-assoc
,:right-assoc
,:chainable
, and:pairwise
. Certain Core functions currently have hard-coded versions of various arities. - Some terms, including
let
and arbitrarymatch
expressions (other than those used to define semantics in SemGuS)
The roadmap for next-up features includes:
- Arbitrary
let
andmatch
terms
If there is an unsupported feature that you would like added, drop us a line by submitting an issue (or commenting on an existing one). This will help us prioritize what to put on our roadmap.
Installation
To install the stand-alone parsing tool, find the binary for your operating system on the Releases page. Unzip it and put the semgus-parser
(or semgus-parser.exe
) in a convenient location. No other dependencies are required. You may have to mark it
executable on Linux and macOS; just run chmod a+x semgus-parser
in the folder with the binary.
If you have the .NET 6 SDK installed, the parsing tool can also be installed automatically through NuGet:
dotnet tool install --global Semgus.Parser.Tool
The C# parsing library is available in NuGet. Look for the Semgus.Parser
package.
Usage
semgus-parser [--format <format>] [--mode <mode>] [--output <filename>] -- <input.sem> ...
Passing -
as the input filename (or not supplying any filenames) makes the tool read from standard input.
Format Verification
Run the tool with a format of verify
to perform a syntax verification. In addition to syntax verification,
this format prints out the problem information, which can be checked for correctness. This output
format is not designed to be machine readable; use the JSON output format instead.
JSON Converter
The SemgusParser
project contains a utility that reads in a SemGuS file and produces JSON data representing
the problem, usable by other non-.NET tools that cannot directly link with this library.
Usage
semgus-parser --format json [--mode stream|batch] [--output <filename.json>] -- <input.sem> ...
Passing -
as the input filename (or not supplying any filenames) makes the tool read from standard input.
The two modes, stream
and batch
, alter the output format of this tool. In stream
mode (the default),
the output is a stream of newline-delimited JSON objects representing parsing events. This is suitable for
interactive mode, or when the output of this tool is being directly piped to the consuming process. In
batch
mode, the output is a JSON array, with each item in the array being a parsing event object. This format
is suitable for outputting to a file as a complete JSON datatype. Note that the event object format is identical
between these two modes; only the output structure differs.
In stream mode:
{ ...event 1... }
{ ...event 2... }
{ ...event 3... }
.
.
.
In batch mode:
[
{ ...event 1... },
{ ...event 2... },
{ ...event 3... },
.
.
.
]
Event object format
Each event object has two fields that denote what type of event it represents: $event
and $type
. The $event
field holds the name of the particular event. The $type
field denotes the general type of event: currently, either
semgus
, for a SemGuS-specific eventsmt
, for a general SMT-LIB2 eventmeta
, for metadata about the problem
meta
events
set-info
Holds general metadata about the problem. The <value>
is either a string, number, or list of values (which might be lists, strings, numbers, etc.).
{ "$event": "set-info", "$type": "meta", "keyword": "<key>", "value": <value> }
end-of-stream
Sent at the end of the event stream.
{ "$event": "end-of-stream", "$type": "meta" }
semgus
events
check-synth
Signals that the synthesizer should perform synthesis with the information provided in previous events.
{ "$event": "check-synth", "$type": "semgus" }
declare-term-type
Declares that a particular symbol will be used as a term type. Does not contain the actual term type definition.
{ "$event": "declare-term-type", "$type": "semgus", "name": "<term-type-name>" }
define-term-type
Defines a set of constructors for a term type. All term types referenced will have been previously declared by a declare-term-type
event.
{ "$event": "define-term-type", "$type": "semgus", "name": "<term-type-name>", "constructors": [ <constructors> ] }
Each constructor (a.k.a. operator) has the form:
{ "name": "<constructor-name>", "children": ["<term-type>", ...] }
Example:
{
"name": "E",
"constructors": [
{
"name": "$x", "children": []
},
{
"name": "$y", "children": []
},
{
"name": "$0", "children": []
},
{
"name": "$1", "children": []
},
{
"name": "$+", "children": ["E", "E"]
},
{
"name": "$ite", "children": ["B", "E", "E"]
}
],
"$event": "define-term-type",
"$type": "semgus"
}
chc
An individual constrained Horn clause generated by the problem.
{"head": <head-rel>, "bodyRelations":[<body-rels>...], "inputVariables":["<var>"...], "outputVariables":["<var>"...], "variables":["<var>"...],"constraint": <term>, "constructor": <constructor>,"$event":"chc","$type":"semgus"}
Where each semantic relation has the form:
{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]}
The constructor has the form:
{"name":"<name>","arguments":["<var>"...],"argumentSorts":["<sort>"...],"returnSort":"<sort>"}
Terms have the general form:
{ "$termType": "<type>", ... }
Term types include application
, exists
, forall
, and variable
. Literals are simply a literal string or number.
An example term:
{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"}
Example:
{"head":{"name":"E.Sem","signature":["E","Int","Int","Int"],"arguments":["et","x","y","r"]},"bodyRelations":[],"inputVariables":["x","y"],"outputVariables":["r"],"variables":["et","x","y","r"],"constraint":{"name":"=","returnSort":"Bool","argumentSorts":["Int","Int"],"arguments":[{"name":"r","sort":"Int","$termType":"variable"},{"name":"y","sort":"Int","$termType":"variable"}],"$termType":"application"},"constructor":{"name":"$y","arguments":[],"argumentSorts":[],"returnSort":"E"},"$event":"chc","$type":"semgus"}
constraint
A Boolean predicate term.
{ "$event": "constraint", "$type": "semgus", "constraint": <term> }
The term is defined as above.
synth-fun
Contains the name of the function to synthesize, as well as the concrete grammar being used.
{ "$event": "synth-fun", "$type": "semgus", "grammar": <grammar>, "name": "<name>", "termType": "<name>" }
The grammar object is defined as:
{ "nonTerminals": [ {"name": "<name>", "termType": "<name>"}, ...], "productions": [<production>...] }
Each production object is:
{ "instance": "<nt-name>", "operator": "<op-name>", "occurrences": ["<nt-name>"] }
Note that an occurrence will be null
if it is not a non-terminal in the operator constructor, i.e. a discovered constant.
Product | Versions Compatible and additional computed target framework versions. |
---|---|
.NET | net6.0 is compatible. net6.0-android was computed. net6.0-ios was computed. net6.0-maccatalyst was computed. net6.0-macos was computed. net6.0-tvos was computed. net6.0-windows was computed. net7.0 was computed. net7.0-android was computed. net7.0-ios was computed. net7.0-maccatalyst was computed. net7.0-macos was computed. net7.0-tvos was computed. net7.0-windows was computed. net8.0 was computed. net8.0-android was computed. net8.0-browser was computed. net8.0-ios was computed. net8.0-maccatalyst was computed. net8.0-macos was computed. net8.0-tvos was computed. net8.0-windows was computed. |
-
net6.0
- Microsoft.Extensions.Logging (>= 6.0.0)
- Microsoft.Extensions.Logging.Abstractions (>= 6.0.0)
- Semgus.Common (>= 2.1.0)
- Semgus.Sexpr (>= 2.1.0)
NuGet packages
This package is not used by any NuGet packages.
GitHub repositories
This package is not used by any popular GitHub repositories.
Version | Downloads | Last updated |
---|---|---|
2.6.0-preview3 | 67 | 3/24/2024 |
2.6.0-preview2 | 58 | 3/23/2024 |
2.6.0-preview1 | 70 | 3/12/2024 |
2.5.0 | 149 | 1/4/2024 |
2.5.0-preview1 | 95 | 8/22/2023 |
2.4.2-preview1 | 92 | 6/19/2023 |
2.4.1 | 172 | 5/1/2023 |
2.4.0 | 214 | 3/23/2023 |
2.4.0-preview1 | 118 | 3/6/2023 |
2.3.0 | 233 | 2/24/2023 |
2.3.0-preview2 | 119 | 2/21/2023 |
2.3.0-preview1 | 135 | 1/16/2023 |
2.2.0 | 398 | 9/26/2022 |
2.2.0-preview1 | 140 | 8/16/2022 |
2.1.1 | 400 | 7/21/2022 |
2.1.0 | 418 | 7/13/2022 |
2.1.0-preview2 | 149 | 5/30/2022 |
2.1.0-preview1 | 160 | 4/20/2022 |
2.0.0 | 433 | 4/12/2022 |
2.0.0-rc1 | 145 | 4/11/2022 |
2.0.0-alpha5 | 146 | 3/29/2022 |
2.0.0-alpha4 | 145 | 3/27/2022 |