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

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

18

        SymbolTable, 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

7638

    matches!(f, SolverFamily::Minion)

34

7638

});

35

36

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

37

/// without affecting other backends.

38

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

39

1563130

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

40

1563130

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

41

1504034

        return Err(RuleNotApplicable);

42

};

43

44

59096

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

45

40914

        return Err(RuleNotApplicable);

46

};

47

48

18182

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

49

18

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

50

        return Err(RuleNotApplicable);

51

};

52

53

18

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

54

18

        Metadata::new(),

55

18

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

56

18

        indices.clone(),

57

18

)))

58

1563130

59

60

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

61

254710

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

62

    // product = val

63

    let val: Atom;

64

    let product: Moo<Expr>;

65

66

254710

    match expr.clone() {

67

11387

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

68

11387

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

69

11387

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

70

71

11387

            if let Some(f) = a_atom {

72

                // val = product

73

9054

                val = f.clone();

74

9054

                product = b;

75

9054

            } else if let Some(f) = b_atom {

76

                // product = val

77

1411

                val = f.clone();

78

1411

                product = a;

79

1411

            } else {

80

922

                return Err(RuleNotApplicable);

81

82

83

3775

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

84

3775

            val = Atom::Reference(reference);

85

3775

            product = e;

86

3775

87

        _ => {

88

239548

            return Err(RuleNotApplicable);

89

90

91

92

14240

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

93

13754

        return Err(RuleNotApplicable);

94

486

95

96

486

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

97

        return Err(RuleNotApplicable);

98

};

99

100

486

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

101

345

    if factors_vec.len() < 2 {

102

        return Err(RuleNotApplicable);

103

345

104

105

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

106

    // Introduce auxvars until it is a binop

107

108

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

109

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

110

111

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

112

345

    let x: Atom = factors_vec

113

345

        .pop()

114

345

        .unwrap()

115

345

        .try_into()

116

345

        .or(Err(RuleNotApplicable))?;

117

118

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

119

162

    let mut y: Atom = factors_vec

120

162

        .pop()

121

162

        .unwrap()

122

162

        .try_into()

123

162

        .or(Err(RuleNotApplicable))?;

124

125

162

    let mut symbols = symbols.clone();

126

162

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

127

128

    // FIXME: add a test for this

129

174

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

130

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

131

        // similar to other introduction rules.

132

12

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

133

134

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

135

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

136

12

        let aux_domain = Expr::Product(

137

12

            Metadata::new(),

138

12

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

139

12

140

12

        .domain_of()

141

12

        .ok_or(ApplicationError::DomainError)?;

142

143

12

        let aux_decl = symbols.gen_find(&aux_domain);

144

12

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

145

146

12

        let new_top_expr = Expr::FlatProductEq(

147

12

            Metadata::new(),

148

12

            Moo::new(y),

149

12

            Moo::new(next_factor_atom),

150

12

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

151

12

);

152

153

12

        new_tops.push(new_top_expr);

154

12

        y = aux_var;

155

156

157

162

    Ok(Reduction::new(

158

162

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

159

162

        new_tops,

160

162

        symbols,

161

162

))

162

254710

163

164

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

165

///

166

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

167

/// sum constraints are used.

168

///

169

/// # Details

170

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

171

/// it does its own flattening.

172

///

173

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

174

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

175

/// from a sum:

176

///

177

///```text

178

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

179

///   ~~> flatten_vecop

180

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

181

///

182

///

183

/// __0 =aux 1*a

184

/// __1 =aux 2*b

185

/// __2 =aux 3*c

186

/// ```

187

///

188

/// Therefore, introduce_weightedsumleq_sumgeq does its own flattening.

189

///

190

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

191

/// weighted sums.

192

///

193

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

194

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

195

///

196

///```text

197

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

198

///

199

///   ~> introduce_weightedsumleq_sumgeq

200

///

201

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

202

///

203

/// with new top level constraints

204

///

205

/// __0 = c*d

206

/// __1 = e/f

207

/// __2 = g/h

208

/// ```

209

///

210

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

211

///

212

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

213

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

214

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

215

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

216

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

217

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

218

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

219

///

220

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

221

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

222

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

223

731929

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

224

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

225

    // constraints to make at the end

226

227

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

228

    // elsewhere, as this caused cyclic rule application:

229

//

230

    // ```

231

    // 2*a + b = c

232

//

233

    //   ~~> sumeq_to_inequalities

234

//

235

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

236

//

237

    // --

238

//

239

    // 2*a + b <= c

240

//

241

    //   ~~> flatten_generic

242

    // __1 <=c

243

//

244

    // with new top level constraint

245

//

246

    // 2*a + b =aux __1

247

//

248

    // --

249

//

250

    // 2*a + b =aux __1

251

//

252

    //   ~~> sumeq_to_inequalities

253

//

254

    // LOOP!

255

    // ```

256

    enum EqualityKind {

257

Eq,

258

        Leq,

259

        Geq,

260

261

262

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

263

//

264

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

265

    // on the right hand side.

266

//

267

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

268

39165

    fn match_sum_total(

269

39165

        a: Moo<Expr>,

270

39165

        b: Moo<Expr>,

271

39165

        equality_kind: EqualityKind,

272

39165

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

273

        match (

274

39165

            Moo::unwrap_or_clone(a),

275

39165

            Moo::unwrap_or_clone(b),

276

39165

            equality_kind,

277

) {

278

111

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

279

111

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

280

111

                    .unwrap_list()

281

111

                    .ok_or(RuleNotApplicable)?;

282

57

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

283

284

677

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

285

677

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

286

677

                    .unwrap_list()

287

677

                    .ok_or(RuleNotApplicable)?;

288

133

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

289

290

121

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

291

121

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

292

121

                    .unwrap_list()

293

121

                    .ok_or(RuleNotApplicable)?;

294

109

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

295

296

30

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

297

30

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

298

30

                    .unwrap_list()

299

30

                    .ok_or(RuleNotApplicable)?;

300

27

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

301

302

1396

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

303

1396

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

304

1396

                    .unwrap_list()

305

1396

                    .ok_or(RuleNotApplicable)?;

306

780

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

307

308

2178

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

309

2178

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

310

2178

                    .unwrap_list()

311

2178

                    .ok_or(RuleNotApplicable)?;

312

572

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

313

314

34652

            _ => Err(RuleNotApplicable),

315

316

39165

317

318

731929

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

319

13486

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

320

1456

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

321

24223

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

322

12909

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

323

12909

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

324

12909

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

325

5832

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

326

5832

                    .unwrap_list()

327

5832

                    .ok_or(RuleNotApplicable)?;

328

4971

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

329

            } else {

330

7077

                Err(RuleNotApplicable)

331

332

333

679855

        _ => Err(RuleNotApplicable),

334

686932

}?;

335

336

6649

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

337

6649

    let mut symtab = symtab.clone();

338

339

    #[allow(clippy::mutable_key_type)]

340

6649

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

341

342

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

343

//

344

10885

    for expr in sum_exprs {

345

10885

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

346

347

7273

        if coeff == 0 {

348

            continue;

349

7273

350

351

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

352

7273

        coefficients_and_vars

353

7273

            .entry(var)

354

7273

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

355

7273

            .or_insert(coeff);

356

357

358

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

359

6007

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

360

361

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

362

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

363

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

364

3037

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

365

3037

        .into_iter()

366

6547

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

367

3959

        .sorted_by(|a, b| {

368

3959

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

369

3959

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

370

3959

            a_atom_str.cmp(&b_atom_str)

371

3959

})

372

6547

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

373

3037

        .unzip();

374

375

3037

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

376

576

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

377

576

            Metadata::new(),

378

576

            Moo::new(matrix_expr![

379

576

                Expr::FlatWeightedSumLeq(

380

576

                    Metadata::new(),

381

576

                    coefficients.clone(),

382

576

                    vars.clone(),

383

576

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

384

576

),

385

576

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

386

576

]),

387

576

),

388

2159

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

389

2159

            Metadata::new(),

390

2159

            Moo::new(matrix_expr![

391

2159

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

392

2159

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

393

2159

]),

394

2159

),

395

        (EqualityKind::Leq, true) => {

396

24

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

397

398

60

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

399

        (EqualityKind::Geq, true) => {

400

30

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

401

402

188

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

403

};

404

405

3037

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

406

731929

407

408

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

409

///

410

///

411

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

412

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

413

///

414

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

415

///

416

/// # Errors

417

///

418

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

419

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

420

///

421

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

422

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

423

///

424

///

425

10885

fn flatten_weighted_sum_term(

426

10885

    term: Expr,

427

10885

    symtab: &mut SymbolTable,

428

10885

    top_level_exprs: &mut Vec<Expr>,

429

10885

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

430

1242

    match term {

431

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

432

//

433

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

434

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

435

//

436

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

437

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

438

1242

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

439

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

440

//

441

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

442

            // non-list matrix literal.

443

1242

            let factors = Moo::unwrap_or_clone(factors)

444

1242

                .unwrap_list()

445

1242

                .ok_or(RuleNotApplicable)?;

446

447

942

            match factors.as_slice() {

448

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

449

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

450

942

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

451

452

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

453

816

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

454

816

                    *coeff,

455

816

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

456

)),

457

458

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

459

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

460

                    *coeff,

461

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

462

)),

463

464

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

465

466

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

467

468

18

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

469

18

e,

470

18

                    rest @ ..,

471

                ] => {

472

18

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

473

18

                    product_terms.push(e.clone());

474

18

                    let product =

475

18

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

476

                    Ok((

477

18

                        *coeff,

478

18

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

479

))

480

481

482

                // no coefficient:

483

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

484

                _ => {

485

108

                    let product =

486

108

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

487

                    Ok((

488

1,

489

108

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

490

))

491

492

493

494

258

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

495

-1,

496

258

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

497

)),

498

9385

        term => Ok((

499

1,

500

9385

            flatten_expression_to_atom(term, symtab, top_level_exprs)?,

501

)),

502

503

10885

504

505

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

506

/// necessary.

507

///

508

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

509

/// `top_level_exprs`.

510

///

511

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

512

/// returned as-is.

513

///

514

/// # Errors

515

///

516

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

517

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

518

///

519

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

520

///    succeeds when the expression given is atomic.

521

///

522

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

523

///

524

11533

fn flatten_expression_to_atom(

525

11533

    expr: Expr,

526

11533

    symtab: &mut SymbolTable,

527

11533

    top_level_exprs: &mut Vec<Expr>,

528

11533

) -> Result<Atom, ApplicationError> {

529

11533

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

530

6539

        return Ok(atom);

531

4994

532

533

4994

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

534

1589

    *symtab = aux_var_info.symbols();

535

1589

    top_level_exprs.push(aux_var_info.top_level_expr());

536

537

1589

    Ok(aux_var_info.as_atom())

538

11533

539

540

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

541

254710

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

542

    // div = val

543

    let val: Atom;

544

    let div: Moo<Expr>;

545

    let meta: Metadata;

546

547

254710

    match expr.clone() {

548

11387

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

549

11387

            meta = m;

550

551

11387

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

552

11387

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

553

554

11387

            if let Some(f) = a_atom {

555

                // val = div

556

9054

                val = f.clone();

557

9054

                div = b;

558

9054

            } else if let Some(f) = b_atom {

559

                // div = val

560

1411

                val = f.clone();

561

1411

                div = a;

562

1411

            } else {

563

922

                return Err(RuleNotApplicable);

564

565

566

3775

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

567

3775

            meta = m;

568

3775

            val = Atom::Reference(reference);

569

3775

            div = e;

570

3775

571

        _ => {

572

239548

            return Err(RuleNotApplicable);

573

574

575

576

14240

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

577

13760

        return Err(RuleNotApplicable);

578

480

579

580

480

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

581

480

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

582

438

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

583

584

402

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

585

402

        meta,

586

402

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

587

402

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

588

402

        Moo::new(val),

589

402

)))

590

254710

591

592

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

593

254710

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

594

    // div = val

595

    let val: Atom;

596

    let div: Moo<Expr>;

597

    let meta: Metadata;

598

599

254710

    match expr.clone() {

600

11387

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

601

11387

            meta = m;

602

11387

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

603

11387

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

604

605

11387

            if let Some(f) = a_atom {

606

                // val = div

607

9054

                val = f.clone();

608

9054

                div = b;

609

9054

            } else if let Some(f) = b_atom {

610

                // div = val

611

1411

                val = f.clone();

612

1411

                div = a;

613

1411

            } else {

614

922

                return Err(RuleNotApplicable);

615

616

617

3775

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

618

3775

            meta = m;

619

3775

            val = Atom::Reference(reference);

620

3775

            div = e;

621

3775

622

        _ => {

623

239548

            return Err(RuleNotApplicable);

624

625

626

627

14240

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

628

14096

        return Err(RuleNotApplicable);

629

144

630

631

144

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

632

144

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

633

144

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

634

635

132

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

636

132

        meta,

637

132

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

638

132

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

639

132

        Moo::new(val),

640

132

)))

641

254710

642

643

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

644

530765

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

645

530765

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

646

18478

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

647

18478

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

648

18478

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

649

18478

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

650

18478

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

651

652

18478

            if let Some(a_atom) = a_atom {

653

14315

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

654

4163

            } else if let Some(b_atom) = b_atom {

655

2044

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

656

            } else {

657

2119

                Err(RuleNotApplicable)

658

659

660

661

8442

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

662

8442

            let a = Atom::Reference(reference);

663

8442

            let expr = Moo::unwrap_or_clone(expr);

664

8442

            Ok((a, expr))

665

666

667

503845

        _ => Err(RuleNotApplicable),

668

505964

}?;

669

670

24801

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

671

24669

        return Err(RuleNotApplicable);

672

};

673

674

132

    let y = Moo::unwrap_or_clone(y);

675

132

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

676

677

120

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

678

120

        Metadata::new(),

679

120

        Moo::new(x),

680

120

        Moo::new(y),

681

120

)))

682

530765

683

684

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

685

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

686

254710

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

687

254710

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

688

11387

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

689

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

690

72

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

691

11315

            _ => Err(RuleNotApplicable),

692

},

693

694

3775

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

695

54

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

696

54

                let total_ref_atom = Atom::Reference(total_reference);

697

54

                Ok((a, b, total_ref_atom))

698

699

3721

            _ => Err(RuleNotApplicable),

700

},

