Grcov report - rewrite

1

use conjure_cp::{

2

    Model,

3

    ast::{

4

        AbstractLiteral, Atom, DeclarationPtr, Domain, Expression, Field, Literal, Metadata, Moo,

5

        Name, Range, Reference, SymbolTable, eval_constant, normalise_evaluator_local,

6

},

7

    into_matrix_expr, matrix_expr,

8

    rule_engine::{Rule, get_all_rules, get_rule_by_name, resolve_rule_sets, rewrite_model},

9

    settings::{QuantifiedExpander, SolverFamily, set_comprehension_expander},

10

    solver::{Solver, adaptors},

11

};

12

#[allow(unused_imports)]

13

#[allow(clippy::single_component_path_imports)] // ensure this is linked so we can lookup rules

14

use conjure_cp_rules;

15

use pretty_assertions::assert_eq;

16

use std::process::exit;

17

use uniplate::Uniplate;

18

19

#[test]

20

1

fn rules_present() {

21

1

    let rules = get_all_rules();

22

1

    assert!(!rules.is_empty());

23

1

24

25

#[test]

26

1

fn sum_of_constants() {

27

1

    let valid_sum_expression = Expression::Sum(

28

1

        Metadata::new(),

29

1

        Moo::new(matrix_expr![

30

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

31

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),

32

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(3))),

33

1

]),

34

1

);

35

36

1

    let invalid_sum_expression = Expression::Sum(

37

1

        Metadata::new(),

38

1

        Moo::new(matrix_expr![

39

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

40

1

            Expression::Atomic(

41

1

                Metadata::new(),

42

1

                Atom::Reference(Reference::new(DeclarationPtr::new_find(

43

1

                    Name::user("a"),

44

1

                    Domain::bool()

45

1

                ))),

46

1

),

47

1

]),

48

1

);

49

50

1

    assert_eq!(evaluate_sum_of_constants(&valid_sum_expression), Some(6));

51

52

1

    assert_eq!(evaluate_sum_of_constants(&invalid_sum_expression), None);

53

1

54

55

4

