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_factor(f: &Factor) -> Name {

18

27

    <Factor as Biplate<Name>>::universe_bi(f)[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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

32

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

33

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

41

1

            Expression::FactorE(

42

1

                Metadata::new(),

43

1

                Factor::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::FactorE(_, Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

79

1

                Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

80

1

                Expression::Sum(

81

1

                    Metadata::new(),

82

1

                    vec![

83

1

                        Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

84

1

                        Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

85

1

],

86

1

),

87

1

                Expression::FactorE(

88

1

                    Metadata::new(),

89

1

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

90

1

),

91

1

],

92

1

)),

93

1

        Box::new(Expression::FactorE(

94

1

            Metadata::new(),

95

1

            Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

104

1

                Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

105

1

                Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(3))),

106

1

                Expression::FactorE(

107

1

                    Metadata::new(),

108

1

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

109

1

),

110

1

],

111

1

)),

112

1

        Box::new(Expression::FactorE(

113

1

            Metadata::new(),

114

1

            Factor::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::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

159

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

160

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

189

1

                Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

190

1

],

191

1

)),

192

1

        Box::new(Expression::FactorE(

193

1

            Metadata::new(),

194

1

            Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

209

1

                Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

210

1

],

211

1

            Box::new(Expression::FactorE(

212

1

                Metadata::new(),

213

1

                Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Int(2))),

239

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(3))),

240

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::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::FactorE(

264

1

                    Metadata::new(),

265

1

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

266

1

),

267

1

                Expression::FactorE(

268

1

                    Metadata::new(),

269

1

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

270

1

),

271

1

                Expression::FactorE(

272

1

                    Metadata::new(),

273

1

                    Factor::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::FactorE(

289

1

                    Metadata::new(),

290

1

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

291

1

),

292

1

                Expression::FactorE(

293

1

                    Metadata::new(),

294

1

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

295

1

),

296

1

                Expression::FactorE(

297

1

                    Metadata::new(),

298

1

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

299

1

),

300

1

],

301

1

            Box::new(Expression::FactorE(

302

1

                Metadata::new(),

303

1

                Factor::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::FactorE(

312

1

            Metadata::new(),

313

1

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

314

1

)),

315

1

        Box::new(Expression::FactorE(

316

1

            Metadata::new(),

317

1

            Factor::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::FactorE(

329

1

                Metadata::new(),

330

1

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

331

1

)),

332

1

            Box::new(Expression::FactorE(

333

1

                Metadata::new(),

334

1

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

335

1

)),

336

1

            Box::new(Expression::FactorE(

337

1

                Metadata::new(),

338

1

                Factor::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::FactorE(

381

1

                Metadata::new(),

382

1

                Factor::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::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

409

1

                    Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(false))),

410

1

],

411

1

),

412

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

427

1

                Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(false))),

428

1

                Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

445

1

                    Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(false))),

446

1

],

447

1

),

448

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

463

1

                Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(false))),

464

1

                Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

478

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

495

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(

512

1

            Metadata::new(),

513

1

            Factor::Literal(Literal::Bool(true)),

514

1

)],

515

1

);

516

1

    let mut expr_or = Expression::Or(

517

1

        Metadata::new(),

518

1

        vec![Expression::FactorE(

519

1

            Metadata::new(),

520

1

            Factor::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::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true)))

536

1

);

537

