Grcov report - minion.rs

1

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

2

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

3

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

4

5

use std::collections::VecDeque;

6

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

7

8

use crate::{

9

    extra_check,

10

    utils::{is_flat, to_aux_var},

11

};

12

use conjure_cp::ast::Moo;

13

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

14

use conjure_cp::{

15

    ast::Metadata,

16

    ast::{

17

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

18

        Typeable,

19

},

20

    into_matrix_expr, matrix_expr,

21

    rule_engine::{

22

        ApplicationError, ApplicationResult, Reduction, register_rule, register_rule_set,

23

},

24

    settings::SolverFamily,

25

};

26

27

use itertools::Itertools;

28

use uniplate::Uniplate;

29

30

use ApplicationError::RuleNotApplicable;

31

32

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

33

5151

    matches!(f, SolverFamily::Minion)

34

5151

});

35

36

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

37

193435

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

38

    // product = val

39

    let val: Atom;

40

    let product: Moo<Expr>;

41

42

193435

    match expr.clone() {

43

10036

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

44

10036

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

45

10036

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

46

47

10036

            if let Some(f) = a_atom {

48

                // val = product

49

7202

                val = f.clone();

50

7202

                product = b;

51

7202

            } else if let Some(f) = b_atom {

52

                // product = val

53

2259

                val = f.clone();

54

2259

                product = a;

55

2259

            } else {

56

575

                return Err(RuleNotApplicable);

57

58

59

3483

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

60

3483

            val = Atom::Reference(reference);

61

3483

            product = e;

62

3483

63

        _ => {

64

179916

            return Err(RuleNotApplicable);

65

66

67

68

12944

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

69

12476

        return Err(RuleNotApplicable);

70

468

71

72

468

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

73

        return Err(RuleNotApplicable);

74

};

75

76

468

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

77

225

    if factors_vec.len() < 2 {

78

        return Err(RuleNotApplicable);

79

225

80

81

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

82

    // Introduce auxvars until it is a binop

83

84

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

85

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

86

87

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

88

225

    let x: Atom = factors_vec

89

225

        .pop()

90

225

        .unwrap()

91

225

        .try_into()

92

225

        .or(Err(RuleNotApplicable))?;

93

94

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

95

153

    let mut y: Atom = factors_vec

96

153

        .pop()

97

153

        .unwrap()

98

153

        .try_into()

99

153

        .or(Err(RuleNotApplicable))?;

100

101

153

    let mut symbols = symbols.clone();

102

153

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

103

104

    // FIXME: add a test for this

105

162

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

106

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

107

        // similar to other introduction rules.

108

9

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

109

110

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

111

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

112

9

        let aux_domain = Expr::Product(

113

9

            Metadata::new(),

114

9

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

115

9

116

9

        .domain_of()

117

9

        .ok_or(ApplicationError::DomainError)?;

118

119

9

        let aux_decl = symbols.gensym(&aux_domain);

120

9

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

121

122

9

        let new_top_expr = Expr::FlatProductEq(

123

9

            Metadata::new(),

124

9

            Moo::new(y),

125

9

            Moo::new(next_factor_atom),

126

9

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

127

9

);

128

129

9

        new_tops.push(new_top_expr);

130

9

        y = aux_var;

131

132

133

153

    Ok(Reduction::new(

134

153

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

135

153

        new_tops,

136

153

        symbols,

137

153

))

138

193435

139

140

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

141

///

142

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

143

/// sum constraints are used.

144

///

145

/// # Details

146

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

147

/// it does its own flattening.

148

///

149

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

150

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

151

/// from a sum:

152

///

153

///```text

154

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

155

///   ~~> flatten_vecop

156

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

157

///

158

///

159

/// __0 =aux 1*a

160

/// __1 =aux 2*b

161

/// __2 =aux 3*c

162

/// ```

163

///

164

/// Therefore, introduce_weightedsumleq_sumgeq does its own flattening.

165

///

166

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

167

/// weighted sums.

168

///

169

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

170

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

171

///

172

///```text

173

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

174

///

175

///   ~> introduce_weightedsumleq_sumgeq

176

///

177

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

178

///

179

/// with new top level constraints

180

///

181

/// __0 = c*d

182

/// __1 = e/f

183

/// __2 = g/h

184

/// ```

185

///

186

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

187

///

188

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

189

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

190

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

191

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

192

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

193

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

194

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

195

///

196

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

197

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

198

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

199

443335

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

200

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

201

    // constraints to make at the end

202

203

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

204

    // elsewhere, as this caused cyclic rule application:

205

//

206

    // ```

207

    // 2*a + b = c

208

//

209

    //   ~~> sumeq_to_inequalities

210

//

211

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

212

//

213

    // --

214

//

215

    // 2*a + b <= c

216

//

217

    //   ~~> flatten_generic

218

    // __1 <=c

219

//

220

    // with new top level constraint

221

//

222

    // 2*a + b =aux __1

223

//

224

    // --

225

//

226

    // 2*a + b =aux __1

227

//

228

    //   ~~> sumeq_to_inequalities

229

//

230

    // LOOP!

231

    // ```

232

    enum EqualityKind {

233

Eq,

234

        Leq,

235

        Geq,

236

237

238

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

239

//

240

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

241

    // on the right hand side.

242

//

243

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

244

29921

    fn match_sum_total(

245

29921

        a: Moo<Expr>,

246

29921

        b: Moo<Expr>,

247

29921

        equality_kind: EqualityKind,

248

29921

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

249

        match (

250

29921

            Moo::unwrap_or_clone(a),

251

29921

            Moo::unwrap_or_clone(b),

252

29921

            equality_kind,

253

) {

254

90

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

255

90

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

256

90

                    .unwrap_list()

257

90

                    .ok_or(RuleNotApplicable)?;

258

9

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

259

260

153

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

261

153

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

262

153

                    .unwrap_list()

263

153

                    .ok_or(RuleNotApplicable)?;

264

63

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

265

266

45

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

267

45

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

268

45

                    .unwrap_list()

269

45

                    .ok_or(RuleNotApplicable)?;

270

27

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

271

272

27

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

273

27

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

274

27

                    .unwrap_list()

275

27

                    .ok_or(RuleNotApplicable)?;

276

18

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

277

278

2835

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

279

2835

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

280

2835

                    .unwrap_list()

281

2835

                    .ok_or(RuleNotApplicable)?;

282

1125

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

283

284

2169

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

285

2169

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

286

2169

                    .unwrap_list()

287

2169

                    .ok_or(RuleNotApplicable)?;

288

432

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

289

290

24602

            _ => Err(RuleNotApplicable),

291

292

29921

293

294

443335

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

295

8377

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

296

1386

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

297

20158

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

298

9370

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

299

9370

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

300

9370

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

301

3983

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

302

3983

                    .unwrap_list()

303

3983

                    .ok_or(RuleNotApplicable)?;

304

2135

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

305

            } else {

306

5387

                Err(RuleNotApplicable)

307

308

309

404044

        _ => Err(RuleNotApplicable),

310

409431

}?;

311

312

3809

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

313

3809

    let mut symtab = symtab.clone();

314

315

    #[allow(clippy::mutable_key_type)]

316

3809

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

317

318

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

319

//

320

7789

    for expr in sum_exprs {

321

7789

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

322

323

6763

        if coeff == 0 {

324

            continue;

325

6763

326

327

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

328

6763

        coefficients_and_vars

329

6763

            .entry(var)

330

6763

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

331

6763

            .or_insert(coeff);

332

333

334

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

335

5551

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

336

337

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

338

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

339

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

340

2783

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

341

2783

        .into_iter()

342

5971

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

343

3563

        .sorted_by(|a, b| {

344

3563

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

345

3563

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

346

3563

            a_atom_str.cmp(&b_atom_str)

347

3563

})

348

5971

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

349

2783

        .unzip();

350

351

2783

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

352

450

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

353

450

            Metadata::new(),

354

450

            Moo::new(matrix_expr![

355

450

                Expr::FlatWeightedSumLeq(

356

450

                    Metadata::new(),

357

450

                    coefficients.clone(),

358

450

                    vars.clone(),

359

450

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

360

450

),

361

450

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

362

450

]),

363

450

),

364

2225

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

365

2225

            Metadata::new(),

366

2225

            Moo::new(matrix_expr![

367

2225

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

368

2225

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

369

2225

]),

370

2225

),

371

        (EqualityKind::Leq, true) => {

372

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

373

374

27

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

375

        (EqualityKind::Geq, true) => {

376

9

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

377

378

72

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

379

};

380

381

2783

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

382

443335

383

384

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

385

///

386

///

387

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

388

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

389

///

390

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

391

///

392

/// # Errors

393

///

394

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

395

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

396

///

397

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

398

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

399

///

400

///

401

7789

fn flatten_weighted_sum_term(

402

7789

    term: Expr,

403

7789

    symtab: &mut SymbolTable,

404

7789

    top_level_exprs: &mut Vec<Expr>,

405

7789

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

406

1350

    match term {

407

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

408

//

409

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

410

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

411

//

412

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

413

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

414

1350

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

415

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

416

//

417

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

418

            // non-list matrix literal.

419

1350

            let factors = Moo::unwrap_or_clone(factors)

420

1350

                .unwrap_list()

421

1350

                .ok_or(RuleNotApplicable)?;

422

423

891

            match factors.as_slice() {

424

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

425

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

426

891

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

427

428

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

429

738

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

430

738

                    *coeff,

431

738

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

432

)),

433

434

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

435

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

436

                    *coeff,

437

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

438

)),

439

440

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

441

442

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

443

444

18

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

445

18

e,

446

18

                    rest @ ..,

447

                ] => {

448

18

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

449

18

                    product_terms.push(e.clone());

450

18

                    let product =

451

18

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

452

                    Ok((

453

18

                        *coeff,

454

18

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

455

))

456

457

458

                // no coefficient:

459

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

460

                _ => {

461

135

                    let product =

462

135

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

463

                    Ok((

464

1,

465

135

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

466

))

467

468

469

470

189

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

471

-1,

472

189

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

473

)),

474

6250

        term => Ok((

475

1,

476

6250

            flatten_expression_to_atom(term, symtab, top_level_exprs)?,

477

)),

478

479

7789

480

481

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

482

/// necessary.

483

///

484

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

485

/// `top_level_exprs`.

486

///

487

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

488

/// returned as-is.

489

///

490

/// # Errors

491

///

492

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

493

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

494

///

495

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

496

///    succeeds when the expression given is atomic.

497

///

498

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

499

///

500

8248

fn flatten_expression_to_atom(

501

8248

    expr: Expr,

502

8248

    symtab: &mut SymbolTable,

503

8248

    top_level_exprs: &mut Vec<Expr>,

504

8248

) -> Result<Atom, ApplicationError> {

505

8248

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

506

6342

        return Ok(atom);

507

1906

508

509

1906

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

510

1330

    *symtab = aux_var_info.symbols();

511

1330

    top_level_exprs.push(aux_var_info.top_level_expr());

512

513

1330

    Ok(aux_var_info.as_atom())

514

8248

515

516

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

517

193435

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

518

    // div = val

519

    let val: Atom;

520

    let div: Moo<Expr>;

521

    let meta: Metadata;

522

523

193435

    match expr.clone() {

524

10036

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

525

10036

            meta = m;

526

527

10036

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

528

10036

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

529

530

10036

            if let Some(f) = a_atom {

531

                // val = div

532

7202

                val = f.clone();

533

7202

                div = b;

534

7202

            } else if let Some(f) = b_atom {

535

                // div = val

536

2259

                val = f.clone();

537

2259

                div = a;

538

2259

            } else {

539

575

                return Err(RuleNotApplicable);

540

541

542

3483

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

543

3483

            meta = m;

544

3483

            val = Atom::Reference(reference);

545

3483

            div = e;

546

3483

547

        _ => {

548

179916

            return Err(RuleNotApplicable);

549

550

551

552

12944

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

553

12575

        return Err(RuleNotApplicable);

554

369

555

556

369

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

557

369

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

558

342

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

559

560

315

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

561

315

        meta.clone_dirty(),

562

315

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

563

315

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

564

315

        Moo::new(val),

565

315

)))

566

193435

567

568

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

569

193435

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

570

    // div = val

571

    let val: Atom;

572

    let div: Moo<Expr>;

573

    let meta: Metadata;

574

575

193435

    match expr.clone() {

576

10036

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

577

10036

            meta = m;

578

10036

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

579

10036

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

580

581

10036

            if let Some(f) = a_atom {

582

                // val = div

583

7202

                val = f.clone();

584

7202

                div = b;

585

7202

            } else if let Some(f) = b_atom {

586

                // div = val

587

2259

                val = f.clone();

588

2259

                div = a;

589

2259

            } else {

590

575

                return Err(RuleNotApplicable);

591

592

593

3483

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

594

3483

            meta = m;

595

3483

            val = Atom::Reference(reference);

596

3483

            div = e;

597

3483

598

        _ => {

599

179916

            return Err(RuleNotApplicable);

600

601

602

603

12944

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

604

12755

        return Err(RuleNotApplicable);

605

189

606

607

189

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

608

189

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

609

189

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

610

611

162

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

612

162

        meta.clone_dirty(),

613

162

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

614

162

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

615

162

        Moo::new(val),

616

162

)))

617

193435

618

619

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

620

320500

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

621

320500

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

622

15254

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

623

15254

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

624

15254

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

625

15254

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

626

15254

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

627

628

15254

            if let Some(a_atom) = a_atom {

629

11054

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

630

4200

            } else if let Some(b_atom) = b_atom {

631

3069

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

632

            } else {

633

1131

                Err(RuleNotApplicable)

634

635

636

637

6201

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

638

6201

            let a = Atom::Reference(reference);

639

6201

            let expr = Moo::unwrap_or_clone(expr);

640

6201

            Ok((a, expr))

641

642

643

299045

        _ => Err(RuleNotApplicable),

644

300176

}?;

645

646

20324

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

647

20234

        return Err(RuleNotApplicable);

648

};

649

650

90

    let y = Moo::unwrap_or_clone(y);

651

90

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

652

653

90

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

654

90

        Metadata::new(),

655

90

        Moo::new(x),

656

90

        Moo::new(y),

657

90

)))

658

320500

659

660

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

661

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

662

193435

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

663

193435

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

664

10036

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

665

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

666

63

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

667

9973

            _ => Err(RuleNotApplicable),

668

},

669

670

3483

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

671

87

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

672

87

                let total_ref_atom = Atom::Reference(total_reference);

673

87

                Ok((a, b, total_ref_atom))

674

675

3396

            _ => Err(RuleNotApplicable),

676

},

