Struct ConstraintPoster

pub struct ConstraintPoster<'solver, ConstraintImpl> { /* private fields */ }

A structure which is responsible for adding the created Constraints to the Solver. For an example on how to use this, see crate::constraints.

Implementations

impl<'a, ConstraintImpl> ConstraintPoster<'a, ConstraintImpl>

pub fn with_tag(self, tag: NonZero<u32>) -> Self

Tag the constraint with an integer. This tag is used in the proof to identify which constraints trigger particular inferences.

impl<ConstraintImpl: Constraint> ConstraintPoster<'_, ConstraintImpl>

pub fn post(self) -> Result<(), ConstraintOperationError>

Add the Constraint to the Solver.

This method returns a ConstraintOperationError if the addition of the Constraint led to a root-level conflict.

pub fn implied_by( self, reification_literal: Literal, ) -> Result<(), ConstraintOperationError>

Add the half-reified version of the Constraint to the Solver; i.e. post the constraint r -> constraint where r is a reification literal.

This method returns a ConstraintOperationError if the addition of the Constraint led to a root-level conflict.

impl<ConstraintImpl: NegatableConstraint> ConstraintPoster<'_, ConstraintImpl>

pub fn reify( self, reification_literal: Literal, ) -> Result<(), ConstraintOperationError>

Add the reified version of the Constraint to the Solver; i.e. post the constraint r <-> constraint where r is a reification literal.

This method returns a ConstraintOperationError if the addition of the Constraint led to a root-level conflict.

Trait Implementations

impl<'solver, ConstraintImpl: Debug> Debug for ConstraintPoster<'solver, ConstraintImpl>

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

Formats the value using the given formatter.

impl<ConstraintImpl> Drop for ConstraintPoster<'_, ConstraintImpl>

fn drop(&mut self)

Executes the destructor for this type.