Grcov report - minion.rs

1

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

2

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

3

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

4

5

use std::convert::TryInto;

6

7

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

8

9

use crate::metadata::Metadata;

10

use crate::rule_engine::{

11

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

12

};

13

use crate::rules::extra_check;

14

15

use crate::solver::SolverFamily;

16

use crate::Model;

17

use uniplate::Uniplate;

18

use ApplicationError::*;

19

20

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

21

22

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

23

24

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

25

73525

fn introduce_producteq(expr: &Expr, model: &Model) -> ApplicationResult {

26

73525

    // product = val

27

73525

    let val: Atom;

28

73525

    let product: Expr;

29

73525

30

73525

    match expr.clone() {

31

4930

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

32

4930

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

33

4930

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

34

35

4930

            if let Some(f) = a_atom {

36

4369

                // val = product

37

4369

                val = f.clone();

38

4369

                product = *b;

39

4369

            } else if let Some(f) = b_atom {

40

561

                // product = val

41

561

                val = f.clone();

42

561

                product = *a;

43

561

            } else {

44

                return Err(RuleNotApplicable);

45

46

47

663

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

48

663

            val = name.into();

49

663

            product = *e;

50

663

51

        _ => {

52

67932

            return Err(RuleNotApplicable);

53

54

55

56

5593

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

57

5525

        return Err(RuleNotApplicable);

58

68

59

60

68

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

61

        return Err(RuleNotApplicable);

62

};

63

64

68

    if factors.len() < 2 {

65

        return Err(RuleNotApplicable);

66

68

67

68

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

69

    // Introduce auxvars until it is a binop

70

71

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

72

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

73

74

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

75

68

    let x: Atom = factors

76

68

        .pop()

77

68

        .unwrap()

78

68

        .try_into()

79

68

        .or(Err(RuleNotApplicable))?;

80

81

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

82

51

    let mut y: Atom = factors

83

51

        .pop()

84

51

        .unwrap()

85

51

        .try_into()

86

51

        .or(Err(RuleNotApplicable))?;

87

88

51

    let mut model = model.clone();

89

51

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

90

91

    // FIXME: add a test for this

92

68

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

93

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

94

        // similar to other introduction rules.

95

17

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

96

97

17

        let aux_var = model.gensym();

98

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

99

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

100

17

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

101

17

            .domain_of(&model.symbols().clone())

102

17

            .ok_or(ApplicationError::DomainError)?;

103

104

17

        model.add_variable(aux_var.clone(), DecisionVariable { domain: aux_domain });

105

17

106

17

        let new_top_expr =

107

17

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

108

17

109

17

        new_tops.push(new_top_expr);

110

17

        y = aux_var.into();

111

112

113

51

    Ok(Reduction::new(

114

51

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

115

51

        new_tops,

116

51

        model.symbols().clone(),

117

51

))

118

73525

119

120

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

121

///

122

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

123

/// sum constraints are used.

124

///

125

/// # Details

126

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

127

/// it does its own flattening.

128

///

129

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

130

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

131

/// from a sum:

132

///

133

///```text

134

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

135

///   ~~> flatten_vecop

136

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

137

///

138

/// with new top level constraints

139

///

140

/// __0 =aux 1*a

141

/// __1 =aux 2*b

142

/// __2 =aux 3*c

143

/// ```

144

///

145

/// Therefore, introduce_weightedsumleq_sumgeq does its own flattening.

146

///

147

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

148

/// weighted sums.

149

///

150

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

151

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

152

///

153

///```text

154

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

155

///

156

///   ~> introduce_weightedsumleq_sumgeq

157

///

158

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

159

///

160

/// with new top level constraints

161

///

162

/// __0 = c*d

163

/// __1 = e/f

164

/// __2 = g/h

165

/// ```

166

///

167

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

168

///

169

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

170

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

171

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

172

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

173

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

174

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

175

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

176

///

177

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

178

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

179

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

180

195755

fn introduce_weighted_sumleq_sumgeq(expr: &Expr, model: &Model) -> ApplicationResult {

181

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

182

    // constraints to make at the end

183

184

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

185

    // elsewhere, as this caused cyclic rule application:

186

//

187

    // ```

188

    // 2*a + b = c

189

//

190

    //   ~~> sumeq_to_inequalities

191

//

192

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

193

//

194

    // --

195

//

196

    // 2*a + b <= c

197

//

198

    //   ~~> flatten_generic

199

    // __1 <=c

200

//

201

    // with new top level constraint

202

//

203

    // 2*a + b =aux __1

204

//

205

    // --

206

//

207

    // 2*a + b =aux __1

208

//

209

    //   ~~> sumeq_to_inequalities

210

//

211

    // LOOP!

212

    // ```

213

    enum EqualityKind {

214

Eq,

215

        Leq,

216

        Geq,

217

218

219

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

220

//

221

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

222

    // on the right hand side.

223

//

224

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

225

29869

    fn match_sum_total(

226

29869

        a: Expr,

227

29869

        b: Expr,

228

29869

        equality_kind: EqualityKind,

229

29869

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

230

29869

        match (a, b, equality_kind) {

231

119

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

232

119

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

233

234

85

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

235

85

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

236

237

51

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

238

51

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

239

240

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

241

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

242

243

204

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

244

204

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

245

246

51

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

247

51

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

248

249

29359

            _ => Err(RuleNotApplicable),

250

251

29869

252

253

195755

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

254

12614

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

255

986

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

256

16269

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

257

2329

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

258

2329

            let total: Atom = n.into();

259

2329

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

260

68

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

261

            } else {

262

2261

                Err(RuleNotApplicable)

263

264

265

163557

        _ => Err(RuleNotApplicable),

266

165818

}?;

267

268

578

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

269

578

    let mut model = model.clone();

270

578

271

578

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

272

578

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

273

578

274

578

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

275

578

    let mut found_non_one_coeff = false;

276

277

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

278

2142

    for expr in sum_exprs {

279

1564

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

280

            // atom: v ~> 1*v

281

1071

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

282

283

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

284

285

            // weighted sum term: c * e.

286

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

287

            // flattening

288

255

            Expr::Product(_, factors)

289

255

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

290

255

291

255

                match &factors[..] {

292

                    // c * <atom>

293

221

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

294

221

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

295

296

297

                    // c * <some non-flat expression>

298

17

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

299

17

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

300

17

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

301

17

302

17

                        model = aux_var_info.model();

303

17

                        let var = aux_var_info.as_atom();

304

17

                        new_top_exprs.push(aux_var_info.top_level_expr());

305

17

                        (c.clone(), var)

306

307

308

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

309

17

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

310

17

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

311

17

312

17

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

313

17

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

314

17

315

17

                        model = aux_var_info.model();

316

17

                        let var = aux_var_info.as_atom();

317

17

                        new_top_exprs.push(aux_var_info.top_level_expr());

318

17

                        (c.clone(), var)

319

320

321

                    _ => unreachable!(),

322

323

324

325

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

326

//

327

            // flatten e if non-atomic

328

102

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

329

                // needs flattening

330

102

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

331

17

                    model = aux_var_info.model();

332

17

                    new_top_exprs.push(aux_var_info.top_level_expr());

333

17

                    aux_var_info.as_atom()

334

                } else {

335

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

336

                    #[allow(clippy::unwrap_used)]

337

85

                    e.try_into().unwrap()

338

};

339

340

102

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

341

342

343

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

344

//

345

            // includes products without coefficients.

346

136

            e => {

347

//

348

136

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

349

350

136

                model = aux_var_info.model();

351

136

                let var = aux_var_info.as_atom();

352

136

                new_top_exprs.push(aux_var_info.top_level_expr());

353

136

                (Lit::Int(1), var)

354

355

};

356

357

1564

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

358

1564

        found_non_one_coeff |= coeff_num != 1;

359

1564

        coefficients.push(coeff);

360

1564

        vars.push(var);

361

362

363

578

    let use_weighted_sum = found_non_one_coeff;

364

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

365

578

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

366

68

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

367

68

            Metadata::new(),

368

68

            vec![

369

68

                Expr::FlatWeightedSumLeq(

370

68

                    Metadata::new(),

371

68

                    coefficients.clone(),

372

68

                    vars.clone(),

373

68

                    total.clone(),

374

68

),

375

68

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

376

68

],

377

68

),

378

255

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

379

255

            Metadata::new(),

380

255

            vec![

381

255

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

382

255

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

383

255

],

384

255

),

385

        (EqualityKind::Leq, true) => {

386

51

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

387

388

68

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

389

        (EqualityKind::Geq, true) => {

390

17

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

391

392

119

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

393

};

394

395

578

    Ok(Reduction::new(

396

578

        new_expr,

397

578

        new_top_exprs,

398

578

        model.symbols().clone(),

399

578

))

400

195755

401

402

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

403

73525

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

404

73525

    // div = val

405

73525

    let val: Atom;

406

73525

    let div: Expr;

407

73525

    let meta: Metadata;

408

73525

409

73525

    match expr.clone() {

410

4930

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

411

4930

            meta = m;

412

4930

413

4930

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

414

4930

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

415

416

4930

            if let Some(f) = a_atom {

417

4369

                // val = div

418

4369

                val = f.clone();

419

4369

                div = *b;

420

4369

            } else if let Some(f) = b_atom {

421

561

                // div = val

422

561

                val = f.clone();

423

561

                div = *a;

424

561

            } else {

425

                return Err(RuleNotApplicable);

426

427

428

663

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

429

663

            meta = m;

430

663

            val = name.into();

431

663

            div = *e;

432

663

433

        _ => {

434

67932

            return Err(RuleNotApplicable);

435

436

437

438

5593

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

439

4913

        return Err(RuleNotApplicable);

440

680

441

680

442

680

    let children = div.children();

443

680

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

444

612

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

445

446

561

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

447

561

        meta.clone_dirty(),

448

561

        a.clone(),

449

561

        b.clone(),

450

561

        val,

451

561

)))

452

73525

453

454

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

455

73525

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

456

73525

    // div = val

457

73525

    let val: Atom;

458

73525

    let div: Expr;

459

73525

    let meta: Metadata;

460

73525

461

73525

    match expr.clone() {

462

4930

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

463

4930

            meta = m;

464

4930

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

465

4930

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

466

467

4930

            if let Some(f) = a_atom {

468

4369

                // val = div

469

4369

                val = f.clone();

470

4369

                div = *b;

471

4369

            } else if let Some(f) = b_atom {

472

561

                // div = val

473

561

                val = f.clone();

474

561

                div = *a;

475

561

            } else {

476

                return Err(RuleNotApplicable);

477

478

479

663

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

480

663

            meta = m;

481

663

            val = name.into();

482

663

            div = *e;

483

663

484

        _ => {

485

67932

            return Err(RuleNotApplicable);

486

487

488

489

5593

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

490

5151

        return Err(RuleNotApplicable);

491

442

492

442

493

442

    let children = div.children();

494

442

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

495

442

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

496

497

391

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

498

391

        meta.clone_dirty(),

499

391

        a.clone(),

500

391

        b.clone(),

501

391

        val,

502

391

)))

503

73525

504

505

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

506

166413

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

507

166413

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

508

13175

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

509

13175

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

510

13175

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

511

512

13175

            if let Some(a_atom) = a_atom {

513

7429

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

514

5746

            } else if let Some(b_atom) = b_atom {

515

5746

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

516

            } else {

517

                Err(RuleNotApplicable)

518

519

520

521

1819

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

522

523

151419

        _ => Err(RuleNotApplicable),

524

151419

}?;

525

526

14994

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

527

14841

        return Err(RuleNotApplicable);

528

};

529

530

153

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

531

532

136

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

533

166413

534

535

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

536

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

537

73525

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

538

73525

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

539

4930

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

540

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

541

102

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

542

4828

            _ => Err(RuleNotApplicable),

543

},

544

68595

        _ => Err(RuleNotApplicable),

545

73423

}?;

546

547

102

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

548

85

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

549

550

85

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

551

85

        Metadata::new(),

552

85

a,

553

85

b,

554

85

        total,

555

85

)))

556

73525

557

558

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

559

///

560

/// ```text

561

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

562

///

563

///   where x,y are atoms

564

/// ```

565

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

566

166413

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

567

166413

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

568

153238

        return Err(RuleNotApplicable);

569

};

