Struct Executor

pub struct Executor {

    pub ctx: Context,
    pub cfg: Cfg,
    pub deducers: Vec<DeducerEnum>,
    pub data: Vec<Data>,
    pub counter: Cell<usize>,
    pub subproblem_count: Cell<usize>,
    pub cur_size: Cell<usize>,
    pub cur_nt: Cell<usize>,
    pub waiting_tasks: UnsafeCell<TaskWaitingCost>,
    pub top_task: UnsafeCell<JoinHandle<&'static Expr>>,
    expr_collector: UnsafeCell<Vec<EV>>,
    pub bridge: Bridge,
    pub start_time: Instant,
}

A structure representing an executor for managing and coordinating the synthesis process.

This structure encapsulates various fields required to execute synthesis tasks effectively, such as tracking state and managing data flow.

Usage:

let exec = Executor::new(ctx, cfg);
let result = exec.solve_top_blocked();
let result = DefineFun { sig: problem.synthfun().sig.clone(), expr: result};

Fields

ctx: Context

cfg: Cfg

deducers: Vec<DeducerEnum>

All deducers used in the executor.

data: Vec<Data>

Term Dispatcher data structures

counter: Cell<usize>

A counter for the number of expressions enumerated.

subproblem_count: Cell<usize>

A counter for the number of subproblems processed.

cur_size: Cell<usize>

The current size of the expression being processed.

cur_nt: Cell<usize>

The current non-terminal index being processed.

waiting_tasks: UnsafeCell<TaskWaitingCost>

No longer used Queue of tasks waiting for cost limit to be released.

top_task: UnsafeCell<JoinHandle<&'static Expr>>

Top task to be executed.

expr_collector: UnsafeCell<Vec<EV>>

bridge: Bridge

Bridge to interact with other threads

start_time: Instant

Timestamp when the executor started.

Implementations

impl Executor

pub fn problem_count(&self) -> usize

Retrieves the count of subproblems processed by the executor.

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

Creates a new instance.

pub fn top_task(&self) -> &mut JoinHandle<&'static Expr>

pub fn collect_expr(&self, e: &'static Expr, v: Value)

Collects expressions and their associated values. Save them into the expr_collector field.

pub fn waiting_tasks(&self) -> &mut TaskWaitingCost

Returns a mutable reference to the field waiting_tasks.

pub fn extract_expr_collector(&self) -> Vec<EV>

Extracts the contents of the expr_collector and returns them as a Vec<EV>.

pub fn cur_data(&self) -> &Data

Provides a method to access the current data entry from the data vector within the Executor context.

pub async fn solve_task(&'static self, problem: Problem) -> &'static Expr

Solves a given synthesis problem asynchronously and returns a reference to an expression.

pub async fn generate_condition( &'static self, problem: Problem, result: &'static Expr, ) -> &'static Expr

Asynchronously generates a conditional expression for a given problem and result.

pub fn solve_top_blocked(self) -> &'static Expr

Attempts to solve the top-level problem and manage its execution.

pub fn solve_top_with_limit(self) -> Option<&'static Expr>

Attempts to solve the top problem with a limit within the Executor.

pub fn size(&self) -> usize

Retrieves the current size of the executor.

pub fn nt(&self) -> usize

Retrieves the current non-terminal index from the executor.

pub fn count(&self) -> usize

Returns the current value of the counter field.

pub fn enum_expr(&'static self, e: Expr, v: Value) -> Result<(), ()>

Handle when a new express is enumerated.

fn collect_condition(&'static self, e: &Expr)

Collects and inserts an expression into a shared collection of conditions CONDITIONS

fn run(&'static self) -> Result<(), ()>

Start Enumeration