Grcov report - minion.rs

1

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

2

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

3

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

4

5

use std::convert::TryInto;

6

use std::rc::Rc;

7

8

use crate::ast::Declaration;

9

use crate::ast::{Atom, Domain, Expression as Expr, Literal as Lit, ReturnType, SymbolTable};

10

11

use crate::matrix_expr;

12

use crate::metadata::Metadata;

13

use crate::rule_engine::{

14

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

15

};

16

use crate::rules::extra_check;

17

18

use crate::solver::SolverFamily;

19

use itertools::Itertools;

20

use uniplate::Uniplate;

21

use ApplicationError::*;

22

23

use super::utils::{is_flat, to_aux_var};

24

25

register_rule_set!("Minion", ("Base"), (SolverFamily::Minion));

26

27

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

28

122598

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

29

122598

    // product = val

30

122598

    let val: Atom;

31

122598

    let product: Expr;

32

122598

33

122598

    match expr.clone() {

34

6462

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

35

6462

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

36

6462

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

37

38

6462

            if let Some(f) = a_atom {

39

5508

                // val = product

40

5508

                val = f.clone();

41

5508

                product = *b;

42

5508

            } else if let Some(f) = b_atom {

43

936

                // product = val

44

936

                val = f.clone();

45

936

                product = *a;

46

936

            } else {

47

18

                return Err(RuleNotApplicable);

48

49

50

792

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

51

792

            val = name.into();

52

792

            product = *e;

53

792

54

        _ => {

55

115344

            return Err(RuleNotApplicable);

56

57

58

59

7236

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

60

7164

        return Err(RuleNotApplicable);

61

72

62

63

72

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

64

        return Err(RuleNotApplicable);

65

};

66

67

72

    if factors.len() < 2 {

68

        return Err(RuleNotApplicable);

69

72

70

71

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

72

    // Introduce auxvars until it is a binop

73

74

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

75

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

76

77

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

78

72

    let x: Atom = factors

79

72

        .pop()

80

72

        .unwrap()

81

72

        .try_into()

82

72

        .or(Err(RuleNotApplicable))?;

83

84

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

85

54

    let mut y: Atom = factors

86

54

        .pop()

87

54

        .unwrap()

88

54

        .try_into()

89

54

        .or(Err(RuleNotApplicable))?;

90

91

54

    let mut symbols = symbols.clone();

92

54

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

93

94

    // FIXME: add a test for this

95

72

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

96

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

97

        // similar to other introduction rules.

98

18

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

99

100

18

        let aux_var = symbols.gensym();

101

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

102

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

103

18

        let aux_domain = Expr::Product(Metadata::new(), vec![y.clone().into(), next_factor])

104

18

            .domain_of(&symbols)

105

18

            .ok_or(ApplicationError::DomainError)?;

106

107

18

        symbols.insert(Rc::new(Declaration::new_var(aux_var.clone(), aux_domain)));

108

18

109

18

        let new_top_expr =

110

18

            Expr::FlatProductEq(Metadata::new(), y, next_factor_atom, aux_var.clone().into());

111

18

112

18

        new_tops.push(new_top_expr);

113

18

        y = aux_var.into();

114

115

116

54

    Ok(Reduction::new(

117

54

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

118

54

        new_tops,

119

54

        symbols,

120

54

))

121

122598

122

123

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

124

///

125

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

126

/// sum constraints are used.

127

///

128

/// # Details

129

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

130

/// it does its own flattening.

131

///

132

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

133

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

134

/// from a sum:

135

///

136

///```text

137

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

138

///   ~~> flatten_vecop

139

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

140

///

141

/// with new top level constraints

142

///

143

/// __0 =aux 1*a

144

/// __1 =aux 2*b

145

/// __2 =aux 3*c

146

/// ```

147

///

148

/// Therefore, introduce_weightedsumleq_sumgeq does its own flattening.

149

///

150

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

151

/// weighted sums.

152

///

153

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

154

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

155

///

156

///```text

157

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

158

///

159

///   ~> introduce_weightedsumleq_sumgeq

160

///

161

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

162

///

163

/// with new top level constraints

164

///

165

/// __0 = c*d

166

/// __1 = e/f

167

/// __2 = g/h

168

/// ```

169

///

170

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

171

///

172

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

173

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

174

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

175

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

176

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

177

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

178

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

179

///

180

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

181

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

182

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

183

279144

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

184

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

185

    // constraints to make at the end

186

187

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

188

    // elsewhere, as this caused cyclic rule application:

189

//

190

    // ```

191

    // 2*a + b = c

192

//

193

    //   ~~> sumeq_to_inequalities

194

//

195

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

196

//

197

    // --

198

//

199

    // 2*a + b <= c

200

//

201

    //   ~~> flatten_generic

202

    // __1 <=c

203

//

204

    // with new top level constraint

205

//

206

    // 2*a + b =aux __1

207

//

208

    // --

209

//

210

    // 2*a + b =aux __1

211

//

212

    //   ~~> sumeq_to_inequalities

213

//

214

    // LOOP!

215

    // ```

216

    enum EqualityKind {

217

Eq,

218

        Leq,

219

        Geq,

220

221

222

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

223

//

224

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

225

    // on the right hand side.

226

//

227

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

228

35964

    fn match_sum_total(

229

35964

        a: Expr,

230

35964

        b: Expr,

231

35964

        equality_kind: EqualityKind,

232

35964

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

233

35964

        match (a, b, equality_kind) {

234

180

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

235

180

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

236

237

126

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

238

126

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

239

240

72

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

241

72

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

242

243

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

244

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

245

246

270

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

247

270

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

248

249

144

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

250

144

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

251

252

35172

            _ => Err(RuleNotApplicable),

253

254

35964

255

256

279144

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

257

14886

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

258

1224

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

259

19854

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

260

2682

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

261

2682

            let total: Atom = n.into();

262

2682

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

263

90

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

264

            } else {

265

2592

                Err(RuleNotApplicable)

266

267

268

240498

        _ => Err(RuleNotApplicable),

269

243090

}?;

270

271

882

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

272

882

    let mut symbols = symbols.clone();

273

882

274

882

    let mut coefficients: Vec<Lit> = vec![];

275

882

    let mut vars: Vec<Atom> = vec![];

276

882

277

882

    // if all coefficients are 1, use normal sum rule instead

278

882

    let mut found_non_one_coeff = false;

279

280

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

281

2826

    for expr in sum_exprs {

282

1944

        let (coeff, var): (Lit, Atom) = match expr {

283

            // atom: v ~> 1*v

284

1422

            Expr::Atomic(_, atom) => (Lit::Int(1), atom),

285

286

            // assuming normalisation / partial eval, literal will be first term

287

288

            // weighted sum term: c * e.

289

            // e can either be an atom, the rest of the product to be flattened, or an other expression that needs

290

            // flattening

291

270

            Expr::Product(_, factors)

292

270

                if factors.len() > 1 && matches!(factors[0], Expr::Atomic(_, Atom::Literal(_))) =>

293

270

294

270

                match &factors[..] {

295

                    // c * <atom>

296

234

                    [Expr::Atomic(_, Atom::Literal(c)), Expr::Atomic(_, atom)] => {

297

234

                        (c.clone(), atom.clone())

298

299

300

                    // c * <some non-flat expression>

301

18

                    [Expr::Atomic(_, Atom::Literal(c)), e1] => {

302

18

                        #[allow(clippy::unwrap_used)] // aux var failing is a bug

303

18

                        let aux_var_info = to_aux_var(e1, &symbols).unwrap();

304

18

305

18

                        symbols = aux_var_info.symbols();

306

18

                        let var = aux_var_info.as_atom();

307

18

                        new_top_exprs.push(aux_var_info.top_level_expr());

308

18

                        (c.clone(), var)

309

310

311

                    // c * a * b * c * ...

312

18

                    [Expr::Atomic(_, Atom::Literal(c)), ref rest @ ..] => {

313

18

                        let e1 = Expr::Product(Metadata::new(), rest.to_vec());

314

18

315

18

                        #[allow(clippy::unwrap_used)] // aux var failing is a bug

316

18

                        let aux_var_info = to_aux_var(&e1, &symbols).unwrap();

317

18

318

18

                        symbols = aux_var_info.symbols();

319

18

                        let var = aux_var_info.as_atom();

320

18

                        new_top_exprs.push(aux_var_info.top_level_expr());

321

18

                        (c.clone(), var)

322

323

324

                    _ => unreachable!(),

325

326

327

328

            // negated terms: `-e ~> -1*e`

329

//

330

            // flatten e if non-atomic

331

108

            Expr::Neg(_, e) => {

332

                // needs flattening

333

108

                let v: Atom = if let Some(aux_var_info) = to_aux_var(&e, &symbols) {

334

18

                    symbols = aux_var_info.symbols();

335

18

                    new_top_exprs.push(aux_var_info.top_level_expr());

336

18

                    aux_var_info.as_atom()

337

                } else {

338

                    // if we can't flatten it, it must be an atom!

339

                    #[allow(clippy::unwrap_used)]

340

90

                    e.try_into().unwrap()

341

};

342

343

108

                (Lit::Int(-1), v)

344

345

346

            // flatten non-flat terms without coefficients: e1 ~> (1,__0)

347

//

348

            // includes products without coefficients.

349

288

            e => {

350

//

351

288

                let aux_var_info = to_aux_var(&e, &symbols).ok_or(RuleNotApplicable)?;

352

353

144

                symbols = aux_var_info.symbols();

354

144

                let var = aux_var_info.as_atom();

355

144

                new_top_exprs.push(aux_var_info.top_level_expr());

356

144

                (Lit::Int(1), var)

357

358

};

359

360

1944

        let coeff_num: i32 = coeff.clone().try_into().or(Err(RuleNotApplicable))?;

361

1944

        found_non_one_coeff |= coeff_num != 1;

362

1944

        coefficients.push(coeff);

363

1944

        vars.push(var);

364

365

366

738

    let use_weighted_sum = found_non_one_coeff;

367

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

368

738

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

369

72

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

370

72

            Metadata::new(),

371

72

            Box::new(matrix_expr![

372

72

                Expr::FlatWeightedSumLeq(

373

72

                    Metadata::new(),

374

72

                    coefficients.clone(),

375

72

                    vars.clone(),

376

72

                    total.clone(),

377

72

),

378

72

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

379

72

]),

380

72

),

381

342

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

382

342

            Metadata::new(),

383

342

            Box::new(matrix_expr![

384

342

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

385

342

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

386

342

]),

387

342

),

388

        (EqualityKind::Leq, true) => {

389

54

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

390

391

90

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

392

        (EqualityKind::Geq, true) => {

393

18

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

394

395

162

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

396

};

397

398

738

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

399

279144

400

401

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

402

122598

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

403

122598

    // div = val

404

122598

    let val: Atom;

405

122598

    let div: Expr;

406

122598

    let meta: Metadata;

407

122598

408

122598

    match expr.clone() {

409

6462

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

410

6462

            meta = m;

411

6462

412

6462

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

413

6462

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

414

415

6462

            if let Some(f) = a_atom {

416

5508

                // val = div

417

5508

                val = f.clone();

418

5508

                div = *b;

419

5508

            } else if let Some(f) = b_atom {

420

936

                // div = val

421

936

                val = f.clone();

422

936

                div = *a;

423

936

            } else {

424

18

                return Err(RuleNotApplicable);

425

426

427

792

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

428

792

            meta = m;

429

792

            val = name.into();

430

792

            div = *e;

431

792

432

        _ => {

433

115344

            return Err(RuleNotApplicable);

434

435

436

437

7236

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

438

6516

        return Err(RuleNotApplicable);

439

720

440

720

441

720

    let children = div.children();

442

720

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

443

648

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

444

445

594

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

446

594

        meta.clone_dirty(),

447

594

        a.clone(),

448

594

        b.clone(),

449

594

        val,

450

594

)))

451

122598

452

453

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

454

122598

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

455

122598

    // div = val

456

122598

    let val: Atom;

457

122598

    let div: Expr;

458

122598

    let meta: Metadata;

459

122598

460

122598

    match expr.clone() {

461

6462

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

462

6462

            meta = m;

463

6462

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

464

6462

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

465

466

6462

            if let Some(f) = a_atom {

467

5508

                // val = div

468

5508

                val = f.clone();

469

5508

                div = *b;

470

5508

            } else if let Some(f) = b_atom {

471

936

                // div = val

472

936

                val = f.clone();

473

936

                div = *a;

474

936

            } else {

475

18

                return Err(RuleNotApplicable);

476

477

478

792

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

479

792

            meta = m;

480

792

            val = name.into();

481

792

            div = *e;

482

792

483

        _ => {

484

115344

            return Err(RuleNotApplicable);

485

486

487

488

7236

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

489

6768

        return Err(RuleNotApplicable);

490

468

491

468

492

468

    let children = div.children();

493

468

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

494

468

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

495

496

414

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

497

414

        meta.clone_dirty(),

498

414

        a.clone(),

499

414

        b.clone(),

500

414

        val,

501

414

)))

502

122598

503

504

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

505

233118

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

506

233118

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

507

15282

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

508

15282

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

509

15282

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

510

511

15282

            if let Some(a_atom) = a_atom {

512

8766

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

513

6516

            } else if let Some(b_atom) = b_atom {

514

6498

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

515

            } else {

516

18

                Err(RuleNotApplicable)

517

518

519

520

2088

        Expr::AuxDeclaration(_, a, b) => Ok((a.into(), *b)),

521

522

215748

        _ => Err(RuleNotApplicable),

523

215766

}?;

524

525

17352

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

526

17190

        return Err(RuleNotApplicable);

527

};

528

529

162

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

530

531

144

    Ok(Reduction::pure(Expr::FlatAbsEq(Metadata::new(), x, y)))

532

233118

533

534

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

535

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

536

122598

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

537

122598

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

538

6462

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

539

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

540

108

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

541

6354

            _ => Err(RuleNotApplicable),

542

},

543

116136

        _ => Err(RuleNotApplicable),

544

122490

}?;

545

546

108

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

547

90

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

548

549

90

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

550

90

        Metadata::new(),

551

90

a,

552

90

b,

553

90

        total,

554

90

)))

555

122598

556

557

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

558

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

559

122598

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

560

122598

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

561

122166

        return Err(RuleNotApplicable);

562

};

563

564

432

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

565

566

54

    let atoms = es

567

54

        .into_iter()

568

162

        .map(|e| match e {

569

162

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

570

            _ => Err(RuleNotApplicable),

571

162

})

572

54

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

573

574

54

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

575

122598

576

577

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

578

///

579

/// ```text

580

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

581

///

582

///   where x,y are atoms

583

/// ```

584

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

585

233118

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

586

233118

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

587

217836

        return Err(RuleNotApplicable);

588

};

589

590

30528

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

591

30528

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

592

23508

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

593

23454

            return None;

594

};

595

596

54

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

597

598

36

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

599

30528

600

601

15282

    let a = *a.clone();

602

15282

    let b = *b.clone();

603

604

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

605

15282

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

606

15246

        return Err(RuleNotApplicable);

607

};

608

609

36

    Ok(Reduction::pure(Expr::FlatMinusEq(Metadata::new(), x, y)))

610

233118

611

612

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

613

///

614

/// ```text

615

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

616

///

617

///   where x,y are atoms

618

/// ```

619

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

620

233118

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

621

    // a =aux -b

622

//

623

233118

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

624

231030

        return Err(RuleNotApplicable);

625

};

