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

    solver::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

    matches!(f, SolverFamily::Minion)

34

});

35

36

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

37

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

38

    // product = val

39

    let val: Atom;

40

    let product: Moo<Expr>;

41

42

    match expr.clone() {

43

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

44

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

45

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

46

47

            if let Some(f) = a_atom {

48

                // val = product

49

                val = f.clone();

50

                product = b;

51

            } else if let Some(f) = b_atom {

52

                // product = val

53

                val = f.clone();

54

                product = a;

55

            } else {

56

                return Err(RuleNotApplicable);

57

58

59

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

60

            val = Atom::Reference(reference);

61

            product = e;

62

63

        _ => {

64

            return Err(RuleNotApplicable);

65

66

67

68

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

69

        return Err(RuleNotApplicable);

70

71

72

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

73

        return Err(RuleNotApplicable);

74

};

75

76

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

77

    if factors_vec.len() < 2 {

78

        return Err(RuleNotApplicable);

79

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

    let x: Atom = factors_vec

89

        .pop()

90

        .unwrap()

91

        .try_into()

92

        .or(Err(RuleNotApplicable))?;

93

94

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

95

    let mut y: Atom = factors_vec

96

        .pop()

97

        .unwrap()

98

        .try_into()

99

        .or(Err(RuleNotApplicable))?;

100

101

    let mut symbols = symbols.clone();

102

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

103

104

    // FIXME: add a test for this

105

    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

        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

        let aux_domain = Expr::Product(

113

            Metadata::new(),

114

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

115

116

        .domain_of()

117

        .ok_or(ApplicationError::DomainError)?;

118

119

        let aux_decl = symbols.gensym(&aux_domain);

120

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

121

122

        let new_top_expr = Expr::FlatProductEq(

123

            Metadata::new(),

124

            Moo::new(y),

125

            Moo::new(next_factor_atom),

126

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

127

);

128

129

        new_tops.push(new_top_expr);

130

        y = aux_var;

131

132

133

    Ok(Reduction::new(

134

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

135

        new_tops,

136

        symbols,

137

))

138

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

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

    fn match_sum_total(

245

        a: Moo<Expr>,

246

        b: Moo<Expr>,

247

        equality_kind: EqualityKind,

248

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

249

        match (

250

            Moo::unwrap_or_clone(a),

251

            Moo::unwrap_or_clone(b),

252

            equality_kind,

253

) {

254

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

255

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

256

                    .unwrap_list()

257

                    .ok_or(RuleNotApplicable)?;

258

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

259

260

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

261

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

262

                    .unwrap_list()

263

                    .ok_or(RuleNotApplicable)?;

264

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

265

266

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

267

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

268

                    .unwrap_list()

269

                    .ok_or(RuleNotApplicable)?;

270

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

271

272

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

273

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

274

                    .unwrap_list()

275

                    .ok_or(RuleNotApplicable)?;

276

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

277

278

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

279

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

280

                    .unwrap_list()

281

                    .ok_or(RuleNotApplicable)?;

282

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

283

284

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

285

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

286

                    .unwrap_list()

287

                    .ok_or(RuleNotApplicable)?;

288

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

289

290

            _ => Err(RuleNotApplicable),

291

292

293

294

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

295

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

296

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

297

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

298

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

299

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

300

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

301

                let sum_terms = Moo::unwrap_or_clone(sum_terms)

302

                    .unwrap_list()

303

                    .ok_or(RuleNotApplicable)?;

304

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

305

            } else {

306

                Err(RuleNotApplicable)

307

308

309

        _ => Err(RuleNotApplicable),

310

}?;

311

312

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

313

    let mut symtab = symtab.clone();

314

315

    #[allow(clippy::mutable_key_type)]

316

    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

    for expr in sum_exprs {

321

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

322

323

        if coeff == 0 {

324

            continue;

325

326

327

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

328

        coefficients_and_vars

329

            .entry(var)

330

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

331

            .or_insert(coeff);

332

333

334

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

335

    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

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

341

        .into_iter()

342

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

343

        .sorted_by(|a, b| {

344

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

345

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

346

            a_atom_str.cmp(&b_atom_str)

347

})

348

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

349

        .unzip();

350

351

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

352

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

353

            Metadata::new(),

354

            Moo::new(matrix_expr![

355

                Expr::FlatWeightedSumLeq(

356

                    Metadata::new(),

357

                    coefficients.clone(),

358

                    vars.clone(),

359

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

360

),

361

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

362

]),

363

),

364

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

365

            Metadata::new(),

366

            Moo::new(matrix_expr![

367

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

368

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

369

]),

370

),

371

        (EqualityKind::Leq, true) => {

372

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

373

374

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

375

        (EqualityKind::Geq, true) => {

376

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

377

378

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

379

};

380

381

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

382

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

fn flatten_weighted_sum_term(

402

    term: Expr,

403

    symtab: &mut SymbolTable,

404

    top_level_exprs: &mut Vec<Expr>,

405

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

406

    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

        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

            let factors = Moo::unwrap_or_clone(factors)

420

                .unwrap_list()

421

                .ok_or(RuleNotApplicable)?;

422

423

            match factors.as_slice() {

424

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

425

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

426

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

427

428

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

429

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

430

                    *coeff,

431

                    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

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

445

e,

446

                    rest @ ..,

447

                ] => {

448

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

449

                    product_terms.push(e.clone());

450

                    let product =

451

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

452

                    Ok((

453

                        *coeff,

454

                        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

                    let product =

462

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

463

                    Ok((

464

1,

465

                        flatten_expression_to_atom(product, symtab, top_level_exprs)?,

466

))

467

468

469

470

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

471

-1,

472

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

473

)),

474

        term => Ok((

475

1,

476

            flatten_expression_to_atom(term, symtab, top_level_exprs)?,

477

)),

478

479

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

fn flatten_expression_to_atom(

501

    expr: Expr,

502

    symtab: &mut SymbolTable,

503

    top_level_exprs: &mut Vec<Expr>,

504

) -> Result<Atom, ApplicationError> {

505

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

506

        return Ok(atom);

507

508

509

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

510

    *symtab = aux_var_info.symbols();

511

    top_level_exprs.push(aux_var_info.top_level_expr());

512

513

    Ok(aux_var_info.as_atom())

514

515

516

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

517

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

    match expr.clone() {

524

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

525

            meta = m;

526

527

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

528

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

529

530

            if let Some(f) = a_atom {

531

                // val = div

532

                val = f.clone();

533

                div = b;

534

            } else if let Some(f) = b_atom {

535

                // div = val

536

                val = f.clone();

537

                div = a;

538

            } else {

539

                return Err(RuleNotApplicable);

540

541

542

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

543

            meta = m;

544

            val = Atom::Reference(reference);

545

            div = e;

546

547

        _ => {

548

            return Err(RuleNotApplicable);

549

550

551

552

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

553

        return Err(RuleNotApplicable);

554

555

556

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

557

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

558

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

559

560

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

561

        meta.clone_dirty(),

562

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

563

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

564

        Moo::new(val),

565

)))

566

567

568

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

569

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

    match expr.clone() {

576

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

577

            meta = m;

578

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

579

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

580

581

            if let Some(f) = a_atom {

582

                // val = div

583

                val = f.clone();

584

                div = b;

585

            } else if let Some(f) = b_atom {

586

                // div = val

587

                val = f.clone();

588

                div = a;

589

            } else {

590

                return Err(RuleNotApplicable);

591

592

593

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

594

            meta = m;

595

            val = Atom::Reference(reference);

596

            div = e;

597

598

        _ => {

599

            return Err(RuleNotApplicable);

600

601

602

603

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

604

        return Err(RuleNotApplicable);

605

606

607

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

608

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

609

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

610

611

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

612

        meta.clone_dirty(),

613

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

614

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

615

        Moo::new(val),

616

)))

617

618

619

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

620

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

621

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

622

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

623

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

624

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

625

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

626

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

627

628

            if let Some(a_atom) = a_atom {

629

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

630

            } else if let Some(b_atom) = b_atom {

631

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

632

            } else {

633

                Err(RuleNotApplicable)

634

635

636

637

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

638

            let a = Atom::Reference(reference);

639

            let expr = Moo::unwrap_or_clone(expr);

640

            Ok((a, expr))

641

642

643

        _ => Err(RuleNotApplicable),

644

}?;

645

646

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

647

        return Err(RuleNotApplicable);

648

};

649

650

    let y = Moo::unwrap_or_clone(y);

651

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

652

653

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

654

        Metadata::new(),

655

        Moo::new(x),

656

        Moo::new(y),

657

)))

658

659

660

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

661

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

662

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

663

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

664

        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

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

667

            _ => Err(RuleNotApplicable),

668

},

669

670

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

671

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

672

                let total_ref_atom = Atom::Reference(total_reference);

673

                Ok((a, b, total_ref_atom))

674

675

            _ => Err(RuleNotApplicable),

676

},

677

        _ => Err(RuleNotApplicable),

678

}?;

679

680

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

681

        .try_into()

682

        .or(Err(RuleNotApplicable))?;

683

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

684

        .try_into()

685

        .or(Err(RuleNotApplicable))?;

686

687

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

688

        Metadata::new(),

689

        Moo::new(a),

690

        Moo::new(b),

691

        Moo::new(total),

692

)))

