Grcov report - base.rs

1

use conjure_core::ast::{

2

    Constant as Const, DecisionVariable, Domain, Expression as Expr, Range, SymbolTable,

3

};

4

use conjure_core::metadata::Metadata;

5

use conjure_core::rule_engine::{

6

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

7

};

8

use conjure_core::Model;

9

use uniplate::biplate::Uniplate;

10

11

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

12

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

13

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

14

15

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

16

17

/**

18

 * Remove nothing's from expressions:

19

 * ```text

20

 * and([a, nothing, b]) = and([a, b])

21

 * sum([a, nothing, b]) = sum([a, b])

22

 * sum_leq([a, nothing, b], c) = sum_leq([a, b], c)

23

 * ...

24

 * ```

25

*/

26

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

27

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

28

    fn remove_nothings(exprs: Vec<Expr>) -> Result<Vec<Expr>, ApplicationError> {

29

        let mut changed = false;

30

        let mut new_exprs = Vec::new();

31

32

        for e in exprs {

33

            match e.clone() {

34

                Expr::Nothing => {

35

                    changed = true;

36

37

                _ => new_exprs.push(e),

38

39

40

41

        if changed {

42

            Ok(new_exprs)

43

        } else {

44

            Err(ApplicationError::RuleNotApplicable)

45

46

47

48

    fn get_lhs_rhs(sub: Vec<Expr>) -> (Vec<Expr>, Box<Expr>) {

49

        if sub.is_empty() {

50

            return (Vec::new(), Box::new(Expr::Nothing));

51

52

53

        let lhs = sub[..(sub.len() - 1)].to_vec();

54

        let rhs = Box::new(sub[sub.len() - 1].clone());

55

        (lhs, rhs)

56

57

58

    // FIXME (niklasdewally): temporary conversion until I get the Uniplate APIs figured out

59

    // Uniplate *should* support Vec<> not im::Vector

60

    let new_sub = remove_nothings(expr.children().into_iter().collect())?;

61

62

    match expr {

63

        Expr::And(md, _) => Ok(Reduction::pure(Expr::And(md.clone(), new_sub))),

64

        Expr::Or(md, _) => Ok(Reduction::pure(Expr::Or(md.clone(), new_sub))),

65

        Expr::Sum(md, _) => Ok(Reduction::pure(Expr::Sum(md.clone(), new_sub))),

66

        Expr::SumEq(md, _, _) => {

67

            let (lhs, rhs) = get_lhs_rhs(new_sub);

68

            Ok(Reduction::pure(Expr::SumEq(md.clone(), lhs, rhs)))

69

70

        Expr::SumLeq(md, _lhs, _rhs) => {

71

            let (lhs, rhs) = get_lhs_rhs(new_sub);

72

            Ok(Reduction::pure(Expr::SumLeq(md.clone(), lhs, rhs)))

73

74

        Expr::SumGeq(md, _lhs, _rhs) => {

75

            let (lhs, rhs) = get_lhs_rhs(new_sub);

76

            Ok(Reduction::pure(Expr::SumGeq(md.clone(), lhs, rhs)))

77

78

        _ => Err(ApplicationError::RuleNotApplicable),

79

80

81

82

/**

83

 * Remove empty expressions:

84

 * ```text

85

 * [] = Nothing

86

 * ```

87

*/

88

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

89

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

90

    match expr {

91

        Expr::Nothing | Expr::Reference(_, _) | Expr::Constant(_, _) => {

92

            Err(ApplicationError::RuleNotApplicable)

93

94

        _ => {

95

            if expr.children().is_empty() {

96

                Ok(Reduction::pure(Expr::Nothing))

97

            } else {

98

                Err(ApplicationError::RuleNotApplicable)

99

100

101

102

103

104

/**

105

 * Evaluate sum of constants:

106

 * ```text

107

 * sum([1, 2, 3]) = 6

108

 * ```

109

*/

110

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

111

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

112

    match expr {

113

        Expr::Sum(_, exprs) => {

114

            let mut sum = 0;

115

            let mut new_exprs = Vec::new();

116

            let mut changed = false;

117

            for e in exprs {

118

                match e {

119

                    Expr::Constant(_metadata, Const::Int(i)) => {

120

                        sum += i;

121

                        changed = true;

122

123

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

124

125

126

            if !changed {

127

                return Err(ApplicationError::RuleNotApplicable);

128

129

            // TODO (kf77): Get existing metadata instead of creating a new one

130

            new_exprs.push(Expr::Constant(Metadata::new(), Const::Int(sum)));

131

            Ok(Reduction::pure(Expr::Sum(Metadata::new(), new_exprs))) // Let other rules handle only one Expr being contained in the sum

132

133

        _ => Err(ApplicationError::RuleNotApplicable),

134

135

136

137

/**

138

 * Unwrap trivial sums:

139

 * ```text

140

 * sum([a]) = a

141

 * ```

142

*/

143

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

144

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

145

    match expr {

146

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

147

        _ => Err(ApplicationError::RuleNotApplicable),

148

149

150

151

/**

152

 * Flatten nested sums:

153

 * ```text

154

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

155

 * ```

156

*/

157

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

158

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

159

    match expr {

160

        Expr::Sum(metadata, exprs) => {

161

            let mut new_exprs = Vec::new();

162

            let mut changed = false;

163

            for e in exprs {

164

                match e {

165

                    Expr::Sum(_, sub_exprs) => {

166

                        changed = true;

167

                        for e in sub_exprs {

168

                            new_exprs.push(e.clone());

169

170

171

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

172

173

174

            if !changed {

175

                return Err(ApplicationError::RuleNotApplicable);

176

177

            Ok(Reduction::pure(Expr::Sum(

178

                metadata.clone_dirty(),

179

                new_exprs,

180

)))

181

182

        _ => Err(ApplicationError::RuleNotApplicable),

183

184

185

186

/**

187

* Unwrap nested `or`

188

189

* ```text

190

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

191

* ```

192

*/

193

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

194

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

195

    match expr {

196

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

197

            let mut new_exprs = Vec::new();

198

            let mut changed = false;

199

            for e in exprs {

200

                match e {

201

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

202

                        changed = true;

203

                        for e in exprs {

204

                            new_exprs.push(e.clone());

205

206

207

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

208

209

210

            if !changed {

211

                return Err(ApplicationError::RuleNotApplicable);

212

213

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

214

215

        _ => Err(ApplicationError::RuleNotApplicable),

216

217

218

219

/**

220

* Unwrap nested `and`

221

222

* ```text

223

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

224

* ```

225

*/

226

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

227

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

228

    match expr {

229

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

230

            let mut new_exprs = Vec::new();

231

            let mut changed = false;

232

            for e in exprs {

233

                match e {

234

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

235

                        changed = true;

236

                        for e in exprs {

237

                            new_exprs.push(e.clone());

238

239

240

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

241

242

243

            if !changed {

244

                return Err(ApplicationError::RuleNotApplicable);

245

246

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

247

                metadata.clone_dirty(),

248

                new_exprs,

249

)))

250

251

        _ => Err(ApplicationError::RuleNotApplicable),

252

253

254

255

/**

256

* Remove double negation:

257

258

* ```text

259

* not(not(a)) = a

260

* ```

261

*/

262

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

263

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

264

    match expr {

265

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

266

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

267

            _ => Err(ApplicationError::RuleNotApplicable),

268

},

269

        _ => Err(ApplicationError::RuleNotApplicable),

270

271

272

273

/**

274

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

275

 * ```text

276

 * and([a]) = a

277

 * ```

278

*/

279

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

280

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

281

    match expr {

282

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

283

            if exprs.len() == 1 {

284

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

285

286

            Err(ApplicationError::RuleNotApplicable)

287

288

        _ => Err(ApplicationError::RuleNotApplicable),

289

290

291

292

/**

293

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

294

 * ```text

295

 * or([a]) = a

296

 * ```

297

*/

298

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

299

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

300

    match expr {

301

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

302

            if exprs.len() == 1 {

303

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

304

305

            Err(ApplicationError::RuleNotApplicable)

306

307

        _ => Err(ApplicationError::RuleNotApplicable),

308

309

310

311

/**

312

 * Remove constant bools from or expressions

313

 * ```text

314

 * or([true, a]) = true

315

 * or([false, a]) = a

316

 * ```

317

*/

318

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

319

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

320

    match expr {

321

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

322

            let mut new_exprs = Vec::new();

323

            let mut changed = false;

324

            for e in exprs {

325

                match e {

326

                    Expr::Constant(metadata, Const::Bool(val)) => {

327

                        if *val {

328

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

329

                            return Ok(Reduction::pure(Expr::Constant(

330

                                metadata.clone_dirty(),

331

                                Const::Bool(true),

332

                            )));

333

                        } else {

334

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

335

                            changed = true;

336

337

338

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

339

340

341

            if !changed {

342

                return Err(ApplicationError::RuleNotApplicable);

343

344

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

345

346

        _ => Err(ApplicationError::RuleNotApplicable),

347

348

349

350

/**

351

 * Remove constant bools from and expressions

352

 * ```text

353

 * and([true, a]) = a

354

 * and([false, a]) = false

355

 * ```

356

*/

357

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

358

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

359

    match expr {

360

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

361

            let mut new_exprs = Vec::new();

362

            let mut changed = false;

363

            for e in exprs {

364

                match e {

365

                    Expr::Constant(metadata, Const::Bool(val)) => {

366

                        if !*val {

367

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

368

                            return Ok(Reduction::pure(Expr::Constant(

369

                                metadata.clone_dirty(),

370

                                Const::Bool(false),

371

                            )));

372

                        } else {

373

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

374

                            changed = true;

375

376

377

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

378

379

380

            if !changed {

381

                return Err(ApplicationError::RuleNotApplicable);

382

383

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

384

                metadata.clone_dirty(),

385

                new_exprs,

386

)))

387

388

        _ => Err(ApplicationError::RuleNotApplicable),

389

390

391

392

/**

393

 * Evaluate Not expressions with constant bools

394

 * ```text

395

 * not(true) = false

396

 * not(false) = true

397

 * ```

398

*/

399

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

400

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

401

    match expr {

402

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

403

            Expr::Constant(metadata, Const::Bool(val)) => Ok(Reduction::pure(Expr::Constant(

404

                metadata.clone_dirty(),

405

                Const::Bool(!val),

406

            ))),

407

            _ => Err(ApplicationError::RuleNotApplicable),

408

},

409

        _ => Err(ApplicationError::RuleNotApplicable),

410

411

412

413

/**

414

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

415

 * ```text

416

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

417

 * ```

418

*/

419

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

420

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

421

    match expr {

422

        Expr::Min(metadata, exprs) => {

423

            let new_name = mdl.gensym();

424

425

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

426

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

427

            for e in exprs {

428

                new_top.push(Expr::Leq(

429

                    Metadata::new(),

430

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

431

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

432

));

433

                disjunction.push(Expr::Eq(

434

                    Metadata::new(),

435

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

436

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

437

));

438

439

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

440

441

            let mut new_vars = SymbolTable::new();

442

            let domain = expr

443

                .domain_of(&mdl.variables)

444

                .ok_or(ApplicationError::DomainError)?;

445

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

446

447

            Ok(Reduction::new(

448

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

449

                Expr::And(metadata.clone_dirty(), new_top),

450

                new_vars,

451

))

452

453

        _ => Err(ApplicationError::RuleNotApplicable),

454

455

456

457

/**

458

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

459

460

* ```text

461

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

462

* ```

463

*/

464

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

465

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

466

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

467

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

468

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

469

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

470

                return Some(i);

471

472

473

        None

474

475

476

    match expr {

477

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

478

            Some(idx) => {

479

                let mut rest = exprs.clone();

480

                let and_expr = rest.remove(idx);

481

482

                match and_expr {

483

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

484

                        let mut new_and_contents = Vec::new();

485

486

                        for e in and_exprs {

487

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

488

                            let mut new_or_contents = rest.clone();

489

                            new_or_contents.push(e.clone());

490

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

491

492

493

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

494

                            metadata.clone_dirty(),

495

                            new_and_contents,

496

)))

497

498

                    _ => Err(ApplicationError::RuleNotApplicable),

499

500

501

            None => Err(ApplicationError::RuleNotApplicable),

502

},

503

        _ => Err(ApplicationError::RuleNotApplicable),

504

505

506

507

/**

508

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

509

510

* ```text

511

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

512

* ```

513

*/

514

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

515

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

516

    match expr {

517

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

518

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

519

                if exprs.len() == 1 {

520

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

521

                    return Ok(Reduction::pure(Expr::Not(

522

                        Metadata::new(),

523

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

524

                    )));

525

526

                let mut new_exprs = Vec::new();

527

                for e in exprs {

528

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

529

530

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

531

532

            _ => Err(ApplicationError::RuleNotApplicable),

533

},

534

        _ => Err(ApplicationError::RuleNotApplicable),

535

536

537

538

/**

539

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

540

541

* ```text

542

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

543

* ```

544

*/

545

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

546

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

547

    match expr {

548

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

549

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

550

                if exprs.len() == 1 {

551

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

552

                    return Ok(Reduction::pure(Expr::Not(

553

                        Metadata::new(),

554

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

555

                    )));

556

557

                let mut new_exprs = Vec::new();

558

                for e in exprs {

559

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

560

561

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

562

563

            _ => Err(ApplicationError::RuleNotApplicable),

564

},

565

        _ => Err(ApplicationError::RuleNotApplicable),

566

567