package syguslib-utils

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Legend:
Library
Module
Module type
Parameter
Class
Class type

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

Semantic identity of commands

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

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

val declares : Sygus.command -> string list

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

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

Compare two commands by the symbols they declare.

val max_definition : Sygus.command

A static definition for the max operation.

val min_definition : Sygus.command

A static definition for the min operation.

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

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

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

Writes a command to an output channel.

module Command : sig ... end

module Term : sig ... end

module Ident : sig ... end

module Lit : sig ... end

module Sort : sig ... end