Struct EqualsRule 

pub struct EqualsRule { /* private fields */ }

Check that there is a constraint in the database that is equal to the expected constraint.

Implementations

impl EqualsRule

pub fn new( constraint: PBConstraintEnum, hint: Option<isize>, add_result: bool, ) -> Self

pub fn parse( lex: Lexer<'_, RuleToken>, context: &mut Context, add_result: bool, ) -> Result<Self, ParserError>

Trait Implementations

impl Debug for EqualsRule

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

Formats the value using the given formatter.

impl Rule for EqualsRule

fn compute( &mut self, context: &mut Context, database: &mut Database, ) -> Result<Vec<Rc<DBConstraint>>, CheckingError>

Check the conditions for the rule and return the derived constraints.

fn get_returned_id(&self) -> Option<isize>

fn elaborate( &self, context: &mut Context, database: &Database, ) -> Result<(), ElaborationError>

Elaborate the proof rule to the kernel proof.

fn is_subproof_friendly(&self) -> bool

Returns true if the rule can be used within a subproof.

fn trace_rule(&self, lex: Lexer<'_, RuleToken>)

fn get_deleted<'a>( &'a self, _database: &Database, ) -> Result<Option<DeletionSequenceEnum<'a>>, CheckingError>

Return the ids of constraints deleted by the rule.

fn add_constraints_to_core(&self, _context: &Context) -> bool

Return true if resulting constraints are added to the core set instead of the derived set by default.

fn swaps_database(&self) -> bool

Returns true if the rule swaps out the currently considered database.

fn get_new_database(&mut self) -> (Database, PropagationEngine)

Get the new database to be swapped out.

fn handle_old_database( &mut self, _context: &mut Context, _database: Database, _prop_engine: PropagationEngine, )

Give the old database to the rule to handle it.