570

571

26316

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

572

26316

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

573

20196

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

574

20145

            return None;

575

};

576

577

51

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

578

579

34

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

580

26316

581

582

13175

    let a = *a.clone();

583

13175

    let b = *b.clone();

584

585

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

586

13175

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

587

13141

        return Err(RuleNotApplicable);

588

};

589

590

34

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

591

166413

592

593

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

594

///

595

/// ```text

596

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

597

///

598

///   where x,y are atoms

599

/// ```

600

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

601

166413

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

602

    // a =aux -b

603

//

604

166413

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

605

164594

        return Err(RuleNotApplicable);

606

};

607

608

1819

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

609

610

1819

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

611

1751

        return Err(RuleNotApplicable);

612

};

613

614

68

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

615

34

        return Err(RuleNotApplicable);

616

};

617

618

34

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

619

166413

620

621

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

622

///

623

/// ```text

624

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

625

/// where x is atomic, y is atomic

626

///

627

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

628

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

629

/// ```

630

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

631

166413

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

632

166413

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

633

162452

        return Err(RuleNotApplicable);

634

};

635

636

3961

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

637

638

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

639

//

640

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

641

323

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

642

102

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

643

102

            Metadata::new(),

644

102

            x_atom.clone(),

645

102

            y_atom.clone(),