677

179916

        _ => Err(RuleNotApplicable),

678

193285

}?;

679

680

150

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

681

150

        .try_into()

682

150

        .or(Err(RuleNotApplicable))?;

683

141

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

684

141

        .try_into()

685

141

        .or(Err(RuleNotApplicable))?;

686

687

141

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

688

141

        Metadata::new(),

689

141

        Moo::new(a),

690

141

        Moo::new(b),

691

141

        Moo::new(total),

692

141

)))

693

193435

694

695

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

696

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

697

193435

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

698

193435

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

699

192382

        return Err(RuleNotApplicable);

700

};

701

702

1053

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

703

704

216

    let atoms = es

705

216

        .into_iter()

706

801

        .map(|e| match e {

707

783

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

708

18

            _ => Err(RuleNotApplicable),

709

801

})

710

216

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

711

712

198

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

713

193435

714

715

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

716

///

717

/// ```text

718

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

719

///

720

///   where x,y are atoms

721

/// ```

722

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

723

320500

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

724

320500

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

725

305246

        return Err(RuleNotApplicable);

726

};

727

728

30481

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

729

30481

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

730

23440

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

731

23269

            return None;

732

};

733

734

171

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

735

736

72

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

737

30481

738

739

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

740

15254

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

741

15182

        return Err(RuleNotApplicable);

