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::Declaration;

9

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

10

11

use crate::metadata::Metadata;

12

use crate::rule_engine::{

13

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

14

};

15

use crate::rules::extra_check;

16

17

use crate::solver::SolverFamily;

18

use uniplate::Uniplate;

19

use ApplicationError::*;

20

21

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

22

23

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

24

25

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

26

76670

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

27

76670

    // product = val

28

76670

    let val: Atom;

29

76670

    let product: Expr;

30

76670

31

76670

    match expr.clone() {

32

4913

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

33

4913

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

34

4913

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

35

36

4913

            if let Some(f) = a_atom {

37

4369

                // val = product

38

4369

                val = f.clone();

39

4369

                product = *b;

40

4369

            } else if let Some(f) = b_atom {

41

544

                // product = val

42

544

                val = f.clone();

43

544

                product = *a;

44

544

            } else {

45

                return Err(RuleNotApplicable);

46

47

48

663

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

49

663

            val = name.into();

50

663

            product = *e;

51

663

52

        _ => {

53

71094

            return Err(RuleNotApplicable);

54

55

56

57

5576

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

58

5508

        return Err(RuleNotApplicable);

59

68

60

61

68

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

62

        return Err(RuleNotApplicable);

63

};

64

65

68

    if factors.len() < 2 {

66

        return Err(RuleNotApplicable);

67

68

69

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

70

    // Introduce auxvars until it is a binop

71

72

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

73

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

74

75

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

76

68

    let x: Atom = factors

77

68

        .pop()

78

68

        .unwrap()

79

68

        .try_into()

80

68

        .or(Err(RuleNotApplicable))?;

81

82

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

83

51

    let mut y: Atom = factors

84

51

        .pop()

85

51

        .unwrap()

86

51

        .try_into()

87

51

        .or(Err(RuleNotApplicable))?;

88

89

51

    let mut symbols = symbols.clone();

90

51

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

91

92

    // FIXME: add a test for this

93

68

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

94

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

95

        // similar to other introduction rules.

96

17

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

97

98

17

        let aux_var = symbols.gensym();

99

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

100

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

101

17

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

102

17

            .domain_of(&symbols)

103

17

            .ok_or(ApplicationError::DomainError)?;

104

105

17

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

106

17

107

17

        let new_top_expr =

108

17

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

109

17

110

17

        new_tops.push(new_top_expr);

111

17

        y = aux_var.into();

112

113

114

51

    Ok(Reduction::new(

115

51

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

116

51

        new_tops,

117

51

        symbols,

118

51

))

119

76670

120

121

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

122

///

123

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

124

/// sum constraints are used.

125

///

126

/// # Details

127

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

128

/// it does its own flattening.

129

///

130

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

131

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

132

/// from a sum:

133

///

134

///```text

135

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

136

///   ~~> flatten_vecop

137

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

138

///

139

/// with new top level constraints

140

///

141

/// __0 =aux 1*a

142

/// __1 =aux 2*b

143

/// __2 =aux 3*c

144

/// ```

145

///

146

/// Therefore, introduce_weightedsumleq_sumgeq does its own flattening.

147

///

148

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

149

/// weighted sums.

150

///

151

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

152

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

153

///

154

///```text

155

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

156

///

157

///   ~> introduce_weightedsumleq_sumgeq

158

///

159

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

160

///

161

/// with new top level constraints

162

///

163

/// __0 = c*d

164

/// __1 = e/f

165

/// __2 = g/h

166

/// ```

167

///

168

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

169

///

170

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

171

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

172

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

173

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

174

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

175

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

176

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

177

///

178

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

179

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

180

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

181

200991

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

182

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

183

    // constraints to make at the end

184

185

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

186

    // elsewhere, as this caused cyclic rule application:

187

//

188

    // ```

189

    // 2*a + b = c

190

//

191

    //   ~~> sumeq_to_inequalities

192

//

193

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

194

//

195

    // --

196

//

197

    // 2*a + b <= c

198

//

199

    //   ~~> flatten_generic

200

    // __1 <=c

201

//

202

    // with new top level constraint

203

//

204

    // 2*a + b =aux __1

205

//

206

    // --

207

//

208

    // 2*a + b =aux __1

209

//

210

    //   ~~> sumeq_to_inequalities

211

//

212

    // LOOP!

213

    // ```

214

    enum EqualityKind {

215

Eq,

216

        Leq,

217

        Geq,

218

219

220

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

221

//

222

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

223

    // on the right hand side.

224

//

225

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

226

30311

    fn match_sum_total(

227

30311

        a: Expr,

228

30311

        b: Expr,

229

30311

        equality_kind: EqualityKind,

230

30311

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

231

30311

        match (a, b, equality_kind) {

232

119

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

233

119

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

234

235

85

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

236

85

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

237

238

51

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

239

51

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

240

241

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

242

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

243

244

238

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

245

238

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

246

247

51

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

248

51

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

249

250

29767

            _ => Err(RuleNotApplicable),

251

252

30311

253

254

200991

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

255

12869

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

256

1139

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

257

16303

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

258

2397

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

259

2397

            let total: Atom = n.into();

260

2397

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

261

68

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

262

            } else {

263

2329

                Err(RuleNotApplicable)

264

265

266

168283

        _ => Err(RuleNotApplicable),

267

170612

}?;

268

269

612

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

270

612

    let mut symbols = symbols.clone();

271

612

272

612

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

273

612

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

274

612

275

612

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

276

612

    let mut found_non_one_coeff = false;

277

278

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

279

2244

    for expr in sum_exprs {

280

1632

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

281

            // atom: v ~> 1*v

282

1139

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

283

284

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

285

286

            // weighted sum term: c * e.

287

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

288

            // flattening

289

255

            Expr::Product(_, factors)

290

255

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

291

255

292

255

                match &factors[..] {

293

                    // c * <atom>

294

221

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

295

221

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

296

297

298

                    // c * <some non-flat expression>

299

17

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

300

17

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

301

17

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

302

17

303

17

                        symbols = aux_var_info.symbols();

304

17

                        let var = aux_var_info.as_atom();

305

17

                        new_top_exprs.push(aux_var_info.top_level_expr());

306

17

                        (c.clone(), var)

307

308

309

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

310

17

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

311

17

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

312

17

313

17

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

314

17

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

315

17

316

17

                        symbols = aux_var_info.symbols();

317

17

                        let var = aux_var_info.as_atom();

318

17

                        new_top_exprs.push(aux_var_info.top_level_expr());

319

17

                        (c.clone(), var)

320

321

322

                    _ => unreachable!(),

323

324

325

326

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

327

//

328

            // flatten e if non-atomic

329

102

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

330

                // needs flattening

331

102

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

332

17

                    symbols = aux_var_info.symbols();

333

17

                    new_top_exprs.push(aux_var_info.top_level_expr());

334

17

                    aux_var_info.as_atom()

335

                } else {

336

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

337

                    #[allow(clippy::unwrap_used)]

338

85

                    e.try_into().unwrap()

339

};

340

341

102

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

342

343

344

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

345

//

346

            // includes products without coefficients.

347

136

            e => {

348

//

349

136

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

350

351

136

                symbols = aux_var_info.symbols();

352

136

                let var = aux_var_info.as_atom();

353

136

                new_top_exprs.push(aux_var_info.top_level_expr());

354

136

                (Lit::Int(1), var)

355

356

};

357

358

1632

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

359

1632

        found_non_one_coeff |= coeff_num != 1;

360

1632

        coefficients.push(coeff);

361

1632

        vars.push(var);

362

363

364

612

    let use_weighted_sum = found_non_one_coeff;

365

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

366

612

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

367

68

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

368

68

            Metadata::new(),

369

68

            vec![

370

68

                Expr::FlatWeightedSumLeq(

371

68

                    Metadata::new(),

372

68

                    coefficients.clone(),

373

68

                    vars.clone(),

374

68

                    total.clone(),

375

68

),

376

68

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

377

68

],

378

68

),

379

289

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

380

289

            Metadata::new(),

381

289

            vec![

382

289

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

383

289

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

384

289

],

385

289

),

386

        (EqualityKind::Leq, true) => {

387

51

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

388

389

68

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

390

        (EqualityKind::Geq, true) => {

391

17

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

392

393

119

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

394

};

395

396

612

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

397

200991

398

399

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

400

76670

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

401

76670

    // div = val

402

76670

    let val: Atom;

403

76670

    let div: Expr;

404

76670

    let meta: Metadata;

405

76670

406

76670

    match expr.clone() {

407

4913

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

408

4913

            meta = m;

409

4913

410

4913

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

411

4913

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

412

413

4913

            if let Some(f) = a_atom {

414

4369

                // val = div

415

4369

                val = f.clone();

416

4369

                div = *b;

417

4369

            } else if let Some(f) = b_atom {

418

544

                // div = val

419

544

                val = f.clone();

420

544

                div = *a;

421

544

            } else {

422

                return Err(RuleNotApplicable);

423

424

425

663

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

426

663

            meta = m;

427

663

            val = name.into();

428

663

            div = *e;

429

663

430

        _ => {

431

71094

            return Err(RuleNotApplicable);

432

433

434

435

5576

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

436

4896

        return Err(RuleNotApplicable);

437

680

438

680

439

680

    let children = div.children();

440

680

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

441

612

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

442

443

561

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

444

561

        meta.clone_dirty(),

445

561

        a.clone(),

446

561

        b.clone(),

447

561

        val,

448

561

)))

449

76670

450

451

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

452

76670

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

453

76670

    // div = val

454

76670

    let val: Atom;

455

76670

    let div: Expr;

456

76670

    let meta: Metadata;

457

76670

458

76670

    match expr.clone() {

459

4913

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

460

4913

            meta = m;

461

4913

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

462

4913

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

463

464

4913

            if let Some(f) = a_atom {

465

4369

                // val = div

466

4369

                val = f.clone();

467

4369

                div = *b;

468

4369

            } else if let Some(f) = b_atom {

469

544

                // div = val

470

544

                val = f.clone();

471

544

                div = *a;

472

544

            } else {

473

                return Err(RuleNotApplicable);

474

475

476

663

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

477

663

            meta = m;

478

663

            val = name.into();

479

663

            div = *e;

480

663

481

        _ => {

482

71094

            return Err(RuleNotApplicable);

483

484

485

486

5576

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

487

5134

        return Err(RuleNotApplicable);

488

442

489

442

490

442

    let children = div.children();

491

442

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

492

442

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

493

494

391

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

495

391

        meta.clone_dirty(),

496

391

        a.clone(),

497

391

        b.clone(),

498

391

        val,

499

391

)))

500

76670

501

502

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

503

169983

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

504

169983

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

505

13158

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

506

13158

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

507

13158

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

508

509

13158

            if let Some(a_atom) = a_atom {

510

7429

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

511

5729

            } else if let Some(b_atom) = b_atom {

512

5729

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

513

            } else {

514

                Err(RuleNotApplicable)

515

516

517

518

1853

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

519

520

154972

        _ => Err(RuleNotApplicable),

521

154972

}?;

522

523

15011

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

524

14858

        return Err(RuleNotApplicable);

525

};

526

527

153

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

528

529

136

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

530

169983

531

532

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

533

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

534

76670

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

535

76670

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

536

4913

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

537

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

538

102

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

539

4811

            _ => Err(RuleNotApplicable),

540

},

541

71757

        _ => Err(RuleNotApplicable),

542

76568

}?;

543

544

102

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

545

85

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

546

547

85

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

548

85

        Metadata::new(),

549

85

a,

550

85

b,

551

85

        total,

552

85

)))