646

102

            0.into(),

647

102

)))

648

    } else {

649

221

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

650

221

            Metadata::new(),

651

221

            y.clone(),

652

221

            x_atom.clone(),

653

221

)))

654

655

166413

656

657

/// Flattens an implication.

658

///

659

/// ```text

660

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

661

///  ~~>

662

/// __0 -> y,

663

///

664

/// with new top level constraints

665

/// __0 =aux x

666

///

667

/// ```

668

///

669

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

670

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

671

/// an argument:

672

///

673

/// ``` text

674

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

675

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

676

/// ```

677

///

678

/// See [`introduce_reifyimply_ineq_from_imply`].

679

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

680

73525

fn flatten_imply(expr: &Expr, model: &Model) -> ApplicationResult {

681

73525

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

682

73236

        return Err(RuleNotApplicable);

683

};

684

685

    // flatten x

686

289

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

687

688

289

    let model = aux_var_info.model();

689

289

    let new_x = aux_var_info.as_expr();

690

289

691

289

    Ok(Reduction::new(

692

289

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

693

289

        vec![aux_var_info.top_level_expr()],

694

289

        model.symbols().clone(),

695

289

))

696

73525

697

698

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

699

73525

fn flatten_generic(expr: &Expr, model: &Model) -> ApplicationResult {

700

65501

    if !matches!(

701

73525

        expr,

702

        Expr::SafeDiv(_, _, _)

703

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

704

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

705

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

706

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

707

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

708

            | Expr::Abs(_, _)

709

            | Expr::Product(_, _)

710

            | Expr::Neg(_, _)

711

            | Expr::Not(_, _)

712

) {

713

65501

        return Err(RuleNotApplicable);

714

8024

715

8024

716

8024

    let mut children = expr.children();

717

8024

718

8024

    let mut model = model.clone();

719

8024

    let mut num_changed = 0;

720

8024

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

721

722

15334

    for child in children.iter_mut() {

723

15334

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

724

612

            model = aux_var_info.model();

725

612

            new_tops.push(aux_var_info.top_level_expr());

726

612

            *child = aux_var_info.as_expr();

727

612

            num_changed += 1;

728

14722

729

730

731

8024

    if num_changed == 0 {

732

7429

        return Err(RuleNotApplicable);

733

595

734

595

735

595

    let expr = expr.with_children(children);

736

595

737

595

    Ok(Reduction::new(expr, new_tops, model.symbols().clone()))

738

73525

739

740

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

741

73525

fn flatten_eq(expr: &Expr, model: &Model) -> ApplicationResult {

742

73525

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

743

68595

        return Err(RuleNotApplicable);

744

4930

745

4930

746

4930

    let mut children = expr.children();

747

4930

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

748

749

4930

    let mut model = model.clone();

750

4930

    let mut num_changed = 0;

751

4930

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

752

753

9860

    for child in children.iter_mut() {

754

9860

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

755

680

            model = aux_var_info.model();

756

680

            new_tops.push(aux_var_info.top_level_expr());

757

680

            *child = aux_var_info.as_expr();

758

680

            num_changed += 1;

759

9180

760

761

762

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

763

4930

    if num_changed != 2 {

764

4930

        return Err(RuleNotApplicable);

765

766

767

    let expr = expr.with_children(children);

768

769

    Ok(Reduction::new(expr, new_tops, model.symbols().clone()))

770

73525

771

772

/// Converts a Geq to an Ineq

773

///

774

/// ```text

775

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

776

/// ```

777

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

778

24361

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

779

24361

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

780

24038

        return Err(RuleNotApplicable);

781

};

782

783

323

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

784

        return Err(RuleNotApplicable);

785

};

786

787

323

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

788

        return Err(RuleNotApplicable);

789

};

790

791

323

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

792

323

        meta.clone_dirty(),

793

323

y,

794

323

x,

795

323

        Lit::Int(0),

796

323

)))

797

24361

798

799

/// Converts a Leq to an Ineq

800

///

801

/// ```text

802

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

803

/// ```

804

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

805

24361

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

806

24361

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

807

23834

        return Err(RuleNotApplicable);

808

};