742

};

743

744

72

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

745

72

        Metadata::new(),

746

72

        Moo::new(x),

747

72

        Moo::new(y),

748

72

)))

749

320500

750

751

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

752

///

753

/// ```text

754

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

755

///

756

///   where x,y are atoms

757

/// ```

758

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

759

320500

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

760

    // a =aux -b

761

//

762

320500

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

763

314299

        return Err(RuleNotApplicable);

764

};

765

766

6201

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

767

768

6201

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

769

6165

        return Err(RuleNotApplicable);

770

};

771

772

36

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

773

18

        return Err(RuleNotApplicable);

774

};

775

776

18

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

777

18

        Metadata::new(),

778

18

        Moo::new(a),

779

18

        Moo::new(b),

780

18

)))

781

320500

782

783

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

784

///

785

/// ```text

786

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

787

/// where x is atomic, y is atomic

788

///

789

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

790

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

791

/// ```

792

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

793

320500

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

794

320500

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

795

319207

        return Err(RuleNotApplicable);

796

};

797

798

1293

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

799

800

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

801

//

802

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

803

431

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

804

81

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

805

81

            Metadata::new(),

806

81

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

807

81

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

808

81

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

809

81

)))

810

    } else {

811

350

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

812

350

            Metadata::new(),

813

350

            y.clone(),

814

350

            x_atom.clone(),

815

350

)))