701

239548

        _ => Err(RuleNotApplicable),

702

254584

}?;

703

704

126

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

705

126

        .try_into()

706

126

        .or(Err(RuleNotApplicable))?;

707

114

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

708

114

        .try_into()

709

114

        .or(Err(RuleNotApplicable))?;

710

711

114

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

712

114

        Metadata::new(),

713

114

        Moo::new(a),

714

114

        Moo::new(b),

715

114

        Moo::new(total),

716

114

)))

717

254710

718

719

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

720

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

721

254710

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

722

254710

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

723

253462

        return Err(RuleNotApplicable);

724

};

725

726

1248

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

727

728

288

    let atoms = es

729

288

        .into_iter()

730

1110

        .map(|e| match e {

731

1092

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

732

18

            _ => Err(RuleNotApplicable),

733

1110

})

734

288

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

735

736

270

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

737

254710

738

739

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

740

///

741

/// ```text

742

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

743

///

744

///   where x,y are atoms

745

/// ```

746

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

747

530765

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

748

530765

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

749

512287

        return Err(RuleNotApplicable);

750

};

751

752

36920

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

753

36920

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

754

28826

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

755

28766

            return None;

756

};

757

758

60

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

759

760

48

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

761

36920

762

763

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

764

18478

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

765

18430

        return Err(RuleNotApplicable);

