Grcov report - eval.rs

1

#![allow(dead_code)]

2

use crate::ast::enumerated::EnumVariant;

3

use crate::ast::{

4

    AbstractLiteral, Atom, DeclarationKind, Expression as Expr, Field, Literal as Lit, Metadata,

5

    Moo,

6

    comprehension::{Comprehension, ComprehensionQualifier},

7

    matrix,

8

};

9

use crate::bug_assert;

10

use crate::into_matrix;

11

use itertools::{Itertools as _, izip};

12

use std::cmp::Ordering as CmpOrdering;

13

use std::collections::HashSet;

14

15

use super::partial_eval::{run_partial_evaluator, run_partial_evaluator_local};

16

17

3436

pub(crate) fn factorial_i32(n: i32) -> Option<i32> {

18

3436

    if n < 0 {

19

        return None;

20

3436

21

22

3436

    (1..=n).try_fold(1_i32, i32::checked_mul)

23

3436

24

25

fn eval_constant_set(expr: &Expr) -> Option<Vec<Lit>> {

26

    let Lit::AbstractLiteral(AbstractLiteral::Set(values)) = eval_constant(expr)? else {

27

        return None;

28

};

29

30

    Some(values)

31

32

33

/// Compare literals only when their outer Essence literal kinds agree.

34

///

35

/// Inner types are guaranteed by expression type checking; keeping this guard here also makes

36

/// direct evaluator calls on unlike primitive or abstract literal kinds safely unevaluable.

37

10140294

fn equal_constant_literals(lhs: &Lit, rhs: &Lit) -> Option<bool> {

38

10140294

    match (lhs, rhs) {

39

12

        (Lit::EnumVariant(lhs), Lit::EnumVariant(rhs)) if lhs.ty == rhs.ty => {

40

12

            Some(lhs.variant == rhs.variant)

41

42

8

        (Lit::Unnamed(lhs), Lit::Unnamed(rhs)) if lhs.ty == rhs.ty => Some(lhs.value == rhs.value),

43

        (Lit::Int(_), Lit::Int(_)) | (Lit::Bool(_), Lit::Bool(_)) => {

44

9813847

            Some(lhs.essence_cmp(rhs) == CmpOrdering::Equal)

45

46

        (Lit::AbstractLiteral(lhs_abstract), Lit::AbstractLiteral(rhs_abstract))

47

326369

            if std::mem::discriminant(lhs_abstract) == std::mem::discriminant(rhs_abstract) =>

48

49

326369

            Some(lhs.essence_cmp(rhs) == CmpOrdering::Equal)

50

51

58

        _ => None,

52

53

10140294

54

55

/// Preserve already-distinct literal order; constant duplicates denote the same set member.

56

572073028

fn normalise_constant_set(mut literal: Lit) -> Lit {

57

572073028

    if let Lit::AbstractLiteral(AbstractLiteral::Set(items)) = &mut literal

58

3570878

        && super::literals::distinct_literal_count(items) != items.len()

59

60

39907

        items.sort_by(Lit::essence_cmp);

61

134302

        items.dedup_by(|a, b| a.essence_cmp(b).is_eq());

62

572033121

63

572073028

    literal

64

572073028

65

66

/// Simplify an expression to a constant using only constants already present at this node.

67

///

68

/// This is intended for the rewriter: child expressions should have been simplified by the

69

/// scheduler before their parent is considered. Use [`eval_constant`] when a caller explicitly

70

/// wants recursive evaluation of an arbitrary expression.

71

1641994121

pub fn eval_constant_local(expr: &Expr) -> Option<Lit> {

72

1641994121

    if !has_only_locally_evaluable_operands(expr) {

73

489088160

        return None;

74

1152905961

75

76

1152905961

    eval_constant(expr)

77

1641994121

78

79

/// Applies the evaluator normalisation hook to a focused expression.

80

///

81

/// Evaluators are privileged simplifications, not ordinary rewrite rules. The rewriter invokes

82

/// this hook before normal rule scheduling and immediately after a successful ordinary rule,

83

/// walking upward while evaluation keeps simplifying parents. This exploits the semantic property

84

/// that local constant and partial evaluation is always preferable to trying lower-priority rules,

85

/// while avoiding millions of failed universal `constant_evaluator` rule attempts.

86

///

87

/// Away from [`Expr::Root`], the hook is pure and local: it does not create auxiliaries, mutate

88

/// the symbol table, or recursively inspect arbitrary descendants. Children are expected to have

89

/// been normalised by the scheduler before their parent is evaluated.

90

///

91

/// At [`Expr::Root`], a selective deep pass runs over top-level constraints (skipping solver-flat

92

/// forms). Callers that know which root child changed should prefer

93

/// [`normalise_root_selective_deep_expr`] with `only_constraint` so sibling constraints are not

94

/// re-traversed. Local root-list reshaping (flatten top-level `and`) is intentionally deferred to

95

/// [`finish_root_evaluator_normalisation`]: doing it mid-loop materialises huge root lists and

96

/// explodes worklist rule attempts.

97

1679842111

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

98

1679842111

    match expr {

99

18157650

        Expr::Root(_, exprs) => normalise_root_constraints_selective_deep(exprs, None),

100

        // Focused `AbstractLiteral` literals must not repeatedly refold to themselves; parents

101

        // still see the `Atomic(Literal(...))` form when the hook walks upward.

102

14752959

        Expr::Atomic(_, Atom::Literal(Lit::AbstractLiteral(_))) => None,

103

1646931502

        _ => fold_constant_expression_local(expr).or_else(|| {

104

1637353590

            run_partial_evaluator_local(expr)

105

1637353590

                .ok()

106

5906254

                .map(|reduction| reduction.new_expression)

107

1637353590

}),

108

109

16430823

    .filter(|new_expr| new_expr != expr)

110

1679842111

111

112

/// Applies local root-list partial evaluation (strip `true`, propagate `false`, flatten `and`s).

113

1643252

pub fn normalise_root_constraints_local(exprs: &[Expr]) -> Option<Expr> {

114

1643252

    if exprs.is_empty() {

115

        return Some(Expr::Root(Metadata::new(), vec![true.into()]));

116

1643252

117

118

1643252

    let root = Expr::Root(Metadata::new(), exprs.to_vec());

119

1643252

    run_partial_evaluator_local(&root)

120

1643252

        .ok()

121

291711

        .map(|reduction| reduction.new_expression)

122

291711

        .filter(|new_root| new_root != &root)

123

1643252

124

125

/// Deep-normalises selected non-flat top-level constraints in `root`.

126

5

pub fn normalise_root_selective_deep_expr(

127

5

    root: &Expr,

128

5

    only_constraint: Option<usize>,

129

5

) -> Option<Expr> {

130

5

    let Expr::Root(_, exprs) = root else {

131

        return None;

132

};

133

134

5

    normalise_root_constraints_selective_deep(exprs, only_constraint)

135

5

136

137

4

pub fn normalise_root_constraints_deep(root: &Expr) -> Option<Expr> {

138

4

    normalise_root_selective_deep_expr(root, None)

139

4

140

141

/// Finishes evaluator normalisation on the model root after rewriting completes.

142

///

143

/// Applies local root-list partial evaluation to a fixpoint (strip `true`, propagate `false`,

144

/// flatten top-level `and`). Deep evaluation of individual constraints already runs during

145

/// rewriting via [`normalise_evaluator_local`] / [`normalise_root_selective_deep_expr`]; this

146

/// finish pass must not be inlined into the mid-loop Root hook because flattening `and` early

147

/// explodes worklist size on large expansions.

148

1351541

pub fn finish_root_evaluator_normalisation(root: &Expr) -> Option<Expr> {

149

1351541

    let Expr::Root(_, exprs) = root else {

150

        return None;

151

};

152

153

1351541

    let mut current = Expr::Root(Metadata::new(), exprs.clone());

154

1351541

    let mut changed = false;

155

1643250

    while let Expr::Root(_, current_exprs) = &current {

156

1643250

        let Some(next) = normalise_root_constraints_local(current_exprs) else {

157

1351541

            break;

158

};

159

291709

        current = next;

160

291709

        changed = true;

161

162

1351541

    changed.then_some(current)

163

1351541

164

165

/// Deep-normalises a single top-level constraint, or returns `None` if it is already normal.

166

///

167

/// Callers that know which root child changed should prefer this over rebuilding the whole root:

168

/// the root hook runs after every rewrite, so touching siblings there costs O(model size) per

169

/// rewrite.

170

183517137

pub fn normalise_root_constraint_deep(constraint: &Expr) -> Option<Expr> {

171

183517137

    if constraint_skips_deep_root_normalisation(constraint) {

172

181

        return None;

173

183516956

174

175

183516956

    normalise_constraint_deep_to_fixpoint(constraint)

176

183517137

177

178

18157655

fn normalise_root_constraints_selective_deep(

179

18157655

    exprs: &[Expr],

180

18157655

    only_constraint: Option<usize>,

181

18157655

) -> Option<Expr> {

182

18157655

    if exprs.is_empty() {

183

921978

        return Some(Expr::Root(Metadata::new(), vec![true.into()]));

184

17235677

185

186

    // Normalise first and only rebuild the root list once something has actually changed. Building

187

    // the replacement eagerly clones every sibling constraint on each call, which dominates the

188

    // post-rewrite root hook on models with many top-level constraints.

189

17235677

    let mut normalised: Vec<(usize, Expr)> = Vec::new();

190

17235677

    for (index, constraint) in exprs.iter().enumerate() {

191

183516698

        if only_constraint.is_some_and(|only| only != index) {

192

1

            continue;

193

183516697

194

195

183516697

        if let Some(replacement) = normalise_root_constraint_deep(constraint) {

196

36862

            normalised.push((index, replacement));

197

183479835

198

199

200

17235677

    if normalised.is_empty() {

201

17210995

        return None;

202

24682

203

204

24682

    let mut constraints = exprs.to_vec();

205

24682

    for (index, replacement) in normalised {

206

36862

        constraints[index] = replacement;

207

208

209

24682

    Some(Expr::Root(Metadata::new(), constraints))

210

18157655

211

212

/// Whether a top-level constraint has already been lowered to solver-flat form.

213

///

214

/// Deep root normalisation must not rewrite these: doing so can disturb auxiliaries introduced

215

/// for Minion (for example chained `FlatProductEq` constraints) or repeat expensive work.

216

183517137

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

217

183517137

    match expr {

218

        Expr::FlatProductEq(_, _, _, _)

219

        | Expr::FlatSumLeq(_, _, _)

220

        | Expr::FlatSumGeq(_, _, _)

221

        | Expr::FlatMinEq(_, _, _)

222

        | Expr::FlatIneq(_, _, _, _)

223

        | Expr::FlatMinusEq(_, _, _)

224

        | Expr::FlatAbsEq(_, _, _)

225

        | Expr::FlatAllDiff(_, _)

226

        | Expr::FlatTable(..)

227

        | Expr::FlatShortTable(..)

228

        | Expr::SmtDistinct(_, _)

229

        | Expr::FlatWeightedSumLeq(_, _, _, _)

230

        | Expr::FlatWeightedSumGeq(_, _, _, _)

231

        | Expr::FlatWatchedLiteral(_, _, _)

232

        | Expr::MinionDivEqUndefZero(_, _, _, _)

233

        | Expr::MinionModuloEqUndefZero(_, _, _, _)

234

        | Expr::MinionPow(_, _, _, _)

235

        | Expr::MinionReify(_, _, _)

236

        | Expr::MinionReifyImply(_, _, _)

237

        | Expr::MinionWInIntervalSet(_, _, _)

238

        | Expr::MinionWInSet(_, _, _)

239

181

        | Expr::MinionElementOne(_, _, _, _) => true,

240

6267915

        Expr::AuxDeclaration(_, _, inner) => matches!(

241

6267915

            inner.as_ref(),

242

            Expr::Product(_, _) | Expr::FlatProductEq(_, _, _, _)

243

),

244

177249041

        _ => false,

245

246

183517137

247

248

144531023

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

249

144531023

    let constant = eval_constant(expr)?;

250

36863

    fold_constant_expression(expr, constant).filter(|folded| folded != expr)

251

144531023

252

253

183516956

fn normalise_constraint_deep_to_fixpoint(constraint: &Expr) -> Option<Expr> {

254

183516956

    if matches!(constraint, Expr::Atomic(_, Atom::Literal(_))) {

255

39022795

        return None;

256

144494161

257

258

144494161

    let mut current = constraint.clone();

259

144494161

    let mut changed = false;

260

261

144531023

    while let Some(step) = fold_constant_expression_deep(&current)

262

144531021

        .or_else(|| partial_evaluator_deep_step(&current))

263

36862

        .filter(|step| step != &current)

264

265

36862

        current = step;

266

36862

        changed = true;

267

268

269

144494161

    changed

270

144494161

        .then_some(current)

271

36862

        .filter(|current| current != constraint)

272

183516956

273

274

144531021

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

275

144531021

    run_partial_evaluator(expr)

276

144531021

        .ok()

277

36860

        .map(|reduction| reduction.new_expression)

278

36860

        .filter(|new_expr| new_expr != expr)

279

144531021

280

281

/// Constant-folds `expr` locally unless doing so would inline a referenced matrix literal.

282

1646931502

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

283

1646931502

    let constant = match expr {

284

        // Comprehensions are atomic in arena traversal; evaluate them in one step here rather than

285

        // via operand checks that would repeat the same work for every parent.

286

4937381

        Expr::Comprehension(_, _) => eval_constant(expr)?,

287

1641994121

        _ => eval_constant_local(expr)?,

288

};

289

199605273

    fold_constant_expression(expr, constant).filter(|folded| folded != expr)

290

1646931502

291

292

199642136

fn fold_constant_expression(expr: &Expr, constant: Lit) -> Option<Expr> {

293

199642136

    if let Expr::Atomic(_, Atom::Literal(existing)) = expr

294

189955729

        && existing == &constant

295

296

189955729

        return None;

297

9686407

298

299

9686407

    if matches!(

300

9686407

        (expr, constant.clone()),

301

302

            Expr::Atomic(_, Atom::Reference(_)),

303

            Lit::AbstractLiteral(AbstractLiteral::Matrix(_, _))

304

305

) {

306

93670

        return None;

307

9592737

308

309

9592737

    let folded = Expr::Atomic(Metadata::new(), Atom::Literal(constant));

310

9592737

    if let Expr::TypeAnnotation(_, _, domain) = expr

311

8555

        && let Expr::Atomic(

312

8555

_,

313

8555

            Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Matrix(elems, _))),

314

8555

        ) = &folded

315

8555

        && elems.is_empty()

316

317

8555

        return Some(Expr::TypeAnnotation(

318

8555

            Metadata::new(),

319

8555

            Moo::new(folded),

320

8555

            domain.clone(),

321

8555

));

322

9584182

323

324

9584182

    if let Expr::DomainAnnotation(_, _, domain) = expr

325

6268

        && let Expr::Atomic(

326

6268

_,

327

6268

            Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Matrix(elems, _))),

328

6268

        ) = &folded

329

6268

        && elems.is_empty()

330

331

6268

        return Some(Expr::DomainAnnotation(

332

6268

            Metadata::new(),

333

6268

            Moo::new(folded),

334

6268

            domain.clone(),

335

6268

));

336

9577914

337

338

9577914

    if let Expr::Comprehension(_, comprehension) = expr

339

35613

        && let Expr::Atomic(

340

35613

_,

341

35613

            Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Matrix(elems, _))),

342

35613

        ) = &folded

343

35613

        && elems.is_empty()

344

6268

        && let Some(domain) = comprehension.domain_of()

345

346

6268

        return Some(Expr::DomainAnnotation(

347

6268

            Metadata::new(),

348

6268

            Moo::new(folded),

349

6268

            domain,

350

6268

));

351

9571646

352

353

9571646

    Some(folded)

354

199642136

355

356

1641994121

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

357

1641994121

    match expr {

358

189918868

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

359

        // Whether a reference resolves to a constant is the evaluator's result, not an

360

        // applicability question. Resolving it here would clone/evaluate the value letting and

361

        // then make eval_constant do the same work again.

362

582450297

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

363

256896316

        Expr::AbstractLiteral(_, lit) => abstract_literal_children_are_locally_evaluable(lit),

364

        Expr::TypeAnnotation(_, inner, _) | Expr::DomainAnnotation(_, inner, _) => {

365

14839

            is_locally_evaluable_expr(inner.as_ref())

366

367

        Expr::Comprehension(_, _) | Expr::Root(_, _) => false,

368

        // Visit children by reference. `Uniplate::children()` clones the whole child list, so on a

369

        // wide node (e.g. `or` over a large matrix) this test alone costs O(subtree); the evaluator

370

        // hook runs it on every ancestor after every rewrite, which makes rewriting quadratic.

371

        _ => {

372

612713801

            let mut all_constant = true;

373

831188673

            expr.for_each_expr_child(&mut |child| {

374

831188673

                all_constant = all_constant && is_locally_evaluable_expr(child);

375

831188673

});

376

612713801

            all_constant

377

378

379

1641994121

380

381

1714297238

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

382

1714297238

    match expr {

383

123331943

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

384

848793050

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

385

253069246

        Expr::AbstractLiteral(_, lit) => abstract_literal_children_are_locally_evaluable(lit),

386

        Expr::TypeAnnotation(_, inner, _) | Expr::DomainAnnotation(_, inner, _) => {

387

14839

            is_locally_evaluable_expr(inner.as_ref())

388

389

489088160

        _ => false,

390

391

1714297238

392

393

509965562

fn abstract_literal_children_are_locally_evaluable(lit: &AbstractLiteral<Expr>) -> bool {

394

509965562

    match lit {

395

        AbstractLiteral::Set(items)

396

        | AbstractLiteral::MSet(items)

397

        | AbstractLiteral::Tuple(items)

398

504021432

        | AbstractLiteral::Matrix(items, _) => items.iter().all(is_locally_evaluable_expr),

399

18705

        AbstractLiteral::Record(fields) => fields

400

18705

            .iter()

401

37410

            .all(|field| is_locally_evaluable_expr(&field.value)),

402

5319238

        AbstractLiteral::Sequence(items) => items.iter().all(is_locally_evaluable_expr),

403

        AbstractLiteral::Function(items) => items

404

            .iter()

405

            .all(|(from, to)| is_locally_evaluable_expr(from) && is_locally_evaluable_expr(to)),

406

2117

        AbstractLiteral::Relation(items) => items

407

2117

            .iter()

408

6351

            .all(|tuple| tuple.iter().all(is_locally_evaluable_expr)),

409

522

        AbstractLiteral::Partition(parts) => parts

410

522

            .iter()

411

522

            .all(|part| part.iter().all(is_locally_evaluable_expr)),

412

16298

        AbstractLiteral::Permutation(cycles) => cycles

413

16298

            .iter()

414

16733

            .all(|cycle| cycle.iter().all(is_locally_evaluable_expr)),

415

587250

        AbstractLiteral::Variant(field) => is_locally_evaluable_expr(&field.value),

416

417

509965562

418

419

/// Simplify an expression to a constant if possible

420

/// Returns:

421

/// `None` if the expression cannot be simplified to a constant (e.g. if it contains a variable)

422

/// `Some(Const)` if the expression can be simplified to a constant

423

2450011005

pub fn eval_constant(expr: &Expr) -> Option<Lit> {

424

2450011005

    match expr {

425

        Expr::TypeAnnotation(_, expr, _) | Expr::DomainAnnotation(_, expr, _) => {

426

29694

            eval_constant(expr)

427

428

        Expr::Supset(_, a, b) => {

429

            let (

430

                Lit::AbstractLiteral(AbstractLiteral::Set(a)),

431

                Lit::AbstractLiteral(AbstractLiteral::Set(b)),

432

348

            ) = (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?)

433

            else {

434

                return None;

435

};

436

437

348

            let a_set: HashSet<Lit> = a.iter().cloned().collect();

438

348

            let b_set: HashSet<Lit> = b.iter().cloned().collect();

439

440

348

            if a_set.difference(&b_set).count() > 0 {

441

261

                Some(Lit::Bool(a_set.is_superset(&b_set)))

442

            } else {

443

87

                Some(Lit::Bool(false))

444

445

446

        Expr::SupsetEq(_, a, b) => {

447

            let (

448

                Lit::AbstractLiteral(AbstractLiteral::Set(a)),

449

                Lit::AbstractLiteral(AbstractLiteral::Set(b)),

450

348

            ) = (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?)

451

            else {

452

                return None;

453

};

454

455

348

            Some(Lit::Bool(

456

348

                a.iter()

457

348

                    .cloned()

458

348

                    .collect::<HashSet<Lit>>()

459

348

                    .is_superset(&b.iter().cloned().collect::<HashSet<Lit>>()),

460

348

))

461

462

        Expr::Subset(_, a, b) => {

463

            let (

464

                Lit::AbstractLiteral(AbstractLiteral::Set(a)),

465

                Lit::AbstractLiteral(AbstractLiteral::Set(b)),

466

96889

            ) = (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?)

467

            else {

468

                return None;

469

};

470

471

435

            let a_set: HashSet<Lit> = a.iter().cloned().collect();

472

435

            let b_set: HashSet<Lit> = b.iter().cloned().collect();

473

474

435

            if b_set.difference(&a_set).count() > 0 {

475

348

                Some(Lit::Bool(a_set.is_subset(&b_set)))

476

            } else {

477

87

                Some(Lit::Bool(false))

478

479

480

        Expr::SubsetEq(_, a, b) => {

481

            let (

482

                Lit::AbstractLiteral(AbstractLiteral::Set(a)),

483

                Lit::AbstractLiteral(AbstractLiteral::Set(b)),

484

179135

            ) = (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?)

485

            else {

486

                return None;

487

};

488

489

377

            Some(Lit::Bool(

490

377

                a.iter()

491

377

                    .cloned()

492

377

                    .collect::<HashSet<Lit>>()

493

377

                    .is_subset(&b.iter().cloned().collect::<HashSet<Lit>>()),

494

377

))

495

496

        Expr::Intersect(_, a, b) => {

497

            let (

498

                Lit::AbstractLiteral(AbstractLiteral::Set(a)),

499

                Lit::AbstractLiteral(AbstractLiteral::Set(b)),

500

33060

            ) = (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?)

501

            else {

502

                return None;

503

};

504

505

15747

            let mut res: Vec<Lit> = Vec::new();

506

15747

            for lit in a {

507

28913

                if b.contains(&lit) && !res.contains(&lit) {

508

15573

                    res.push(lit);

509

13340

510

511

15747

            Some(Lit::AbstractLiteral(AbstractLiteral::Set(res)))

512

513

        Expr::Difference(_, a, b) => {

514

            let (

515

                Lit::AbstractLiteral(AbstractLiteral::Set(a)),

516

                Lit::AbstractLiteral(AbstractLiteral::Set(b)),

517

5199

            ) = (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?)

518

            else {

519

                return None;

520

};

521

522

4205

            let mut res: Vec<Lit> = Vec::new();

523

4205

            for lit in a {

524

12615

                if !b.contains(&lit) && !res.contains(&lit) {

525

8410

                    res.push(lit);

526

4205

527

528

4205

            Some(Lit::AbstractLiteral(AbstractLiteral::Set(res)))

529

530

        Expr::Union(_, a, b) => {

531

            let (

532

                Lit::AbstractLiteral(AbstractLiteral::Set(a)),

533

                Lit::AbstractLiteral(AbstractLiteral::Set(b)),

534

16921

            ) = (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?)

535

            else {

536

                return None;

537

};

538

539

13514

            let mut res: Vec<Lit> = Vec::new();

540

13514

            for lit in a {

541

26506

                res.push(lit);

542

543

13514

            for lit in b {

544

26506

                if !res.contains(&lit) {

545

17371

                    res.push(lit);

546

9135

547

548

13514

            Some(Lit::AbstractLiteral(AbstractLiteral::Set(res)))

549

550

        Expr::In(_, a, b) => {

551

5905408

            let member = eval_constant(a)?;

552

4621085

            let collection = eval_constant(b)?;

553

82844

            let values = generator_values_from_constant_collection(&collection)?;

554

141875

            Some(Lit::Bool(values.iter().any(|value| {

555

141875

                value.essence_cmp(&member) == CmpOrdering::Equal

556

141875

            })))

557

558

        Expr::FromSolution(_, _) => None,

559

        Expr::DominanceRelation(_, _) => None,

560

        Expr::InDomain(_, e, domain) => {

561

28246

            let Expr::Atomic(_, Atom::Literal(lit)) = e.as_ref() else {

562

28246

                return None;

563

};

564

565

            domain.contains(lit).ok().map(Into::into)

566

567

527240728

        Expr::Atomic(_, Atom::Literal(c)) => Some(normalise_constant_set(c.clone())),

568

        Expr::Atomic(_, Atom::Reference(reference)) => {

569

1070052148

            reference.resolve_constant().map(normalise_constant_set)

570

571

99437336

        Expr::AbstractLiteral(_, a) => Some(normalise_constant_set(Lit::AbstractLiteral(

572

99437336

            a.clone().into_literals()?,

573

        ))),

574

        Expr::Comprehension(_, comprehension) => {

575

8982450

            eval_constant_comprehension(comprehension.as_ref())

576

577

677151

        Expr::RecordField(_, rec, fld_name) => match eval_constant(rec.as_ref())? {

578

            Lit::AbstractLiteral(AbstractLiteral::Record(ents)) => {

579

8497

                for Field { name, value } in ents {

580

12731

                    if name.eq(fld_name) {

581

8497

                        return Some(value);

582

4234

583

584

                None

585

586

33873

            Lit::AbstractLiteral(AbstractLiteral::Variant(field)) if field.name == *fld_name => {

587

33873

                Some(field.value.clone())

588

589

            _ => None,

590

},

591

        Expr::UnsafeIndex(_, subject, indices) | Expr::SafeIndex(_, subject, indices) => {

592

80256385

            let subject: Lit = eval_constant(subject.as_ref())?;

593

13648554

            let indices: Vec<Lit> = indices

594

13648554

                .iter()

595

13648554

                .map(eval_constant)

596

13648554

                .collect::<Option<Vec<Lit>>>()?;

597

598

13014046

            match subject {

599

                Lit::AbstractLiteral(subject @ AbstractLiteral::Matrix(_, _)) => {

600

9987722

                    matrix::flatten_enumerate(subject)

601

36123853

                        .find(|(i, _)| i == &indices)

602

                        .map(|(_, x)| x)

603

604

                Lit::AbstractLiteral(subject @ AbstractLiteral::Tuple(_)) => {

605

3026324

                    let AbstractLiteral::Tuple(elems) = subject else {

606

                        return None;

607

};

608

609

                    bug_assert!(indices.len() == 1, "nested tuples not supported yet");

610

611

3026324

                    let Lit::Int(index) = indices[0].clone() else {

612

                        return None;

613

};

614

615

3026324

                    if elems.len() < index as usize || index < 1 {

616

                        return None;

617

3026324

618

619

                    // -1 for 0-indexing vs 1-indexing

620

3026324

                    let item = elems[index as usize - 1].clone();

621

622

3026324

                    Some(item)

623

624

                Lit::AbstractLiteral(subject @ AbstractLiteral::Record(_)) => {

625

                    let AbstractLiteral::Record(elems) = subject else {

626

                        return None;

627

};

628

629

                    bug_assert!(indices.len() == 1, "nested record not supported yet");

630

631

                    let Lit::Int(index) = indices[0].clone() else {

632

                        return None;

633

};

634

635

                    if elems.len() < index as usize || index < 1 {

636

                        return None;

637

638

639

                    // -1 for 0-indexing vs 1-indexing

640

                    let item = elems[index as usize - 1].clone();

641

                    Some(item.value)

642

643

                _ => None,

644

645

646

        Expr::UnsafeSlice(_, subject, indices) | Expr::SafeSlice(_, subject, indices) => {

647

1592388

            let subject: Lit = eval_constant(subject.as_ref())?;

648

2117

            let Lit::AbstractLiteral(subject @ AbstractLiteral::Matrix(_, _)) = subject else {

649

                return None;

650

};

651

652

2117

            let hole_dim = indices

653

2117

                .iter()

654

2117

                .cloned()

655

4234

                .position(|x| x.is_none())

656

2117

                .expect("slice expression should have a hole dimension");

657

658

2117

            let missing_domain = matrix::index_domains(&subject)[hole_dim].clone();

659

660

2117

            let indices: Vec<Option<Lit>> = indices

661

2117

                .iter()

662

2117

                .cloned()

663

4234

                .map(|x| {

664

                    // the outer option represents success of this iterator, the inner the index

665

                    // slice.

666

4234

                    match x {

667

2117

                        Some(x) => eval_constant(&x).map(Some),

668

2117

                        None => Some(None),

669

670

4234

})

671

                .collect::<Option<Vec<Option<Lit>>>>()?;

672

673

2117

            let indices_in_slice: Vec<Vec<Lit>> = missing_domain

674

2117

                .values()

675

2117

                .ok()?

676

6351

                .map(|i| {

677

6351

                    let mut indices = indices.clone();

678

6351

                    indices[hole_dim] = Some(i);

679

                    // These unwraps will only fail if we have multiple holes.

680

                    // As this is invalid, panicking is fine.

681

12702

                    indices.into_iter().map(|x| x.unwrap()).collect_vec()

682

6351

})

683

                .collect_vec();

684

685

            // Note: indices_in_slice is not necessarily sorted, so this is the best way.

686

2117

            let elems = matrix::flatten_enumerate(subject)

687

19053

                .filter(|(i, _)| indices_in_slice.contains(i))

688

                .map(|(_, elem)| elem)

689

                .collect();

690

691

2117

            Some(Lit::AbstractLiteral(into_matrix![elems]))

692

693

343302

        Expr::Abs(_, e) => un_op::<i32, i32>(|a| a.abs(), e).map(Lit::Int),

694

54210092

        Expr::Eq(_, a, b) => Some(Lit::Bool(equal_constant_literals(

695

54210092

            &eval_constant(a)?,

696

7109735

            &eval_constant(b)?,

697

29

        )?)),

698

13071486

        Expr::Neq(_, a, b) => Some(Lit::Bool(!equal_constant_literals(

699

13071486

            &eval_constant(a)?,

700

4040918

            &eval_constant(b)?,

701

29

        )?)),

702

9808010

        Expr::Lt(_, a, b) => bin_op::<i32, bool>(|a, b| a < b, a, b).map(Lit::Bool),

703

2225734

        Expr::Gt(_, a, b) => bin_op::<i32, bool>(|a, b| a > b, a, b).map(Lit::Bool),

704

22823442

        Expr::Leq(_, a, b) => bin_op::<i32, bool>(|a, b| a <= b, a, b).map(Lit::Bool),

705

3066030

        Expr::Geq(_, a, b) => bin_op::<i32, bool>(|a, b| a >= b, a, b).map(Lit::Bool),

706

109873492

        Expr::Not(_, expr) => un_op::<bool, bool>(|e| !e, expr).map(Lit::Bool),

707

        Expr::And(_, e) => {

708

44910816

            vec_lit_op::<bool, bool>(|e| e.iter().all(|&e| e), e.as_ref()).map(Lit::Bool)

709

710

1236502

        Expr::Table(_, _, _) | Expr::FlatTable(..) | Expr::FlatShortTable(..) => None,

711

510400

        Expr::NegativeTable(_, _, _) | Expr::ShortTable(_, _, _) => None,

712

683675

        Expr::AtLeast(_, _, _, _) => None,

713

143956

        Expr::AtMost(_, _, _, _) => None,

714

5771

        Expr::Gcc(_, _, _, _) | Expr::GccWeak(_, _, _, _) => None,

715

1152

        Expr::Root(_, _) => None,

716

        Expr::Or(_, es) => {

717

            // possibly cheating; definitely should be in partial eval instead

718

123585484

            for e in es.unwrap_list_cow()?.iter() {

719

330837848

                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(true))) = e {

720

86579

                    return Some(Lit::Bool(true));

721

330751269

};

722

723

724

123043090

            vec_lit_op::<bool, bool>(|e| e.iter().any(|&e| e), es.as_ref()).map(Lit::Bool)

725

726

        // A `catchUndef` still standing at constant-folding time has no bubble to consult, so the

727

        // inner expression is total here and the default is unreachable.

728

452806

        Expr::CatchUndef(_, a, _) => eval_constant(a),

729

14026150

        Expr::Imply(_, a, b) => bin_op::<bool, bool>(|a, b| !a || b, a, b).map(Lit::Bool),

730

8442711

        Expr::Iff(_, a, b) => bin_op::<bool, bool>(|a, b| a == b, a, b).map(Lit::Bool),

731

30575532

        Expr::Sum(_, exprs) => vec_lit_op::<i32, i32>(|e| e.iter().sum(), exprs).map(Lit::Int),

732

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

733

14026005

            vec_lit_op::<i32, i32>(|e| e.iter().product(), exprs).map(Lit::Int)

734

735

        Expr::FlatIneq(_, a, b, c) => {

736

444787

            let a: i32 = a.try_into().ok()?;

737

403929

            let b: i32 = b.try_into().ok()?;

738

            let c: i32 = c.try_into().ok()?;

739

740

            Some(Lit::Bool(a <= b + c))

741

742

        Expr::FlatSumGeq(_, exprs, a) => {

743

166911

            let sum = exprs.iter().try_fold(0, |acc, atom: &Atom| {

744

166911

                let n: i32 = atom.try_into().ok()?;

745

70870

                let acc = acc + n;

746

70870

                Some(acc)

747

166911

            })?;

748

749

29

            Some(Lit::Bool(sum >= a.try_into().ok()?))

750

751

        Expr::FlatSumLeq(_, exprs, a) => {

752

131775

            let sum = exprs.iter().try_fold(0, |acc, atom: &Atom| {

753

131775

                let n: i32 = atom.try_into().ok()?;

754

52679

                let acc = acc + n;

755

52679

                Some(acc)

756

131775

            })?;

757

758

29

            Some(Lit::Bool(sum >= a.try_into().ok()?))

759

760

        Expr::FlatMinEq(_, vars, result) => {

761

319

            let min = vars

762

319

                .iter()

763

348

                .try_fold(None, |acc: Option<i32>, atom: &Atom| {

764

348

                    let n: i32 = atom.try_into().ok()?;

765

29

                    Some(Some(acc.map_or(n, |m| m.min(n))))

766

348

                })??;

767

            let result: i32 = result.try_into().ok()?;

768

            Some(Lit::Bool(min == result))

769

770

        Expr::Min(_, e) => {

771

707079

            opt_vec_lit_op::<i32, i32>(|e| e.iter().min().copied(), e.as_ref()).map(Lit::Int)

772

773

        Expr::Max(_, e) => {

774

598056

            opt_vec_lit_op::<i32, i32>(|e| e.iter().max().copied(), e.as_ref()).map(Lit::Int)

775

776

        Expr::UnsafeDiv(_, a, b) | Expr::SafeDiv(_, a, b) => {

777

13761490

            super::floor_div(unwrap_expr::<i32>(a)?, unwrap_expr::<i32>(b)?).map(Lit::Int)

778

779

        Expr::UnsafeMod(_, a, b) | Expr::SafeMod(_, a, b) => {

780

7843875

            super::floor_mod(unwrap_expr::<i32>(a)?, unwrap_expr::<i32>(b)?).map(Lit::Int)

781

782

11542

        Expr::Substring(_, s, t) => match (s.as_ref(), t.as_ref()) {

783

784

                Expr::Atomic(_, Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Sequence(s)))),

785

                Expr::Atomic(_, Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Sequence(t)))),

786

            ) => {

787

                if s.len() > t.len() {

788

                    return Some(Lit::Bool(false));

789

790

791

                let found = t.windows(s.len()).any(|window| window == s.as_slice());

792

                Some(Lit::Bool(found))

793

794

11542

            _ => None,

795

},

796

2523

        Expr::Subsequence(_, s, t) => match (s.as_ref(), t.as_ref()) {

797

798

                Expr::Atomic(_, Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Sequence(s)))),

799

                Expr::Atomic(_, Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Sequence(t)))),

800

            ) => {

801

                let mut i = 0;

802

                let mut j = 0;

803

804

                while i < s.len() && j < t.len() {

805

                    if s[i] == t[j] {

806

                        i += 1;

807

808

                    j += 1;

809

810

811

                Some(Lit::Bool(i == s.len()))

812

813

2523

            _ => None,

814

},

815

        Expr::MinionDivEqUndefZero(_, a, b, c) => {

816

            // div always rounds down

817

122046

            let a: i32 = a.try_into().ok()?;

818

29

            let b: i32 = b.try_into().ok()?;

819

            let c: i32 = c.try_into().ok()?;

820

821

            if b == 0 {

822

                return None;

823

824

825

            let a = a as f32;

826

            let b = b as f32;

827

            let div: i32 = (a / b).floor() as i32;

828

            Some(Lit::Bool(div == c))

829

830

241803

        Expr::Bubble(_, a, b) => bin_op::<bool, bool>(|a, b| a && b, a, b).map(Lit::Bool),

831

        Expr::MinionReify(_, a, b) => {

832

1665

            let result = eval_constant(a)?;

833

834

1077

            let result: bool = result.try_into().ok()?;

835

1077

            let b: bool = b.try_into().ok()?;

836

837

            Some(Lit::Bool(b == result))

838

839

        Expr::MinionReifyImply(_, a, b) => {

840

432

            let result = eval_constant(a)?;

841

842

            let result: bool = result.try_into().ok()?;

843

            let b: bool = b.try_into().ok()?;

844

845

            if b {

846

                Some(Lit::Bool(result))

847

            } else {

848

                Some(Lit::Bool(true))

849

850

851

        Expr::MinionModuloEqUndefZero(_, a, b, c) => {

852

            // From Savile Row. Same semantics as division.

853

//

854

            //   a - (b * floor(a/b))

855

//

856

            // We don't use % as it has the same semantics as /. We don't use / as we want to round

857

            // down instead, not towards zero.

858

859

124134

            let a: i32 = a.try_into().ok()?;

860

29

            let b: i32 = b.try_into().ok()?;

861

            let c: i32 = c.try_into().ok()?;

862

863

            if b == 0 {

864

                return None;

865

866

867

            let modulo = super::floor_mod(a, b)?;

868

            Some(Lit::Bool(modulo == c))

869

870

        Expr::MinionPow(_, a, b, c) => {

871

            // only available for positive a b c

872

873

1421

            let a: i32 = a.try_into().ok()?;

874

            let b: i32 = b.try_into().ok()?;

875

            let c: i32 = c.try_into().ok()?;

876

877

            if a <= 0 {

878

                return None;

879

880

881

            if b <= 0 {

882

                return None;

883

884

885

            if c <= 0 {

886

                return None;

887

888

889

            Some(Lit::Bool(a ^ b == c))

890

891

261

        Expr::MinionWInSet(_, _, _) => None,

892

        Expr::MinionWInIntervalSet(_, x, intervals) => {

893

609

            let x_lit: &Lit = x.try_into().ok()?;

894

895

            let x_lit = match x_lit.clone() {

896

                Lit::Int(i) => Some(i),

897

                Lit::Bool(true) => Some(1),

898

                Lit::Bool(false) => Some(0),

899

                _ => None,

900

}?;

901

902

            let mut intervals = intervals.iter();

903

            while let Some(lower) = intervals.next() {

904

                let Some(upper) = intervals.next() else {

905

                    break;

906

};

907

                if &x_lit >= lower && &x_lit <= upper {

908

                    return Some(Lit::Bool(true));

909

910

911

912

            Some(Lit::Bool(false))

913

914

        Expr::Flatten(_, _, _) => {

915

            // TODO

916

3044826

            None

917

918

        // Constant folding treats the SMT-native form exactly like the one it came from.

919

        Expr::AllDiff(_, e) | Expr::SmtDistinct(_, e) => {

920

1500445

            let es = e.unwrap_list_cow()?;

921

29232

            let mut lits: HashSet<Lit> = HashSet::new();

922

29232

            for expr in es.iter() {

923

33814

                let Expr::Atomic(_, Atom::Literal(x)) = expr else {

924

27028

                    return None;

925

};

926

6786

                match x {

927

                    Lit::Int(_) | Lit::Bool(_) | Lit::EnumVariant(_) | Lit::Unnamed(_) => {

928

6786

                        if lits.contains(x) {

929

                            return Some(Lit::Bool(false));

930

                        } else {

931

6786

                            lits.insert(x.clone());

932

933

934

                    Lit::AbstractLiteral(_) => return None, // Reject AbstractLiteral cases

935

936

937

2204

            Some(Lit::Bool(true))

938

939

        Expr::FlatAllDiff(_, es) => {

940

7523

            let mut lits: HashSet<Lit> = HashSet::new();

941

7523

            for atom in es {

942

7523

                let Atom::Literal(x) = atom else {

943

7523

                    return None;

944

};

945

946

                match x {

947

                    Lit::Int(_) | Lit::Bool(_) | Lit::EnumVariant(_) | Lit::Unnamed(_) => {

948

                        if lits.contains(x) {

949

                            return Some(Lit::Bool(false));

950

                        } else {

951

                            lits.insert(x.clone());

952

953

954

                    Lit::AbstractLiteral(_) => return None, // Reject AbstractLiteral cases

955

956

957

            Some(Lit::Bool(true))

958

959

1262859

        Expr::FlatWatchedLiteral(_, _, _) => None,

960

6297150

        Expr::AuxDeclaration(_, _, _) => None,

961

367056

        Expr::Neg(_, a) => match eval_constant(a.as_ref())? {

962

100455

            Lit::Int(a) => Some(Lit::Int(-a)),

963

            _ => None,

964

},

965

2523

        Expr::Factorial(_, a) => match eval_constant(a.as_ref())? {

966

2523

            Lit::Int(a) => factorial_i32(a).map(Lit::Int),

967

            _ => None,

968

},

969

19480985

        Expr::Minus(_, a, b) => bin_op::<i32, i32>(|a, b| a - b, a, b).map(Lit::Int),

970

        Expr::FlatMinusEq(_, a, b) => {

971

1856

            let a: i32 = a.try_into().ok()?;

972

            let b: i32 = b.try_into().ok()?;

973

            Some(Lit::Bool(a == -b))

974

975

        Expr::FlatProductEq(_, a, b, c) => {

976

7732

            let a: i32 = a.try_into().ok()?;

977

            let b: i32 = b.try_into().ok()?;

978

            let c: i32 = c.try_into().ok()?;

979

            Some(Lit::Bool(a * b == c))

980

981

        Expr::FlatWeightedSumLeq(_, cs, vs, total) => {

982

13293

            let cs: Vec<i32> = cs

983

13293

                .iter()

984

38247

                .map(|x| TryInto::<i32>::try_into(x).ok())

985

                .collect::<Option<Vec<i32>>>()?;

986

13293

            let vs: Vec<i32> = vs

987

13293

                .iter()

988

21732

                .map(|x| TryInto::<i32>::try_into(x).ok())

989

13293

                .collect::<Option<Vec<i32>>>()?;

990

            let total: i32 = total.try_into().ok()?;

991

992

            let sum: i32 = izip!(cs, vs).fold(0, |acc, (c, v)| acc + (c * v));

993

994

            Some(Lit::Bool(sum <= total))

995

996

        Expr::FlatWeightedSumGeq(_, cs, vs, total) => {

997

12684

            let cs: Vec<i32> = cs

998

12684

                .iter()

999

36855

                .map(|x| TryInto::<i32>::try_into(x).ok())

1000

                .collect::<Option<Vec<i32>>>()?;

1001

12684

            let vs: Vec<i32> = vs

1002

12684

                .iter()

1003

21152

                .map(|x| TryInto::<i32>::try_into(x).ok())

1004

12684

                .collect::<Option<Vec<i32>>>()?;

1005

            let total: i32 = total.try_into().ok()?;

1006

1007

            let sum: i32 = izip!(cs, vs).fold(0, |acc, (c, v)| acc + (c * v));

1008

1009

            Some(Lit::Bool(sum >= total))

1010

1011

        Expr::FlatAbsEq(_, x, y) => {

1012

435

            let x: i32 = x.try_into().ok()?;

1013

29

            let y: i32 = y.try_into().ok()?;

1014

1015

            Some(Lit::Bool(x == y.abs()))

1016

1017

        Expr::UnsafePow(_, a, b) | Expr::SafePow(_, a, b) => {

1018

1576233

            let a: &Atom = a.try_into().ok()?;

1019

1487870

            let a: i32 = a.try_into().ok()?;

1020

1021

1098186

            let b: &Atom = b.try_into().ok()?;

1022

1098186

            let b: i32 = b.try_into().ok()?;

1023

1024

1097838

            if (a != 0 || b != 0) && b >= 0 {

1025

1097838

                Some(Lit::Int(a.pow(b as u32)))

1026

            } else {

1027

                None

1028

1029

1030

        Expr::Metavar(_, _) => None,

1031

24770

        Expr::MinionElementOne(_, _, _, _) => None,

1032

        Expr::ToInt(_, expression) => {

1033

101610989

            let lit = eval_constant(expression.as_ref())?;

1034

30988280

            match lit {

1035

                Lit::Int(_) => Some(lit),

1036

16133490

                Lit::Bool(true) => Some(Lit::Int(1)),

1037

14854790

                Lit::Bool(false) => Some(Lit::Int(0)),

1038

                _ => None,

1039

1040

1041

219078

        Expr::SatObjective(..) => None,

1042

        Expr::SATInt(_, _, _, _) => {

1043

            // TODO: If this SATInt is composed of literals, we should evaluate it back to an

1044

            // integer literal.

1045

//

1046

            // This is important because `is_all_constant` currently returns true for SATInts

1047

            // containing no references. If we don't evaluate them here, bubble rules will skip

1048

            // them (thinking they'll be constant-folded later), but they'll actually reach

1049

            // the solver adaptors as un-encoded unsafe operations, causing panics.

1050

36158139

            None

1051

1052

        Expr::PairwiseSum(_, a, b) => {

1053

            match (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?) {

1054

                (Lit::Int(a_int), Lit::Int(b_int)) => Some(Lit::Int(a_int + b_int)),

1055

                _ => None,

1056

1057

1058

        Expr::PairwiseProduct(_, a, b) => {

1059

            match (eval_constant(a.as_ref())?, eval_constant(b.as_ref())?) {

1060

                (Lit::Int(a_int), Lit::Int(b_int)) => Some(Lit::Int(a_int * b_int)),

1061

                _ => None,

1062

1063

1064

        Expr::Defined(_, f) => {

1065

19981

            let Lit::AbstractLiteral(AbstractLiteral::Function(pairs)) = eval_constant(f)? else {

1066

                return None;

1067

};

1068

            Some(Lit::AbstractLiteral(AbstractLiteral::Set(

1069

                pairs.into_iter().map(|(key, _)| key).collect(),

1070

)))

1071

1072

        Expr::Range(_, f) => {

1073

44718

            let Lit::AbstractLiteral(AbstractLiteral::Function(pairs)) = eval_constant(f)? else {

1074

                return None;

1075

};

1076

            let mut values = Vec::new();

1077

            for (_, value) in pairs {

1078

                if !values.contains(&value) {

1079

                    values.push(value);

1080

1081

1082

            Some(Lit::AbstractLiteral(AbstractLiteral::Set(values)))

1083

1084

        Expr::Image(_, f, arg) => {

1085

930268

            let arg = eval_constant(arg)?;

1086

168380

            match eval_constant(f)? {

1087

                Lit::AbstractLiteral(AbstractLiteral::Function(pairs)) => pairs

1088

                    .into_iter()

1089

                    .find(|(key, _)| *key == arg)

1090

                    .map(|(_, value)| value),

1091

                // A sequence is a function from int(1..n), so applying it reads the entry at

1092

                // that one-based position. Out of range is undefined, so unevaluable.

1093

                Lit::AbstractLiteral(AbstractLiteral::Sequence(values)) => {

1094

                    let Lit::Int(index) = arg else {

1095

                        return None;

1096

};

1097

                    usize::try_from(index)

1098

                        .ok()

1099

                        .filter(|index| *index >= 1)

1100

                        .and_then(|index| values.get(index - 1).cloned())

1101

1102

                // Cycle notation: find which cycle (if any) mentions `arg` and return the next

1103

                // element in it (wrapping around); an element mentioned in no cycle is an

1104

                // implicit fixed point, mapping to itself.

1105

                Lit::AbstractLiteral(AbstractLiteral::Permutation(cycles)) => {

1106

10591

                    for cycle in &cycles {

1107

19070

                        if let Some(pos) = cycle.iter().position(|x| *x == arg) {

1108

6356

                            return Some(cycle[(pos + 1) % cycle.len()].clone());

1109

4237

1110

1111

4235

                    Some(arg)

1112

1113

                _ => None,

1114

1115

1116

        Expr::PreImage(_, f, img) => {

1117

            let Lit::AbstractLiteral(AbstractLiteral::Function(pairs)) = eval_constant(f)? else {

1118

                return None;

1119

};

1120

            let img = eval_constant(img)?;

1121

            let mut keys = Vec::new();

1122

            for (key, value) in pairs {

1123

                if value == img && !keys.contains(&key) {

1124

                    keys.push(key);

1125

1126

1127

            Some(Lit::AbstractLiteral(AbstractLiteral::Set(keys)))

1128

1129

        // Not yet needed by any in-scope function case; the partial evaluator already refuses

1130

        // these gracefully (Err(RuleNotApplicable)) rather than panicking.

1131

        Expr::ImageSet(_, _, _) => None,

1132

1450

        Expr::Inverse(_, _, _) => None,

1133

        Expr::PermInverse(_, _) => None,

1134

        Expr::Compose(_, _, _) => None,

1135

        Expr::Restrict(_, _, _) => None,

1136

        Expr::ToSet(_, _) => None,

1137

        Expr::ToMSet(_, _) => None,

1138

        Expr::ToRelation(_, _) => None,

1139

        Expr::Active(_, variant, alternative) => {

1140

            let Lit::AbstractLiteral(AbstractLiteral::Variant(field)) =

1141

193258

                eval_constant(variant.as_ref())?

1142

            else {

1143

                return None;

1144

};

1145

67746

            Some(Lit::Bool(field.name == *alternative))

1146

1147

        Expr::RelationProj(_, _, _) => todo!(),

1148

        // Not yet needed by any in-scope partition case; the partial evaluator already refuses

1149

        // these gracefully (Err(RuleNotApplicable)) rather than panicking. Constant partition

1150

        // literal equality/membership already works via the generic Literal equality path above,

1151

        // without going through these operators at all.

1152

        Expr::Apart(_, _, _) => None,

1153

        Expr::Together(_, _, _) => None,

1154

        Expr::Participants(_, _) => None,

1155

        Expr::Party(_, _, _) => None,

1156

        Expr::Parts(_, _) => None,

1157

        Expr::Card(_, collection) => {

1158

341493

            let Lit::AbstractLiteral(collection) = eval_constant(collection)? else {

1159

                return None;

1160

};

1161

141621

            let length = match collection {

1162

130097

                AbstractLiteral::Set(values) => super::literals::distinct_literal_count(&values),

1163

                AbstractLiteral::MSet(values)

1164

                | AbstractLiteral::Sequence(values)

1165

5173

                | AbstractLiteral::Matrix(values, _) => values.len(),

1166

                AbstractLiteral::Function(entries) => entries.len(),

1167

2117

                AbstractLiteral::Relation(entries) => entries.len(),

1168

                // A permutation's cardinality is its numMoved count -- how many elements are

1169

                // mentioned in some cycle -- not the number of cycles, matching the same

1170

                // "unmentioned = fixed point" convention used everywhere else for permutations

1171

                // (contains()'s size check, PermutationAsFunction's own numMoved structural

1172

                // constraint).

1173

4234

                AbstractLiteral::Permutation(cycles) => cycles.iter().flatten().count(),

1174

                _ => return None,

1175

};

1176

141621

            i32::try_from(length).ok().map(Lit::Int)

1177

1178

        Expr::LexLt(_, a, b) => {

1179

742603

            let lt = vec_expr_pairs_op::<i32, _>(a, b, |pairs, (a_len, b_len)| {

1180

348

                pairs

1181

348

                    .iter()

1182

696

                    .find_map(|(a, b)| match a.cmp(b) {

1183

174

                        CmpOrdering::Less => Some(true),     // First difference is <

1184

                        CmpOrdering::Greater => Some(false), // First difference is >

1185

522

                        CmpOrdering::Equal => None,          // No difference

1186

696

})

1187

348

                    .unwrap_or(a_len < b_len) // [1,1] <lex [1,1,x]

1188

742255

            })?;

1189

348

            Some(lt.into())

1190

1191

        Expr::LexLeq(_, a, b) => {

1192

766673

            let lt = vec_expr_pairs_op::<i32, _>(a, b, |pairs, (a_len, b_len)| {

1193

174

                pairs

1194

174

                    .iter()

1195

348

                    .find_map(|(a, b)| match a.cmp(b) {

1196

174

                        CmpOrdering::Less => Some(true),

1197

                        CmpOrdering::Greater => Some(false),

1198

174

                        CmpOrdering::Equal => None,

1199

348

})

1200

174

                    .unwrap_or(a_len <= b_len) // [1,1] <=lex [1,1,x]

1201

766499

            })?;

1202

174

            Some(lt.into())

1203

1204

60349

        Expr::LexGt(_, a, b) => eval_constant(&Expr::LexLt(Metadata::new(), b.clone(), a.clone())),

1205

        Expr::LexGeq(_, a, b) => {

1206

130384

            eval_constant(&Expr::LexLeq(Metadata::new(), b.clone(), a.clone()))

1207

1208

        Expr::FlatLexLt(_, a, b) => {

1209

8845

            let lt = atoms_pairs_op::<i32, _>(a, b, |pairs, (a_len, b_len)| {

1210

                pairs

1211

                    .iter()

1212

                    .find_map(|(a, b)| match a.cmp(b) {

1213

                        CmpOrdering::Less => Some(true),

1214

                        CmpOrdering::Greater => Some(false),

1215

                        CmpOrdering::Equal => None,

1216

})

1217

                    .unwrap_or(a_len < b_len)

1218

8845

            })?;

1219

            Some(lt.into())

1220

1221

        Expr::FlatLexLeq(_, a, b) => {

1222

3074

            let lt = atoms_pairs_op::<i32, _>(a, b, |pairs, (a_len, b_len)| {

1223

                pairs

1224

                    .iter()

1225

                    .find_map(|(a, b)| match a.cmp(b) {

1226

                        CmpOrdering::Less => Some(true),

1227

                        CmpOrdering::Greater => Some(false),

1228

                        CmpOrdering::Equal => None,

1229

})

1230

                    .unwrap_or(a_len <= b_len)

1231

3074

            })?;

1232

            Some(lt.into())

1233

1234

        Expr::Pred(_, expr) => {

1235

            let ev = unwrap_expr::<EnumVariant>(expr)?;

1236

            ev.pred().map(Lit::EnumVariant)

1237

1238

        Expr::Succ(_, expr) => {

1239

16

            let ev = unwrap_expr::<EnumVariant>(expr)?;

1240

16

            ev.succ().map(Lit::EnumVariant)

1241

1242

        Expr::AllDifferentExcept(_, _, _) | Expr::ElementId(_, _, _) | Expr::IndexOf(_, _, _) => {

1243

1295546

            None

1244

1245

        // Needs the target's domain to expand, which this function has no access to; the

1246

        // fallback rewrite rule (passes::attribute_as_constraint) handles expansion instead.

1247

        Expr::AttributeAsConstraint(_, _, _, _)

1248

        | Expr::SatElement(_, _, _, _)

1249

1290152

        | Expr::SatAllDifferentComparisons(_, _) => None,

1250

1251

2450011005

1252

1253

110216794

pub fn un_op<T, A>(f: fn(T) -> A, a: &Expr) -> Option<A>

1254

110216794

where

1255

110216794

    T: TryFrom<Lit>,

1256

1257

110216794

    let a = unwrap_expr::<T>(a)?;

1258

339413

    Some(f(a))

1259

110216794

1260

1261

80114865

pub fn bin_op<T, A>(f: fn(T, T) -> A, a: &Expr, b: &Expr) -> Option<A>

1262

80114865

where

1263

80114865

    T: TryFrom<Lit>,

1264

1265

80114865

    let a = unwrap_expr::<T>(a)?;

1266

41051475

    let b = unwrap_expr::<T>(b)?;

1267

27165896

    Some(f(a, b))

1268

80114865

1269

1270

#[allow(dead_code)]

1271

pub fn tern_op<T, A>(f: fn(T, T, T) -> A, a: &Expr, b: &Expr, c: &Expr) -> Option<A>

1272

where

1273

    T: TryFrom<Lit>,

1274

1275

    let a = unwrap_expr::<T>(a)?;

1276

    let b = unwrap_expr::<T>(b)?;

1277

    let c = unwrap_expr::<T>(c)?;

1278

    Some(f(a, b, c))

1279

1280

1281

pub fn vec_op<T, A>(f: fn(Vec<T>) -> A, a: &[Expr]) -> Option<A>

1282

where

1283

    T: TryFrom<Lit>,

1284

1285

    let a = a.iter().map(unwrap_expr).collect::<Option<Vec<T>>>()?;

1286

    Some(f(a))

1287

1288

1289

212555443

pub fn vec_lit_op<T, A>(f: fn(Vec<T>) -> A, a: &Expr) -> Option<A>

1290

212555443

where

1291

212555443

    T: TryFrom<Lit>,

1292

1293

212555443

    Some(f(eval_list_items(a)?))

1294

212555443

1295

1296

type PairsCallback<T, A> = fn(Vec<(T, T)>, (usize, usize)) -> A;

1297

1298

/// Calls the given function on each consecutive pair of elements in the list expressions.

1299

/// Also passes the length of the two lists.

1300

1509276

fn vec_expr_pairs_op<T, A>(a: &Expr, b: &Expr, f: PairsCallback<T, A>) -> Option<A>

1301

1509276

where

1302

1509276

    T: TryFrom<Lit>,

1303

1304

1509276

    let a_exprs = a.clone().unwrap_matrix_unchecked()?.0;

1305

576781

    let b_exprs = b.clone().unwrap_matrix_unchecked()?.0;

1306

576781

    let lens = (a_exprs.len(), b_exprs.len());

1307

1308

576781

    let lit_pairs = std::iter::zip(a_exprs, b_exprs)

1309

577303

        .map(|(a, b)| Some((unwrap_expr(&a)?, unwrap_expr(&b)?)))

1310

576259

        .collect::<Option<Vec<(T, T)>>>()?;

1311

522

    Some(f(lit_pairs, lens))

1312

1509276

1313

1314

/// Same as [`vec_expr_pairs_op`], but over slices of atoms.

1315

11919

fn atoms_pairs_op<T, A>(a: &[Atom], b: &[Atom], f: PairsCallback<T, A>) -> Option<A>

1316

11919

where

1317

11919

    T: TryFrom<Atom>,

1318

1319

11919

    let lit_pairs = Iterator::zip(a.iter(), b.iter())

1320

11919

        .map(|(a, b)| Some((a.clone().try_into().ok()?, b.clone().try_into().ok()?)))

1321

11919

        .collect::<Option<Vec<(T, T)>>>()?;

1322

    Some(f(lit_pairs, (a.len(), b.len())))

1323

11919

1324

1325

pub fn opt_vec_op<T, A>(f: fn(Vec<T>) -> Option<A>, a: &[Expr]) -> Option<A>

1326

where

1327

    T: TryFrom<Lit>,

1328

1329

    let a = a.iter().map(unwrap_expr).collect::<Option<Vec<T>>>()?;

1330

    f(a)

1331

1332

1333

1305135

pub fn opt_vec_lit_op<T, A>(f: fn(Vec<T>) -> Option<A>, a: &Expr) -> Option<A>

1334

1305135

where

1335

1305135

    T: TryFrom<Lit>,

1336

1337

1305135

    f(eval_list_items(a)?)

1338

1305135

1339

1340

#[allow(dead_code)]

1341

pub fn flat_op<T, A>(f: fn(Vec<T>, T) -> A, a: &[Expr], b: &Expr) -> Option<A>

1342

where

1343

    T: TryFrom<Lit>,

1344

1345

    let a = a.iter().map(unwrap_expr).collect::<Option<Vec<T>>>()?;

1346

    let b = unwrap_expr::<T>(b)?;

1347

    Some(f(a, b))

1348

1349

1350

497660767

pub fn unwrap_expr<T: TryFrom<Lit>>(expr: &Expr) -> Option<T> {

1351

497660767

    let c = eval_constant(expr)?;

1352

133656284

    TryInto::<T>::try_into(c).ok()

1353

497660767

1354

1355

213860578

fn eval_list_items<T>(expr: &Expr) -> Option<Vec<T>>

1356

213860578

where

1357

213860578

    T: TryFrom<Lit>,

1358

1359

213860578

    if let Some((items, _)) = expr.unwrap_matrix_unchecked_ref() {

1360

203175985

        return items.iter().map(unwrap_expr).collect();

1361

10684593

1362

1363

10684593

    let collection = eval_constant(expr)?;

1364

6375036

    generator_values_from_constant_collection(&collection)?

1365

        .into_iter()

1366

6375036

        .map(TryInto::try_into)

1367

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

1368

        .ok()

1369

213860578

1370

1371

8982450

fn eval_constant_comprehension(comprehension: &Comprehension) -> Option<Lit> {

1372

8982450

    let mut values = Vec::new();

1373

8982450

    eval_comprehension_qualifiers(comprehension, 0, &mut values)?;

1374

44844

    Some(Lit::AbstractLiteral(

1375

44844

        AbstractLiteral::matrix_implied_indices(values),

1376

44844

))

1377

8982450

1378

1379

20485156

fn eval_comprehension_qualifiers(

1380

20485156

    comprehension: &Comprehension,

1381

20485156

    qualifier_index: usize,

1382

20485156

    values: &mut Vec<Lit>,

1383

20485156

) -> Option<()> {

1384

20485156

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

1385

7682208

        values.push(eval_constant(&comprehension.return_expression)?);

1386

158439

        return Some(());

1387

12802948

1388

1389

12802948

    match &comprehension.qualifiers[qualifier_index] {

1390

        ComprehensionQualifier::Generator { ptr } => {

1391

10853395

            let domain = ptr.domain()?;

1392

10853395

            let generator_values = domain

1393

10853395

                .resolve()

1394

10852959

                .and_then(|x| x.values())

1395

436

                .ok()?

1396

                .collect_vec();

1397

1398

10852959

            for value in generator_values {

1399

10999882

                with_temporary_quantified_binding(ptr, &value, || {

1400

10999882

                    eval_comprehension_qualifiers(comprehension, qualifier_index + 1, values)

1401

10999882

                })?;

1402

1403

1404

        ComprehensionQualifier::ExpressionGenerator { ptr } => {

1405

            // clone immediately so the read lock guard is dropped

1406

895496

            let expr = ptr.as_quantified_expr()?.clone();

1407

895496

            let generator_values = generator_values_from_expr(&expr)?;

1408

1409

209964

            for value in generator_values {

1410

272662

                with_temporary_quantified_binding(ptr, &value, || {

1411

272662

                    eval_comprehension_qualifiers(comprehension, qualifier_index + 1, values)

1412

272662

                })?;

1413

1414

1415

1054057

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

1416

            Lit::Bool(true) => {

1417

230162

                eval_comprehension_qualifiers(comprehension, qualifier_index + 1, values)?

1418

1419

96026

            Lit::Bool(false) => {}

1420

            _ => return None,

1421

},

1422

1423

1424

399426

    Some(())

1425

20485156

1426

1427

/// Values for a constant collection expression used during constant folding.

1428

///

1429

/// This does not enumerate decision-variable domains; quantification over decisions is not

1430

/// unrolled here.

1431

895496

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

1432

895496

    generator_values_from_constant_collection(&eval_constant(expr)?)

1433

895496

1434

1435

6667844

pub(crate) fn generator_values_from_constant_collection(lit: &Lit) -> Option<Vec<Lit>> {

1436

6667844

    match lit {

1437

        Lit::AbstractLiteral(AbstractLiteral::Set(values))

1438

        | Lit::AbstractLiteral(AbstractLiteral::MSet(values))

1439

911844

        | Lit::AbstractLiteral(AbstractLiteral::Tuple(values)) => Some(values.clone()),

1440

5756000

        Lit::AbstractLiteral(AbstractLiteral::Matrix(values, _)) => Some(values.clone()),

1441

        Lit::AbstractLiteral(list) => list.unwrap_list().cloned(),

1442

        _ => None,

1443

1444

6667844

1445

1446

11272544

fn with_temporary_quantified_binding<T>(

1447

11272544

    quantified: &crate::ast::DeclarationPtr,

1448

11272544

    value: &Lit,

1449

11272544

    f: impl FnOnce() -> Option<T>,

1450

11272544

) -> Option<T> {

1451

11272544

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

1452

11272544

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

1453

10999882

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

1454

1455

        targets.push(generator.clone());

1456

11272544

1457

1458

11272544

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

1459

11272544

    for mut target in targets {

1460

11272544

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

1461

11272544

            Metadata::new(),

1462

11272544

            Atom::Literal(value.clone()),

1463

11272544

        )));

1464

11272544

        originals.push((target, old_kind));

1465

1466

1467

11272544

    let result = f();

1468

1469

11272544

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

1470

11272544

        let _ = target.replace_kind(old_kind);

1471

1472

1473

11272544

    result

1474

11272544

1475

1476

#[cfg(test)]

1477

mod tests {

1478

    use super::*;

1479

    use crate::matrix_expr;

1480

1481

38

    fn int_lit(value: i32) -> Expr {

1482

38

        Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Int(value)))

1483

38

1484

1485

7

    fn bool_lit(value: bool) -> Expr {

1486

7

        Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Bool(value)))

1487

7

1488

1489

2

    fn variant_lit(alternative: &str, value: Expr) -> Expr {

1490

2

        Expr::AbstractLiteral(

1491

2

            Metadata::new(),

1492

2

            AbstractLiteral::Variant(Moo::new(Field {

1493

2

                name: crate::ast::Name::user(alternative),

1494

2

                value,

1495

2

            })),

1496

2

1497

2

1498

1499

16

    fn root(exprs: Vec<Expr>) -> Expr {

1500

16

        Expr::Root(Metadata::new(), exprs)

1501

16

1502

1503

    #[test]

1504

1

    fn evaluates_active_on_variant_literals() {

1505

1

        let variant = Moo::new(variant_lit("value", int_lit(2)));

1506

1

        let active = Expr::Active(

1507

1

            Metadata::new(),

1508

1

            variant.clone(),

1509

1

            crate::ast::Name::user("value"),

1510

1

);

1511

1

        let inactive = Expr::Active(Metadata::new(), variant, crate::ast::Name::user("flag"));

1512

1513

1

        assert_eq!(eval_constant(&active), Some(Lit::Bool(true)));

1514

1

        assert_eq!(eval_constant(&inactive), Some(Lit::Bool(false)));

1515

1

        assert!(run_partial_evaluator_local(&active).is_ok());

1516

1517

1

        let field = Expr::RecordField(

1518

1

            Metadata::new(),

1519

1

            Moo::new(variant_lit("value", int_lit(2))),

1520

1

            crate::ast::Name::user("value"),

1521

1

);

1522

1

        assert_eq!(eval_constant(&field), Some(Lit::Int(2)));

1523

1

1524

1525

    #[test]

1526

1

    fn local_root_partial_eval_strips_true_constraints() {

1527

1

        let expr = root(vec![bool_lit(true), int_lit(1)]);

1528

1

        let Expr::Root(_, exprs) = &expr else {

1529

            panic!("expected root");

1530

};

1531

1

        let normalised = normalise_root_constraints_local(exprs).unwrap();

1532

1

        assert_eq!(normalised, root(vec![int_lit(1)]));

1533

1

1534

1535

    #[test]

1536

1

    fn local_root_partial_eval_propagates_false() {

1537

1

        let expr = root(vec![bool_lit(false), int_lit(1)]);

1538

1

        let Expr::Root(_, exprs) = &expr else {

1539

            panic!("expected root");

1540

};

1541

1

        let normalised = normalise_root_constraints_local(exprs).unwrap();

1542

1

        assert_eq!(normalised, root(vec![bool_lit(false)]));

1543

1

1544

1545

    #[test]

1546

1

    fn deep_root_normalisation_folds_ground_constraint() {

1547

1

        let expr = root(vec![Expr::Sum(

1548

1

            Metadata::new(),

1549

1

            Moo::new(matrix_expr![int_lit(1), int_lit(2), int_lit(3)]),

1550

1

        )]);

1551

1

        let normalised = normalise_root_constraints_deep(&expr).unwrap();

1552

1

        assert_eq!(normalised, root(vec![int_lit(6)]));

1553

1

1554

1555

    #[test]

1556

1

    fn deep_root_normalisation_applies_partial_eval_steps() {

1557

1

        let expr = root(vec![Expr::Or(

1558

1

            Metadata::new(),

1559

1

            Moo::new(matrix_expr![bool_lit(false), int_lit(1)]),

1560

1

        )]);

1561

1

        let normalised = normalise_root_constraints_deep(&expr).unwrap();

1562

1

        assert_eq!(

1563

1

            normalised,

1564

1

            root(vec![Expr::Or(

1565

1

                Metadata::new(),

1566

1

                Moo::new(matrix_expr![int_lit(1)]),

1567

1

)])

1568

);

1569

1

1570

1571

    #[test]

1572

1

    fn selective_deep_root_normalisation_skips_solver_flat_constraints() {

1573

1

        let flat = Expr::FlatProductEq(

1574

1

            Metadata::new(),

1575

1

            Moo::new(Atom::Literal(Lit::Int(1))),

1576

1

            Moo::new(Atom::Literal(Lit::Int(2))),

1577

1

            Moo::new(Atom::Literal(Lit::Int(3))),

1578

1

);

1579

1

        let expr = root(vec![bool_lit(true), flat]);

1580

1

        assert!(normalise_root_constraints_deep(&expr).is_none());

1581

1

1582

1583

    #[test]

1584

1

    fn deep_root_normalisation_terminates_on_already_folded_constraint() {

1585

1

        let expr = root(vec![int_lit(5)]);

1586

1

        assert!(normalise_root_constraints_deep(&expr).is_none());

1587

1

1588

1589

    #[test]

1590

1

    fn local_evaluator_normalisation_terminates_on_already_folded_literal() {

1591

1

        let expr = int_lit(5);

1592

1

        assert!(normalise_evaluator_local(&expr).is_none());

1593

1

1594

1595

    #[test]

1596

1

    fn constant_set_cardinality_is_folded() {

1597

1

        let set = Expr::Atomic(

1598

1

            Metadata::new(),

1599

1

            Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Set(vec![

1600

1

                Lit::Int(1),

1601

1

                Lit::Int(2),

1602

1

            ]))),

1603

1

);

1604

1

        let cardinality = Expr::Card(Metadata::new(), Moo::new(set));

1605

1606

1

        assert_eq!(eval_constant(&cardinality), Some(Lit::Int(2)));

1607

1

1608

1609

    #[test]

1610

1

    fn constant_set_duplicates_are_normalised_before_cardinality() {

1611

1

        let literal = Lit::AbstractLiteral(AbstractLiteral::Set(vec![1.into(), 1.into()]));

1612

1

        let atomic = Expr::from(literal);

1613

1

        let expression = Expr::AbstractLiteral(

1614

1

            Metadata::new(),

1615

1

            AbstractLiteral::Set(vec![1.into(), 1.into()]),

1616

1

);

1617

1

        for set in [atomic, expression] {

1618

2

            let cardinality = Expr::Card(Metadata::new(), Moo::new(set));

1619

2

            assert_eq!(eval_constant(&cardinality), Some(Lit::Int(1)));

1620

1621

1

        let multiset = Expr::from(Lit::AbstractLiteral(AbstractLiteral::MSet(vec![

1622

1

            1.into(),

1623

1

            1.into(),

1624

1

        ])));

1625

1

        assert_eq!(

1626

1

            eval_constant(&Expr::Card(Metadata::new(), Moo::new(multiset))),

1627

1

            Some(Lit::Int(2))

1628

);

1629

1

1630

1631

    #[test]

1632

1

    fn constant_set_minimum_and_maximum_are_folded() {

1633

1

        let set = Expr::from(Lit::AbstractLiteral(AbstractLiteral::Set(vec![

1634

1

            Lit::Int(4),

1635

1

            Lit::Int(1),

1636

1

            Lit::Int(3),

1637

1

        ])));

1638

1639

1

        assert_eq!(

1640

1

            eval_constant(&Expr::Min(Metadata::new(), Moo::new(set.clone()))),

1641

1

            Some(Lit::Int(1))

1642

);

1643

1

        assert_eq!(

1644

1

            eval_constant(&Expr::Max(Metadata::new(), Moo::new(set))),

1645

1

            Some(Lit::Int(4))

1646

);

1647

1

1648

1649

    #[test]

1650

1

    fn constant_set_membership_supports_composite_values() {

1651

        let member =

1652

1

            Lit::AbstractLiteral(AbstractLiteral::Tuple(vec![Lit::Bool(true), Lit::Int(2)]));

1653

1

        let set = Lit::AbstractLiteral(AbstractLiteral::Set(vec![member.clone()]));

1654

1

        let membership = Expr::In(

1655

1

            Metadata::new(),

1656

1

            Moo::new(Expr::from(member)),

1657

1

            Moo::new(Expr::from(set)),

1658

1

);

1659

1660

1

        assert_eq!(eval_constant(&membership), Some(Lit::Bool(true)));

1661

1

1662

1663

    #[test]

1664

1

    fn constant_equality_supports_composite_values() {

1665

1

        let tuple = Lit::AbstractLiteral(AbstractLiteral::Tuple(vec![Lit::Int(1), Lit::Int(3)]));

1666

1

        let equal = Expr::Eq(

1667

1

            Metadata::new(),

1668

1

            Moo::new(Expr::from(tuple.clone())),

1669

1

            Moo::new(Expr::from(tuple)),

1670

1

);

1671

1

        let unequal = Expr::Neq(

1672

1

            Metadata::new(),

1673

1

            Moo::new(Expr::from(Lit::AbstractLiteral(AbstractLiteral::Tuple(

1674

1

                vec![Lit::Int(1), Lit::Int(3)],

1675

1

            )))),

1676

1

            Moo::new(Expr::from(Lit::AbstractLiteral(AbstractLiteral::Tuple(

1677

1

                vec![Lit::Int(1), Lit::Int(4)],

1678

1

            )))),

1679

1

);

1680

1681

1

        assert_eq!(eval_constant(&equal), Some(Lit::Bool(true)));

1682

1

        assert_eq!(eval_constant(&unequal), Some(Lit::Bool(true)));

1683

1684

1

        let set_equality = Expr::Eq(

1685

1

            Metadata::new(),

1686

1

            Moo::new(Expr::from(Lit::AbstractLiteral(AbstractLiteral::Set(

1687

1

                vec![Lit::Int(1), Lit::Int(2)],

1688

1

            )))),

1689

1

            Moo::new(Expr::from(Lit::AbstractLiteral(AbstractLiteral::Set(

1690

1

                vec![Lit::Int(2), Lit::Int(1)],

1691

1

            )))),

1692

1

);

1693

1

        assert_eq!(eval_constant(&set_equality), Some(Lit::Bool(true)));

1694

1

1695

1696

    #[test]

1697

1

    fn finish_root_normalisation_applies_local_root_rules() {

1698

1

        let expr = root(vec![bool_lit(true), int_lit(1)]);

1699

1

        let normalised = finish_root_evaluator_normalisation(&expr).unwrap();

1700

1

        assert_eq!(normalised, root(vec![int_lit(1)]));

1701

1

1702

1703

    #[test]

1704

1

    fn selective_deep_only_constraint_folds_target_index() {

1705

1

        let ground = Expr::Sum(

1706

1

            Metadata::new(),

1707

1

            Moo::new(matrix_expr![int_lit(1), int_lit(2), int_lit(3)]),

1708

1

);

1709

1

        let untouched = Expr::Sum(

1710

1

            Metadata::new(),

1711

1

            Moo::new(matrix_expr![int_lit(4), int_lit(5)]),

1712

1

);

1713

1

        let expr = root(vec![ground, untouched.clone()]);

1714

1

        let normalised = normalise_root_selective_deep_expr(&expr, Some(0)).unwrap();

1715

1

        assert_eq!(normalised, root(vec![int_lit(6), untouched]));

1716

1

1717

1718

    #[test]

1719

1

    fn finish_root_normalisation_flattens_top_level_and() {

1720

1

        let expr = root(vec![Expr::And(

1721

1

            Metadata::new(),

1722

1

            Moo::new(matrix_expr![bool_lit(true), int_lit(1), int_lit(2)]),

1723

1

        )]);

1724

1

        let normalised = finish_root_evaluator_normalisation(&expr).unwrap();

1725

1

        assert_eq!(normalised, root(vec![int_lit(1), int_lit(2)]));

1726

1

1727

1728

2

    fn permutation_lit(cycles: Vec<Vec<Expr>>) -> Expr {

1729

2

        Expr::AbstractLiteral(Metadata::new(), AbstractLiteral::Permutation(cycles))

1730

2

1731

1732

    #[test]

1733

1

    fn evaluates_image_on_a_permutation_literal_moved_point() {

1734

1

        let p = Moo::new(permutation_lit(vec![

1735

1

            vec![int_lit(1), int_lit(3), int_lit(5)],

1736

1

            vec![int_lit(2), int_lit(4)],

1737

1

        ]));

1738

1

        let image_1 = Expr::Image(Metadata::new(), p.clone(), Moo::new(int_lit(1)));

1739

1

        let image_3 = Expr::Image(Metadata::new(), p.clone(), Moo::new(int_lit(3)));

1740

1

        let image_5 = Expr::Image(Metadata::new(), p.clone(), Moo::new(int_lit(5)));

1741

1

        let image_2 = Expr::Image(Metadata::new(), p.clone(), Moo::new(int_lit(2)));

1742

1

        let image_4 = Expr::Image(Metadata::new(), p, Moo::new(int_lit(4)));

1743

1744

1

        assert_eq!(eval_constant(&image_1), Some(Lit::Int(3)));

1745

1

        assert_eq!(eval_constant(&image_3), Some(Lit::Int(5)));

1746

1

        assert_eq!(eval_constant(&image_5), Some(Lit::Int(1)));

1747

1

        assert_eq!(eval_constant(&image_2), Some(Lit::Int(4)));

1748

1

        assert_eq!(eval_constant(&image_4), Some(Lit::Int(2)));

1749

1

1750

1751

    #[test]

1752

1

    fn evaluates_image_on_a_permutation_literal_fixed_point() {

1753

1

        let p = Moo::new(permutation_lit(vec![vec![int_lit(1), int_lit(2)]]));

1754

1

        let image_3 = Expr::Image(Metadata::new(), p, Moo::new(int_lit(3)));

1755

1756

        // 3 is not mentioned in any cycle, so it is an implicit fixed point.

1757

1

        assert_eq!(eval_constant(&image_3), Some(Lit::Int(3)));

1758

1

1759