693

694

695

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

696

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

697

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

698

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

699

        return Err(RuleNotApplicable);

700

};

701

702

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

703

704

    let atoms = es

705

        .into_iter()

706

        .map(|e| match e {

707

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

708

            _ => Err(RuleNotApplicable),

709

})

710

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

711

712

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

713

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

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

724

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

725

        return Err(RuleNotApplicable);

726

};

727

728

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

729

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

730

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

731

            return None;

732

};

733

734

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

735

736

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

737

738

739

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

740

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

741

        return Err(RuleNotApplicable);

742

};

743

744

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

745

        Metadata::new(),

746

        Moo::new(x),

747

        Moo::new(y),

748

)))

749

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

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

760

    // a =aux -b

761

//

762

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

763

        return Err(RuleNotApplicable);

764

};

765

766

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

767

768

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

769

        return Err(RuleNotApplicable);

770

};

771

772

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

773

        return Err(RuleNotApplicable);

774

};

775

776

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

777

        Metadata::new(),

778

        Moo::new(a),

779

        Moo::new(b),

780

)))

781

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

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

794

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

795

        return Err(RuleNotApplicable);

796

};

797

798

    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

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

804

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

805

            Metadata::new(),

806

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

807

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

808

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

809

)))

810

    } else {

811

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

812

            Metadata::new(),

813

            y.clone(),

814

            x_atom.clone(),

815

)))