1

    assert_eq!(

538

1

        expr_or,

539

1

        Expression::FactorE(Metadata::new(), Factor::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::FactorE(

553

1

                    Metadata::new(),

554

1

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

555

1

),

556

1

                Expression::FactorE(

557

1

                    Metadata::new(),

558

1

                    Factor::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::FactorE(

577

1

                        Metadata::new(),

578

1

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

579

1

))

580

1

),

581

1

                Expression::Not(

582

1

                    Metadata::new(),

583

1

                    Box::new(Expression::FactorE(

584

1

                        Metadata::new(),

585

1

                        Factor::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::FactorE(

603

1

                    Metadata::new(),

604

1

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

605

1

),

606

1

                Expression::FactorE(

607

1

                    Metadata::new(),

608

1

                    Factor::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::FactorE(

627

1

                        Metadata::new(),

628

1

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

629

1

))

630

1

),

631

1

                Expression::Not(

632

1

                    Metadata::new(),

633

1

                    Box::new(Expression::FactorE(

634

1

                        Metadata::new(),

635

1

                        Factor::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::FactorE(

650

1

            Metadata::new(),

651

1

            Factor::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::FactorE(

667

1

            Metadata::new(),

668

1

            Factor::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::FactorE(Metadata::new(), Factor::Reference(Name::MachineName(1))),

688

1

                    Expression::FactorE(Metadata::new(), Factor::Reference(Name::MachineName(2))),

689

1

],

690

1

),

691

1

            Expression::FactorE(Metadata::new(), Factor::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::FactorE(

708

1

                            Metadata::new(),

709

1

                            Factor::Reference(Name::MachineName(3))

710

1

),

711

1

                        Expression::FactorE(

712

1

                            Metadata::new(),

713

1

                            Factor::Reference(Name::MachineName(1))

714

1

),

715

1

716

1

),

717

1

                Expression::Or(

718

1

                    Metadata::new(),

719

1

                    vec![

720

1

                        Expression::FactorE(

721

1

                            Metadata::new(),

722

1

                            Factor::Reference(Name::MachineName(3))

723

1

),

724

1

                        Expression::FactorE(

725

1

                            Metadata::new(),

726

1

                            Factor::Reference(Name::MachineName(2))

727

1

),

728

1

729

1

),

730

1

731

1

),

732

1

);

733

1

734

735

// #[test]

736

// fn rule_ensure_div() {

737

//     let ensure_div = get_rule_by_name("ensure_div").unwrap();

738

739

//     let expr = Expression::Div(

740

//         Metadata::new(),

741

//         Box::new(Expression::FactorE(

742

//             Metadata::new(),

743

//Factor::ReferenceF(Name::UserName("a".to_string())),

744

//         )),

745

//         Box::new(Expression::FactorE(

746

//             Metadata::new(),

747

//Factor::ReferenceF(Name::UserName("b".to_string())),

748

//         )),

749

//     );

750

751

//     let red = ensure_div.apply(&expr, &Model::new_empty(Default::default())).unwrap();

752

753

//     assert_eq!(

754

//         red.new_expression,

755

//         Expression::SafeDiv(

756

//             Metadata::new(),

757

//             Box::new(Expression::FactorE(

758

//                 Metadata::new(),

759

//Factor::ReferenceF(Name::UserName("a".to_string()))

760

//             )),

761

//             Box::new(Expression::FactorE(

762

//                 Metadata::new(),

763

//Factor::ReferenceF(Name::UserName("b".to_string()))

764

//             )),

765

//         ),

766

//     );

767

//     assert_eq!(

768

//         red.new_top,

769

//         Expression::Neq(

770

//             Metadata::new(),

771

//             Box::new(Expression::FactorE(

772

//                 Metadata::new(),

773

//Factor::ReferenceF(Name::UserName("b".to_string()))

774

//             )),

775

//             Box::new(Expression::Constant(Metadata::new(), Constant::Int(0)))

776

//         )

777

//     );

778

// }

779

780

///

781

/// Reduce and solve:

782

/// ```text

783

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

784

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

785

/// such that a < b

786

/// ```

787

///

788

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

789

/// of applying the rules manually.

790

#[test]

791

1

fn rewrite_solve_xyz() {

792

1

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

793

794

1

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

795

1

        Ok(rs) => rs,

796

        Err(e) => {

797

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

798

            exit(1);

799

800

};

801

1

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

802

1

803

1

    // Create variables and domains

804

1

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

805

1

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

806

1

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

807

1

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

808

1

809

1

    // Construct nested expression

810

1

    let nested_expr = Expression::And(

811

1

        Metadata::new(),

812

1

        vec![

813

1

            Expression::Eq(

814

1

                Metadata::new(),

815

1

                Box::new(Expression::Sum(

816

1

                    Metadata::new(),

817

1

                    vec![

818

1

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

819

1

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

820

1

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

821

1

],

822

1

)),

823

1

                Box::new(Expression::FactorE(

824

1

                    Metadata::new(),

825

1

                    Factor::Literal(Literal::Int(4)),

826

1

)),

827

1

),

828

1

            Expression::Lt(

829

1

                Metadata::new(),

830

1

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

831

1

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

832

1

),

833

1

],

834

1

);

835

836

1

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

837

1

        Ok(rs) => rs,

838

        Err(e) => {

839

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

840

            exit(1);

841

842

};

843

844

    // Apply rewrite function to the nested expression

845

1

    let rewritten_expr = rewrite_model(

846

1

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

847

1

        &rule_sets,

848

1

849

1

    .unwrap()

850

1

    .constraints;

851

1

852

1

    // Check if the expression is in its simplest form

853

1

    let expr = rewritten_expr.clone();

854

1

    assert!(is_simple(&expr));

855

856

    // Create model with variables and constraints

857

1

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

858

1

859

1

    // Insert variables and domains

860

1

    model.variables.insert(

861

1

        var_name_from_factor(&variable_a.clone()),

862

1

        DecisionVariable {

863

1

            domain: domain.clone(),

864

1

},

865

1

);

866

1

    model.variables.insert(

867

1

        var_name_from_factor(&variable_b.clone()),

868

1

        DecisionVariable {

869

1

            domain: domain.clone(),

870

1

},

871

1

);

872

1

    model.variables.insert(

873

1

        var_name_from_factor(&variable_c.clone()),

874

1

        DecisionVariable {

875

1

            domain: domain.clone(),

876

1

},

877

1

);

878

1

879

1

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

880

1

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

881

1

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

882

1

883

884

#[test]

885

1

fn rewrite_solve_xyz_parameterized() {

886

1

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

887

888

1

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

889

1

        Ok(rs) => rs,

890

        Err(e) => {

891

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

892

            exit(1);

893

894

};

895

1

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

896

1

897

1

    // Create variables and domain

898

1

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

899

1

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

900

1

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

901

1

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

902

1

903

1

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

904

1

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

905

906

5

    for num_or_clauses in test_cases {

907

        // Construct OR'd expression

908

4

        let mut or_exprs = Vec::new();

909

10

        for _i in 0..num_or_clauses {

910

10

            let expr = Expression::And(

911

10

                Metadata::new(),

912

10

                vec![

913

10

                    Expression::Eq(

914

10

                        Metadata::new(),

915

10

                        Box::new(Expression::Sum(

916

10

                            Metadata::new(),

917

10

                            vec![

918

10

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

919

10

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

920

10

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

921

10

],

922

10

)),

923

10

                        Box::new(Expression::FactorE(

924

10

                            Metadata::new(),

925

10

                            Factor::Literal(Literal::Int(4)),

926

10

)),

927

10

),

928

10

                    Expression::Lt(

929

10

                        Metadata::new(),

930

10

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

931

10

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

932

10

),

933

10

],

934

10

);

935

10

            or_exprs.push(expr);

936

10

937

4

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

938

4

939

4

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

940

4

        let model_for_rewrite_unoptimized =

941

4

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

942

4

943

4

        // Apply rewrite function to the nested expression

944

4

        let rewritten_expr = rewrite_model(&model_for_rewrite, &rule_sets)

945

4

            .unwrap()

946

4

            .constraints;

947

4

948

4

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

949

4

950

4

        let rewritten_expr_unoptimized = rewrite_model(&model_for_rewrite_unoptimized, &rule_sets)

951

4

            .unwrap()

952

4

            .constraints;

953

4

954

4

        env::remove_var("OPTIMIZATIONS");

955

4

956

4

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

957

4

        let info_file_name_unoptimized =

958

4

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

959

4

960

4

        save_stats_json(

961

4

            model_for_rewrite.context,

962

4

            "tests",

963

4

            &info_file_name_optimized,

964

4

965

4

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

966

4

        save_stats_json(

967

4

            model_for_rewrite_unoptimized.context,

968

4

            "tests",

969

4

            &info_file_name_unoptimized,

970

4

971

4

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

972

4

973

4

        // Check if the expression is in its simplest form

974

4

        let expr = rewritten_expr.clone();

975

4

        assert!(is_simple(&expr));

976

977

4

        let expr_unoptimized = rewritten_expr_unoptimized.clone();

978

4

        assert!(is_simple(&expr_unoptimized));

979

980

        // Create model with variables and constraints

981

4

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

982

4

        let mut model_unoptimized = Model::new(

983

4

            HashMap::new(),

984

4

            rewritten_expr_unoptimized,

985

4

            Default::default(),

986

4

);

987

4

988

4

        // Insert variables and domains

989

4

        model.variables.insert(

990

4

            var_name_from_factor(&variable_a.clone()),

991

4

            DecisionVariable {

992

4

                domain: domain.clone(),

993

4

},

994

4

);

995

4

        model.variables.insert(

996

4

            var_name_from_factor(&variable_b.clone()),

997

4

            DecisionVariable {

998

4

                domain: domain.clone(),

999

4

},

1000

4

);

1001

4

        model.variables.insert(

1002

4

            var_name_from_factor(&variable_c.clone()),

1003

4

            DecisionVariable {

1004

4

                domain: domain.clone(),

1005

4

},

1006

4

);

1007

4

1008

4

        model_unoptimized.variables.insert(

1009

4

            var_name_from_factor(&variable_a.clone()),

1010

4

            DecisionVariable {

1011

4

                domain: domain.clone(),

1012

4

},

1013

4

);

1014

4

        model_unoptimized.variables.insert(

1015

4

            var_name_from_factor(&variable_b.clone()),

1016

4

            DecisionVariable {

1017

4

                domain: domain.clone(),

1018

4

},

1019

4

);

1020

4

        model_unoptimized.variables.insert(

1021

4

            var_name_from_factor(&variable_c.clone()),

1022

4

            DecisionVariable {

1023

4

                domain: domain.clone(),

1024

4

},

1025

4

);

1026

4

1027

4

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

1028

4

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

1029

4

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

1030

4

1031

4

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

1032

4

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

1033

4

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

1034

4

1035

1

1036

1037

struct RuleResult<'a> {

1038

    #[allow(dead_code)]

1039

    rule: &'a Rule<'a>,

1040

    new_expression: Expression,

1041

1042

1043

/// # Returns

1044

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

1045

/// - False otherwise.

1046

9

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

1047

9

    let rules = get_rules();

1048

9

    let mut new = expression.clone();

1049

9

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

1050

        new = step;

1051

1052

9

    new == *expression

1053

9

1054

1055

/// # Returns

1056

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

1057

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

1058

4233

fn is_simple_iteration<'a>(

1059

4233

    expression: &'a Expression,

1060

4233

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

1061

4233

) -> Option<Expression> {

1062

4233

    let rule_results = apply_all_rules(expression, rules);

1063

4233

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

1064

        return Some(new);

1065

    } else {

1066

4233

        let mut sub = expression.children();

1067

4233

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

1068

4224

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

1069

                sub[i] = new;

1070

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

1071

4224

1072

1073

1074

4233

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

1075

4233

1076

1077

/// # Returns

1078

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

1079

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

1080

4233

fn apply_all_rules<'a>(

1081

4233

    expression: &'a Expression,

1082

4233

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

1083

4233

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

1084

4233

    let mut results = Vec::new();

1085

165087

    for rule in rules {

1086

160854

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

1087

            Ok(red) => {

1088

                results.push(RuleResult {

1089

                    rule,

1090

                    new_expression: red.new_expression,

1091

});

1092

1093

160854

            Err(_) => continue,

1094

1095

1096

4233

    results

1097

4233

1098

1099

/// # Returns

1100

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

1101

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

1102

4233

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

1103

4233

    if results.is_empty() {

1104

4233

        return None;

1105

1106

    // Return the first result for now

1107

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

1108

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

1109

4233

1110

1111

#[test]

1112

1

fn eval_const_int() {

1113

1

    let expr = Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1)));

1114

1

    let result = eval_constant(&expr);

1115

1

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

1116

1

1117

1118

#[test]

1119

1

fn eval_const_bool() {

1120

1

    let expr = Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true)));

1121

1

    let result = eval_constant(&expr);

1122

1

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

1123

1

1124

1125

#[test]

1126

1

fn eval_const_and() {

1127

1

    let expr = Expression::And(

1128

1

        Metadata::new(),

1129

1

        vec![

1130

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

1131

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(false))),

1132

1

],

1133

1

);

1134

1

    let result = eval_constant(&expr);

1135

1

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

1136

1

1137

1138

#[test]

1139

1

fn eval_const_ref() {

1140

1

    let expr = Expression::FactorE(

1141

1

        Metadata::new(),

1142

1

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

1143

1

);

1144

1

    let result = eval_constant(&expr);

1145

1

    assert_eq!(result, None);

1146

1

1147

1148

#[test]

1149

1

fn eval_const_nested_ref() {

1150

1

    let expr = Expression::Sum(

1151

1

        Metadata::new(),

1152

1

        vec![

1153

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

1154

1

            Expression::And(

1155

1

                Metadata::new(),

1156

1

                vec![

1157

1

                    Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

1158

1

                    Expression::FactorE(

1159

1

                        Metadata::new(),

1160

1

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

1161

1

),

1162

1

],

1163

1

),

1164

1

],

1165

1

);

1166

1

    let result = eval_constant(&expr);

1167

1

    assert_eq!(result, None);

1168

1

1169

1170

#[test]

1171

1

fn eval_const_eq_int() {

1172

1

    let expr = Expression::Eq(

1173

1

        Metadata::new(),

1174

1

        Box::new(Expression::FactorE(

1175

1

            Metadata::new(),

1176

1

            Factor::Literal(Literal::Int(1)),

1177

1

)),

1178

1

        Box::new(Expression::FactorE(

1179

1

            Metadata::new(),

1180

1

            Factor::Literal(Literal::Int(1)),

1181

1

)),

1182

1

);

1183

1

    let result = eval_constant(&expr);

1184

1

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

1185

1

1186

1187

#[test]

1188

1

fn eval_const_eq_bool() {

1189

1

    let expr = Expression::Eq(

1190

1

        Metadata::new(),

1191

1

        Box::new(Expression::FactorE(

1192

1

            Metadata::new(),

1193

1

            Factor::Literal(Literal::Bool(true)),

1194

1

)),

1195

1

        Box::new(Expression::FactorE(

1196

1

            Metadata::new(),

1197

1

            Factor::Literal(Literal::Bool(true)),

1198

1

)),

1199

1

);

1200

1

    let result = eval_constant(&expr);

1201

1

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

1202

1

1203

1204

#[test]

1205

1

fn eval_const_eq_mixed() {

1206

1

    let expr = Expression::Eq(

1207

1

        Metadata::new(),

1208

1

        Box::new(Expression::FactorE(

1209

1

            Metadata::new(),

1210

1

            Factor::Literal(Literal::Int(1)),

1211

1

)),

1212

1

        Box::new(Expression::FactorE(

1213

1

            Metadata::new(),

1214

1

            Factor::Literal(Literal::Bool(true)),

1215

1

)),

1216

1

);

1217

1

    let result = eval_constant(&expr);

1218

1

    assert_eq!(result, None);

1219

1

1220

1221

#[test]

1222

1

fn eval_const_sum_mixed() {

1223

1

    let expr = Expression::Sum(

1224

1

        Metadata::new(),

1225

1

        vec![

1226

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Int(1))),

1227

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(true))),

1228

1

],

1229

1

);

1230

1

    let result = eval_constant(&expr);

1231

1

    assert_eq!(result, None);

1232

1

1233

1234

#[test]

1235

1

fn eval_const_sum_xyz() {

1236

1

    let expr = Expression::And(

1237

1

        Metadata::new(),

1238

1

        vec![

1239

1

            Expression::Eq(

1240

1

                Metadata::new(),

1241

1

                Box::new(Expression::Sum(

1242

1

                    Metadata::new(),

1243

1

                    vec![

1244

1

                        Expression::FactorE(

1245

1

                            Metadata::new(),

1246

1

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

1247

1

),

1248

1

                        Expression::FactorE(

1249

1

                            Metadata::new(),

1250

1

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

1251

1

),

1252

1

                        Expression::FactorE(

1253

1

                            Metadata::new(),

1254

1

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

1255

1

),

1256

1

],

1257

1

)),

1258

1

                Box::new(Expression::FactorE(

1259

1

                    Metadata::new(),

1260

1

                    Factor::Literal(Literal::Int(4)),

1261

1

)),

1262

1

),

1263

1

            Expression::Geq(

1264

1

                Metadata::new(),

1265

1

                Box::new(Expression::FactorE(

1266

1

                    Metadata::new(),

1267

1

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

1268

1

)),

1269

1

                Box::new(Expression::FactorE(

1270

1

                    Metadata::new(),

1271

1

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

1272

1

)),

1273

1

),

1274

1

],

1275

1

);

1276

1

    let result = eval_constant(&expr);

1277

1

    assert_eq!(result, None);

1278

1

1279

1280

#[test]

1281

1

fn eval_const_or() {

1282

1

    let expr = Expression::Or(

1283

1

        Metadata::new(),

1284

1

        vec![

1285

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(false))),

1286

1

            Expression::FactorE(Metadata::new(), Factor::Literal(Literal::Bool(false))),

1287

1

],

1288

1

);

1289

1

    let result = eval_constant(&expr);

1290

1

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

1291

1