809

810

527

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

811

        return Err(RuleNotApplicable);

812

};

813

814

527

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

815

17

        return Err(RuleNotApplicable);

816

};

817

818

510

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

819

510

        meta.clone_dirty(),

820

510

x,

821

510

y,

822

510

        Lit::Int(0),

823

510

)))

824

24361

825

826

// TODO: add this rule for geq

827

828

/// ```text

829

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

830

/// ```

831

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

832

193715

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

833

193715

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

834

181305

        return Err(RuleNotApplicable);

835

};

836

837

12410

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

838

17

        return Err(RuleNotApplicable);

839

};

840

841

12393

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

842

12359

        return Err(RuleNotApplicable);

843

};

844

845

34

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

846

34

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

847

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

848

        _ => {

849

            return Err(RuleNotApplicable);

850

851

};

852

853

34

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

854

34

        meta.clone_dirty(),

855

34

x,

856

34

        y.clone(),

857

34

        k.clone(),

858

34

)))

859

193715

860

861

/// ```text

862

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

863

/// ```

864

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

865

200294

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

866

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

867

200294

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

868

199172

        return Err(RuleNotApplicable);

869

};

870

871

1122

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

872

        return Err(RuleNotApplicable);

873

};

874

875

1122

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

876

1037

        return Err(RuleNotApplicable);