fn evaluate_sum_of_constants(expr: &Expression) -> Option<i32> {

56

4

    match expr {

57

        Expression::Sum(_metadata, expressions) => {

58

4

            let expressions = (**expressions).clone().unwrap_list()?;

59

4

            let mut sum = 0;

60

4

            for e in expressions {

61

10

                match e {

62

                    Expression::Atomic(_, Atom::Literal(Literal::Int(value))) => {

63

8

                        sum += value;

64

65

2

                    _ => return None,

66

67

68

2

            Some(sum)

69

70

        _ => None,

71

72

4

73

74

#[test]

75

1

fn recursive_sum_of_constants() {

76

1

    let a = Atom::Reference(Reference::new(DeclarationPtr::new_find(

77

1

        Name::user("a"),

78

1

        Domain::int(vec![Range::Bounded(1, 5)]),

79

1

    )));

80

1

    let complex_expression = Expression::Eq(

81

1

        Metadata::new(),

82

1

        Moo::new(Expression::Sum(

83

1

            Metadata::new(),

84

1

            Moo::new(matrix_expr![

85

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

86

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),

87

1

                Expression::Sum(

88

1

                    Metadata::new(),

89

1

                    Moo::new(matrix_expr![

90

1

                        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

91

1

                        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),

92

1

]),

93

1

),

94

1

                Expression::Atomic(Metadata::new(), a.clone()),

95

1

]),

96

1

)),

97

1

        Moo::new(Expression::Atomic(

98

1

            Metadata::new(),

99

1

            Atom::Literal(Literal::Int(3)),

100

1

)),

101

1

);

102

1

    let correct_simplified_expression = Expression::Eq(

103

1

        Metadata::new(),

104

1

        Moo::new(Expression::Sum(

105

1

            Metadata::new(),

106

1

            Moo::new(matrix_expr![

107

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

108

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),

109

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(3))),

110

1

                Expression::Atomic(Metadata::new(), a),

111

1

]),

112

1

)),

113

1

        Moo::new(Expression::Atomic(

114

1

            Metadata::new(),

115

1

            Atom::Literal(Literal::Int(3)),

116

1

)),

117

1

);

118

119

1

    let simplified_expression = simplify_expression(complex_expression);

120

1

    assert_eq!(simplified_expression, correct_simplified_expression);

121

1

122

123

7

fn simplify_expression(expr: Expression) -> Expression {

124

7

    match expr {

125

        Expression::Sum(_metadata, expressions) => {

126

2

            let expressions = Moo::unwrap_or_clone(expressions).unwrap_list().unwrap();

127

2

            if let Some(result) = evaluate_sum_of_constants(&Expression::Sum(

128

2

                Metadata::new(),

129

2

                Moo::new(into_matrix_expr![expressions.clone()]),

130

2

            )) {

131

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(result)))

132

            } else {

133

1

                Expression::Sum(

134

1

                    Metadata::new(),

135

1

                    Moo::new(into_matrix_expr![

136

1

                        expressions.into_iter().map(simplify_expression).collect()

137

1

]),

138

1

139

140

141

1

        Expression::Eq(_metadata, left, right) => Expression::Eq(

142

1

            Metadata::new(),

143

1

            Moo::new(simplify_expression(Moo::unwrap_or_clone(left))),

144

1

            Moo::new(simplify_expression(Moo::unwrap_or_clone(right))),

145

1

),

146

        Expression::Geq(_metadata, left, right) => Expression::Geq(

147

            Metadata::new(),

148

            Moo::new(simplify_expression(Moo::unwrap_or_clone(left))),

149

            Moo::new(simplify_expression(Moo::unwrap_or_clone(right))),

150

),

151

4

        _ => expr,

152

153

7

154

155

#[test]

156

1

fn rule_sum_constants() {

157

1

    let mut expr = Expression::Sum(

158

1

        Metadata::new(),

159

1

        Moo::new(matrix_expr![

160

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

161

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),

162

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(3))),

163

1

]),

164

1

);

165

166

1

    expr = normalise_evaluator_local(&expr).unwrap();

167

168

1

    assert_eq!(

169

1

        expr,

170

1

        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(6)))

171

);

172

1

173

174

#[test]

175

1

fn rule_sum_geq() {

176

1

    let introduce_sumgeq = get_rule_by_name("introduce_weighted_sumleq_sumgeq").unwrap();

177

178

1

    let mut expr = Expression::Geq(

179

1

        Metadata::new(),

180

1

        Moo::new(Expression::Sum(

181

1

            Metadata::new(),

182

1

            Moo::new(matrix_expr![

183

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

184

1

                Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),

185

1

]),

186

1

)),

187

1

        Moo::new(Expression::Atomic(

188

1

            Metadata::new(),

189

1

            Atom::Literal(Literal::Int(3)),

190

1

)),

191

1

);

192

193

1

    expr = introduce_sumgeq

194

1

        .apply(&expr, &SymbolTable::new())

195

1

        .unwrap()

196

1

        .new_expression;

197

198

1

    assert_eq!(

199

1

        expr,

200

1

        Expression::FlatSumGeq(

201

1

            Metadata::new(),

202

1

            vec![

203

1

                Atom::Literal(Literal::Int(1)),

204

1

                Atom::Literal(Literal::Int(2)),

205

1

],

206

1

            Atom::Literal(Literal::Int(3))

207

1

208

);

209

1

210

211

///

212

/// Reduce and solve:

213

/// ```text

214

/// find a,b,c : int(1..3)

215

/// such that a + b + c <= 2 + 3 - 1

216

/// such that a < b

217

/// ```

218

#[test]

219

1

fn reduce_solve_xyz() {

220

1

    println!("Rules: {:?}", get_all_rules());

221

1

    let lt_to_leq = get_rule_by_name("lt_to_leq").unwrap();

222

1

    let leq_to_ineq = get_rule_by_name("x_leq_y_plus_k_to_ineq").unwrap();

223

1

    let introduce_sumleq = get_rule_by_name("introduce_weighted_sumleq_sumgeq").unwrap();

224

225

    // 2 + 3 - 1

226

1

    let mut expr1 = Expression::Sum(

227

1

        Metadata::new(),

228

1

        Moo::new(matrix_expr![

229

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2))),

230

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(3))),

231

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(-1))),

232

1

]),

233

1

);

234

235

1

    expr1 = normalise_evaluator_local(&expr1).unwrap();

236

1

    assert_eq!(

237

1

        expr1,

238

1

        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(4)))

239

);

240

241

1

    let a = Atom::Reference(Reference::new(DeclarationPtr::new_find(

242

1

        Name::user("a"),

243

1

        Domain::int(vec![Range::Bounded(1, 5)]),

244

1

    )));

245

1

    let b = Atom::Reference(Reference::new(DeclarationPtr::new_find(

246

1

        Name::user("b"),

247

1

        Domain::int(vec![Range::Bounded(1, 5)]),

248

1

    )));

249

1

    let c = Atom::Reference(Reference::new(DeclarationPtr::new_find(

250

1

        Name::user("c"),

251

1

        Domain::int(vec![Range::Bounded(1, 5)]),

252

1

    )));

253

254

    // a + b + c = 4

255

1

    expr1 = Expression::Leq(

256

1

        Metadata::new(),

257

1

        Moo::new(Expression::Sum(

258

1

            Metadata::new(),

259

1

            Moo::new(matrix_expr![

260

1

                Expression::Atomic(Metadata::new(), a.clone()),

261

1

                Expression::Atomic(Metadata::new(), b.clone()),

262

1

                Expression::Atomic(Metadata::new(), c.clone()),

263

1

]),

264

1

)),

265

1

        Moo::new(expr1),

266

1

);

