Grcov report - rewrite

1

use std::collections::HashMap;

2

use std::env;

3

use std::process::exit;

4

5

use conjure_core::rules::eval_constant;

6

use conjure_core::solver::SolverFamily;

7

use conjure_oxide::{

8

    ast::*,

9

    get_rule_by_name, get_rules,

10

    rule_engine::{resolve_rule_sets, rewrite_model},

11

    solver::{adaptors, Solver},

12

    utils::testing::save_stats_json,

13

    Metadata, Model, Rule,

14

};

15

use uniplate::{Biplate, Uniplate};

16

17

27

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

18

27

    <Atom as Biplate<Name>>::universe_bi(a)[0].clone()

19

27

20

#[test]

21

1

fn rules_present() {

22

1

    let rules = get_rules();

23

1

    assert!(!rules.is_empty());

24

1

25

26

#[test]

27

1

fn sum_of_constants() {

28

1

    let valid_sum_expression = Expression::Sum(

29

1

        Metadata::new(),

30

1

        vec![

31

1

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

32

1

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

33

1

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

34

1

],

35

1

);

36

1

37

1

    let invalid_sum_expression = Expression::Sum(

38

1

        Metadata::new(),

39

1

        vec![

40

1

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

41

1

            Expression::Atomic(

42

1

                Metadata::new(),

43

1

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

44

1

),

45

1

],

46

1

);

47

1

48

1

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

49

50

1

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

51

1

52

53

4

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

54

4

    match expr {

55

4

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

56

4

            let mut sum = 0;

57

12

            for e in expressions {

58

8

                match e {

59

8

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

60

8

                        sum += value;

61

8

62

2

                    _ => return None,

63

64

65

2

            Some(sum)

66

67

        _ => None,

68

69

4

70

71

#[test]

72

1

fn recursive_sum_of_constants() {

73

1

    let complex_expression = Expression::Eq(

74

1

        Metadata::new(),

75

1

        Box::new(Expression::Sum(

76

1

            Metadata::new(),

77

1

            vec![

78

1

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

79

1

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

80

1

                Expression::Sum(

81

1

                    Metadata::new(),

82

1

                    vec![

83

1

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

84

1

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

85

1

],

86

1

),

87

1

                Expression::Atomic(

88

1

                    Metadata::new(),

89

1

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

90

1

),

91

1

],

92

1

)),

93

1

        Box::new(Expression::Atomic(

94

1

            Metadata::new(),

95

1

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

96

1

)),

97

1

);

98

1

    let correct_simplified_expression = Expression::Eq(

99

1

        Metadata::new(),

100

1

        Box::new(Expression::Sum(

101

1

            Metadata::new(),

102

1

            vec![

103

1

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

104

1

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

105

1

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

106

1

                Expression::Atomic(

107

1

                    Metadata::new(),

108

1

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

109

1

),

110

1

],

111

1

)),

112

1

        Box::new(Expression::Atomic(

113

1

            Metadata::new(),

114

1

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

115

1

)),

116

1

);

117

1

118

1

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

119

1

    assert_eq!(simplified_expression, correct_simplified_expression);

120

1

121

122

7

fn simplify_expression(expr: Expression) -> Expression {

123

7

    match expr {

124

2

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

125

1

            if let Some(result) =

126

2

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

127

128

1

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

129

            } else {

130

1

                Expression::Sum(

131

1

                    Metadata::new(),

132

1

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

133

1

134

135

136

1

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

137

1

            Metadata::new(),

138

1

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

139

1

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

140

1

),

141

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

142

            Metadata::new(),

143

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

144

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

145

),

146

4

        _ => expr,

147

148

7

149

150

#[test]

151

1

fn rule_sum_constants() {

152

1

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

153

1

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

154

1

155

1

    let mut expr = Expression::Sum(

156

1

        Metadata::new(),

157

1

        vec![

158

1

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

159

1

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

160

1

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

161

1

],

162

1

);

163

1

164

1

    expr = sum_constants

165

1

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

166

1

        .unwrap()

167

1

        .new_expression;

168

1

    expr = unwrap_sum

169

1

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

170

1

        .unwrap()

171

1

        .new_expression;

172

1

173

1

    assert_eq!(

174

1

        expr,

175

1

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

176

1

);

177

1

178

179

#[test]

180

1

fn rule_sum_geq() {

181

1

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

182

1

183

1

    let mut expr = Expression::Geq(

184

1

        Metadata::new(),

185

1

        Box::new(Expression::Sum(

186

1

            Metadata::new(),

187

1

            vec![

188

1

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

189

1

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

190

1

],

191

1

)),

192

1

        Box::new(Expression::Atomic(

193

1

            Metadata::new(),

194

1

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

195

1

)),

196

1

);

197

1

198

1

    expr = flatten_sum_geq

199

1

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

200

1

        .unwrap()

201

1

        .new_expression;

202

1

203

1

    assert_eq!(

204

1

        expr,

205

1

        Expression::SumGeq(

206

1

            Metadata::new(),

207

1

            vec![

208

1

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

209

1

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

210

1

],

211

1

            Box::new(Expression::Atomic(

212

1

                Metadata::new(),

213

1

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

214

1

))

215

1

216

1

);

217

1

218

219

///

220

/// Reduce and solve:

221

/// ```text

222

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

223

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

224

/// such that a < b

225

/// ```

226

#[test]

227

1

fn reduce_solve_xyz() {

228

1

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

229

1

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

230

1

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

231

1

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

232

1

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

233

1

234

1

    // 2 + 3 - 1

235

1

    let mut expr1 = Expression::Sum(

236

1

        Metadata::new(),

237

1

        vec![

238

1

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

239

1

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

240

1

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

241

1

],

242

1

);

243

1

244

1

    expr1 = sum_constants

245

1

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

246

1

        .unwrap()

247

1

        .new_expression;

248

1

    expr1 = unwrap_sum

249

1

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

250

1

        .unwrap()

251

1

        .new_expression;

252

1

    assert_eq!(

253

1

        expr1,

254

1

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

255

1

);

256

257

    // a + b + c = 4

258

1

    expr1 = Expression::Leq(

259

1

        Metadata::new(),

260

1

        Box::new(Expression::Sum(

261

1

            Metadata::new(),

262

1

            vec![

263

1

                Expression::Atomic(

264

1

                    Metadata::new(),

265

1

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

266

1

),

267

1

                Expression::Atomic(

268

1

                    Metadata::new(),

269

1

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

270

1

),

271

1

                Expression::Atomic(

272

1

                    Metadata::new(),

273

1

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

274

1

),

275

1

],

276

1

)),

277

1

        Box::new(expr1),

278

1

);

279

1

    expr1 = sum_leq_to_sumleq

280

1

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

281

1

        .unwrap()

282

1

        .new_expression;

283

1

    assert_eq!(

284

1

        expr1,

285

1

        Expression::SumLeq(

286

1

            Metadata::new(),

287

1

            vec![

288

1

                Expression::Atomic(

289

1

                    Metadata::new(),

290

1

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

291

1

),

292

1

                Expression::Atomic(

293

1

                    Metadata::new(),

294

1

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

295

1

),

296

1

                Expression::Atomic(

297

1

                    Metadata::new(),

298

1

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

299

1

),

300

1

],

301

1

            Box::new(Expression::Atomic(

302

1

                Metadata::new(),

303

1

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

304

1

))

305

1

306

1

);

307

308

    // a < b

309

1

    let mut expr2 = Expression::Lt(

310

1

        Metadata::new(),

311

1

        Box::new(Expression::Atomic(

312

1

            Metadata::new(),

313

1

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

314

1

)),

315

1

        Box::new(Expression::Atomic(

316

1

            Metadata::new(),

317

1

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

318

1

)),

319

1

);

320

1

    expr2 = lt_to_ineq

321

1

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

322

1

        .unwrap()

323

1

        .new_expression;

324

1

    assert_eq!(

325

1

        expr2,

326

1

        Expression::Ineq(

327

1

            Metadata::new(),

328

1

            Box::new(Expression::Atomic(

329

1

                Metadata::new(),

330

1

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

331

1

)),

332

1

            Box::new(Expression::Atomic(

333

1

                Metadata::new(),

334

1

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

335

1

)),

336

1

            Box::new(Expression::Atomic(

337

1

                Metadata::new(),

338

1

                Atom::Literal(Literal::Int(-1))

339

1

))

340

1

341

1

);

342

343

1

    let mut model = Model::new(

344

1

        HashMap::new(),

345

1

        Expression::And(Metadata::new(), vec![expr1, expr2]),

346

1

        Default::default(),

347

1

);

348

1

    model.variables.insert(

349

1

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

350

1

        DecisionVariable {

351

1

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

352

1

},

353

1

);

354

1

    model.variables.insert(

355

1

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

356

1

        DecisionVariable {

357

1

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

358

1

},

359

1

);

360

1

    model.variables.insert(

361

1

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

362

1

        DecisionVariable {

363

1

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

364

1

},

365

1

);

366

1

367

1

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

368

1

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

369

1

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

370

1

371

372

#[test]

373

1

fn rule_remove_double_negation() {

374

1

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

375

1

376

1

    let mut expr = Expression::Not(

377

1

        Metadata::new(),

378

1

        Box::new(Expression::Not(

379

1

            Metadata::new(),

380

1

            Box::new(Expression::Atomic(

381

1

                Metadata::new(),

382

1

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

383

1

)),

384

1

)),

385

1

);

386

1

387

1

    expr = remove_double_negation

388

1

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

389

1

        .unwrap()

390

1

        .new_expression;

391

1

392

1

    assert_eq!(

393

1

        expr,

394

1

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

395

1

);

396

1

397

398

#[test]

399

1

fn rule_unwrap_nested_or() {

400

1

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

401

1

402

1

    let mut expr = Expression::Or(

403

1

        Metadata::new(),

404

1

        vec![

405

1

            Expression::Or(

406

1

                Metadata::new(),

407

1

                vec![

408

1

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

409

1

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

410

1

],

411

1

),

412

1

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

413

1

],

414

1

);

415

1

416

1

    expr = unwrap_nested_or

417

1

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

418

1

        .unwrap()

419

1

        .new_expression;

420

1

421

1

    assert_eq!(

422

1

        expr,

423

1

        Expression::Or(

424

1

            Metadata::new(),

425

1

            vec![

426

1

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

427

1

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

428

1

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

429

1

430

1

431

1

);

432

1

433

434

#[test]

435

1

fn rule_unwrap_nested_and() {

436

1

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

437

1

438

1

    let mut expr = Expression::And(

439

1

        Metadata::new(),

440

1

        vec![

441

1

            Expression::And(

442

1

                Metadata::new(),

443

1

                vec![

444

1

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

445

1

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

446

1

],

447

1

),

448

1

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

449

1

],

450

1

);

451

1

452

1

    expr = unwrap_nested_and

453

1

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

454

1

        .unwrap()

455

1

        .new_expression;

456

1

457

1

    assert_eq!(

458

1

        expr,

459

1

        Expression::And(

460

1

            Metadata::new(),

461

1

            vec![

462

1

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

463

1

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

464

1

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

465

1

466

1

467

1

);

468

1

469

470

#[test]

471

1

fn unwrap_nested_or_not_changed() {

472

1

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

473

1

474

1

    let expr = Expression::Or(

475

1

        Metadata::new(),

476

1

        vec![

477

1

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

478

1

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

479

1

],

480

1

);

481

1

482

1

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

483

1

484

1

    assert!(result.is_err());

485

1

486

487

#[test]

488

1

fn unwrap_nested_and_not_changed() {

489

1

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

490

1

491

1

    let expr = Expression::And(

492

1

        Metadata::new(),

493

1

        vec![

494

1

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

495

1

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

496

1

],

497

1

);

498

1

499

1

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

500

1

501

1

    assert!(result.is_err());

502

1

503

504

#[test]

505

1

fn remove_trivial_and_or() {

506

1

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

507

1

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

508

1

509

1

    let mut expr_and = Expression::And(

510

1

        Metadata::new(),

511

1

        vec![Expression::Atomic(

512

1

            Metadata::new(),

513

1

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

514

1

)],

515

1

);

516

1

    let mut expr_or = Expression::Or(

517

1

        Metadata::new(),

518

1

        vec![Expression::Atomic(

519

1

            Metadata::new(),

520

1

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

521

1

)],

522

1

);

523

1

524

1

    expr_and = remove_trivial_and

525

1

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

526

1

        .unwrap()

527

1

        .new_expression;

528

1

    expr_or = remove_trivial_or

529

1

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

530

1

        .unwrap()

531

1

        .new_expression;

532

1

533

1

    assert_eq!(

534

1

        expr_and,

535

1

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

536

1

);

537

1

    assert_eq!(

538

1

        expr_or,

539

1

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

540

1

);

541

1

542

543

#[test]

544

1

fn rule_distribute_not_over_and() {

545

1

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

546

1

547

1

    let mut expr = Expression::Not(

548

1

        Metadata::new(),

549

1

        Box::new(Expression::And(

550

1

            Metadata::new(),

551

1

            vec![

552

1

                Expression::Atomic(

553

1

                    Metadata::new(),

554

1

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

555

1

),

556

1

                Expression::Atomic(

557

1

                    Metadata::new(),

558

1

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

559

1

),

560

1

],

561

1

)),

562

1

);

563

1

564

1

    expr = distribute_not_over_and

565

1

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

566

1

        .unwrap()

567

1

        .new_expression;

568

1

569

1

    assert_eq!(

570

1

        expr,

571

1

        Expression::Or(

572

1

            Metadata::new(),

573

1

            vec![

574

1

                Expression::Not(

575

1

                    Metadata::new(),

576

1

                    Box::new(Expression::Atomic(

577

1

                        Metadata::new(),

578

1

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

579

1

))

580

1

),

581

1

                Expression::Not(

582

1

                    Metadata::new(),

583

1

                    Box::new(Expression::Atomic(

584

1

                        Metadata::new(),

585

1

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

586

1

))

587

1

),

588

1

589

1

590

1

);

591

1

592

593

#[test]

594

1

fn rule_distribute_not_over_or() {

595

1

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

596

1

597

1

    let mut expr = Expression::Not(

598

1

        Metadata::new(),

599

1

        Box::new(Expression::Or(

600

1

            Metadata::new(),

601

1

            vec![

602

1

                Expression::Atomic(

603

1

                    Metadata::new(),

604

1

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

605

1

),

606

1

                Expression::Atomic(

607

1

                    Metadata::new(),

608

1

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

609

1

),

610

1

],

611

1

)),

612

1

);

613

1

614

1

    expr = distribute_not_over_or

615

1

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

616

1

        .unwrap()

617

1

        .new_expression;

618

1

619

1

    assert_eq!(

620

1

        expr,

621

1

        Expression::And(

622

1

            Metadata::new(),

623

1

            vec![

624

1

                Expression::Not(

625

1

                    Metadata::new(),

626

1

                    Box::new(Expression::Atomic(

627

1

                        Metadata::new(),

628

1

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

629

1

))

630

1

),

631

1

                Expression::Not(

632

1

                    Metadata::new(),

633

1

                    Box::new(Expression::Atomic(

634

1

                        Metadata::new(),

635

1

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

636

1

))

637

1

),

638

1

639

1

640

1

);

641

1

642

643

#[test]

644

1

fn rule_distribute_not_over_and_not_changed() {

645

1

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

646

1

647

1

    let expr = Expression::Not(

648

1

        Metadata::new(),

649

1

        Box::new(Expression::Atomic(

650

1

            Metadata::new(),

651

1

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

652

1

)),

653

1

);

654

1

655

1

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

656

1

657

1

    assert!(result.is_err());

658

1

659

660

#[test]

661

1

fn rule_distribute_not_over_or_not_changed() {

662

1

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

663

1

664

1

    let expr = Expression::Not(

665

1

        Metadata::new(),

666

1

        Box::new(Expression::Atomic(

667

1

            Metadata::new(),

668

1

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

669

1

)),

670

1

);

671

1

672

1

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

673

1

674

1

    assert!(result.is_err());

675

1

676

677

#[test]

678

1

fn rule_distribute_or_over_and() {

679

1

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

680

1

681

1

    let expr = Expression::Or(

682

1

        Metadata::new(),

683

1

        vec![

684

1

            Expression::And(

685

1

                Metadata::new(),

686

1

                vec![

687

1

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

688

1

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

689

1

],

690

1

),

691

1

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

692

1

],

693

1

);

694

1

695

1

    let red = distribute_or_over_and

696

1

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

697

1

        .unwrap();

698

1

699

1

    assert_eq!(

700

1

        red.new_expression,

701

1

        Expression::And(

702

1

            Metadata::new(),

703

1

            vec![

704

1

                Expression::Or(

705

1

                    Metadata::new(),

706

1

                    vec![

707

1

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

708

1

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

709

1

710

1

),

711

1

                Expression::Or(

712

1

                    Metadata::new(),

713

1

                    vec![

714

1

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

715

1

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

716

1

717

1

),

718

1

719

1

),

720

1

);

721

1

722

723

///

724

/// Reduce and solve:

725

/// ```text

726

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

727

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

728

/// such that a < b

729

/// ```

730

///

731

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

732

/// of applying the rules manually.

733

#[test]

734

1

fn rewrite_solve_xyz() {

735

1

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

736

737

1

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

738

1

        Ok(rs) => rs,

739

        Err(e) => {

740

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

741

            exit(1);

742

743

};

744

1

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

745

1

746

1

    // Create variables and domains

747

1

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

748

1

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

749

1

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

750

1

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

751

1

752

1

    // Construct nested expression

753

1

    let nested_expr = Expression::And(

754

1

        Metadata::new(),

755

1

        vec![

756

1

            Expression::Eq(

757

1

                Metadata::new(),

758

1

                Box::new(Expression::Sum(

759

1

                    Metadata::new(),

760

1

                    vec![

761

1

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

762

1

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

763

1

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

764

1

],

765

1

)),

766

1

                Box::new(Expression::Atomic(

767

1

                    Metadata::new(),

768

1

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

769

1

)),

770

1

),

771

1

            Expression::Lt(

772

1

                Metadata::new(),

773

1

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

774

1

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

775

1

),

776

1

],

777

1

);

778

779

1

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

780

1

        Ok(rs) => rs,

781

        Err(e) => {

782

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

783

            exit(1);

784

785

};

786

787

    // Apply rewrite function to the nested expression

788

1

    let rewritten_expr = rewrite_model(

789

1

        &Model::new(HashMap::new(), nested_expr, Default::default()),

790

1

        &rule_sets,

791

1

792

1

    .unwrap()

793

1

    .constraints;

794

1

795

1

    // Check if the expression is in its simplest form

796

1

    let expr = rewritten_expr.clone();

797

1

    assert!(is_simple(&expr));

798

799

    // Create model with variables and constraints

800

1

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

801

1

802

1

    // Insert variables and domains

803

1

    model.variables.insert(

804

1

        var_name_from_atom(&variable_a.clone()),

805

1

        DecisionVariable {

806

1

            domain: domain.clone(),

807

1

},

808

1

);

809

1

    model.variables.insert(

810

1

        var_name_from_atom(&variable_b.clone()),

811

1

        DecisionVariable {

812

1

            domain: domain.clone(),

813

1

},

814

1

);

815

1

    model.variables.insert(

816

1

        var_name_from_atom(&variable_c.clone()),

817

1

        DecisionVariable {

818

1

            domain: domain.clone(),

819

1

},

820

1

);

821

1

822

1

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

823

1

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

824

1

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

825

1

826

827

#[test]

828

1

fn rewrite_solve_xyz_parameterized() {

829

1

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

830

831

1

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

832

1

        Ok(rs) => rs,

833

        Err(e) => {

834

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

835

            exit(1);

836

837

};

838

1

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

839

1

840

1

    // Create variables and domain

841

1

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

842

1

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

843

1

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

844

1

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

845

1

846

1

    // Create a vector of test cases with varying number of OR clauses

847

1

    let test_cases = vec![1, 2, 3, 4];

848

849

5

    for num_or_clauses in test_cases {

850

        // Construct OR'd expression

851

4

        let mut or_exprs = Vec::new();

852

10

        for _i in 0..num_or_clauses {

853

10

            let expr = Expression::And(

854

10

                Metadata::new(),

855

10

                vec![

856

10

                    Expression::Eq(

857

10

                        Metadata::new(),

858

10

                        Box::new(Expression::Sum(

859

10

                            Metadata::new(),

860

10

                            vec![

861

10

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

862

10

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

863

10

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

864

10

],

865

10

)),

866

10

                        Box::new(Expression::Atomic(

867

10

                            Metadata::new(),

868

10

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

869

10

)),

870

10

),

871

10

                    Expression::Lt(

872

10

                        Metadata::new(),

873

10

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

874

10

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

875

10

),

876

10

],

877

10

);

878

10

            or_exprs.push(expr);

879

10

880

4

        let nested_expr = Expression::Or(Metadata::new(), or_exprs);

881

4

882

4

        let model_for_rewrite = Model::new(HashMap::new(), nested_expr.clone(), Default::default());

883

4

        let model_for_rewrite_unoptimized =

884

4

            Model::new(HashMap::new(), nested_expr.clone(), Default::default());

885

4

886

4

        // Apply rewrite function to the nested expression

887

4

        let rewritten_expr = rewrite_model(&model_for_rewrite, &rule_sets)

888

4

            .unwrap()

889

4

            .constraints;

890

4

891

4

        env::set_var("OPTIMIZATIONS", "0");

892

4

893

4

        let rewritten_expr_unoptimized = rewrite_model(&model_for_rewrite_unoptimized, &rule_sets)

894

4

            .unwrap()

895

4

            .constraints;

896

4

897

4

        env::remove_var("OPTIMIZATIONS");

898

4

899

4

        let info_file_name_optimized = format!("rewrite_solve_xyz_optimized_{}", num_or_clauses);

900

4

        let info_file_name_unoptimized =

901

4

            format!("rewrite_solve_xyz_unoptimized_{}", num_or_clauses);

902

4

903

4

        save_stats_json(

904

4

            model_for_rewrite.context,

905

4

            "tests",

906

4

            &info_file_name_optimized,

907

4

908

4

        .expect("Could not save stats!");

909

4

        save_stats_json(

910

4

            model_for_rewrite_unoptimized.context,

911

4

            "tests",

912

4

            &info_file_name_unoptimized,

913

4

914

4

        .expect("Could not save stats!");

915

4

916

4

        // Check if the expression is in its simplest form

917

4

        let expr = rewritten_expr.clone();

918

4

        assert!(is_simple(&expr));

919

920

4

        let expr_unoptimized = rewritten_expr_unoptimized.clone();

921

4

        assert!(is_simple(&expr_unoptimized));

922

923

        // Create model with variables and constraints

924

4

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

925

4

        let mut model_unoptimized = Model::new(

926

4

            HashMap::new(),

927

4

            rewritten_expr_unoptimized,

928

4

            Default::default(),

929

4

);

930

4

931

4

        // Insert variables and domains

932

4

        model.variables.insert(

933

4

            var_name_from_atom(&variable_a.clone()),

934

4

            DecisionVariable {

935

4

                domain: domain.clone(),

936

4

},

937

4

);

938

4

        model.variables.insert(

939

4

            var_name_from_atom(&variable_b.clone()),

940

4

            DecisionVariable {

941

4

                domain: domain.clone(),

942

4

},

943

4

);

944

4

        model.variables.insert(

945

4

            var_name_from_atom(&variable_c.clone()),

946

4

            DecisionVariable {

947

4

                domain: domain.clone(),

948

4

},

949

4

);

950

4

951

4

        model_unoptimized.variables.insert(

952

4

            var_name_from_atom(&variable_a.clone()),

953

4

            DecisionVariable {

954

4

                domain: domain.clone(),

955

4

},

956

4

);

957

4

        model_unoptimized.variables.insert(

958

4

            var_name_from_atom(&variable_b.clone()),

959

4

            DecisionVariable {

960

4

                domain: domain.clone(),

961

4

},

962

4

);

963

4

        model_unoptimized.variables.insert(

964

4

            var_name_from_atom(&variable_c.clone()),

965

4

            DecisionVariable {

966

4

                domain: domain.clone(),

967

4

},

968

4

);

969

4

970

4

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

971

4

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

972

4

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

973

4

974

4

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

975

4

        let solver_unoptimized = solver_unoptimized.load_model(model_unoptimized).unwrap();

976

4

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

977

4

978

1

979

980

struct RuleResult<'a> {

981

    #[allow(dead_code)]

982

    rule: &'a Rule<'a>,

983

    new_expression: Expression,

984

985

986

/// # Returns

987

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

988

/// - False otherwise.

989

9

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

990

9

    let rules = get_rules();

991

9

    let mut new = expression.clone();

992

9

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

993

        new = step;

994

995

9

    new == *expression

996

9

997

998

/// # Returns

999

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

1000

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

1001

4233

fn is_simple_iteration<'a>(

1002

4233

    expression: &'a Expression,

1003

4233

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

1004

4233

) -> Option<Expression> {

1005

4233

    let rule_results = apply_all_rules(expression, rules);

1006

4233

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

1007

        return Some(new);

1008

    } else {

1009

4233

        let mut sub = expression.children();

1010

4233

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

1011

4224

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

1012

                sub[i] = new;

1013

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

1014

4224

1015

1016

1017

4233

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

1018

4233

1019

1020

/// # Returns

1021

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

1022

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

1023

4233

fn apply_all_rules<'a>(

1024

4233

    expression: &'a Expression,

1025

4233

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

1026

4233

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

1027

4233

    let mut results = Vec::new();

1028

165087

    for rule in rules {

1029

160854

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

1030

            Ok(red) => {

1031

                results.push(RuleResult {

1032

                    rule,

1033

                    new_expression: red.new_expression,

1034

});

1035

1036

160854

            Err(_) => continue,

1037

1038

1039

4233

    results

1040

4233

1041

1042

/// # Returns

1043

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

1044

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

1045

4233

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

1046

4233

    if results.is_empty() {

1047

4233

        return None;

1048

1049

    // Return the first result for now

1050

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

1051

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

1052

4233

1053

1054

#[test]

1055

1

fn eval_const_int() {

1056

1

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

1057

1

    let result = eval_constant(&expr);

1058

1

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

1059

1

1060

1061

#[test]

1062

1

fn eval_const_bool() {

1063

1

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

1064

1

    let result = eval_constant(&expr);

1065

1

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

1066

1

1067

1068

#[test]

1069

1

fn eval_const_and() {

1070

1

    let expr = Expression::And(

1071

1

        Metadata::new(),

1072

1

        vec![

1073

1

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

1074

1

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

1075

1

],

1076

1

);

1077

1

    let result = eval_constant(&expr);

1078

1

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

1079

1

1080

1081

#[test]

1082

1

fn eval_const_ref() {

1083

1

    let expr = Expression::Atomic(

1084

1

        Metadata::new(),

1085

1

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

1086

1

);

1087

1

    let result = eval_constant(&expr);

1088

1

    assert_eq!(result, None);

1089

1

1090

1091

#[test]

1092

1

fn eval_const_nested_ref() {

1093

1

    let expr = Expression::Sum(

1094

1

        Metadata::new(),

1095

1

        vec![

1096

1

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

1097

1

            Expression::And(

1098

1

                Metadata::new(),

1099

1

                vec![

1100

1

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

1101

1

                    Expression::Atomic(

1102

1

                        Metadata::new(),

1103

1

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

1104

1

),

1105

1

],

1106

1

),

1107

1

],

1108

1

);

1109

1

    let result = eval_constant(&expr);

1110

1

    assert_eq!(result, None);

1111

1

1112

1113

#[test]

1114

1

fn eval_const_eq_int() {

1115

1

    let expr = Expression::Eq(

1116

1

        Metadata::new(),

1117

1

        Box::new(Expression::Atomic(

1118

1

            Metadata::new(),

1119

1

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

1120

1

)),

1121

1

        Box::new(Expression::Atomic(

1122

1

            Metadata::new(),

1123

1

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

1124

1

)),

1125

1

);

1126

1

    let result = eval_constant(&expr);

1127

1

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

1128

1

1129

1130

#[test]

1131

1

fn eval_const_eq_bool() {

1132

1

    let expr = Expression::Eq(

1133

1

        Metadata::new(),

1134

1

        Box::new(Expression::Atomic(

1135

1

            Metadata::new(),

1136

1

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

1137

1

)),

1138

1

        Box::new(Expression::Atomic(

1139

1

            Metadata::new(),

1140

1

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

1141

1

)),

1142

1

);

1143

1

    let result = eval_constant(&expr);

1144

1

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

1145

1

1146

1147

#[test]

1148

1

fn eval_const_eq_mixed() {

1149

1

    let expr = Expression::Eq(

1150

1

        Metadata::new(),

1151

1

        Box::new(Expression::Atomic(

1152

1

            Metadata::new(),

1153

1

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

1154

1

)),

1155

1

        Box::new(Expression::Atomic(

1156

1

            Metadata::new(),

1157

1

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

1158

1

)),

1159

1

);

1160

1

    let result = eval_constant(&expr);

1161

1

    assert_eq!(result, None);

1162

1

1163

1164

#[test]

1165

1

fn eval_const_sum_mixed() {

1166

1

    let expr = Expression::Sum(

1167

1

        Metadata::new(),

1168

1

        vec![

1169

1

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

1170

1

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

1171

1

],

1172

1

);

1173

1

    let result = eval_constant(&expr);

1174

1

    assert_eq!(result, None);

1175

1

1176

1177

#[test]

1178

1

fn eval_const_sum_xyz() {

1179

1

    let expr = Expression::And(

1180

1

        Metadata::new(),

1181

1

        vec![

1182

1

            Expression::Eq(

1183

1

                Metadata::new(),

1184

1

                Box::new(Expression::Sum(

1185

1

                    Metadata::new(),

1186

1

                    vec![

1187

1

                        Expression::Atomic(

1188

1

                            Metadata::new(),

1189

1

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

1190

1

),

1191

1

                        Expression::Atomic(

1192

1

                            Metadata::new(),

1193

1

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

1194

1

),

1195

1

                        Expression::Atomic(

1196

1

                            Metadata::new(),

1197

1

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

1198

1

),

1199

1

],

1200

1

)),

1201

1

                Box::new(Expression::Atomic(

1202

1

                    Metadata::new(),

1203

1

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

1204

1

)),

1205

1

),

1206

1

            Expression::Geq(

1207

1

                Metadata::new(),

1208

1

                Box::new(Expression::Atomic(

1209

1

                    Metadata::new(),

1210

1

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

1211

1

)),

1212

1

                Box::new(Expression::Atomic(

1213

1

                    Metadata::new(),

1214

1

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

1215

1

)),

1216

1

),

1217

1

],

1218

1

);

1219

1

    let result = eval_constant(&expr);

1220

1

    assert_eq!(result, None);

1221

1

1222

1223

#[test]

1224

1

fn eval_const_or() {

1225

1

    let expr = Expression::Or(

1226

1

        Metadata::new(),

1227

1

        vec![

1228

1

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

1229

1

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

1230

1

],

1231

1

);

1232

1

    let result = eval_constant(&expr);

1233

1

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

1234

1