Module solutions

Acumulative case-splitting solutions.

Structs

ConditionTracker

A structure for tracking condition evaluations within a given context.

Solutions

A structure encapsulating the state and configuration for managing synthesis solutions along with multi-threaded search execution.

Statics

CONDITIONS

A global static mutex-protected container for optionally holding condition tracking data.

Functions

bicoeff

Calculate the binomial coefficient for the given parameters.

cond_search_thread

Enables a condition search thread by modifying the configuration and initiating a new asynchronous synthesis search. This function activates condition search mode by setting the corresponding flag in the configuration, then delegates thread creation to a helper that starts the synthesis process, ultimately returning a join handle for the resulting expression.

new_thread

Creates a new asynchronous task that executes a synthesis search using the provided configuration and evaluation context.

new_thread_with_limit

Spawns an asynchronous task that executes a limited search procedure and returns its corresponding expression.

test_tree_hole_contains

Returns a boolean indicating whether one or more “tree holes” fully satisfy the provided set of indices. The function iterates over each element in the given collection and checks if every index in the provided slice corresponds to a value of 1 in that element, thereby determining if the set of indices is entirely contained within any of the elements.