267

1

    expr1 = introduce_sumleq

268

1

        .apply(&expr1, &SymbolTable::new())

269

1

        .unwrap()

270

1

        .new_expression;

271

1

    assert_eq!(

272

1

        expr1,

273

1

        Expression::FlatSumLeq(

274

1

            Metadata::new(),

275

1

            vec![a.clone(), b.clone(), c],

276

1

            Atom::Literal(Literal::Int(4))

277

1

278

);

279

280

    // a < b

281

1

    let mut expr2 = Expression::Lt(

282

1

        Metadata::new(),

283

1

        Moo::new(Expression::Atomic(Metadata::new(), a.clone())),

284

1

        Moo::new(Expression::Atomic(Metadata::new(), b.clone())),

285

1

);

286

1

    expr2 = lt_to_leq

287

1

        .apply(&expr2, &SymbolTable::new())

288

1

        .unwrap()

289

1

        .new_expression;

290

291

1

    expr2 = leq_to_ineq

292

1

        .apply(&expr2, &SymbolTable::new())

293

1

        .unwrap()

294

1

        .new_expression;

295

1

    assert_eq!(

296

1

        expr2,

297

1

        Expression::FlatIneq(

298

1

            Metadata::new(),

299

1

            Moo::new(a),

300

1

            Moo::new(b),

301

1

            Box::new(Literal::Int(-1)),

302

1

303

);

304

305

1

    let mut model = Model::new(Default::default());

306

1

    *model.constraints_mut() = vec![expr1, expr2];

307

308

1

    model

309

1

        .symbols_mut()

310

1

        .insert(DeclarationPtr::new_find(

311

1

            Name::user("a"),

312

1

            Domain::int(vec![Range::Bounded(1, 3)]),

313

1

))

314

1

        .unwrap();

315

1

    model

316

1

        .symbols_mut()

317

1

        .insert(DeclarationPtr::new_find(

318

1

            Name::user("b"),

319

1

            Domain::int(vec![Range::Bounded(1, 3)]),

320

1

))

321

1

        .unwrap();

322

1

    model

323

1

        .symbols_mut()

324

1

        .insert(DeclarationPtr::new_find(

325

1

            Name::user("c"),

326

1

            Domain::int(vec![Range::Bounded(1, 3)]),

327

1

))

328

1

        .unwrap();

329

330

1

    let solver: Solver = Solver::new(adaptors::Minion::new());

331

1

    let solver = solver.load_model(model).unwrap();

332

1

    solver.solve(Box::new(|_| true)).unwrap();

333

1

334

335

#[test]

336

1

fn rule_remove_double_negation() {

337

1

    let remove_double_negation = get_rule_by_name("remove_double_negation").unwrap();

338

339

1

    let mut expr = Expression::Not(

340

1

        Metadata::new(),

341

1

        Moo::new(Expression::Not(

342

1

            Metadata::new(),

343

1

            Moo::new(Expression::Atomic(

344

1

                Metadata::new(),

345

1

                Atom::Literal(Literal::Bool(true)),

346

1

)),

347

1

)),

348

1

);

349

350

1

    expr = remove_double_negation

351

1

        .apply(&expr, &SymbolTable::new())

352

1

        .unwrap()

353

1

        .new_expression;

354

355

1

    assert_eq!(

356

1

        expr,

357

1

        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true)))

358

);

359

1

360

361

#[test]

362

1

fn remove_trivial_and_or() {

363

1

    let remove_trivial_and = get_rule_by_name("remove_unit_vector_and").unwrap();

364

1

    let remove_trivial_or = get_rule_by_name("remove_unit_vector_or").unwrap();

365

366

1

    let mut expr_and = Expression::And(

367

1

        Metadata::new(),

368

1

        Moo::new(matrix_expr![Expression::Atomic(

369

1

            Metadata::new(),

370

1

            Atom::Literal(Literal::Bool(true)),

371

1

        )]),

372

1

);

373

1

    let mut expr_or = Expression::Or(

374

1

        Metadata::new(),

375

1

        Moo::new(matrix_expr![Expression::Atomic(

376

1

            Metadata::new(),

377

1

            Atom::Literal(Literal::Bool(false)),

378

1

        )]),

379

1

);

380

381

1

    expr_and = remove_trivial_and

382

1

        .apply(&expr_and, &SymbolTable::new())

383

1

        .unwrap()

384

1

        .new_expression;

385

1

    expr_or = remove_trivial_or

386

1

        .apply(&expr_or, &SymbolTable::new())

387

1

        .unwrap()

388

1

        .new_expression;

389

390

1

    assert_eq!(

391

1

        expr_and,

392

1

        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true)))