816

817

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

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

824

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

825

        return Err(RuleNotApplicable);

826

};

827

828

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

829

        return Err(RuleNotApplicable);

830

};

831

832

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

833

        return Err(RuleNotApplicable);

834

};

835

836

    let mut out_ranges = vec![];

837

838

    for range in ranges {

839

        match range {

840

            Range::Single(x) => {

841

                out_ranges.push(*x);

842

                out_ranges.push(*x);

843

844

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

845

                out_ranges.push(*x);

846

                out_ranges.push(*y);

847

848

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

849

                return Err(RuleNotApplicable);

850

851

852

853

854

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

855

        Metadata::new(),

856

        atom.clone(),

857

        out_ranges,

858

)))

859

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

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

867

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

868

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

869

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

870

                Ok((eq, subject, indices))

871

872

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

873

                Ok((eq, subject, indices))

874

875

            _ => Err(RuleNotApplicable),

876

},

877

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

878

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

879

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

880

881

            _ => Err(RuleNotApplicable),

882

},

883

        _ => Err(RuleNotApplicable),

884

}?;

885

886

    if indices.len() != 1 {

887

        return Err(RuleNotApplicable);

888

889

890

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

891

        return Err(RuleNotApplicable);

892

};

893

894

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

895

        return Err(RuleNotApplicable);

896

};

897

898

    let mut atom_list = vec![];

899

900

    for elem in list {

901

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

902

            return Err(RuleNotApplicable);

903

};

904

905

        atom_list.push(elem);

906

907

908

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

909

        Metadata::new(),

910

        atom_list,

911

        Moo::new(index),

912

        Moo::new(equalto),

913

)))

914

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

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

940

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

941

        return Err(RuleNotApplicable);

942

};

943

944

    // flatten x

945

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

946

947

    let symbols = aux_var_info.symbols();

948

    let new_x = aux_var_info.as_expr();

949

950

    Ok(Reduction::new(

951

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

952

        vec![aux_var_info.top_level_expr()],

953

        symbols,

954

))

955

956

957

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

958

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

