Grcov report - minion.rs

1

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

2

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

3

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

4

5

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

6

7

use crate::{

8

    extra_check,

9

    utils::{is_flat, rewrite_children, to_aux_var},

10

};

11

use conjure_cp::ast::Moo;

12

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

13

use conjure_cp::{

14

    ast::Metadata,

15

    ast::{

16

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

17

        SymbolTable, Typeable,

18

},

19

    into_matrix_expr, matrix_expr,

20

    rule_engine::{

21

        ApplicationError, ApplicationResult, Reduction, register_rule, register_rule_set,

22

},

23

    settings::SolverFamily,

24

};

25

26

use ApplicationError::RuleNotApplicable;

27

use itertools::Itertools;

28

29

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

30

8094

    matches!(f, SolverFamily::Minion)

31

8094

});

32

33

/// Inlines constant matrix references just for Minion so Base matrix rules can lower them

34

/// without affecting other backends.

35

#[register_rule("Minion", 9000, [SafeIndex])]

36

1660446

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

37

1660446

    let Expr::SafeIndex(_, subject, indices) = expr else {

38

1601686

        return Err(RuleNotApplicable);

39

};

40

41

58760

    let Expr::Atomic(_, Atom::Reference(reference)) = subject.as_ref() else {

42

40914

        return Err(RuleNotApplicable);

43

};

44

45

17846

    let constant = reference.resolve_constant().ok_or(RuleNotApplicable)?;

46

18

    let Lit::AbstractLiteral(AbstractLiteral::Matrix(_, _)) = &constant else {

47

        return Err(RuleNotApplicable);

48

};

49

50

18

    Ok(Reduction::pure(Expr::SafeIndex(

51

18

        Metadata::new(),

52

18

        Moo::new(Expr::Atomic(Metadata::new(), Atom::Literal(constant))),

53

18

        indices.clone(),

54

18

)))

55

1660446

56

57

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

58

278768

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

59

    // product = val

60

    let val: Atom;

61

    let product: Moo<Expr>;

62

63

