Grcov report - rules.rs

1

use conjure_cp::ast::comprehension::ComprehensionQualifier;

2

use conjure_cp::ast::{Expression as Expr, *};

3

use conjure_cp::rule_engine::{

4

    ApplicationError::{DomainError, RuleNotApplicable},

5

    ApplicationResult, RuleEffect, register_rule, register_rule_set,

6

};

7

use conjure_cp::settings::SolverFamily;

8

use conjure_cp::{bug, essence_expr};

9

use uniplate::Uniplate;

10

11

// These rules are applicable regardless of what theories are used.

12

register_rule_set!("Smt", ("Base"), |f: &SolverFamily| {

13

294803

    matches!(f, SolverFamily::Z3)

14

294803

});

15

16

/// An auxiliary declaration is an equality.

17

///

18

/// `x =aux e` says the fresh variable `x` stands for `e`. Minion keeps these around so its flat

19

/// constraint forms can absorb them (`sumeq(..., x)` rather than a separate equality); a solver

20

/// with no such forms just asserts the equality.

21

#[register_rule("Smt", 2000, [AuxDeclaration])]

22

91

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

23

91

    let Expr::AuxDeclaration(_, reference, value) = expr else {

24

21

        return Err(RuleNotApplicable);

25

};

26

70

    Ok(RuleEffect::pure(Expr::Eq(

27

70

        Metadata::new(),

28

70

        Moo::new(reference.clone().into()),

29

70

        value.clone(),

30

70

)))

31

91

32

33

#[register_rule("Smt", 1000, [InDomain])]

34

259

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

35

259

    let Expr::InDomain(_, inner, domain) = expr else {

36

21

        return Err(RuleNotApplicable);

37

};

38

39

238

    let dom = domain.resolve().map_err(|_| RuleNotApplicable)?;

40

238

    let new_expr = match dom.as_ref() {

41

        GroundDomain::Empty(_) => Ok(Expr::Atomic(

42

            Metadata::new(),

43

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

44

)),

45

        // Bool values are always in the bool domain

46

        GroundDomain::Bool => Ok(Expr::Atomic(

47

            Metadata::new(),

48

            Atom::Literal(Literal::Bool(true)),

49

)),

50

        GroundDomain::Int(ranges, _) => {

51

238

            let elements: Vec<_> = ranges

52

238

                .iter()

53

280

                .map(|range| match range {

54

                    Range::Single(n) => {

55

84

                        let eq = Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Int(*n)));

56

84

                        Expr::Eq(Metadata::new(), inner.clone(), Moo::new(eq))

57

58

                    Range::Bounded(l, r) => {

59

196

                        let l_expr = Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Int(*l)));

60

196

                        let r_expr = Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Int(*r)));

61

196

                        let lit = AbstractLiteral::matrix_implied_indices(vec![

62

196

                            Expr::Geq(Metadata::new(), inner.clone(), Moo::new(l_expr)),

63

196

                            Expr::Leq(Metadata::new(), inner.clone(), Moo::new(r_expr)),

64

196

]);

65

196

                        Expr::And(

66

196

                            Metadata::new(),

67

196

                            Moo::new(Expr::AbstractLiteral(Metadata::new(), lit)),

68

196

69

70

                    Range::UnboundedL(r) => {

71

                        let bound = Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Int(*r)));

72

                        Expr::Leq(Metadata::new(), inner.clone(), Moo::new(bound))

73

74

                    Range::UnboundedR(l) => {

75

                        let bound = Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Int(*l)));

76

                        Expr::Geq(Metadata::new(), inner.clone(), Moo::new(bound))

77

78

                    Range::Unbounded => bug!("integer domains should not have unbounded ranges"),

79

280

})

80

                .collect();

81

238

            Ok(Expr::Or(

82

238

                Metadata::new(),

83

238

                Moo::new(Expr::AbstractLiteral(

84

238

                    Metadata::new(),

85

238

                    AbstractLiteral::matrix_implied_indices(elements),

86

238

)),

87

238

))

88

89

        _ => Err(RuleNotApplicable),

90

}?;

91

238

    Ok(RuleEffect::pure(new_expr))

92

259

93

94

/// Turn a matrix slice into a 1-d matrix of the slice elements

95

/// E.g. m[1,..] ~> [m[1,1], m[1,2], m[1,3]]

96

#[register_rule("Smt", 1000, [SafeSlice])]

97

798

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

98

798

    let Expr::SafeSlice(_, m, slice_idxs) = expr else {

99

21

        return Err(RuleNotApplicable);

100

};

101

102

777

    let mat_idxs = matrix::bound_index_domains_of_expr(m.as_ref()).ok_or(RuleNotApplicable)?;

103

104

