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

3434

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

23

13158

    for e in exprs {

24

9894

        if let Sum(_, _) = e {

25

170

            return true;

26

9724

27

28

3264

    false

29

3434

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

5831

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

35

5831

    match expr {

36

3434

        Sum(_, exprs) => {

37

3434

            if is_nested_sum(exprs) {

38

170

                Err(RuleNotApplicable)

39

            } else {

40

3264

                Ok(exprs.clone())

41

42

43

2397

        _ => Err(RuleNotApplicable),

44

45

5831

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

8217324

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

75

8217324

    match expr {

76

272

        Geq(metadata, a, b) => {

77

272

            let exprs = sum_to_vector(a)?;

78

34

            Ok(Reduction::pure(SumGeq(

79

34

                metadata.clone_dirty(),

80

34

                exprs,

81

34

                b.clone(),

82

34

)))

83

84

8217052

        _ => Err(RuleNotApplicable),

85

86

8217324

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

8217324

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

96

8217324

    match expr {

97

374

        Leq(metadata, a, b) => {

98

374

            let exprs = sum_to_vector(a)?;

99

68

            Ok(Reduction::pure(SumLeq(

100

68

                metadata.clone_dirty(),

101

68

                exprs,

102

68

                b.clone(),

103

68

)))

104

105

8216950

        _ => Err(RuleNotApplicable),

106

107

8217324

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

8217307

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

117

8217307

    match expr {

118

4165

        Eq(metadata, a, b) => {

119

4165

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

120

3145

                Ok(Reduction::pure(SumEq(

121

3145

                    metadata.clone_dirty(),

122

3145

                    exprs,

123

3145

                    b.clone(),

124

3145

)))

125

1020

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

126

17

                Ok(Reduction::pure(SumEq(

127

17

                    metadata.clone_dirty(),

128

17

                    exprs,

129

17

                    a.clone(),

130

17

)))

131

            } else {

132

1003

                Err(RuleNotApplicable)

133

134

135

8213142

        _ => Err(RuleNotApplicable),

136

137

8217307

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

8217307

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

156

8217307

    match expr {

157

3196

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

158

3196

            Metadata::new(),

159

3196

            vec![

160

3196

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

161

3196

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

162

3196

],

163

3196

        ))),

164

8214111

        _ => Err(RuleNotApplicable),

165

166

8217307

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

8217324

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

177

8217324

    match expr {

178

3111

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

179

3111

            metadata.clone_dirty(),

180

3111

            a.clone(),

181

3111

            b.clone(),

182

3111

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

183

3111

        ))),

184

8214213

        _ => Err(RuleNotApplicable),

185

186

8217324

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

8217307

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

197

8217307

    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

8217307

        _ => Err(RuleNotApplicable),

205

206

8217307

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

8217307

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

217

8217307

    match expr {

218

255

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

219

255

            metadata.clone_dirty(),

220

255

            b.clone(),

221

255

            a.clone(),

222

255

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

223

255

        ))),

224

8217052

        _ => Err(RuleNotApplicable),

225

226

8217307

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

8217307

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

237

8217307

    match expr {

238

357

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

239

357

            metadata.clone_dirty(),

240

357

            a.clone(),

241

357

            b.clone(),

242

357

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

243

357

        ))),

244

8216950

        _ => Err(RuleNotApplicable),

245

246

8217307

247

248

/// ```text

249

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

250

/// ```

251

252

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

253

8217307

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

254

8217307

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

255

8216950

        return Err(RuleNotApplicable);

256

};

257

258

357

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

259

119

        return Err(RuleNotApplicable);

260

};

261

262

238

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

263

221

        return Err(RuleNotApplicable);

264

};

265

266

17

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

267

        return Err(RuleNotApplicable);

268

};

269

270

17

    Ok(Reduction::pure(Ineq(

271

17

        expr.get_meta().clone_dirty(),

272

17

        Box::new(x),

273

17

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

274

17

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

275

17

)))

276

8217307

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

8217307

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

299

8217307

    let mut mdl = mdl.clone();

300

