Struct MWSynthGoal 

pub struct MWSynthGoal {
    pub pre: String,
    pub post: String,
    pub output_var: String,
    pub subgoals: Vec<MWSynthGoal>,
}

A Manna–Waldinger synthesis goal: (precondition, postcondition, output variable).

Fields

pre: String

The precondition predicate.

post: String

The postcondition predicate relating inputs and output.

output_var: String

The output variable name.

subgoals: Vec<MWSynthGoal>

Sub-goals generated by applying a rule.

Implementations

impl MWSynthGoal

pub fn leaf( pre: impl Into<String>, post: impl Into<String>, output_var: impl Into<String>, ) -> Self

Create a leaf synthesis goal.

use oxilean_std::program_synthesis::MWSynthGoal;
let g = MWSynthGoal::leaf("true", "y = x + 1", "y");
assert!(g.subgoals.is_empty());

pub fn with_subgoals( pre: impl Into<String>, post: impl Into<String>, output_var: impl Into<String>, subgoals: Vec<MWSynthGoal>, ) -> Self

Create a goal with sub-goals (internal node).

pub fn depth(&self) -> usize

Depth of the goal tree.

pub fn is_leaf(&self) -> bool

Check whether this is an atomic (leaf) goal.

Trait Implementations

impl Clone for MWSynthGoal

fn clone(&self) -> MWSynthGoal

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for MWSynthGoal

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for MWSynthGoal

fn eq(&self, other: &MWSynthGoal) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for MWSynthGoal

impl StructuralPartialEq for MWSynthGoal