Grcov report - expand

1

use conjure_cp::{

2

    ast::{

3

        Atom, DeclarationKind, DeclarationPtr, DomainPtr, Expression, Literal, Metadata, Name,

4

        SymbolTable,

5

        ac_operators::ACOperatorKind,

6

        comprehension::{Comprehension, ComprehensionQualifier},

7

        eval_constant,

8

},

9

    bug, into_matrix_expr,

10

    solver::SolverError,

11

};

12

use uniplate::Uniplate as _;

13

14

use super::via_solver_common::{

15

    lift_machine_references_into_parent_scope, min_max_skip_value, simplify_expression,

16

    strip_guarded_safe_index_conditions,

17

};

18

19

/// Expands the comprehension without calling an external solver.

20

///

21

/// Qualifiers are interpreted left-to-right. Generators behave like nested loops, and

22

/// conditions behave like `if` statements at their position in that loop nest. Constant

23

/// conditions prune immediately; symbolic conditions in an AC context wrap the expansion

24

/// of the remaining qualifiers using [`Comprehension::skip_operator`]'s skip semantics.

25

234648

pub fn expand_native(

26

234648

    comprehension: Comprehension,

27

234648

    parent_symbols: &mut SymbolTable,

28

234648

) -> Result<Vec<Expression>, SolverError> {

29

    // For Min/Max, the safe value to substitute for a guarded-out element must come from the

30

    // comprehension's *general* return-expression domain, computed once here before any

31

    // generator's `with_temporary_quantified_binding` narrows a quantified variable's domain down

32

    // to one concrete value per branch -- computing it later, from an already-narrowed branch's

33

    // own (possibly single-valued) result, would make the skip value equal to that one value

34

    // instead of a bound safe for every possible element, corrupting the guard.

35

234648

    let min_max_skip_value = match comprehension.skip_operator {

36

1

        Some(op @ (ACOperatorKind::Min | ACOperatorKind::Max)) => Some(min_max_skip_value(

37

1

            &comprehension.return_expression,

38

1

            op == ACOperatorKind::Min,

39

1

        )?),

40

234647

        _ => None,

41

};

42

234648

    expand_qualifiers(

43

234648

        &comprehension,

44

234648

0,

45

234648

        parent_symbols,

46

234648

        comprehension.skip_operator,

47

234648

        min_max_skip_value,

48

234648

49

234648

50

51

2618705

fn expand_qualifiers(

52

2618705

    comprehension: &Comprehension,

53

2618705

    qualifier_index: usize,

54

2618705

    parent_symbols: &mut SymbolTable,

55

2618705

    ac_operator: Option<ACOperatorKind>,

56

2618705

    min_max_skip_value: Option<Literal>,

57

2618705

) -> Result<Vec<Expression>, SolverError> {

58

2618705

    if qualifier_index == comprehension.qualifiers.len() {

59

1994536

        let child_symbols = comprehension.symbols().clone();

60

        let return_expression =

61

1994536

            concretise_resolved_reference_atoms(comprehension.return_expression.clone());

62

        // Comprehensions are leaves in Expression's Uniplate traversal. Expand any nested

63

        // comprehensions while the current generators still have their temporary bindings, so

64

        // dependent domains in the nested comprehension can resolve those bindings.

65

1994536

        let return_expression = expand_nested_comprehensions(return_expression, parent_symbols)?;

66

1994536

        let Some(return_expression) = strip_guarded_safe_index_conditions(return_expression) else {

67

            return Ok(vec![]);

68

};

69

1994536

        let return_expression = simplify_expression(return_expression);

70

        // Drop AC identities here so And/Or/Sum/Product expansions do not materialise a huge

71

        // vector of tautologies that the rewriter must later strip. Min/Max have no universal

72

        // identity (ACOperatorKind::identity() panics for them), so this optimisation just

73

        // doesn't apply to them -- every element stays, which is still correct, just not maximally

74

        // compact.

75

1994536

        if let Some(op) = ac_operator

76

1983356

            && !matches!(op, ACOperatorKind::Min | ACOperatorKind::Max)

77

1983353

            && let Expression::Atomic(_, Atom::Literal(lit)) = &return_expression

78

986321

            && lit == &op.identity()

79

80

907812

            return Ok(vec![]);

81

1086724

82

1086724

        let return_expression = lift_machine_references_into_parent_scope(

83

1086724

            return_expression,

84

1086724

            &child_symbols,

85

1086724

            parent_symbols,

86

1086724

);

87

1086724

        return Ok(vec![return_expression]);

88

624169

89

90

624169

    let expanded = match &comprehension.qualifiers[qualifier_index] {

91

        ComprehensionQualifier::Generator { ptr } => {

92

371373

            let name = ptr.name().clone();

93

371373

            let domain = ptr.domain().expect("generator declaration has domain");

94

371373

            let values = resolve_generator_values(&name, &domain)?;

95

371373

            let mut expanded = Vec::new();

96

97

371373

            for literal in values {

98

2136032

                let mut suffix = with_temporary_quantified_binding(ptr, &literal, || {

99

2136032

                    expand_qualifiers(

100

2136032

                        comprehension,

101

2136032

                        qualifier_index + 1,

102

2136032

                        parent_symbols,

103

2136032

                        ac_operator,

104

2136032

                        min_max_skip_value.clone(),

105

2136032

106

2136032

                })?;

107

2136032

                expanded.append(&mut suffix);

108

109

110

371373

            expanded

111

112

252796

        ComprehensionQualifier::Condition(condition) => match evaluate_bool_guard(condition)? {

113

8366

            Some(true) => expand_qualifiers(

114

8366

                comprehension,

115

8366

                qualifier_index + 1,

116

8366

                parent_symbols,

117

8366

                ac_operator,

118

8366

                min_max_skip_value,

119

8366

)?,

120

4771

            Some(false) => vec![],

121

            None => {

122

239659

                let suffix = expand_qualifiers(

123

239659

                    comprehension,

124

239659

                    qualifier_index + 1,

125

239659

                    parent_symbols,

126

239659

                    ac_operator,

127

239659

                    min_max_skip_value.clone(),

128

239659

)?;

129

239659

                apply_guard_to_suffix(condition, suffix, ac_operator, min_max_skip_value)?

130

131

},

132

        ComprehensionQualifier::ExpressionGenerator { .. } => {

133

            // See `expand_comprehension_native`: expression generators are not unrolled natively.

134

            bug!(

135

                "Comprehension expander should not be called on comprehensions containing ExpressionGenerator"

136

);

137

138

};

139

140

624169

    Ok(expanded)

141

2618705

142

143

22375915

fn expand_nested_comprehensions(

144

22375915

    expr: Expression,

145

22375915

    parent_symbols: &mut SymbolTable,

146

22375915

) -> Result<Expression, SolverError> {

147

    // Expand a comprehension before descending into it. Its own generators have to be bound before

148

    // anything nested in its body is expanded, since a nested generator's domain may depend on them

149

    // -- `forAll blockLeft : int(1..exposedBlock-1)` inside `exists exposedBlock : ...`. Expanding

150

    // inside out would reach `blockLeft` while `exposedBlock` is still unbound.

151

22375915

    if let Expression::Comprehension(_, comprehension) = &expr {

152

176496

        let results = expand_native(comprehension.as_ref().clone(), parent_symbols)?;

153

176496

        return Ok(into_matrix_expr!(results));

154

22199419

155

156

22199419

    let children = expr

157

22199419

        .children()

158

22199419

        .into_iter()

159

20381379

        .map(|child| expand_nested_comprehensions(child, parent_symbols))

160

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

161

22199419

    Ok(expr.with_children(children))

162

22375915

163

164

239659

fn apply_guard_to_suffix(

165

239659

    guard: &Expression,

166

239659

    suffix: Vec<Expression>,

167

239659

    ac_operator: Option<ACOperatorKind>,

168

239659

    min_max_skip_value: Option<Literal>,

169

239659

) -> Result<Vec<Expression>, SolverError> {

170

239659

    if suffix.is_empty() {

171

169274

        return Ok(vec![]);

172

70385

173

174

70385

    let Some(ac_operator) = ac_operator else {

175

        return Err(SolverError::ModelInvalid(format!(

176

            "comprehension has symbolic guard but no AC operator context for native expansion: {guard:?}"

177

        )));

178

};

179

180

70385

    let guard = concretise_resolved_reference_atoms(guard.clone());

181

70385

    let guard = simplify_expression(guard);

182

70385

    let suffix = ac_operator.as_expression(into_matrix_expr!(suffix));

183

184

70385

    let skip_expr = match (ac_operator, min_max_skip_value) {

185

        (ACOperatorKind::Min | ACOperatorKind::Max, Some(skip_value)) => {

186

1

            ac_operator.make_min_max_skip_operation(guard, suffix, skip_value)

187

188

        (ACOperatorKind::Min | ACOperatorKind::Max, None) => {

189

            bug!("min/max comprehension expansion is missing its precomputed skip value")

190

191

70384

        _ => ac_operator.make_skip_operation(guard, suffix),

192

};

193

70385

    Ok(vec![skip_expr])

194

239659

195

196

371373

fn resolve_generator_values(name: &Name, domain: &DomainPtr) -> Result<Vec<Literal>, SolverError> {

197

371373

    let resolved = domain.resolve().map_err(|e| {

198

        SolverError::ModelFeatureNotSupported(format!(

199

            "quantified variable '{name}' has unresolved domain after assigning previous generators: {domain}; error: {e}"

200

))

201

    })?;

202

203

371373

    resolved.values().map(|iter| iter.collect()).map_err(|err| {

204

        SolverError::ModelFeatureNotSupported(format!(

205

            "quantified variable '{name}' has non-enumerable domain: {err}"

206

))

207

})

208

371373

209

210

2136032

fn with_temporary_quantified_binding<T>(

211

2136032

    quantified: &DeclarationPtr,

212

2136032

    value: &Literal,

213

2136032

    f: impl FnOnce() -> Result<T, SolverError>,

214

2136032

) -> Result<T, SolverError> {

215

2136032

    let mut targets = vec![quantified.clone()];

216

2136032

    if let DeclarationKind::Quantified(inner) = &*quantified.kind()

217

2136032

        && let Some(generator) = inner.generator()

218

219

        targets.push(generator.clone());

220

2136032

221

222

2136032

    let mut originals = Vec::with_capacity(targets.len());

223

2136032

    for mut target in targets {

224

2136032

        let old_kind = target.replace_kind(DeclarationKind::TemporaryValueLetting(

225

2136032

            Expression::Atomic(Metadata::new(), Atom::Literal(value.clone())),

226

2136032

));

227

2136032

        originals.push((target, old_kind));

228

229

230

2136032

    let result = f();

231

232

2136032

    for (mut target, old_kind) in originals.into_iter().rev() {

233

2136032

        let _ = target.replace_kind(old_kind);

234

235

236

2136032

    result

237

2136032

238

239

/// Returns `Ok(Some(bool))` for constant guards, `Ok(None)` for symbolic guards.

240

252796

fn evaluate_bool_guard(guard: &Expression) -> Result<Option<bool>, SolverError> {

241

252796

    let simplified = simplify_expression(guard.clone());

242

252796

    match eval_constant(&simplified) {

243

13137

        Some(Literal::Bool(value)) => Ok(Some(value)),

244

        Some(other) => Err(SolverError::ModelInvalid(format!(

245

            "native comprehension guard must evaluate to Bool, got {other}: {guard}"

246

        ))),

247

239659

        None => Ok(None),

248

249

252796

250

251

2064921

fn concretise_resolved_reference_atoms(expr: Expression) -> Expression {

252

    use uniplate::Biplate as _;

253

12175814

    expr.transform_bi(&|atom: Atom| match atom {

254

9321067

        Atom::Reference(reference) => reference

255

9321067

            .resolve_constant()

256

9321067

            .map_or_else(|| Atom::Reference(reference), Atom::Literal),

257

2854747

        other => other,

258

12175814

})

259

2064921

260

261

#[cfg(test)]

262

mod tests {

263

    use conjure_cp::ast::{

264

        DeclarationPtr, Domain, IntVal, Moo, Range, Reference, SymbolTablePtr,

265

        comprehension::ComprehensionBuilder,

266

};

267

268

    use super::*;

269

270

5

    fn atom_ref(ptr: DeclarationPtr) -> Expression {

271

5

        Expression::Atomic(Metadata::new(), Atom::new_ref(ptr))

272

5

273

274

9

    fn int(value: i32) -> Expression {

275

9

        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(value)))

276

9

277

278

    #[test]

279

1

    fn constant_guard_prunes_false_branches_without_identity_elements() {

280

1

        let parent_symbols = SymbolTablePtr::new();

281

1

        let mut builder = ComprehensionBuilder::new(parent_symbols.clone());

282

1

        builder = builder.generator(DeclarationPtr::new_find(

283

1

            Name::user("i"),

284

1

            Domain::int(vec![Range::Bounded(1, 9)]),

285

1

));

286

1

        let i = builder

287

1

            .generator_symboltable()

288

1

            .read()

289

1

            .lookup_local(&Name::user("i"))

290

1

            .expect("i should be in comprehension scope");

291

292

1

        let i_expr = atom_ref(i);

293

1

        builder = builder.guard(Expression::Eq(

294

1

            Metadata::new(),

295

1

            Moo::new(Expression::UnsafeMod(

296

1

                Metadata::new(),

297

1

                Moo::new(i_expr.clone()),

298

1

                Moo::new(int(2)),

299

1

)),

300

1

            Moo::new(int(0)),

301

1

));

302

303

1

        let comprehension = builder.with_return_value(i_expr);

304

1

        let expanded = expand_native(comprehension, &mut parent_symbols.read().clone()).unwrap();

305

306

1

        assert_eq!(expanded, vec![int(2), int(4), int(6), int(8)]);

307

1

308

309

    #[test]

310

1

    fn min_max_skip_value_uses_the_return_expressions_domain_bound() {

311

1

        let i = DeclarationPtr::new_find(Name::user("i"), Domain::int(vec![Range::Bounded(5, 8)]));

312

1

        let i_expr = atom_ref(i);

313

314

1

        assert_eq!(

315

1

            min_max_skip_value(&i_expr, true).unwrap(),

316

1

            Literal::Int(8),

317

            "min's skip value should be the upper bound"

318

);

319

1

        assert_eq!(

320

1

            min_max_skip_value(&i_expr, false).unwrap(),

321

1

            Literal::Int(5),

322

            "max's skip value should be the lower bound"

323

);

324

1

325

326

    #[test]

327

1

    fn min_comprehension_with_a_symbolic_guard_never_lets_the_skip_value_win() {

328

        // Regression test: min/max comprehensions used to be tagged with ACOperatorKind::Sum as

329

        // their skip_operator, so a symbolic guard substituted 0 (Sum's identity) for guarded-out

330

        // elements -- not a neutral value for min. Domain is entirely positive (6..8) so 0 would

331

        // have won the min if the bug were still present.

332

1

        let parent_symbols = SymbolTablePtr::new();

333

1

        let b = DeclarationPtr::new_find(Name::user("b"), Domain::bool());

334

1

        parent_symbols.write().insert(b.clone());

335

336

1

        let mut builder = ComprehensionBuilder::new(parent_symbols.clone()).generator(

337

1

            DeclarationPtr::new_find(Name::user("i"), Domain::int(vec![Range::Bounded(6, 8)])),

338

1

);

339

1

        let i = builder

340

1

            .generator_symboltable()

341

1

            .read()

342

1

            .lookup_local(&Name::user("i"))

343

1

            .expect("i should be in comprehension scope");

344

1

        let i_expr = atom_ref(i);

345

346

        // `i != 6 \/ b`: with b left symbolic, only i=6's guard is undetermined at expansion time.

347

1

        builder = builder.guard(Expression::Or(

348

1

            Metadata::new(),

349

1

            Moo::new(conjure_cp::matrix_expr![

350

1

                Expression::Neq(Metadata::new(), Moo::new(i_expr.clone()), Moo::new(int(6))),

351

1

                atom_ref(b),

352

1

]),

353

1

));

354

355

1

        let mut comprehension = builder.with_return_value(i_expr);

356

1

        comprehension.skip_operator = Some(ACOperatorKind::Min);

357

1

        let expanded = expand_native(comprehension, &mut parent_symbols.read().clone()).unwrap();

358

359

        // Every literal `0` in the expanded tree would indicate the old Sum-identity bug; the

360

        // skip value must be the domain's own upper bound (8) instead.

361

1

        let flat = format!("{expanded:?}");

362

1

        assert!(

363

1

            !flat.contains("Int(0)"),

364

            "min skip value must not be Sum's identity (0): {flat}"

365

);

366

1

        assert!(

367

1

            flat.contains("Int(8)"),

368

            "min skip value should be the domain upper bound (8): {flat}"

369

);

370

1

371

372

    #[test]

373

1

    fn native_expansion_drops_and_identity_results() {

374

1

        let parent_symbols = SymbolTablePtr::new();

375

1

        let mut comprehension = ComprehensionBuilder::new(parent_symbols.clone())

376

1

            .generator(DeclarationPtr::new_find(

377

1

                Name::user("i"),

378

1

                Domain::int(vec![Range::Bounded(1, 3)]),

379

1

))

380

1

            .with_return_value(Expression::from(true));

381

1

        comprehension.skip_operator = Some(ACOperatorKind::And);

382

383

1

        let expanded = expand_native(comprehension, &mut parent_symbols.read().clone()).unwrap();

384

1

        assert!(expanded.is_empty());

385

1

386

387

    #[test]

388

1

    fn nested_comprehension_domains_see_outer_generator_bindings() {

389

1

        let parent_symbols = SymbolTablePtr::new();

390

1

        let mut outer = ComprehensionBuilder::new(parent_symbols.clone()).generator(

391

1

            DeclarationPtr::new_find(Name::user("i"), Domain::int(vec![Range::Bounded(1, 2)])),

392

1

);

393

1

        let i = outer

394

1

            .generator_symboltable()

395

1

            .read()

396

1

            .lookup_local(&Name::user("i"))

397

1

            .expect("i should be in outer comprehension scope");

398

399

1

        let mut inner = ComprehensionBuilder::new(outer.generator_symboltable()).generator(

400

1

            DeclarationPtr::new_find(

401

1

                Name::user("j"),

402

1

                Domain::int(vec![Range::Single(IntVal::Reference(Reference::new(i)))]),

403

1

),

404

1

);

405

1

        let j = inner

406

1

            .generator_symboltable()

407

1

            .read()

408

1

            .lookup_local(&Name::user("j"))

409

1

            .expect("j should be in inner comprehension scope");

410

1

        let inner = Expression::Comprehension(

411

1

            Metadata::new(),

412

1

            Moo::new(inner.with_return_value(atom_ref(j))),

413

1

);

414

1

        let outer = outer.with_return_value(inner);

415

416

1

        let expanded = expand_native(outer, &mut parent_symbols.read().clone()).unwrap();

417

418

1

        assert_eq!(

419

1

            expanded,

420

1

            vec![

421

1

                simplify_expression(into_matrix_expr!(vec![int(1)])),

422

1

                simplify_expression(into_matrix_expr!(vec![int(2)])),

423

424

);

425

1

426