Grcov report - rewrite

1

use std::collections::VecDeque;

2

use std::process::exit;

3

4

use conjure_core::rules::eval_constant;

5

use conjure_core::solver::SolverFamily;

6

use conjure_oxide::{

7

    ast::*,

8

    get_rule_by_name, get_rules,

9

    rule_engine::{resolve_rule_sets, rewrite_model},

10

    solver::{adaptors, Solver},

11

    Metadata, Model, Rule,

12

};

13

use uniplate::{Biplate, Uniplate};

14

15

3

fn var_name_from_atom(a: &Atom) -> Name {

16

3

    let names: VecDeque<Name> = a.universe_bi();

17

3

    names[0].clone()

18

3

19

#[test]

20

1

fn rules_present() {

21

1

    let rules = get_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

        vec![

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

1

36

1

    let invalid_sum_expression = Expression::Sum(

37

1

        Metadata::new(),

38

1

        vec![

39

1

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

40

1

            Expression::Atomic(

41

1

                Metadata::new(),

42

1

                Atom::Reference(Name::UserName(String::from("a"))),

43

1

),

44

1

],

45

1

);

46

1

47

1

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

48

49

1

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

50

1

51

52

4

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

53

4

    match expr {

54

4

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

55

4

            let mut sum = 0;

56

12

            for e in expressions {

57

8

                match e {

58

8

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

59

8

                        sum += value;

60

8

61

2

                    _ => return None,

62

63

64

2

            Some(sum)

65

66

        _ => None,

67

68

4

69

70

#[test]

71

1

fn recursive_sum_of_constants() {

72

1

    let complex_expression = Expression::Eq(

73

1

        Metadata::new(),

74

1

        Box::new(Expression::Sum(

75

1

            Metadata::new(),

76

1

            vec![

77

1

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

78

1

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

79

1

                Expression::Sum(

80

1

                    Metadata::new(),

81

1

                    vec![

82

1

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

83

1

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

84

1

],

85

1

),

86

1

                Expression::Atomic(

87

1

                    Metadata::new(),

88

1

                    Atom::Reference(Name::UserName(String::from("a"))),

89

1

),

90

1

],

91

1

)),

92

1

        Box::new(Expression::Atomic(

93

1

            Metadata::new(),

94

1

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

95

1

)),

96

1

);

97

1

    let correct_simplified_expression = Expression::Eq(

98

1

        Metadata::new(),

99

1

        Box::new(Expression::Sum(

100

1

            Metadata::new(),

101

1

            vec![

102

1

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

103

1

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

104

1

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

105

1

                Expression::Atomic(

106

1

                    Metadata::new(),

107

1

                    Atom::Reference(Name::UserName(String::from("a"))),

108

1

),

109

1

],

110

1

)),

111

1

        Box::new(Expression::Atomic(

112

1

            Metadata::new(),

113

1

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

114

1

)),

115

1

);

116

1

117

1

    let simplified_expression = simplify_expression(complex_expression.clone());

118

1

    assert_eq!(simplified_expression, correct_simplified_expression);

119

1

120

121

7

fn simplify_expression(expr: Expression) -> Expression {

122

7

    match expr {

123

2

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

124

1

            if let Some(result) =

125

2

                evaluate_sum_of_constants(&Expression::Sum(Metadata::new(), expressions.clone()))

126

127

1

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

128

            } else {

129

1

                Expression::Sum(

130

1

                    Metadata::new(),

131

1

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

132

1

133

134

135

1

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

136

1

            Metadata::new(),

137

1

            Box::new(simplify_expression(*left)),

138

1

            Box::new(simplify_expression(*right)),

139

1

),

140

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

141

            Metadata::new(),

142

            Box::new(simplify_expression(*left)),

143

            Box::new(simplify_expression(*right)),

144

),

145

4

        _ => expr,

146

147

7

148

149

#[test]

150

1

fn rule_sum_constants() {

151

1

    let sum_constants = get_rule_by_name("partial_evaluator").unwrap();

152

1

    let unwrap_sum = get_rule_by_name("remove_unit_vector_sum").unwrap();

153

1

154

1

    let mut expr = Expression::Sum(

155

1

        Metadata::new(),

156

1

        vec![

157

1

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

158

1

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

159

1

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

160

1

],

161

1

);

162

1

163

1

    expr = sum_constants

164

1

        .apply(&expr, &Model::new_empty(Default::default()))

165

1

        .unwrap()

166

1

        .new_expression;

167

1

    expr = unwrap_sum

168

1

        .apply(&expr, &Model::new_empty(Default::default()))

169

1

        .unwrap()

170

1

        .new_expression;

171

1

172

1

    assert_eq!(

173

1

        expr,

174

1

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

175

1

);

176

1

177

178

#[test]

179

1

fn rule_sum_geq() {

180

1

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

181

1

182

1

    let mut expr = Expression::Geq(

183

1

        Metadata::new(),

184

1

        Box::new(Expression::Sum(

185

1

            Metadata::new(),

186

1

            vec![

187

1

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

188

1

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

189

1

],

190

1

)),

191

1

        Box::new(Expression::Atomic(

192

1

            Metadata::new(),

193

1

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

194

1

)),

195

1

);

196

1

197

1

    expr = introduce_sumgeq

198

1

        .apply(&expr, &Model::new_empty(Default::default()))

199

1

        .unwrap()

200

1

        .new_expression;

201

1

202

1

    assert_eq!(

203

1

        expr,

204

1

        Expression::FlatSumGeq(

205

1

            Metadata::new(),

206

1

            vec![

207

1

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

208

1

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

209

1

],

210

1

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

211

1

212

1

);

213

1

214

215

///

216

/// Reduce and solve:

217

/// ```text

218

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

219

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

220

/// such that a < b

221

/// ```

222

#[test]

223

1

fn reduce_solve_xyz() {

224

1

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

225

1

    let sum_constants = get_rule_by_name("partial_evaluator").unwrap();

226

1

    let unwrap_sum = get_rule_by_name("remove_unit_vector_sum").unwrap();

227

1

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

228

1

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

229

1

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

230

1

231

1

    // 2 + 3 - 1

232

1

    let mut expr1 = Expression::Sum(

233

1

        Metadata::new(),

234

1

        vec![

235

1

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

236

1

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

237

1

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

238

1

],

239

1

);

240

1

241

1

    expr1 = sum_constants

242

1

        .apply(&expr1, &Model::new_empty(Default::default()))

243

1

        .unwrap()

244

1

        .new_expression;

245

1

    expr1 = unwrap_sum

246

1

        .apply(&expr1, &Model::new_empty(Default::default()))

247

1

        .unwrap()

248

1

        .new_expression;

249

1

    assert_eq!(

250

1

        expr1,

251

1

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

252

1

);

253

254

    // a + b + c = 4

255

1

    expr1 = Expression::Leq(

256

1

        Metadata::new(),

257

1

        Box::new(Expression::Sum(

258

1

            Metadata::new(),

259

1

            vec![

260

1

                Expression::Atomic(

261

1

                    Metadata::new(),

262

1

                    Atom::Reference(Name::UserName(String::from("a"))),

263

1

),

264

1

                Expression::Atomic(

265

1

                    Metadata::new(),

266

1

                    Atom::Reference(Name::UserName(String::from("b"))),

267

1

),

268

1

                Expression::Atomic(

269

1

                    Metadata::new(),

270

1

                    Atom::Reference(Name::UserName(String::from("c"))),

271

1

),

272

1

],

273

1

)),

274

1

        Box::new(expr1),

275

1

);

276

1

    expr1 = introduce_sumleq

277

1

        .apply(&expr1, &Model::new_empty(Default::default()))

278

1

        .unwrap()

279

1

        .new_expression;

280

1

    assert_eq!(

281

1

        expr1,

282

1

        Expression::FlatSumLeq(

283

1

            Metadata::new(),

284

1

            vec![

285

1

                Atom::Reference(Name::UserName(String::from("a"))),

286

1

                Atom::Reference(Name::UserName(String::from("b"))),

287

1

                Atom::Reference(Name::UserName(String::from("c"))),

288

1

],

289

1

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

290

1

291

1

);

292

293

    // a < b

294

1

    let mut expr2 = Expression::Lt(

295

1

        Metadata::new(),

296

1

        Box::new(Expression::Atomic(

297

1

            Metadata::new(),

298

1

            Atom::Reference(Name::UserName(String::from("a"))),

299

1

)),

300

1

        Box::new(Expression::Atomic(

301

1

            Metadata::new(),

302

1

            Atom::Reference(Name::UserName(String::from("b"))),

303

1

)),

304

1

);

305

1

    expr2 = lt_to_leq

306

1

        .apply(&expr2, &Model::new_empty(Default::default()))

307

1

        .unwrap()

308

1

        .new_expression;

309

1

310

1

    expr2 = leq_to_ineq

311

1

        .apply(&expr2, &Model::new_empty(Default::default()))

312

1

        .unwrap()

313

1

        .new_expression;

314

1

    assert_eq!(

315

1

        expr2,

316

1

        Expression::FlatIneq(

317

1

            Metadata::new(),

318

1

            Atom::Reference(Name::UserName(String::from("a"))),

319

1

            Atom::Reference(Name::UserName(String::from("b"))),

320

1

            Literal::Int(-1),

321

1

322

1

);

323

324

1

    let mut model = Model::new(SymbolTable::new(), vec![expr1, expr2], Default::default());

325

1

    model.add_variable(

326

1

        Name::UserName(String::from("a")),

327

1

        DecisionVariable {

328

1

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

329

1

},

330

1

);

331

1

    model.add_variable(

332

1

        Name::UserName(String::from("b")),

333

1

        DecisionVariable {

334

1

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

335

1

},

336

1

);

337

1

    model.add_variable(

338

1

        Name::UserName(String::from("c")),

339

1

        DecisionVariable {

340

1

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

341

1

},

342

1

);

343

1

344

1

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

345

1

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

346

1

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

347

1

348

349

#[test]

350

1

fn rule_remove_double_negation() {

351

1

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

352

1

353

1

    let mut expr = Expression::Not(

354

1

        Metadata::new(),

355

1

        Box::new(Expression::Not(

356

1

            Metadata::new(),

357

1

            Box::new(Expression::Atomic(

358

1

                Metadata::new(),

359

1

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

360

1

)),

361

1

)),

362

1

);

363

1

364

1

    expr = remove_double_negation

365

1

        .apply(&expr, &Model::new_empty(Default::default()))

366

1

        .unwrap()

367

1

        .new_expression;

368

1

369

1

    assert_eq!(

370

1

        expr,

371

1

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

372

1

);

373

1

374

375

#[test]

376

1

fn remove_trivial_and_or() {

377

1

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

378

1

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

379

1

380

1

    let mut expr_and = Expression::And(

381

1

        Metadata::new(),

382

1

        vec![Expression::Atomic(

383

1

            Metadata::new(),

384

1

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

385

1

)],

386

1

);

387

1

    let mut expr_or = Expression::Or(

388

1

        Metadata::new(),

389

1

        vec![Expression::Atomic(

390

1

            Metadata::new(),

391

1

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

392

1

)],

393

1

);

394

1

395

1

    expr_and = remove_trivial_and

396

1

        .apply(&expr_and, &Model::new_empty(Default::default()))

397

1

        .unwrap()

398

1

        .new_expression;

399

1

    expr_or = remove_trivial_or

400

1

        .apply(&expr_or, &Model::new_empty(Default::default()))

401

1

        .unwrap()

402

1

        .new_expression;

403

1

404

1

    assert_eq!(

405

1

        expr_and,

406

1

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

407

1

);

408

1

    assert_eq!(

409

1

        expr_or,

410

1

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

411

1

);

412

1

413

414

#[test]

415

1

fn rule_distribute_not_over_and() {

416

1

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

417

1

418

1

    let mut expr = Expression::Not(

419

1

        Metadata::new(),

420

1

        Box::new(Expression::And(

421

1

            Metadata::new(),

422

1

            vec![

423

1

                Expression::Atomic(

424

1

                    Metadata::new(),

425

1

                    Atom::Reference(Name::UserName(String::from("a"))),

426

1

),

427

1

                Expression::Atomic(

428

1

                    Metadata::new(),

429

1

                    Atom::Reference(Name::UserName(String::from("b"))),

430

1

),

431

1

],

432

1

)),

433

1

);

434

1

435

1

    expr = distribute_not_over_and

436

1

        .apply(&expr, &Model::new_empty(Default::default()))

437

1

        .unwrap()

438

1

        .new_expression;

439

1

440

1

    assert_eq!(

441

1

        expr,

442

1

        Expression::Or(

443

1

            Metadata::new(),

444

1

            vec![

445

1

                Expression::Not(

446

1

                    Metadata::new(),

447

1

                    Box::new(Expression::Atomic(

448

1

                        Metadata::new(),

449

1

                        Atom::Reference(Name::UserName(String::from("a")))

450

1

))

451

1

),

452

1

                Expression::Not(

453

1

                    Metadata::new(),

454

1

                    Box::new(Expression::Atomic(

455

1

                        Metadata::new(),

456

1

                        Atom::Reference(Name::UserName(String::from("b")))

457

1

))

458

1

),

459

1

460

1

461

1

);

462

1

463

464

#[test]

465

1

fn rule_distribute_not_over_or() {

466

1

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

467

1

468

1

    let mut expr = Expression::Not(

469

1

        Metadata::new(),

470

1

        Box::new(Expression::Or(

471

1

            Metadata::new(),

472

1

            vec![

473

1

                Expression::Atomic(

474

1

                    Metadata::new(),

475

1

                    Atom::Reference(Name::UserName(String::from("a"))),

476

1

),

477

1

                Expression::Atomic(

478

1

                    Metadata::new(),

479

1

                    Atom::Reference(Name::UserName(String::from("b"))),

480

1

),

481

1

],

482

1

)),

483

1

);

484

1

485

1

    expr = distribute_not_over_or

486

1

        .apply(&expr, &Model::new_empty(Default::default()))

487

1

        .unwrap()

488

1

        .new_expression;

489

1

490

1

    assert_eq!(

491

1

        expr,

492

1

        Expression::And(

493

1

            Metadata::new(),

494

1

            vec![

495

1

                Expression::Not(

496

1

                    Metadata::new(),

497

1

                    Box::new(Expression::Atomic(

498

1

                        Metadata::new(),

499

1

                        Atom::Reference(Name::UserName(String::from("a")))

500

1

))

501

1

),

502

1

                Expression::Not(

503

1

                    Metadata::new(),

504

1

                    Box::new(Expression::Atomic(

505

1

                        Metadata::new(),

506

1

                        Atom::Reference(Name::UserName(String::from("b")))

507

1

))

508

1

),

509

1

510

1

511

1

);

512

1

513

514

#[test]

515

1

fn rule_distribute_not_over_and_not_changed() {

516

1

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

517

1

518

1

    let expr = Expression::Not(

519

1

        Metadata::new(),

520

1

        Box::new(Expression::Atomic(

521

1

            Metadata::new(),

522

1

            Atom::Reference(Name::UserName(String::from("a"))),

523

1

)),

524

1

);

525

1

526

1

    let result = distribute_not_over_and.apply(&expr, &Model::new_empty(Default::default()));

527

1

528

1

    assert!(result.is_err());

529

1

530

531

#[test]

532

1

fn rule_distribute_not_over_or_not_changed() {

533

1

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

534

1

535

1

    let expr = Expression::Not(

536

1

        Metadata::new(),

537

1

        Box::new(Expression::Atomic(

538

1

            Metadata::new(),

539

1

            Atom::Reference(Name::UserName(String::from("a"))),

540

1

)),

541

1

);

542

1

543

1

    let result = distribute_not_over_or.apply(&expr, &Model::new_empty(Default::default()));

544

1

545

1

    assert!(result.is_err());

546

1

547

548

#[test]

549

1

fn rule_distribute_or_over_and() {

550

1

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

551

1

552

1

    let expr = Expression::Or(

553

1

        Metadata::new(),

554

1

        vec![

555

1

            Expression::And(

556

1

                Metadata::new(),

557

1

                vec![

558

1

                    Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(1))),

559

1

                    Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(2))),

560

1

],

561

1

),

562

1

            Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(3))),

563

1

],

564

1

);

565

1

566

1

    let red = distribute_or_over_and

567

1

        .apply(&expr, &Model::new_empty(Default::default()))

568

1

        .unwrap();

569

1

570

1

    assert_eq!(

571

1

        red.new_expression,

572

1

        Expression::And(

573

1

            Metadata::new(),

574

1

            vec![

575

1

                Expression::Or(

576

1

                    Metadata::new(),

577

1

                    vec![

578

1

                        Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(3))),

579

1

                        Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(1))),

580

1

581

1

),

582

1

                Expression::Or(

583

1

                    Metadata::new(),

584

1

                    vec![

585

1

                        Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(3))),

586

1

                        Expression::Atomic(Metadata::new(), Atom::Reference(Name::MachineName(2))),

587

1

588

1

),

589

1

590

1

),

591

1

);

592

1

593

594

///

595

/// Reduce and solve:

596

/// ```text

597

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

598

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

599

/// such that a < b

600

/// ```

601

///

602

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

603

/// of applying the rules manually.

604

#[test]

605

1

fn rewrite_solve_xyz() {

606

1

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

607

608

1

    let rule_sets = match resolve_rule_sets(SolverFamily::Minion, &vec!["Constant".to_string()]) {

609

1

        Ok(rs) => rs,

610

        Err(e) => {

611

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

612

            exit(1);

613

614

};

615

1

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

616

1

617

1

    // Create variables and domains

618

1

    let variable_a = Atom::Reference(Name::UserName(String::from("a")));

619

1

    let variable_b = Atom::Reference(Name::UserName(String::from("b")));

620

1

    let variable_c = Atom::Reference(Name::UserName(String::from("c")));

621

1

    let domain = Domain::IntDomain(vec![Range::Bounded(1, 3)]);

622

1

623

1

    // Construct nested expression

624

1

    let nested_expr = Expression::And(

625

1

        Metadata::new(),

626

1

        vec![

627

1

            Expression::Eq(

628

1

                Metadata::new(),

629

1

                Box::new(Expression::Sum(

630

1

                    Metadata::new(),

631

1

                    vec![

632

1

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

633

1

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

634

1

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

635

1

],

636

1

)),

637

1

                Box::new(Expression::Atomic(

638

1

                    Metadata::new(),

639

1

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

640

1

)),

641

1

),

642

1

            Expression::Lt(

643

1

                Metadata::new(),

644

1

                Box::new(Expression::Atomic(Metadata::new(), variable_a.clone())),

645

1

                Box::new(Expression::Atomic(Metadata::new(), variable_b.clone())),

646

1

),

647

1

],

648

1

);

649

650

1

    let rule_sets = match resolve_rule_sets(SolverFamily::Minion, &vec!["Constant".to_string()]) {

651

1

        Ok(rs) => rs,

652

        Err(e) => {

653

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

654

            exit(1);

655

656

};

657

658

    // Apply rewrite function to the nested expression

659

1

    let rewritten_expr = rewrite_model(

660

1

        &Model::new(SymbolTable::new(), vec![nested_expr], Default::default()),

661

1

        &rule_sets,

662

1

663

1

    .unwrap()

664

1

    .constraints;

665

1

666

1

    // Check if the expression is in its simplest form

667

1

668

1

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

669

670

    // Create model with variables and constraints

671

1

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

672

1

673

1

    // Insert variables and domains

674

1

    model.add_variable(

675

1

        var_name_from_atom(&variable_a.clone()),

676

1

        DecisionVariable {

677

1

            domain: domain.clone(),

678

1

},

679

1

);

680

1

    model.add_variable(

681

1

        var_name_from_atom(&variable_b.clone()),

682

1

        DecisionVariable {

683

1

            domain: domain.clone(),

684

1

},

685

1

);

686

1

    model.add_variable(

687

1

        var_name_from_atom(&variable_c.clone()),

688

1

        DecisionVariable {

689

1

            domain: domain.clone(),

690

1

},

691

1

);

692

1

693

1

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

694

1

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

695

1

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

696

1

697

698

struct RuleResult<'a> {

699

    #[allow(dead_code)]

700

    rule: &'a Rule<'a>,

701

    new_expression: Expression,

702

703

704

/// # Returns

705

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

706

/// - False otherwise.

707

1

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

708

1

    let rules = get_rules();

709

1

    let mut new = expression.clone();

710

1

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

711

        new = step;

712

713

1

    new == *expression

714

1

715

716

/// # Returns

717

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

718

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

719

4

fn is_simple_iteration<'a>(

720

4

    expression: &'a Expression,

721

4

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

722

4

) -> Option<Expression> {

723

4

    let rule_results = apply_all_rules(expression, rules);

724

4

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

725

        return Some(new);

726

    } else {

727

4

        let mut sub = expression.children();

728

4

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

729

3

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

730

                sub[i] = new;

731

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

732

3

733

734

735

4

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

736

4

737

738

/// # Returns

739

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

740

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

741

4

fn apply_all_rules<'a>(

742

4

    expression: &'a Expression,

743

4

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

744

4

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

745

4

    let mut results = Vec::new();

746

212

    for rule in rules {

747

208

        match rule.apply(expression, &Model::new_empty(Default::default())) {

748

            Ok(red) => {

749

                results.push(RuleResult {

750

                    rule,

751

                    new_expression: red.new_expression,

752

});

753

754

208

            Err(_) => continue,

755

756

757

4

    results

758

4

759

760

/// # Returns

761

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

762

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

763

4

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

764

4

    if results.is_empty() {

765

4

        return None;

766

767

    // Return the first result for now

768

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

769

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

770

4

771

772

#[test]

773

1

fn eval_const_int() {

774

1

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

775

1

    let result = eval_constant(&expr);

776

1

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

777

1

778

779

#[test]

780

1

fn eval_const_bool() {

781

1

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

782

1

    let result = eval_constant(&expr);

783

1

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

784

1

785

786

#[test]

787

1

fn eval_const_and() {

788

1

    let expr = Expression::And(

789

1

        Metadata::new(),

790

1

        vec![

791

1

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

792

1

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

793

1

],

794

1

);

795

1

    let result = eval_constant(&expr);

796

1

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

797

1

798

799

#[test]

800

1

fn eval_const_ref() {

801

1

    let expr = Expression::Atomic(

802

1

        Metadata::new(),

803

1

        Atom::Reference(Name::UserName(String::from("a"))),

804

1

);

805

1

    let result = eval_constant(&expr);

806

1

    assert_eq!(result, None);

807

1

808

809

#[test]

810

1

fn eval_const_nested_ref() {

811

1

    let expr = Expression::Sum(

812

1

        Metadata::new(),

813

1

        vec![

814

1

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

815

1

            Expression::And(

816

1

                Metadata::new(),

817

1

                vec![

818

1

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

819

1

                    Expression::Atomic(

820

1

                        Metadata::new(),

821

1

                        Atom::Reference(Name::UserName(String::from("a"))),

822

1

),

823

1

],

824

1

),

825

1

],

826

1

);

827

1

    let result = eval_constant(&expr);

828

1

    assert_eq!(result, None);

829

1

830

831

#[test]

832

1

fn eval_const_eq_int() {

833

1

    let expr = Expression::Eq(

834

1

        Metadata::new(),

835

1

        Box::new(Expression::Atomic(

836

1

            Metadata::new(),

837

1

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

838

1

)),

839

1

        Box::new(Expression::Atomic(

840

1

            Metadata::new(),

841

1

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

842

1

)),

843

1

);

844

1

    let result = eval_constant(&expr);

845

1

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

846

1

847

848

#[test]

849

1

fn eval_const_eq_bool() {

850

1

    let expr = Expression::Eq(

851

1

        Metadata::new(),

852

1

        Box::new(Expression::Atomic(

853

1

            Metadata::new(),

854

1

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

855

1

)),

856

1

        Box::new(Expression::Atomic(

857

1

            Metadata::new(),

858

1

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

859

1

)),

860

1

);

861

1

    let result = eval_constant(&expr);

862

1

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

863

1

864

865

#[test]

866

1

fn eval_const_eq_mixed() {

867

1

    let expr = Expression::Eq(

868

1

        Metadata::new(),

869

1

        Box::new(Expression::Atomic(

870

1

            Metadata::new(),

871

1

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

872

1

)),

873

1

        Box::new(Expression::Atomic(

874

1

            Metadata::new(),

875

1

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

876

1

)),

877

1

);

878

1

    let result = eval_constant(&expr);

879

1

    assert_eq!(result, None);

880

1

881

882

#[test]

883

1

fn eval_const_sum_mixed() {

884

1

    let expr = Expression::Sum(

885

1

        Metadata::new(),

886

1

        vec![

887

1

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

888

1

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

889

1

],

890

1

);

891

1

    let result = eval_constant(&expr);

892

1

    assert_eq!(result, None);

893

1

894

895

#[test]

896

1

fn eval_const_sum_xyz() {

897

1

    let expr = Expression::And(

898

1

        Metadata::new(),

899

1

        vec![

900

1

            Expression::Eq(

901

1

                Metadata::new(),

902

1

                Box::new(Expression::Sum(

903

1

                    Metadata::new(),

904

1

                    vec![

905

1

                        Expression::Atomic(

906

1

                            Metadata::new(),

907

1

                            Atom::Reference(Name::UserName(String::from("x"))),

908

1

),

909

1

                        Expression::Atomic(

910

1

                            Metadata::new(),

911

1

                            Atom::Reference(Name::UserName(String::from("y"))),

912

1

),

913

1

                        Expression::Atomic(

914

1

                            Metadata::new(),

915

1

                            Atom::Reference(Name::UserName(String::from("z"))),

916

1

),

917

1

],

918

1

)),

919

1

                Box::new(Expression::Atomic(

920

1

                    Metadata::new(),

921

1

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

922

1

)),

923

1

),

924

1

            Expression::Geq(

925

1

                Metadata::new(),

926

1

                Box::new(Expression::Atomic(

927

1

                    Metadata::new(),

928

1

                    Atom::Reference(Name::UserName(String::from("x"))),

929

1

)),

930

1

                Box::new(Expression::Atomic(

931

1

                    Metadata::new(),

932

1

                    Atom::Reference(Name::UserName(String::from("y"))),

933

1

)),

934

1

),

935

1

],

936

1

);

937

1

    let result = eval_constant(&expr);

938

1

    assert_eq!(result, None);

939

1

940

941

#[test]

942

1

fn eval_const_or() {

943

1

    let expr = Expression::Or(

944

1

        Metadata::new(),

945

1

        vec![

946

1

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

947

1

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

948

1

],

949

1

);

950

1

    let result = eval_constant(&expr);

951

1

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

952

1