Grcov report - minion.rs

1

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

2

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

3

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

4

5

use crate::ast::{

6

    Constant as Const, DecisionVariable, Domain, Expression as Expr, Range, SymbolTable,

7

};

8

use crate::metadata::Metadata;

9

use crate::rule_engine::{

10

    register_rule, register_rule_set, ApplicationError, ApplicationResult, Reduction,

11

};

12

use crate::solver::SolverFamily;

13

use crate::Model;

14

use uniplate::Uniplate;

15

16

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

17

18

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

19

    for e in exprs {

20

        if let Expr::Sum(_, _) = e {

21

            return true;

22

23

24

    false

25

26

27

/**

28

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

29

*/

30

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

31

    match expr {

32

        Expr::Sum(_, exprs) => {

33

            if is_nested_sum(exprs) {

34

                Err(ApplicationError::RuleNotApplicable)

35

            } else {

36

                Ok(exprs.clone())

37

38

39

        _ => Err(ApplicationError::RuleNotApplicable),

40

41

42

43

// /**

44

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

45

//  * ```text

46

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

47

//  * ```

48

//  */

49

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

50

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

51

//     match expr {

52

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

53

//             metadata.clone_dirty(),

54

//             vec![

55

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

56

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

57

//             ],

58

//         ))),

59

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

60

//     }

61

// }

62

63

/**

64

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

65

 * ```text

66

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

67

 * ```

68

*/

69

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

70

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

71

    match expr {

72

        Expr::Geq(metadata, a, b) => {

73

            let exprs = sum_to_vector(a)?;

74

            Ok(Reduction::pure(Expr::SumGeq(

75

                metadata.clone_dirty(),

76

                exprs,

77

                b.clone(),

78

)))

79

80

        _ => Err(ApplicationError::RuleNotApplicable),

81

82

83

84

/**

85

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

86

 * ```text

87

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

88

 * ```

89

*/

90

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

91

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

92

    match expr {

93

        Expr::Leq(metadata, a, b) => {

94

            let exprs = sum_to_vector(a)?;

95

            Ok(Reduction::pure(Expr::SumLeq(

96

                metadata.clone_dirty(),

97

                exprs,

98

                b.clone(),

99

)))

100

101

        _ => Err(ApplicationError::RuleNotApplicable),

102

103

104

105

/**

106

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

107

 * ```text

108

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

109

 * ```

110

*/

111

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

112

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

113

    match expr {

114

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

115

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

116

                Ok(Reduction::pure(Expr::SumEq(

117

                    metadata.clone_dirty(),

118

                    exprs,

119

                    b.clone(),

120

)))

121

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

122

                Ok(Reduction::pure(Expr::SumEq(

123

                    metadata.clone_dirty(),

124

                    exprs,

125

                    a.clone(),

126

)))

127

            } else {

128

                Err(ApplicationError::RuleNotApplicable)

129

130

131

        _ => Err(ApplicationError::RuleNotApplicable),

132

133

134

135

/**

136

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

137

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

138

 * ```text

139

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

140

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

141

 *   sumgeq([a, b], c)

142

 * })

143

 * ```

144

 * I. e.

145

 * ```text

146

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

147

 * a + b = c

148

 * ```

149

*/

150

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

151

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

152

    match expr {

153

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

154

            Metadata::new(),

155

            vec![

156

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

157

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

158

],

159

        ))),

160

        _ => Err(ApplicationError::RuleNotApplicable),

161

162

163

164

/**

165

* Convert a Lt to an Ineq:

166

167

* ```text

168

* a < b => a - b < -1

169

* ```

170

*/

171

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

172

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

173

    match expr {

174

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

175

            metadata.clone_dirty(),

176

            a.clone(),

177

            b.clone(),

178

            Box::new(Expr::Constant(Metadata::new(), Const::Int(-1))),

179

        ))),

180

        _ => Err(ApplicationError::RuleNotApplicable),

181

182

183

184

/**

185

* Convert a Gt to an Ineq:

186

187

* ```text

188

* a > b => b - a < -1

189

* ```

190

*/

191

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

192

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

193

    match expr {

194

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

195

            metadata.clone_dirty(),

196

            b.clone(),

197

            a.clone(),

198

            Box::new(Expr::Constant(Metadata::new(), Const::Int(-1))),

199

        ))),

200

        _ => Err(ApplicationError::RuleNotApplicable),

201

202

203

204

/**

205

* Convert a Geq to an Ineq:

206

207

* ```text

208

* a >= b => b - a < 0

209

* ```

210

*/

211

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

212

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

213

    match expr {

214

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

215

            metadata.clone_dirty(),

216

            b.clone(),

217

            a.clone(),

218

            Box::new(Expr::Constant(Metadata::new(), Const::Int(0))),

219

        ))),

220

        _ => Err(ApplicationError::RuleNotApplicable),

221

222

223

224

/**

225

* Convert a Leq to an Ineq:

226

227

* ```text

228

* a <= b => a - b < 0

229

* ```

230

*/

231

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

232

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

233

    match expr {

234

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

235

            metadata.clone_dirty(),

236

            a.clone(),

237

            b.clone(),

238

            Box::new(Expr::Constant(Metadata::new(), Const::Int(0))),

239

        ))),