816

817

320500

818

819

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

820

///

821

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

822

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

823

320500

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

824

320500

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

825

319933

        return Err(RuleNotApplicable);

826

};

827

828

567

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

829

531

        return Err(RuleNotApplicable);

830

};

831

832

36

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

833

        return Err(RuleNotApplicable);

834

};

835

836

36

    let mut out_ranges = vec![];

837

838

36

    for range in ranges {

839

36

        match range {

840

            Range::Single(x) => {

841

                out_ranges.push(*x);

842

                out_ranges.push(*x);

843

844

36

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

845

36

                out_ranges.push(*x);

846

36

                out_ranges.push(*y);

847

36

848

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

849

                return Err(RuleNotApplicable);

850

851

852

853

854

36

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

855

36

        Metadata::new(),

856

36

        atom.clone(),

857

36

        out_ranges,

858

36

)))

859

320500

860

861

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

862

///

863

/// 1. the subject is a list literal

864

/// 2. the subject is one dimensional

865

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

866

320500

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

867

320500

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

868

15254

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

869

36

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

870

36

                Ok((eq, subject, indices))

871

872

702

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

873

702

                Ok((eq, subject, indices))

874

875

14516

            _ => Err(RuleNotApplicable),

876

},

877

6201

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

878

840

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

879