777

    if slice_idxs.len() != mat_idxs.len() {

105

        return Err(DomainError);

106

777

107

108

    // Find where in the index vector the ".." is

109

777

    let (slice_dim, _) = slice_idxs

110

777

        .iter()

111

777

        .enumerate()

112

1078

        .find(|(_, idx)| idx.is_none())

113

777

        .ok_or(RuleNotApplicable)?;

114

    let other_idxs = {

115

777

        let opt: Option<Vec<_>> = [&slice_idxs[..slice_dim], &slice_idxs[(slice_dim + 1)..]]

116

777

            .concat()

117

777

            .into_iter()

118

777

            .collect();

119

777

        opt.ok_or(DomainError)?

120

};

121

777

    let elements: Vec<Expr> = mat_idxs[slice_dim]

122

777

        .values()

123

        .map_err(|_| DomainError)?

124

4683

        .map(|lit| {

125

4683

            let mut new_idx = other_idxs.clone();

126

4683

            new_idx.insert(slice_dim, Expr::Atomic(Metadata::new(), Atom::Literal(lit)));

127

4683

            Expr::SafeIndex(Metadata::new(), m.clone(), new_idx)

128

4683

})

129

        .collect();

130

777

    Ok(RuleEffect::pure(Expr::AbstractLiteral(

131

777

        Metadata::new(),

132

777

        AbstractLiteral::matrix_implied_indices(elements),

133

777

)))

134

798

135

136

/// Expressions like allDiff and sum support 1-dimensional matrices as inputs, e.g. sum(m) where m is indexed by 1..3.

137

///

138

/// This rule is similar to `expand_matrix_components_reference`, but turns the matrix reference

139

/// into a slice rather than its components.

140

/// Other rules like `flatten_matrix_slice` take care of actually turning the slice into the matrix elements.

141

#[register_rule("Smt", 999)]

142

367415

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

143

367415

    if let Expr::SafeSlice(_, _, _)

144

367415

    | Expr::UnsafeSlice(_, _, _)

145

367415

    | Expr::SafeIndex(_, _, _)

146

367415

    | Expr::UnsafeIndex(_, _, _) = expr

147

148

37793

        return Err(RuleNotApplicable);

149

329622

};

150

151

