Grcov report - expansion.rs

1

//! Comprehension expansion rules

2

3

mod expand_native;

4

mod expand_via_solver;

5

mod expand_via_solver_ac;

6

7

pub use expand_native::expand_native;

8

pub use expand_via_solver::expand_via_solver;

9

pub use expand_via_solver_ac::expand_via_solver_ac;

10

11

use std::collections::VecDeque;

12

13

use conjure_cp::{

14

    ast::{

15

        Expression as Expr, SymbolTable,

16

        comprehension::{Comprehension, quantified_expander_for_comprehensions},

17

},

18

    into_matrix_expr,

19

    rule_engine::{

20

        ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,

21

},

22

    settings::QuantifiedExpander,

23

};

24

use uniplate::Biplate;

25

26

use uniplate::Uniplate;

27

28

/// Expand comprehensions inside AC operators using `--quantified-expander via-solver-ac`.

29

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

30

35726

fn expand_comprehension_via_solver_ac(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

31

35726

    if quantified_expander_for_comprehensions() != QuantifiedExpander::ViaSolverAc {

32

41

        return Err(RuleNotApplicable);

33

35685

34

35

    // Is this an ac expression?

36

35685

    let ac_operator_kind = expr.to_ac_operator_kind().ok_or(RuleNotApplicable)?;

37

38

2397

    debug_assert_eq!(

39

2397

        expr.children().len(),

40

1,

41

        "AC expressions should have exactly one child."

42

);

43

44

2397

    let Expr::Comprehension(_, ref comprehension) = expr.children()[0] else {

45

2175

        return Err(RuleNotApplicable);

46

};

47

48

    // unwrap comprehensions inside out. This reduces calls to minion when rewriting nested

49

    // comprehensions.

50

222

    let nested_comprehensions: VecDeque<Comprehension> =

51

222

        (**comprehension).clone().return_expression().universe_bi();

52

222

    if !nested_comprehensions.is_empty() {

53

111

        return Err(RuleNotApplicable);

54

111

};

55

56

    // TODO: check what kind of error this throws and maybe panic

57

111

    let mut symbols = symbols.clone();

58

111

    let results = expand_via_solver_ac((**comprehension).clone(), &mut symbols, ac_operator_kind)

59

111

        .or(Err(RuleNotApplicable))?;

60

61

108

    let new_expr = ac_operator_kind.as_expression(into_matrix_expr!(results));

62

108

    Ok(Reduction::with_symbols(new_expr, symbols))

63

35726

64

65

/// Expand comprehensions using `--quantified-expander native`.

66

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

67

24944

fn expand_comprehension_native(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

68

24944

    if quantified_expander_for_comprehensions() != QuantifiedExpander::Native {

69

24903

        return Err(RuleNotApplicable);

70

41

71

72

41

    let Expr::Comprehension(_, comprehension) = expr else {

73

41

        return Err(RuleNotApplicable);

74

};

75

76

    // unwrap comprehensions inside out. This reduces calls to minion when rewriting nested

77

    // comprehensions.

78

    let nested_comprehensions: VecDeque<Comprehension> =

79

        (**comprehension).clone().return_expression().universe_bi();

80

    if !nested_comprehensions.is_empty() {

81

        return Err(RuleNotApplicable);

82

};

83

84

    // TODO: check what kind of error this throws and maybe panic

85

86

    let mut symbols = symbols.clone();

87

    let results =

88

        expand_native(comprehension.as_ref().clone(), &mut symbols).or(Err(RuleNotApplicable))?;

89

90

    Ok(Reduction::with_symbols(into_matrix_expr!(results), symbols))

91

24944

92

93

/// Expand comprehensions using `--quantified-expander via-solver` (and as fallback for

94

/// non-AC comprehensions when `--quantified-expander via-solver-ac`).

95

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

96

24944

fn expand_comprehension_via_solver(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

97

41

    if !matches!(

98

24944

        quantified_expander_for_comprehensions(),

99

        QuantifiedExpander::ViaSolver | QuantifiedExpander::ViaSolverAc

100

) {

101

41

        return Err(RuleNotApplicable);

102

24903

103

104

24903

    let Expr::Comprehension(_, comprehension) = expr else {

105

24852

        return Err(RuleNotApplicable);

106

};

107

108

    // unwrap comprehensions inside out. This reduces calls to minion when rewriting nested

109

    // comprehensions.

110

51

    let nested_comprehensions: VecDeque<Comprehension> =

111

51

        (**comprehension).clone().return_expression().universe_bi();

112

51

    if !nested_comprehensions.is_empty() {

113

39

        return Err(RuleNotApplicable);

114

12

};

115

116

    // TODO: check what kind of error this throws and maybe panic

117

118

12

    let mut symbols = symbols.clone();

119

12

    let results = expand_via_solver(comprehension.as_ref().clone(), &mut symbols)

120

12

        .or(Err(RuleNotApplicable))?;

121

122

12

    Ok(Reduction::with_symbols(into_matrix_expr!(results), symbols))

123

24944