766

};

767

768

48

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

769

48

        Metadata::new(),

770

48

        Moo::new(x),

771

48

        Moo::new(y),

772

48

)))

773

530765

774

775

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

776

///

777

/// ```text

778

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

779

///

780

///   where x,y are atoms

781

/// ```

782

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

783

530765

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

784

    // a =aux -b

785

//

786

530765

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

787

522323

        return Err(RuleNotApplicable);

788

};

789

790

8442

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

791

792

8442

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

793

8394

        return Err(RuleNotApplicable);

794

};

795

796

48

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

797

24

        return Err(RuleNotApplicable);

798

};

799

800

24

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

801

24

        Metadata::new(),

802

24

        Moo::new(a),

803

24

        Moo::new(b),

804

24

)))

805

530765

806

807

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

808

///

809

/// ```text

810

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

811

/// where x is atomic, y is atomic

812

///

813

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

814

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

815

/// ```

816

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

817

530765

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

818

530765

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

819

528835

        return Err(RuleNotApplicable);

820

};

821

822

1930

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

823

824

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

825

//

826

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

827

532

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

828

136

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

829

136

            Metadata::new(),

830

136

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

831

136

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

832

136

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

833

136

)))

834

    } else {

835

396

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

836

396

            Metadata::new(),

837

396

            y.clone(),

838

396

            x_atom.clone(),

839

396

)))