278768

    match expr.clone() {

64

11389

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

65

11389

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

66

11389

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

67

68

11389

            if let Some(f) = a_atom {

69

                // val = product

70

9078

                val = f.clone();

71

9078

                product = b;

72

9078

            } else if let Some(f) = b_atom {

73

                // product = val

74

1389

                val = f.clone();

75

1389

                product = a;

76

1389

            } else {

77

922

                return Err(RuleNotApplicable);

78

79

80

3775

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

81

3775

            val = Atom::Reference(reference);

82

3775

            product = e;

83

3775

84

        _ => {

85

263604

            return Err(RuleNotApplicable);

86

87

88

89

14242

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

90

13756

        return Err(RuleNotApplicable);

91

486

92

93

486

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

94

        return Err(RuleNotApplicable);

95

};

96

97

486

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

98

345

    if factors_vec.len() < 2 {

99

        return Err(RuleNotApplicable);

100

345

101

102

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

103

    // Introduce auxvars until it is a binop

104

105

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

106

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

107

108

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

109

345

    let x: Atom = factors_vec

110

345

        .pop()

111

345

        .unwrap()

112

345

        .try_into()

113

345

        .or(Err(RuleNotApplicable))?;

114

115

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

116

162

    let mut y: Atom = factors_vec

117

162

        .pop()

118

162

        .unwrap()

119

162

        .try_into()

120

162

        .or(Err(RuleNotApplicable))?;

121

122

162

    let mut symbols = symbols.clone();

123

162

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

124

125

    // FIXME: add a test for this

126

174

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

127

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

128

        // similar to other introduction rules.

129

12

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

130

131

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

132

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

133

12

        let aux_domain = Expr::Product(

134

12

            Metadata::new(),

135

12

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

136

12

137

12

        .domain_of()

138

12

        .ok_or(ApplicationError::DomainError)?;

139

140

12

        let aux_decl = symbols.gen_find(&aux_domain);

141

12

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

142

143

12

        let new_top_expr = Expr::FlatProductEq(

144

12

            Metadata::new(),

145

12

            Moo::new(y),

146

12

            Moo::new(next_factor_atom),

147

12

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

148

12

);

149

150

12

        new_tops.push(new_top_expr);

151

12

        y = aux_var;

152

153

154

162

    Ok(Reduction::new(

155

162

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

156

162

        new_tops,

157

162

        symbols,

158

162

))

159

278768

160

161

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

162

///

163

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

164

/// sum constraints are used.

165

///

166

/// # Details

167

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

168

/// it does its own flattening.

169

///

170

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

171

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

172

/// from a sum:

173

///

174

///```text

175

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

176

///   ~~> flatten_vecop

177

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

178

///

179

///

180

/// __0 =aux 1*a

181

/// __1 =aux 2*b

182

/// __2 =aux 3*c

183

/// ```

184

///

185

/// Therefore, introduce_weightedsumleq_sumgeq does its own flattening.

186

///

187

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

188

/// weighted sums.

189

///

190

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

191

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

192

///

193

///```text

194

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

195

///

196

///   ~> introduce_weightedsumleq_sumgeq

197

///

198

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

199

///

200

/// with new top level constraints

201

///

202

/// __0 = c*d

203

/// __1 = e/f

204

/// __2 = g/h

205

/// ```

206

///

207

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

208

///

209

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

210

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

211

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

212

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

213

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

214

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

215

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

216

///

217

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

218

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

219

#[register_rule("Minion", 4600, [Leq, Geq, Eq, AuxDeclaration])]

220

817361

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

221

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

222

    // constraints to make at the end

223

224

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

225

    // elsewhere, as this caused cyclic rule application:

226

//

227

    // ```

228

    // 2*a + b = c

229

//

230

    //   ~~> sumeq_to_inequalities

231

//

232

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

233

//

234

    // --

235

//

236

    // 2*a + b <= c

237

//

238

    //   ~~> flatten_generic

239

    // __1 <=c

240

//

241

    // with new top level constraint

242

//

243

    // 2*a + b =aux __1

244

//

245

    // --

246

//

247

    // 2*a + b =aux __1

248

//

249

    //   ~~> sumeq_to_inequalities

250

//

251

    // LOOP!

252

    // ```

253

    enum EqualityKind {

254

Eq,

255

        Leq,

256

        Geq,

257

258

259

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

260

//

261

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

262

    // on the right hand side.

263

//

264

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

265

42095

    fn match_sum_total(

266

42095

        a: Moo<Expr>,

267

42095

        b: Moo<Expr>,

268

42095

        equality_kind: EqualityKind,

269

42095

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

270

        match (

271

42095

            Moo::unwrap_or_clone(a),

272

42095

            Moo::unwrap_or_clone(b),

273

42095

            equality_kind,

274

) {

275

219

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

276

219

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

277

219

                    .unwrap_list()

278

219

                    .ok_or(RuleNotApplicable)?;

279

165

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

280

281

935

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

282

935

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

283

935

                    .unwrap_list()

284

935

                    .ok_or(RuleNotApplicable)?;

285

391

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

286

287

121

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

288

121

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

289

121

                    .unwrap_list()

290

121

                    .ok_or(RuleNotApplicable)?;

291

109

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

292

293

30

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

294

30

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

295

30

                    .unwrap_list()

296

30

                    .ok_or(RuleNotApplicable)?;

297

27

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

298

299

1398

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

300

1398

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

301

1398

                    .unwrap_list()

302

1398

                    .ok_or(RuleNotApplicable)?;

303

780

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

304

305

2178

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

306

2178

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

307

2178

                    .unwrap_list()

308

2178

                    .ok_or(RuleNotApplicable)?;

309

572

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

310

311

37214

            _ => Err(RuleNotApplicable),

312

313

42095

314

315

817361

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

316

16378

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

317

1432

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

318

24285

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

319

13377

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

320

13377

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

321

13377

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

322

5994

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

323

5994

                    .unwrap_list()

324

5994

                    .ok_or(RuleNotApplicable)?;

325

5133

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

326

            } else {

327

7383

                Err(RuleNotApplicable)

328

329

330

761889

        _ => Err(RuleNotApplicable),

331

769272

}?;

332

333

7177

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

334

7177

    let mut symtab = symtab.clone();

335

336

    #[allow(clippy::mutable_key_type)]

337

7177

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

338

339

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

340

//

341

11941

    for expr in sum_exprs {

342

11941

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

343

344

8329

        if coeff == 0 {

345

            continue;

346

8329

347

348

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

349

8329

        coefficients_and_vars

350

8329

            .entry(var)

351

8329

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

352

8329

            .or_insert(coeff);

353

354

355

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

356

7000

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

357

358

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

359

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

360

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

361

3565

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

362

3565

        .into_iter()

363

7567

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

364

4432

        .sorted_by(|a, b| {

365

4432

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

366

4432

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

367

4432

            a_atom_str.cmp(&b_atom_str)

368

4432

})

369

7567

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

370

3565

        .unzip();

371

372

3565

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

373

576

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

374

576

            Metadata::new(),

375

576

            Moo::new(matrix_expr![

376

576

                Expr::FlatWeightedSumLeq(

377

576

                    Metadata::new(),

378

576

                    coefficients.clone(),

379

576

                    vars.clone(),

380

576

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

381

576

),

382

576

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

383

576

]),

384

576

),

385

2321

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

386

2321

            Metadata::new(),

387

2321

            Moo::new(matrix_expr![

388

2321

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

389

2321

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

390

2321

]),

391

2321

),

392

        (EqualityKind::Leq, true) => {

393

60

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

394

395

132

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

396

        (EqualityKind::Geq, true) => {

397

30

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

398

399

446

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

400

};

401

402

3565

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

403

817361

404

405

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

406

///

407

///

408

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

409

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

410

///

411

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

412

///

413

/// # Errors

414

///

415

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

416

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

417

///

418

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

419

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

420

///

421

///

422

11941

fn flatten_weighted_sum_term(

423

11941

    term: Expr,

424

11941

    symtab: &mut SymbolTable,

425

11941

    top_level_exprs: &mut Vec<Expr>,

426

11941

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

427

1242

    match term {

428

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

429

//

430

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

431

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

432

//

433

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

434

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

435

1242

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

436

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

437

//

438

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

439

            // non-list matrix literal.

440

1242

            let factors = Moo::unwrap_or_clone(factors)

441

1242

                .unwrap_list()

442

1242

                .ok_or(RuleNotApplicable)?;

443

444

942

            match factors.as_slice() {

445

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

446

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

447

942

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

448

449

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

450

816

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

451

816

                    *coeff,

452

816

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

453

)),

454

455

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

456

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

457

                    *coeff,

458

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

459

)),

460

461

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

462

463

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

464

465

18

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

466

18

e,

467

18

                    rest @ ..,

468

                ] => {

469

18

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

470

18

                    product_terms.push(e.clone());

471

18

                    let product =

472

18

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

473

                    Ok((

474

18

                        *coeff,

475

18

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

476

))

477

478

479

                // no coefficient:

480

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

481

                _ => {

482

108

                    let product =

483

108

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

484

                    Ok((

485

1,

486

108

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

487

))

488

489

490

491

258

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

492

-1,

493

258

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

494

)),

495

10441

        term => Ok((

496

1,

497

10441

            flatten_expression_to_atom(term, symtab, top_level_exprs)?,

498

)),

499

500

11941

501

502

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

503

/// necessary.

504

///

505

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

506

/// `top_level_exprs`.

507

///

508

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

509

/// returned as-is.

510

///

511

/// # Errors

512

///

513

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

514

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

515

///

516

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

517

///    succeeds when the expression given is atomic.

518

///

519

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

520

///

521

12589

fn flatten_expression_to_atom(

522

12589

    expr: Expr,

523

12589

    symtab: &mut SymbolTable,

524

12589

    top_level_exprs: &mut Vec<Expr>,

525

12589

) -> Result<Atom, ApplicationError> {

526

12589

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

527

7541

        return Ok(atom);

528

5048

529

530

5048

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

531

1643

    *symtab = aux_var_info.symbols();

532

1643

    top_level_exprs.push(aux_var_info.top_level_expr());

533

534

1643

    Ok(aux_var_info.as_atom())

535

12589

536

537

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

538

278768

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

539

    // div = val

540

    let val: Atom;

541

    let div: Moo<Expr>;

542

    let meta: Metadata;

543

544

278768

    match expr.clone() {

545

11389

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

546

11389

            meta = m;

547

548

11389

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

549

11389

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

550

551

11389

            if let Some(f) = a_atom {

552

                // val = div

553

9078

                val = f.clone();

554

9078

                div = b;

555

9078

            } else if let Some(f) = b_atom {

556

                // div = val

557

1389

                val = f.clone();

558

1389

                div = a;

559

1389

            } else {

560

922

                return Err(RuleNotApplicable);

561

562

563

3775

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

564

3775

            meta = m;

565

3775

            val = Atom::Reference(reference);

566

3775

            div = e;

567

3775

568

        _ => {

569

263604

            return Err(RuleNotApplicable);

570

571

572

573

14242

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

574

13762

        return Err(RuleNotApplicable);

575

480

576

577

480

    let Expr::SafeDiv(_, a, b) = div.as_ref() else {

578

        return Err(RuleNotApplicable);

579

};

580

480

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

581

438

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

582

583

402

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

584

402

        meta,

585

402

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

586

402

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

587

402

        Moo::new(val),

588

402

)))

589

278768

590

591

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

592

278768

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

593

    // div = val

594

    let val: Atom;

595

    let div: Moo<Expr>;

596

    let meta: Metadata;

597

598

278768

    match expr.clone() {

599

11389

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

600

11389

            meta = m;

601

11389

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

602

11389

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

603

604

11389

            if let Some(f) = a_atom {

605

                // val = div

606

9078

                val = f.clone();

607

9078

                div = b;

608

9078

            } else if let Some(f) = b_atom {

609

                // div = val

610

1389

                val = f.clone();

611

1389

                div = a;

612

1389

            } else {

613

922

                return Err(RuleNotApplicable);

614

615

616

3775

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

617

3775

            meta = m;

618

3775

            val = Atom::Reference(reference);

619

3775

            div = e;

620

3775

621

        _ => {

622

263604

            return Err(RuleNotApplicable);

623

624

625

626

14242

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

627

14098

        return Err(RuleNotApplicable);

628

144

629

630

144

    let Expr::SafeMod(_, a, b) = div.as_ref() else {

631

        return Err(RuleNotApplicable);

632

};

633

144

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

634

144

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

635

636

132

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

637

132

        meta,

638

132

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

639

132

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

640

132

        Moo::new(val),

641

132

)))

642

278768

643

644

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

645

575409

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

646

575409

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

647

18522

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

648

18522

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

649

18522

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

650

18522

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

651

18522

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

652

653

18522

            if let Some(a_atom) = a_atom {

654

14357

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

655

4165

            } else if let Some(b_atom) = b_atom {

656

2046

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

657

            } else {

658

2119

                Err(RuleNotApplicable)

659

660

661

662

8748

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

663

8748

            let a = Atom::Reference(reference);

664

8748

            let expr = Moo::unwrap_or_clone(expr);

665

8748

            Ok((a, expr))

666

667

668

548139

        _ => Err(RuleNotApplicable),

669

550258

}?;

670

671

25151

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

672

24995

        return Err(RuleNotApplicable);

673

};

674

675

156

    let y = Moo::unwrap_or_clone(y);

676

156

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

677

678

144

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

679

144

        Metadata::new(),

680

144

        Moo::new(x),

681

144

        Moo::new(y),

682

144

)))

683

575409

684

685

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

686

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

687

278768

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

688

278768

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

689

11389

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

690

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

691

72

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

692

11317

            _ => Err(RuleNotApplicable),

693

},

694

695

3775

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

696

54

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

697

54

                let total_ref_atom = Atom::Reference(total_reference);

698

54

                Ok((a, b, total_ref_atom))

699

700

3721

            _ => Err(RuleNotApplicable),

701

},