240

        _ => Err(ApplicationError::RuleNotApplicable),

241

242

243

244

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

245

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

246

//     match expr {

247

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

248

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

249

//                 metadata.clone(),

250

//                 vec![

251

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

252

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

253

//                 ],

254

//             )));

255

//         }

256

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

257

//     }

258

// }

259

260

/**

261

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

262

*/

263

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

264

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

265

    use Expr::*;

266

    match expr {

267

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

268

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

269

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

270

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

271

        _ => {

272

            return Err(ApplicationError::RuleNotApplicable);

273

274

275

276

    let mut sub = expr.children();

277

278

    let mut new_vars = SymbolTable::new();

279

    let mut new_top = vec![];

280

281

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

282

    for c in sub.iter_mut() {

283

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

284

            let new_name = mdl.gensym();

285

            let domain = c

286

                .domain_of(&mdl.variables)

287

                .ok_or(ApplicationError::DomainError)?;

288

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

289

290

            new_top.push(Expr::DivEq(

291

                Metadata::new(),

292

                a.clone(),

293

                b.clone(),

294

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

295

));

296

297

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

298

299

300

    if !new_top.is_empty() {

301

        return Ok(Reduction::new(

302

            expr.with_children(sub),

303

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

304

            new_vars,

305

));

306

307

    Err(ApplicationError::RuleNotApplicable)

308

309

310

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

311

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

312

    match expr {

313

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

314

            if let Expr::SafeDiv(_, x, y) = a.as_ref() {

315

                match **b {

316

                    Expr::Reference(_, _) | Expr::Constant(_, _) => {}

317

                    _ => {

318

                        return Err(ApplicationError::RuleNotApplicable);

319

320

};

321

322

                Ok(Reduction::pure(Expr::DivEq(

323

                    metadata.clone_dirty(),

324

                    x.clone(),

325

                    y.clone(),

326

                    b.clone(),

327

)))

328

            } else if let Expr::SafeDiv(_, x, y) = b.as_ref() {

329

                match **a {

330

                    Expr::Reference(_, _) | Expr::Constant(_, _) => {}

331

                    _ => {

332

                        return Err(ApplicationError::RuleNotApplicable);

333

334

};

335

                Ok(Reduction::pure(Expr::DivEq(

336

                    metadata.clone_dirty(),

337

                    x.clone(),

338

                    y.clone(),

339

                    a.clone(),

340

)))

341

            } else {

342

                Err(ApplicationError::RuleNotApplicable)

343

344

345

        _ => Err(ApplicationError::RuleNotApplicable),

346

347

348

349

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

350

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

351

    match expr {

352

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

353

            Expr::Neq(_, b, c) => {

354

                if !b.can_be_undefined() && !c.can_be_undefined() {

355

                    Ok(Reduction::pure(Expr::Eq(

356

                        Metadata::new(),

357

                        b.clone(),

358

                        c.clone(),

359

)))

360

                } else {

361

                    Err(ApplicationError::RuleNotApplicable)

362

363

364

            _ => Err(ApplicationError::RuleNotApplicable),

365

},

366

        _ => Err(ApplicationError::RuleNotApplicable),

367

368

369

370

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

371

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

372

    match expr {

373

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

374

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

375

                if !b.can_be_undefined() && !c.can_be_undefined() {

376

                    Ok(Reduction::pure(Expr::Neq(

377

                        Metadata::new(),

378

                        b.clone(),

379

                        c.clone(),

380

)))

381

                } else {

382

                    Err(ApplicationError::RuleNotApplicable)

383

384

385

            _ => Err(ApplicationError::RuleNotApplicable),

386

},

387

        _ => Err(ApplicationError::RuleNotApplicable),

388

389