840

841

530765

842

843

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

844

///

845

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

846

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

847

530765

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

848

530765

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

849

530639

        return Err(RuleNotApplicable);

850

};

851

852

126

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

853

78

        return Err(RuleNotApplicable);

854

};

855

856

48

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

857

        return Err(RuleNotApplicable);

858

};

859

860

48

    let mut out_ranges = vec![];

861

862

48

    for range in ranges {

863

48

        match range {

864

            Range::Single(x) => {

865

                out_ranges.push(*x);

866

                out_ranges.push(*x);

867

868

48

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

869

48

                out_ranges.push(*x);

870

48

                out_ranges.push(*y);

871

48

872

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

873

                return Err(RuleNotApplicable);

874

875

876

877

878

48

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

879

48

        Metadata::new(),

880

48

        atom.clone(),

881

48

        out_ranges,

882

48

)))

883

530765

884

885

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

886

///

887

/// 1. the subject is a list literal

888

/// 2. the subject is one dimensional

889

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

890

530765

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

891

530765

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

892

18478

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

893

48

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

894

48

                Ok((eq, subject, indices))

895

896

954

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

897

954

                Ok((eq, subject, indices))

898

899

17476

            _ => Err(RuleNotApplicable),

900

},

901

8442

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

902

1080

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

903