840

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

880

881

5361

            _ => Err(RuleNotApplicable),

882

},

883

299045

        _ => Err(RuleNotApplicable),

884

318922

}?;

885

886

1578

    if indices.len() != 1 {

887

36

        return Err(RuleNotApplicable);

888

1542

889

890

1542

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

891

180

        return Err(RuleNotApplicable);

892

};

893

894

1362

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

895

270

        return Err(RuleNotApplicable);

896

};

897

898

1092

    let mut atom_list = vec![];

899

900

6696

    for elem in list {

901

6696

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

902

126

            return Err(RuleNotApplicable);

903

};

904

905

6570

        atom_list.push(elem);

906

907

908

966

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

909

966

        Metadata::new(),

910

966

        atom_list,

911

966

        Moo::new(index),

912

966

        Moo::new(equalto),

913

966

)))

914

320500

915

916

/// Flattens an implication.

917

///

918

/// ```text

919

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

920

///  ~~>

921

/// __0 -> y,

922

///

923

/// with new top level constraints

924

/// __0 =aux x

925

///

926

/// ```

927

///

928

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

929

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

930

/// an argument:

931

///

932

/// ``` text

933

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

934

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

935

/// ```

936

///

937

/// See [`introduce_reifyimply_ineq_from_imply`].

938

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