553

76670

554

555

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

556

///

557

/// ```text

558

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

559

///

560

///   where x,y are atoms

561

/// ```

562

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

563

169983

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

564

169983

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

565

156825

        return Err(RuleNotApplicable);

566

};

567

568

26282

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

569

26282

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

570

20179

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

571

20128

            return None;

572

};

573

574

51

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

575

576

34

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

577

26282

578

579

13158

    let a = *a.clone();

580

13158

    let b = *b.clone();

581

582

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

583

13158

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

584

13124

        return Err(RuleNotApplicable);

585

};

586

587

34

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

588

169983

589

590

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

591

///

592

/// ```text

593

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

594

///

595

///   where x,y are atoms

596

/// ```

597

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

598

169983

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

599

    // a =aux -b

600

//

601

169983

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

602

168130

        return Err(RuleNotApplicable);

603

};

604

605

1853

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

606

607

1853

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

608

1785

        return Err(RuleNotApplicable);

609

};

610

611

68

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

612

34

        return Err(RuleNotApplicable);

613

};

614

615

34

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

616

169983

617

618

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

619

///

620

/// ```text

621

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

622

/// where x is atomic, y is atomic

623

///

624

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

625

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

626

/// ```

627

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

628

169983

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

629

169983

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

630

165903

        return Err(RuleNotApplicable);

