Grcov report - base.rs

1

use std::rc::Rc;

2

3

use conjure_core::ast::{Atom, Expression as Expr, Literal as Lit, SymbolTable};

4

use conjure_core::metadata::Metadata;

5

use conjure_core::rule_engine::{

6

    register_rule, register_rule_set, ApplicationError, ApplicationError::RuleNotApplicable,

7

    ApplicationResult, Reduction,

8

};

9

use uniplate::Uniplate;

10

11

use Atom::*;

12

use Expr::*;

13

use Lit::Bool;

14

15

use crate::ast::Declaration;

16

use crate::{into_matrix_expr, matrix_expr};

17

18

register_rule_set!("Base", ());

19

20

/// This rule simplifies expressions where the operator is applied to an empty set of sub-expressions.

21

///

22

/// For example:

23

/// - `or([])` simplifies to `false` since no disjunction exists.

24

///

25

/// **Applicable examples:**

26

/// ```text

27

/// or([])  ~> false

28

/// X([]) ~> Nothing

29

/// ```

30

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

31

418122

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

32

    // excluded expressions

33

140778

    if matches!(

34

418122

        expr,

35

        Atomic(_, _)

36

            | Root(_, _)

37

            | FlatIneq(_, _, _, _)

38

            | FlatMinusEq(_, _, _)

39

            | FlatSumGeq(_, _, _)

40

            | FlatSumLeq(_, _, _)

41

            | FlatProductEq(_, _, _, _)

42

            | FlatWatchedLiteral(_, _, _)

43

            | FlatWeightedSumGeq(_, _, _, _)

44

            | FlatWeightedSumLeq(_, _, _, _)

45

            | MinionDivEqUndefZero(_, _, _, _)

46

            | MinionModuloEqUndefZero(_, _, _, _)

47

            | MinionPow(_, _, _, _)

48

            | MinionReify(_, _, _)

49

            | MinionReifyImply(_, _, _)

50

            | FlatAbsEq(_, _, _)

51

            | Min(_, _)

52

            | Max(_, _)

53

            | AllDiff(_, _)

54

            | FlatAllDiff(_, _)

55

            | AbstractLiteral(_, _)

56

) {

57

277344

        return Err(ApplicationError::RuleNotApplicable);

58

140778

59

140778

60

140778

    if !expr.children().is_empty() {

61

140778

        return Err(ApplicationError::RuleNotApplicable);

62

63

64

    let new_expr = match expr {

65

        Or(_, _) => Atomic(Metadata::new(), Literal(Bool(false))),

66

        _ => And(Metadata::new(), Box::new(matrix_expr![])),

67

};

68

69

    Ok(Reduction::pure(new_expr))

70

418122

71

72

/**

73

 * Turn a Min into a new variable and post a top-level constraint to ensure the new variable is the minimum.

74

 * ```text

75

1

 * min([a, b]) ~> c ; c <= a & c <= b & (c = a | c = b)

76

1

 * ```

77

1

*/

78

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

79

317232

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

80

317232

    let Expr::Min(_, inside_min_expr) = expr else {

81

316998

        return Err(RuleNotApplicable);

82

};

83

84

    // let matrix expressions / comprehensions be unrolled first before applying this rule.

85

234

    let Some(exprs) = inside_min_expr.as_ref().clone().unwrap_list() else {

86

126

        return Err(RuleNotApplicable);

87

};

88

89

108

    let mut symbols = symbols.clone();

90

108

    let new_name = symbols.gensym();

91

108

92

108

    let mut new_top = Vec::new(); // the new variable must be less than or equal to all the other variables

93

108

    let mut disjunction = Vec::new(); // the new variable must be equal to one of the variables

94

324

    for e in exprs {

95

216

        new_top.push(Leq(

96

216

            Metadata::new(),

97

216

            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

98

216

            Box::new(e.clone()),

99

216

));

100

216

        disjunction.push(Eq(

101

216

            Metadata::new(),

102

216

            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

103

216

            Box::new(e.clone()),

104

216

));

105

216

106

    // TODO: deal with explicit index domains

107

108

    new_top.push(Or(

108

        Metadata::new(),

109

108

        Box::new(into_matrix_expr![disjunction]),

110

108

));

111

112

108

    let domain = expr

113

108

        .domain_of(&symbols)

114

108

        .ok_or(ApplicationError::DomainError)?;

115

108

    symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));

116

108

117

108

    Ok(Reduction::new(

118

108

        Atomic(Metadata::new(), Reference(new_name)),

119

108

        new_top,

120

108

        symbols,

121

108

))

122

317232

123

124

/**

125

 * Turn a Max into a new variable and post a top level constraint to ensure the new variable is the maximum.

126

 * ```text

127

1

 * max([a, b]) ~> c ; c >= a & c >= b & (c = a | c = b)

128

1

 * ```

129

1

*/

130

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

131

317232

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

132

317232

    let Expr::Max(_, inside_max_expr) = expr else {

133

317052

        return Err(RuleNotApplicable);

134

};

135

136

180

    let Some(exprs) = inside_max_expr.as_ref().clone().unwrap_list() else {

137

126

        return Err(RuleNotApplicable);

138

};

139

140

54

    let mut symbols = symbols.clone();

141

54

    let new_name = symbols.gensym();

142

54

143

54

    let mut new_top = Vec::new(); // the new variable must be more than or equal to all the other variables

144

54

    let mut disjunction = Vec::new(); // the new variable must more than or equal to one of the variables

145

162

    for e in exprs {

146

108

        new_top.push(Geq(

147

108

            Metadata::new(),

148

108

            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

149

108

            Box::new(e.clone()),

150

108

));

151

108

        disjunction.push(Eq(

152

108

            Metadata::new(),

153

108

            Box::new(Atomic(Metadata::new(), Reference(new_name.clone()))),

154

108

            Box::new(e.clone()),

155

108

));

156

108

157

    // FIXME: deal with explicitly given domains

158

54

    new_top.push(Or(

159

54

        Metadata::new(),

160

54

        Box::new(into_matrix_expr![disjunction]),

161

54

));

162

163

54

    let domain = expr

164

54

        .domain_of(&symbols)

165

54

        .ok_or(ApplicationError::DomainError)?;

166

54

    symbols.insert(Rc::new(Declaration::new_var(new_name.clone(), domain)));

167

54

168

54

    Ok(Reduction::new(

169

54

        Atomic(Metadata::new(), Reference(new_name)),

170

54

        new_top,

171

54

        symbols,

172

54

))

173

317232