Grcov report - utils.rs

1

use std::collections::VecDeque;

2

3

use conjure_cp::ast::eval_constant;

4

use conjure_cp::ast::{

5

    AbstractLiteral, Atom, DeclarationPtr, DomainPtr, Expression as Expr, GroundDomain, Literal,

6

    Metadata, Moo, Range, Reference, SymbolTable,

7

    categories::{Category, CategoryOf},

8

    comprehension::{Comprehension, ComprehensionQualifier},

9

    records::Field,

10

};

11

use conjure_cp::representation::get_applicable_repr_by_short_name;

12

use conjure_cp::rule_engine::{ApplicationError, ApplicationError::RuleNotApplicable, RuleEffect};

13

use conjure_cp::{bug, bug_assert, bug_assert_eq, essence_expr, into_matrix_expr, matrix_expr};

14

use itertools::{Itertools, izip};

15

16

use tracing::{instrument, trace};

17

use uniplate::{Biplate, Uniplate};

18

19

/// True iff `expr` is an `Atom`.

20

793918

pub fn is_atom(expr: &Expr) -> bool {

21

793918

    matches!(expr, Expr::Atomic(_, _))

22

793918

23

24

/// True iff `expr` is an `Atom` or `Not(Atom)`.

25

44986308

pub fn is_literal(expr: &Expr) -> bool {

26

44986308

    match expr {

27

32206766

        Expr::Atomic(_, _) => true,

28

46781

        Expr::Not(_, inner) => matches!(**inner, Expr::Atomic(_, _)),

29

12732761

        _ => false,

30

31

44986308

32

33

/// True if `expr` is flat; i.e. it only contains atoms.

34

pub fn is_flat(expr: &Expr) -> bool {

35

    let mut flat = true;

36

    expr.for_each_expr_child(&mut |child| flat = flat && is_atom(child));

37

    flat

38

39

40

/// Rewrites the direct expression children of `expr`, preserving the number of children.

41

///

42

/// Returns the rebuilt expression and the number of children marked as changed by `rewrite`.

43

11959017

pub fn rewrite_children(

44

11959017

    expr: &Expr,

45

11959017

    mut rewrite: impl FnMut(Expr) -> (Expr, bool),

46

11959017

) -> (Expr, usize) {

47

11959017

    let mut num_changed = 0;

48

11959017

    let children: VecDeque<Expr> = expr

49

11959017

        .children()

50

11959017

        .into_iter()

51

30841697

        .map(|child| {

52

30841697

            let (new_child, changed) = rewrite(child);

53

30841697

            if changed {

54

46608

                num_changed += 1;

55

30795089

56

30841697

            new_child

57

30841697

})

58

        .collect();

59

60

11959017

    (expr.with_children(children), num_changed)

61

11959017

62

63

/// Returns the only direct `Vec<Expr>` child of `expr`, if it has exactly one.

64

555317

pub fn single_vec_child(expr: &Expr) -> Option<Vec<Expr>> {

65

555317

    let mut child_vecs: VecDeque<Vec<Expr>> = expr.children_bi();

66

555317

    if child_vecs.len() == 1 {

67

555135

        child_vecs.pop_front()

68

    } else {

69

182

        None

70

71

555317

72

73

/// Rebuilds `expr` with a replacement for its only direct `Vec<Expr>` child.

74

140904

pub fn with_single_vec_child(expr: &Expr, child: Vec<Expr>) -> Expr {

75

140904

    expr.with_children_bi(VecDeque::from([child]))

76

140904

77

78

pub fn eval_to_usize(expr: &Expr) -> usize {

79

    match eval_constant(expr) {

80

        Some(Literal::Int(n)) if n >= 0 => n as usize,

81

        Some(lit) => bug!("expected a non-negative integer, got `{lit}`"),

82

        None => bug!("expected a constant expression, got `{expr}`"),

83

84

85

86

/// True iff the expression is a tuple literal.

87

598238

pub fn is_tuple_lit(expr: &Expr) -> bool {

88

598238

    matches!(

89

598238

        expr,

90

        Expr::AbstractLiteral(_, AbstractLiteral::Tuple(..))

91

            | Expr::Atomic(

92

_,

93

                Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Tuple(..)))

94

95

96

598238

97

98

/// Gets the entries of a tuple expression, if it is one.

99

7169485

pub fn tuple_expr_entries(expr: &Expr) -> Option<Vec<Expr>> {

100

7169485

    match expr {

101

15988

        Expr::AbstractLiteral(_, AbstractLiteral::Tuple(elems)) => Some(elems.clone()),

102

        Expr::Atomic(_, Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Tuple(elems)))) => {

103

176414

            Some(elems.iter().cloned().map(Expr::from).collect())

104

105

6977083

        _ => None,

106

107

7169485

108

109

/// Resolve a value letting used as a table operand.

110

6104903

pub fn table_operand(expr: &Expr) -> Expr {

111

6104903

    if let Expr::Atomic(_, Atom::Reference(reference)) = expr {

112

594286

        if let Some(value) = reference.resolve_expression() {

113

2954

            return value;

114

591332

115

591332

        if let Some(value) = reference.resolve_constant() {

116

            return value.into();

117

591332

118

5510617

119

6101949

    expr.clone()

120

6104903

121

122

/// Read an ordered table input or dense row. Sets deliberately have no positional meaning.

123

702184

pub fn table_ordered_entries(expr: &Expr) -> Option<Vec<Expr>> {

124

702184

    match table_operand(expr) {

125

459284

        Expr::AbstractLiteral(_, AbstractLiteral::Sequence(entries)) => Some(entries),

126

        Expr::Atomic(

127

_,

128

            Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Sequence(entries))),

129

116648

        ) => Some(entries.into_iter().map(Expr::from).collect()),

130

126252

        expr => expr.unwrap_matrix_unchecked().map(|(entries, _)| entries),

131

132

702184

133

134

/// Read an unordered table relation, retaining matrix syntax for existing models.

135

511511

pub fn table_rows(expr: &Expr) -> Option<Vec<Expr>> {

136

511511

    match table_operand(expr) {

137

237461

        Expr::AbstractLiteral(_, AbstractLiteral::Set(entries)) => Some(entries),

138

        Expr::Atomic(_, Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Set(entries)))) => {

139

242914

            Some(entries.into_iter().map(Expr::from).collect())

140

141

31136

        expr => expr.unwrap_matrix_unchecked().map(|(entries, _)| entries),

142

143

511511

144

145

/// Read a sparse row of tuple pairs; sets permit different row sizes without ragged matrices.

146

22673

pub fn short_table_row_entries(expr: &Expr) -> Option<Vec<Expr>> {

147

22673

    let (entries, is_set) = match table_operand(expr) {

148

2947

        Expr::AbstractLiteral(_, AbstractLiteral::Set(entries)) => (entries, true),

149

        Expr::Atomic(_, Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Set(entries)))) => {

150

19726

            (entries.into_iter().map(Expr::from).collect(), true)

151

152

        expr => (table_ordered_entries(&expr)?, false),

153

};

154

22673

    if !is_set {

155

        return Some(entries);

156

22673

157

    // Repeated members of a set must not become repeated position assignments.

158

22673

    let mut unique = Vec::with_capacity(entries.len());

159

22673

    for entry in entries {

160

38458

        if !unique.contains(&entry) {

161

38458

            unique.push(entry);

162

163

164

22673

    Some(unique)

165

22673

166

167

140390293

pub fn as_eq_or_neq(expr: &Expr) -> Result<(&Expr, &Expr, bool), ApplicationError> {

168

140390293

    match expr {

169

113800770

        Expr::Eq(_, left, right) => Ok((left.as_ref(), right.as_ref(), false)),

170

18173532

        Expr::Neq(_, left, right) => Ok((left.as_ref(), right.as_ref(), true)),

171

8415991

        _ => Err(RuleNotApplicable),

172

173

140390293

174

175

120756

pub fn collect_eq_or_neq<A, B>(neq: bool, itr: impl Iterator<Item = (A, B)>) -> Expr

176

120756

where

177

120756

    A: Into<Expr> + Clone,

178

120756

    B: Into<Expr> + Clone,

179

180

120756

    if neq {

181

104055

        let constraints = itr.map(|(a, b)| essence_expr!(&a != &b)).collect_vec();

182

46452

        Expr::Or(Metadata::new(), Moo::new(into_matrix_expr!(constraints)))

183

    } else {

184

159634

        let constraints = itr.map(|(a, b)| essence_expr!(&a == &b)).collect_vec();

185

74304

        Expr::And(Metadata::new(), Moo::new(into_matrix_expr!(constraints)))

186

187

120756

188

189

/// An atom is only genuinely ready for a flat solver-level comparison (`FlatLexLt`/`FlatLexLeq`,

190

/// `AllDiff`, ...) when it is a literal, or a reference whose own domain is already scalar. A

191

/// reference to a still-abstract domain (e.g. a set or tuple field) is wrapped in `Expr::Atomic`

192

/// like any other atom, but treating it as ready would leak the abstract declaration's name

193

/// straight into the backend instead of chasing through to whatever concrete representation it

194

/// ends up with.

195

29988

pub(crate) fn as_resolved_atom(expr: &Expr) -> Option<Atom> {

196

29988

    let Expr::Atomic(_, atom) = expr else {

197

581

        return None;

198

};

199

29407

    if let Atom::Reference(reference) = atom

200

29407

        && reference.ptr().domain().is_some_and(|domain| {

201

29407

            crate::passes::representation::domain_needs_representation(&domain)

202

29407

})

203

204

12607

        return None;

205

16800

206

16800

    Some(atom.clone())

207

29988

208

209

5999

fn expressions_as_atoms(exprs: &[Expr]) -> Option<Vec<Atom>> {

210

5999

    exprs.iter().map(as_resolved_atom).collect()

211

5999

212

213

5117

pub fn collect_cmp_exprs(cmp_op: &Expr, lhs_fields: Vec<Expr>, rhs_fields: Vec<Expr>) -> Expr {

214

5117

    let len = lhs_fields.len();

215

5117

    bug_assert_eq!(

216

5117

        len,

217

5117

        rhs_fields.len(),

218

        "comparison of collections with different shapes"

219

);

220

221

5117

    if let Some(lhs_atoms) = expressions_as_atoms(&lhs_fields)

222

882

        && let Some(rhs_atoms) = expressions_as_atoms(&rhs_fields)

223

224

882

        match cmp_op {

225

            Expr::LexLeq(..) => return Expr::FlatLexLeq(Metadata::new(), lhs_atoms, rhs_atoms),

226

882

            Expr::LexLt(..) => return Expr::FlatLexLt(Metadata::new(), lhs_atoms, rhs_atoms),

227

            _ => {}

228

229

4235

230

231

    // cases[j] means "fields 0..j are equal, and field j satisfies cmp_op" -- so field i's own

232

    // equality belongs to every *later* case's prefix (j > i), not to the earlier cases already

233

    // built from fields before it.

234

4235

    let mut cases = vec![Vec::<Expr>::with_capacity(len); len];

235

4235

    for (i, (lhs, rhs)) in izip!(lhs_fields, rhs_fields).enumerate() {

236

9940

        let equal = essence_expr!(&lhs = &rhs);

237

9940

        let comparison = field_cmp_expr(cmp_op, lhs, rhs);

238

9940

        cases[i].push(comparison);

239

9940

        for case in cases.iter_mut().skip(i + 1) {

240

7175

            case.push(equal.clone());

241

242

243

244

4235

    let conjunctions = cases

245

4235

        .into_iter()

246

9940

        .map(|case| Expr::And(Metadata::new(), Moo::new(into_matrix_expr!(case))))

247

        .collect();

248

4235

    Expr::Or(Metadata::new(), Moo::new(into_matrix_expr!(conjunctions)))

249

5117

250

251

/// `cmp_op` is chosen for the tuple as a whole (e.g. `LexLt` because some *other* field is

252

/// abstract and needs list-style comparison), but each field must be compared with whatever

253

/// operator actually matches its own type. A scalar field has no list/lex structure of its own,

254

/// so a lexicographic operator must be downgraded to its plain counterpart; a still-abstract field

255

/// (e.g. a nested set) has no native `<`, so it keeps the lexicographic operator, wrapped as a

256

/// singleton list -- the shape a field's own representation-specific ordering rule (e.g.

257

/// `lex_explicit_sets`) expects -- and is left for that rule to expand.

258

9940

fn field_cmp_expr(cmp_op: &Expr, lhs: Expr, rhs: Expr) -> Expr {

259

9940

    let scalar = as_resolved_atom(&lhs).is_some() && as_resolved_atom(&rhs).is_some();

260

9940

    match (cmp_op, scalar) {

261

1778

        (Expr::LexLt(..), true) => Expr::Lt(Metadata::new(), Moo::new(lhs), Moo::new(rhs)),

262

        (Expr::LexLeq(..), true) => Expr::Leq(Metadata::new(), Moo::new(lhs), Moo::new(rhs)),

263

8162

        (Expr::LexLt(..), false) => Expr::LexLt(

264

8162

            Metadata::new(),

265

8162

            Moo::new(matrix_expr![lhs]),

266

8162

            Moo::new(matrix_expr![rhs]),

267

8162

),

268

        (Expr::LexLeq(..), false) => Expr::LexLeq(

269

            Metadata::new(),

270

            Moo::new(matrix_expr![lhs]),

271

            Moo::new(matrix_expr![rhs]),

272

),

273

        _ => cmp_op.with_children(VecDeque::from([lhs, rhs])),

274

275

9940

276

277

38625350

pub fn as_comparison_op(expr: &Expr) -> Option<(Moo<Expr>, Moo<Expr>)> {

278

38625350

    match expr {

279

        Expr::Eq(_, lhs, rhs)

280

        | Expr::Neq(_, lhs, rhs)

281

        | Expr::Lt(_, lhs, rhs)

282

        | Expr::Gt(_, lhs, rhs)

283

        | Expr::Leq(_, lhs, rhs)

284

38569919

        | Expr::Geq(_, lhs, rhs) => Some((lhs.clone(), rhs.clone())),

285

55431

        _ => None,

286

287

38625350

288

289

39929275

pub fn as_lex_comparison_op(expr: &Expr) -> Option<(Moo<Expr>, Moo<Expr>)> {

290

39929275

    match expr {

291

        Expr::LexGt(_, lhs, rhs)

292

        | Expr::LexLt(_, lhs, rhs)

293

        | Expr::LexGeq(_, lhs, rhs)

294

1303925

        | Expr::LexLeq(_, lhs, rhs) => Some((lhs.clone(), rhs.clone())),

295

38625350

        _ => None,

296

297

39929275

298

299

39929275

pub fn as_cmp_or_lex_op(expr: &Expr) -> Option<(Moo<Expr>, Moo<Expr>)> {

300

39929275

    as_lex_comparison_op(expr).or_else(|| as_comparison_op(expr))

301

39929275

302

303

88816

pub fn eq_or_neq(neq: bool, lhs: Expr, rhs: Expr) -> Expr {

304

88816

    if neq {

305

32501

        essence_expr!(&lhs != &rhs)

306

    } else {

307

56315

        essence_expr!(&lhs = &rhs)

308

309

88816

310

311

/// True if the entire AST is constants.

312

#[allow(dead_code)]

313

pub fn is_all_constant(expression: &Expr) -> bool {

314

    expression

315

        .universe_bi()

316

        .into_iter()

317

        .all(|atom| matches!(atom, Atom::Literal(_)))

318

319

/// Converts a vector of expressions to a vector of atoms.

320

///

321

/// # Returns

322

///

323

/// `Some(Vec<Atom>)` if the vectors direct children expressions are all atomic, otherwise `None`.

324

#[allow(dead_code)]

325

pub fn expressions_to_atoms(exprs: &Vec<Expr>) -> Option<Vec<Atom>> {

326

    let mut atoms: Vec<Atom> = vec![];

327

    for expr in exprs {

328

        let Expr::Atomic(_, atom) = expr else {

329

            return None;

330

};

331

        atoms.push(atom.clone());

332

333

334

    Some(atoms)

335

336

337

/// Replaces every direct child of `expr` that needs one with a fresh auxiliary variable.

338

///

339

/// `applies` decides whether the rewrite goes ahead, given the number of children that need an

340

/// auxiliary and the total number of children. It is consulted before the model-wide symbol table

341

/// is cloned, so a rule that does not apply pays neither for the clone nor for the rebuild.

342

///

343

/// Child domains are derived once and reused for the rewrite. Deriving the domain of an expression

344

/// can enumerate its whole value set, and expression clones start with an empty domain cache, so

345

/// each domain is worth deriving exactly once per call.

346

406469

pub fn flatten_children_to_aux_vars(

347

406469

    expr: &Expr,

348

406469

    symbols: &SymbolTable,

349

406469

    applies: impl FnOnce(usize, usize) -> bool,

350

406469

) -> Option<(Expr, Vec<Expr>, SymbolTable)> {

351

406469

    let children = expr.children();

352

406469

    let child_domains: Vec<Option<DomainPtr>> = children.iter().map(to_aux_var_domain).collect();

353

354

406469

    let needs_aux = child_domains

355

406469

        .iter()

356

713340

        .filter(|domain| domain.is_some())

357

        .count();

358

406469

    if !applies(needs_aux, children.len()) {

359

321394

        return None;

360

85075

361

362

85075

    let mut symbols = symbols.clone();

363

85075

    let mut new_tops: Vec<Expr> = vec![];

364

85075

    let mut new_children: VecDeque<Expr> = VecDeque::with_capacity(children.len());

365

85075

    for (child, domain) in children.into_iter().zip(child_domains) {

366

128094

        match domain {

367

            Some(domain) => {

368

86814

                let (reference, top) = materialise_aux_var_in(&child, &mut symbols, &domain);

369

86814

                new_tops.push(top);

370

86814

                new_children.push_back(Expr::Atomic(Metadata::new(), Atom::Reference(reference)));

371

372

41280

            None => new_children.push_back(child),

373

374

375

376

85075

    Some((expr.with_children(new_children), new_tops, symbols))

377

406469

378

379

/// Creates a new auxiliary variable using the given expression.

380

///

381

/// # Returns

382

///

383

/// * `None` if `Expr` is a `Atom`, or `Expr` does not have a domain (for example, if it is a `Bubble`).

384

///

385

/// * `Some(ToAuxVarOutput)` if successful, containing:

386

///

387

///     + A new symbol table, modified to include the auxiliary variable.

388

///     + A new top level expression, containing the declaration of the auxiliary variable.

389

///     + A reference to the auxiliary variable to replace the existing expression with.

390

///

391

/// Adds an auxiliary for `expr` directly to an existing speculative symbol table.

392

///

393

/// Use this when constructing one or more auxiliaries inside an effect. It avoids cloning the

394

/// complete, growing symbol table for each auxiliary.

395

#[instrument(skip_all, fields(expr = %expr))]

396

65057

pub fn to_aux_var_in(expr: &Expr, symbols: &mut SymbolTable) -> Option<(Reference, Expr)> {

397

65057

    let domain = to_aux_var_domain(expr)?;

398

54163

    Some(materialise_aux_var_in(expr, symbols, &domain))

399

65057

400

401

/// Whether `expr` is a matrix Minion's `element` can search directly.

402

///

403

/// A list qualifies. So does a matrix literal of atoms with a contiguous integer index domain,

404

/// since `introduce_element_from_index` shifts a non-1-based index onto `element`'s own positions.

405

/// Anything else -- a reference, or a literal still holding compound elements -- is left alone:

406

/// hoisting it into an auxiliary here would hide it from the representation rules that lower it.

407

6951

fn is_element_lowerable_subject(expr: &Expr) -> bool {

408

6951

    if expr.is_list() {

409

6720

        return true;

410

231

411

412

    // A literal matrix reaches here either spelled out or already folded into an atom.

413

231

    let index_domain = match expr {

414

        Expr::AbstractLiteral(_, AbstractLiteral::Matrix(elements, index_domain)) => {

415

21

            if !elements

416

21

                .iter()

417

49

                .all(|element| matches!(element, Expr::Atomic(_, _)))

418

419

21

                return false;

420

421

            let Ok(resolved) = index_domain.resolve() else {

422

                return false;

423

};

424

            resolved

425

426

        Expr::Atomic(

427

_,

428

            Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Matrix(_, index_domain))),

429

210

        ) => index_domain.clone(),

430

        _ => return false,

431

};

432

433

210

    let GroundDomain::Int(ranges, _) = index_domain.as_ref() else {

434

        return false;

435

};

436

210

    Range::is_contiguous(ranges)

437

6951

438

439

793918

fn to_aux_var_domain(expr: &Expr) -> Option<DomainPtr> {

440

    // No need to put an atom in an aux_var

441

793918

    if is_atom(expr) {

442

600488

        if cfg!(debug_assertions) {

443

600488

            trace!(why = "expression is an atom", "to_aux_var() failed");

444

445

600488

        return None;

446

193430

447

448

    // Anything that should be bubbled, bubble

449

193430

    let mut safe = true;

450

193430

    let mut categories = std::collections::HashSet::new();

451

1312044

    expr.for_each_expression(&mut |subexpr| {

452

1312044

        safe &= !matches!(

453

1312044

            subexpr,

454

1312044

            Expr::UnsafeDiv(_, _, _)

455

1312044

                | Expr::UnsafeMod(_, _, _)

456

1312044

                | Expr::UnsafePow(_, _, _)

457

1312044

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

458

1312044

                | Expr::Bubble(_, _, _)

459

1312044

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

460

1312044

);

461

1312044

        categories.insert(subexpr.category_of());

462

1312044

});

463

193430

    if !safe {

464

12

        if cfg!(debug_assertions) {

465

12

            trace!(why = "expression is unsafe", "to_aux_var() failed");

466

467

12

        return None;

468

193418

469

470

    // Do not put abstract literals containing expressions into aux vars.

471

//

472

    // e.g. for `[1,2,3,f/2,e][e]`, the lhs should not be put in an aux var.

473

//

474

    // instead, we should flatten the elements inside this abstract literal, or wait for it to be

475

    // turned into an atom, or an abstract literal containing only literals - e.g. through an index

476

    // or slice operation.

477

//

478

193418

    if let Expr::AbstractLiteral(_, _) = expr {

479

3955

        if cfg!(debug_assertions) {

480

3955

            trace!(

481

                why = "expression is an abstract literal",

482

                "to_aux_var() failed"

483

);

484

485

3955

        return None;

486

189463

487

488

    // Only flatten an expression if it contains decision variables or decision variables with some

489

    // constants.

490

//

491

    // i.e. dont flatten things containing givens, quantified variables, just constants, etc.

492

    bug_assert!(!categories.is_empty());

493

494

189463

    if !(categories.len() == 1 && categories.contains(&Category::Decision)

495

136996

        || categories.len() == 2

496

136233

            && categories.contains(&Category::Decision)

497

136233

            && categories.contains(&Category::Constant))

498

499

763

        if let Expr::ElementId(_, _, value) | Expr::IndexOf(_, _, value) = expr {

500

756

            let value_categories = value.universe_categories();

501

756

            if !(value_categories.len() == 1 && value_categories.contains(&Category::Decision)

502

756

                || value_categories.len() == 2

503

                    && value_categories.contains(&Category::Decision)

504

                    && value_categories.contains(&Category::Constant))

505

506

756

                if cfg!(debug_assertions) {

507

756

                    trace!(

508

                        why =

509

                            "expression has sub-expressions that are not in the decision category",

510

                        "to_aux_var() failed"

511

);

512

513

756

                return None;

514

515

        } else {

516

7

            if cfg!(debug_assertions) {

517

7

                trace!(

518

                    why = "expression has sub-expressions that are not in the decision category",

519

                    "to_aux_var() failed"

520

);

521

522

7

            return None;

523

524

188700

525

526

    // Avoid introducing auxvars for generic matrix indexing (can create many redundant auxvars

527

    // before comprehension expansion). However, keep list indexing eligible so Minion lowering

528

    // can introduce `element` constraints in non-equality contexts.

529

188700

    if let Expr::SafeIndex(_, subject, indices) = expr {

530

6951

        let index_has_element_id = indices

531

6951

            .iter()

532

6951

            .any(|index| matches!(index, Expr::ElementId(..) | Expr::IndexOf(..)));

533

6951

        let can_lower_via_element = is_element_lowerable_subject(subject)

534

6930

            && indices.iter().all(|i| matches!(i, Expr::Atomic(_, _)));

535

536

6951

        if !can_lower_via_element && !index_has_element_id {

537

4697

            if cfg!(debug_assertions) {

538

4697

                trace!(expr=%expr, why = "matrix indexing is not element-lowerable", "to_aux_var() failed");

539

540

4697

            return None;

541

2254

542

181749

543

544

184003

    let Some(domain) = expr.domain_of() else {

545

294

        if cfg!(debug_assertions) {

546

294

            trace!(expr=%expr, why = "could not find the domain of the expression", "to_aux_var() failed");

547

548

294

        return None;

549

};

550

551

183709

    Some(domain)

552

793918

553

554

15515

fn materialise_aux_var(expr: &Expr, symbols: &SymbolTable, domain: &DomainPtr) -> ToAuxVarOutput {

555

15515

    let mut symbols = symbols.clone();

556

15515

    let (reference, aux_expression) = materialise_aux_var_in(expr, &mut symbols, domain);

557

558

15515

    ToAuxVarOutput {

559

15515

        aux_reference: reference,

560

15515

        aux_expression,

561

15515

        symbols,

562

15515

        _unconstructable: (),

563

15515

564

15515

565

566

156492

fn materialise_aux_var_in(

567

156492

    expr: &Expr,

568

156492

    symbols: &mut SymbolTable,

569

156492

    domain: &DomainPtr,

570

156492

) -> (Reference, Expr) {

571

156492

    let decl = symbols.gen_find_auxiliary(domain);

572

156492

    let mut reference = Reference::new(decl);

573

156492

    let mut representation_constraints = Vec::new();

574

575

156492

    if let Some(preference) = domain.representation_preference() {

576

1

        let reference_name = reference.name().clone();

577

        let rule =

578

1

            get_applicable_repr_by_short_name(reference.ptr(), preference).unwrap_or_else(|| {

579

                bug!(

580

                    "representation `{preference}` inferred for auxiliary `{}` is not applicable",

581

                    reference_name

582

583

});

584

        let (repr_symbols, constraints) = {

585

1

            let (_, repr_symbols, constraints) = reference

586

1

                .select_or_init_repr_via(rule)

587

                .unwrap_or_else(|error| {

588

                    bug!(

589

                        "could not initialise representation `{preference}` for auxiliary `{}`: {error}",

590

                        reference_name

591

592

});

593

1

            (repr_symbols, constraints)

594

};

595

1

        symbols.update_insert(reference.ptr().clone());

596

1

        symbols.extend(repr_symbols);

597

1

        representation_constraints = constraints;

598

156491

599

600

156492

    if cfg!(debug_assertions) {

601

156492

        trace!(expr=%expr, "to_auxvar() succeeded in putting expr into an auxvar");

602

603

604

    let auxiliary =

605

156492

        Expr::AuxDeclaration(Metadata::new(), reference.clone(), Moo::new(expr.clone()));

606

156492

    let aux_expression = if representation_constraints.is_empty() {

607

156491

        auxiliary

608

    } else {

609

1

        let mut expressions = vec![auxiliary];

610

1

        expressions.extend(representation_constraints);

611

1

        Expr::And(Metadata::new(), Moo::new(into_matrix_expr!(expressions)))

612

};

613

614

156492

    (reference, aux_expression)

615

156492

616

617

/// Defers auxiliary variable allocation until a selected rule is materialised.

618

15521

pub fn defer_aux_var(

619

15521

    expr: &Expr,

620

15521

    build: impl Fn(ToAuxVarOutput) -> RuleEffect + Send + Sync + 'static,

621

15521

) -> Option<RuleEffect> {

622

15521

    let domain = to_aux_var_domain(expr)?;

623

15515

    let expr = expr.clone();

624

625

15515

    Some(RuleEffect::deferred(move |symbols| {

626

15515

        let aux = materialise_aux_var(&expr, symbols, &domain);

627

15515

        build(aux)

628

15515

}))

629

15521

630

631

/// Output passed to deferred auxiliary-effect builders.

632

pub struct ToAuxVarOutput {

633

    aux_reference: Reference,

634

    aux_expression: Expr,

635

    symbols: SymbolTable,

636

    _unconstructable: (),

637

638

639

impl ToAuxVarOutput {

640

    /// Returns the new auxiliary variable as an `Atom`.

641

15515

    pub fn as_atom(&self) -> Atom {

642

15515

        Atom::Reference(self.aux_reference.clone())

643

15515

644

645

    /// Returns the new auxiliary variable as an `Expression`.

646

///

647

    /// This expression will have default `Metadata`.

648

15515

    pub fn as_expr(&self) -> Expr {

649

15515

        Expr::Atomic(Metadata::new(), self.as_atom())

650

15515

651

652

    /// Returns the top level `Expression` to add to the model.

653

15515

    pub fn top_level_expr(&self) -> Expr {

654

15515

        self.aux_expression.clone()

655

15515

656

657

    /// Returns the new `SymbolTable`, modified to contain this auxiliary variable in the symbol table.

658

15515

    pub fn symbols(&self) -> SymbolTable {

659

15515

        self.symbols.clone()

660

15515

661

662

663

/// Clone comprehension with expression generator into its own detached comprehension scope

664

/// and rewrite all uses of the original quantified declaration to a fresh branch-local

665

/// expression generator.

666

68

pub fn replace_expression_generator_source(

667

68

    comp: &Comprehension,

668

68

    gen_decl: &DeclarationPtr,

669

68

    replacement_expr: Expr,

670

68

) -> (Comprehension, DeclarationPtr) {

671

    let replacement_ptr =

672

68

        DeclarationPtr::new_quantified_expr(gen_decl.name().clone(), replacement_expr);

673

68

    let mut comprehension = comp.clone();

674

675

    // detach the scope so rewriting this branch does not mutate the original

676

    // comprehension through shared pointers

677

68

    comprehension.symbols = comprehension.symbols.detach();

678

679

    // rewrite all uses of the original quantified declaration to the branch-local

680

    // generator declaration

681

68

    comprehension.return_expression =

682

68

        comprehension

683

68

            .return_expression

684

42

            .transform_bi(&|decl: DeclarationPtr| {

685

42

                if decl == *gen_decl {

686

12

                    replacement_ptr.clone()

687

                } else {

688

30

                    decl

689

690

42

});

691

692

68

    comprehension.qualifiers = comprehension

693

68

        .qualifiers

694

68

        .into_iter()

695

68

        .map(|qualifier| {

696

204

            qualifier.transform_bi(&|decl: DeclarationPtr| {

697

204

                if decl == *gen_decl {

698

68

                    replacement_ptr.clone()

699

                } else {

700

136

                    decl

701

702

204

})

703

68

})

704

        .collect();

705

706

    // keep the detached local scope in sync with the rewritten generator

707

    // declarations used by this branch

708

68

    comprehension

709

68

        .symbols

710

68

        .write()

711

68

        .update_insert(replacement_ptr.clone());

712

68

    for qualifier in &comprehension.qualifiers {

713

68

        match qualifier {

714

            ComprehensionQualifier::ExpressionGenerator { ptr }

715

            | ComprehensionQualifier::Generator { ptr } => {

716

68

                comprehension.symbols.write().update_insert(ptr.clone());

717

718

            ComprehensionQualifier::Condition(_) => {}

719

720

721

722

68

    (comprehension, replacement_ptr)

723

68

724

725

/// `Some(minimum)` iff `values` is a contiguous run of `Literal::Int`s starting at `minimum` --

726

/// the cheap case for [`unpack_literal_digit`], decodable as plain arithmetic rather than an

727

/// indexed lookup.

728

17473

pub fn contiguous_int_min(values: &[Literal]) -> Option<i32> {

729

17473

    let Literal::Int(minimum) = values.first()? else {

730

8216

        return None;

731

};

732

9257

    values

733

9257

        .iter()

734

9257

        .enumerate()

735

29932

        .all(|(offset, value)| *value == Literal::Int(*minimum + offset as i32))

736

9257

        .then_some(*minimum)

737

17473

738

739

/// Given a decoded position `digit` (a decision-variable expression, not necessarily constant --

740

/// this is what makes the compound case below non-trivial) and the ordered list of possible

741

/// literal values at that position, build an expression for "the value at position `digit`".

742

/// Shared between `TuplePacked` and `RecordPacked`'s own digit-decoding, since a packed field or

743

/// element can be either shape (and can nest one inside the other).

744

///

745

/// Scalar (bool, or non-contiguous int) values fall back to a plain `SafeIndex` into a literal

746

/// matrix of those values, dynamically indexed by `digit` -- the Minion backend already supports

747

/// that (the same shape `FunctionExplicit::values_matrix` uses). A *compound* (tuple or record)

748

/// value can't take that path: indexing a matrix of compound elements by a non-constant position

749

/// is not something the backend can turn into a per-field `Element` constraint chain, and it

750

/// silently produces an unresolved literal handed straight to the solver ("expected a literal but

751

/// got `AbstractLiteral(...)`"). Instead, each candidate's own fields are projected out (every

752

/// candidate shares the same shape, since the caller builds them all from one domain), and the

753

/// value is rebuilt as an inline tuple/record literal expression whose *own* fields are each

754

/// decoded recursively by this same function -- reusing `digit`, since every candidate is keyed by

755

/// the same packed position. A field that's itself a contiguous int range (the common case) hits

756

/// the cheap arithmetic path one level down; a doubly-nested compound value recurses again.

757

17473

pub fn unpack_literal_digit(digit: &Expr, values: &[Literal]) -> Expr {

758

17473

    if let Some(minimum) = contiguous_int_min(values) {

759

6294

        return match minimum {

760

            0 => digit.clone(),

761

6294

            minimum => essence_expr!(&digit + &minimum),

762

};

763

11179

764

11179

    if let Some(rebuilt) = unpack_compound_literal_digit(digit, values) {

765

989

        return rebuilt;

766

10190

767

10190

    let values = values.iter().cloned().map(Expr::from).collect::<Vec<_>>();

768

10190

    Expr::SafeIndex(

769

10190

        Metadata::new(),

770

10190

        Moo::new(into_matrix_expr!(values)),

771

10190

        vec![essence_expr!(&digit + 1)],

772

10190

773

17473

774

775

/// The compound-value case of [`unpack_literal_digit`]: `None` unless every value is a tuple (or

776

/// every value is a record with the same field names) -- guaranteed for a genuine packed field's

777

/// own value list, but checked directly rather than assumed, since a mismatch here should fall

778

/// back to the -- still correct, if unreduced until something else eliminates it -- generic path

779

/// instead of panicking.

780

11179

fn unpack_compound_literal_digit(digit: &Expr, values: &[Literal]) -> Option<Expr> {

781

11179

    match values.first()? {

782

        Literal::AbstractLiteral(AbstractLiteral::Tuple(first_fields)) => {

783

988

            let arity = first_fields.len();

784

988

            let mut field_values: Vec<Vec<Literal>> = vec![Vec::with_capacity(values.len()); arity];

785

988

            for value in values {

786

3952

                let Literal::AbstractLiteral(AbstractLiteral::Tuple(fields)) = value else {

787

                    return None;

788

};

789

3952

                if fields.len() != arity {

790

                    return None;

791

3952

792

3952

                for (slot, field) in field_values.iter_mut().zip(fields) {

793

7904

                    slot.push(field.clone());

794

795

796

988

            let rebuilt_fields = field_values

797

988

                .into_iter()

798

1976

                .map(|values| unpack_literal_digit(digit, &values))

799

                .collect();

800

988

            Some(Expr::AbstractLiteral(

801

988

                Metadata::new(),

802

988

                AbstractLiteral::Tuple(rebuilt_fields),

803

988

))

804

805

        Literal::AbstractLiteral(AbstractLiteral::Record(first_fields)) => {

806

1

            let names: Vec<_> = first_fields

807

1

                .iter()

808

2

                .map(|field| field.name.clone())

809

                .collect();

810

            let mut field_values: Vec<Vec<Literal>> =

811

1

                vec![Vec::with_capacity(values.len()); names.len()];

812

1

            for value in values {

813

4

                let Literal::AbstractLiteral(AbstractLiteral::Record(fields)) = value else {

814

                    return None;

815

};

816

4

                if fields.len() != names.len() {

817

                    return None;

818

4

819

4

                for (name, slot) in names.iter().zip(field_values.iter_mut()) {

820

8

                    let field_value = fields

821

8

                        .iter()

822

12

                        .find(|field| &field.name == name)?

823

                        .value

824

                        .clone();

825

8

                    slot.push(field_value);

826

827

828

1

            let rebuilt_fields = names

829

1

                .into_iter()

830

1

                .zip(field_values)

831

                .map(|(name, values)| Field {

832

2

                    name,

833

2

                    value: unpack_literal_digit(digit, &values),

834

2

})

835

                .collect();

836

1

            Some(Expr::AbstractLiteral(

837

1

                Metadata::new(),

838

1

                AbstractLiteral::Record(rebuilt_fields),

839

1

))

840

841

10190

        _ => None,

842

843

11179

844

845

/// Validate sparse tuple assignments and convert Essence positions to zero-based offsets.

846

22673

pub(crate) fn checked_short_table_row(expr: &Expr, width: usize) -> Option<Vec<(usize, Expr)>> {

847

22673

    let mut positions = std::collections::HashSet::new();

848

22673

    short_table_row_entries(expr)?

849

        .into_iter()

850

38458

        .map(|pair| {

851

38458

            let entries = tuple_expr_entries(&pair)?;

852

38458

            let [position, value] = entries.as_slice() else {

853

                return None;

854

};

855

38458

            let Literal::Int(position) = conjure_cp::ast::eval_constant(position)? else {

856

                return None;

857

};

858

38458

            let position = usize::try_from(position.checked_sub(1)?).ok()?;

859

38458

            if position >= width || !positions.insert(position) {

860

                return None;

861

38458

862

38458

            Some((position, value.clone()))

863

38458

})

864

        .collect()

865

22673