631

};

632

633

4080

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

634

635

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

636

//

637

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

638

374

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

639

102

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

640

102

            Metadata::new(),

641

102

            x_atom.clone(),

642

102

            y_atom.clone(),

643

102

            0.into(),

644

102

)))

645

    } else {

646

272

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

647

272

            Metadata::new(),

648

272

            y.clone(),

649

272

            x_atom.clone(),

650

272

)))

651

652

169983

653

654

/// Flattens an implication.

655

///

656

/// ```text

657

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

658

///  ~~>

659

/// __0 -> y,

660

///

661

/// with new top level constraints

662

/// __0 =aux x

663

///

664

/// ```

665

///

666

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

667

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

668

/// an argument:

669

///

670

/// ``` text

671

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

672

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

673

/// ```

674

///

675

/// See [`introduce_reifyimply_ineq_from_imply`].

676

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

677

76670

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

678

76670

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

679

76347

        return Err(RuleNotApplicable);

680

};

681

682

    // flatten x

683

323

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

684

685

323

    let symbols = aux_var_info.symbols();

686

323

    let new_x = aux_var_info.as_expr();

687

323

688

323

    Ok(Reduction::new(

689

323

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

690

323

        vec![aux_var_info.top_level_expr()],

691

323

        symbols,

692

323

))