1080

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

904

905

7362

            _ => Err(RuleNotApplicable),

906

},

907

12824

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

908

2

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

909

910

503843

        _ => Err(RuleNotApplicable),

911

528681

}?;

912

913

2084

    if indices.len() != 1 {

914

        return Err(RuleNotApplicable);

915

2084

916

917

2084

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

918

342

        return Err(RuleNotApplicable);

919

};

920

921

1742

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

922

336

        return Err(RuleNotApplicable);

923

};

924

925

1406

    let mut atom_list = vec![];

926

927

8944

    for elem in list {

928

8944

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

929

162

            return Err(RuleNotApplicable);

930

};

931

932

8782

        atom_list.push(elem);

933

934

935

1244

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

936

1244

        Metadata::new(),

937

1244

        atom_list,

938

1244

        Moo::new(index),

939

1244

        Moo::new(equalto),

940

1244

)))

941

530765

942

943

/// Flattens an implication.

944

///

945

/// ```text

946

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

947

///  ~~>

948

/// __0 -> y,

949

///

950

/// with new top level constraints

951

/// __0 =aux x

952

///

953

/// ```

954

///

955

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

956

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

957

/// an argument:

958

///

959

/// ``` text

960

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

961

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

962

/// ```

963

///

964

/// See [`introduce_reifyimply_ineq_from_imply`].

