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

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

19

20

3030

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

21

11610

    for e in exprs {

22

8730

        if let Sum(_, _) = e {

23

150

            return true;

24

8580

25

26

2880

    false

27

3030

28

29

/**

30

 * 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)

31

*/

32

5145

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

33

5145

    match expr {

34

3030

        Sum(_, exprs) => {

35

3030

            if is_nested_sum(exprs) {

36

150

                Err(RuleNotApplicable)

37

            } else {

38

2880

                Ok(exprs.clone())

39

40

41

2115

        _ => Err(RuleNotApplicable),

42

43

5145

44

45

// /**

46

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

47

//  * ```text

48

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

49

//  * ```

50

//  */

51

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

52

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

53

//     match expr {

54

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

55

//             metadata.clone_dirty(),

56

//             vec![

57

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

58

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

59

//             ],

60

//         ))),

61

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

62

//     }

63

// }

64

65

/**

66

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

67

 * ```text

68

1

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

69

1

 * ```

70

1

*/

71

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

72

7250580

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

73

7250580

    match expr {

74

240

        Geq(metadata, a, b) => {

75

240

            let exprs = sum_to_vector(a)?;

76

30

            Ok(Reduction::pure(SumGeq(

77

30

                metadata.clone_dirty(),

78

30

                exprs,

79

30

                b.clone(),

80

30

)))

81

82

7250340

        _ => Err(RuleNotApplicable),

83

84

7250580

85

86

/**

87

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

88

 * ```text

89

1

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

90

1

 * ```

91

1

*/

92

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

93

7250580

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

94

7250580

    match expr {

95

330

        Leq(metadata, a, b) => {

96

330

            let exprs = sum_to_vector(a)?;

97

60

            Ok(Reduction::pure(SumLeq(

98

60

                metadata.clone_dirty(),

99

60

                exprs,

100

60

                b.clone(),

101

60

)))

102

103

7250250

        _ => Err(RuleNotApplicable),

104

105

7250580

106

107

/**

108

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

109

 * ```text

110

1

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

111

1

 * ```

112

1

*/

113

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

114

7250565

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

115

7250565

    match expr {

116

3675

        Eq(metadata, a, b) => {

117

3675

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

118

2775

                Ok(Reduction::pure(SumEq(

119

2775

                    metadata.clone_dirty(),

120

2775

                    exprs,

121

2775

                    b.clone(),

122

2775

)))

123

900

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

124

15

                Ok(Reduction::pure(SumEq(

125

15

                    metadata.clone_dirty(),

126

15

                    exprs,

127

15

                    a.clone(),

128

15

)))

129

            } else {

130

885

                Err(RuleNotApplicable)

131

132

133

7246890

        _ => Err(RuleNotApplicable),

134

135

7250565

136

137

/**

138

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

139

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

140

 * ```text

141

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

142

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

143

 *   sumgeq([a, b], c)

144

1

 * })

145

1

 * ```

146

1

 * I. e.

147

 * ```text

148

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

149

1

 * a + b = c

150

1

 * ```

151

1

*/

152

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

153

7250565

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

154

7250565

    match expr {

155

2820

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

156

2820

            Metadata::new(),

157

2820

            vec![

158

2820

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

159

2820

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

160

2820

],

161

2820

        ))),

162

7247745

        _ => Err(RuleNotApplicable),

163

164

7250565

165

166

/**

167

* Convert a Lt to an Ineq:

168

169

* ```text

170

1

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

171

1

* ```

172

1

*/

173

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

174

7250580

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

175

7250580

    match expr {

176

2745

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

177

2745

            metadata.clone_dirty(),

178

2745

            a.clone(),

179

2745

            b.clone(),

180

2745

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

181

2745

        ))),

182

7247835

        _ => Err(RuleNotApplicable),

183

184

7250580

185

186

/**

187

* Convert a Gt to an Ineq:

188

189

* ```text

190

1

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

191

1

* ```

192

1

*/

193

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

194

7250565

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

195

7250565

    match expr {

196

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

197

            metadata.clone_dirty(),

198

            b.clone(),

199

            a.clone(),

200

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

201

        ))),

202

7250565

        _ => Err(RuleNotApplicable),

203

204

7250565

205

206

/**

207

* Convert a Geq to an Ineq:

208

209

* ```text

210

1

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

211

1

* ```

212

1

*/

213

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

214

7250565

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

215

7250565

    match expr {

216

225

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

217

225

            metadata.clone_dirty(),

218

225

            b.clone(),

219

225

            a.clone(),

220

225

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

221

225

        ))),

222

7250340

        _ => Err(RuleNotApplicable),

223

224

7250565

225

226

/**

227

* Convert a Leq to an Ineq:

228

229

* ```text

230

1

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

231

1

* ```

232

1

*/

233

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

234

7250565

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

235

7250565

    match expr {

236

315

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

237

315

            metadata.clone_dirty(),

238

315

            a.clone(),

239

315

            b.clone(),

240

315

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

241

315

        ))),

242

7250250

        _ => Err(RuleNotApplicable),

243

244

7250565

245

246

/// ```text

247

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

248

/// ```

249

250

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

251

7250565

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

252

7250565

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

253

7250250

        return Err(RuleNotApplicable);

254

};

