Struct SyGuSProblem 

pub struct SyGuSProblem {
    pub function_name: String,
    pub arguments: Vec<(String, String)>,
    pub return_sort: String,
    pub grammar: CFG,
    pub constraint: String,
}

A SyGuS problem instance.

Fields

function_name: String

Name of the function to synthesise.

arguments: Vec<(String, String)>

Argument names and their sorts.

return_sort: String

Return sort.

grammar: CFG

Grammar constraining syntactic form.

constraint: String

Logical constraint (correctness spec).

Implementations

impl SyGuSProblem

pub fn new( function_name: impl Into<String>, arguments: Vec<(String, String)>, return_sort: impl Into<String>, grammar: CFG, constraint: impl Into<String>, ) -> Self

Build a SyGuS problem.

pub fn arity(&self) -> usize

Return the arity (number of arguments).

Trait Implementations

impl Clone for SyGuSProblem

fn clone(&self) -> SyGuSProblem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SyGuSProblem

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

Formats the value using the given formatter.