965

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

966

254710

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

967

254710

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

968

254076

        return Err(RuleNotApplicable);

969

};

970

971

    // flatten x

972

634

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

973

974

434

    let symbols = aux_var_info.symbols();

975

434

    let new_x = aux_var_info.as_expr();

976

977

434

    Ok(Reduction::new(

978

434

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

979

434

        vec![aux_var_info.top_level_expr()],

980

434

        symbols,

981

434

))

982

254710

983

984

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

985

254710

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

986

235160

    if !matches!(

987

254710

        expr,

988

        Expr::SafeDiv(_, _, _)

989

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

990

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

991

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

992

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

993

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

994

            | Expr::Abs(_, _)

995

            | Expr::Neg(_, _)

996

            | Expr::Not(_, _)

997

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

998

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

999

            | Expr::ToInt(_, _)

1000

) {

1001

235160

        return Err(RuleNotApplicable);

1002

19550

1003

1004

19550

    let mut children = expr.children();

1005

1006

19550

    let mut symbols = symbols.clone();

1007

19550

    let mut num_changed = 0;

1008

19550

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

1009

1010

36712

    for child in children.iter_mut() {

1011

36712

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

1012

2642

            symbols = aux_var_info.symbols();

1013

2642

            new_tops.push(aux_var_info.top_level_expr());

1014

2642

            *child = aux_var_info.as_expr();

1015

2642

            num_changed += 1;

1016

34070

1017

1018

1019

19550

    if num_changed == 0 {

1020

16974

        return Err(RuleNotApplicable);

1021

2576

1022

1023

2576

    let expr = expr.with_children(children);

1024

1025

2576

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

1026

254710

1027

1028

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

1029

254710

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

1030

254710

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

1031

243323

        return Err(RuleNotApplicable);

1032

11387

1033

1034

11387

    let children = expr.children();

1035

11387

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

1036

1037

11387

    let mut new_children = VecDeque::new();

1038

11387

    let mut symbols = symbols.clone();

1039

11387

    let mut num_changed = 0;

1040

11387

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

1041

1042

22774

    for child in children {

1043

22774

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

1044

2918

            symbols = aux_var_info.symbols();

1045

2918

            new_tops.push(aux_var_info.top_level_expr());

1046

2918

            new_children.push_back(aux_var_info.as_expr());

1047

2918

            num_changed += 1;

1048

19856

1049

1050

1051

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

1052

11387

    if num_changed != 2 {

1053

11227

        return Err(RuleNotApplicable);

1054

160

1055

1056

160

    let expr = expr.with_children(new_children);

1057

1058

160

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

1059

254710

1060

1061

/// Flattens products containing lists.

1062

///

1063

/// For example,

1064

///

1065

/// ```plain

1066

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

1067

/// ```

1068

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

1069

254710

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

1070

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

1071

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

1072

    // literal in an aux var.

1073

//

1074

    // e.g.

1075

//

1076

    // flatten_generic would do

1077

//

1078

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

1079

//

1080

    // we want to do

1081

//

1082

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

1083

//

1084

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

1085

//

1086

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

1087

//

1088

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

1089

    //  matrix literal.

1090

//

1091

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

1092

1093

254710

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

1094

253414

        return Err(RuleNotApplicable);

1095

};

1096

1097

1296

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

1098

1099

495

    let mut new_factors = vec![];

1100

495

    let mut top_level_exprs = vec![];

1101

495

    let mut symtab = symtab.clone();

1102

1103

948

    for factor in factors {

1104

948

        new_factors.push(Expr::Atomic(

1105

948

            Metadata::new(),

1106

948

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

1107

));

1108

1109

1110

    // have we done anything?

1111

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

1112

402

    if top_level_exprs.is_empty() {

1113

294

        return Err(RuleNotApplicable);

1114

108

1115

1116

108

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

1117

108

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

1118

254710

1119

1120

/// Flattens a matrix literal that contains expressions.

1121

///

1122

/// For example,

1123

///

1124

/// ```plain

1125

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

1126

///

1127

/// where

1128

/// __0 =aux e/2,

1129

/// __1 =aux f*5

1130

/// ```

1131

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

1132

64701

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

1133

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

1134

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

1135

63232

    if matches!(

1136

64701

        expr,

1137

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

1138

) {

1139

1469

        return Err(RuleNotApplicable);

1140

63232

1141

1142

    // flatten any children that are matrix literals

1143

63232

    let mut children = expr.children();

1144

1145

63232

    let mut has_changed = false;

1146

63232

    let mut symbols = symtab.clone();

1147

63232

    let mut top_level_exprs = vec![];

1148

1149

63232

    for child in children.iter_mut() {

1150

        // is this a matrix literal?

1151

//

1152

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

1153

        // matrices, not just those that are lists.

1154

//

1155

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

1156

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

1157

39918

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

1158

37762

            continue;

1159

};

1160

1161

        // flatten expressions

1162

4754

        for e in es.iter_mut() {

1163

4754

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

1164

136

                *e = aux_info.as_expr();

1165

136

                top_level_exprs.push(aux_info.top_level_expr());

1166

136

                symbols = aux_info.symbols();

1167

136

                has_changed = true;

1168

4618

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

1169

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

1170

1171

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

1172

                // inside a matrix list.

1173

//

1174

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

1175

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

1176

//

1177

                // we want to flatten this to

1178

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

1179

1180

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

1181

                    continue;

1182

};

1183

1184

                let categories = e.universe_categories();

1185

1186

                // must contain a decision variable

1187

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

1188

                    continue;

1189

1190

1191

                // must not contain givens or quantified variables

1192

                if categories.contains(&Category::Parameter)

1193

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

1194

1195

                    continue;

1196

1197

1198

                let decl = symbols.gen_find(&domain);

1199

1200

                top_level_exprs.push(Expr::AuxDeclaration(

1201

                    Metadata::new(),

1202

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

1203

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

1204

));

1205

1206

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

1207

1208

                has_changed = true;

1209

4618

1210

1211

1212

2156

        *child = into_matrix_expr!(es;index_domain);

1213

1214

1215

63232

    if has_changed {

1216

74

        Ok(Reduction::new(

1217

74

            expr.with_children(children),

1218

74

            top_level_exprs,

1219

74

            symbols,

1220

74

))

1221

    } else {

1222

63158

        Err(RuleNotApplicable)

1223

1224

64701

1225

1226

/// Converts a Geq to an Ineq

1227

///

1228

/// ```text

1229

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

1230

/// ```

1231

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

1232

170770

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

1233

170770

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

1234

170219

        return Err(RuleNotApplicable);

1235

};

1236

1237

551

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

1238

14

        return Err(RuleNotApplicable);

1239

};

1240

1241

537

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

1242

        return Err(RuleNotApplicable);

1243

};

1244

1245

537

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

1246

537

        meta,

1247

537

        Moo::new(y),

1248

537

        Moo::new(x),

1249

537

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

1250

537

)))

1251

170770

1252

1253

/// Converts a Leq to an Ineq

1254

///

1255

/// ```text

1256

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

1257

/// ```

1258

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

1259

170770

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

1260

170770

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

1261

168946

        return Err(RuleNotApplicable);

1262

};

1263

1264

1824

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

1265

66

        return Err(RuleNotApplicable);

1266

};