702

263604

        _ => Err(RuleNotApplicable),

703

278642

}?;

704

705

126

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

706

126

        .try_into()

707

126

        .or(Err(RuleNotApplicable))?;

708

114

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

709

114

        .try_into()

710

114

        .or(Err(RuleNotApplicable))?;

711

712

114

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

713

114

        Metadata::new(),

714

114

        Moo::new(a),

715

114

        Moo::new(b),

716

114

        Moo::new(total),

717

114

)))

718

278768

719

720

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

721

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

722

278768

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

723

278768

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

724

277520

        return Err(RuleNotApplicable);

725

};

726

727

1248

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

728

729

288

    let atoms = es

730

288

        .into_iter()

731

1110

        .map(|e| match e {

732

1092

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

733

18

            _ => Err(RuleNotApplicable),

734

1110

})

735

288

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

736

737

270

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

738

278768

739

740

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

741

///

742

/// ```text

743

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

744

///

745

///   where x,y are atoms

746

/// ```

747

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

748

575409

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

749

575409

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

750

556887

        return Err(RuleNotApplicable);

751

};

752

753

37008

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

754

37008

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

755

28888

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

756

28828

            return None;

757

};

758

759

60

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

760

761

48

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

762

37008

763

764

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

765

18522

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

766

18474

        return Err(RuleNotApplicable);

