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

391032

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

32

    // excluded expressions

33

132786

    if matches!(

34

391032

        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

            | AbstractLiteral(_, _)

55

) {

56

258246

        return Err(ApplicationError::RuleNotApplicable);

57

132786

58

132786

59

132786

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

60

132786

        return Err(ApplicationError::RuleNotApplicable);

61

62

63

    let new_expr = match expr {

64

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

65

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

66

};

67

68

    Ok(Reduction::pure(new_expr))

69

391032

70

71

/**

72

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

73

 * ```text

74

1

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

75

1

 * ```

76

1

*/

77

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

78

305802

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

79

305802

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

80

305568

        return Err(RuleNotApplicable);

81

};

82

83

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

84

234

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

85

126

        return Err(RuleNotApplicable);

86

};

87

88

108

    let mut symbols = symbols.clone();

89

108

    let new_name = symbols.gensym();

90

108

91

108

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

92

108

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

93

324

    for e in exprs {

94

216

        new_top.push(Leq(

95

216

            Metadata::new(),

96

216

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

97

216

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

98

216

));

99

216

        disjunction.push(Eq(

100

216

            Metadata::new(),

101

216

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

102

216

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

103

216

));

104

216

105

    // TODO: deal with explicit index domains

106

108

    new_top.push(Or(

107

108

        Metadata::new(),

108

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

109

108

));

110

111

108

    let domain = expr

112

108

        .domain_of(&symbols)

113

108

        .ok_or(ApplicationError::DomainError)?;

114

108

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

115

108

116

108

    Ok(Reduction::new(

117

108

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

118

108

        new_top,

119

108

        symbols,

120

108

))

121

305802

122

123

/**

124

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

125

 * ```text

126

1

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

127

1

 * ```

128

1

*/

129

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

130

305802

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

131

305802

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

132

305622

        return Err(RuleNotApplicable);

133

};

134

135

180

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

136

126

        return Err(RuleNotApplicable);

137

};

138

139

54

    let mut symbols = symbols.clone();

140

54

    let new_name = symbols.gensym();

141

54

142

54

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

143

54

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

144

162

    for e in exprs {

145

108

        new_top.push(Geq(

146

108

            Metadata::new(),

147

108

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

148

108

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

149

108

));

150

108

        disjunction.push(Eq(

151

108

            Metadata::new(),

152

108

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

153

108

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

154

108

));

155

108

156

    // FIXME: deal with explicitly given domains

157

54

    new_top.push(Or(

158

54

        Metadata::new(),

159

54

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

160

54

));

161

162

54

    let domain = expr

163

54

        .domain_of(&symbols)

164

54

        .ok_or(ApplicationError::DomainError)?;

165

54

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

166

54

167

54

    Ok(Reduction::new(

168

54

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

169

54

        new_top,

170

54

        symbols,

171

54

))

172

305802