1267

1268

1758

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

1269

140

        return Err(RuleNotApplicable);

1270

};

1271

1272

1618

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

1273

1618

        meta,

1274

1618

        Moo::new(x),

1275

1618

        Moo::new(y),

1276

1618

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

1277

1618

)))

1278

170770

1279

1280

// TODO: add this rule for geq

1281

1282

/// ```text

1283

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

1284

/// ```

1285

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

1286

586240

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

1287

586240

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

1288

575161

        return Err(RuleNotApplicable);

1289

};

1290

1291

11079

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

1292

1746

        return Err(RuleNotApplicable);

1293

};

1294

1295

9333

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

1296

8786

        return Err(RuleNotApplicable);

1297

};

1298

1299

547

    let sum_exprs = (*sum_exprs)

1300

547

        .clone()

1301

547

        .unwrap_list()

1302

547

        .ok_or(RuleNotApplicable)?;

1303

3

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

1304

3

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

1305

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

1306

        _ => {

1307

            return Err(RuleNotApplicable);

1308

1309

};

1310

1311

3

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

1312

3

        meta,

1313

3

        Moo::new(x),

1314

3

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

1315

3

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

1316

3

)))

1317

586240

1318

1319

/// ```text

1320

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

1321

/// ```

1322

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

1323

783117

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