767

};

768

769

48

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

770

48

        Metadata::new(),

771

48

        Moo::new(x),

772

48

        Moo::new(y),

773

48

)))

774

575409

775

776

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

777

///

778

/// ```text

779

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

780

///

781

///   where x,y are atoms

782

/// ```

783

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

784

575409

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

785

    // a =aux -b

786

//

787

575409

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

788

566661

        return Err(RuleNotApplicable);

789

};

790

791

8748

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

792

793

8748

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

794

8700

        return Err(RuleNotApplicable);

795

};

796

797

48

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

798

24

        return Err(RuleNotApplicable);

799

};

800

801

24

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

802

24

        Metadata::new(),

803

24

        Moo::new(a),

804

24

        Moo::new(b),

805

24

)))

806

575409

807

808

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

809

///

810

/// ```text

811

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

812

/// where x is atomic, y is atomic

813

///

814

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

815

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

816

/// ```

817

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

818

575409

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

819

575409

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

820

572885

        return Err(RuleNotApplicable);

821

};

822

823

2524

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

824

825

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

826

//

827

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

828

1126

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

829

730

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

830

730

            Metadata::new(),

831

730

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

832

730

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

833

730

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

834

730

)))

835

    } else {

836

396

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

837

396

            Metadata::new(),

838

396

            y.clone(),

839

396

            x_atom.clone(),

840

396

)))

