1 
// Subset rule for sets
2 
use conjure_cp::ast::Metadata;
3 
use conjure_cp::ast::{Expression as Expr, Moo, ReturnType, SymbolTable, Typeable};
4 
use conjure_cp::matrix_expr;
5 
use conjure_cp::rule_engine::Reduction;
6 
use conjure_cp::rule_engine::{
7 
    ApplicationError::RuleNotApplicable, ApplicationResult, register_rule,
8 
};
9 

            

        

            

                10
            

            

                
            

            

                
#[register_rule(("Base", 8700))]

            

        

            

                11
            

            

                
            

            

                
fn subset_to_subset_eq_neq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

            

        

            

                12
            

            

                
            

            

                
    match expr {

            

        

            

                13
            

            

                
            

            

                
        Expr::Subset(_, a, b)

            

        

            

                14
            

            

                
            

            

                
            if matches!(a.as_ref().return_type(), ReturnType::Set(_))

            

        

            

                15
            

            

                
            

            

                
                && matches!(b.as_ref().return_type(), ReturnType::Set(_)) =>

            

        

            

                16
            

            

                
            

            

                
        {

            

        

            

                17
            

            

                
            

            

                
            let expr1 = Expr::SubsetEq(Metadata::new(), a.clone(), b.clone());

            

        

            

                18
            

            

                
            

            

                
            let expr2 = Expr::Neq(Metadata::new(), a.clone(), b.clone());

            

        

            

                19
            

            

                
            

            

                
            Ok(Reduction::pure(Expr::And(

            

        

            

                20
            

            

                
            

            

                
                Metadata::new(),

            

        

            

                21
            

            

                
            

            

                
                Moo::new(matrix_expr![expr1, expr2]),

            

        

            

                22
            

            

                
            

            

                
            )))

            

        

            

                23
            

            

                
            

            

                
        }

            

        

            

                24
            

            

                
            

            

                
        _ => Err(RuleNotApplicable),

            

        

            

                25
            

            

                
            

            

                
    }

            

        

            

                26
            

            

                
            

            

                
}