package syguslib-utils

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module `Syguslib.Semantic`Source

This module defines a few high-level properties of SyGuS programs. Setter commands and some utility functions on solver responses are specified here.

Sourceval is_setter_command : Sygus.command -> bool

Returns true when the command is a setter command, that is, sets some option. logic, or feature for the solver.

Sourceval is_well_formed : Sygus.program -> bool

Returns true if the program is well-formed. A well-formed program has the form (set-logic ..)(setter-command ..)*(other-commands..)*

Sourceval declares : Sygus.command -> string list

Returns the list of symbols declared by a command, in no particular order

Sourceval compare_declares : Sygus.command -> Sygus.command -> int

Compare two commands by the symbols they declare.

Sourceval max_definition : Sygus.command

A static definition for the max operation.

Sourceval min_definition : Sygus.command

A static definition for the min operation.

Sourceval rename : (string * string) list -> Sygus.sygus_term -> Sygus.sygus_term

A transformation function that renames all variables in a sygus term.

Sourceval write_command : out_channel -> Sygus.command -> unit

Writes a command to an output channel.

Sourcemodule Command : sig ... end

Sourcemodule Term : sig ... end

Sourcemodule Ident : sig ... end

Sourcemodule Lit : sig ... end

Sourcemodule Sort : sig ... end