841

842

575409

843

844

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

845

///

846

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

847

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

848

575409

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

849

575409

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

850

575283

        return Err(RuleNotApplicable);

851

};

852

853

126

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

854

78

        return Err(RuleNotApplicable);

855

};

856

857

48

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

858

        return Err(RuleNotApplicable);

859

};

860

861

48

    let mut out_ranges = vec![];

862

863

48

    for range in ranges {

864

48

        match range {

865

            Range::Single(x) => {

866

                out_ranges.push(*x);

867

                out_ranges.push(*x);

868

869

48

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

870

48

                out_ranges.push(*x);

871

48

                out_ranges.push(*y);

872

48

873

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

874

                return Err(RuleNotApplicable);

875

876

877

878

879

48

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

880

48

        Metadata::new(),

881

48

        atom.clone(),

882

48

        out_ranges,

883

48

)))

884

575409

885

886

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

887

///

888

/// 1. the subject is a list literal

889

/// 2. the subject is one dimensional

890

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

891

575409

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

892

575409

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

893

18522

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

894

24

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

895

24

                Ok((eq, subject, indices))

896

897

882

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

898

882

                Ok((eq, subject, indices))

899

900

17616

            _ => Err(RuleNotApplicable),

901

},

902

8748

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

903

1080

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

904

1080

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

905

906

7668

            _ => Err(RuleNotApplicable),

907

},

908

12632

        Expr::SafeIndex(_, subject, indices) if expr.return_type() == ReturnType::Bool => {

909

2

            Ok((Atom::Literal(Lit::Bool(true)), subject, indices))

910

911

548137

        _ => Err(RuleNotApplicable),

912

573421

}?;

913

914

1988

    if indices.len() != 1 {

915

        return Err(RuleNotApplicable);

916

1988

917

918

1988

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

919

246

        return Err(RuleNotApplicable);

920

};

921

922

1742

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

