Grcov report - base.rs

1

use conjure_core::ast::{

2

    DecisionVariable, Expression as Expr, Factor, Literal as Lit, SymbolTable,

3

};

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 conjure_core::Model;

10

use uniplate::Uniplate;

11

12

use Expr::*;

13

use Factor::*;

14

use Lit::*;

15

16

/*****************************************************************************/

17

/*        This file contains basic rules for simplifying expressions         */

18

/*****************************************************************************/

19

20

register_rule_set!("Base", 100, ());

21

22

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

23

///

24

/// For example:

25

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

26

///

27

/// **Applicable examples:**

28

/// ```text

29

/// or([])  ~> false

30

/// X([]) ~> Nothing

31

/// ```

32

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

33

8222390

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

34

    // excluded expressions

35

2086087

    if matches!(

36

6135827

        expr,

37

        FactorE(_, Reference(_,))

38

            | FactorE(_, Literal(_))

39

            | WatchedLiteral(_, _, _)

40

            | FactorE(_, Reference(_,))

41

            | FactorE(_, Literal(_))

42

            | WatchedLiteral(_, _, _)

43

            | DivEq(_, _, _, _)

44

) {

45

6136303

        return Err(ApplicationError::RuleNotApplicable);

46

2086087

47

2086087

48

2086087

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

49

2086036

        return Err(ApplicationError::RuleNotApplicable);

50

51

52

51

    let new_expr = match expr {

53

17

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

54

34

        _ => And(Metadata::new(), vec![]), // TODO: (yb33) Change it to a simple vector after we refactor our model,

55

};

56

57

51

    Ok(Reduction::pure(new_expr))

58

8222390

59

60

/**

61

 * Unwrap trivial sums:

62

 * ```text

63

1

 * sum([a]) = a

64

1

 * ```

65

1

*/

66

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

67

8222424

fn unwrap_sum(expr: &Expr, _: &Model) -> ApplicationResult {

68

204

    match expr {

69

204

        Sum(_, exprs) if (exprs.len() == 1) => Ok(Reduction::pure(exprs[0].clone())),

70

8222390

        _ => Err(ApplicationError::RuleNotApplicable),

71

72

8222424

73

74

/**

75

 * Flatten nested sums:

76

 * ```text

77

1

 * sum(sum(a, b), c) = sum(a, b, c)

78

1

 * ```

79

1

*/

80

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

81

8222390

pub fn flatten_nested_sum(expr: &Expr, _: &Model) -> ApplicationResult {

82

8222390

    match expr {

83

170

        Sum(metadata, exprs) => {

84

170

            let mut new_exprs = Vec::new();

85

170

            let mut changed = false;

86

646

            for e in exprs {

87

476

                match e {

88

170

                    Sum(_, sub_exprs) => {

89

170

                        changed = true;

90

510

                        for e in sub_exprs {

91

340

                            new_exprs.push(e.clone());

92

340

93

94

306

                    _ => new_exprs.push(e.clone()),

95

96

97

170

            if !changed {

98

                return Err(ApplicationError::RuleNotApplicable);

99

170

100

170

            Ok(Reduction::pure(Sum(metadata.clone_dirty(), new_exprs)))

101

102

8222220

        _ => Err(ApplicationError::RuleNotApplicable),

103

104

8222390

105

106

/**

107

* Unwrap nested `or`

108

109

* ```text

110

1

* or(or(a, b), c) = or(a, b, c)

111

1

* ```

112

1

*/

113

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

114

8222424

fn unwrap_nested_or(expr: &Expr, _: &Model) -> ApplicationResult {

115

8222424

    match expr {

116

428740

        Or(metadata, exprs) => {

117

428740

            let mut new_exprs = Vec::new();

118

428740

            let mut changed = false;

119

2094468

            for e in exprs {

120

1665728

                match e {

121

102

                    Or(_, exprs) => {

122

102

                        changed = true;

123

306

                        for e in exprs {

124

204

                            new_exprs.push(e.clone());

125

204

126

127

1665626

                    _ => new_exprs.push(e.clone()),

128

129

130

428740

            if !changed {

131

428638

                return Err(ApplicationError::RuleNotApplicable);

132

102

133

102

            Ok(Reduction::pure(Or(metadata.clone_dirty(), new_exprs)))

134

135

7793684

        _ => Err(ApplicationError::RuleNotApplicable),

136

137

8222424

138

139

/**

140

* Unwrap nested `and`

141

142

* ```text

143

1

* and(and(a, b), c) = and(a, b, c)

144

1

* ```

145

1

*/

146

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

147

8222424

fn unwrap_nested_and(expr: &Expr, _: &Model) -> ApplicationResult {

148

8222424

    match expr {

149

19788

        And(metadata, exprs) => {

150

19788

            let mut new_exprs = Vec::new();

151

19788

            let mut changed = false;

152

616998

            for e in exprs {

153

597210

                match e {

154

4369

                    And(_, exprs) => {

155

4369

                        changed = true;

156

13056

                        for e in exprs {

157

8687

                            new_exprs.push(e.clone());

158

8687

159

160

592841

                    _ => new_exprs.push(e.clone()),

161

162

163

19788

            if !changed {

164

15419

                return Err(ApplicationError::RuleNotApplicable);

165

4369

166

4369

            Ok(Reduction::pure(And(metadata.clone_dirty(), new_exprs)))

167

168

8202636

        _ => Err(ApplicationError::RuleNotApplicable),

169

170

8222424

171

172

/**

173

* Remove double negation:

174

175

* ```text

176

1

* not(not(a)) = a

177

1

* ```

178

1

*/

179

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

180

8222407

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

181

8222407

    match expr {

182

544

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

183

17

            Not(_, expr_box) => Ok(Reduction::pure(*expr_box.clone())),

184

527

            _ => Err(ApplicationError::RuleNotApplicable),

185

},

186

8221863

        _ => Err(ApplicationError::RuleNotApplicable),

187

188

8222407

189

190

/**

191

 * Remove trivial `and` (only one element):

192

 * ```text

193

1

 * and([a]) = a

194

1

 * ```

195

1

*/

196

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

197

8222407

fn remove_trivial_and(expr: &Expr, _: &Model) -> ApplicationResult {

198

8222407

    match expr {

199

19771

        And(_, exprs) => {

200

19771

            if exprs.len() == 1 {

201

17

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

202

19754

203

19754

            Err(ApplicationError::RuleNotApplicable)

204

205

8202636

        _ => Err(ApplicationError::RuleNotApplicable),

206

207

8222407

208

209

/**

210

 * Remove trivial `or` (only one element):

211

 * ```text

212

1

 * or([a]) = a

213

1

 * ```

214

1

*/

215

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

216

8222407

fn remove_trivial_or(expr: &Expr, _: &Model) -> ApplicationResult {

217

428723

    match expr {

218

428723

        // do not conflict with unwrap_nested_or rule.

219

428723

        Or(_, exprs) if exprs.len() == 1 && !matches!(exprs[0], Or(_, _)) => {

220

51

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

221

222

8222356

        _ => Err(ApplicationError::RuleNotApplicable),

223

224

8222407

225

226

/**

227

<<<<<<< HEAD

228

 * Remove constant bools from or expressions

229

 * ```text

230

 * or([true, a]) = true

231

1

 * or([false, a]) = a

232

1

 * ```

233

1

*/

234

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

235

8222390

fn remove_constants_from_or(expr: &Expr, _: &Model) -> ApplicationResult {

236

8222390

    match expr {

237

428706

        Or(metadata, exprs) => {

238

428706

            let mut new_exprs = Vec::new();

239

428706

            let mut changed = false;

240

2094332

            for e in exprs {

241

68

                match e {

242

68

                    FactorE(metadata, Literal(Bool(val))) => {

243

68

                        if *val {

244

                            // If we find a true, the whole expression is true

245

34

                            return Ok(Reduction::pure(FactorE(

246

34

                                metadata.clone_dirty(),

247

34

                                Literal(Bool(true)),

248

34

                            )));

249

34

                        } else {

250

34

                            // If we find a false, we can ignore it

251

34

                            changed = true;

252

34

253

254

1665592

                    _ => new_exprs.push(e.clone()),

255

256

257

428672

            if !changed {

258

428638

                return Err(ApplicationError::RuleNotApplicable);

259

34

260

34

            Ok(Reduction::pure(Or(metadata.clone_dirty(), new_exprs)))

261

262

7793684

        _ => Err(ApplicationError::RuleNotApplicable),

263

264

8222390

265

266

/**

267

 * Remove constant bools from and expressions

268

 * ```text

269

 * and([true, a]) = a

270

1

 * and([false, a]) = false

271

1

 * ```

272

1

*/

273

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

274

8222390

fn remove_constants_from_and(expr: &Expr, _: &Model) -> ApplicationResult {

275

8222390

    match expr {

276

19754

        And(metadata, exprs) => {

277

19754

            let mut new_exprs = Vec::new();

278

19754

            let mut changed = false;

279

616896

            for e in exprs {

280

68

                match e {

281

68

                    FactorE(metadata, Literal(Bool(val))) => {

282

68

                        if !*val {

283

                            // If we find a false, the whole expression is false

284

                            return Ok(Reduction::pure(FactorE(

285

                                metadata.clone_dirty(),

286

                                Literal(Bool(false)),

287

                            )));

288

68

                        } else {

289

68

                            // If we find a true, we can ignore it

290

68

                            changed = true;

291

68

292

293

597074

                    _ => new_exprs.push(e.clone()),

294

295

296

19754

            if !changed {

297

19686

                return Err(ApplicationError::RuleNotApplicable);

298

68

299

68

            Ok(Reduction::pure(And(metadata.clone_dirty(), new_exprs)))

300

301

8202636

        _ => Err(ApplicationError::RuleNotApplicable),

302

303

8222390

304

305

/**

306

 * Evaluate Not expressions with constant bools

307

 * ```text

308

 * not(true) = false

309

1

 * not(false) = true

310

1

 * ```

311

1

*/

312

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

313

8222390

fn evaluate_constant_not(expr: &Expr, _: &Model) -> ApplicationResult {

314

8222390

    match expr {

315

527

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

316

            FactorE(metadata, Literal(Bool(val))) => Ok(Reduction::pure(FactorE(

317

                metadata.clone_dirty(),

318

                Literal(Bool(!val)),

319

            ))),

320

527

            _ => Err(ApplicationError::RuleNotApplicable),

321

},

322

8221863

        _ => Err(ApplicationError::RuleNotApplicable),

323

324

8222390

325

326

/**

327

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

328

 * ```text

329

1

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

330

1

 * ```

331

1

*/

332

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

333

8222390

fn min_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult {

334

8222390

    match expr {

335

119

        Min(metadata, exprs) => {

336

119

            let new_name = mdl.gensym();

337

119

338

119

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

339

119

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

340

357

            for e in exprs {

341

238

                new_top.push(Leq(

342

238

                    Metadata::new(),

343

238

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

344

238

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

345

238

));

346

238

                disjunction.push(Eq(

347

238

                    Metadata::new(),

348

238

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

349

238

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

350

238

));

351

238

352

119

            new_top.push(Or(Metadata::new(), disjunction));

353

119

354

119

            let mut new_vars = SymbolTable::new();

355

119

            let domain = expr

356

119

                .domain_of(&mdl.variables)

357

119

                .ok_or(ApplicationError::DomainError)?;

358

119

            new_vars.insert(new_name.clone(), DecisionVariable::new(domain));

359

119

360

119

            Ok(Reduction::new(

361

119

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

362

119

                And(metadata.clone_dirty(), new_top),

363

119

                new_vars,

364

119

))

365

366

8222271

        _ => Err(ApplicationError::RuleNotApplicable),

367

368

8222390

369

370

/**

371

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

372

 * ```text

373

1

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

374

1

 * ```

375

1

*/

376

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

377

8222390

fn max_to_var(expr: &Expr, mdl: &Model) -> ApplicationResult {

378

8222390

    match expr {

379

68

        Max(metadata, exprs) => {

380

68

            let new_name = mdl.gensym();

381

68

382

68

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

383

68

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

384

204

            for e in exprs {

385

136

                new_top.push(Geq(

386

136

                    Metadata::new(),

387

136

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

388

136

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

389

136

));

390

136

                disjunction.push(Eq(

391

136

                    Metadata::new(),

392

136

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

393

136

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

394

136

));

395

136

396

68

            new_top.push(Or(Metadata::new(), disjunction));

397

68

398

68

            let mut new_vars = SymbolTable::new();

399

68

            let domain = expr

400

68

                .domain_of(&mdl.variables)

401

68

                .ok_or(ApplicationError::DomainError)?;

402

68

            new_vars.insert(new_name.clone(), DecisionVariable::new(domain));

403

68

404

68

            Ok(Reduction::new(

405

68

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

406

68

                And(metadata.clone_dirty(), new_top),

407

68

                new_vars,

408

68

))

409

410

8222322

        _ => Err(ApplicationError::RuleNotApplicable),

411

412

8222390

413

414

/**

415

* Apply the Distributive Law to expressions like `Or([..., And(a, b)])`

416

417

* ```text

418

1

* or(and(a, b), c) = and(or(a, c), or(b, c))

419

1

* ```

420

1

*/

421

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

422

8222407

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

423

428723

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

424

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

425

1657245

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

426

1657245

            if let And(_, _) = e {

427

3944

                return Some(i);

428

1653301

429

430

424779

        None

431

428723

432

433

8222407

    match expr {

434

428723

        Or(_, exprs) => match find_and(exprs) {

435

3944

            Some(idx) => {

436

3944

                let mut rest = exprs.clone();

437

3944

                let and_expr = rest.remove(idx);

438

3944

439

3944

                match and_expr {

440

3944

                    And(metadata, and_exprs) => {

441

3944

                        let mut new_and_contents = Vec::new();

442

443

11832

                        for e in and_exprs {

444

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

445

7888

                            let mut new_or_contents = rest.clone();

446

7888

                            new_or_contents.push(e.clone());

447

7888

                            new_and_contents.push(Or(metadata.clone_dirty(), new_or_contents))

448

449

450

3944

                        Ok(Reduction::pure(And(

451

3944

                            metadata.clone_dirty(),

452

3944

                            new_and_contents,

453

3944

)))

454

455

                    _ => Err(ApplicationError::RuleNotApplicable),

456

457

458

424779

            None => Err(ApplicationError::RuleNotApplicable),

459

},

460

7793684

        _ => Err(ApplicationError::RuleNotApplicable),

461

462

8222407

463

464

/**

465

* Distribute `not` over `and` (De Morgan's Law):

466

467

* ```text

468

1

* not(and(a, b)) = or(not a, not b)

469

1

* ```

470

1

*/

471

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

472

8222424

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

473

34239853

    for child in expr.universe() {

474

34239853

        if matches!(child, Expr::UnsafeDiv(_, _, _) | Expr::Bubble(_, _, _)) {

475

1598

            return Err(RuleNotApplicable);

476

34238255

477

478

8220826

    match expr {

479

306

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

480

136

            And(metadata, exprs) => {

481

136

                if exprs.len() == 1 {

482

51

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

483

51

                    return Ok(Reduction::pure(Not(

484

51

                        Metadata::new(),

485

51

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

486

51

                    )));

487

85

488

85

                let mut new_exprs = Vec::new();

489

255

                for e in exprs {

490

170

                    new_exprs.push(Not(metadata.clone(), Box::new(e.clone())));

491

170

492

85

                Ok(Reduction::pure(Or(metadata.clone(), new_exprs)))

493

494

170

            _ => Err(ApplicationError::RuleNotApplicable),

495

},

496

8220520

        _ => Err(ApplicationError::RuleNotApplicable),

497

498

8222424

499

500

/**

501

* Distribute `not` over `or` (De Morgan's Law):

502

503

* ```text

504

1

* not(or(a, b)) = and(not a, not b)

505

1

* ```

506

1

*/

507

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

508

8222424

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

509

8222424

    match expr {

510

561

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

511

17

            Or(metadata, exprs) => {

512

17

                if exprs.len() == 1 {

513

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

514

                    return Ok(Reduction::pure(Not(

515

                        Metadata::new(),

516

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

517

                    )));

518

17

519

17

                let mut new_exprs = Vec::new();

520

51

                for e in exprs {

521

34

                    new_exprs.push(Not(metadata.clone(), Box::new(e.clone())));

522

34

523

17

                Ok(Reduction::pure(And(metadata.clone(), new_exprs)))

524

525

544

            _ => Err(ApplicationError::RuleNotApplicable),

526

},

527

8221863

        _ => Err(ApplicationError::RuleNotApplicable),

528

529

8222424

530

531

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

532

8222390

fn negated_neq_to_eq(expr: &Expr, _: &Model) -> ApplicationResult {

533

8222390

    match expr {

534

527

        Not(_, a) => match a.as_ref() {

535

68

            Neq(_, b, c) if (!b.can_be_undefined() && !c.can_be_undefined()) => {

536

68

                Ok(Reduction::pure(Eq(Metadata::new(), b.clone(), c.clone())))

537

538

459

            _ => Err(RuleNotApplicable),

539

},

540

8221863

        _ => Err(RuleNotApplicable),

541

542

8222390

543

544

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

545

8222390

fn negated_eq_to_neq(expr: &Expr, _: &Model) -> ApplicationResult {

546

8222390

    match expr {

547

527

        Not(_, a) => match a.as_ref() {

548

170

            Eq(_, b, c) if (!b.can_be_undefined() && !c.can_be_undefined()) => {

549

51

                Ok(Reduction::pure(Neq(Metadata::new(), b.clone(), c.clone())))

550

551

476

            _ => Err(RuleNotApplicable),

552

},

553

8221863

        _ => Err(RuleNotApplicable),

554

555

8222390