Grcov report - minion.rs

1

/************************************************************************/

2

/*        Rules for translating to Minion-supported constraints         */

3

/************************************************************************/

4

5

use std::collections::VecDeque;

6

use std::{collections::HashMap, convert::TryInto};

7

8

use crate::{

9

    extra_check,

10

    utils::{is_flat, to_aux_var},

11

};

12

use conjure_cp::ast::Moo;

13

use conjure_cp::ast::categories::Category;

14

use conjure_cp::{

15

    ast::Metadata,

16

    ast::{

17

        Atom, Expression as Expr, Literal as Lit, Range, Reference, ReturnType, SymbolTable,

18

        Typeable,

19

},

20

    into_matrix_expr, matrix_expr,

21

    rule_engine::{

22

        ApplicationError, ApplicationResult, Reduction, register_rule, register_rule_set,

23

},

24

    settings::SolverFamily,

25

};

26

27

use itertools::Itertools;

28

use uniplate::Uniplate;

29

30

use ApplicationError::RuleNotApplicable;

31

32

register_rule_set!("Minion", ("Base"), |f: &SolverFamily| {

33

982

    matches!(f, SolverFamily::Minion)

34

982

});

35

36

#[register_rule(("Minion", 4200))]

37

30152

fn introduce_producteq(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

38

    // product = val

39

    let val: Atom;

40

    let product: Moo<Expr>;

41

42

30152

    match expr.clone() {

43

1698

        Expr::Eq(_m, a, b) => {

44

1698

            let a_atom: Option<&Atom> = (&a).try_into().ok();

45

1698

            let b_atom: Option<&Atom> = (&b).try_into().ok();

46

47

1698

            if let Some(f) = a_atom {

48

                // val = product

49

1170

                val = f.clone();

50

1170

                product = b;

51

1170

            } else if let Some(f) = b_atom {

52

                // product = val

53

405

                val = f.clone();

54

405

                product = a;

55

405

            } else {

56

123

                return Err(RuleNotApplicable);

57

58

59

780

        Expr::AuxDeclaration(_m, reference, e) => {

60

780

            val = Atom::Reference(reference);

61

780

            product = e;

62

780

63

        _ => {

64

27674

            return Err(RuleNotApplicable);

65

66

67

68

2355

    if !(matches!(&*product, Expr::Product(_, _,))) {

69

2259

        return Err(RuleNotApplicable);

70

96

71

72

96

    let Expr::Product(_, factors) = &*product else {

73

        return Err(RuleNotApplicable);

74

};

75

76

96

    let mut factors_vec = (**factors).clone().unwrap_list().ok_or(RuleNotApplicable)?;

77

42

    if factors_vec.len() < 2 {

78

        return Err(RuleNotApplicable);

79

42

80

81

    // Product is a vecop, but FlatProductEq a binop.

82

    // Introduce auxvars until it is a binop

83

84

    // the expression returned will be x*y=val.

85

    // if factors is > 2 arguments, y will be an auxiliary variable

86

87

    #[allow(clippy::unwrap_used)] // should never panic - length is checked above

88

42

    let x: Atom = factors_vec

89

42

        .pop()

90

42

        .unwrap()

91

42

        .try_into()

92

42

        .or(Err(RuleNotApplicable))?;

93

94

    #[allow(clippy::unwrap_used)] // should never panic - length is checked above

95

33

    let mut y: Atom = factors_vec

96

33

        .pop()

97

33

        .unwrap()

98

33

        .try_into()

99

33

        .or(Err(RuleNotApplicable))?;

100

101

33

    let mut symbols = symbols.clone();

102

33

    let mut new_tops: Vec<Expr> = vec![];

103

104

    // FIXME: add a test for this

105

36

    while let Some(next_factor) = factors_vec.pop() {

106

        // Despite adding auxvars, I still require all atoms as factors, making this rule act

107

        // similar to other introduction rules.

108

3

        let next_factor_atom: Atom = next_factor.clone().try_into().or(Err(RuleNotApplicable))?;

109

110

        // TODO: find this domain without having to make unnecessary Expr and Metadata objects

111

        // Just using the domain of expr doesn't work

112

3

        let aux_domain = Expr::Product(

113

3

            Metadata::new(),

114

3

            Moo::new(matrix_expr![y.clone().into(), next_factor]),

115

3

116

3

        .domain_of()

117

3

        .ok_or(ApplicationError::DomainError)?;

118

119

3

        let aux_decl = symbols.gensym(&aux_domain);

120

3

        let aux_var = Atom::Reference(Reference::new(aux_decl));

121

122

3

        let new_top_expr = Expr::FlatProductEq(

123

3

            Metadata::new(),

124

3

            Moo::new(y),

125

3

            Moo::new(next_factor_atom),

126

3

            Moo::new(aux_var.clone()),

127

3

);

128

129

3

        new_tops.push(new_top_expr);

130

3

        y = aux_var;

131

132

133

33

    Ok(Reduction::new(

134

33

        Expr::FlatProductEq(Metadata::new(), Moo::new(x), Moo::new(y), Moo::new(val)),

135

33

        new_tops,

136

33

        symbols,

137

33

))

138

30152

139

140

/// Introduces `FlatWeightedSumLeq`, `FlatWeightedSumGeq`, `FlatSumLeq`, FlatSumGeq` constraints.

141

///

142

/// If the input is a weighted sum, the weighted sum constraints are used, otherwise the standard

143

/// sum constraints are used.

144

///

145

/// # Details

146

/// This rule is a bit unusual compared to other introduction rules in that

147

/// it does its own flattening.

148

///

149

/// Weighted sums are expressed as sums of products, which are not

150

/// flat. Flattening a weighted sum generically makes it indistinguishable

151

/// from a sum:

152

///

153

///```text

154

/// 1*a + 2*b + 3*c + d <= 10

155

///   ~~> flatten_vecop

156

/// __0 + __1 + __2 + d <= 10

157

///

158

///

159

/// __0 =aux 1*a

160

/// __1 =aux 2*b

161

/// __2 =aux 3*c

162

/// ```

163

///

164

/// Therefore, introduce_weightedsumleq_sumgeq does its own flattening.

165

///

166

/// Having custom flattening semantics means that we can make more things

167

/// weighted sums.

168

///

169

/// For example, consider `a + 2*b + 3*c*d + (e / f) + 5*(g/h) <= 18`. This

170

/// rule turns this into a single flat_weightedsumleq constraint:

171

///

172

///```text

173

/// a + 2*b + 3*c*d + (e/f) + 5*(g/h) <= 30

174

///

175

///   ~> introduce_weightedsumleq_sumgeq

176

///

177

/// flat_weightedsumleq([1,2,3,1,5],[a,b,__0,__1,__2],30)

178

///

179

/// with new top level constraints

180

///

181

/// __0 = c*d

182

/// __1 = e/f

183

/// __2 = g/h

184

/// ```

185

///

186

/// The rules to turn terms into coefficient variable pairs are the following:

187

///

188

/// 1. Non-weighted atom: `a ~> (1,a)`

189

/// 2. Other non-weighted term: `e ~> (1,__0)`, with new constraint `__0 =aux e`

190

/// 3. Weighted atom: `c*a ~> (c,a)`

191

/// 4. Weighted non-atom: `c*e ~> (c,__0)` with new constraint` __0 =aux e`

192

/// 5. Weighted product: `c*e*f ~> (c,__0)` with new constraint `__0 =aux (e*f)`

193

/// 6. Negated atom: `-x ~> (-1,x)`

194

/// 7. Negated expression: `-e ~> (-1,__0)` with new constraint `__0 = e`

195

///

196

/// Cases 6 and 7 could potentially be a normalising rule `-e ~> -1*e`. However, I think that we

197

/// should only turn negations into a product when they are inside a sum, not all the time.

198

#[register_rule(("Minion", 4600))]

199

49475

fn introduce_weighted_sumleq_sumgeq(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {

200

    // Keep track of which type of (in)equality was in the input, and use this to decide what

201

    // constraints to make at the end

202

203

    // We handle Eq directly in this rule instead of letting it be decomposed to <= and >=

204

    // elsewhere, as this caused cyclic rule application:

205

//

206

    // ```

207

    // 2*a + b = c

208

//

209

    //   ~~> sumeq_to_inequalities

210

//

211

    // 2*a + b <=c /\ 2*a + b >= c

212

//

213

    // --

214

//

215

    // 2*a + b <= c

216

//

217

    //   ~~> flatten_generic

218

    // __1 <=c

219

//

220

    // with new top level constraint

221

//

222

    // 2*a + b =aux __1

223

//

224

    // --

225

//

226

    // 2*a + b =aux __1

227

//

228

    //   ~~> sumeq_to_inequalities

229

//

230

    // LOOP!

231

    // ```

232

    enum EqualityKind {

233

Eq,

234

        Leq,

235

        Geq,

236

237

238

    // Given the LHS, RHS, and the type of inequality, return the sum, total, and new inequality.

239

//

240

    // The inequality returned is the one that puts the sum is on the left hand side and the total

241

    // on the right hand side.

242

//

243

    // For example, `1 <= a + b` will result in ([a,b],1,Geq).

244

4020

    fn match_sum_total(

245

4020

        a: Moo<Expr>,

246

4020

        b: Moo<Expr>,

247

4020

        equality_kind: EqualityKind,

248

4020

    ) -> Result<(Vec<Expr>, Atom, EqualityKind), ApplicationError> {

249

        match (

250

4020

            Moo::unwrap_or_clone(a),

251

4020

            Moo::unwrap_or_clone(b),

252

4020

            equality_kind,

253

) {

254

30

            (Expr::Sum(_, sum_terms), Expr::Atomic(_, total), EqualityKind::Leq) => {

255

30

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

256

30

                    .unwrap_list()

257

30

                    .ok_or(RuleNotApplicable)?;

258

3

                Ok((sum_terms, total, EqualityKind::Leq))

259

260

42

            (Expr::Atomic(_, total), Expr::Sum(_, sum_terms), EqualityKind::Leq) => {

261

42

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

262

42

                    .unwrap_list()

263

42

                    .ok_or(RuleNotApplicable)?;

264

18

                Ok((sum_terms, total, EqualityKind::Geq))

265

266

15

            (Expr::Sum(_, sum_terms), Expr::Atomic(_, total), EqualityKind::Geq) => {

267

15

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

268

15

                    .unwrap_list()

269

15

                    .ok_or(RuleNotApplicable)?;

270

9

                Ok((sum_terms, total, EqualityKind::Geq))

271

272

            (Expr::Atomic(_, total), Expr::Sum(_, sum_terms), EqualityKind::Geq) => {

273

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

274

                    .unwrap_list()

275

                    .ok_or(RuleNotApplicable)?;

276

                Ok((sum_terms, total, EqualityKind::Leq))

277

278

318

            (Expr::Sum(_, sum_terms), Expr::Atomic(_, total), EqualityKind::Eq) => {

279

318

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

280

318

                    .unwrap_list()

281

318

                    .ok_or(RuleNotApplicable)?;

282

99

                Ok((sum_terms, total, EqualityKind::Eq))

283

284

252

            (Expr::Atomic(_, total), Expr::Sum(_, sum_terms), EqualityKind::Eq) => {

285

252

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

286

252

                    .unwrap_list()

287

252

                    .ok_or(RuleNotApplicable)?;

288

114

                Ok((sum_terms, total, EqualityKind::Eq))

289

290

3363

            _ => Err(RuleNotApplicable),

291

292

4020

293

294

49475

    let (sum_exprs, total, equality_kind) = match expr.clone() {

295

648

        Expr::Leq(_, a, b) => Ok(match_sum_total(a, b, EqualityKind::Leq)?),

296

222

        Expr::Geq(_, a, b) => Ok(match_sum_total(a, b, EqualityKind::Geq)?),

297

3150

        Expr::Eq(_, a, b) => Ok(match_sum_total(a, b, EqualityKind::Eq)?),

298

1434

        Expr::AuxDeclaration(_, reference, a) => {

299

1434

            let total: Atom = Atom::Reference(reference);

300

1434

            if let Expr::Sum(_, sum_terms) = Moo::unwrap_or_clone(a) {

301

486

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

302

486

                    .unwrap_list()

303

486

                    .ok_or(RuleNotApplicable)?;

304

162

                Ok((sum_terms, total, EqualityKind::Eq))

305

            } else {

306

948

                Err(RuleNotApplicable)

307

308

309

44021

        _ => Err(RuleNotApplicable),

310

44969

}?;

311

312

405

    let mut new_top_exprs: Vec<Expr> = vec![];

313

405

    let mut symtab = symtab.clone();

314

315

    #[allow(clippy::mutable_key_type)]

316

405

    let mut coefficients_and_vars: HashMap<Atom, i32> = HashMap::new();

317

318

    // for each sub-term, get the coefficient and the variable, flattening if necessary.

319

//

320

915

    for expr in sum_exprs {

321

915

        let (coeff, var) = flatten_weighted_sum_term(expr, &mut symtab, &mut new_top_exprs)?;

322

323

840

        if coeff == 0 {

324

            continue;

325

840

326

327

        // collect coefficients for like terms, so 2*x + -1*x ~~> 1*x

328

840

        coefficients_and_vars

329

840

            .entry(var)

330

840

            .and_modify(|x| *x += coeff)

331

840

            .or_insert(coeff);

332

333

334

    // the expr should use a regular sum instead if the coefficients are all 1.

335

699

    let use_weighted_sum = !coefficients_and_vars.values().all(|x| *x == 1 || *x == 0);

336

337

    // This needs a consistent iteration order so that the output is deterministic. However,

338

    // HashMap doesn't provide this. Can't use BTreeMap or Ord to achieve this, as not everything

339

    // in the AST implements Ord. Instead, order things by their pretty printed value.

340

330

    let (vars, coefficients): (Vec<Atom>, Vec<Lit>) = coefficients_and_vars

341

330

        .into_iter()

342

777

        .filter(|(_, c)| *c != 0)

343

555

        .sorted_by(|a, b| {

344

555

            let a_atom_str = format!("{}", a.0);

345

555

            let b_atom_str = format!("{}", b.0);

346

555

            a_atom_str.cmp(&b_atom_str)

347

555

})

348

777

        .map(|(v, c)| (v, Lit::Int(c)))

349

330

        .unzip();

350

351

330

    let new_expr: Expr = match (equality_kind, use_weighted_sum) {

352

51

        (EqualityKind::Eq, true) => Expr::And(

353

51

            Metadata::new(),

354

51

            Moo::new(matrix_expr![

355

51

                Expr::FlatWeightedSumLeq(

356

51

                    Metadata::new(),

357

51

                    coefficients.clone(),

358

51

                    vars.clone(),

359

51

                    Moo::new(total.clone()),

360

51

),

361

51

                Expr::FlatWeightedSumGeq(Metadata::new(), coefficients, vars, Moo::new(total)),

362

51

]),

363

51

),

364

252

        (EqualityKind::Eq, false) => Expr::And(

365

252

            Metadata::new(),

366

252

            Moo::new(matrix_expr![

367

252

                Expr::FlatSumLeq(Metadata::new(), vars.clone(), total.clone()),

368

252

                Expr::FlatSumGeq(Metadata::new(), vars, total),

369

252

]),

370

252

),

371

        (EqualityKind::Leq, true) => {

372

            Expr::FlatWeightedSumLeq(Metadata::new(), coefficients, vars, Moo::new(total))

373

374

3

        (EqualityKind::Leq, false) => Expr::FlatSumLeq(Metadata::new(), vars, total),

375

        (EqualityKind::Geq, true) => {

376

            Expr::FlatWeightedSumGeq(Metadata::new(), coefficients, vars, Moo::new(total))

377

378

24

        (EqualityKind::Geq, false) => Expr::FlatSumGeq(Metadata::new(), vars, total),

379

};

380

381

330

    Ok(Reduction::new(new_expr, new_top_exprs, symtab))

382

49475

383

384

/// For a term inside a weighted sum, return coefficient*variable.

385

///

386

///

387

/// If the term is in the form <coefficient> * <non flat expression>, the expression is flattened

388

/// to a new auxvar, which is returned as the variable for this term.

389

///

390

/// New auxvars are added to `symtab`, and their top level constraints to `top_level_exprs`.

391

///

392

/// # Errors

393

///

394

/// + Returns [`ApplicationError::RuleNotApplicable`] if a non-flat expression cannot be turned

395

///   into an atom. See [`flatten_expression_to_atom`].

396

///

397

/// + Returns [`ApplicationError::RuleNotApplicable`] if the term is a product containing a matrix

398

///   literal, and that matrix literal is not a list.

399

///

400

///

401

915

fn flatten_weighted_sum_term(

402

915

    term: Expr,

403

915

    symtab: &mut SymbolTable,

404

915

    top_level_exprs: &mut Vec<Expr>,

405

915

) -> Result<(i32, Atom), ApplicationError> {

406

174

    match term {

407

        // we can only see check the product for coefficients it contains a matrix literal.

408

//

409

        // e.g. the input expression `product([2,x])` returns (2,x), but `product(my_matrix)`

410

        // returns (1,product(my_matrix)).

411

//

412

        // if the product contains a matrix literal but it is not a list, throw `RuleNotApplicable`

413

        // to allow it to be changed into a list by another rule.

414

174

        Expr::Product(_, factors) if factors.is_matrix_literal() => {

415

            // this fails if factors is not a matrix literal or that matrix literal is not a list.

416

//

417

            // we already check for the first case above, so this should only error when we have a

418

            // non-list matrix literal.

419

174

            let factors = Moo::unwrap_or_clone(factors)

420

174

                .unwrap_list()

421

174

                .ok_or(RuleNotApplicable)?;

422

423

126

            match factors.as_slice() {

424

                // product([]) ~~> (0,0)

425

                // coefficients of 0 should be ignored by the caller.

426

126

                [] => Ok((0, Atom::Literal(Lit::Int(0)))),

427

428

                // product([4,y]) ~~> (4,y)

429

108

                [Expr::Atomic(_, Atom::Literal(Lit::Int(coeff))), e] => Ok((

430

108

                    *coeff,

431

108

                    flatten_expression_to_atom(e.clone(), symtab, top_level_exprs)?,

432

)),

433

434

                // product([y,4]) ~~> (y,4)

435

                [e, Expr::Atomic(_, Atom::Literal(Lit::Int(coeff)))] => Ok((

436

                    *coeff,

437

                    flatten_expression_to_atom(e.clone(), symtab, top_level_exprs)?,

438

)),

439

440

                // assume the coefficients have been placed at the front by normalisation rules

441

442

                // product[1,x,y,...] ~> return (coeff,product([x,y,...]))

443

444

6

                    Expr::Atomic(_, Atom::Literal(Lit::Int(coeff))),

445

6

e,

446

6

                    rest @ ..,

447

                ] => {

448

6

                    let mut product_terms = Vec::from(rest);

449

6

                    product_terms.push(e.clone());

450

6

                    let product =

451

6

                        Expr::Product(Metadata::new(), Moo::new(into_matrix_expr!(product_terms)));

452

                    Ok((

453

6

                        *coeff,

454

6

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

455

))

456

457

458

                // no coefficient:

459

                // product([x,y,z]) ~~> (1,product([x,y,z])

460

                _ => {

461

12

                    let product =

462

12

                        Expr::Product(Metadata::new(), Moo::new(into_matrix_expr!(factors)));

463

                    Ok((

464

1,

465

12

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

466

))

467

468

469

470

42

        Expr::Neg(_, inner_term) => Ok((

471

-1,

472

42

            flatten_expression_to_atom(Moo::unwrap_or_clone(inner_term), symtab, top_level_exprs)?,

473

)),

474

699

        term => Ok((

475

1,

476

699

            flatten_expression_to_atom(term, symtab, top_level_exprs)?,

477

)),

478

479

915

480

481

/// Converts the input expression to an atom, placing it into a new auxiliary variable if

482

/// necessary.

483

///

484

/// The auxiliary variable will be added to the symbol table and its top-level-constraint to

485

/// `top_level_exprs`.

486

///

487

/// If the expression is already atomic, no auxiliary variables are created, and the atom is

488

/// returned as-is.

489

///

490

/// # Errors

491

///

492

///  + Returns [`ApplicationError::RuleNotApplicable`] if the expression cannot be placed into an

493

///    auxiliary variable. For example, expressions that do not have domains.

494

///

495

///    This function supports the same expressions as [`to_aux_var`], except that this functions

496

///    succeeds when the expression given is atomic.

497

///

498

///    See [`to_aux_var`] for more information.

499

///

500

1059

fn flatten_expression_to_atom(

501

1059

    expr: Expr,

502

1059

    symtab: &mut SymbolTable,

503

1059

    top_level_exprs: &mut Vec<Expr>,

504

1059

) -> Result<Atom, ApplicationError> {

505

1059

    if let Expr::Atomic(_, atom) = expr {

506

909

        return Ok(atom);

507

150

508

509

150

    let aux_var_info = to_aux_var(&expr, symtab).ok_or(RuleNotApplicable)?;

510

72

    *symtab = aux_var_info.symbols();

511

72

    top_level_exprs.push(aux_var_info.top_level_expr());

512

513

72

    Ok(aux_var_info.as_atom())

514

1059

515

516

#[register_rule(("Minion", 4200))]

517

30152

fn introduce_diveq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

518

    // div = val

519

    let val: Atom;

520

    let div: Moo<Expr>;

521

    let meta: Metadata;

522

523

30152

    match expr.clone() {

524

1698

        Expr::Eq(m, a, b) => {

525

1698

            meta = m;

526

527

1698

            let a_atom: Option<&Atom> = (&a).try_into().ok();

528

1698

            let b_atom: Option<&Atom> = (&b).try_into().ok();

529

530

1698

            if let Some(f) = a_atom {

531

                // val = div

532

1170

                val = f.clone();

533

1170

                div = b;

534

1170

            } else if let Some(f) = b_atom {

535

                // div = val

536

405

                val = f.clone();

537

405

                div = a;

538

405

            } else {

539

123

                return Err(RuleNotApplicable);

540

541

542

780

        Expr::AuxDeclaration(m, reference, e) => {

543

780

            meta = m;

544

780

            val = Atom::Reference(reference);

545

780

            div = e;

546

780

547

        _ => {

548

27674

            return Err(RuleNotApplicable);

549

550

551

552

2355

    if !(matches!(&*div, Expr::SafeDiv(_, _, _))) {

553

2238

        return Err(RuleNotApplicable);

554

117

555

556

117

    let children: VecDeque<Expr> = div.as_ref().children();

557

117

    let a: &Atom = (&children[0]).try_into().or(Err(RuleNotApplicable))?;

558

108

    let b: &Atom = (&children[1]).try_into().or(Err(RuleNotApplicable))?;

559

560

99

    Ok(Reduction::pure(Expr::MinionDivEqUndefZero(

561

99

        meta.clone_dirty(),

562

99

        Moo::new(a.clone()),

563

99

        Moo::new(b.clone()),

564

99

        Moo::new(val),

565

99

)))

566

30152

567

568

#[register_rule(("Minion", 4200))]

569

30152

fn introduce_modeq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

570

    // div = val

571

    let val: Atom;

572

    let div: Moo<Expr>;

573

    let meta: Metadata;

574

575

30152

    match expr.clone() {

576

1698

        Expr::Eq(m, a, b) => {

577

1698

            meta = m;

578

1698

            let a_atom: Option<&Atom> = (&a).try_into().ok();

579

1698

            let b_atom: Option<&Atom> = (&b).try_into().ok();

580

581

1698

            if let Some(f) = a_atom {

582

                // val = div

583

1170

                val = f.clone();

584

1170

                div = b;

585

1170

            } else if let Some(f) = b_atom {

586

                // div = val

587

405

                val = f.clone();

588

405

                div = a;

589

405

            } else {

590

123

                return Err(RuleNotApplicable);

591

592

593

780

        Expr::AuxDeclaration(m, reference, e) => {

594

780

            meta = m;

595

780

            val = Atom::Reference(reference);

596

780

            div = e;

597

780

598

        _ => {

599

27674

            return Err(RuleNotApplicable);

600

601

602

603

2355

    if !(matches!(&*div, Expr::SafeMod(_, _, _))) {

604

2295

        return Err(RuleNotApplicable);

605

60

606

607

60

    let children: VecDeque<Expr> = div.as_ref().children();

608

60

    let a: &Atom = (&children[0]).try_into().or(Err(RuleNotApplicable))?;

609

60

    let b: &Atom = (&children[1]).try_into().or(Err(RuleNotApplicable))?;

610

611

51

    Ok(Reduction::pure(Expr::MinionModuloEqUndefZero(

612

51

        meta.clone_dirty(),

613

51

        Moo::new(a.clone()),

614

51

        Moo::new(b.clone()),

615

51

        Moo::new(val),

616

51

)))

617

30152

618

619

#[register_rule(("Minion", 4400))]

620

40607

fn introduce_abseq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

621

40607

    let (x, abs_y): (Atom, Expr) = match expr.clone() {

622

2397

        Expr::Eq(_, a, b) => {

623

2397

            let a: Expr = Moo::unwrap_or_clone(a);

624

2397

            let b: Expr = Moo::unwrap_or_clone(b);

625

2397

            let a_atom: Option<&Atom> = (&a).try_into().ok();

626

2397

            let b_atom: Option<&Atom> = (&b).try_into().ok();

627

628

2397

            if let Some(a_atom) = a_atom {

629

1674

                Ok((a_atom.clone(), b))

630

723

            } else if let Some(b_atom) = b_atom {

631

594

                Ok((b_atom.clone(), a))

632

            } else {

633

129

                Err(RuleNotApplicable)

634

635

636

637

1131

        Expr::AuxDeclaration(_, reference, expr) => {

638

1131

            let a = Atom::Reference(reference);

639

1131

            let expr = Moo::unwrap_or_clone(expr);

640

1131

            Ok((a, expr))

641

642

643

37079

        _ => Err(RuleNotApplicable),

644

37208

}?;

645

646

3399

    let Expr::Abs(_, y) = abs_y else {

647

3369

        return Err(RuleNotApplicable);

648

};

649

650

30

    let y = Moo::unwrap_or_clone(y);

651

30

    let y: Atom = y.try_into().or(Err(RuleNotApplicable))?;

652

653

30

    Ok(Reduction::pure(Expr::FlatAbsEq(

654

30

        Metadata::new(),

655

30

        Moo::new(x),

656

30

        Moo::new(y),

657

30

)))

658

40607

659

660

/// Introduces a `MinionPowEq` constraint from a `SafePow`

661

#[register_rule(("Minion", 4200))]

662

30152

fn introduce_poweq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

663

30152

    let (a, b, total) = match expr.clone() {

664

1698

        Expr::Eq(_, e1, e2) => match (Moo::unwrap_or_clone(e1), Moo::unwrap_or_clone(e2)) {

665

            (Expr::Atomic(_, total), Expr::SafePow(_, a, b)) => Ok((a, b, total)),

666

21

            (Expr::SafePow(_, a, b), Expr::Atomic(_, total)) => Ok((a, b, total)),

667

1677

            _ => Err(RuleNotApplicable),

668

},

669

670

780

        Expr::AuxDeclaration(_, total_reference, e) => match Moo::unwrap_or_clone(e) {

671

30

            Expr::SafePow(_, a, b) => {

672

30

                let total_ref_atom = Atom::Reference(total_reference);

673

30

                Ok((a, b, total_ref_atom))

674

675

750

            _ => Err(RuleNotApplicable),

676

},

677

27674

        _ => Err(RuleNotApplicable),

678

30101

}?;

679

680

51

    let a: Atom = Moo::unwrap_or_clone(a)

681

51

        .try_into()

682

51

        .or(Err(RuleNotApplicable))?;

683

48

    let b: Atom = Moo::unwrap_or_clone(b)

684

48

        .try_into()

685

48

        .or(Err(RuleNotApplicable))?;

686

687

48

    Ok(Reduction::pure(Expr::MinionPow(

688

48

        Metadata::new(),

689

48

        Moo::new(a),

690

48

        Moo::new(b),

691

48

        Moo::new(total),

692

48

)))

693

30152

694

695

/// Introduces a `FlatAlldiff` constraint from an `AllDiff`

696

#[register_rule(("Minion", 4200))]

697

30152

fn introduce_flat_alldiff(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

698

30152

    let Expr::AllDiff(_, es) = expr else {

699

29879

        return Err(RuleNotApplicable);

700

};

701

702

273

    let es = (**es).clone().unwrap_list().ok_or(RuleNotApplicable)?;

703

704

72

    let atoms = es

705

72

        .into_iter()

706

267

        .map(|e| match e {

707

261

            Expr::Atomic(_, atom) => Ok(atom),

708

6

            _ => Err(RuleNotApplicable),

709

267

})

710

72

        .process_results(|iter| iter.collect_vec())?;

711

712

66

    Ok(Reduction::pure(Expr::FlatAllDiff(Metadata::new(), atoms)))

713

30152

714

715

/// Introduces a Minion `MinusEq` constraint from `x = -y`, where x and y are atoms.

716

///

717

/// ```text

718

/// x = -y ~> MinusEq(x,y)

719

///

720

///   where x,y are atoms

721

/// ```

722

#[register_rule(("Minion", 4400))]

723

40607

fn introduce_minuseq_from_eq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

724

40607

    let Expr::Eq(_, a, b) = expr else {

725

38210

        return Err(RuleNotApplicable);

726

};

727

728

4785

    fn try_get_atoms(a: &Moo<Expr>, b: &Moo<Expr>) -> Option<(Atom, Atom)> {

729

4785

        let a: &Atom = (&**a).try_into().ok()?;

730

3708

        let Expr::Neg(_, b) = &**b else {

731

3651

            return None;

732

};

733

734

57

        let b: &Atom = b.try_into().ok()?;

735

736

24

        Some((a.clone(), b.clone()))

737

4785

738

739

    // x = - y. Find this symmetrically (a = - b or b = -a)

740

2397

    let Some((x, y)) = try_get_atoms(a, b).or_else(|| try_get_atoms(b, a)) else {

741

2373

        return Err(RuleNotApplicable);

742

};

743

744

24

    Ok(Reduction::pure(Expr::FlatMinusEq(

745

24

        Metadata::new(),

746

24

        Moo::new(x),

747

24

        Moo::new(y),

748

24

)))

749

40607

750

751

/// Introduces a Minion `MinusEq` constraint from `x =aux -y`, where x and y are atoms.

752

///

753

/// ```text

754

/// x =aux -y ~> MinusEq(x,y)

755

///

756

///   where x,y are atoms

757

/// ```

758

#[register_rule(("Minion", 4400))]

759

40607

fn introduce_minuseq_from_aux_decl(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

760

    // a =aux -b

761

//

762

40607

    let Expr::AuxDeclaration(_, reference, b) = expr else {

763

39476

        return Err(RuleNotApplicable);

764

};

765

766

1131

    let a = Atom::Reference(reference.clone());

767

768

1131

    let Expr::Neg(_, b) = (**b).clone() else {

769

1119

        return Err(RuleNotApplicable);

770

};

771

772

12

    let Ok(b) = b.try_into() else {

773

6

        return Err(RuleNotApplicable);

774

};

775

776

6

    Ok(Reduction::pure(Expr::FlatMinusEq(

777

6

        Metadata::new(),

778

6

        Moo::new(a),

779

6

        Moo::new(b),

780

6

)))

781

40607

782

783

/// Converts an implication to either `ineq` or `reifyimply`

784

///

785

/// ```text

786

/// x -> y ~> ineq(x,y,0)

787

/// where x is atomic, y is atomic

788

///

789

/// x -> y ~> reifyimply(y,x)

790

/// where x is atomic, y is non-atomic

791

/// ```

792

#[register_rule(("Minion", 4400))]

793

40607

fn introduce_reifyimply_ineq_from_imply(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

794

40607

    let Expr::Imply(_, x, y) = expr else {

795

40364

        return Err(RuleNotApplicable);

796

};

797

798

243

    let x_atom: &Atom = x.as_ref().try_into().or(Err(RuleNotApplicable))?;

799

800

    // if both x and y are atoms,  x -> y ~> ineq(x,y,0)

801

//

802

    // if only x is an atom, x -> y ~> reifyimply(y,x)

803

81

    if let Ok(y_atom) = TryInto::<&Atom>::try_into(y.as_ref()) {

804

45

        Ok(Reduction::pure(Expr::FlatIneq(

805

45

            Metadata::new(),

806

45

            Moo::new(x_atom.clone()),

807

45

            Moo::new(y_atom.clone()),

808

45

            Box::new(0.into()),

809

45

)))

810

    } else {

811

36

        Ok(Reduction::pure(Expr::MinionReifyImply(

812

36

            Metadata::new(),

813

36

            y.clone(),

814

36

            x_atom.clone(),

815

36

)))

816

817

40607

818

819

/// Converts `__inDomain(a,domain) to w-inintervalset.

820

///

821

/// This applies if domain is integer and finite.

822

#[register_rule(("Minion", 4400))]

823

40607

fn introduce_wininterval_set_from_indomain(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

824

40607

    let Expr::InDomain(_, e, domain) = expr else {

825

40544

        return Err(RuleNotApplicable);

826

};

827

828

63

    let Expr::Atomic(_, atom @ Atom::Reference(_)) = e.as_ref() else {

829

51

        return Err(RuleNotApplicable);

830

};

831

832

12

    let Some(ranges) = domain.as_int_ground() else {

833

        return Err(RuleNotApplicable);

834

};

835

836

12

    let mut out_ranges = vec![];

837

838

12

    for range in ranges {

839

12

        match range {

840

            Range::Single(x) => {

841

                out_ranges.push(*x);

842

                out_ranges.push(*x);

843

844

12

            Range::Bounded(x, y) => {

845

12

                out_ranges.push(*x);

846

12

                out_ranges.push(*y);

847

12

848

            Range::UnboundedR(_) | Range::UnboundedL(_) | Range::Unbounded => {

849

                return Err(RuleNotApplicable);

850

851

852

853

854

12

    Ok(Reduction::pure(Expr::MinionWInIntervalSet(

855

12

        Metadata::new(),

856

12

        atom.clone(),

857

12

        out_ranges,

858

12

)))

859

40607

860

861

/// Converts `[....][i]` to `element_one` if:

862

///

863

/// 1. the subject is a list literal

864

/// 2. the subject is one dimensional

865

#[register_rule(("Minion", 4400))]

866

40607

fn introduce_element_from_index(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

867

40607

    let (equalto, subject, indices) = match expr.clone() {

868

2397

        Expr::Eq(_, e1, e2) => match (Moo::unwrap_or_clone(e1), Moo::unwrap_or_clone(e2)) {

869

12

            (Expr::Atomic(_, eq), Expr::SafeIndex(_, subject, indices)) => {

870

12

                Ok((eq, subject, indices))

871

872

207

            (Expr::SafeIndex(_, subject, indices), Expr::Atomic(_, eq)) => {

873

207

                Ok((eq, subject, indices))

874

875

2178

            _ => Err(RuleNotApplicable),

876

},

877

1131

        Expr::AuxDeclaration(_, reference, expr) => match Moo::unwrap_or_clone(expr) {

878

30

            Expr::SafeIndex(_, subject, indices) => {

879

30

                Ok((Atom::Reference(reference), subject, indices))

880

881

1101

            _ => Err(RuleNotApplicable),

882

},

883

37079

        _ => Err(RuleNotApplicable),

884

40358

}?;

885

886

249

    if indices.len() != 1 {

887

12

        return Err(RuleNotApplicable);

888

237

889

890

237

    let Some(list) = Moo::unwrap_or_clone(subject).unwrap_list() else {

891

81

        return Err(RuleNotApplicable);

892

};

893

894

156

    let Expr::Atomic(_, index) = indices[0].clone() else {

895

54

        return Err(RuleNotApplicable);

896

};

897

898

102

    let mut atom_list = vec![];

899

900

285

    for elem in list {

901

285

        let Expr::Atomic(_, elem) = elem else {

902

42

            return Err(RuleNotApplicable);

903

};

904

905

243

        atom_list.push(elem);

906

907

908

60

    Ok(Reduction::pure(Expr::MinionElementOne(

909

60

        Metadata::new(),

910

60

        atom_list,

911

60

        Moo::new(index),

912

60

        Moo::new(equalto),

913

60

)))

914

40607

915

916

/// Flattens an implication.

917

///

918

/// ```text

919

/// e -> y  (where e is non atomic)

920

///  ~~>

921

/// __0 -> y,

922

///

923

/// with new top level constraints

924

/// __0 =aux x

925

///

926

/// ```

927

///

928

/// Unlike other expressions, only the left hand side of implications are flattened. This is

929

/// because implications can be expressed as a `reifyimply` constraint, which takes a constraint as

930

/// an argument:

931

///

932

/// ``` text

933

/// r -> c ~> refifyimply(r,c)

934

///  where r is an atom, c is a constraint

935

/// ```

936

///

937

/// See [`introduce_reifyimply_ineq_from_imply`].

938

#[register_rule(("Minion", 4200))]

939

30152

fn flatten_imply(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

940

30152

    let Expr::Imply(meta, x, y) = expr else {

941

30059

        return Err(RuleNotApplicable);

942

};

943

944

    // flatten x

945

93

    let aux_var_info = to_aux_var(x.as_ref(), symbols).ok_or(RuleNotApplicable)?;

946

947

48

    let symbols = aux_var_info.symbols();

948

48

    let new_x = aux_var_info.as_expr();

949

950

48

    Ok(Reduction::new(

951

48

        Expr::Imply(meta.clone(), Moo::new(new_x), y.clone()),

952

48

        vec![aux_var_info.top_level_expr()],

953

48

        symbols,

954

48

))

955

30152

956

957

#[register_rule(("Minion", 4200))]

958

30152

fn flatten_generic(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

959

27386

    if !matches!(

960

30152

        expr,

961

        Expr::SafeDiv(_, _, _)

962

            | Expr::Neq(_, _, _)

963

            | Expr::SafeMod(_, _, _)

964

            | Expr::SafePow(_, _, _)

965

            | Expr::Leq(_, _, _)

966

            | Expr::Geq(_, _, _)

967

            | Expr::Abs(_, _)

968

            | Expr::Neg(_, _)

969

            | Expr::Not(_, _)

970

            | Expr::SafeIndex(_, _, _)

971

            | Expr::InDomain(_, _, _)

972

            | Expr::ToInt(_, _)

973

) {

974

27386

        return Err(RuleNotApplicable);

975

2766

976

977

2766

    let mut children = expr.children();

978

979

2766

    let mut symbols = symbols.clone();

980

2766

    let mut num_changed = 0;

981

2766

    let mut new_tops: Vec<Expr> = vec![];

982

983

5406

    for child in children.iter_mut() {

984

5406

        if let Some(aux_var_info) = to_aux_var(child, &symbols) {

985

300

            symbols = aux_var_info.symbols();

986

300

            new_tops.push(aux_var_info.top_level_expr());

987

300

            *child = aux_var_info.as_expr();

988

300

            num_changed += 1;

989

5106

990

991

992

2766

    if num_changed == 0 {

993

2469

        return Err(RuleNotApplicable);

994

297

995

996

297

    let expr = expr.with_children(children);

997

998

297

    Ok(Reduction::new(expr, new_tops, symbols))

999

30152

1000

1001

#[register_rule(("Minion", 4200))]

1002

30152

fn flatten_eq(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

1003

30152

    if !matches!(expr, Expr::Eq(_, _, _)) {

1004

28454

        return Err(RuleNotApplicable);

1005

1698

1006

1007

1698

    let children = expr.children();

1008

1698

    debug_assert_eq!(children.len(), 2);

1009

1010

1698

    let mut new_children = VecDeque::new();

1011

1698

    let mut symbols = symbols.clone();

1012

1698

    let mut num_changed = 0;

1013

1698

    let mut new_tops: Vec<Expr> = vec![];

1014

1015

3396

    for child in children {

1016

3396

        if let Some(aux_var_info) = to_aux_var(&child, &symbols) {

1017

354

            symbols = aux_var_info.symbols();

1018

354

            new_tops.push(aux_var_info.top_level_expr());

1019

354

            new_children.push_back(aux_var_info.as_expr());

1020

354

            num_changed += 1;

1021

3042

1022

1023

1024

    // eq: both sides have to be non flat for the rule to be applicable!

1025

1698

    if num_changed != 2 {

1026

1692

        return Err(RuleNotApplicable);

1027

6

1028

1029

6

    let expr = expr.with_children(new_children);

1030

1031

6

    Ok(Reduction::new(expr, new_tops, symbols))

1032

30152

1033

1034

/// Flattens products containing lists.

1035

///

1036

/// For example,

1037

///

1038

/// ```plain

1039

/// product([|x|,y,z]) ~~> product([aux1,y,z]), aux1=|x|

1040

/// ```

1041

#[register_rule(("Minion", 4200))]

1042

30152

fn flatten_product(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {

1043

    // product cannot use flatten_generic as we don't want to put the immediate child in an aux

1044

    // var, as that is the matrix literal. Instead we want to put the children of the matrix

1045

    // literal in an aux var.

1046

//

1047

    // e.g.

1048

//

1049

    // flatten_generic would do

1050

//

1051

    // product([|x|,y,z]) ~~> product(aux1), aux1=[x,y,z]

1052

//

1053

    // we want to do

1054

//

1055

    // product([|x|,y,z]) ~~> product([aux1,y,z]), aux1=|x|

1056

//

1057

    // We only want to flatten products containing matrix literals that are lists but not child terms, e.g.

1058

//

1059

    //  product(x[1,..]) ~~> product(aux1),aux1 = x[1,..].

1060

//

1061

    //  Instead, we let the representation and vertical rules for matrices turn x[1,..] into a

1062

    //  matrix literal.

1063

//

1064

    //  product(x[1,..]) ~~ slice_matrix_to_atom ~~> product([x11,x12,x13,x14])

1065

1066

30152

    let Expr::Product(_, factors) = expr else {

1067

29759

        return Err(RuleNotApplicable);

1068

};

1069

1070

393

    let factors = (**factors).clone().unwrap_list().ok_or(RuleNotApplicable)?;

1071

1072

117

    let mut new_factors = vec![];

1073

117

    let mut top_level_exprs = vec![];

1074

117

    let mut symtab = symtab.clone();

1075

1076

192

    for factor in factors {

1077

192

        new_factors.push(Expr::Atomic(

1078

192

            Metadata::new(),

1079

192

            flatten_expression_to_atom(factor, &mut symtab, &mut top_level_exprs)?,

1080

));

1081

1082

1083

    // have we done anything?

1084

    // if we have created any aux-vars, they will have added a top_level_declaration.

1085

66

    if top_level_exprs.is_empty() {

1086

63

        return Err(RuleNotApplicable);

1087

3

1088

1089

3

    let new_expr = Expr::Product(Metadata::new(), Moo::new(into_matrix_expr![new_factors]));

1090

3

    Ok(Reduction::new(new_expr, top_level_exprs, symtab))

1091

30152

1092

1093

/// Flattens a matrix literal that contains expressions.

1094

///

1095

/// For example,

1096

///

1097

/// ```plain

1098

/// [1,e/2,f*5] ~~> [1,__0,__1],

1099

///

1100

/// where

1101

/// __0 =aux e/2,

1102

/// __1 =aux f*5

1103

/// ```

1104

#[register_rule(("Minion", 1000))] // this should be a lower priority than matrix to list

1105

7346

fn flatten_matrix_literal(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {

1106

    // do not flatten matrix literals inside sum, or, and, product as these expressions either do

1107

    // their own flattening, or do not need flat expressions.

1108

7001

    if matches!(

1109

7346

        expr,

1110

        Expr::And(_, _) | Expr::Or(_, _) | Expr::Sum(_, _) | Expr::Product(_, _)

1111

) {

1112

345

        return Err(RuleNotApplicable);

1113

7001

1114

1115

    // flatten any children that are matrix literals

1116

7001

    let mut children = expr.children();

1117

1118

7001

    let mut has_changed = false;

1119

7001

    let mut symbols = symtab.clone();

1120

7001

    let mut top_level_exprs = vec![];

1121

1122

7001

    for child in children.iter_mut() {

1123

        // is this a matrix literal?

1124

//

1125

        // as we arn't changing the number of arguments in the matrix, we can apply this to all

1126

        // matrices, not just those that are lists.

1127

//

1128

        // this also means that this rule works with n-d matrices -- the inner dimensions of n-d

1129

        // matrices cant be turned into lists, as described the docstring for matrix_to_list.

1130

6040

        let Some((mut es, index_domain)) = child.clone().unwrap_matrix_unchecked() else {

1131

6016

            continue;

1132

};

1133

1134

        // flatten expressions

1135

105

        for e in es.iter_mut() {

1136

105

            if let Some(aux_info) = to_aux_var(e, &symbols) {

1137

15

                *e = aux_info.as_expr();

1138

15

                top_level_exprs.push(aux_info.top_level_expr());

1139

15

                symbols = aux_info.symbols();

1140

15

                has_changed = true;

1141

90

            } else if let Expr::SafeIndex(_, subject, _) = e

1142

18

                && !matches!(**subject, Expr::Atomic(_, Atom::Reference(_)))

1143

1144

                // we dont normally flatten indexing expressions, but we want to do it if they are

1145

                // inside a matrix list.

1146

//

1147

                // remove_dimension_from_matrix_indexing turns [[1,2,3],[4,5,6]][i,j]

1148

                // into [[1,2,3][j],[4,5,6][j],[7,8,9][j]][i].

1149

//

1150

                // we want to flatten this to

1151

                // [__0,__1,__2][i]

1152

1153

18

                let Some(domain) = e.domain_of() else {

1154

                    continue;

1155

};

1156

1157

18

                let categories = e.universe_categories();

1158

1159

                // must contain a decision variable

1160

18

                if !categories.contains(&Category::Decision) {

1161

                    continue;

1162

18

1163

1164

                // must not contain givens or quantified variables

1165

18

                if categories.contains(&Category::Parameter)

1166

18

                    || categories.contains(&Category::Quantified)

1167

1168

                    continue;

1169

18

1170

1171

18

                let decl = symbols.gensym(&domain);

1172

1173

18

                top_level_exprs.push(Expr::AuxDeclaration(

1174

18

                    Metadata::new(),

1175

18

                    Reference::new(decl.clone()),

1176

18

                    Moo::new(e.clone()),

1177

18

));

1178

1179

18

                *e = Expr::Atomic(Metadata::new(), Atom::Reference(Reference::new(decl)));

1180

1181

18

                has_changed = true;

1182

72

1183

1184

1185

24

        *child = into_matrix_expr!(es;index_domain);

1186

1187

1188

7001

    if has_changed {

1189

18

        Ok(Reduction::new(

1190

18

            expr.with_children(children),

1191

18

            top_level_exprs,

1192

18

            symbols,

1193

18

))

1194

    } else {

1195

6983

        Err(RuleNotApplicable)

1196

1197

7346

1198

1199

/// Converts a Geq to an Ineq

1200

///

1201

/// ```text

1202

/// x >= y ~> y <= x + 0 ~> ineq(y,x,0)

1203

/// ```

1204

#[register_rule(("Minion", 4100))]

1205

22469

fn geq_to_ineq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1206

22469

    let Expr::Geq(meta, e1, e2) = expr.clone() else {

1207

22373

        return Err(RuleNotApplicable);

1208

};

1209

1210

96

    let Expr::Atomic(_, x) = Moo::unwrap_or_clone(e1) else {

1211

6

        return Err(RuleNotApplicable);

1212

};

1213

1214

90

    let Expr::Atomic(_, y) = Moo::unwrap_or_clone(e2) else {

1215

        return Err(RuleNotApplicable);

1216

};

1217

1218

90

    Ok(Reduction::pure(Expr::FlatIneq(

1219

90

        meta.clone_dirty(),

1220

90

        Moo::new(y),

1221

90

        Moo::new(x),

1222

90

        Box::new(Lit::Int(0)),

1223

90

)))

1224

22469

1225

1226

/// Converts a Leq to an Ineq

1227

///

1228

/// ```text

1229

/// x <= y ~> x <= y + 0 ~> ineq(x,y,0)

1230

/// ```

1231

#[register_rule(("Minion", 4100))]

1232

22469

fn leq_to_ineq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1233

22469

    let Expr::Leq(meta, e1, e2) = expr.clone() else {

1234

22247

        return Err(RuleNotApplicable);

1235

};

1236

1237

222

    let Expr::Atomic(_, x) = Moo::unwrap_or_clone(e1) else {

1238

3

        return Err(RuleNotApplicable);

1239

};

1240

1241

219

    let Expr::Atomic(_, y) = Moo::unwrap_or_clone(e2) else {

1242

        return Err(RuleNotApplicable);

1243

};

1244

1245

219

    Ok(Reduction::pure(Expr::FlatIneq(

1246

219

        meta.clone_dirty(),

1247

219

        Moo::new(x),

1248

219

        Moo::new(y),

1249

219

        Box::new(Lit::Int(0)),

1250

219

)))

1251

22469

1252

1253

// TODO: add this rule for geq

1254

1255

/// ```text

1256

/// x <= y + k ~> ineq(x,y,k)

1257

/// ```

1258

#[register_rule(("Minion",4500))]

1259

44795

fn x_leq_y_plus_k_to_ineq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1260

44795

    let Expr::Leq(meta, e1, e2) = expr.clone() else {

1261

44168

        return Err(RuleNotApplicable);

1262

};

1263

1264

627

    let Expr::Atomic(_, x) = Moo::unwrap_or_clone(e1) else {

1265

51

        return Err(RuleNotApplicable);

1266

};

1267

1268

576

    let Expr::Sum(_, sum_exprs) = Moo::unwrap_or_clone(e2) else {

1269

549

        return Err(RuleNotApplicable);

1270

};

1271

1272

27

    let sum_exprs = (*sum_exprs)

1273

27

        .clone()

1274

27

        .unwrap_list()

1275

27

        .ok_or(RuleNotApplicable)?;

1276

3

    let (y, k) = match sum_exprs.as_slice() {

1277

3

        [Expr::Atomic(_, y), Expr::Atomic(_, Atom::Literal(k))] => (y, k),

1278

        [Expr::Atomic(_, Atom::Literal(k)), Expr::Atomic(_, y)] => (y, k),

1279

        _ => {

1280

            return Err(RuleNotApplicable);

1281

1282

};

1283

1284

3

    Ok(Reduction::pure(Expr::FlatIneq(

1285

3

        meta.clone_dirty(),

1286

3

        Moo::new(x),

1287

3

        Moo::new(y.clone()),

1288

3

        Box::new(k.clone()),

1289

3

)))

1290

44795

1291

1292

/// ```text

1293

/// y + k >= x ~> ineq(x,y,k)

1294

/// ```

1295

#[register_rule(("Minion",4800))]

1296

55814

fn y_plus_k_geq_x_to_ineq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1297

    // impl same as x_leq_y_plus_k but with lhs and rhs flipped

1298

55814

    let Expr::Geq(meta, e2, e1) = expr.clone() else {

1299

55544

        return Err(RuleNotApplicable);

1300

};

1301

1302

270

    let Expr::Atomic(_, x) = Moo::unwrap_or_clone(e1) else {

1303

        return Err(RuleNotApplicable);

1304

};

1305

1306

270

    let Expr::Sum(_, sum_exprs) = Moo::unwrap_or_clone(e2) else {

1307

213

        return Err(RuleNotApplicable);

1308

};

1309

1310

57

    let sum_exprs = Moo::unwrap_or_clone(sum_exprs)

1311

57

        .unwrap_list()

1312

57

        .ok_or(RuleNotApplicable)?;

1313

51

    let (y, k) = match sum_exprs.as_slice() {

1314

45

        [Expr::Atomic(_, y), Expr::Atomic(_, Atom::Literal(k))] => (y, k),

1315

        [Expr::Atomic(_, Atom::Literal(k)), Expr::Atomic(_, y)] => (y, k),

1316

        _ => {

1317

6

            return Err(RuleNotApplicable);

1318

1319

};

1320

1321

45

    Ok(Reduction::pure(Expr::FlatIneq(

1322

45

        meta.clone_dirty(),

1323

45

        Moo::new(x),

1324

45

        Moo::new(y.clone()),

1325

45

        Box::new(k.clone()),

1326

45

)))

1327

55814

1328

1329

/// Flattening rule for not(bool_lit)

1330

///

1331

/// For some boolean variable x:

1332

/// ```text

1333

///  not(x)      ~>  w-literal(x,0)

1334

/// ```

1335

///

1336

/// ## Rationale

1337

///

1338

/// Minion's watched-and and watched-or constraints only takes other constraints as arguments.

1339

///

1340

/// This restates boolean variables as the equivalent constraint "SAT if x is true".

1341

///

1342

/// The regular bool_lit case is dealt with directly by the Minion solver interface (as it is a

1343

/// trivial match).

1344

1345

#[register_rule(("Minion", 4100))]

1346

22469

fn not_literal_to_wliteral(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1347

22469

    match expr {

1348

39

        Expr::Not(m, expr) => {

1349

39

            if let Expr::Atomic(_, Atom::Reference(reference)) = (**expr).clone()

1350

36

                && reference.ptr().domain().is_some_and(|d| d.is_bool())

1351

1352

36

                return Ok(Reduction::pure(Expr::FlatWatchedLiteral(

1353

36

                    m.clone_dirty(),

1354

36

                    reference,

1355

36

                    Lit::Bool(false),

1356

36

                )));

1357

3

1358

3

            Err(RuleNotApplicable)

1359

1360

22430

        _ => Err(RuleNotApplicable),

1361

1362

22469

1363

1364

/// Flattening rule for not(X) in Minion, where X is a constraint.

1365

///

1366

/// ```text

1367

/// not(X) ~> reify(X,0)

1368

/// ```

1369

///

1370

/// This rule has lower priority than boolean_literal_to_wliteral so that we can assume that the

1371

/// nested expressions are constraints not variables.

1372

1373

#[register_rule(("Minion", 4090))]

1374

20012

fn not_constraint_to_reify(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1375

20009

    if !matches!(expr, Expr::Not(_,c) if !matches!(**c, Expr::Atomic(_,_))) {

1376

20009

        return Err(RuleNotApplicable);

1377

3

1378

1379

3

    let Expr::Not(m, e) = expr else {

1380

        unreachable!();

1381

};

1382

1383

3

    extra_check! {

1384

        if !is_flat(e) {

1385

            return Err(RuleNotApplicable);

1386

1387

};

1388

1389

3

    Ok(Reduction::pure(Expr::MinionReify(

1390

3

        m.clone(),

1391

3

        e.clone(),

1392

3

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

1393

3

)))

1394

20012

1395

1396

/// Converts an equality to a boolean into a `reify` constraint.

1397

///

1398

/// ```text

1399

/// x =aux c ~> reify(c,x)

1400

/// x = c ~> reify(c,x)

1401

///

1402

/// where c is a boolean constraint

1403

/// ```

1404

#[register_rule(("Minion", 4400))]

1405

40607

fn bool_eq_to_reify(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1406

40607

    let (atom, e): (Atom, Moo<Expr>) = match expr {

1407

1131

        Expr::AuxDeclaration(_, reference, e) => Ok((Atom::from(reference.clone()), e.clone())),

1408

2397

        Expr::Eq(_, a, b) => match (a.as_ref(), b.as_ref()) {

1409

1674

            (Expr::Atomic(_, atom), _) => Ok((atom.clone(), b.clone())),

1410

594

            (_, Expr::Atomic(_, atom)) => Ok((atom.clone(), a.clone())),

1411

129

            _ => Err(RuleNotApplicable),

1412

},

1413

1414

37079

        _ => Err(RuleNotApplicable),

1415

37208

}?;

1416

1417

    // e does not have to be valid minion constraint yet, as long as we know it can turn into one

1418

    // (i.e. it is boolean).

1419

3399

    if e.as_ref().return_type() != ReturnType::Bool {

1420

3153

        return Err(RuleNotApplicable);

1421

246

};

1422

1423

246

    Ok(Reduction::pure(Expr::MinionReify(Metadata::new(), e, atom)))

1424

40607

1425

1426

/// Converts an iff to an `Eq` constraint.

1427

///

1428

/// ```text

1429

/// Iff(a,b) ~> Eq(a,b)

1430

///

1431

/// ```

1432

#[register_rule(("Minion", 4400))]

1433

40607

fn iff_to_eq(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

1434

40607

    let Expr::Iff(_, x, y) = expr else {

1435

40598

        return Err(RuleNotApplicable);

1436

};

1437

1438

9

    Ok(Reduction::pure(Expr::Eq(

1439

9

        Metadata::new(),

1440

9

        x.clone(),

1441

9

        y.clone(),

1442

9

)))

1443

40607