923

336

        return Err(RuleNotApplicable);

924

};

925

926

1406

    let mut atom_list = vec![];

927

928

8944

    for elem in list {

929

8944

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

930

162

            return Err(RuleNotApplicable);

931

};

932

933

8782

        atom_list.push(elem);

934

935

936

1244

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

937

1244

        Metadata::new(),

938

1244

        atom_list,

939

1244

        Moo::new(index),

940

1244

        Moo::new(equalto),

941

1244

)))

942

575409

943

944

/// Flattens an implication.

945

///

946

/// ```text

947

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

948

///  ~~>

949

/// __0 -> y,

950

///

951

/// with new top level constraints

952

/// __0 =aux x

953

///

954

/// ```

955

///

956

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

957

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

958

/// an argument:

959

///

960

/// ``` text

961

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

962

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

963

/// ```

964

///

965

/// See [`introduce_reifyimply_ineq_from_imply`].

966

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

967

278768

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

968

278768

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

969

278134

        return Err(RuleNotApplicable);

970

};

971

972

    // flatten x

973

634

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

974

975

434

    let symbols = aux_var_info.symbols();

976

434

    let new_x = aux_var_info.as_expr();

977

978

434

    Ok(Reduction::new(

979

434

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

980

434

        vec![aux_var_info.top_level_expr()],

981

434

        symbols,

982

434

))

983

278768

984

985

#[register_rule("Minion", 4200, [SafeDiv, Neq, SafeMod, SafePow, Leq, Geq, Abs, Neg, Not, SafeIndex, InDomain, ToInt])]

986

278768

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

987

