Trait NegatableConstraint 

pub trait NegatableConstraint: Constraint {
    type NegatedConstraint: NegatableConstraint + 'static;

    // Required method
    fn negation(&self) -> Self::NegatedConstraint;

    // Provided method
    fn reify(
        self,
        solver: &mut Solver,
        reification_literal: Literal,
    ) -> Result<(), ConstraintOperationError>
       where Self: Sized { ... }
}

A Constraint which has a well-defined negation.

Having a negation means the Constraint can be fully reified; i.e., a constraint C can be turned into r <-> C where r is a reification literal.

For example, the negation of the Constraint a = b is (well-)defined as a != b.

Required Associated Types

type NegatedConstraint: NegatableConstraint + 'static

Required Methods

fn negation(&self) -> Self::NegatedConstraint

Provided Methods

fn reify( self, solver: &mut Solver, reification_literal: Literal, ) -> Result<(), ConstraintOperationError>

where Self: Sized,

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.

The tag allows inferences to be traced to the constraint that implies them. They will show up in the proof log.

Implementors