939

193435

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

940

193435

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

941

193076

        return Err(RuleNotApplicable);

942

};

943

944

    // flatten x

945

359

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

946

947

359

    let symbols = aux_var_info.symbols();

948

359

    let new_x = aux_var_info.as_expr();

949

950

359

    Ok(Reduction::new(

951

359

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

952

359

        vec![aux_var_info.top_level_expr()],

953

359

        symbols,

954

359

))

955

193435

956

957

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

958

193435

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

959

176007

    if !matches!(

960

193435

        expr,

961

        Expr::SafeDiv(_, _, _)

962

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

963

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

964

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

965

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

966

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

967

            | Expr::Abs(_, _)

968

            | Expr::Neg(_, _)

969

            | Expr::Not(_, _)

970

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

971

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

972

            | Expr::ToInt(_, _)

973

) {

974

176007

        return Err(RuleNotApplicable);

975

17428

976

977

17428

    let mut children = expr.children();

978

979

17428

    let mut symbols = symbols.clone();

980

17428

    let mut num_changed = 0;

981

17428

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

982

983

33686

    for child in children.iter_mut() {

984

33686

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

985

2705

            symbols = aux_var_info.symbols();

986

2705

            new_tops.push(aux_var_info.top_level_expr());

987

2705

            *child = aux_var_info.as_expr();

988

2705

            num_changed += 1;

989

30981

990

991

992

17428

    if num_changed == 0 {

993

14768

        return Err(RuleNotApplicable);

994

2660

995

996

2660

    let expr = expr.with_children(children);

997

998

2660

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

999

193435

1000

1001

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

1002

193435

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

1003

193435

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

1004

183399

        return Err(RuleNotApplicable);

1005

10036

1006

1007

10036

    let children = expr.children();

1008

10036

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

1009

1010

10036

    let mut new_children = VecDeque::new();

1011

10036

    let mut symbols = symbols.clone();

1012

10036

    let mut num_changed = 0;

1013

10036

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

1014

1015

20072

    for child in children {

1016

20072

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

1017

3859

            symbols = aux_var_info.symbols();

1018

3859

            new_tops.push(aux_var_info.top_level_expr());

1019

3859

            new_children.push_back(aux_var_info.as_expr());

1020

3859

            num_changed += 1;

1021

16213

1022

1023

1024

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

1025

10036

    if num_changed != 2 {

1026

9929

        return Err(RuleNotApplicable);

1027

107

1028

1029

107

    let expr = expr.with_children(new_children);

1030

1031

107

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

1032

193435

1033

1034

/// Flattens products containing lists.

1035

///

1036

/// For example,

1037

///

1038

/// ```plain

1039

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

1040

/// ```

1041

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

1042

193435

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

1043

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

1044

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

1045

    // literal in an aux var.

1046

//

1047

    // e.g.

1048

//

1049

    // flatten_generic would do

1050

//

1051

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

1052

//

1053

    // we want to do

1054

//

1055

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

1056

//

1057

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

1058

//

1059

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

1060

//

1061

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

1062

    //  matrix literal.

1063

//

1064

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

1065

1066

193435

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

1067

191743

        return Err(RuleNotApplicable);

1068

};

1069

1070

1692

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

1071

1072

459

    let mut new_factors = vec![];

1073

459

    let mut top_level_exprs = vec![];

1074

459

    let mut symtab = symtab.clone();

1075

1076

918

    for factor in factors {

1077

918

        new_factors.push(Expr::Atomic(

1078

918

            Metadata::new(),

1079

918

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

1080

));

1081

1082

1083

    // have we done anything?

1084

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

1085

450

    if top_level_exprs.is_empty() {

1086

360

        return Err(RuleNotApplicable);

1087

90

1088

1089

90

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

1090

90

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

1091

193435

1092

1093

/// Flattens a matrix literal that contains expressions.

1094

///

1095

/// For example,

1096

///

1097

/// ```plain

1098

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

1099

///

1100

/// where

1101

/// __0 =aux e/2,

1102

/// __1 =aux f*5

1103

/// ```

1104

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

1105

32612

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

1106

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

1107

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

1108

31450

    if matches!(

1109

32612

        expr,

1110

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

1111

) {

1112

1162

        return Err(RuleNotApplicable);

1113

31450

1114

1115

    // flatten any children that are matrix literals

1116

31450

    let mut children = expr.children();

1117

1118

31450

    let mut has_changed = false;

1119

31450

    let mut symbols = symtab.clone();

1120

31450

    let mut top_level_exprs = vec![];

1121

1122

31450

    for child in children.iter_mut() {

1123

        // is this a matrix literal?

1124

//

1125

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

1126

        // matrices, not just those that are lists.

1127

//

1128

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

1129

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

1130

27848

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

1131

27587

            continue;

1132

};

1133

1134

        // flatten expressions

1135

1188

        for e in es.iter_mut() {

1136

1188

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

1137

99

                *e = aux_info.as_expr();

1138

99

                top_level_exprs.push(aux_info.top_level_expr());

1139

99

                symbols = aux_info.symbols();

1140

99

                has_changed = true;

1141

1089

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

1142

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

1143

1144

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

1145

                // inside a matrix list.

1146

//

1147

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

1148

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

1149

//

1150

                // we want to flatten this to

1151

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

1152

1153

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

1154

                    continue;

1155

};

1156

1157

                let categories = e.universe_categories();

1158

1159

                // must contain a decision variable

1160

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

1161

                    continue;

1162

1163

1164

                // must not contain givens or quantified variables

1165

                if categories.contains(&Category::Parameter)

1166

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

1167

1168

                    continue;

1169

1170

1171

                let decl = symbols.gensym(&domain);

1172

1173

                top_level_exprs.push(Expr::AuxDeclaration(

1174

                    Metadata::new(),

1175

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

1176

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

1177

));

1178

1179

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

1180

1181

                has_changed = true;

1182

1089

1183

1184

1185

261

        *child = into_matrix_expr!(es;index_domain);

1186

1187

1188

31450

    if has_changed {

1189

54

        Ok(Reduction::new(

1190

54

            expr.with_children(children),

1191

54

            top_level_exprs,

1192

54

            symbols,

1193

54

))

1194

    } else {

1195

31396

        Err(RuleNotApplicable)

1196

1197

32612

1198

1199

/// Converts a Geq to an Ineq

1200

///

1201

/// ```text

1202

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

1203

/// ```

1204

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

1205

127961

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

1206

127961

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

1207

127466

        return Err(RuleNotApplicable);

1208

};

1209

1210

495

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

1211

        return Err(RuleNotApplicable);

1212

};

1213

1214

495

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

1215

        return Err(RuleNotApplicable);

1216

};

1217

1218

495

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

1219

495

        meta.clone_dirty(),

1220

495

        Moo::new(y),

1221

495

        Moo::new(x),

1222

495

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

1223

495

)))

1224

127961

1225

1226

/// Converts a Leq to an Ineq

1227

///

1228

/// ```text

1229

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

1230

/// ```

1231

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

1232

127961

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

1233

127961

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

1234

126325

        return Err(RuleNotApplicable);

1235

};

1236

1237

1636

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

1238

        return Err(RuleNotApplicable);

1239

};