256728

    if !matches!(

988

278768

        expr,

989

        Expr::SafeDiv(_, _, _)

990

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

991

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

992

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

993

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

994

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

995

            | Expr::Abs(_, _)

996

            | Expr::Neg(_, _)

997

            | Expr::Not(_, _)

998

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

999

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

1000

            | Expr::ToInt(_, _)

1001

) {

1002

256728

        return Err(RuleNotApplicable);

1003

22040

1004

1005

22040

    let mut symbols = symbols.clone();

1006

22040

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

1007

1008

39784

    let (expr, num_changed) = rewrite_children(expr, |child| {

1009

39784

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

1010

3056

            symbols = aux_var_info.symbols();

1011

3056

            new_tops.push(aux_var_info.top_level_expr());

1012

3056

            (aux_var_info.as_expr(), true)

1013

        } else {

1014

36728

            (child, false)

1015

1016

39784

});

1017

1018

22040

    if num_changed == 0 {

1019

19050

        return Err(RuleNotApplicable);

1020

2990

1021

1022

2990

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

1023

278768

1024

1025

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

1026

278768

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

1027

278768

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

1028

267379

        return Err(RuleNotApplicable);

1029

11389

1030

1031

11389

    let mut symbols = symbols.clone();

1032

11389

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

1033

1034

22778

    let (expr, num_changed) = rewrite_children(expr, |child| {

1035

22778

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

1036

2918

            symbols = aux_var_info.symbols();

1037

2918

            new_tops.push(aux_var_info.top_level_expr());

1038

2918

            (aux_var_info.as_expr(), true)

1039

        } else {

1040

19860

            (child, false)

1041

1042

22778

});

1043

1044

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

1045

11389

    if num_changed != 2 {

1046

11229

        return Err(RuleNotApplicable);

1047

160

1048

1049

160

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

1050

278768

1051

1052

/// Flattens products containing lists.

1053

///

1054

/// For example,

1055

///

1056

/// ```plain

1057

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

1058

/// ```

1059

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

1060

278768

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

1061

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

1062

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

1063

    // literal in an aux var.

1064

//

1065

    // e.g.

1066

//

1067

    // flatten_generic would do

1068

//

1069

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

1070

//

1071

    // we want to do

1072

//

1073

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

1074

//

1075

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

1076

//

1077

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

1078

//

1079

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

1080

    //  matrix literal.

1081

//

1082

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

1083

1084

278768

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

1085

277472

        return Err(RuleNotApplicable);

1086

};

1087

1088

1296

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

1089

1090

495

    let mut new_factors = vec![];

1091

495

    let mut top_level_exprs = vec![];

1092

495

    let mut symtab = symtab.clone();

1093

1094

948

    for factor in factors {

1095

948

        new_factors.push(Expr::Atomic(

1096

948

            Metadata::new(),

1097

948

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

1098

));

1099

1100

1101

    // have we done anything?

1102

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

1103

402

    if top_level_exprs.is_empty() {

1104

294

        return Err(RuleNotApplicable);

1105

108

1106

1107

108

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

1108

108

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

1109

278768

1110

1111

/// Flattens a matrix literal that contains expressions.

1112

///

1113

/// For example,

1114

///

1115

/// ```plain

1116

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

1117

///

1118

/// where

1119

/// __0 =aux e/2,

1120

/// __1 =aux f*5

1121

/// ```

1122

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

1123

73429

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

1124

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

1125

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

1126

69780

    if matches!(

1127

73429

        expr,

1128

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

1129

) {

1130

3649

        return Err(RuleNotApplicable);

1131

69780

1132

1133

69780

    let mut symbols = symtab.clone();

1134

69780

    let mut top_level_exprs = vec![];

1135

1136

    // flatten any children that are matrix literals

1137

69780

    let (expr, num_changed) = rewrite_children(expr, |child| {

1138

        // is this a matrix literal?

1139

//

1140

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

1141

        // matrices, not just those that are lists.

1142

//

1143

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

1144

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

1145

46154

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

1146

43998

            return (child, false);

1147

};

1148

1149

2156

        let mut child_changed = false;

1150

1151

        // flatten expressions

1152

4754

        for e in es.iter_mut() {

1153

4754

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

1154

136

                *e = aux_info.as_expr();

1155

136

                top_level_exprs.push(aux_info.top_level_expr());

1156

136

                symbols = aux_info.symbols();

1157

136

                child_changed = true;

1158

4618

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

1159

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

1160

1161

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

1162

                // inside a matrix list.

1163

//

1164

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

1165

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

1166

//

1167

                // we want to flatten this to

1168

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

1169

1170

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

1171

                    continue;

1172

};

1173

1174

                let categories = e.universe_categories();

1175

1176

                // must contain a decision variable

1177

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

1178

                    continue;

1179

1180

1181

                // must not contain givens or quantified variables

1182

                if categories.contains(&Category::Parameter)

1183

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

1184

1185

                    continue;

1186

1187

1188

                let decl = symbols.gen_find(&domain);

1189

1190

                top_level_exprs.push(Expr::AuxDeclaration(

1191

                    Metadata::new(),

1192

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

1193

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

1194

));

1195

1196

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

1197

1198

                child_changed = true;

1199

4618

1200

1201

1202

2156

        (into_matrix_expr!(es;index_domain), child_changed)

1203

46154

});

1204

1205

69780

    if num_changed != 0 {

1206

74

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

1207

    } else {

1208

69706

        Err(RuleNotApplicable)

1209

1210

73429

1211

1212

/// Converts a Geq to an Ineq

1213

///

1214

/// ```text

1215

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

1216

/// ```

1217

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

1218

181772

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

1219

181772

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

1220

181233

        return Err(RuleNotApplicable);

1221

};

1222

1223

539

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

1224

14

        return Err(RuleNotApplicable);

1225

};

1226

1227

525

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

1228

        return Err(RuleNotApplicable);

1229

};

1230

1231

525

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

1232

525

        meta,

1233

525

        Moo::new(y),

1234

525

        Moo::new(x),

1235

525

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

1236

525

)))

1237

181772

1238

1239

/// Converts a Leq to an Ineq

1240

///

1241

/// ```text

1242

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

1243

/// ```

1244

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

1245

181772

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

1246

181772

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

1247

179690

        return Err(RuleNotApplicable);

1248

};

1249

1250

2082

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

1251

66

        return Err(RuleNotApplicable);

1252

};

1253

1254

2016

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

1255

140

        return Err(RuleNotApplicable);

1256

};

1257

1258

1876

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

1259

1876

        meta,

1260

1876

        Moo::new(x),

1261

1876

        Moo::new(y),

1262

1876

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

1263

1876

)))

1264

181772

1265

1266