626

627

2088

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

628

629

2088

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

630

2016

        return Err(RuleNotApplicable);

631

};

632

633

72

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

634

36

        return Err(RuleNotApplicable);

635

};

636

637

36

    Ok(Reduction::pure(Expr::FlatMinusEq(Metadata::new(), a, b)))

638

233118

639

640

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

641

///

642

/// ```text

643

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

644

/// where x is atomic, y is atomic

645

///

646

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

647

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

648

/// ```

649

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

650

233118

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

651

233118

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

652

228654

        return Err(RuleNotApplicable);

653

};

654

655

4464

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

656

657

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

658

//

659

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

660

540

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

661

216

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

662

216

            Metadata::new(),

663

216

            x_atom.clone(),

664

216

            y_atom.clone(),

665

216

            0.into(),

666

216

)))

667

    } else {

668

324

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

669

324

            Metadata::new(),

670

324

            y.clone(),

671

324

            x_atom.clone(),

672

324

)))

673

674

233118

675

676

/// Flattens an implication.

677

///

678

/// ```text

679

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

680

///  ~~>

681

/// __0 -> y,

682

///

683

/// with new top level constraints

684

/// __0 =aux x

685

///

686

/// ```

687

///

688

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

689

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

690

/// an argument:

691

///

692

/// ``` text

