Grcov report - base.rs

1

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

2

use conjure_core::metadata::Metadata;

3

use conjure_core::rule_engine::{

4

    register_rule, register_rule_set, ApplicationError, ApplicationError::RuleNotApplicable,

5

    ApplicationResult, Reduction,

6

};

7

use conjure_core::Model;

8

use uniplate::Uniplate;

9

10

use Atom::*;

11

use Expr::*;

12

use Lit::*;

13

14

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

15

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

16

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

17

18

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

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

18

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

32

    // excluded expressions

33

9

    if matches!(

34

18

        expr,

35

        Atomic(_, _)

36

            | WatchedLiteral(_, _, _)

37

            | DivEqUndefZero(_, _, _, _)

38

            | ModuloEqUndefZero(_, _, _, _)

39

) {

40

9

        return Err(ApplicationError::RuleNotApplicable);

41

9

42

9

43

9

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

44

        return Err(ApplicationError::RuleNotApplicable);

45

9

46

47

9

    let new_expr = match expr {

48

9

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

49

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

50

};

51

52

9

    Ok(Reduction::pure(new_expr))

53

18

54

55

/**

56

 * Unwrap trivial sums:

57

 * ```text

58

 * sum([a]) = a

59

 * ```

60

*/

61

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

62

18

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

63

    match expr {

64

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

65

18

        _ => Err(ApplicationError::RuleNotApplicable),

66

67

18

68

69

/**

70

 * Flatten nested sums:

71

 * ```text

72

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

73

 * ```

74

*/

75

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

76

18

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

77

18

    match expr {

78

        Sum(metadata, exprs) => {

79

            let mut new_exprs = Vec::new();

80

            let mut changed = false;

81

            for e in exprs {

82

                match e {

83

                    Sum(_, sub_exprs) => {

84

                        changed = true;

85

                        for e in sub_exprs {

86

                            new_exprs.push(e.clone());

87

88

89

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

90

91

92

            if !changed {

93

                return Err(ApplicationError::RuleNotApplicable);

94

95

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

96

97

18

        _ => Err(ApplicationError::RuleNotApplicable),

98

99

18

100

101

/**

102

* Unwrap nested `or`

103

104

* ```text

105

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

106

* ```

107

*/

108

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

109

18

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

110

18

    match expr {

111

9

        Or(metadata, exprs) => {

112

9

            let mut new_exprs = Vec::new();

113

9

            let mut changed = false;

114

9

            for e in exprs {

115

                match e {

116

                    Or(_, exprs) => {

117

                        changed = true;

118

                        for e in exprs {

119

                            new_exprs.push(e.clone());

120

121

122

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

123

124

125

9

            if !changed {

126

9

                return Err(ApplicationError::RuleNotApplicable);

127

128

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

129

130

9

        _ => Err(ApplicationError::RuleNotApplicable),

131

132

18

133

134

/**

135

* Unwrap nested `and`

136

137

* ```text

138

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

139

* ```

140

*/

141

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

142

18

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

143

18

    match expr {

144

        And(metadata, exprs) => {

145

            let mut new_exprs = Vec::new();

146

            let mut changed = false;

147

            for e in exprs {

148

                match e {

149

                    And(_, exprs) => {

150

                        changed = true;

151

                        for e in exprs {

152

                            new_exprs.push(e.clone());

153

154

155

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

156

157

158

            if !changed {

159

                return Err(ApplicationError::RuleNotApplicable);

160

161

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

162

163

18

        _ => Err(ApplicationError::RuleNotApplicable),

164

165

18

166

167

/**

168

* Remove double negation:

169

170

* ```text

171

* not(not(a)) = a

172

* ```

173

*/

174

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

175

18

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

176

18

    match expr {

177

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

178

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

179

            _ => Err(ApplicationError::RuleNotApplicable),

180

},

181

18

        _ => Err(ApplicationError::RuleNotApplicable),

182

183

18

184

185

/**

186

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

187

 * ```text

188

 * and([a]) = a

189

 * ```

190

*/

191

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

192

18

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

193

18

    match expr {

194

        And(_, exprs) => {

195

            if exprs.len() == 1 {

196

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

197

198

            Err(ApplicationError::RuleNotApplicable)

199

200

18

        _ => Err(ApplicationError::RuleNotApplicable),

201

202

18

203

204

/**

205

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

206

 * ```text

207

 * or([a]) = a

208

 * ```

209

*/

210

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

211

18

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

212

9

    match expr {

213

9

        // do not conflict with unwrap_nested_or rule.

214

9

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

215

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

216

217

18

        _ => Err(ApplicationError::RuleNotApplicable),

218

219

18

220

221

/**

222

 * Remove constant bools from or expressions

223

 * ```text

224

 * or([true, a]) = true

225

 * or([false, a]) = a

226

 * ```

227

*/

228

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

229

18

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

230

18

    match expr {

231

9

        Or(metadata, exprs) => {

232

9

            let mut new_exprs = Vec::new();

233

9

            let mut changed = false;

234

9

            for e in exprs {

235

                match e {

236

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

237

                        if *val {

238

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

239

                            return Ok(Reduction::pure(Atomic(

240

                                metadata.clone_dirty(),

241

                                Literal(Bool(true)),

242

                            )));

243

                        } else {

244

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

245

                            changed = true;

246

247

248

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

249

250

251

9

            if !changed {

252

9

                return Err(ApplicationError::RuleNotApplicable);

253

254

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

255

256

9

        _ => Err(ApplicationError::RuleNotApplicable),

257

258

18

259

260

/**

261

 * Remove constant bools from and expressions

262

 * ```text

263

 * and([true, a]) = a

264

 * and([false, a]) = false

265

 * ```

266

*/

267

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

268

18

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

269

18

    match expr {

270

        And(metadata, exprs) => {

271

            let mut new_exprs = Vec::new();

272

            let mut changed = false;

273

            for e in exprs {

274

                match e {

275

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

276

                        if !*val {

277

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

278

                            return Ok(Reduction::pure(Atomic(

279

                                metadata.clone_dirty(),

280

                                Literal(Bool(false)),

281

                            )));

282

                        } else {

283

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

284

                            changed = true;

285

286

287

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

288

289

290

            if !changed {

291

                return Err(ApplicationError::RuleNotApplicable);

292

293

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

294

295

18

        _ => Err(ApplicationError::RuleNotApplicable),

296

297

18

298

299

/**

300

 * Evaluate Not expressions with constant bools

301

 * ```text

302

 * not(true) = false

303

 * not(false) = true

304

 * ```

305

*/

306

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

307

18

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

308

18

    match expr {

309

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

310

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

311

                metadata.clone_dirty(),

312

                Literal(Bool(!val)),

313

            ))),

314

            _ => Err(ApplicationError::RuleNotApplicable),

315

},

316

18

        _ => Err(ApplicationError::RuleNotApplicable),

317

318

18

319

320

/**

321

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

322

 * ```text

323

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

324

 * ```

325

*/

326

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

327

18

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

328

18

    match expr {

329

        Min(metadata, exprs) => {

330

            let new_name = mdl.gensym();

331

332

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

333

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

334

            for e in exprs {

335

                new_top.push(Leq(

336

                    Metadata::new(),

337

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

338

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

339

));

340

                disjunction.push(Eq(

341

                    Metadata::new(),

342

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

343

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

344

));

345

346

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

347

348

            let mut new_vars = SymbolTable::new();

349

            let domain = expr

350

                .domain_of(&mdl.variables)

351

                .ok_or(ApplicationError::DomainError)?;

352

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

353

354

            Ok(Reduction::new(

355

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

356

                vec![],

357

                new_vars,

358

))

359

360

18

        _ => Err(ApplicationError::RuleNotApplicable),

361

362

18

363

364

/**

365

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

366

 * ```text

367

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

368

 * ```

369

*/

370

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

371

18

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

372

18

    match expr {

373

        Max(metadata, exprs) => {

374

            let new_name = mdl.gensym();

375

376

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

377

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

378

            for e in exprs {

379

                new_top.push(Geq(

380

                    Metadata::new(),

381

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

382

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

383

));

384

                disjunction.push(Eq(

385

                    Metadata::new(),

386

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

387

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

388

));

389

390

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

391

392

            let mut new_vars = SymbolTable::new();

393

            let domain = expr

394

                .domain_of(&mdl.variables)

395

                .ok_or(ApplicationError::DomainError)?;

396

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

397

398

            Ok(Reduction::new(

399

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

400

                vec![],

401

                new_vars,

402

))

403

404

18

        _ => Err(ApplicationError::RuleNotApplicable),

405

406

18

407

408

/**

409

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

410

411

* ```text

412

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

413

* ```

414

*/

415

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

416

18

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

417

9

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

418

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

419

9

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

420

            if let And(_, _) = e {

421

                return Some(i);

422

423

424

9

        None

425

9

426

427

18

    match expr {

428

9

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

429

            Some(idx) => {

430

                let mut rest = exprs.clone();

431

                let and_expr = rest.remove(idx);

432

433

                match and_expr {

434

                    And(metadata, and_exprs) => {

435

                        let mut new_and_contents = Vec::new();

436

437

                        for e in and_exprs {

438

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

439

                            let mut new_or_contents = rest.clone();

440

                            new_or_contents.push(e.clone());

441

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

442

443

444

                        Ok(Reduction::pure(And(

445

                            metadata.clone_dirty(),

446

                            new_and_contents,

447

)))

448

449

                    _ => Err(ApplicationError::RuleNotApplicable),

450

451

452

9

            None => Err(ApplicationError::RuleNotApplicable),

453

},

454

9

        _ => Err(ApplicationError::RuleNotApplicable),

455

456

18

457

458

/**

459

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

460

461

* ```text

462

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

463

* ```

464

*/

465

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

466

18

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

467

18

    for child in expr.universe() {

468

18

        if matches!(

469

18

            child,

470

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

471

) {

472

            return Err(RuleNotApplicable);

473

18

474

475

18

    match expr {

476

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

477

            And(metadata, exprs) => {

478

                if exprs.len() == 1 {

479

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

480

                    return Ok(Reduction::pure(Not(

481

                        Metadata::new(),

482

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

483

                    )));

484

485

                let mut new_exprs = Vec::new();

486

                for e in exprs {

487

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

488

489

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

490

491

            _ => Err(ApplicationError::RuleNotApplicable),

492

},

493

18

        _ => Err(ApplicationError::RuleNotApplicable),

494

495

18

496

497

/**

498

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

499

500

* ```text

501

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

502

* ```

503

*/

504

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

505

18

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

506

18

    match expr {

507

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

508

            Or(metadata, exprs) => {

509

                if exprs.len() == 1 {

510

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

511

                    return Ok(Reduction::pure(Not(

512

                        Metadata::new(),

513

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

514

                    )));

515

516

                let mut new_exprs = Vec::new();

517

                for e in exprs {

518

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

519

520

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

521

522

            _ => Err(ApplicationError::RuleNotApplicable),

523

},

524

18

        _ => Err(ApplicationError::RuleNotApplicable),

525

526

18

527

528

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

529

18

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

530

18

    match expr {

531

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

532

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

533

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

534

535

            _ => Err(RuleNotApplicable),

536

},

537

18

        _ => Err(RuleNotApplicable),

538

539

18

540

541

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

542

18

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

543

18

    match expr {

544

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

545

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

546

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

547

548

            _ => Err(RuleNotApplicable),

549

},

550

18

        _ => Err(RuleNotApplicable),

551

552

18