1240

1241

1636

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

1242

        return Err(RuleNotApplicable);

1243

};

1244

1245

1636

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

1246

1636

        meta.clone_dirty(),

1247

1636

        Moo::new(x),

1248

1636

        Moo::new(y),

1249

1636

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

1250

1636

)))

1251

127961

1252

1253

// TODO: add this rule for geq

1254

1255

/// ```text

1256

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

1257

/// ```

1258

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

1259

364086

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

1260

364086

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

1261

356048

        return Err(RuleNotApplicable);

1262

};

1263

1264

8038

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

1265

288

        return Err(RuleNotApplicable);

1266

};

1267

1268

7750

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

1269

7651

        return Err(RuleNotApplicable);

1270

};

1271

1272

99

    let sum_exprs = (*sum_exprs)

1273

99

        .clone()

1274

99

        .unwrap_list()

1275

99

        .ok_or(RuleNotApplicable)?;

1276

9

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

1277

9

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

1278

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

1279

        _ => {

1280

            return Err(RuleNotApplicable);

1281

1282

};

1283

1284

9

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

1285

9

        meta.clone_dirty(),

1286

9

        Moo::new(x),

1287

9

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

1288

9

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

1289

9

)))

1290

364086

1291

1292

/// ```text

1293

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

1294

/// ```

