Lowering

Trait Lowering 

Source
pub trait Lowering: ExprLowering {
    // Required methods
    fn generate_constraint(
        &self,
        op: CmpOp,
        lhs: &Self::CellOutput,
        rhs: &Self::CellOutput,
    ) -> Result<()>;
    fn num_constraints(&self) -> usize;
    fn generate_comment(&self, s: String) -> Result<()>;
    fn generate_assume_deterministic(&self, slot: Slot) -> Result<()>;
    fn generate_call(
        &self,
        name: &str,
        selectors: &[Self::CellOutput],
        outputs: &[Slot],
    ) -> Result<()>;
    fn generate_assert(&self, expr: &Self::CellOutput) -> Result<()>;
    fn generate_post_condition(&self, expr: &Self::CellOutput) -> Result<()>;

    // Provided method
    fn checked_generate_constraint(
        &self,
        op: CmpOp,
        lhs: &Self::CellOutput,
        rhs: &Self::CellOutput,
    ) -> Result<()> { ... }
}
Expand description

Defines the interface code generators expose for generating code in their corresponding IR.

Required Methods§

Source

fn generate_constraint( &self, op: CmpOp, lhs: &Self::CellOutput, rhs: &Self::CellOutput, ) -> Result<()>

Generates a constraint.

Source

fn num_constraints(&self) -> usize

Returns the number of generated constraints.

Source

fn generate_comment(&self, s: String) -> Result<()>

Generates IR representing a comment with the given text.

Source

fn generate_assume_deterministic(&self, slot: Slot) -> Result<()>

Generates an statement that hints that the given Slot must be assumed to be deterministic.

Source

fn generate_call( &self, name: &str, selectors: &[Self::CellOutput], outputs: &[Slot], ) -> Result<()>

Generates a call to another group.

Source

fn generate_assert(&self, expr: &Self::CellOutput) -> Result<()>

Generates an assertion using the given expression.

How exactly this assertion is represented is backend dependant.

Source

fn generate_post_condition(&self, expr: &Self::CellOutput) -> Result<()>

Generates an assertion using the given expression that is treated as a post-condition.

How exactly this assertion is represented is backend dependant.

Provided Methods§

Source

fn checked_generate_constraint( &self, op: CmpOp, lhs: &Self::CellOutput, rhs: &Self::CellOutput, ) -> Result<()>

Attempts to generate a constraint and fails if it couldn’t be generated.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§