Crate synthphonia

Source

Modules§

backward
Backward Deducer
expr
Representing Expression
forward
Forward enumerator
galloc
Global allocation
log
Logging
parser
SyGuS-IF parsing
solutions
Acumulative case-splitting solutions.
text
Handle special text objects.
tree_learning
Decision Tree Learning
utils
Utility functions
value
Representing Value

Macros§

async_clone
Creates an asynchronous block that clones a collection of variables before evaluating a given expression.
async_closure
Generates an asynchronous closure that rebinding the provided expressions and evaluates a given expression within the async context. This macro takes a list of expressions to be rebound using a helper rebinding macro, then returns an async move block that evaluates the specified expression while capturing the rebound variables.
closure
Creates a closure-like block that performs variable rebinding before evaluating an expression. This macro takes a comma-separated list of identifier pairs, where each pair specifies a rebinding using a helper mechanism, and a trailing expression; it expands to a block that first applies the rebinding operations and then evaluates the provided expression within that modified scope.
const_value
This macro converts literal values into constant representations based on their type.
crit
Logs critical messages based on the defined logging level.
debg
A macro for custom debug logging.
debg2
Expands to produce a debug logging statement for high verbosity levels.
debgb
Expands into a conditional logging block for debugging expressions.
debgb2
Expands to a logging and evaluation mechanism.
default_value
Expands to provide a default value for various data types.
expr
Macro to create of expressions in the Synthphonia module.
expr_no_use
for_all_formatting_op
for_all_op1
Defines a macro that generates a sequence of unary operations for expressions in the synthesis framework.
for_all_op2
Expands to include a sequence of binary (two-operand) operations as part of the Expr Ops sub-module.
for_all_op3
Defines a macro that expands to include a set of three-element operations used within the expression handling of string synthesis tasks.
impl_basic
Defines a macro for creating structures with basic functionality.
impl_formatop
impl_name
Defines a macro that automates the implementation of several traits for a given type.
impl_op1
Implements a macro to define unary operations for expression types.
impl_op2
This macro facilitates the implementation of the Op2 trait for a given struct, allowing it to define binary operations on values.
impl_op3
Defines a macro for implementing a ternary operation trait.
impl_op1_opt
Defines a macro to implement the Op1 trait for a given type, focusing on optional transformations.
impl_op2_opt
Defines a macro for implementing a two-operand operation trait with optional evaluation.
impl_op3_opt
A macro for implementing ternary operations with optional characteristics.
info
Expands a logging macro for outputting informational messages.
infob
Evaluates a given expression with conditional logging of informational messages based on the current log level.
never
Generates an asynchronous expression that yields a future which never resolves. This macro conditionally produces a pending future, either using the default type or a specified type parameter, blocking execution indefinitely when awaited.
new_op1
Defines a macro to simplify the creation and implementation of unary operations in the synthesis framework.
new_op2
Defines a macro for creating new binary operations within the expression framework.
new_op3
Creates a new ternary operation macro for use within the string synthesis framework.
new_op1_opt
Defines a macro for creating a new unary operation.
new_op2_opt
This macro facilitates the creation of a new binary operation with optional behavior.
new_op3_opt
Defines a macro that simplifies the creation and implementation of three-input (ternary) operations with optional functionality.
rebinding
Provides utility for rebinding a variable with different semantics. This macro accepts a pattern specifying the rebinding mode—ref, clone, move, or mut—followed by an identifier, and expands it into a let binding that creates a new binding corresponding to that mode (borrowing immutably, cloning, moving, or borrowing mutably).
warn
This macro generates a warning message.

Structs§

Cli 🔒
A command-line interface configuration providing options for controlling a string synthesis process.

Statics§

COUNTER
no longer used
DEBUG
No longer used

Functions§

enrich_configuration 🔒
Enhances the given configuration by integrating it with a parsed problem derived from the provided SyGuS-IF string.
main 🔒
Executes the main asynchronous function for processing string synthesis problems using a command-line interface.