959

    if !matches!(

960

        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

        return Err(RuleNotApplicable);

975

976

977

    let mut children = expr.children();

978

979

    let mut symbols = symbols.clone();

980

    let mut num_changed = 0;

981

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

982

983

    for child in children.iter_mut() {

984

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

985

            symbols = aux_var_info.symbols();

986

            new_tops.push(aux_var_info.top_level_expr());

987

            *child = aux_var_info.as_expr();

988

            num_changed += 1;

989

990

991

992

    if num_changed == 0 {

993

        return Err(RuleNotApplicable);

994

995

996

    let expr = expr.with_children(children);

997

998

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

999

1000

1001

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

1002

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

1003

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

1004

        return Err(RuleNotApplicable);

1005

1006

1007

    let children = expr.children();

1008

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

1009

1010

    let mut new_children = VecDeque::new();

1011

    let mut symbols = symbols.clone();

1012

    let mut num_changed = 0;

1013

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

1014

1015

    for child in children {

1016

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

1017

            symbols = aux_var_info.symbols();

1018

            new_tops.push(aux_var_info.top_level_expr());

1019

            new_children.push_back(aux_var_info.as_expr());

1020

            num_changed += 1;

1021

1022

1023

1024

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

1025

    if num_changed != 2 {

1026

        return Err(RuleNotApplicable);

1027

1028

1029

    let expr = expr.with_children(new_children);

1030

1031

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

1032

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

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

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

1067

        return Err(RuleNotApplicable);

1068

};

1069

1070

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

1071

1072

    let mut new_factors = vec![];

1073

    let mut top_level_exprs = vec![];

1074

    let mut symtab = symtab.clone();

1075

1076

    for factor in factors {

1077

        new_factors.push(Expr::Atomic(

1078

            Metadata::new(),

1079

            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

    if top_level_exprs.is_empty() {

1086

        return Err(RuleNotApplicable);

1087

1088

1089

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

1090

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

1091

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

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

    if matches!(

1109

        expr,

1110

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

1111

) {

1112

        return Err(RuleNotApplicable);

1113

1114

1115

    // flatten any children that are matrix literals

1116

    let mut children = expr.children();

1117

1118

    let mut has_changed = false;

1119

    let mut symbols = symtab.clone();

1120

    let mut top_level_exprs = vec![];

1121

1122

    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

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

1131

            continue;

1132

};

1133

1134

        // flatten expressions

1135

        for e in es.iter_mut() {

1136

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

1137

                *e = aux_info.as_expr();

1138

                top_level_exprs.push(aux_info.top_level_expr());

1139

                symbols = aux_info.symbols();

1140

                has_changed = true;

1141

            } 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

1183

1184

1185

        *child = into_matrix_expr!(es;index_domain);

1186

1187

1188

    if has_changed {

1189

        Ok(Reduction::new(

1190

            expr.with_children(children),

1191

            top_level_exprs,

1192

            symbols,

1193

))

1194

    } else {

1195

        Err(RuleNotApplicable)

1196

1197

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

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

1206

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

1207

        return Err(RuleNotApplicable);

1208

};

1209

1210

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

1211

        return Err(RuleNotApplicable);

1212

};

1213

1214

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

1215

        return Err(RuleNotApplicable);

1216

};

1217

1218

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

1219

        meta.clone_dirty(),

1220

        Moo::new(y),

1221

        Moo::new(x),

1222

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

1223

)))

1224

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

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

1233

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

1234

        return Err(RuleNotApplicable);

1235

};

1236

1237

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

1238

        return Err(RuleNotApplicable);

1239

};

1240

1241

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

1242

        return Err(RuleNotApplicable);

1243

};

1244

1245

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

1246

        meta.clone_dirty(),

1247

        Moo::new(x),

1248

        Moo::new(y),

1249

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

1250

)))

1251

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

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

1260

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

1261

        return Err(RuleNotApplicable);

1262

};

1263

1264

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

1265

        return Err(RuleNotApplicable);

1266

};

1267

1268

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

1269

        return Err(RuleNotApplicable);

1270

};

1271

1272

    let sum_exprs = (*sum_exprs)

1273

        .clone()

1274

        .unwrap_list()

1275

        .ok_or(RuleNotApplicable)?;

1276

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

1277

        [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

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

1285

        meta.clone_dirty(),

1286

        Moo::new(x),

1287

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

1288

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

1289

)))

1290

1291

1292

/// ```text

1293

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

1294

/// ```

1295

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

1296

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

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

1299

        return Err(RuleNotApplicable);

1300

};

1301

1302

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

1303

        return Err(RuleNotApplicable);

1304

};

1305

1306

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

1307

        return Err(RuleNotApplicable);

1308

};

1309

1310

    let sum_exprs = Moo::unwrap_or_clone(sum_exprs)

1311

        .unwrap_list()

1312

        .ok_or(RuleNotApplicable)?;

1313

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

1314

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

1315

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

1316

        _ => {

1317

            return Err(RuleNotApplicable);

1318

1319

};

1320

1321

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

1322

        meta.clone_dirty(),

1323

        Moo::new(x),

1324

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

1325

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

1326

)))

1327

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

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

1347

    match expr {

1348

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

1349

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

1350

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

1351

1352

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

1353

                    m.clone_dirty(),

1354

                    reference,

1355

                    Lit::Bool(false),

1356

                )));

1357

1358

            Err(RuleNotApplicable)

1359

1360

        _ => Err(RuleNotApplicable),

1361

1362

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

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

1375

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

1376

        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

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

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

1406

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

1407

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

1408

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

1409

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

1410

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

1411

            _ => Err(RuleNotApplicable),

1412

},

1413

1414

        _ => Err(RuleNotApplicable),

1415

}?;

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

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

1420

        return Err(RuleNotApplicable);

1421

};

1422

1423

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

1424

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

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

1434

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

1435

        return Err(RuleNotApplicable);

1436

};

1437

1438

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

1439

        Metadata::new(),

1440

        x.clone(),

1441

        y.clone(),

1442

)))

1443