393

);

394

1

    assert_eq!(

395

1

        expr_or,

396

1

        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false)))

397

);

398

1

399

400

#[test]

401

1

fn rule_distribute_not_over_and() {

402

1

    let distribute_not_over_and = get_rule_by_name("distribute_not_over_and").unwrap();

403

404

1

    let a = Atom::Reference(Reference::new(DeclarationPtr::new_find(

405

1

        Name::user("a"),

406

1

        Domain::bool(),

407

1

    )));

408

409

1

    let b = Atom::Reference(Reference::new(DeclarationPtr::new_find(

410

1

        Name::user("b"),

411

1

        Domain::bool(),

412

1

    )));

413

414

1

    let mut expr = Expression::Not(

415

1

        Metadata::new(),

416

1

        Moo::new(Expression::And(

417

1

            Metadata::new(),

418

1

            Moo::new(matrix_expr![

419

1

                Expression::Atomic(Metadata::new(), a.clone()),

420

1

                Expression::Atomic(Metadata::new(), b.clone()),

421

1

]),

422

1

)),

423

1

);

424

425

1

    expr = distribute_not_over_and

426

1

        .apply(&expr, &SymbolTable::new())

427

1

        .unwrap()

428

1

        .new_expression;

429

430

1

    assert_eq!(

431

1

        expr,

432

1

        Expression::Or(

433

1

            Metadata::new(),

434

1

            Moo::new(matrix_expr![

435

1

                Expression::Not(

436

1

                    Metadata::new(),

437

1

                    Moo::new(Expression::Atomic(Metadata::new(), a))

438

1

),

439

1

                Expression::Not(

440

1

                    Metadata::new(),

441

1

                    Moo::new(Expression::Atomic(Metadata::new(), b))

442

1

),

443

1

])

444

1

445

);

446

1

447

448

#[test]

449

1

fn rule_distribute_not_over_or() {

450

1

    let distribute_not_over_or = get_rule_by_name("distribute_not_over_or").unwrap();

451

452

1

    let a = Atom::Reference(Reference::new(DeclarationPtr::new_find(

453

1

        Name::user("a"),

454

1

        Domain::bool(),

455

1

    )));

456

457

1

    let b = Atom::Reference(Reference::new(DeclarationPtr::new_find(

458

1

        Name::user("b"),

459

1

        Domain::bool(),

460

1

    )));

461

462

1

    let mut expr = Expression::Not(

463

1

        Metadata::new(),

464

1

        Moo::new(Expression::Or(

465

1

            Metadata::new(),

466

1

            Moo::new(matrix_expr![

467

1

                Expression::Atomic(Metadata::new(), a.clone()),

468

1

                Expression::Atomic(Metadata::new(), b.clone()),

469

1

]),

470

1

)),

471

1

);

472

473

1

    expr = distribute_not_over_or

474

1

        .apply(&expr, &SymbolTable::new())

475

1

        .unwrap()

476

1

        .new_expression;

477

478

1

    assert_eq!(

479

1

        expr,

480

1

        Expression::And(

481

1

            Metadata::new(),

482

1

            Moo::new(matrix_expr![

483

1

                Expression::Not(

484

1

                    Metadata::new(),

485

1

                    Moo::new(Expression::Atomic(Metadata::new(), a))

486

1

),

487

1

                Expression::Not(

488

1

                    Metadata::new(),

489

1

                    Moo::new(Expression::Atomic(Metadata::new(), b))

490

1

),

491

1

])

492

1

493

);

494

1

495

496

#[test]

497

1

fn rule_distribute_not_over_and_not_changed() {

498

1

    let distribute_not_over_and = get_rule_by_name("distribute_not_over_and").unwrap();

499

500

1

    let expr = Expression::Not(

501

1

        Metadata::new(),

502

1

        Moo::new(Expression::Atomic(

503

1

            Metadata::new(),

504

1

            Atom::Reference(Reference::new(DeclarationPtr::new_find(

505

1

                Name::user("a"),

506

1

                Domain::int(vec![Range::Bounded(1, 5)]),

507

1

            ))),

508

1

)),

509

1

);

510

511

1

    let result = distribute_not_over_and.apply(&expr, &SymbolTable::new());

512

513

1

    assert!(result.is_err());

514

1

515

516

#[test]

517

1

fn rule_distribute_not_over_or_not_changed() {

518

1

    let distribute_not_over_or = get_rule_by_name("distribute_not_over_or").unwrap();

519

520

1

    let expr = Expression::Not(

521

1

        Metadata::new(),

522

1

        Moo::new(Expression::Atomic(

523

1

            Metadata::new(),

524

1

            Atom::Reference(Reference::new(DeclarationPtr::new_find(

525

1

                Name::user("a"),

526

1

                Domain::int(vec![Range::Bounded(1, 5)]),

527

1

            ))),

528

1

)),

529

1

);

530

531

1

    let result = distribute_not_over_or.apply(&expr, &SymbolTable::new());

532

533

1

    assert!(result.is_err());

534

1

535

536

#[test]

537

1

fn rule_distribute_or_over_and() {

538

1

    let distribute_or_over_and = get_rule_by_name("distribute_or_over_and").unwrap();

539

540

1

    let d1 = Atom::Reference(Reference::new(DeclarationPtr::new_find(

541

1

        Name::Machine(1),

542

1

        Domain::bool(),

543

1

    )));

544

545

1

    let d2 = Atom::Reference(Reference::new(DeclarationPtr::new_find(

546

1

        Name::Machine(2),

547

1

        Domain::bool(),

548

1

    )));

549

550

1

    let expr = Expression::Or(

551

1

        Metadata::new(),

552

1

        Moo::new(matrix_expr![

553

1

            Expression::And(

554

1

                Metadata::new(),

555

1

                Moo::new(matrix_expr![

556

1

                    Expression::Atomic(Metadata::new(), d1.clone()),

557

1

                    Expression::Atomic(Metadata::new(), d2.clone()),

558

1

]),

559

1

),

560

1

            Expression::Atomic(Metadata::new(), d2.clone()),

561

1

]),

562

1

);

563

564

1

    let red = distribute_or_over_and

565

1

        .apply(&expr, &SymbolTable::new())

566

1

        .unwrap();

567

568

1

    assert_eq!(

569

1

        red.new_expression,

570

1

        Expression::And(

571

1

            Metadata::new(),

572

1

            Moo::new(matrix_expr![

573

1

                Expression::Or(

574

1

                    Metadata::new(),

575

1

                    Moo::new(matrix_expr![

576

1

                        Expression::Atomic(Metadata::new(), d2.clone()),

577

1

                        Expression::Atomic(Metadata::new(), d1),

578

1

])

579

1

),

580

1

                Expression::Or(

581

1

                    Metadata::new(),

582

1

                    Moo::new(matrix_expr![

583

1

                        Expression::Atomic(Metadata::new(), d2.clone()),

584

1

                        Expression::Atomic(Metadata::new(), d2),

585

1

])

586

1

),

587

1

])

588

1

),

589

);

590

1

591

592

///

593

/// Reduce and solve:

594

/// ```text

595

/// find a,b,c : int(1..3)

596

/// such that a + b + c = 4

597

/// such that a < b

598

/// ```

599

///

600

/// This test uses the rewrite function to simplify the expression instead

601

/// of applying the rules manually.

602

#[test]

603

1

fn rewrite_solve_xyz() {

604

1

    println!("Rules: {:?}", get_all_rules());

605

1

    set_comprehension_expander(QuantifiedExpander::Native);

606

607

1

    let rule_sets = match resolve_rule_sets(SolverFamily::Minion, &["Base", "Bubble"]) {

608

1

        Ok(rs) => rs,

609

        Err(e) => {

610

            eprintln!("Error resolving rule sets: {e}");

611

            exit(1);

612

613

};

614

1

    println!("Rule sets: {rule_sets:?}");

615

616

    // Create variables and domains

617

1

    let decl_a = DeclarationPtr::new_find(Name::user("a"), Domain::int(vec![Range::Bounded(1, 5)]));

618

619

1

    let decl_b = DeclarationPtr::new_find(Name::user("b"), Domain::int(vec![Range::Bounded(1, 5)]));

620

621

1

    let decl_c = DeclarationPtr::new_find(Name::user("c"), Domain::int(vec![Range::Bounded(1, 5)]));

622

623

1

    let a = Atom::Reference(Reference::new(decl_a.clone()));

624

1

    let b = Atom::Reference(Reference::new(decl_b.clone()));

625

1

    let c = Atom::Reference(Reference::new(decl_c.clone()));

626

627

    // Construct nested expression

628

1

    let nested_expr = Expression::And(

629

1

        Metadata::new(),

630

1

        Moo::new(matrix_expr![

631

1

            Expression::Eq(

632

1

                Metadata::new(),

633

1

                Moo::new(Expression::Sum(

634

1

                    Metadata::new(),

635

1

                    Moo::new(matrix_expr![

636

1

                        Expression::Atomic(Metadata::new(), a.clone()),

637

1

                        Expression::Atomic(Metadata::new(), b.clone()),

638

1

                        Expression::Atomic(Metadata::new(), c),

639

1

]),

640

1

)),

641

1

                Moo::new(Expression::Atomic(

642

1

                    Metadata::new(),

643

1

                    Atom::Literal(Literal::Int(4)),

644

1

)),

645

1

),

646

1

            Expression::Lt(

647

1

                Metadata::new(),

648

1

                Moo::new(Expression::Atomic(Metadata::new(), a)),

649

1

                Moo::new(Expression::Atomic(Metadata::new(), b)),

650

1

),

651

1

]),

652

1

);

653

654

1

    let rule_sets = match resolve_rule_sets(SolverFamily::Minion, &["Base", "Bubble"]) {

655

1

        Ok(rs) => rs,

656

        Err(e) => {

657

            eprintln!("Error resolving rule sets: {e}");

658

            exit(1);

659

660

};

661

662

    // Apply rewrite function to the nested expression

663

1

    let mut model = Model::new(Default::default());

664

665

    // Insert variables and domains

666

1

    model.symbols_mut().insert(decl_a).unwrap();

667

1

    model.symbols_mut().insert(decl_b).unwrap();

668

1

    model.symbols_mut().insert(decl_c).unwrap();

669

670

1

    *model.constraints_mut() = vec![nested_expr];

671

672

1

    model = rewrite_model(

673

1

        &model,

674

1

        &rule_sets,

675

1

        conjure_cp::settings::RewriteConfig::baseline(),

676

1

677

1

    .unwrap();

678

1

    let rewritten_expr = model.constraints();

679

680

    // Check if the expression is in its simplest form

681

682

1

    assert!(rewritten_expr.iter().all(is_simple));

683

684

1

    let solver: Solver = Solver::new(adaptors::Minion::new());

685

1

    let solver = solver.load_model(model).unwrap();

686

1

    solver.solve(Box::new(|_| true)).unwrap();

687

1

688

689

struct RuleResult<'a> {

690

    #[allow(dead_code)]

691

    rule: &'a Rule<'a>,

692

    new_expression: Expression,

693

694

695

/// # Returns

696

/// - True if `expression` is in its simplest form.

697

/// - False otherwise.

698

3

pub fn is_simple(expression: &Expression) -> bool {

699

3

    let rules = get_all_rules();

700

3

    let mut new = expression.clone();

701

3

    while let Some(step) = is_simple_iteration(&new, &rules) {

702

        new = step;

703

704

3

    new == *expression

705

3

706

707

/// # Returns

708

/// - Some(<new_expression>) after applying the first applicable rule to `expr` or a sub-expression.

709

/// - None if no rule is applicable to the expression or any sub-expression.

710

3

fn is_simple_iteration<'a>(

711

3

    expression: &'a Expression,

712

3

    rules: &'a Vec<&'a Rule<'a>>,

713

3

) -> Option<Expression> {

714

3

    let rule_results = apply_all_rules(expression, rules);

715

3

    if let Some(new) = choose_rewrite(&rule_results) {

716

        return Some(new);

717

    } else {

718

3

        let mut sub = expression.children();

719

3

        for i in 0..sub.len() {

720

            if let Some(new) = is_simple_iteration(&sub[i], rules) {

721

                sub[i] = new;

722

                return Some(expression.with_children(sub.clone()));

723

724

725

726

3

    None // No rules applicable to this branch of the expression

727

3

728

729

/// # Returns

730

/// - A list of RuleResults after applying all rules to `expression`.

731

/// - An empty list if no rules are applicable.

732

3

fn apply_all_rules<'a>(

733

3

    expression: &'a Expression,

734

3

    rules: &'a Vec<&'a Rule<'a>>,

735

3

) -> Vec<RuleResult<'a>> {

736

3

    let mut results = Vec::new();

737

3

    for rule in rules {

738

993

        match rule.apply(expression, &SymbolTable::new()) {

739

            Ok(red) => {

740

                results.push(RuleResult {

741

                    rule,

742

                    new_expression: red.new_expression,

743

});

744

745

993

            Err(_) => continue,

746

747

748

3

    results

749

3

750

751

/// # Returns

752

/// - Some(<new_expression>) after applying the first rule in `results`.

753

/// - None if `results` is empty.

754

3

fn choose_rewrite(results: &[RuleResult]) -> Option<Expression> {

755

3

    if results.is_empty() {

756

3

        return None;

757

758

    // Return the first result for now

759

    // println!("Applying rule: {:?}", results[0].rule);

760

    Some(results[0].new_expression.clone())

761

3

762

763

#[test]

764

1

fn eval_const_int() {

765

1

    let expr = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));

766

1

    let result = eval_constant(&expr);

767

1

    assert_eq!(result, Some(Literal::Int(1)));

768

1

769

770

#[test]

771

1

fn eval_const_bool() {

772

1

    let expr = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true)));

773

1

    let result = eval_constant(&expr);

774

1

    assert_eq!(result, Some(Literal::Bool(true)));

775

1

776

777

#[test]

778

1

fn eval_const_record_field_from_abstract_literal() {

779

1

    let expr = Expression::RecordField(

780

1

        Metadata::new(),

781

1

        Moo::new(Expression::AbstractLiteral(

782

1

            Metadata::new(),

783

1

            AbstractLiteral::Record(vec![

784

1

                Field {

785

1

                    name: Name::user("a"),

786

1

                    value: Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

787

1

},

788

1

                Field {

789

1

                    name: Name::user("b"),

790

1

                    value: Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(4))),

791

1

},

792

1

]),

793

1

)),

794

1

        Name::user("a"),

795

1

);

796

797

1

    assert_eq!(eval_constant(&expr), Some(Literal::Bool(false)));

798

1

799

800

#[test]

801

1

fn eval_const_set_ops_from_abstract_literals() {

802

6

    fn set(values: &[i32]) -> Moo<Expression> {

803

6

        Moo::new(Expression::AbstractLiteral(

804

6

            Metadata::new(),

805

            AbstractLiteral::Set(

806

6

                values

807

6

                    .iter()

808

13

                    .map(|value| {

809

13

                        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(*value)))

810

13

})

811

                    .collect(),

812

),

813

))

814

6

815

816

1

    let union = Expression::Union(Metadata::new(), set(&[1, 2]), set(&[2, 3]));

817

1

    assert_eq!(

818

1

        eval_constant(&union),

819

1

        Some(Literal::AbstractLiteral(AbstractLiteral::Set(vec![

820

1

            Literal::Int(1),

821

1

            Literal::Int(2),

822

1

            Literal::Int(3),

823

1

        ])))

824

);

825

826

1

    let intersect = Expression::Intersect(Metadata::new(), set(&[1, 2]), set(&[2, 3]));

827

1

    assert_eq!(

828

1

        eval_constant(&intersect),

829

1

        Some(Literal::AbstractLiteral(AbstractLiteral::Set(vec![

830

1

            Literal::Int(2),

831

1

        ])))

832

);

833

834

1

    let subset_eq = Expression::SubsetEq(Metadata::new(), set(&[1, 2]), set(&[1, 2, 3]));

835

1

    assert_eq!(eval_constant(&subset_eq), Some(Literal::Bool(true)));

836

1

837

838

#[test]

839

1

fn eval_const_and() {

840

1

    let expr = Expression::And(

841

1

        Metadata::new(),

842

1

        Moo::new(matrix_expr![

843

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true))),

844

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

845

1

]),

846

1

);

847

1

    let result = eval_constant(&expr);

848

1

    assert_eq!(result, Some(Literal::Bool(false)));

849

1

850

851

#[test]

852

1

fn eval_const_ref() {

853

1

    let expr = Expression::Atomic(

854

1

        Metadata::new(),

855

1

        Atom::Reference(Reference::new(DeclarationPtr::new_find(

856

1

            Name::user("a"),

857

1

            Domain::int(vec![Range::Bounded(1, 5)]),

858

1

        ))),

859

1

);

860

1

    let result = eval_constant(&expr);

861

1

    assert_eq!(result, None);

862

1

863

864

#[test]

865

1

fn eval_const_nested_ref() {

866

1

    let expr = Expression::Sum(

867

1

        Metadata::new(),

868

1

        Moo::new(matrix_expr![

869

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

870

1

            Expression::And(

871

1

                Metadata::new(),

872

1

                Moo::new(matrix_expr![

873

1

                    Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true))),

874

1

                    Expression::Atomic(

875

1

                        Metadata::new(),

876

1

                        Atom::Reference(Reference::new(DeclarationPtr::new_find(

877

1

                            Name::user("a"),

878

1

                            Domain::int(vec![Range::Bounded(1, 5)])

879

1

)))

880

1

),

881

1

]),

882

1

),

883

1

]),

884

1

);

885

1

    let result = eval_constant(&expr);

886

1

    assert_eq!(result, None);

887

1

888

889

#[test]

890

1

fn eval_const_eq_int() {

891

1

    let expr = Expression::Eq(

892

1

        Metadata::new(),

893

1

        Moo::new(Expression::Atomic(

894

1

            Metadata::new(),

895

1

            Atom::Literal(Literal::Int(1)),

896

1

)),

897

1

        Moo::new(Expression::Atomic(

898

1

            Metadata::new(),

899

1

            Atom::Literal(Literal::Int(1)),

900

1

)),

901

1

);

902

1

    let result = eval_constant(&expr);

903

1

    assert_eq!(result, Some(Literal::Bool(true)));

904

1

905

906

#[test]

907

1

fn eval_const_eq_bool() {

908

1

    let expr = Expression::Eq(

909

1

        Metadata::new(),

910

1

        Moo::new(Expression::Atomic(

911

1

            Metadata::new(),

912

1

            Atom::Literal(Literal::Bool(true)),

913

1

)),

914

1

        Moo::new(Expression::Atomic(

915

1

            Metadata::new(),

916

1

            Atom::Literal(Literal::Bool(true)),

917

1

)),

918

1

);

919

1

    let result = eval_constant(&expr);

920

1

    assert_eq!(result, Some(Literal::Bool(true)));

921

1

922

923

#[test]

924

1

fn eval_const_eq_mixed() {

925

1

    let expr = Expression::Eq(

926

1

        Metadata::new(),

927

1

        Moo::new(Expression::Atomic(

928

1

            Metadata::new(),

929

1

            Atom::Literal(Literal::Int(1)),

930

1

)),

931

1

        Moo::new(Expression::Atomic(

932

1

            Metadata::new(),

933

1

            Atom::Literal(Literal::Bool(true)),

934

1

)),

935

1

);

936

1

    let result = eval_constant(&expr);

937

1

    assert_eq!(result, None);

938

1

939

940

#[test]

941

1

fn eval_const_neq_mixed() {

942

1

    let expr = Expression::Neq(

943

1

        Metadata::new(),

944

1

        Moo::new(Expression::Atomic(

945

1

            Metadata::new(),

946

1

            Atom::Literal(Literal::Int(1)),

947

1

)),

948

1

        Moo::new(Expression::Atomic(

949

1

            Metadata::new(),

950

1

            Atom::Literal(Literal::Bool(true)),

951

1

)),

952

1

);

953

1

    let result = eval_constant(&expr);

954

1

    assert_eq!(result, None);

955

1

956

957

#[test]

958

1

fn eval_const_sum_mixed() {

959

1

    let expr = Expression::Sum(

960

1

        Metadata::new(),

961

1

        Moo::new(matrix_expr![

962

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1))),

963

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true))),

964

1

]),

965

1

);

966

1

    let result = eval_constant(&expr);

967

1

    assert_eq!(result, None);

968

1

969

970

#[test]

971

1

fn eval_const_sum_xyz() {

972

1

    let expr = Expression::And(

973

1

        Metadata::new(),

974

1

        Moo::new(matrix_expr![

975

1

            Expression::Eq(

976

1

                Metadata::new(),

977

1

                Moo::new(Expression::Sum(

978

1

                    Metadata::new(),

979

1

                    Moo::new(matrix_expr![

980

1

                        Expression::Atomic(

981

1

                            Metadata::new(),

982

1

                            Atom::Reference(Reference::new(DeclarationPtr::new_find(

983

1

                                Name::user("x"),

984

1

                                Domain::int(vec![Range::Bounded(1, 5)])

985

1

)))

986

1

),

987

1

                        Expression::Atomic(

988

1

                            Metadata::new(),

989

1

                            Atom::Reference(Reference::new(DeclarationPtr::new_find(

990

1

                                Name::user("y"),

991

1

                                Domain::int(vec![Range::Bounded(1, 5)])

992

1

)))

993

1

),

994

1

                        Expression::Atomic(

995

1

                            Metadata::new(),

996

1

                            Atom::Reference(Reference::new(DeclarationPtr::new_find(

997

1

                                Name::user("z"),

998

1

                                Domain::int(vec![Range::Bounded(1, 5)])

999

1

)))

1000

1

),

1001

1

])

1002

1

)),

1003

1

                Moo::new(Expression::Atomic(

1004

1

                    Metadata::new(),

1005

1

                    Atom::Literal(Literal::Int(4)),

1006

1

)),

1007

1

),

1008

1

            Expression::Geq(

1009

1

                Metadata::new(),

1010

1

                Moo::new(Expression::Atomic(

1011

1

                    Metadata::new(),

1012

1

                    Atom::Reference(Reference::new(DeclarationPtr::new_find(

1013

1

                        Name::user("x"),

1014

1

                        Domain::int(vec![Range::Bounded(1, 5)])

1015

1

)))

1016

1

)),

1017

1

                Moo::new(Expression::Atomic(

1018

1

                    Metadata::new(),

1019

1

                    Atom::Reference(Reference::new(DeclarationPtr::new_find(

1020

1

                        Name::user("y"),

1021

1

                        Domain::int(vec![Range::Bounded(1, 5)])

1022

1

)))

1023

1

)),

1024

1

),

1025

1

]),

1026

1

);

1027

1

    let result = eval_constant(&expr);

1028

1

    assert_eq!(result, None);

1029

1

1030

1031

#[test]

1032

1

fn eval_const_or() {

1033

1

    let expr = Expression::Or(

1034

1

        Metadata::new(),

1035

1

        Moo::new(matrix_expr![

1036

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

1037

1

            Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

1038

1

]),

1039

1

);

1040

1

    let result = eval_constant(&expr);

1041

1

    assert_eq!(result, Some(Literal::Bool(false)));

1042

1