877

};

878

879

85

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

880

34

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

881

17

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

882

        _ => {

883

34

            return Err(RuleNotApplicable);

884

885

};

886

887

51

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

888

51

        meta.clone_dirty(),

889

51

x,

890

51

        y.clone(),

891

51

        k.clone(),

892

51

)))

893

200294

894

895

/// Flattening rule for not(bool_lit)

896

///

897

/// For some boolean variable x:

898

/// ```text

899

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

900

/// ```

901

///

902

/// ## Rationale

903

///

904

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

905

///

906

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

907

///

908

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

909

/// trivial match).

910

911

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

912

24361

fn not_literal_to_wliteral(expr: &Expr, mdl: &Model) -> ApplicationResult {

913

    use Domain::BoolDomain;

914

24361

    match expr {

915

85

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

916

85

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

917

85

                if mdl

918

85

                    .get_domain(&name)

919

85

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

920

921

85

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

922

85

                        m.clone_dirty(),

923

85

                        name.clone(),

924

85

                        Lit::Bool(false),

925

85

                    )));

926

927

928

            Err(RuleNotApplicable)

929

930

24276

        _ => Err(RuleNotApplicable),

931

932

24361

933

934

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

935

///

936

/// ```text

937

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

938

/// ```

939

///

940

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

941

/// nested expressions are constraints not variables.

942

943

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

944

10387

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

945

10387

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

946

10387

        return Err(RuleNotApplicable);

947

948

949

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

950

        unreachable!();

951

};

952

953

    extra_check! {

954

        if !is_flat(e) {

955

            return Err(RuleNotApplicable);

956

957

};

958

959

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

960

        m.clone(),

961

        e.clone(),

962

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

963

)))

964

10387

965

966

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

967

///

968

/// ```text

969

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

970

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

971

///

972

/// where c is a boolean constraint

973

/// ```

974

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

975

166413

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

976

166413

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

977

1819

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

978

13175

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

979

7429

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

980

5746

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

981

            _ => Err(RuleNotApplicable),

982

},

983

984

151419

        _ => Err(RuleNotApplicable),

985

151419

}?;

986

987

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

988

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

989

14994

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

990

14637

        return Err(RuleNotApplicable);

991

};

992

993

357

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

994

357

        Metadata::new(),

995

357

        e.clone(),

996

357

        atom,

997

357

)))

998

166413