Struct ConstraintSynthEngine 

pub struct ConstraintSynthEngine {
    pub hard_constraints: Vec<String>,
    pub soft_constraints: Vec<(String, u32)>,
    pub template: Option<String>,
}

A constraint-based synthesis engine that encodes the problem as SMT.

Fields

hard_constraints: Vec<String>

Hard constraints that the synthesised program must satisfy.

soft_constraints: Vec<(String, u32)>

Soft constraints (ranked by weight).

template: Option<String>

The program template (sketch).

Implementations

impl ConstraintSynthEngine

pub fn new() -> Self

Create a new empty constraint synthesis engine.

pub fn add_hard(&mut self, constraint: impl Into<String>)

Add a hard constraint.

pub fn add_soft(&mut self, constraint: impl Into<String>, weight: u32)

Add a soft constraint with a weight.

pub fn set_template(&mut self, template: impl Into<String>)

Set the program template (sketch with holes).

pub fn num_constraints(&self) -> usize

Count total constraints.

pub fn encode_pbo(&self) -> String

Encode as a pseudo-Boolean optimisation problem (placeholder).

pub fn solve(&self) -> Option<String>

Attempt to synthesise a program satisfying all hard constraints. Returns the filled template or None if unsatisfiable.

Trait Implementations

impl Clone for ConstraintSynthEngine

fn clone(&self) -> ConstraintSynthEngine

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ConstraintSynthEngine

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

Formats the value using the given formatter.

impl Default for ConstraintSynthEngine

fn default() -> ConstraintSynthEngine

Returns the “default value” for a type.