Struct Solutions

pub struct Solutions {
    cfg: Cfg,
    ctx: Context,
    solutions: Vec<(&'static Expr, Bits)>,
    solved_examples: Bits,
    pub threads: MappedFutures<Vec<usize>, JoinHandle<Expression>>,
    start_time: Instant,
    last_update: Instant,
    ite_limit: usize,
    tree_hole: Vec<Box<[u128]>>,
}

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

It integrates various components such as a configuration context, a collection of candidate solutions paired with evaluation bits, and management of concurrent solution search threads. Additionally, it tracks the synthesis start time, last update timestamp, an adaptive limit parameter, and a filtering structure (tree hole) used during example set generation and thread interruption.

Fields

cfg: Cfg

ctx: Context

solutions: Vec<(&'static Expr, Bits)>

solved_examples: Bits

threads: MappedFutures<Vec<usize>, JoinHandle<Expression>>

start_time: Instant

last_update: Instant

ite_limit: usize

tree_hole: Vec<Box<[u128]>>

Implementations

impl Solutions

pub fn new(cfg: Cfg, ctx: Context) -> Self

Creates a new instance with the provided configuration and context. This function initializes the internal condition tracker based on the context, ensuring that no previous tracker is present, and then sets up all the initial fields required for solution management and concurrent search execution, including a default tree hole, empty solution set, and mapped futures for thread management.

pub fn count(&self) -> usize

Counts the number of stored synthesis solutions.

Returns the total count of solution entries currently maintained within the internal collection.

pub fn add_new_solution(&mut self, expr: &'static Expr) -> Option<&'static Expr>

Adds a new candidate solution by evaluating an expression and updating the internal solution set accordingly.

The method first attempts to derive an evaluation result from the provided expression and then checks if this new result is subsumed by any existing solution; if so, it immediately returns without modification. Otherwise, it filters out any previously stored solutions that are redundant relative to the new one, updates the union of solved examples, and adds the new solution.

Continues by assessing whether the inclusive solved example set now covers all required cases, returning the expression if complete. In parallel, it iterates over the currently scheduled threads, aborting any whose example sets are fully encompassed by the new evaluation and triggering the launch of new threads. Finally, it leverages auxiliary mechanisms to generate a final solution if possible, or returns None if the candidate fails to yield a valid update.

pub fn generate_result(&self, limit: bool) -> Option<&'static Expr>

Determines and generates a synthesized result based on solved examples.

Checks whether the complete set of examples has been addressed; if so, it invokes a tree-learning procedure using a configurable operator limit depending on the provided flag and returns the synthesized solution expression. Otherwise, it returns none.

pub fn learn_tree(&self, ite_limit_rate: usize) -> Option<&'static Expr>

Learns a decision tree that synthesizes an expression using the current set of solutions and conditions, dynamically adjusting the iteration limit based on elapsed time and a provided rate parameter.

Computes an adaptive limit derived from the runtime duration and toggles a global condition tracker before invoking a tree learning procedure. Returns an expression reference if the tree learning process determines that a complete solution has been found, otherwise yields None.

pub fn check_cover(&self, example_set: &[usize]) -> bool

Checks whether any stored solution in the current context fully covers the specified example set.

This function iterates over all solutions and verifies if all indices in the provided example set are included in the corresponding coverage bitmask of any solution. It returns true as soon as a matching solution is found, and false otherwise.

pub fn generate_example_set(&mut self) -> Option<Vec<usize>>

Generates a new set of example indices for initiating a synthesis thread. This method iterates over potential subset sizes, calculating binomial coefficients to limit enumeration, and constructs candidate subsets based on configured conditions—either filtering through a predefined mask or generating all possible combinations.

It randomizes the order of these candidate subsets and validates each by ensuring that the example set is neither already covered by existing solutions nor in use by running threads. When a valid subset is found, it returns the set; otherwise, it yields None if no appropriate example set can be generated.

pub fn update_tree_hole(&mut self, tree_hole: Vec<Box<[u128]>>)

Updates the tree hole configuration for the current synthesis process while ensuring that threads no longer covered by the new configuration are aborted and replaced. This method assigns the new tree hole, iterates through the active thread example sets, verifies each against the updated tree hole using a helper function, and for any that fail the condition, it aborts the corresponding thread and promptly creates a replacement thread to preserve continuous progress in the synthesis search.

pub fn create_new_thread(&mut self)

Creates a new asynchronous thread to perform synthesis search using a generated example set. This function attempts to generate a candidate example set and, if successful, constructs a new context augmented with these examples to spawn an additional thread executing the synthesis process; otherwise, it logs that no example set is available.

pub fn create_all_search_thread(&mut self)

Creates and registers an asynchronous thread that performs exhaustive search over all examples from the current context.

This function gathers every example index by iterating from 0 to the context’s length, clones the current configuration and context, and then spawns a new search thread using those values. The resulting thread is inserted into the solutions’ thread registry, initiating a comprehensive condition search for viable synthesis solutions.

pub async fn solve_loop(&mut self) -> &'static Expr

Continuously polls and adapts the synthesis process until a valid expression covering all examples is discovered.

This asynchronous loop concurrently listens for solutions generated by worker threads and performs periodic adaptive adjustments. It evaluates incoming candidate expressions, updates and manages the set of current solutions, and dynamically modifies search parameters using time-based adjustments. When a complete solution is identified, it aborts remaining threads and returns the synthesized expression.