693

76670

694

695

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

696

76670

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

697

68527

    if !matches!(

698

76670

        expr,

699

        Expr::SafeDiv(_, _, _)

700

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

701

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

702

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

703

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

704

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

705

            | Expr::Abs(_, _)

706

            | Expr::Product(_, _)

707

            | Expr::Neg(_, _)

708

            | Expr::Not(_, _)

709

) {

710

68527

        return Err(RuleNotApplicable);

711

8143

712

8143

713

8143

    let mut children = expr.children();

714

8143

715

8143

    let mut symbols = symbols.clone();

716

8143

    let mut num_changed = 0;

717

8143

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

718

719

15572

    for child in children.iter_mut() {

720

15572

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

721

612

            symbols = aux_var_info.symbols();

722

612

            new_tops.push(aux_var_info.top_level_expr());

723

612

            *child = aux_var_info.as_expr();

724

612

            num_changed += 1;

725

14960

726

727

728

8143

    if num_changed == 0 {

729

7548

        return Err(RuleNotApplicable);

730

595

731

595

732

595

    let expr = expr.with_children(children);

733

595

734

595

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

735

76670

736

737

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

738

76670

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

739

76670

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

740

71757

        return Err(RuleNotApplicable);

741

4913

742

4913

743

4913

    let mut children = expr.children();

744

4913

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

745

746

4913

    let mut symbols = symbols.clone();

747

4913

    let mut num_changed = 0;

748

4913

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

749

750

9826

    for child in children.iter_mut() {

751

9826

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

752

680

            symbols = aux_var_info.symbols();

753

680

            new_tops.push(aux_var_info.top_level_expr());

754

680

            *child = aux_var_info.as_expr();

755

680

            num_changed += 1;

756

9146

757

758

759

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

760

4913

    if num_changed != 2 {

761

4913

        return Err(RuleNotApplicable);

762

763

764

    let expr = expr.with_children(children);

765

766

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

767

76670

768

769

/// Converts a Geq to an Ineq

770

///

771

/// ```text

772

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

773

/// ```

774

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

775

26248

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

776

26248

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

777

25908

        return Err(RuleNotApplicable);

778

};

779

780

340

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

781

        return Err(RuleNotApplicable);

782

};

783

784

340

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

785

        return Err(RuleNotApplicable);

786

};

787

788

340

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

789

340

        meta.clone_dirty(),

790

340

y,

791

340

x,

792

340

        Lit::Int(0),

793

340

)))