329622

    for (child, ctx) in expr.holes() {

152

217809

        let Expr::Atomic(_, Atom::Reference(decl)) = &child else {

153

180658

            continue;

154

};

155

156

37151

        let dom = decl.resolved_domain().ok_or(RuleNotApplicable)?;

157

37151

        let GroundDomain::Matrix(_, index_domains, _) = dom.as_ref() else {

158

37004

            continue;

159

};

160

161

        // Must be a 1d matrix

162

147

        if index_domains.len() > 1 {

163

            continue;

164

147

165

166

147

        let new_child = Expr::SafeSlice(Metadata::new(), Moo::new(child.clone()), vec![None]);

167

147

        return Ok(RuleEffect::pure(ctx(new_child)));

168

169

170

329475

    Err(RuleNotApplicable)

171

367415

172

173

/// This rule is applicable in SMT when atomic representation is not used for matrices.

174

///

175

/// Namely, it unwraps flatten(m) into [m[1, 1], m[1, 2], ...]

176

#[register_rule("Smt", 999, [Flatten])]

177

21

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

178

    // TODO: depth not supported yet

179

21

    let Expr::Flatten(_, None, m) = expr else {

180

21

        return Err(RuleNotApplicable);

181

};

182

183

    let index_domains = matrix::bound_index_domains_of_expr(m.as_ref()).ok_or(RuleNotApplicable)?;

184

185

    let elems: Vec<Expr> = matrix::try_enumerate_indices(index_domains)

186

        .map_err(|_| DomainError)?

187

        .map(|lits| {

188

            let idxs: Vec<Expr> = lits.into_iter().map(Into::into).collect();

189

            Expr::SafeIndex(Metadata::new(), m.clone(), idxs)

190

})

191

        .collect();

192

193

    let new_dom = GroundDomain::Int(

194

        vec![Range::Bounded(

195

1,

196

            elems

197

                .len()

198

                .try_into()

199

                .expect("length of matrix should be able to be held in Int type"),

200

)],

201

        None,

202

);

203

    let new_expr = Expr::AbstractLiteral(

204

        Metadata::new(),

205

        AbstractLiteral::Matrix(elems, new_dom.into()),

206

);

207

    Ok(RuleEffect::pure(new_expr))

208

21

209

210

/// Expands a sum over an "in set" comprehension to a list.

211

///

212

/// TODO: We currently only support one "in set" generator.

213

/// This rule can be made much more general and nicer.

214

#[register_rule("Smt", 999, [Sum])]

215

5383

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

216

5383

    let Expr::Sum(_, inner) = expr else {

217

21

        return Err(RuleNotApplicable);

218

};

219

5362

    let Expr::Comprehension(_, comp) = inner.as_ref() else {

220

5362

        return Err(RuleNotApplicable);

221

};

222

223

    let [ComprehensionQualifier::ExpressionGenerator { ptr }] = &comp.qualifiers[..] else {

224

        return Err(RuleNotApplicable);

225

};

226

227

    let Some(set) = ptr

228

        .as_quantified_expr()

229

        .map(|expr_guard| expr_guard.clone())

230

    else {

231

        return Err(RuleNotApplicable);

232

};

233

234

    let elem_domain = set

235

        .domain_of()

236

        .expect("Expression must have a domain")

237

        .element_domain()

238

        .expect("Expression must contain elements with uniform domain");

239

    let list: Vec<_> = elem_domain

240

        .values()

241

        .map_err(|_| DomainError)?

242

        .map(|lit| essence_expr!("&lit * toInt(&lit in &set)"))

243

        .collect();

244

245

    let new_expr = Expr::Sum(

246

        Metadata::new(),

247

        Moo::new(Expr::AbstractLiteral(

248

            Metadata::new(),

249

            AbstractLiteral::matrix_implied_indices(list),

250

)),

251

);

252

    Ok(RuleEffect::pure(new_expr))

253

5383

254

255

/// Unwraps a subsetEq expression into checking membership equality.

256

///

257

/// Any elements not in the domain of one set must not be in the other set.

258

#[register_rule("Smt", 999, [SubsetEq])]

259

21

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

260

21

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

261

21

        return Err(RuleNotApplicable);

262

};

263

264

    let dom_a = a

265

        .domain_of()

266

        .and_then(|d| d.resolve().ok())

267

        .ok_or(DomainError)?;

268

    let dom_b = b

269

        .domain_of()

270

        .and_then(|d| d.resolve().ok())

271

        .ok_or(DomainError)?;

272

273

    let GroundDomain::Set(_, elem_dom_a) = dom_a.as_ref() else {

274

        return Err(RuleNotApplicable);

275

};

276

    let GroundDomain::Set(_, elem_dom_b) = dom_b.as_ref() else {

277

        return Err(RuleNotApplicable);

278

};

279

280

    let domain_a_iter = elem_dom_a.values().map_err(|_| DomainError)?;

281

    let memberships = domain_a_iter

282

        .map(|lit| {

283

            let b_contains = elem_dom_b.contains(&lit).map_err(|_| DomainError)?;

284

            match b_contains {

285

                true => Ok(essence_expr!("(&lit in &a) -> (&lit in &b)")),

286

                false => Ok(essence_expr!("!(&lit in &a)")),

287

288

})

289

        .collect::<Result<Vec<_>, _>>()?;

290

291

    let new_expr = Expr::And(

292

        Metadata::new(),

293

        Moo::new(Expr::AbstractLiteral(

294

            Metadata::new(),

295

            AbstractLiteral::matrix_implied_indices(memberships),

296

)),

297

);

298

299

    Ok(RuleEffect::pure(new_expr))

300

21

301

302

/// Unwraps equality between sets into checking membership equality.

303

///

304

/// This is an optimisation over unwrap_subseteq to avoid unnecessary additional -> exprs

305

/// where a single <-> is enough. This must apply before eq_to_subset_eq.

306

#[register_rule("Smt", 8801, [Eq])]

307

43072

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

308

43072

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

309

21

        return Err(RuleNotApplicable);

310

};

311

312

43051

    let dom_a = a

313

43051

        .domain_of()

314

42820

        .and_then(|d| d.resolve().ok())

315

43051

        .ok_or(DomainError)?;

316

42820

    let dom_b = b

317

42820

        .domain_of()

318

42478

        .and_then(|d| d.resolve().ok())

319

42820

        .ok_or(DomainError)?;

320

321

42478

    let GroundDomain::Set(_, elem_dom_a) = dom_a.as_ref() else {

322

42478

        return Err(RuleNotApplicable);

323

};

324

    let GroundDomain::Set(_, elem_dom_b) = dom_b.as_ref() else {

325

        return Err(RuleNotApplicable);

326

};

327

328

    let union_val_iter = elem_dom_a

329

        .union(elem_dom_b)

330

        .and_then(|d| d.values())

331

        .map_err(|_| DomainError)?;

332

    let memberships = union_val_iter

333

        .map(|lit| {

334

            let a_contains = elem_dom_a.contains(&lit).map_err(|_| DomainError)?;

335

            let b_contains = elem_dom_b.contains(&lit).map_err(|_| DomainError)?;

336

            match (a_contains, b_contains) {

337

                (true, true) => Ok(essence_expr!("(&lit in &a) <-> (&lit in &b)")),

338

                (true, false) => Ok(essence_expr!("!(&lit in &a)")),

339

                (false, true) => Ok(essence_expr!("!(&lit in &b)")),

340

                (false, false) => unreachable!(),

341

342

})

343

        .collect::<Result<Vec<_>, _>>()?;

344

345

    let new_expr = Expr::And(

346

        Metadata::new(),

347

        Moo::new(Expr::AbstractLiteral(

348

            Metadata::new(),

349

            AbstractLiteral::matrix_implied_indices(memberships),

350

)),

351

);

352

353

    Ok(RuleEffect::pure(new_expr))

354

43072