255

256

315

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

257

105

        return Err(RuleNotApplicable);

258

};

259

260

210

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

261

195

        return Err(RuleNotApplicable);

262

};

263

264

15

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

265

        return Err(RuleNotApplicable);

266

};

267

268

15

    Ok(Reduction::pure(Ineq(

269

15

        expr.get_meta().clone_dirty(),

270

15

        Box::new(x),

271

15

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

272

15

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

273

15

)))

274

7250565

275

276

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

277

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

278

//     match expr {

279

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

280

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

281

//                 metadata.clone(),

282

//                 vec![

283

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

284

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

285

//                 ],

286

//             )));

287

//         }

288

//         _ => Err(RuleNotApplicable),

289

//     }

290

// }

291

292

/**

293

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

294

*/

295

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

296

7250565

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

297

7250565

    match expr {

298

3675

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

299

315

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

300

225

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

301

195

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

302

        _ => {

303

7246155

            return Err(RuleNotApplicable);

304

305

306

307

4410

    let mut sub = expr.children();

308

4410

309

4410

    let mut new_vars = SymbolTable::new();

310

4410

    let mut new_top = vec![];

311

4410

312

4410

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

313

4410

    let mut num_changed = 0;

314

8820

    for c in sub.iter_mut() {

315

8820

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

316

90

            num_changed += 1;

317

90

            let new_name = mdl.gensym();

318

90

            let domain = c

319

90

                .domain_of(&mdl.variables)

320

90

                .ok_or(ApplicationError::DomainError)?;

321

90

            new_vars.insert(new_name.clone(), DecisionVariable::new(domain));

322

90

323

90

            new_top.push(DivEq(

324

90

                Metadata::new(),

325

90

                a.clone(),

326

90

                b.clone(),

327

90

                Box::new(FactorE(Metadata::new(), Reference(new_name.clone()))),

328

90

));

329

90

330

90

            *c = FactorE(Metadata::new(), Reference(new_name.clone()));

331

8730

332

333

334

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

335

4410

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

336

3870

        return Err(RuleNotApplicable);

337

540

338

540

339

540

    if !new_top.is_empty() {

340

        return Ok(Reduction::new(

341

            expr.with_children(sub),

342

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

343

            new_vars,

344

));

345

540

346

540

    Err(RuleNotApplicable)

347

7250565

348

349

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

350

7250565

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

351

7250565

    let negated = match expr {

352

3675

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

353

195

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

354

        _ => {

355

7246695

            return Err(RuleNotApplicable);

356

357

};

358

3870

    let metadata = expr.get_meta();

359

3870

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

360

3870

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

361

362

3870

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

363

45

        match b {

364

45

            FactorE(_, _) => {}

365

            _ => {

366

                return Err(RuleNotApplicable);

367

368

};

369

370

45

        if negated {

371

            Ok(Reduction::pure(Not(

372

                metadata.clone_dirty(),

373

                Box::new(DivEq(

374

                    Metadata::new(),

375

                    x.clone(),

376

                    y.clone(),

377

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

378

)),

379

)))

380

        } else {

381

45

            Ok(Reduction::pure(DivEq(

382

45

                metadata.clone_dirty(),

383

45

                x.clone(),

384

45

                y.clone(),

385

45

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

386

45

)))

387

388

3825

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

389

45

        match a {

390

45

            FactorE(_, _) => {}

391

            _ => {

392

                return Err(RuleNotApplicable);

393

394

};

395

396

45

        if negated {

397

15

            Ok(Reduction::pure(Not(

398

15

                metadata.clone_dirty(),

399

15

                Box::new(DivEq(

400

15

                    Metadata::new(),

401

15

                    x.clone(),

402

15

                    y.clone(),

403

15

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

404

15

)),

405

15

)))

406

        } else {

407

30

            Ok(Reduction::pure(DivEq(

408

30

                metadata.clone_dirty(),

409

30

                x.clone(),

410

30

                y.clone(),

411

30

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

412

30

)))

413

414

    } else {

415

3780

        Err(RuleNotApplicable)

416

417

7250565

418

419

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

420

///

421

/// For some boolean variable x:

422

/// ```text

423

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

424

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

425

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

426

/// ```

427

///

428

/// ## Rationale

429

///

430

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

431

///

432

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

433

///

434

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

435

7250565

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

436

    use Domain::BoolDomain;

437

7250565

    match expr {

438

377910

        Or(m, vec) => {

439

377910

            let mut changed = false;

440

377910

            let mut new_vec = Vec::new();

441

1846740

            for expr in vec {

442

1468830

                new_vec.push(match expr {

443

150

                    FactorE(m, Reference(name))

444

150

                        if mdl

445

150

                            .get_domain(name)

446

150

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

447

448

150

                        changed = true;

449

150

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

450

451

1468680

                    e => e.clone(),

452

});

453

454

455

377910

            if !changed {

456

377820

                return Err(RuleNotApplicable);

457

90

458

90

459

90

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

460

461

16755

        And(m, vec) => {

462

16755

            let mut changed = false;

463

16755

            let mut new_vec = Vec::new();

464

541650

            for expr in vec {

465

524895

                new_vec.push(match expr {

466

75

                    FactorE(m, Reference(name))

467

75

                        if mdl

468

75

                            .get_domain(name)

469

75

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

470

471

75

                        changed = true;

472

75

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

473

474

524820

                    e => e.clone(),

475

});

476

477

478

16755

            if !changed {

479

16680

                return Err(RuleNotApplicable);

480

75

481

75

482

75

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

483

484

485

60

        Not(m, expr) => {

486

60

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

487

30

                if mdl

488

30

                    .get_domain(&name)

489

30

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

490

491

30

                    return Ok(Reduction::pure(WatchedLiteral(

492

30

                        m.clone_dirty(),

493

30

                        name.clone(),

494

30

                        Bool(false),

495

30

                    )));

496

497

30

498

30

            Err(RuleNotApplicable)

499

500

6855840

        _ => Err(RuleNotApplicable),

501

502

7250565

503

504

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

505

///

506

/// ```text

507

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

508

/// ```

509

///

510

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

511

/// nested expressions are constraints not variables.

512

513

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

514

7250565

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

515

7250535

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

516

7250535

        return Err(RuleNotApplicable);

517

30

518

519

30

    let Not(m, e) = expr else {

520

        unreachable!();

521

};

522

523

30

    Ok(Reduction::pure(Reify(

524

30

        m.clone(),

525

30

        e.clone(),

526

30

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

527

30

)))

528

7250565