1 
use crate::shared::lex::{lex_elements_to_recursive_or, lex_operand_elements};
2 
use conjure_cp::ast::{Expression as Expr, SymbolTable};
3 
use conjure_cp::rule_engine::{
4 
    ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect, register_rule,
5 
};
6 

            

        

            

                7
            

            

                
            

            

                
/// Expand scalar lexicographic comparisons for library-backed solver relations.

            

        

            

                8
            

            

                
            

            

                
#[register_rule("Smt", 2001, [LexLt, LexLeq])]

            

        

            

                9
            

            

                554
            

            

                
pub(crate) fn expand_lex_lt_leq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

            

        

            

                10
            

            

                554
            

            

                
    let (lhs, rhs) = match expr {

            

        

            

                11
            

            

                533
            

            

                
        Expr::LexLt(_, lhs, rhs) | Expr::LexLeq(_, lhs, rhs) => (lhs, rhs),

            

        

            

                12
            

            

                21
            

            

                
        _ => return Err(RuleNotApplicable),

            

        

            

                13
            

            

                
            

            

                
    };

            

        

            

                14
            

            

                
            

            

                

            

        

            

                15
            

            

                533
            

            

                
    let lhs_elements = lex_operand_elements(lhs)?;

            

        

            

                16
            

            

                533
            

            

                
    let rhs_elements = lex_operand_elements(rhs)?;

            

        

            

                17
            

            

                533
            

            

                
    let allow_equality = matches!(expr, Expr::LexLeq(..));

            

        

            

                18
            

            

                
            

            

                

            

        

            

                19
            

            

                533
            

            

                
    Ok(RuleEffect::pure(lex_elements_to_recursive_or(

            

        

            

                20
            

            

                533
            

            

                
        &lhs_elements,

            

        

            

                21
            

            

                533
            

            

                
        &rhs_elements,

            

        

            

                22
            

            

                533
            

            

                
        allow_equality,

            

        

            

                23
            

            

                533
            

            

                
    )))

            

        

            

                24
            

            

                554
            

            

                
}

            

        

            

                25
            

            

                
            

            

                

            

        

            

                26
            

            

                
            

            

                
#[cfg(test)]

            

        

            

                27
            

            

                
            

            

                
mod tests {

            

        

            

                28
            

            

                
            

            

                
    use super::*;

            

        

            

                29
            

            

                
            

            

                
    use conjure_cp::ast::{Metadata, Moo};

            

        

            

                30
            

            

                
            

            

                
    use conjure_cp::matrix_expr;

            

        

            

                31
            

            

                
            

            

                

            

        

            

                32
            

            

                
            

            

                
    #[test]

            

        

            

                33
            

            

                1
            

            

                
    fn expands_explicit_lists_even_when_element_domains_are_unavailable() {

            

        

            

                34
            

            

                1
            

            

                
        let lhs = matrix_expr![

            

        

            

                35
            

            

                1
            

            

                
            Expr::Metavar(Metadata::new(), "a".into()),

            

        

            

                36
            

            

                1
            

            

                
            Expr::Metavar(Metadata::new(), "b".into())

            

        

            

                37
            

            

                
            

            

                
        ];

            

        

            

                38
            

            

                1
            

            

                
        let rhs = matrix_expr![

            

        

            

                39
            

            

                1
            

            

                
            Expr::Metavar(Metadata::new(), "c".into()),

            

        

            

                40
            

            

                1
            

            

                
            Expr::Metavar(Metadata::new(), "d".into())

            

        

            

                41
            

            

                
            

            

                
        ];

            

        

            

                42
            

            

                1
            

            

                
        assert!(lhs.domain_of().is_none());

            

        

            

                43
            

            

                1
            

            

                
        assert!(rhs.domain_of().is_none());

            

        

            

                44
            

            

                
            

            

                

            

        

            

                45
            

            

                1
            

            

                
        let comparison = Expr::LexLeq(Metadata::new(), Moo::new(lhs), Moo::new(rhs));

            

        

            

                46
            

            

                1
            

            

                
        let result = expand_lex_lt_leq(&comparison, &SymbolTable::new())

            

        

            

                47
            

            

                1
            

            

                
            .expect("explicit list order is enough to expand lex");

            

        

            

                48
            

            

                
            

            

                

            

        

            

                49
            

            

                1
            

            

                
        assert!(!matches!(result.new_expression, Expr::LexLeq(..)));

            

        

            

                50
            

            

                1
            

            

                
    }

            

        

            

                51
            

            

                
            

            

                
}