8217307

    match expr {

301

4165

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

302

357

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

303

255

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

304

221

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

305

        _ => {

306

8212309

            return Err(RuleNotApplicable);

307

308

309

310

4998

    let mut sub = expr.children();

311

4998

312

4998

    let mut new_top = vec![];

313

4998

314

4998

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

315

4998

    let mut num_changed = 0;

316

9996

    for c in sub.iter_mut() {

317

9996

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

318

102

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

319

102

                num_changed += 1;

320

102

                mdl = aux_var_info.model();

321

102

                new_top.push(DivEq(

322

102

                    Metadata::new(),

323

102

                    a.clone(),

324

102

                    b.clone(),

325

102

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

326

102

));

327

102

                *c = aux_var_info.as_expr();

328

102

329

9894

330

331

332

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

333

4998

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

334

4386

        return Err(RuleNotApplicable);

335

612

336

612

337

612

    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

612

344

612

    Err(RuleNotApplicable)

345

8217307

346

347

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

348

8217307

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

349

8217307

    let negated = match expr {

350

4165

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

351

221

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

352

        _ => {

353

8212921

            return Err(RuleNotApplicable);

354

355

};

356

4386

    let metadata = expr.get_meta();

357

4386

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

358

4386

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

359

360

4386

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

361

51

        match b {

362

51

            FactorE(_, _) => {}

363

            _ => {

364

                return Err(RuleNotApplicable);

365

366

};

367

368

51

        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

51

            Ok(Reduction::pure(DivEq(

380

51

                metadata.clone_dirty(),

381

51

                x.clone(),

382

51

                y.clone(),

383

51

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

384

51

)))

385

386

4335

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

387

51

        match a {

388

51

            FactorE(_, _) => {}

389

            _ => {

390

                return Err(RuleNotApplicable);

391

392

};

393

394

51

        if negated {

395

17

            Ok(Reduction::pure(Not(

396

17

                metadata.clone_dirty(),

397

17

                Box::new(DivEq(

398

17

                    Metadata::new(),

399

17

                    x.clone(),

400

17

                    y.clone(),

401

17

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

402

17

)),

403

17

)))

404

        } else {

405

34

            Ok(Reduction::pure(DivEq(

406

34

                metadata.clone_dirty(),

407

34

                x.clone(),

408

34

                y.clone(),

409

34

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

410

34

)))

411

412

    } else {

413

4284

        Err(RuleNotApplicable)

414

415

8217307

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

8217307

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

434

    use Domain::BoolDomain;

435

8217307

    match expr {

436

428298

        Or(m, vec) => {

437

428298

            let mut changed = false;

438

428298

            let mut new_vec = Vec::new();

439

2092972

            for expr in vec {

440

1664674

                new_vec.push(match expr {

441

170

                    FactorE(m, Reference(name))

442

170

                        if mdl

443

170

                            .get_domain(name)

444

170

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

445

446

170

                        changed = true;

447

170

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

448

449

1664504

                    e => e.clone(),

450

});

451

452

453

428298

            if !changed {

454

428196

                return Err(RuleNotApplicable);

455

102

456

102

457

102

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

458

459

18989

        And(m, vec) => {

460

18989

            let mut changed = false;

461

18989

            let mut new_vec = Vec::new();

462

613870

            for expr in vec {

463

594881

                new_vec.push(match expr {

464

85

                    FactorE(m, Reference(name))

465

85

                        if mdl

466

85

                            .get_domain(name)

467

85

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

468

469

85

                        changed = true;

470

85

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

471

472

594796

                    e => e.clone(),

473

});

474

475

476

18989

            if !changed {

477

18904

                return Err(RuleNotApplicable);

478

85

479

85

480

85

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

481

482

483

68

        Not(m, expr) => {

484

68

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

485

34

                if mdl

486

34

                    .get_domain(&name)

487

34

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

488

489

34

                    return Ok(Reduction::pure(WatchedLiteral(

490

34

                        m.clone_dirty(),

491

34

                        name.clone(),

492

34

                        Bool(false),

493

34

                    )));

494

495

34

496

34

            Err(RuleNotApplicable)

497

498

7769952

        _ => Err(RuleNotApplicable),

499

500

8217307

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

8217307

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

513

8217273

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

514

8217273

        return Err(RuleNotApplicable);

515

34

516

517

34

    let Not(m, e) = expr else {

518

        unreachable!();

519

};

520

521

34

    Ok(Reduction::pure(Reify(

522

34

        m.clone(),

523

34

        e.clone(),

524

34

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

525

34

)))

526

8217307