693

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

694

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

695

/// ```

696

///

697

/// See [`introduce_reifyimply_ineq_from_imply`].

698

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

699

122598

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

700

122598

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

701

122256

        return Err(RuleNotApplicable);

702

};

703

704

    // flatten x

705

342

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

706

707

342

    let symbols = aux_var_info.symbols();

708

342

    let new_x = aux_var_info.as_expr();

709

342

710

342

    Ok(Reduction::new(

711

342

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

712

342

        vec![aux_var_info.top_level_expr()],

713

342

        symbols,

714

342

))

715

122598

716

717

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

718

122598

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

719

113004

    if !matches!(

720

122598

        expr,

721

        Expr::SafeDiv(_, _, _)

722

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

723

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

724

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

725

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

726

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

727

            | Expr::Abs(_, _)

728

            | Expr::Product(_, _)

729

            | Expr::Neg(_, _)

730

            | Expr::Not(_, _)

731

) {

732

113004

        return Err(RuleNotApplicable);

733

9594

734

9594

735

9594

    let mut children = expr.children();

736

9594

737

9594

    let mut symbols = symbols.clone();

738

9594

    let mut num_changed = 0;

739

9594

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

740

741

17892

    for child in children.iter_mut() {

742

17892

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

743

684

            symbols = aux_var_info.symbols();

744

684

            new_tops.push(aux_var_info.top_level_expr());

745

684

            *child = aux_var_info.as_expr();

746

684

            num_changed += 1;

747

17208

748

749

750

9594

    if num_changed == 0 {

751

8928

        return Err(RuleNotApplicable);

752

666

753

666

754

666

    let expr = expr.with_children(children);

755

666

756

666

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

757

122598

758

759

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

760

122598

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

761

122598

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

762

116136

        return Err(RuleNotApplicable);

763

6462

764

6462

765

6462

    let mut children = expr.children();

766

6462

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

767

768

6462

    let mut symbols = symbols.clone();

769

6462

    let mut num_changed = 0;

770

6462

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

771

772

12924

    for child in children.iter_mut() {

773

12924

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

774

1116

            symbols = aux_var_info.symbols();

775

1116

            new_tops.push(aux_var_info.top_level_expr());

776

1116

            *child = aux_var_info.as_expr();

777

1116

            num_changed += 1;

778

11808

779

780

781

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

782

6462

    if num_changed != 2 {

783

6444

        return Err(RuleNotApplicable);

784

18

785

18

786

18

    let expr = expr.with_children(children);

787

18

788

18

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

789

122598

790

791

/// Converts a Geq to an Ineq

792

///

793

/// ```text

794

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

795

/// ```

796

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

797

57276

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

798

57276

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

799

56826

        return Err(RuleNotApplicable);

800

};

801

802

450

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

803

54

        return Err(RuleNotApplicable);

804

};

805

806

396

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

807

36

        return Err(RuleNotApplicable);

808

};

809

810

360

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

811

360

        meta.clone_dirty(),

812

360

y,

813

360

x,

814

360

        Lit::Int(0),

815

360

)))

