Grcov report - bool.rs

1

//! Normalising rules for boolean operations (not, and, or, ->).

2

3

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

4

use conjure_cp::essence_expr;

5

use conjure_cp::into_matrix_expr;

6

use conjure_cp::rule_engine::{

7

    ApplicationError, ApplicationError::RuleNotApplicable, ApplicationResult, Reduction,

8

    register_rule,

9

};

10

use uniplate::Uniplate;

11

12

/// Removes double negations

13

///

14

/// ```text

15

/// not(not(a)) = a

16

/// ```

17

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

18

984840

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

19

984840

    match expr {

20

1188

        Expr::Not(_, contents) => match contents.as_ref() {

21

27

            Expr::Not(_, expr_box) => Ok(Reduction::pure(Moo::unwrap_or_clone(expr_box.clone()))),

22

1161

            _ => Err(ApplicationError::RuleNotApplicable),

23

},

24

983652

        _ => Err(ApplicationError::RuleNotApplicable),

25

26

984840

27

28

/// Distributes `ands` contained in `ors`

29

///

30

/// ```text

31

/// or(and(a, b), c) ~> and(or(a, c), or(b, c))

32

/// ```

33

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

34

984840

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

35

4725

    fn find_and(exprs: &[Expr]) -> Option<usize> {

36

        // ToDo: may be better to move this to some kind of utils module?

37

12942

        for (i, e) in exprs.iter().enumerate() {

38

12942

            if let Expr::And(_, _) = e {

39

270

                return Some(i);

40

12672

41

42

4455

        None

43

4725

44

45

984840

    match expr {

46

6147

        Expr::Or(_, e) => {

47

6147

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

48

1422

                return Err(RuleNotApplicable);

49

};

50

51

4725

            match find_and(&exprs) {

52

270

                Some(idx) => {

53

270

                    let mut rest = exprs.clone();

54

270

                    let and_expr = rest.remove(idx);

55

56

270

                    match and_expr {

57

270

                        Expr::And(metadata, e) => {

58

270

                            let Some(and_exprs) = e.as_ref().clone().unwrap_list() else {

59

9

                                return Err(RuleNotApplicable);

60

};

61

62

261

                            let mut new_and_contents = Vec::new();

63

64

522

                            for e in and_exprs {

65

                                // ToDo: Cloning everything may be a bit inefficient - discuss

66

522

                                let mut new_or_contents = rest.clone();

67

522

                                new_or_contents.push(e.clone());

68

522

                                new_and_contents.push(Expr::Or(

69

522

                                    metadata.clone_dirty(),

70

522

                                    Moo::new(into_matrix_expr![new_or_contents]),

71

522

))

72

73

74

261

                            Ok(Reduction::pure(Expr::And(

75

261

                                metadata.clone_dirty(),

76

261

                                Moo::new(into_matrix_expr![new_and_contents]),

77

261

)))

78

79

                        _ => Err(ApplicationError::RuleNotApplicable),

80

81

82

4455

                None => Err(ApplicationError::RuleNotApplicable),

83

84

85

978693

        _ => Err(ApplicationError::RuleNotApplicable),

86

87

984840

88

89

/// Distributes `not` over `and` by De Morgan's Law

90

///

91

/// ```text

92

/// not(and(a, b)) ~> or(not(a), not(b))

93

/// ```

94

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

95

984849

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

96

5158458

    for child in expr.universe() {

97

5156379

        if matches!(

98

5158458

            child,

99

            Expr::UnsafeDiv(_, _, _) | Expr::Bubble(_, _, _) | Expr::UnsafeMod(_, _, _)

100

) {

101

2079

            return Err(RuleNotApplicable);

102

5156379

103

104

982770

    match expr {

105

1125

        Expr::Not(_, contents) => match contents.as_ref() {

106

432

            Expr::And(metadata, e) => {

107

432

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

108

342

                    return Err(RuleNotApplicable);

109

};

110

111

90

                if exprs.len() == 1 {

112

                    let single_expr = exprs[0].clone();

113

                    return Ok(Reduction::pure(essence_expr!(!&single_expr)));

114

90

115

116

90

                let mut new_exprs = Vec::new();

117

207

                for e in exprs {

118

207

                    new_exprs.push(essence_expr!(!&e));

119

207

120

90

                Ok(Reduction::pure(Expr::Or(

121

90

                    metadata.clone(),

122

90

                    Moo::new(into_matrix_expr![new_exprs]),

123

90

)))

124

125

693

            _ => Err(ApplicationError::RuleNotApplicable),

126

},

127

981645

        _ => Err(ApplicationError::RuleNotApplicable),

128

129

984849

130

131

/// Distributes `not` over `or` by De Morgan's Law

132

///

133

/// ```text

134

/// not(or(a, b)) ~> and(not(a), not(b))

135

/// ```

136

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

137

984849

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

138

984849

    match expr {

139

1197

        Expr::Not(_, contents) => match contents.as_ref() {

140

9

            Expr::Or(metadata, e) => {

141

9

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

142

                    return Err(RuleNotApplicable);

143

};

144

145

9

                if exprs.len() == 1 {

146

                    let single_expr = exprs[0].clone();

147

                    return Ok(Reduction::pure(essence_expr!(!&single_expr)));

148

9

149

150

9

                let mut new_exprs = Vec::new();

151

152

18

                for e in exprs {

153

18

                    new_exprs.push(essence_expr!(!&e));

154

18

155

156

9

                Ok(Reduction::pure(Expr::And(

157

9

                    metadata.clone(),

158

9

                    Moo::new(into_matrix_expr![new_exprs]),

159

9

)))

160

161

1188

            _ => Err(ApplicationError::RuleNotApplicable),

162

},

163

983652

        _ => Err(ApplicationError::RuleNotApplicable),

164

165

984849

166

167

/// Removes ands with a single argument.

168

///

169

/// ```text

170

/// and([a]) ~> a

171

/// ```

172

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

173

174

1217106

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

175

1217106

    match expr {

176

14319

        Expr::And(_, e) => {

177

14319

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

178

11124

                return Err(RuleNotApplicable);

179

};

180

181

3195

            if exprs.len() == 1 {

182

531

                return Ok(Reduction::pure(exprs[0].clone()));

183

2664

184

185

2664

            Err(ApplicationError::RuleNotApplicable)

186

187

1202787

        _ => Err(ApplicationError::RuleNotApplicable),

188

189

1217106

190

191

/// Removes ors with a single argument.

192

///

193

/// ```text

194

/// or([a]) ~> a

195

/// ```

196

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

197

1217106

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

198

1217106

    let Expr::Or(_, e) = expr else {

199

1208196

        return Err(RuleNotApplicable);

200

};

201

202

8910

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

203

1710

        return Err(RuleNotApplicable);

204

};

205

206

    // do not conflict with unwrap_nested_or rule.

207

7200

    if exprs.len() != 1 || matches!(exprs[0], Expr::Or(_, _)) {

208

5868

        return Err(RuleNotApplicable);

209

1332

210

211

1332

    Ok(Reduction::pure(exprs[0].clone()))

212

1217106

213

214

/// Applies the contrapositive of implication.

215

///

216

/// ```text

217

/// !p -> !q ~> q -> p

218

/// ```

219

/// where p,q are safe.

220

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

221

1217097

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

222

1217097

    let Expr::Imply(_, e1, e2) = expr else {

223

1213335

        return Err(RuleNotApplicable);

224

};

225

226

3762

    let Expr::Not(_, p) = e1.as_ref() else {

227

3753

        return Err(RuleNotApplicable);

228

};

229

230

9

    let Expr::Not(_, q) = e2.as_ref() else {

231

        return Err(RuleNotApplicable);

232

};

233

234

    // we only negate e1, e2 if they are safe.

235

9

    if !e1.is_safe() || !e2.is_safe() {

236

        return Err(RuleNotApplicable);

237

9

238

239

9

    Ok(Reduction::pure(essence_expr!(&q -> &p)))

240

1217097

241

242

/// Simplifies the negation of implication.

243

///

244

/// ```text

245

/// !(p->q) ~> p /\ !q

246

/// ```,

247

///

248

/// where p->q is safe

249

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

250

1217097

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

251

1217097

    let Expr::Not(_, e1) = expr else {

252

1215585

        return Err(RuleNotApplicable);

253

};

254

255

1512

    let Expr::Imply(_, p, q) = e1.as_ref() else {

256

1503

        return Err(RuleNotApplicable);

257

};

258

259

    // p->q must be safe to negate

260

9

    if !e1.is_safe() {

261

        return Err(RuleNotApplicable);

262

9

263

264

9

    Ok(Reduction::pure(essence_expr!(r"&p /\ !&q")))

265

1217097

266

267

/// Applies left distributivity to implication.

268

///

269

/// ```text

270

/// ((r -> p) -> (r->q)) ~> (r -> (p -> q))

271

/// ```

272

///

273

/// This rule relies on CSE to unify the two instances of `r` to a single atom; therefore, it might

274

/// not work as well when optimisations are disabled.

275

///

276

/// Has a higher priority than `normalise_implies_uncurry` as this should apply first. See the

277

/// docstring for `normalise_implies_uncurry`.

278

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

279

1217097

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

280

1217097

    let Expr::Imply(_, e1, e2) = expr else {

281

1213335

        return Err(RuleNotApplicable);

282

};

283

284

3762

    let Expr::Imply(_, r1, p) = e1.as_ref() else {

285

3753

        return Err(RuleNotApplicable);

286

};

287

288

9

    let Expr::Imply(_, r2, q) = e2.as_ref() else {

289

        return Err(RuleNotApplicable);

290

};

291

292

    // Instead of checking deep equality, let CSE unify them to a common variable and check for

293

    // that.

294

295

9

    let r1_atom: &Atom = r1.as_ref().try_into().or(Err(RuleNotApplicable))?;

296

9

    let r2_atom: &Atom = r2.as_ref().try_into().or(Err(RuleNotApplicable))?;

297

298

9

    if !(r1_atom == r2_atom) {

299

        return Err(RuleNotApplicable);

300

9

301

302

9

    Ok(Reduction::pure(essence_expr!(&r1 -> (&p -> &q))))

303

1217097

304

305

/// Applies import-export to implication, i.e. uncurrying.

306

///

307

/// ```text

308

/// p -> (q -> r) ~> (p/\q) -> r

309

/// ```

310

///

311

/// This rule has a lower priority of 8400 to allow distributivity, contraposition, etc. to

312

/// apply first.

313

///

314

/// For example, we want to do:

315

///

316

/// ```text

317

/// ((r -> p) -> (r -> q)) ~> (r -> (p -> q))  [left-distributivity]

318

/// (r -> (p -> q)) ~> (r/\p) ~> q [uncurry]

319

/// ```

320

///

321

/// not

322

///

323

/// ```text

324

/// ((r->p) -> (r->q)) ~> ((r->p) /\ r) -> q) ~> [uncurry]

325

/// ```

326

///

327

/// # Rationale

328

///

329

/// With this rule, I am assuming (without empirical evidence) that and is a cheaper constraint

330

/// than implication (in particular, Minion's reifyimply constraint).

331

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

332

984831

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

333

984831

    let Expr::Imply(_, p, e1) = expr else {

334

981510

        return Err(RuleNotApplicable);

335

};

336

337

3321

    let Expr::Imply(_, q, r) = e1.as_ref() else {

338

3294

        return Err(RuleNotApplicable);

339

};

340

341

27

    Ok(Reduction::pure(essence_expr!(r"(&p /\ &q) -> &r")))

342

984831