1324

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

1325

783117

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

1326

781518

        return Err(RuleNotApplicable);

1327

};

1328

1329

1599

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

1330

132

        return Err(RuleNotApplicable);

1331

};

1332

1333

1467

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

1334

1251

        return Err(RuleNotApplicable);

1335

};

1336

1337

216

    let sum_exprs = Moo::unwrap_or_clone(sum_exprs)

1338

216

        .unwrap_list()

1339

216

        .ok_or(RuleNotApplicable)?;

1340

204

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

1341

84

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

1342

6

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

1343

        _ => {

1344

114

            return Err(RuleNotApplicable);

1345

1346

};

1347

1348

90

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

1349

90

        meta,

1350

90

        Moo::new(x),

1351

90

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

1352

90

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

1353

90

)))

1354

783117

1355

1356

/// Flattening rule for not(bool_lit)

1357

///

1358

/// For some boolean variable x:

1359

/// ```text

1360

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

1361

/// ```

1362

///

1363

/// ## Rationale

1364

///

1365

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

1366

///

1367

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

1368

///

1369

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

1370

/// trivial match).

1371

1372

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

1373

170770

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

1374

170770

    match expr {

1375

376

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

1376

376

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

1377

370

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

1378

1379

370

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

1380

370

                    m.clone(),

1381

370

                    reference,

1382

370

                    Lit::Bool(false),

1383

370

                )));

1384

6

1385

6

            Err(RuleNotApplicable)

1386

1387

170394

        _ => Err(RuleNotApplicable),

1388

1389

170770

1390

1391

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

1392

///

1393

/// ```text

1394

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

1395

/// ```

1396

///

1397

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

1398

/// nested expressions are constraints not variables.

1399

1400

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

1401

144777

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

1402

144773

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

1403

144773

        return Err(RuleNotApplicable);

1404

4

1405

1406

4

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

1407

        unreachable!();

1408

};

1409

1410

4

    extra_check! {

1411

        if !is_flat(e) {

1412

            return Err(RuleNotApplicable);

1413

1414

};

1415

1416

4

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

1417

4

        m.clone(),

1418

4

        e.clone(),

1419

4

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

1420

4

)))

1421

144777

1422

1423

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

1424

///

1425

/// ```text

1426

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

1427

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

1428

///

1429

/// where c is a boolean constraint

1430

/// ```

1431

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

1432

530765

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

1433

530765

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

1434

8442

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

1435

18478

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

1436

14315

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

1437

2044

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

1438

2119

            _ => Err(RuleNotApplicable),

1439

},

1440

1441

503845

        _ => Err(RuleNotApplicable),

1442

505964

}?;

1443

1444

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

1445

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

1446

24801

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

1447

23494

        return Err(RuleNotApplicable);

1448

1307

};

1449

1450

1307

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

1451

530765

1452

1453

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

1454

///

1455

/// ```text

1456

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

1457

///

1458

/// ```

1459

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

1460

530765

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

1461

530765

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

1462

530723

        return Err(RuleNotApplicable);

1463

};

1464

1465

42

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

1466

42

        Metadata::new(),

1467

42

        x.clone(),

1468

42

        y.clone(),

1469

42

)))

1470

530765