816

57276

817

818

/// Converts a Leq to an Ineq

819

///

820

/// ```text

821

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

822

/// ```

823

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

824

57276

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

825

57276

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

826

56448

        return Err(RuleNotApplicable);

827

};

828

829

828

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

830

108

        return Err(RuleNotApplicable);

831

};

832

833

720

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

834

18

        return Err(RuleNotApplicable);

835

};

836

837

702

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

838

702

        meta.clone_dirty(),

839

702

x,

840

702

y,

841

702

        Lit::Int(0),

842

702

)))

843

57276

844

845

// TODO: add this rule for geq

846

847

/// ```text

848

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

849

/// ```

850

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

851

275148

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

852

275148

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

853

260550

        return Err(RuleNotApplicable);

854

};

855

856

14598

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

857

126

        return Err(RuleNotApplicable);

858

};

859

860

14472

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

861

14418

        return Err(RuleNotApplicable);

862

};

863

864

54

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

865

36

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

866

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

867

        _ => {

868

18

            return Err(RuleNotApplicable);

869

870

};

871

872

36

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

873

36

        meta.clone_dirty(),

874

36

x,

875

36

        y.clone(),

876

36

        k.clone(),

877

36

)))

878

275148

879

880

/// ```text

881

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

882

/// ```

883

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

