Grcov report - rewrite

1

use std::cell::RefCell;

2

use std::collections::VecDeque;

3

use std::process::exit;

4

use std::rc::Rc;

5

6

use conjure_core::rule_engine::rewrite_naive;

7

use conjure_core::solver::SolverFamily;

8

use conjure_core::{rule_engine::get_all_rules, rules::eval_constant};

9

use conjure_oxide::{

10

    ast::*,

11

    get_rule_by_name,

12

    rule_engine::resolve_rule_sets,

13

    solver::{adaptors, Solver},

14

    Metadata, Model, Rule,

15

};

16

use declaration::Declaration;

17

use uniplate::{Biplate, Uniplate};

18

19

3

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

20

3

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

21

3

    names[0].clone()

22

3

23

#[test]

24

1

fn rules_present() {

25

1

    let rules = get_all_rules();

26

1

    assert!(!rules.is_empty());

27

1

28

29

#[test]

30

1

fn sum_of_constants() {

31

1

    let valid_sum_expression = Expression::Sum(

32

1

        Metadata::new(),

33

1

        vec![

34

1

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

35

1

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

36

1

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

37

1

],

38

1

);

39

1

40

1

    let invalid_sum_expression = Expression::Sum(

41

1

        Metadata::new(),

42

1

        vec![

43

1

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

44

1

            Expression::Atomic(

45

1

                Metadata::new(),

46

1

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

47

1

),

48

1

],

49

1

);

50

1

51

1

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

52

53

1

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

54

1

55

56

4

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

57

4

    match expr {

58

4

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

59

4

            let mut sum = 0;

60

12

            for e in expressions {

61

8

                match e {

62

8

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

63

8

                        sum += value;

64

8

65

2

                    _ => return None,

66

67

68

2

            Some(sum)

69

70

        _ => None,

71

72

4

73

74

#[test]

75

1

fn recursive_sum_of_constants() {

76

1

    let complex_expression = Expression::Eq(

77

1

        Metadata::new(),

78

1

        Box::new(Expression::Sum(

79

1

            Metadata::new(),

80

1

            vec![

81

1

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

82

1

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

83

1

                Expression::Sum(

84

1

                    Metadata::new(),

85

1

                    vec![

86

1

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

87

1

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

88

1

],

89

1

),

90

1

                Expression::Atomic(

91

1

                    Metadata::new(),

92

1

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

93

1

),

94

1

],

95

1

)),

96

1

        Box::new(Expression::Atomic(

97

1

            Metadata::new(),

98

1

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

99

1

)),

100

1

);

101

1

    let correct_simplified_expression = Expression::Eq(

102

1

        Metadata::new(),

103

1

        Box::new(Expression::Sum(

104

1

            Metadata::new(),

105

1

            vec![

106

1

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

107

1

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

108

1

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

109

1

                Expression::Atomic(

110

1

                    Metadata::new(),

111

1

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

112

1

),

113

1

],

114

1

)),

115

1

        Box::new(Expression::Atomic(

116

1

            Metadata::new(),

117

1

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

118

1

)),

119

1

);

120

1

121

1

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

122

1

    assert_eq!(simplified_expression, correct_simplified_expression);

123

1

124

125

7

fn simplify_expression(expr: Expression) -> Expression {

126

7

    match expr {

127

2

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

128

1

            if let Some(result) =

129

2

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

130

131

1

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

132

            } else {

133

1

                Expression::Sum(

134

1

                    Metadata::new(),

135

1

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

136

1

137

138

139

1

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

140

1

            Metadata::new(),

141

1

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

142

1

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

143

1

),

144

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

145

            Metadata::new(),

146

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

147

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

148

),

149

4

        _ => expr,

150

151

7

152

153

#[test]

154

1

fn rule_sum_constants() {

155

1

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

156

1

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

157

1

158

1

    let mut expr = Expression::Sum(

159

1

        Metadata::new(),

160

1

        vec![

161

1

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

162

1

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

163

1

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

164

1

],

165

1

);

166

1

167

1

    expr = sum_constants

168

1

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

169

1

        .unwrap()

170

1

        .new_expression;

171

1

    expr = unwrap_sum

172

1

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

173

1

        .unwrap()

174

1

        .new_expression;

175

1

176

1

    assert_eq!(

177

1

        expr,

178

1

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

179

1

);

180

1

181

182

#[test]

183

1

fn rule_sum_geq() {

184

1

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

185

1

186

1

    let mut expr = Expression::Geq(

187

1

        Metadata::new(),

188

1

        Box::new(Expression::Sum(

189

1

            Metadata::new(),

190

1

            vec![

191

1

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

192

1

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

193

1

],

194

1

)),

195

1

        Box::new(Expression::Atomic(

196

1

            Metadata::new(),

197

1

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

198

1

)),

199

1

);

200

1

201

1

    expr = introduce_sumgeq

202

1

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

203

1

        .unwrap()

204

1

        .new_expression;

205

1

206

1

    assert_eq!(

207

1

        expr,

208

1

        Expression::FlatSumGeq(

209

1

            Metadata::new(),

210

1

            vec![

211

1

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

212

1

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

213

1

],

214

1

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

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_all_rules());

229

1

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

230

1

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

231

1

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

232

1

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

233

1

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

234

1

235

1

    // 2 + 3 - 1

236

1

    let mut expr1 = Expression::Sum(

237

1

        Metadata::new(),

238

1

        vec![

239

1

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

240

1

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

241

1

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

242

1

],

243

1

);

244

1

245

1

    expr1 = sum_constants

246

1

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

247

1

        .unwrap()

248

1

        .new_expression;

249

1

    expr1 = unwrap_sum

250

1

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

251

1

        .unwrap()

252

1

        .new_expression;

253

1

    assert_eq!(

254

1

        expr1,

255

1

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

256

1

);

257

258

    // a + b + c = 4

259

1

    expr1 = Expression::Leq(

260

1

        Metadata::new(),

261

1

        Box::new(Expression::Sum(

262

1

            Metadata::new(),

263

1

            vec![

264

1

                Expression::Atomic(

265

1

                    Metadata::new(),

266

1

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

267

1

),

268

1

                Expression::Atomic(

269

1

                    Metadata::new(),

270

1

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

271

1

),

272

1

                Expression::Atomic(

273

1

                    Metadata::new(),

274

1

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

275

1

),

276

1

],

277

1

)),

278

1

        Box::new(expr1),

279

1

);

280

1

    expr1 = introduce_sumleq

281

1

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

282

1

        .unwrap()

283

1

        .new_expression;

284

1

    assert_eq!(

285

1

        expr1,

286

1

        Expression::FlatSumLeq(

287

1

            Metadata::new(),

288

1

            vec![

289

1

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

290

1

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

291

1

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

292

1

],

293

1

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

294

1

295

1

);

296

297

    // a < b

298

1

    let mut expr2 = Expression::Lt(

299

1

        Metadata::new(),

300

1

        Box::new(Expression::Atomic(

301

1

            Metadata::new(),

302

1

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

303

1

)),

304

1

        Box::new(Expression::Atomic(

305

1

            Metadata::new(),

306

1

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

307

1

)),

308

1

);

309

1

    expr2 = lt_to_leq

310

1

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

311

1

        .unwrap()

312

1

        .new_expression;

313

1

314

1

    expr2 = leq_to_ineq

315

1

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

316

1

        .unwrap()

317

1

        .new_expression;

318

1

    assert_eq!(

319

1

        expr2,

320

1

        Expression::FlatIneq(

321

1

            Metadata::new(),

322

1

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

323

1

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

324

1

            Literal::Int(-1),

325

1

326

1

);

327

328

1

    let model = Model::new(

329

1

        Rc::new(RefCell::new(SymbolTable::new())),

330

1

        vec![expr1, expr2],

331

1

        Default::default(),

332

1

);

333

1

    model

334

1

        .symbols_mut()

335

1

        .insert(Rc::new(Declaration::new_var(

336

1

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

337

1

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

338

1

)))

339

1

        .unwrap();

340

1

    model

341

1

        .symbols_mut()

342

1

        .insert(Rc::new(Declaration::new_var(

343

1

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

344

1

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

345

1

)))

346

1

        .unwrap();

347

1

    model

348

1

        .symbols_mut()

349

1

        .insert(Rc::new(Declaration::new_var(

350

1

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

351

1

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

352

1

)))

353

1

        .unwrap();

354

1

355

1

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

356

1

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

357

1

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

358

1

359

360

#[test]

361

1

fn rule_remove_double_negation() {

362

1

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

363

1

364

1

    let mut expr = Expression::Not(

365

1

        Metadata::new(),

366

1

        Box::new(Expression::Not(

367

1

            Metadata::new(),

368

1

            Box::new(Expression::Atomic(

369

1

                Metadata::new(),

370

1

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

371

1

)),

372

1

)),

373

1

);

374

1

375

1

    expr = remove_double_negation

376

1

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

377

1

        .unwrap()

378

1

        .new_expression;

379

1

380

1

    assert_eq!(

381

1

        expr,

382

1

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

383

1

);

384

1

385

386

#[test]

387

1

fn remove_trivial_and_or() {

388

1

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

389

1

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

390

1

391

1

    let mut expr_and = Expression::And(

392

1

        Metadata::new(),

393

1

        vec![Expression::Atomic(

394

1

            Metadata::new(),

395

1

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

396

1

)],

397

1

);

398

1

    let mut expr_or = Expression::Or(

399

1

        Metadata::new(),

400

1

        vec![Expression::Atomic(

401

1

            Metadata::new(),

402

1

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

403

1

)],

404

1

);

405

1

406

1

    expr_and = remove_trivial_and

407

1

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

408

1

        .unwrap()

409

1

        .new_expression;

410

1

    expr_or = remove_trivial_or

411

1

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

412

1

        .unwrap()

413

1

        .new_expression;

414

1

415

1

    assert_eq!(

416

1

        expr_and,

417

1

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

418

1

);

419

1

    assert_eq!(

420

1

        expr_or,

421

1

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

422

1

);

423

1

424

425

#[test]

426

1

fn rule_distribute_not_over_and() {

427

1

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

428

1

429

1

    let mut expr = Expression::Not(

430

1

        Metadata::new(),

431

1

        Box::new(Expression::And(

432

1

            Metadata::new(),

433

1

            vec![

434

1

                Expression::Atomic(

435

1

                    Metadata::new(),

436

1

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

437

1

),

438

1

                Expression::Atomic(

439

1

                    Metadata::new(),

440

1

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

441

1

),

442

1

],

443

1

)),

444

1

);

445

1

446

1

    expr = distribute_not_over_and

447

1

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

448

1

        .unwrap()

449

1

        .new_expression;

450

1

451

1

    assert_eq!(

452

1

        expr,

453

1

        Expression::Or(

454

1

            Metadata::new(),

455

1

            vec![

456

1

                Expression::Not(

457

1

                    Metadata::new(),

458

1

                    Box::new(Expression::Atomic(

459

1

                        Metadata::new(),

460

1

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

461

1

))

462

1

),

463

1

                Expression::Not(

464

1

                    Metadata::new(),

465

1

                    Box::new(Expression::Atomic(

466

1

                        Metadata::new(),

467

1

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

468

1

))

469

1

),

470

1

471

1

472

1

);

473

1

474

475

#[test]

476

1

fn rule_distribute_not_over_or() {

477

1

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

478

1

479

1

    let mut expr = Expression::Not(

480

1

        Metadata::new(),

481

1

        Box::new(Expression::Or(

482

1

            Metadata::new(),

483

1

            vec![

484

1

                Expression::Atomic(

485

1

                    Metadata::new(),

486

1

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

487

1

),

488

1

                Expression::Atomic(

489

1

                    Metadata::new(),

490

1

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

491

1

),

492

1

],

493

1

)),

494

1

);

495

1

496

1

    expr = distribute_not_over_or

497

1

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

498

1

        .unwrap()

499

1

        .new_expression;

500

1

501

1

    assert_eq!(

502

1

        expr,

503

1

        Expression::And(

504

1

            Metadata::new(),

505

1

            vec![

506

1

                Expression::Not(

507

1

                    Metadata::new(),

508

1

                    Box::new(Expression::Atomic(

509

1

                        Metadata::new(),

510

1

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

511

1

))

512

1

),

513

1

                Expression::Not(

514

1

                    Metadata::new(),

515

1

                    Box::new(Expression::Atomic(

516

1

                        Metadata::new(),

517

1

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

518

1

))

519

1

),

520

1

521

1

522

1

);

523

1

524

525

#[test]

526

1

fn rule_distribute_not_over_and_not_changed() {

527

1

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

528

1

529

1

    let expr = Expression::Not(

530

1

        Metadata::new(),

531

1

        Box::new(Expression::Atomic(

532

1

            Metadata::new(),

533

1

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

534

1

)),

535

1

);

536

1

537

1

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

538

1

539

1

    assert!(result.is_err());

540

1

541

542

#[test]

543

1

fn rule_distribute_not_over_or_not_changed() {

544

1

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

545

1

546

1

    let expr = Expression::Not(

547

1

        Metadata::new(),

548

1

        Box::new(Expression::Atomic(

549

1

            Metadata::new(),

550

1

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

551

1

)),

552

1

);

553

1

554

1

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

555

1

556

1

    assert!(result.is_err());

557

1

558

559

#[test]

560

1

fn rule_distribute_or_over_and() {

561

1

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

562

1

563

1

    let expr = Expression::Or(

564

1

        Metadata::new(),

565

1

        vec![

566

1

            Expression::And(

567

1

                Metadata::new(),

568

1

                vec![

569

1

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

570

1

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

571

1

],

572

1

),

573

1

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

574

1

],

575

1

);

576

1

577

1

    let red = distribute_or_over_and

578

1

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

579

1

        .unwrap();

580

1

581

1

    assert_eq!(

582

1

        red.new_expression,

583

1

        Expression::And(

584

1

            Metadata::new(),

585

1

            vec![

586

1

                Expression::Or(

587

1

                    Metadata::new(),

588

1

                    vec![

589

1

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

590

1

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

591

1

592

1

),

593

1

                Expression::Or(

594

1

                    Metadata::new(),

595

1

                    vec![

596

1

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

597

1

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

598

1

599

1

),

600

1

601

1

),

602

1

);

603

1

604

605

///

606

/// Reduce and solve:

607

/// ```text

608

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

609

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

610

/// such that a < b

611

/// ```

612

///

613

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

614

/// of applying the rules manually.

615

#[test]

616

1

fn rewrite_solve_xyz() {

617

1

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

618

619

1

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

620

1

        Ok(rs) => rs,

621

        Err(e) => {

622

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

623

            exit(1);

624

625

};

626

1

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

627

1

628

1

    // Create variables and domains

629

1

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

630

1

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

631

1

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

632

1

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

633

1

634

1

    // Construct nested expression

635

1

    let nested_expr = Expression::And(

636

1

        Metadata::new(),

637

1

        vec![

638

1

            Expression::Eq(

639

1

                Metadata::new(),

640

1

                Box::new(Expression::Sum(

641

1

                    Metadata::new(),

642

1

                    vec![

643

1

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

644

1

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

645

1

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

646

1

],

647

1

)),

648

1

                Box::new(Expression::Atomic(

649

1

                    Metadata::new(),

650

1

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

651

1

)),

652

1

),

653

1

            Expression::Lt(

654

1

                Metadata::new(),

655

1

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

656

1

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

657

1

),

658

1

],

659

1

);

660

661

1

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

662

1

        Ok(rs) => rs,

663

        Err(e) => {

664

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

665

            exit(1);

666

667

};

668

669

    // Apply rewrite function to the nested expression

670

1

    let rewritten_expr = rewrite_naive(

671

1

        &Model::new(

672

1

            Rc::new(RefCell::new(SymbolTable::new())),

673

1

            vec![nested_expr],

674

1

            Default::default(),

675

1

),

676

1

        &rule_sets,

677

1

        true,

678

1

679

1

    .unwrap()

680

1

    .get_constraints_vec();

681

1

682

1

    // Check if the expression is in its simplest form

683

1

684

1

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

685

686

    // Create model with variables and constraints

687

1

    let model = Model::new(

688

1

        Rc::new(RefCell::new(SymbolTable::new())),

689

1

        rewritten_expr,

690

1

        Default::default(),

691

1

);

692

1

693

1

    // Insert variables and domains

694

1

    model

695

1

        .symbols_mut()

696

1

        .insert(Rc::new(Declaration::new_var(

697

1

            var_name_from_atom(&variable_a.clone()),

698

1

            domain.clone(),

699

1

)))

700

1

        .unwrap();

701

1

    model

702

1

        .symbols_mut()

703

1

        .insert(Rc::new(Declaration::new_var(

704

1

            var_name_from_atom(&variable_b.clone()),

705

1

            domain.clone(),

706

1

)))

707

1

        .unwrap();

708

1

    model

709

1

        .symbols_mut()

710

1

        .insert(Rc::new(Declaration::new_var(

711

1

            var_name_from_atom(&variable_c.clone()),

712

1

            domain.clone(),

713

1

)))

714

1

        .unwrap();

715

1

716

1

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

717

1

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

718

1

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

719

1

720

721

struct RuleResult<'a> {

722

    #[allow(dead_code)]

723

    rule: &'a Rule<'a>,

724

    new_expression: Expression,

725

726

727

/// # Returns

728

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

729

/// - False otherwise.

730

1

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

731

1

    let rules = get_all_rules();

732

1

    let mut new = expression.clone();

733

1

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

734

        new = step;

735

736

1

    new == *expression

737

1

738

739

/// # Returns

740

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

741

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

742

4

fn is_simple_iteration<'a>(

743

4

    expression: &'a Expression,

744

4

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

745

4

) -> Option<Expression> {

746

4

    let rule_results = apply_all_rules(expression, rules);

747

4

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

748

        return Some(new);

749

    } else {

750

4

        let mut sub = expression.children();

751

4

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

752

3

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

753

                sub[i] = new;

754

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

755

3

756

757

758

4

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

759

4

760

761

/// # Returns

762

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

763

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

764

4

fn apply_all_rules<'a>(

765

4

    expression: &'a Expression,

766

4

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

767

4

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

768

4

    let mut results = Vec::new();

769

224

    for rule in rules {

770

220

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

771

            Ok(red) => {

772

                results.push(RuleResult {

773

                    rule,

774

                    new_expression: red.new_expression,

775

});

776

777

220

            Err(_) => continue,

778

779

780

4

    results

781

4

782

783

/// # Returns

784

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

785

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

786

4

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

787

4

    if results.is_empty() {

788

4

        return None;

789

790

    // Return the first result for now

791

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

792

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

793

4

794

795

#[test]

796

1

fn eval_const_int() {

797

1

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

798

1

    let result = eval_constant(&expr);

799

1

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

800

1

801

802

#[test]

803

1

fn eval_const_bool() {

804

1

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

805

1

    let result = eval_constant(&expr);

806

1

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

807

1

808

809

#[test]

810

1

fn eval_const_and() {

811

1

    let expr = Expression::And(

812

1

        Metadata::new(),

813

1

        vec![

814

1

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

815

1

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

816

1

],

817

1

);

818

1

    let result = eval_constant(&expr);

819

1

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

820

1

821

822

#[test]

823

1

fn eval_const_ref() {

824

1

    let expr = Expression::Atomic(

825

1

        Metadata::new(),

826

1

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

827

1

);

828

1

    let result = eval_constant(&expr);

829

1

    assert_eq!(result, None);

830

1

831

832

#[test]

833

1

fn eval_const_nested_ref() {

834

1

    let expr = Expression::Sum(

835

1

        Metadata::new(),

836

1

        vec![

837

1

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

838

1

            Expression::And(

839

1

                Metadata::new(),

840

1

                vec![

841

1

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

842

1

                    Expression::Atomic(

843

1

                        Metadata::new(),

844

1

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

845

1

),

846

1

],

847

1

),

848

1

],

849

1

);

850

1

    let result = eval_constant(&expr);

851

1

    assert_eq!(result, None);

852

1

853

854

#[test]

855

1

fn eval_const_eq_int() {

856

1

    let expr = Expression::Eq(

857

1

        Metadata::new(),

858

1

        Box::new(Expression::Atomic(

859

1

            Metadata::new(),

860

1

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

861

1

)),

862

1

        Box::new(Expression::Atomic(

863

1

            Metadata::new(),

864

1

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

865

1

)),

866

1

);

867

1

    let result = eval_constant(&expr);

868

1

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

869

1

870

871

#[test]

872

1

fn eval_const_eq_bool() {

873

1

    let expr = Expression::Eq(

874

1

        Metadata::new(),

875

1

        Box::new(Expression::Atomic(

876

1

            Metadata::new(),

877

1

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

878

1

)),

879

1

        Box::new(Expression::Atomic(

880

1

            Metadata::new(),

881

1

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

882

1

)),

883

1

);

884

1

    let result = eval_constant(&expr);

885

1

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

886

1

887

888

#[test]

889

1

fn eval_const_eq_mixed() {

890

1

    let expr = Expression::Eq(

891

1

        Metadata::new(),

892

1

        Box::new(Expression::Atomic(

893

1

            Metadata::new(),

894

1

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

895

1

)),

896

1

        Box::new(Expression::Atomic(

897

1

            Metadata::new(),

898

1

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

899

1

)),

900

1

);

901

1

    let result = eval_constant(&expr);

902

1

    assert_eq!(result, None);

903

1

904

905

#[test]

906

1

fn eval_const_sum_mixed() {

907

1

    let expr = Expression::Sum(

908

1

        Metadata::new(),

909

1

        vec![

910

1

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

911

1

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

912

1

],

913

1

);

914

1

    let result = eval_constant(&expr);

915

1

    assert_eq!(result, None);

916

1

917

918

#[test]

919

1

fn eval_const_sum_xyz() {

920

1

    let expr = Expression::And(

921

1

        Metadata::new(),

922

1

        vec![

923

1

            Expression::Eq(

924

1

                Metadata::new(),

925

1

                Box::new(Expression::Sum(

926

1

                    Metadata::new(),

927

1

                    vec![

928

1

                        Expression::Atomic(

929

1

                            Metadata::new(),

930

1

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

931

1

),

932

1

                        Expression::Atomic(

933

1

                            Metadata::new(),

934

1

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

935

1

),

936

1

                        Expression::Atomic(

937

1

                            Metadata::new(),

938

1

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

939

1

),

940

1

],

941

1

)),

942

1

                Box::new(Expression::Atomic(

943

1

                    Metadata::new(),

944

1

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

945

1

)),

946

1

),

947

1

            Expression::Geq(

948

1

                Metadata::new(),

949

1

                Box::new(Expression::Atomic(

950

1

                    Metadata::new(),

951

1

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

952

1

)),

953

1

                Box::new(Expression::Atomic(

954

1

                    Metadata::new(),

955

1

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

956

1

)),

957

1

),

958

1

],

959

1

);

960

1

    let result = eval_constant(&expr);

961

1

    assert_eq!(result, None);

962

1

963

964

#[test]

965

1

fn eval_const_or() {

966

1

    let expr = Expression::Or(

967

1

        Metadata::new(),

968

1

        vec![

969

1

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

970

1

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

971

1

],

972

1

);

973

1

    let result = eval_constant(&expr);

974

1

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

975

1