// TODO: add this rule for geq

1267

1268

/// ```text

1269

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

1270

/// ```

1271

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

1272

662138

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

1273

662138

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

1274

649397

        return Err(RuleNotApplicable);

1275

};

1276

1277

12741

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

1278

2124

        return Err(RuleNotApplicable);

1279

};

1280

1281

10617

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

1282

10070

        return Err(RuleNotApplicable);

1283

};

1284

1285

547

    let sum_exprs = (*sum_exprs)

1286

547

        .clone()

1287

547

        .unwrap_list()

1288

547

        .ok_or(RuleNotApplicable)?;

1289

3

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

1290

3

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

1291

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

1292

        _ => {

1293

            return Err(RuleNotApplicable);

1294

1295

};

1296

1297

3

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

1298

3

        meta,

1299

3

        Moo::new(x),

1300

3

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

1301

3

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

1302

3

)))

1303

662138

1304

1305

/// ```text

1306

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

1307

/// ```

1308

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

1309

873601

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

1310

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

1311

873601

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

1312

872050

        return Err(RuleNotApplicable);

1313

};

1314

1315

1551

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

1316

132

        return Err(RuleNotApplicable);

1317

};

1318

1319

1419

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

1320

1215

        return Err(RuleNotApplicable);

1321

};

1322

1323

204

    let sum_exprs = Moo::unwrap_or_clone(sum_exprs)

1324

204

        .unwrap_list()

1325

204

        .ok_or(RuleNotApplicable)?;

1326

192

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

1327

72

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

1328

6

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

1329

        _ => {

1330

114

            return Err(RuleNotApplicable);

1331

1332

};

1333

1334

78

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

1335

78

        meta,

1336

78

        Moo::new(x),

1337

78

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

1338

78

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

1339

78

)))

1340

873601

1341

1342

/// Flattening rule for not(bool_lit)

1343

///

1344

/// For some boolean variable x:

1345

/// ```text

1346

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

1347

/// ```

1348

///

1349

/// ## Rationale

1350

///

1351

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

1352

///

1353

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

1354

///

1355

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

1356

/// trivial match).

1357

1358

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

1359

181772

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

1360

181772

    match expr {

1361

1276

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

1362

1276

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

1363

676

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

1364

1365

676

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

1366

676

                    m.clone(),

1367

676

                    reference,

1368

676

                    Lit::Bool(false),

1369

676

                )));

1370

600

1371

600

            Err(RuleNotApplicable)

1372

1373

180496

        _ => Err(RuleNotApplicable),

1374

1375

181772

1376

1377

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

1378

///

1379

/// ```text

1380

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

1381

/// ```

1382

///

1383

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

1384

/// nested expressions are constraints not variables.

1385

1386

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

1387

153277

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

1388

153273

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

1389

153273

        return Err(RuleNotApplicable);

1390

4

1391

1392

4

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

1393

        unreachable!();

1394

};

1395

1396

4

    extra_check! {

1397

        if !is_flat(e) {

1398

            return Err(RuleNotApplicable);

1399

1400

};

1401

1402

4

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

1403

4

        m.clone(),

1404

4

        e.clone(),

1405

4

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

1406

4

)))

1407

153277

1408

1409

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

1410

///

1411

/// ```text

1412

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

1413

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

1414

///

1415

/// where c is a boolean constraint

1416

/// ```

1417

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

1418

575409

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

1419

575409

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

1420

8748

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

1421

18522

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

1422

14357

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

1423

2046

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

1424

2119

            _ => Err(RuleNotApplicable),

1425

},

1426

1427

548139

        _ => Err(RuleNotApplicable),

1428

550258

}?;

1429

1430

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

1431

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

1432

25151

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

1433

23538

        return Err(RuleNotApplicable);

1434

1613

};

1435

1436

1613

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

1437

575409

1438

1439

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

1440

///

1441

/// ```text

1442

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

1443

///

1444

/// ```

1445

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

1446

575409

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

1447

575409

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

1448

575367

        return Err(RuleNotApplicable);

1449

};

1450

1451

42

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

1452

42

        Metadata::new(),

1453

42

        x.clone(),

1454

42

        y.clone(),

1455

42

)))

1456

575409