884

284742

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

885

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

886

284742

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

887

283428

        return Err(RuleNotApplicable);

888

};

889

890

1314

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

891

72

        return Err(RuleNotApplicable);

892

};

893

894

1242

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

895

1152

        return Err(RuleNotApplicable);

896

};

897

898

90

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

899

36

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

900

18

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

901

        _ => {

902

36

            return Err(RuleNotApplicable);

903

904

};

905

906

54

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

907

54

        meta.clone_dirty(),

908

54

x,

909

54

        y.clone(),

910

54

        k.clone(),

911

54

)))

912

284742

913

914

/// Flattening rule for not(bool_lit)

915

///

916

/// For some boolean variable x:

917

/// ```text

918

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

919

/// ```

920

///

921

/// ## Rationale

922

///

923

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

924

///

925

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

926

///

927

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

928

/// trivial match).

929

930

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

931

57276

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

932

    use Domain::BoolDomain;

933

57276

    match expr {

934

126

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

935

126

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

936

126

                if symbols

937

126

                    .domain(&name)

938

126

                    .is_some_and(|x| matches!(x, BoolDomain))

939

940

126

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

941

126

                        m.clone_dirty(),

942

126

                        name.clone(),

943

126

                        Lit::Bool(false),

944

126

                    )));

945