794

26248

795

796

/// Converts a Leq to an Ineq

797

///

798

/// ```text

799

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

800

/// ```

801

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

802

26248

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

803

26248

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

804

25653

        return Err(RuleNotApplicable);

805

};

806

807

595

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

808

        return Err(RuleNotApplicable);

809

};

810

811

595

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

812

        return Err(RuleNotApplicable);

813

};

814

815

595

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

816

595

        meta.clone_dirty(),

817

595

x,

818

595

y,

819

595

        Lit::Int(0),

820

595

)))

821

26248

822

823

// TODO: add this rule for geq

824

825

/// ```text

826

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

827

/// ```

828

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

829

197914

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

830

197914

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

831

185300

        return Err(RuleNotApplicable);

832

};

833

834

12614

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

835

17

        return Err(RuleNotApplicable);

836

};

837

838

12597

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

839

12580

        return Err(RuleNotApplicable);

840

};

841

842

17

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

843

17

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

844

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

845

        _ => {

846

            return Err(RuleNotApplicable);

847

848

};

849

850

17

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

851

17

        meta.clone_dirty(),

852

17

x,

853

17

        y.clone(),

854

17

        k.clone(),

855

17

)))

856

197914

857

858

/// ```text

859

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

860

/// ```

861

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

862

206040

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

863

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

864

206040

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

865

204765

        return Err(RuleNotApplicable);

866

};

867

868

1275

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

869

        return Err(RuleNotApplicable);

870

};

871

872

1275

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

873

1190

        return Err(RuleNotApplicable);

874

};

875

876

85

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

877

34

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

878

17

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

879

        _ => {

880

34

            return Err(RuleNotApplicable);

881

882

};

883

884

51

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

885

51

        meta.clone_dirty(),

886

51

x,

887

51

        y.clone(),

888

51

        k.clone(),

889

51

)))

890

206040

891

892

/// Flattening rule for not(bool_lit)

893

///

894

/// For some boolean variable x:

895

/// ```text

896

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

897

/// ```

898

///

899

/// ## Rationale

900

///

901

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

902

///

903

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

904

///

905

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

906

/// trivial match).

907

908

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

909

26248

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

910

    use Domain::BoolDomain;

911

26248

    match expr {

912

85

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

913

85

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

914

85

                if symbols

915

85

                    .domain(&name)

916

85

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

917

918

85

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

919

85

                        m.clone_dirty(),

920

85

                        name.clone(),

921

85

                        Lit::Bool(false),

922

85

                    )));

923

924

925

            Err(RuleNotApplicable)

926

927

26163

        _ => Err(RuleNotApplicable),

928

929

26248

930

931

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

932

///

933

/// ```text

934

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

935

/// ```

936

///

937

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

938

/// nested expressions are constraints not variables.

939

940

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

941

11662

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

942

11662

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

943

11662

        return Err(RuleNotApplicable);

944

945

946

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

947

        unreachable!();

948

};

949

950

    extra_check! {

951

        if !is_flat(e) {

952

            return Err(RuleNotApplicable);

953

954

};

955

956

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

957

        m.clone(),

958

        e.clone(),

959

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

960

)))

961

11662

962

963

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

964

///

965

/// ```text

966

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

967

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

968

///

969

/// where c is a boolean constraint

970

/// ```

971

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

972

169983

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

973

169983

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

974

1853

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

975

13158

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

976

7429

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

977

5729

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

978

            _ => Err(RuleNotApplicable),

979

},

980

981

154972

        _ => Err(RuleNotApplicable),

982

154972

}?;

983

984

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

985

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

986

15011

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

987

14620

        return Err(RuleNotApplicable);

988

};

989

990

391

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

991

391

        Metadata::new(),

992

391

        e.clone(),

993

391

        atom,

994

391

)))

995

169983