Grcov report - minion.rs

1

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

2

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

3

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

4

5

use crate::ast::{

6

    DecisionVariable, Domain, Expression as Expr, Expression::*, Factor::*, Literal::*, SymbolTable,

7

};

8

use crate::metadata::Metadata;

9

use crate::rule_engine::{

10

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

11

};

12

13

use crate::solver::SolverFamily;

14

use crate::Model;

15

use uniplate::Uniplate;

16

use ApplicationError::RuleNotApplicable;

17

18

use super::utils::to_aux_var;

19

20

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

21

22

3030

fn is_nested_sum(exprs: &Vec<Expr>) -> bool {

23

11610

    for e in exprs {

24

8730

        if let Sum(_, _) = e {

25

150

            return true;

26

8580

27

28

2880

    false

29

3030

30

31

/**

32

 * Helper function to get the vector of expressions from a sum (or error if it's a nested sum - we need to flatten it first)

33

*/

34

5145

fn sum_to_vector(expr: &Expr) -> Result<Vec<Expr>, ApplicationError> {

35

5145

    match expr {

36

3030

        Sum(_, exprs) => {

37

3030

            if is_nested_sum(exprs) {

38

150

                Err(RuleNotApplicable)

39

            } else {

40

2880

                Ok(exprs.clone())

41

42

43

2115

        _ => Err(RuleNotApplicable),

44

45

5145

46

47

// /**

48

//  * Convert an Eq to a conjunction of Geq and Leq:

49

//  * ```text

50

//  * a = b => a >= b && a <= b

51

//  * ```

52

//  */

53

// #[register_rule(("Minion", 100))]

54

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

55

//     match expr {

56

//         Expr::Eq(metadata, a, b) => Ok(Reduction::pure(Expr::And(

57

//             metadata.clone_dirty(),

58

//             vec![

59

//                 Expr::Geq(metadata.clone_dirty(), a.clone(), b.clone()),

60

//                 Expr::Leq(metadata.clone_dirty(), a.clone(), b.clone()),

61

//             ],

62

//         ))),

63

//         _ => Err(ApplicationError::RuleNotApplicable),

64

//     }

65

// }

66

67

/**

68

 * Convert a Geq to a SumGeq if the left hand side is a sum:

69

 * ```text

70

1

 * sum([a, b, c]) >= d => sum_geq([a, b, c], d)

71

1

 * ```

72

1

*/

73

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

74

7250580

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

75

7250580

    match expr {

76

240

        Geq(metadata, a, b) => {

77

240

            let exprs = sum_to_vector(a)?;

78

30

            Ok(Reduction::pure(SumGeq(

79

30

                metadata.clone_dirty(),

80

30

                exprs,

81

30

                b.clone(),

82

30

)))

83

84

7250340

        _ => Err(RuleNotApplicable),

85

86

7250580

87

88

/**

89

 * Convert a Leq to a SumLeq if the left hand side is a sum:

90

 * ```text

91

1

 * sum([a, b, c]) <= d => sum_leq([a, b, c], d)

92

1

 * ```

93

1

*/

94

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

95

7250580

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

96

7250580

    match expr {

97

330

        Leq(metadata, a, b) => {

98

330

            let exprs = sum_to_vector(a)?;

99

60

            Ok(Reduction::pure(SumLeq(

100

60

                metadata.clone_dirty(),

101

60

                exprs,

102

60

                b.clone(),

103

60

)))

104

105

7250250

        _ => Err(RuleNotApplicable),

106

107

7250580

108

109

/**

110

 * Convert a 'Eq(Sum([...]))' to a SumEq

111

 * ```text

112

1

 * eq(sum([a, b]), c) => sumeq([a, b], c)

113

1

 * ```

114

1

*/

115

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

116

7250565

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

117

7250565

    match expr {

118

3675

        Eq(metadata, a, b) => {

119

3675

            if let Ok(exprs) = sum_to_vector(a) {

120

2775

                Ok(Reduction::pure(SumEq(

121

2775

                    metadata.clone_dirty(),

122

2775

                    exprs,

123

2775

                    b.clone(),

124

2775

)))

125

900

            } else if let Ok(exprs) = sum_to_vector(b) {

126

15

                Ok(Reduction::pure(SumEq(

127

15

                    metadata.clone_dirty(),

128

15

                    exprs,

129

15

                    a.clone(),

130

15

)))

131

            } else {

132

885

                Err(RuleNotApplicable)

133

134

135

7246890

        _ => Err(RuleNotApplicable),

136

137

7250565

138

139

/**

140

 * Convert a `SumEq` to an `And(SumGeq, SumLeq)`

141

 * This is a workaround for Minion not having support for a flat "equals" operation on sums

142

 * ```text

143

 * sumeq([a, b], c) -> watched_and({

144

 *   sumleq([a, b], c),

145

 *   sumgeq([a, b], c)

146

1

 * })

147

1

 * ```

148

1

 * I. e.

149

 * ```text

150

 * ((a + b) >= c) && ((a + b) <= c)

151

1

 * a + b = c

152

1

 * ```

153

1

*/

154

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

155

7250565

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

156

7250565

    match expr {

157

2820

        SumEq(_metadata, exprs, eq_to) => Ok(Reduction::pure(And(

158

2820

            Metadata::new(),

159

2820

            vec![

160

2820

                SumGeq(Metadata::new(), exprs.clone(), Box::from(*eq_to.clone())),

161

2820

                SumLeq(Metadata::new(), exprs.clone(), Box::from(*eq_to.clone())),

162

2820

],

163

2820

        ))),

164

7247745

        _ => Err(RuleNotApplicable),

165

166

7250565

167

168

/**

169

* Convert a Lt to an Ineq:

170

171

* ```text

172

1

* a < b ~> a <= b -1 ~> ineq(a,b,-1)

173

1

* ```

174

1

*/

175

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

176

7250580

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

177

7250580

    match expr {

178

2745

        Lt(metadata, a, b) => Ok(Reduction::pure(Ineq(

179

2745

            metadata.clone_dirty(),

180

2745

            a.clone(),

181

2745

            b.clone(),

182

2745

            Box::new(FactorE(Metadata::new(), Literal(Int(-1)))),

183

2745

        ))),

184

7247835

        _ => Err(RuleNotApplicable),

185

186

7250580

187

188

/**

189

* Convert a Gt to an Ineq:

190

191

* ```text

192

1

* a > b ~> b <= a -1 ~> ineq(b,a,-1)

193

1

* ```

194

1

*/

195

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

196

7250565

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

197

7250565

    match expr {

198

        Gt(metadata, a, b) => Ok(Reduction::pure(Ineq(

199

            metadata.clone_dirty(),

200

            b.clone(),

201

            a.clone(),

202

            Box::new(FactorE(Metadata::new(), Literal(Int(-1)))),

203

        ))),

204

7250565

        _ => Err(RuleNotApplicable),

205

206

7250565

207

208

/**

209

* Convert a Geq to an Ineq:

210

211

* ```text

212

1

* a >= b ~> b <= a + 0 ~> ineq(b,a,0)

213

1

* ```

214

1

*/

215

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

216

7250565

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

217

7250565

    match expr {

218

225

        Geq(metadata, a, b) => Ok(Reduction::pure(Ineq(

219

225

            metadata.clone_dirty(),

220

225

            b.clone(),

221

225

            a.clone(),

222

225

            Box::new(FactorE(Metadata::new(), Literal(Int(0)))),

223

225

        ))),

224

7250340

        _ => Err(RuleNotApplicable),

225

226

7250565

227

228

/**

229

* Convert a Leq to an Ineq:

230

231

* ```text

232

1

* a <= b ~> a <= b + 0 ~> ineq(a,b,0)

233

1

* ```

234

1

*/

235

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

236

7250565

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

237

7250565

    match expr {

238

315

        Leq(metadata, a, b) => Ok(Reduction::pure(Ineq(

239

315

            metadata.clone_dirty(),

240

315

            a.clone(),

241

315

            b.clone(),

242

315

            Box::new(FactorE(Metadata::new(), Literal(Int(0)))),

243

315

        ))),

244

7250250

        _ => Err(RuleNotApplicable),

245

246

7250565

247

248

/// ```text

249

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

250

/// ```

251

252

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

253

7250565

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

254

7250565

    let Leq(_, x, b) = expr else {

255

7250250

        return Err(RuleNotApplicable);

256

};

257

258

315

    let x @ FactorE(_, Reference(_)) = *x.to_owned() else {

259

105

        return Err(RuleNotApplicable);

260

};

261

262

210

    let Sum(_, c) = *b.to_owned() else {

263

195

        return Err(RuleNotApplicable);

264

};

265

266

15

    let [ref y @ FactorE(_, Reference(_)), ref k @ FactorE(_, Literal(_))] = c[..] else {

267

        return Err(RuleNotApplicable);

268

};

269

270

15

    Ok(Reduction::pure(Ineq(

271

15

        expr.get_meta().clone_dirty(),

272

15

        Box::new(x),

273

15

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

274

15

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

275

15

)))

276

7250565

277

278

// #[register_rule(("Minion", 99))]

279

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

280

//     match expr {

281

//         Eq(metadata, a, b) => {

282

//             return Ok(Reduction::pure(Expr::And(

283

//                 metadata.clone(),

284

//                 vec![

285

//                     Expr::Leq(metadata.clone(), a.clone(), b.clone()),

286

//                     Expr::Geq(metadata.clone(), a.clone(), b.clone()),

287

//                 ],

288

//             )));

289

//         }

290

//         _ => Err(RuleNotApplicable),

291

//     }

292

// }

293

294

/**

295

 * Since Minion doesn't support some constraints with div (e.g. leq, neq), we add an auxiliary variable to represent the division result.

296

*/

297

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

298

7250565

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

299

7250565

    let mut mdl = mdl.clone();

300

7250565

    match expr {

301

3675

        Eq(_, _, _) => {}

302

315

        Leq(_, _, _) => {}

303

225

        Geq(_, _, _) => {}

304

195

        Neq(_, _, _) => {}

305

        _ => {

306

7246155

            return Err(RuleNotApplicable);

307

308

309

310

4410

    let mut sub = expr.children();

311

4410

312

4410

    let mut new_top = vec![];

313

4410

314

4410

    // replace every safe div child with a reference to a new variable

315

4410

    let mut num_changed = 0;

316

8820

    for c in sub.iter_mut() {

317

8820

        if let SafeDiv(_, a, b) = c.clone() {

318

90

            if let Some(aux_var_info) = to_aux_var(c, &mdl) {

319

90

                num_changed += 1;

320

90

                mdl = aux_var_info.model();

321

90

                new_top.push(DivEq(

322

90

                    Metadata::new(),

323

90

                    a.clone(),

324

90

                    b.clone(),

325

90

                    Box::new(aux_var_info.as_expr()),

326

90

));

327

90

                *c = aux_var_info.as_expr();

328

90

329

8730

330

331

332

    //  want to turn Eq(a/b,c) into DivEq(a,b,c) instead, so this rule doesn't apply!

333

4410

    if num_changed <= 1 && matches!(expr, Eq(_, _, _) | Neq(_, _, _)) {

334

3870

        return Err(RuleNotApplicable);

335

540

336

540

337

540

    if !new_top.is_empty() {

338

        return Ok(Reduction::new(

339

            expr.with_children(sub),

340

            And(Metadata::new(), new_top),

341

            mdl.variables,

342

));

343

540

344

540

    Err(RuleNotApplicable)

345

7250565

346

347

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

348

7250565

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

349

7250565

    let negated = match expr {

350

3675

        Eq(_, _, _) => false,

351

195

        Neq(_, _, _) => true,

352

        _ => {

353

7246695

            return Err(RuleNotApplicable);

354

355

};

356

3870

    let metadata = expr.get_meta();

357

3870

    let a = expr.children()[0].clone();

358

3870

    let b = expr.children()[1].clone();

359

360

3870

    if let SafeDiv(_, x, y) = a {

361

45

        match b {

362

45

            FactorE(_, _) => {}

363

            _ => {

364

                return Err(RuleNotApplicable);

365

366

};

367

368

45

        if negated {

369

            Ok(Reduction::pure(Not(

370

                metadata.clone_dirty(),

371

                Box::new(DivEq(

372

                    Metadata::new(),

373

                    x.clone(),

374

                    y.clone(),

375

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

376

)),

377

)))

378

        } else {

379

45

            Ok(Reduction::pure(DivEq(

380

45

                metadata.clone_dirty(),

381

45

                x.clone(),

382

45

                y.clone(),

383

45

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

384

45

)))

385

386

3825

    } else if let SafeDiv(_, x, y) = b {

387

45

        match a {

388

45

            FactorE(_, _) => {}

389

            _ => {

390

                return Err(RuleNotApplicable);

391

392

};

393

394

45

        if negated {

395

15

            Ok(Reduction::pure(Not(

396

15

                metadata.clone_dirty(),

397

15

                Box::new(DivEq(

398

15

                    Metadata::new(),

399

15

                    x.clone(),

400

15

                    y.clone(),

401

15

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

402

15

)),

403

15

)))

404

        } else {

405

30

            Ok(Reduction::pure(DivEq(

406

30

                metadata.clone_dirty(),

407

30

                x.clone(),

408

30

                y.clone(),

409

30

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

410

30

)))

411

412

    } else {

413

3780

        Err(RuleNotApplicable)

414

415

7250565

416

417

/// Flattening rule that converts boolean variables to watched-literal constraints.

418

///

419

/// For some boolean variable x:

420

/// ```text

421

/// and([x,...]) ~> and([w-literal(x,1),..])

422

///  or([x,...]) ~>  or([w-literal(x,1),..])

423

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

424

/// ```

425

///

426

/// ## Rationale

427

///

428

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

429

///

430

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

431

///

432

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

433

7250565

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

434

    use Domain::BoolDomain;

435

7250565

    match expr {

436

377910

        Or(m, vec) => {

437

377910

            let mut changed = false;

438

377910

            let mut new_vec = Vec::new();

439

1846740

            for expr in vec {

440

1468830

                new_vec.push(match expr {

441

150

                    FactorE(m, Reference(name))

442

150

                        if mdl

443

150

                            .get_domain(name)

444

150

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

445

446

150

                        changed = true;

447

150

                        WatchedLiteral(m.clone_dirty(), name.clone(), Bool(true))

448

449

1468680

                    e => e.clone(),

450

});

451

452

453

377910

            if !changed {

454

377820

                return Err(RuleNotApplicable);

455

90

456

90

457

90

            Ok(Reduction::pure(Or(m.clone_dirty(), new_vec)))

458

459

16755

        And(m, vec) => {

460

16755

            let mut changed = false;

461

16755

            let mut new_vec = Vec::new();

462

541650

            for expr in vec {

463

524895

                new_vec.push(match expr {

464

75

                    FactorE(m, Reference(name))

465

75

                        if mdl

466

75

                            .get_domain(name)

467

75

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

468

469

75

                        changed = true;

470

75

                        WatchedLiteral(m.clone_dirty(), name.clone(), Bool(true))

471

472

524820

                    e => e.clone(),

473

});

474

475

476

16755

            if !changed {

477

16680

                return Err(RuleNotApplicable);

478

75

479

75

480

75

            Ok(Reduction::pure(And(m.clone_dirty(), new_vec)))

481

482

483

60

        Not(m, expr) => {

484

60

            if let FactorE(_, Reference(name)) = (**expr).clone() {

485

30

                if mdl

486

30

                    .get_domain(&name)

487

30

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

488

489

30

                    return Ok(Reduction::pure(WatchedLiteral(

490

30

                        m.clone_dirty(),

491

30

                        name.clone(),

492

30

                        Bool(false),

493

30

                    )));

494

495

30

496

30

            Err(RuleNotApplicable)

497

498

6855840

        _ => Err(RuleNotApplicable),

499

500

7250565

501

502

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

503

///

504

/// ```text

505

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

506

/// ```

507

///

508

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

509

/// nested expressions are constraints not variables.

510

511

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

512

7250565

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

513

7250535

    if !matches!(expr, Not(_,c) if !matches!(**c, FactorE(_,_))) {

514

7250535

        return Err(RuleNotApplicable);

515

30

516

517

30

    let Not(m, e) = expr else {

518

        unreachable!();

519

};

520

521

30

    Ok(Reduction::pure(Reify(

522

30

        m.clone(),

523

30

        e.clone(),

524

30

        Box::new(FactorE(Metadata::new(), Literal(Bool(false)))),

525

30

)))

526

7250565