946

947

            Err(RuleNotApplicable)

948

949

57150

        _ => Err(RuleNotApplicable),

950

951

57276

952

953

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

954

///

955

/// ```text

956

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

957

/// ```

958

///

959

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

960

/// nested expressions are constraints not variables.

961

962

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

963

36792

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

964

36792

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

965

36792

        return Err(RuleNotApplicable);

966

967

968

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

969

        unreachable!();

970

};

971

972

    extra_check! {

973

        if !is_flat(e) {

974

            return Err(RuleNotApplicable);

975

976

};

977

978

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

979

        m.clone(),

980

        e.clone(),

981

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

982

)))

983

36792

984

985

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

986

///

987

/// ```text

988

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

989

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

990

///

991

/// where c is a boolean constraint

992

/// ```

993

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

994

233118

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

995

233118

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

996

2088

        Expr::AuxDeclaration(_, name, e) => Ok((name.clone().into(), e.clone())),

997

15282

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

998

8766

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

999

6498

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

1000

18

            _ => Err(RuleNotApplicable),

1001

},

1002

1003

215748

        _ => Err(RuleNotApplicable),

1004

215766

}?;

1005

1006

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

1007

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

1008

17352

    let Some(ReturnType::Bool) = e.as_ref().return_type() else {

1009

16920

        return Err(RuleNotApplicable);

1010

};

1011

1012

432

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

1013

432

        Metadata::new(),

1014

432

        e.clone(),

1015

432

        atom,

1016

432

)))

1017

233118