1295

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

1296

482767

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

1297

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

1298

482767

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

1299

481273

        return Err(RuleNotApplicable);

1300

};

1301

1302

1494

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

1303

171

        return Err(RuleNotApplicable);

1304

};

1305

1306

1323

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

1307

1188

        return Err(RuleNotApplicable);

1308

};

1309

1310

135

    let sum_exprs = Moo::unwrap_or_clone(sum_exprs)

1311

135

        .unwrap_list()

1312

135

        .ok_or(RuleNotApplicable)?;

1313

117

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

1314

99

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

1315

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

1316

        _ => {

1317

18

            return Err(RuleNotApplicable);

1318

1319

};

1320

1321

99

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

1322

99

        meta.clone_dirty(),

1323

99

        Moo::new(x),

1324

99

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

1325

99

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

1326

99

)))

1327

482767

1328

1329

/// Flattening rule for not(bool_lit)

1330

///

1331

/// For some boolean variable x:

1332

/// ```text

1333

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

1334

/// ```

1335

///

1336

/// ## Rationale

1337

///

1338

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

1339

///

1340

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

1341

///

1342

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

1343

/// trivial match).

1344

1345

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

1346

127961

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

1347

127961

    match expr {

1348

135

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

1349

135

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

1350

135

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

1351

1352

135

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

1353

135

                    m.clone_dirty(),

1354

135

                    reference,

1355

135

                    Lit::Bool(false),

1356

135

                )));

1357

1358

            Err(RuleNotApplicable)

1359

1360

127826

        _ => Err(RuleNotApplicable),

1361

1362

127961

1363

1364

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

1365

///

1366

/// ```text

1367

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

1368

/// ```

1369

///

1370

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

1371

/// nested expressions are constraints not variables.

1372

1373

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

1374

110937

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

1375

110937

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

1376

110937

        return Err(RuleNotApplicable);

1377

1378

1379

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

1380

        unreachable!();

1381

};

1382

1383

    extra_check! {

1384

        if !is_flat(e) {

1385

            return Err(RuleNotApplicable);

1386

1387

};

1388

1389

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

1390

        m.clone(),

1391

        e.clone(),

1392

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

1393

)))

1394

110937

1395

1396

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

1397

///

1398

/// ```text

1399

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

1400

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

1401

///

1402

/// where c is a boolean constraint

1403

/// ```

1404

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

1405

320500

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

1406

320500

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

1407

6201

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

1408

15254

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

1409

11054

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

1410

3069

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

1411

1131

            _ => Err(RuleNotApplicable),

1412

},

1413

1414

299045

        _ => Err(RuleNotApplicable),

1415

300176

}?;

1416

1417

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

1418

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

1419

20324

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

1420

18949

        return Err(RuleNotApplicable);

1421

1375

};

1422

1423

1375

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

1424

320500

1425

1426

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

1427

///

1428

/// ```text

1429

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

1430

///

1431

/// ```

1432

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

1433

320500

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

1434

320500

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

1435

320473

        return Err(RuleNotApplicable);

1436

};

1437

1438

27

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

1439

27

        Metadata::new(),

1440

27

        x.clone(),

1441

27

        y.clone(),

1442

27

)))

1443

320500