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

mod via_solver_common;

7

8

pub use expand_native::expand_native;

9

pub use expand_via_solver::expand_via_solver;

10

pub use expand_via_solver_ac::expand_via_solver_ac;

11

12

use conjure_cp::{

13

    ast::{Expression as Expr, SymbolTable, comprehension::Comprehension},

14

    bug, into_matrix_expr,

15

    rule_engine::{

16

        ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,

17

},

18

    settings::{QuantifiedExpander, comprehension_expander},

19

};

20

use uniplate::Uniplate;

21

22

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

23

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

24

112167

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

25

112167

    if comprehension_expander() != QuantifiedExpander::Native {

26

109767

        return Err(RuleNotApplicable);

27

2400

28

29

2400

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

30

2268

        return Err(RuleNotApplicable);

31

};

32

33

132

    let comprehension = comprehension.as_ref().clone();

34

132

    let mut symbols = symbols.clone();

35

132

    let results = expand_native(comprehension, &mut symbols)

36

        .unwrap_or_else(|e| bug!("native comprehension expansion failed: {e}"));

37

132

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

38

112167

39

40

/// Expand comprehensions using `--comprehension-expander via-solver`.

41

///

42

/// Algorithm sketch:

43

/// 1. Match one comprehension node.

44

/// 2. Build a temporary generator submodel from its qualifiers/guards.

45

/// 3. Materialise quantified declarations as temporary `find` declarations.

46

/// 4. Wrap that submodel as a standalone temporary model, with search order restricted to the

47

///    quantified names.

48

/// 5. Rewrite the temporary model using the configured rewriter and Minion-oriented rules.

49

/// 6. Solve the rewritten temporary model with Minion and keep only quantified assignments from

50

///    each solution.

51

/// 7. Instantiate the original return expression under each quantified assignment.

52

/// 8. Replace the comprehension by a matrix literal containing all instantiated return values.

53

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

54

112167

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

55

2400

    if !matches!(

56

112167

        comprehension_expander(),

57

        QuantifiedExpander::ViaSolver | QuantifiedExpander::ViaSolverAc

58

) {

59

2400

        return Err(RuleNotApplicable);

60

109767

61

62

109767

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

63

109323

        return Err(RuleNotApplicable);

64

};

65

66

444

    let comprehension = comprehension.as_ref().clone();

67

444

    let results = expand_via_solver(comprehension)

68

        .unwrap_or_else(|e| bug!("via-solver comprehension expansion failed: {e}"));

69

444

    Ok(Reduction::with_symbols(

70

444

        into_matrix_expr!(results),

71

444

        symbols.clone(),

72

444

))

73

112167

74

75

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

76

///

77

/// Algorithm sketch:

78

/// 1. Match an AC operator whose single child is a comprehension.

79

/// 2. Build a temporary generator submodel from the comprehension qualifiers/guards.

80

/// 3. Add a derived constraint from the return expression to this generator model:

81

///    localise non-local references, and replace non-quantified fragments with dummy variables so

82

///    the constraint depends only on locally solvable symbols.

83

/// 4. Materialise quantified declarations as temporary `find` declarations in the temporary model.

84

/// 5. Rewrite and solve the temporary model with Minion; keep only quantified assignments.

85

/// 6. Instantiate the original return expression under those assignments.

86

/// 7. Rebuild the same AC operator around the instantiated matrix literal.

87

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

88

170337

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

89

170337

    if comprehension_expander() != QuantifiedExpander::ViaSolverAc {

90

5670

        return Err(RuleNotApplicable);

91

164667

92

93

    // Is this an ac expression?

94

164667

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

95

96

11364

    debug_assert_eq!(

97

11364

        expr.children().len(),

98

1,

99

        "AC expressions should have exactly one child."

100

);

101

102

11364

    let comprehension = as_single_comprehension(&expr.children()[0]).ok_or(RuleNotApplicable)?;

103

104

126

    let results =

105

1080

        expand_via_solver_ac(comprehension, ac_operator_kind).or(Err(RuleNotApplicable))?;

106

107

126

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

108

126

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

109

170337

110

111

11364

fn as_single_comprehension(expr: &Expr) -> Option<Comprehension> {

112

11364

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

113

1080

        return Some(comprehension.as_ref().clone());

114

10284

115

116

10284

    let exprs = expr.clone().unwrap_list()?;

117

5556

    let [Expr::Comprehension(_, comprehension)] = exprs.as_slice() else {

118

5556

        return None;

119

};

120

121

    Some(comprehension.as_ref().clone())

122

11364