Grcov report - lex.rs

1

//! Scalar lexicographic comparisons reuse numeric relation and Boolean decisions.

2

use crate::types::record::RecordComponents;

3

use crate::types::tuple::{TupleComponents, TuplePacked};

4

use conjure_cp::ast::{Atom, Expression, Metadata, Moo, SymbolTable};

5

use conjure_cp::rule_engine::{

6

    ApplicationError, ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect,

7

    register_rule,

8

};

9

10

/// The scalars a lex entry contributes: a represented tuple or record contributes its fields in

11

/// order, since its own ordering is lexicographic over them, and a packed tuple its single

12

/// order-preserving integer. Returns `None` for an entry that is already a single element.

13

102137

fn lex_entry_fields(entry: &Expression) -> Option<Vec<Expression>> {

14

102137

    let Expression::Atomic(_, Atom::Reference(reference)) = entry else {

15

69755

        return None;

16

};

17

32382

    let declaration = reference.ptr();

18

32382

    let fields = if let Some(repr) = declaration.get_repr::<TupleComponents>() {

19

5887

        repr.field_exprs()

20

26495

    } else if let Some(repr) = declaration.get_repr::<RecordComponents>() {

21

        repr.field_exprs()

22

    } else {

23

26495

        vec![declaration.get_repr::<TuplePacked>()?.packed_expr()]

24

};

25

    Some(

26

10297

        fields

27

10297

            .into_iter()

28

16184

            .flat_map(|field| lex_entry_fields(&field).unwrap_or_else(|| vec![field]))

29

            .collect(),

30

31

102137

32

33

771960

fn is_scalar(entry: &Expression) -> bool {

34

771960

    entry

35

771960

        .domain_of()

36

771960

        .is_some_and(|domain| domain.is_int() || domain.is_bool())

37

771960

38

39

/// Comparing `[t1, t2]` with `[u1, u2]` lexicographically equals comparing their fields

40

/// `[t1.a, t1.b, t2.a, t2.b]` with `[u1.a, u1.b, u2.a, u2.b]`: entries of one type have one width.

41

/// Runs after `tuple_var_cmp_var`, which already handles a comparison of single tuples.

42

#[register_rule("SAT", 9300, [LexLt, LexLeq])]

43

85057

fn splice_compound_lex_entries(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

44

85057

    let (lhs, rhs) = match expr {

45

85036

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

46

21

        _ => return Err(RuleNotApplicable),

47

};

48

85036

    let mut spliced = false;

49

90482

    let mut splice = |operand: &Expression| -> Result<Moo<Expression>, ApplicationError> {

50

90482

        let mut scalars = Vec::new();

51

90482

        for entry in super::counting::matrix_entries(operand).ok_or(RuleNotApplicable)? {

52

85953

            match lex_entry_fields(&entry) {

53

                Some(fields) => {

54

10297

                    spliced = true;

55

10297

                    scalars.extend(fields);

56

57

                // Splicing one side while the other still holds an unexpanded tuple (say, a

58

                // pending index) would misalign the fields, so only scalars stay as they are.

59

75656

                None if is_scalar(&entry) => scalars.push(entry),

60

75467

                None => return Err(RuleNotApplicable),

61

62

63

7406

        Ok(Moo::new(conjure_cp::into_matrix_expr!(scalars)))

64

90482

};

65

85036

    let (lhs, rhs) = (splice(lhs)?, splice(rhs)?);

66

1960

    if !spliced {

67

        return Err(RuleNotApplicable);

68

1960

69

1960

    Ok(RuleEffect::pure(match expr {

70

980

        Expression::LexLt(..) => Expression::LexLt(Metadata::new(), lhs, rhs),

71

980

        _ => Expression::LexLeq(Metadata::new(), lhs, rhs),

72

}))

73

85057

74

75

#[register_rule("SAT", 18500, [LexLt, LexLeq])]

76

415177

fn scalar_lex_comparison(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

77

415177

    let (lhs, rhs) = match expr {

78

415156

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

79

21

        _ => return Err(RuleNotApplicable),

80

};

81

820785

    let elements = |operand: &Expression| {

82

        // Explicit matrices retain element order even after integer representation, and

83

        // lexicographic order does not depend on their index values.

84

820785

        super::counting::matrix_entries(operand)

85

820785

            .map(Ok)

86

66192

            .unwrap_or_else(|| crate::shared::lex::lex_operand_elements(operand))

87

820785

};

88

415156

    let (lhs, rhs) = (elements(lhs)?, elements(rhs)?);

89

405426

    for entries in [&lhs, &rhs] {

90

536032

        if entries.iter().any(|entry| !is_scalar(entry)) {

91

            // Compound comparisons promote back to lex; their representation rules must run first.

92

328062

            return Err(RuleNotApplicable);

93

154728

94

95

77364

    Ok(RuleEffect::pure(

96

77364

        crate::shared::lex::lex_elements_to_recursive_or(

97

77364

            &lhs,

98

77364

            &rhs,

99

77364

            matches!(expr, Expression::LexLeq(..)),

100

77364

),

101

77364

))

102

415177

103

104

/// Representation ordering constraints may already be flattened into scalar atoms.

105

#[register_rule("SAT", 18500, [FlatLexLt, FlatLexLeq])]

106

21

fn flat_scalar_lex_comparison(expr: &Expression, symbols: &SymbolTable) -> ApplicationResult {

107

21

    let (left, right, strict) = match expr {

108

        Expression::FlatLexLt(_, left, right) => (left, right, true),

109

        Expression::FlatLexLeq(_, left, right) => (left, right, false),

110

21

        _ => return Err(RuleNotApplicable),

111

};

112

    let matrix = |atoms: &[conjure_cp::ast::Atom]| {

113

        Moo::new(conjure_cp::into_matrix_expr!(

114

            atoms

115

                .iter()

116

                .cloned()

117

                .map(Expression::from)

118

                .collect::<Vec<_>>()

119

))

120

};

121

    let expression = if strict {

122

        Expression::LexLt(Metadata::new(), matrix(left), matrix(right))

123

    } else {

124

        Expression::LexLeq(Metadata::new(), matrix(left), matrix(right))

125

};

126

    scalar_lex_comparison(&expression, symbols)

127

21

128

129

/// A lex comparison whose entries include compound values (a set, say) compares the first

130

/// entries, then the rest: `a <lex b` iff `a[1] < b[1]`, or `a[1] = b[1]` and the tails compare

131

/// the same way. A strict comparison of single entries is the entries' own order, which their

132

/// representation rules provide, so it is left to them.

133

#[register_rule("SAT", 9200, [LexLt, LexLeq])]

134

83097

fn decompose_compound_lex(expr: &Expression, _: &SymbolTable) -> ApplicationResult {

135

83097

    let (lhs, rhs, strict) = match expr {

136

76643

        Expression::LexLt(_, lhs, rhs) => (lhs, rhs, true),

137

6433

        Expression::LexLeq(_, lhs, rhs) => (lhs, rhs, false),

138

21

        _ => return Err(RuleNotApplicable),

139

};

140

83076

    let lhs = super::counting::matrix_entries(lhs).ok_or(RuleNotApplicable)?;

141

75516

    let rhs = super::counting::matrix_entries(rhs).ok_or(RuleNotApplicable)?;

142

    // Wait for every entry to be a variable or a scalar, so representation rules see references.

143

84805

    let ready = |entry: &Expression| is_scalar(entry) || matches!(entry, Expression::Atomic(..));

144

75467

    if lhs.iter().chain(&rhs).all(is_scalar)

145

75467

        || !lhs.iter().chain(&rhs).all(ready)

146

        || (strict && lhs.len() == 1 && rhs.len() == 1)

147

148

75467

        return Err(RuleNotApplicable);

149

150

    Ok(RuleEffect::pure(lex_prefix(&lhs, &rhs, strict)))

151

83097

152

153

fn lex_prefix(lhs: &[Expression], rhs: &[Expression], strict: bool) -> Expression {

154

    let (Some((a, lhs_rest)), Some((b, rhs_rest))) = (lhs.split_first(), rhs.split_first()) else {

155

        // An empty list is smaller than a non-empty one, and equal to an empty one.

156

        return Expression::from(lhs.is_empty() && !(strict && rhs.is_empty()));

157

};

158

    let single = |entry: &Expression| Moo::new(conjure_cp::into_matrix_expr!(vec![entry.clone()]));

159

    Expression::Or(

160

        Metadata::new(),

161

        Moo::new(conjure_cp::into_matrix_expr!(vec![

162

            Expression::LexLt(Metadata::new(), single(a), single(b)),

163

            Expression::And(

164

                Metadata::new(),

165

                Moo::new(conjure_cp::into_matrix_expr!(vec![

166

                    Expression::Eq(Metadata::new(), Moo::new(a.clone()), Moo::new(b.clone())),

167

                    lex_prefix(lhs_rest, rhs_rest, strict),

168

                ])),

169

),

170

        ])),

171

172