Grcov report - partial

1

use std::collections::HashSet;

2

3

use indexmap::IndexMap;

4

5

use crate::ast::Typeable;

6

use crate::{

7

    ast::{

8

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

9

        Metadata, Moo, Range, ReturnType,

10

},

11

    into_matrix_expr,

12

    rule_engine::{ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect},

13

};

14

15

/// Constant comparison shape used when dominating bounds under `And`.

16

///

17

/// Only same-operator bounds on the same atomic LHS are merged. Integer strictness is left alone

18

/// (`x > k` is not rewritten to `x >= k+1`) so later solver-family normalisers stay in control.

19

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]

20

enum ConstantBoundOp {

21

    /// Keep the largest RHS: `x > a /\ x > b` ~> `x > max(a, b)`.

22

Gt,

23

    /// Keep the largest RHS: `x >= a /\ x >= b` ~> `x >= max(a, b)`.

24

    Geq,

25

    /// Keep the smallest RHS: `x < a /\ x < b` ~> `x < min(a, b)`.

26

Lt,

27

    /// Keep the smallest RHS: `x <= a /\ x <= b` ~> `x <= min(a, b)`.

28

    Leq,

29

30

31

impl ConstantBoundOp {

32

    /// Whether a larger RHS is the stronger bound for this operator.

33

97385

    fn prefers_larger_rhs(self) -> bool {

34

97385

        matches!(self, ConstantBoundOp::Gt | ConstantBoundOp::Geq)

35

97385

36

37

38

/// Normalises integer ranges so equivalent domains compare structurally equal.

39

6

fn normalise_int_domain(domain: &GroundDomain) -> GroundDomain {

40

6

    match domain {

41

        GroundDomain::Int(ranges, representation) => GroundDomain::Int(

42

5

            Range::squeeze(

43

5

                &ranges

44

5

                    .iter()

45

5

                    .map(|range| Range::new(range.low().copied(), range.high().copied()))

46

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

47

),

48

5

            representation.clone(),

49

),

50

1

        _ => domain.clone(),

51

52

6

53

54

/// Returns whether `expr` is safe after resolving any referenced expressions.

55

77458087

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

56

111450515

    fn helper(expr: &Expr, resolving: &mut HashSet<crate::ast::serde::ObjId>) -> bool {

57

111450515

        if matches!(

58

111450515

            expr,

59

            Expr::UnsafeDiv(_, _, _)

60

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

61

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

62

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

63

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

64

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

65

                | Expr::Pred(_, _)

66

                | Expr::Succ(_, _)

67

) {

68

10402983

            return false;

69

101047532

70

71

        // Applying a partial function is undefined outside the positions it defines, so it has to

72

        // keep its undefinedness until a bubble discharges it.

73

101047532

        if let Expr::Image(_, subject, argument) = expr

74

660214

            && crate::ast::expressions::image_can_be_undefined(subject, argument)

75

76

589570

            return false;

77

100457962

78

79

100457962

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

80

60261754

            let id = reference.id();

81

60261754

            if !resolving.insert(id.clone()) {

82

                return false;

83

60261754

84

60261754

            let is_safe = reference

85

8

                .with_resolved_expression(|resolved| helper(resolved, resolving))

86

60261754

                .unwrap_or(true);

87

60261754

            resolving.remove(&id);

88

60261754

            return is_safe;

89

40196208

90

91

40196208

        let mut is_safe = true;

92

40197148

        expr.for_each_expr_child(&mut |child| {

93

35236176

            if is_safe {

94

33992420

                is_safe = helper(child, resolving);

95

1243756

96

35236176

});

97

40196208

        is_safe

98

111450515

99

100

77458087

    helper(expr, &mut HashSet::new())

101

77458087

102

103

/// Tries to decide `expr in domain` from resolved domains alone.

104

3

fn simplify_in_domain(expr: &Expr, domain: &DomainPtr) -> Option<bool> {

105

3

    if !is_semantically_safe(expr) {

106

        return None;

107

3

108

109

3

    let expr_domain = resolved_ground_domain_of_for_partial_eval(expr)?;

110

3

    let domain = domain.resolve().ok()?;

111

3

    let intersection = expr_domain.intersect(&domain).ok()?;

112

113

3

    if normalise_int_domain(&intersection) == normalise_int_domain(expr_domain.as_ref()) {

114

1

        return Some(true);

115

2

116

117

2

    if intersection.return_type() == ReturnType::Int && intersection.length().ok() == Some(0) {

118

1

        return Some(false);

119

1

120

121

1

    None

122

3

123

124

/// Extracts an integer when `expr` is known to be a singleton integer value.

125

44897570

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

126

44897570

    if let Ok(value) = expr.try_into() {

127

41586939

        return Some(value);

128

3310631

129

130

3310631

    let domain = resolved_ground_domain_of_for_partial_eval(expr)?;

131

3271771

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

132

65221

        return None;

133

};

134

3206550

    let [range] = ranges.as_slice() else {

135

435

        return None;

136

};

137

3206115

    let (Some(low), Some(high)) = (range.low(), range.high()) else {

138

        return None;

139

};

140

141

3206115

    if low == high { Some(*low) } else { None }

142

44897570

143

144

/// Extracts a singleton integer without deriving the domain of a compound expression.

145

///

146

/// Local partial evaluation runs on every dirty ancestor. Calling `domain_of` for arithmetic

147

/// expressions here can enumerate the Cartesian product of both operand domains, turning a cheap

148

/// node-local check into the dominant translation cost. Literal and declaration-domain lookup are

149

/// the constant-size cases needed to fold operations such as `x ** 2` for `x : int(2..2)`.

150

218827

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

151

218827

    match expr {

152

877

        Expr::Atomic(_, Atom::Literal(Lit::Int(value))) => Some(*value),

153

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

154

14921

            let domain = reference.domain()?.resolve().ok()?;

155

14921

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

156

                return None;

157

};

158

14921

            let [range] = ranges.as_slice() else {

159

                return None;

160

};

161

14921

            let (Some(low), Some(high)) = (range.low(), range.high()) else {

162

                return None;

163

};

164

14921

            (low == high).then_some(*low)

165

166

203029

        _ => None,

167

168

218827

169

170

149219

fn matrix_index_offset(index_domain: &DomainPtr, index: i32) -> Option<usize> {

171

149219

    integer_index_offset(index_domain.as_int_ground()?, index)

172

149219

173

174

21228

fn ground_matrix_index_offset(index_domain: &GroundDomain, index: i32) -> Option<usize> {

175

21228

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

176

        return None;

177

};

178

21228

    integer_index_offset(ranges, index)

179

21228

180

181

/// Locate a label by its domain position, including gaps, without enumerating ranges.

182

170447

fn integer_index_offset(ranges: &[Range<i32>], index: i32) -> Option<usize> {

183

170447

    let mut offset = 0usize;

184

170447

    for range in ranges {

185

191675

        let lower = i64::from(*range.low()?);

186

191675

        let index = i64::from(index);

187

191675

        let upper = range.high().map(|value| i64::from(*value));

188

191675

        if index >= lower && upper.is_none_or(|upper| index <= upper) {

189

149219

            return offset.checked_add(usize::try_from(index - lower).ok()?);

190

42456

191

42456

        let length = (upper? - lower + 1).max(0);

192

42456

        offset = offset.checked_add(usize::try_from(length).ok()?)?;

193

194

21228

    None

195

170447

196

197

/// Selects one element from a matrix literal, including a referenced constant matrix.

198

///

199

/// This deliberately clones only the selected element. Resolving the complete matrix into an

200

/// owned `Vec` for every index makes N selections from an N-element matrix quadratic.

201

41601700

fn resolve_matrix_element(subject: &Expr, index: i32) -> Option<Expr> {

202

41601700

    match subject {

203

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

204

            resolve_matrix_element(inner, index)

205

206

149219

        Expr::AbstractLiteral(_, AbstractLiteral::Matrix(elems, index_domain)) => elems

207

149219

            .get(matrix_index_offset(index_domain, index)?)

208

            .cloned(),

209

        Expr::Atomic(

210

_,

211

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

212

10730

        ) => elems

213

10730

            .get(ground_matrix_index_offset(index_domain, index)?)

214

            .cloned()

215

            .map(|literal| Expr::Atomic(Metadata::new(), Atom::Literal(literal))),

216

40181179

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

217

10498

            .with_resolved_expression(|resolved| resolve_matrix_element(resolved, index))

218

            .flatten()

219

40181179

            .or_else(|| {

220

                // Computed constant lettings are uncommon, but retain support for them. This

221

                // fallback may materialise the value; direct matrix lettings above do not.

222

                let Lit::AbstractLiteral(AbstractLiteral::Matrix(elems, index_domain)) =

223

40181179

                    reference.resolve_constant()?

224

                else {

225

                    return None;

226

};

227

10498

                elems

228

10498

                    .get(ground_matrix_index_offset(&index_domain, index)?)

229

                    .cloned()

230

                    .map(|literal| Expr::Atomic(Metadata::new(), Atom::Literal(literal)))

231

40181179

}),

232

1260572

        _ => None,

233

234

41601700

235

236

/// Resolves domains for partial evaluation while avoiding malformed indexing panics.

237

31402474

fn resolved_ground_domain_of_for_partial_eval(expr: &Expr) -> Option<Moo<GroundDomain>> {

238

31402474

    match expr {

239

        Expr::SafeIndex(_, subject, _) => {

240

486533

            let subject_domain = resolved_ground_domain_of_for_partial_eval(subject)?;

241

486533

            let GroundDomain::Matrix(elem_domain, _, _) = subject_domain.as_ref() else {

242

29522

                return None;

243

};

244

245

457011

            Some(elem_domain.clone())

246

247

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

248

            let subject_domain = resolved_ground_domain_of_for_partial_eval(subject)?;

249

            let GroundDomain::Matrix(elem_domain, index_domains, _) = subject_domain.as_ref()

250

            else {

251

                return None;

252

};

253

            let sliced_dimension = indices.iter().position(Option::is_none);

254

255

            match sliced_dimension {

256

                Some(dimension) => Some(Moo::new(GroundDomain::Matrix(

257

                    elem_domain.clone(),

258

                    vec![index_domains[dimension].clone()],

259

                    None,

260

                ))),

261

                None => Some(elem_domain.clone()),

262

263

264

19546

        Expr::UnsafeIndex(_, _, _) | Expr::UnsafeSlice(_, _, _) => None,

265

30896395

        _ => expr.domain_of()?.resolve().ok(),

266

267

31402474

268

269

/// Whether `expr` is an undefined value whose domain is empty.

270

///

271

/// `min`/`max` of an empty collection carries an empty domain despite being unsafe.

272

/// Enum neighbours also carry useful partial domains and are handled separately below.

273

38237564

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

274

38237564

    matches!(expr, Expr::Min(_, values) | Expr::Max(_, values) if is_empty_matrix_operand(values))

275

38237564

276

277

/// Whether an unsafe expression's domain still describes all values it can take.

278

/// An empty domain rules out both equality and disequality under relational semantics.

279

4913195

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

280

4913195

    matches!(

281

4913195

        expr,

282

        Expr::Image(_, _, _) | Expr::Pred(_, _) | Expr::Succ(_, _)

283

284

4913195

285

286

/// Tries to decide `expr = lit` and `expr != lit` from the resolved domain of `expr`.

287

///

288

/// Each direction is decided separately, because an expression that can be undefined does not

289

/// settle both at once: where it is undefined, relational semantics make the containing boolean

290

/// false, which agrees with a `false` equality but contradicts a `true` disequality.

291

32223717

fn simplify_comparison_with_literal(

292

32223717

    expr: &Expr,

293

32223717

    lit: &Lit,

294

32223717

) -> Option<(Option<bool>, Option<bool>)> {

295

    // Deriving the domain of a compound expression enumerates its value set, and combining

296

    // operands takes the Cartesian product of those sets -- packed set representations reach tens

297

    // of thousands of values. An unsafe expression can still be decided below -- an empty

298

    // `min`/`max`, or a literal its domain cannot hold -- but nothing else can, so a safe

299

    // expression is worth the lookup unconditionally and an unsafe one only for those shapes.

300

32223717

    let is_safe = is_semantically_safe(expr);

301

32223717

    if !is_safe && !is_empty_min_max(expr) && !can_derive_unsafe_domain(expr) {

302

4618410

        return None;

303

27605307

304

305

27605307

    let expr_domain = resolved_ground_domain_of_for_partial_eval(expr)?;

306

307

    // An empty domain represents an undefined value. Under relational semantics the closest

308

    // containing Boolean expression is false, for both equality and disequality.

309

27391319

    if matches!(expr_domain.as_ref(), GroundDomain::Empty(_)) {

310

12760

        return Some((Some(false), Some(false)));

311

27378559

312

313

27378559

    if !expr_domain.contains(lit).ok()? {

314

        // A representation rewrite can temporarily leave one side in its source shape and the

315

        // other in its represented shape (for example, `record = tuple`). The source domain does

316

        // not contain represented literals, but that does not make the original comparison false.

317

117251

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

318

56264

            && !reference.ptr().reprs().is_empty()

319

320

26941

            return None;

321

90310

322

        // No value the expression can take equals the literal, and where it is undefined the

323

        // equality is false as well -- so the equality is false either way. The disequality is

324

        // only true where the expression is defined, so it needs safety.

325

90310

        return Some((Some(false), is_safe.then_some(true)));

326

27261308

327

328

27261308

    if !is_safe {

329

294785

        return None;

330

26966523

331

332

26966523

    match (expr_domain.as_ref(), lit) {

333

724548

        (GroundDomain::Bool, Lit::Bool(_)) => None,

334

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

335

21570197

            let [range] = ranges.as_slice() else {

336

643874

                return None;

337

};

338

20926323

            let (Some(low), Some(high)) = (range.low(), range.high()) else {

339

56

                return None;

340

};

341

342

20926267

            if low == high && low == value {

343

112694

                Some((Some(true), Some(false)))

344

            } else {

345

20813573

                None

346

347

348

4671778

        _ => None,

349

350

32223717

351

352

/// Whether deciding a comparison against `expr` is worth a domain lookup in this mode.

353

///

354

/// The local evaluator runs on every dirty ancestor after every rewrite, so it only derives a

355

/// domain when that is a constant-size lookup: a declaration's own domain, or the empty domain of

356

/// an empty `min`/`max`. Deep evaluation runs once per expansion and can afford the general case.

357

65535326

fn comparison_domain_lookup_is_cheap(expr: &Expr, mode: PartialEvalMode) -> bool {

358

65535326

    mode == PartialEvalMode::Deep

359

45225329

        || matches!(expr, Expr::Atomic(_, Atom::Reference(_)))

360

33324369

        || is_empty_min_max(expr)

361

65535326

362

363

/// Tries to decide reflexive equality and inequality when both sides are semantically safe.

364

25401649

fn simplify_reflexive_comparison(x: &Expr, y: &Expr) -> Option<(bool, bool)> {

365

25401649

    if x.identical_atom_to(y) && is_semantically_safe(x) && is_semantically_safe(y) {

366

43152

        return Some((true, false));

367

25358497

368

369

25358497

    if is_semantically_safe(x) && is_semantically_safe(y) && x == y {

370

2900

        return Some((true, false));

371

25355597

372

373

25355597

    None

374

25401649

375

376

86871529

fn simplify_reflexive_comparison_with_mode(

377

86871529

    x: &Expr,

378

86871529

    y: &Expr,

379

86871529

    mode: PartialEvalMode,

380

86871529

) -> Option<(bool, bool)> {

381

86871529

    match mode {

382

25401649

        PartialEvalMode::Deep => simplify_reflexive_comparison(x, y),

383

61469880

        PartialEvalMode::Local => x.identical_atom_to(y).then_some((true, false)),

384

385

86871529

386

387

211347919

pub fn run_partial_evaluator(expr: &Expr) -> ApplicationResult {

388

211347919

    run_partial_evaluator_with_mode(expr, PartialEvalMode::Deep)

389

211347919

390

391

/// Partially evaluates `expr` using only information already available at the focused node.

392

///

393

/// This is intended for the main rewriter, where recursive simplification is supplied by the

394

/// scheduler. Use [`run_partial_evaluator`] when a caller explicitly wants semantic checks that

395

/// can inspect referenced expressions.

396

1638996862

pub fn run_partial_evaluator_local(expr: &Expr) -> ApplicationResult {

397

1638996862

    run_partial_evaluator_with_mode(expr, PartialEvalMode::Local)

398

1638996862

399

400

#[derive(Clone, Copy, Debug, PartialEq, Eq)]

401

enum PartialEvalMode {

402

    Deep,

403

    Local,

404

405

406

/// Rewrites `x = true` / `true = x` to `x` when `x` is a non-literal boolean atom.

407

///

408

/// Nested uses such as `(x = true) <-> and([y = true, ...])` otherwise force Minion flattening to

409

/// introduce aux variables for the left-hand `Eq`, because both sides of the outer equality are

410

/// non-atomic. Lowering the tautological `= true` first keeps a boolean decision variable atomic

411

/// so later equality/reify rules can target it directly.

412

///

413

/// Literal–literal equalities are left alone for constant folding. Non-boolean atoms are refused.

414

94277517

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

415

94277517

    let Expr::Eq(_, left, right) = expr else {

416

11918

        return None;

417

};

418

419

94265599

    let atom = match (left.as_ref(), right.as_ref()) {

420

        (Expr::Atomic(_, Atom::Literal(Lit::Bool(true))), Expr::Atomic(_, atom))

421

29

            if !matches!(atom, Atom::Literal(_)) =>

422

423

29

            right.as_ref()

424

425

        (Expr::Atomic(_, atom), Expr::Atomic(_, Atom::Literal(Lit::Bool(true))))

426

62382

            if !matches!(atom, Atom::Literal(_)) =>

427

428

62382

            left.as_ref()

429

430

94203188

        _ => return None,

431

};

432

433

62411

    if atom.return_type() != ReturnType::Bool {

434

29

        return None;

435

62382

436

437

62382

    Some(atom.clone())

438

94277517

439

440

1850344781

fn run_partial_evaluator_with_mode(expr: &Expr, mode: PartialEvalMode) -> ApplicationResult {

441

    // NOTE: If nothing changes, we must return RuleNotApplicable, or the rewriter will try this

442

    // rule infinitely!

443

    // This is why we always check whether we found a constant or not.

444

1850344781

    match expr {

445

533

        Expr::Difference(_, _, _) => Err(RuleNotApplicable),

446

2958

        Expr::Union(_, _, _) => Err(RuleNotApplicable),

447

4534373

        Expr::In(_, _, _) => Err(RuleNotApplicable),

448

8236

        Expr::Intersect(_, _, _) => Err(RuleNotApplicable),

449

        Expr::Supset(_, _, _) => Err(RuleNotApplicable),

450

        Expr::SupsetEq(_, _, _) => Err(RuleNotApplicable),

451

96454

        Expr::Subset(_, _, _) => Err(RuleNotApplicable),

452

157450

        Expr::SubsetEq(_, _, _) => Err(RuleNotApplicable),

453

258799417

        Expr::AbstractLiteral(_, _) => Err(RuleNotApplicable),

454

826181

        Expr::CatchUndef(_, _, _) => Err(RuleNotApplicable),

455

4901768

        Expr::Comprehension(_, _) => Err(RuleNotApplicable),

456

        Expr::DominanceRelation(_, _) => Err(RuleNotApplicable),

457

8563

        Expr::TypeAnnotation(_, _, _) => Err(RuleNotApplicable),

458

6276

        Expr::DomainAnnotation(_, _, _) => Err(RuleNotApplicable),

459

        Expr::FromSolution(_, _) => Err(RuleNotApplicable),

460

        Expr::Metavar(_, _) => Err(RuleNotApplicable),

461

11888235

        Expr::UnsafeIndex(_, _, _) => Err(RuleNotApplicable),

462

1135055

        Expr::UnsafeSlice(_, _, _) => Err(RuleNotApplicable),

463

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

464

1652855

            Err(RuleNotApplicable)

465

466

620832

        Expr::NegativeTable(_, _, _) | Expr::ShortTable(_, _, _) => Err(RuleNotApplicable),

467

872088

        Expr::AtLeast(_, _, _, _) => Err(RuleNotApplicable),

468

321610

        Expr::AtMost(_, _, _, _) => Err(RuleNotApplicable),

469

5771

        Expr::Gcc(_, _, _, _) | Expr::GccWeak(_, _, _, _) => Err(RuleNotApplicable),

470

431317

        Expr::RecordField(_, _, _) => Err(RuleNotApplicable),

471

        Expr::AttributeAsConstraint(_, _, _, _) => Err(RuleNotApplicable),

472

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

473

            // partially evaluate matrix literals indexed by a constant.

474

44897570

            if indices.is_empty() {

475

                return Err(RuleNotApplicable);

476

44897570

477

478

            // the leading index must be fixed to a single value

479

44897570

            let index = singleton_int_value(&indices[0]).ok_or(RuleNotApplicable)?;

480

481

41591202

            let selected = resolve_matrix_element(subject, index).ok_or(RuleNotApplicable)?;

482

149219

            if indices.len() == 1 {

483

149219

                Ok(RuleEffect::pure(selected))

484

            } else {

485

                Ok(RuleEffect::pure(Expr::SafeIndex(

486

                    Metadata::new(),

487

                    Moo::new(selected),

488

                    indices[1..].to_vec(),

489

)))

490

491

492

450974

        Expr::SafeSlice(_, _, _) => Err(RuleNotApplicable),

493

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

494

100491

            if mode == PartialEvalMode::Deep

495

3

                && let Some(result) = simplify_in_domain(x, domain)

496

497

2

                Ok(RuleEffect::pure(Expr::Atomic(

498

2

                    Metadata::new(),

499

2

                    result.into(),

500

2

)))

501

100489

            } else if let Expr::Atomic(_, Atom::Reference(decl)) = x.as_ref() {

502

28250

                let decl_domain = decl

503

28250

                    .domain()

504

28250

                    .ok_or(RuleNotApplicable)?

505

                    .resolve()

506

                    .map_err(|_| RuleNotApplicable)?;

507

28250

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

508

509

28250

                let intersection = decl_domain

510

28250

                    .intersect(&domain)

511

                    .map_err(|_| RuleNotApplicable)?;

512

513

                // if the declaration's domain is a subset of domain, expr is always true.

514

28250

                if &intersection == decl_domain.as_ref() {

515

1

                    Ok(RuleEffect::pure(Expr::Atomic(Metadata::new(), true.into())))

516

517

                // if no elements of declaration's domain are in the domain (i.e. they have no

518

                // intersection), expr is always false.

519

//

520

                // Only check this when the intersection is a finite integer domain, as we

521

                // currently don't have a way to check whether other domain kinds are empty or not.

522

//

523

                // we should expand this to cover more domain types in the future.

524

28249

                else if intersection.return_type() == ReturnType::Int

525

28249

                    && intersection.length().ok() == Some(0)

526

527

1

                    Ok(RuleEffect::pure(Expr::Atomic(

528

1

                        Metadata::new(),

529

1

                        false.into(),

530

1

)))

531

                } else {

532

28248

                    Err(RuleNotApplicable)

533

534

72239

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

535

                if domain

536

                    .resolve()

537

                    .and_then(|gd| gd.contains(lit))

538

                    .map_err(|_| RuleNotApplicable)?

539

540

                    Ok(RuleEffect::pure(Expr::Atomic(Metadata::new(), true.into())))

541

                } else {

542

                    Ok(RuleEffect::pure(Expr::Atomic(

543

                        Metadata::new(),

544

                        false.into(),

545

)))

546

547

            } else {

548

72239

                Err(RuleNotApplicable)

549

550

551

        Expr::Bubble(_, expr, cond) => {

552

            // definition of bubble is "expr is valid as long as cond is true"

553

//

554

            // check if cond is true and pop the bubble!

555

2531507

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

556

1549067

                Ok(RuleEffect::pure(Moo::unwrap_or_clone(expr.clone())))

557

            } else {

558

982440

                Err(RuleNotApplicable)

559

560

561

798207473

        Expr::Atomic(_, _) => Err(RuleNotApplicable),

562

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

563

68344524

            if expression.return_type() == ReturnType::Int {

564

                Ok(RuleEffect::pure(Moo::unwrap_or_clone(expression.clone())))

565

            } else {

566

68344524

                Err(RuleNotApplicable)

567

568

569

355424

        Expr::Abs(m, e) => match e.as_ref() {

570

4234

            Expr::Neg(_, inner) => Ok(RuleEffect::pure(Expr::Abs(m.clone(), inner.clone()))),

571

351190

            _ => Err(RuleNotApplicable),

572

},

573

        Expr::Sum(m, vec) => {

574

29761330

            let vec = vec.unwrap_list_cow().ok_or(RuleNotApplicable)?;

575

24916690

            let mut acc = 0;

576

24916690

            let mut n_consts = 0;

577

24916690

            for expr in vec.iter() {

578

119723957

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

579

3031095

                    acc += *x;

580

3031095

                    n_consts += 1;

581

116692862

582

583

584

24916690

            if n_consts <= 1 {

585

24887512

                return Err(RuleNotApplicable);

586

29178

587

588

29178

            let mut new_vec: Vec<Expr> = vec

589

29178

                .iter()

590

121696

                .filter(|expr| !matches!(expr, Expr::Atomic(_, Atom::Literal(Lit::Int(_)))))

591

                .cloned()

592

                .collect();

593

29178

            if acc != 0 {

594

21286

                new_vec.push(Expr::Atomic(

595

21286

                    Default::default(),

596

21286

                    Atom::Literal(Lit::Int(acc)),

597

21286

));

598

7892

599

600

29178

            Ok(RuleEffect::pure(Expr::Sum(

601

29178

                m.clone(),

602

29178

                Moo::new(into_matrix_expr![new_vec]),

603

29178

)))

604

605

606

        Expr::Product(m, vec) => {

607

7651475

            let mut acc = 1;

608

7651475

            let mut n_consts = 0;

609

7651475

            let vec = vec.unwrap_list_cow().ok_or(RuleNotApplicable)?;

610

7651446

            for expr in vec.iter() {

611

15312186

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

612

5283600

                    acc *= *x;

613

5283600

                    n_consts += 1;

614

10028586

615

616

617

7651446

            if n_consts == 0 {

618

2368426

                return Err(RuleNotApplicable);

619

5283020

620

621

5283020

            if acc == 0 && mode == PartialEvalMode::Local {

622

2

                return Err(RuleNotApplicable);

623

5283018

624

625

5283018

            if acc != 0 && n_consts == 1 {

626

5282408

                return Err(RuleNotApplicable);

627

610

628

629

610

            let mut new_vec: Vec<Expr> = vec

630

610

                .iter()

631

1800

                .filter(|expr| !matches!(expr, Expr::Atomic(_, Atom::Literal(Lit::Int(_)))))

632

                .cloned()

633

                .collect();

634

635

610

            new_vec.push(Expr::Atomic(

636

610

                Default::default(),

637

610

                Atom::Literal(Lit::Int(acc)),

638

610

));

639

610

            let new_product = Expr::Product(m.clone(), Moo::new(into_matrix_expr![new_vec]));

640

641

610

            if acc == 0 {

642

                // If safe, 0 * exprs ~> 0. Otherwise do not reshuffle: appending the folded

643

                // zero fights `reorder_product` (constant-first) and loops forever under the

644

                // local evaluator. Constant folding/placement is left to `reorder_product`.

645

117

                if mode == PartialEvalMode::Deep && is_semantically_safe(&new_product) {

646

117

                    Ok(RuleEffect::pure(Expr::Atomic(

647

117

                        Default::default(),

648

117

                        Atom::Literal(Lit::Int(0)),

649

117

)))

650

                } else {

651

                    Err(RuleNotApplicable)

652

653

            } else {

654

                // acc !=0, multiple constants found

655

493

                Ok(RuleEffect::pure(new_product))

656

657

658

659

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

660

246239

            let Some(vec) = e.unwrap_list_cow() else {

661

242092

                return Err(RuleNotApplicable);

662

};

663

4147

            let mut acc: Option<i32> = None;

664

4147

            let mut n_consts = 0;

665

4147

            for expr in vec.iter() {

666

2001

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

667

87

                    n_consts += 1;

668

87

                    acc = match acc {

669

                        Some(i) => {

670

                            if i > *x {

671

                                Some(*x)

672

                            } else {

673

                                Some(i)

674

675

676

87

                        None => Some(*x),

677

};

678

1914

679

680

681

4147

            if n_consts <= 1 {

682

4147

                return Err(RuleNotApplicable);

683

684

685

            let mut new_vec: Vec<Expr> = vec

686

                .iter()

687

                .filter(|expr| !matches!(expr, Expr::Atomic(_, Atom::Literal(Lit::Int(_)))))

688

                .cloned()

689

                .collect();

690

            if let Some(i) = acc {

691

                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));

692

693

694

            Ok(RuleEffect::pure(Expr::Min(

695

                m.clone(),

696

                Moo::new(into_matrix_expr![new_vec]),

697

)))

698

699

700

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

701

208684

            let Some(vec) = e.unwrap_list_cow() else {

702

206886

                return Err(RuleNotApplicable);

703

};

704

705

1798

            let mut acc: Option<i32> = None;

706

1798

            let mut n_consts = 0;

707

1798

            for expr in vec.iter() {

708

1653

                if let Expr::Atomic(_, Atom::Literal(Lit::Int(x))) = expr {

709

87

                    n_consts += 1;

710

87

                    acc = match acc {

711

                        Some(i) => {

712

                            if i < *x {

713

                                Some(*x)

714

                            } else {

715

                                Some(i)

716

717

718

87

                        None => Some(*x),

719

};

720

1566

721

722

723

1798

            if n_consts <= 1 {

724

1798

                return Err(RuleNotApplicable);

725

726

727

            let mut new_vec: Vec<Expr> = vec

728

                .iter()

729

                .filter(|expr| !matches!(expr, Expr::Atomic(_, Atom::Literal(Lit::Int(_)))))

730

                .cloned()

731

                .collect();

732

            if let Some(i) = acc {

733

                new_vec.push(Expr::Atomic(Default::default(), Atom::Literal(Lit::Int(i))));

734

735

736

            Ok(RuleEffect::pure(Expr::Max(

737

                m.clone(),

738

                Moo::new(into_matrix_expr![new_vec]),

739

)))

740

741

        Expr::Not(_, e1) => {

742

69047919

            let Expr::Imply(_, p, q) = e1.as_ref() else {

743

69047571

                return Err(RuleNotApplicable);

744

};

745

746

348

            if mode == PartialEvalMode::Deep && !is_semantically_safe(e1) {

747

                return Err(RuleNotApplicable);

748

348

749

750

348

            match (p.as_ref(), q.as_ref()) {

751

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

752

                    Ok(RuleEffect::pure(Expr::from(false)))

753

754

                (_, Expr::Atomic(_, Atom::Literal(Lit::Bool(false)))) => {

755

                    Ok(RuleEffect::pure(Moo::unwrap_or_clone(p.clone())))

756

757

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

758

                    Ok(RuleEffect::pure(Expr::Not(Metadata::new(), q.clone())))

759

760

                (Expr::Atomic(_, Atom::Literal(Lit::Bool(false))), _) => {

761

                    Ok(RuleEffect::pure(Expr::from(false)))

762

763

348

                _ => Err(RuleNotApplicable),

764

765

766

        Expr::Or(m, e) => {

767

            // Empty disjunction is the Or-identity, whatever index domain the matrix carries.

768

213975170

            if is_empty_matrix_operand(e) {

769

5193

                return Ok(RuleEffect::pure(Expr::from(false)));

770

213969977

771

772

213969977

            let Some(terms) = e.unwrap_list_cow() else {

773

757052

                return Err(RuleNotApplicable);

774

};

775

776

213212925

            let mut has_changed = false;

777

213212925

            let mut non_literal_terms = 0;

778

779

            // Inspection pass: decide applicability from borrowed terms, so a disjunction that

780

            // does not fold costs a walk rather than a copy.

781

213212925

            for expr in terms.iter() {

782

505162603

                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {

783

2643874

                    has_changed = true;

784

785

                    // true ~~> entire or is true

786

                    // false ~~> remove false from the or

787

2643874

                    if *x {

788

1289512

                        return Ok(RuleEffect::pure(true.into()));

789

1354362

790

                } else {

791

502518729

                    non_literal_terms += 1;

792

793

794

795

            // The two supported implication tautologies, in expected O(n).

796

211923413

            if check_pairwise_or_tautologies(&terms) {

797

4292

                return Ok(RuleEffect::pure(true.into()));

798

211919121

799

800

            // 3. empty or ~~> false

801

211919121

            if non_literal_terms == 0 {

802

                return Ok(RuleEffect::pure(false.into()));

803

211919121

804

805

211919121

            if !has_changed {

806

211398944

                return Err(RuleNotApplicable);

807

520177

808

809

520177

            let new_terms = terms

810

520177

                .iter()

811

1892664

                .filter(|expr| !matches!(expr, Expr::Atomic(_, Atom::Literal(Lit::Bool(_)))))

812

                .cloned()

813

                .collect::<Vec<_>>();

814

815

520177

            Ok(RuleEffect::pure(Expr::Or(

816

520177

                m.clone(),

817

520177

                Moo::new(into_matrix_expr![new_terms]),

818

520177

)))

819

820

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

821

            // The evaluator revisits a conjunction after each rewrite elsewhere in the model, so

822

            // establish applicability from borrowed conjuncts and only build a replacement once

823

            // the rule is known to apply. A wide `and` -- what unrolling `forAll i : D. ...`

824

            // produces -- is then walked per visit rather than copied, keeping repeated visits

825

            // linear rather than quadratic in the number of conjuncts.

826

            // Empty conjunction is the And-identity, whatever index domain the matrix carries.

827

67165636

            if is_empty_matrix_operand(e) {

828

2

                return Ok(RuleEffect::pure(Expr::from(true)));

829

67165634

830

831

67165634

            let Some(vec) = e.unwrap_list_cow() else {

832

6269350

                return Err(RuleNotApplicable);

833

};

834

835

60896284

            let mut has_changed: bool = false;

836

            // `Atom` is only interior-mutable through `DeclarationPtr`, whose `Hash`/`Eq` use the

837

            // immutable declaration id, so it is stable as a key.

838

            #[allow(clippy::mutable_key_type)]

839

60896284

            let mut distinct_bounds: HashSet<(&Atom, ConstantBoundOp)> = HashSet::new();

840

60896284

            let mut constant_bound_terms: usize = 0;

841

60896284

            for expr in vec.iter() {

842

847668008

                if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = expr {

843

3446237

                    if !x {

844

1235796

                        return Ok(RuleEffect::pure(Expr::Atomic(

845

1235796

                            Default::default(),

846

1235796

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

847

1235796

                        )));

848

2210441

849

2210441

                    has_changed = true;

850

844221771

                } else if let Some((lhs, op, _)) = as_constant_bound_comparison_ref(expr) {

851

530749

                    constant_bound_terms += 1;

852

530749

                    distinct_bounds.insert((lhs, op));

853

843691022

854

855

856

            // Only treat bound aggregation as a change when at least one conjunct was dominated.

857

59660488

            if constant_bound_terms > distinct_bounds.len() {

858

4236

                has_changed = true;

859

59656252

860

861

59660488

            if !has_changed {

862

57451909

                return Err(RuleNotApplicable);

863

2208579

864

2208579

            drop(distinct_bounds);

865

866

            // The rule applies: now build the replacement.

867

2208579

            let mut new_vec: Vec<Expr> = Vec::new();

868

            // Strongest constant bound per (atomic LHS, comparison operator), first-seen order.

869

2208579

            let mut constant_bounds: IndexMap<(Atom, ConstantBoundOp), i32> = IndexMap::new();

870

2208579

            for expr in vec.iter() {

871

5877346

                if matches!(expr, Expr::Atomic(_, Atom::Literal(Lit::Bool(_)))) {

872

2210441

                    continue;

873

3666905

                } else if let Some((lhs, op, rhs)) = as_constant_bound_comparison(expr) {

874

106812

                    merge_constant_bound(&mut constant_bounds, lhs, op, rhs);

875

                } else {

876

3560093

                    new_vec.push(expr.clone());

877

878

879

880

2208579

            for ((lhs, op), rhs) in constant_bounds {

881

9427

                new_vec.push(make_constant_bound_comparison(lhs, op, rhs));

882

883

884

2208579

            if new_vec.is_empty() {

885

                Ok(RuleEffect::pure(Expr::from(true)))

886

            } else {

887

2208579

                Ok(RuleEffect::pure(Expr::And(

888

2208579

                    Metadata::new(),

889

2208579

                    Moo::new(into_matrix_expr![new_vec]),

890

2208579

)))

891

892

893

894

        // similar to And, but booleans are returned wrapped in Root.

895

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

896

1643252

            match es.as_slice() {

897

                [] => Err(RuleNotApplicable),

898

                // want to unwrap nested ands

899

4616

                [Expr::And(_, _)] => Ok(()),

900

                // root([true]) / root([false]) are already evaluated

901

1315833

                [_] => Err(RuleNotApplicable),

902

322803

                [_, _, ..] => Ok(()),

903

1315833

}?;

904

905

327419

            let mut new_vec: Vec<Expr> = Vec::new();

906

327419

            let mut has_changed: bool = false;

907

327419

            for expr in es {

908

2818220

                match expr {

909

                    Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) => {

910

1185259

                        has_changed = true;

911

1185259

                        if !x {

912

                            // false

913

233

                            return Ok(RuleEffect::pure(Expr::Root(

914

233

                                Metadata::new(),

915

233

                                vec![Expr::Atomic(

916

233

                                    Default::default(),

917

233

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

918

233

)],

919

233

                            )));

920

1185026

921

                        // remove trues

922

923

924

                    // flatten ands in root, applying the same true/false rules to conjuncts

925

82625

                    Expr::And(_, vecs) => match Moo::unwrap_or_clone(vecs.clone()).into_list() {

926

                        Some(list) => {

927

82625

                            has_changed = true;

928

82625

                            for conjunct in list {

929

485226

                                match conjunct {

930

                                    Expr::Atomic(_, Atom::Literal(Lit::Bool(false))) => {

931

                                        return Ok(RuleEffect::pure(Expr::Root(

932

                                            Metadata::new(),

933

                                            vec![Expr::Atomic(

934

                                                Default::default(),

935

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

936

)],

937

                                        )));

938

939

1

                                    Expr::Atomic(_, Atom::Literal(Lit::Bool(true))) => {}

940

485225

                                    other => new_vec.push(other),

941

942

943

944

                        None => new_vec.push(expr.clone()),

945

},

946

1550336

                    _ => new_vec.push(expr.clone()),

947

948

949

950

327186

            if !has_changed {

951

35708

                Err(RuleNotApplicable)

952

            } else {

953

291478

                if new_vec.is_empty() {

954

264977

                    new_vec.push(true.into());

955

26501

956

291478

                Ok(RuleEffect::pure(Expr::Root(Metadata::new(), new_vec)))

957

958

959

        Expr::Imply(_m, x, y) => {

960

20921214

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {

961

4847948

                return if *x {

962

                    // (true) -> y ~~> y

963

2302182

                    Ok(RuleEffect::pure(Moo::unwrap_or_clone(y.clone())))

964

                } else {

965

                    // (false) -> y ~~> true

966

2545766

                    Ok(RuleEffect::pure(Expr::Atomic(Metadata::new(), true.into())))

967

};

968

16073266

};

969

970

16073266

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {

971

255391

                return if *y {

972

                    // x -> (true) ~~> true

973

120896

                    Ok(RuleEffect::pure(Expr::from(true)))

974

                } else {

975

                    // x -> (false) ~~> !x

976

134495

                    Ok(RuleEffect::pure(Expr::Not(Metadata::new(), x.clone())))

977

};

978

15817875

};

979

980

            // reflexivity: p -> p ~> true

981

982

            // instead of checking syntactic equivalence of a possibly deep expression,

983

            // let identical-CSE turn them into identical variables first. Then, check if they are

984

            // identical variables.

985

986

15817875

            if x.identical_atom_to(y.as_ref())

987

2672

                && (mode == PartialEvalMode::Local

988

4

                    || (is_semantically_safe(x) && is_semantically_safe(y)))

989

990

2672

                return Ok(RuleEffect::pure(true.into()));

991

15815203

992

993

15815203

            Err(RuleNotApplicable)

994

995

        Expr::Iff(_m, x, y) => {

996

14840957

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(x))) = x.as_ref() {

997

87

                return if *x {

998

                    // (true) <-> y ~~> y

999

                    Ok(RuleEffect::pure(Moo::unwrap_or_clone(y.clone())))

1000

                } else {

1001

                    // (false) <-> y ~~> !y

1002

87

                    Ok(RuleEffect::pure(Expr::Not(Metadata::new(), y.clone())))

1003

};

1004

14840870

};

1005

14840870

            if let Expr::Atomic(_, Atom::Literal(Lit::Bool(y))) = y.as_ref() {

1006

12

                return if *y {

1007

                    // x <-> (true) ~~> x

1008

12

                    Ok(RuleEffect::pure(Moo::unwrap_or_clone(x.clone())))

1009

                } else {

1010

                    // x <-> (false) ~~> !x

1011

                    Ok(RuleEffect::pure(Expr::Not(Metadata::new(), x.clone())))

1012

};

1013

14840858

};

1014

1015

            // reflexivity: p <-> p ~> true

1016

1017

            // instead of checking syntactic equivalence of a possibly deep expression,

1018

            // let identical-CSE turn them into identical variables first. Then, check if they are

1019

            // identical variables.

1020

1021

14840858

            if x.identical_atom_to(y.as_ref())

1022

87

                && (mode == PartialEvalMode::Local

1023

                    || (is_semantically_safe(x) && is_semantically_safe(y)))

1024

1025

87

                return Ok(RuleEffect::pure(true.into()));

1026

14840771

1027

1028

14840771

            Err(RuleNotApplicable)

1029

1030

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

1031

78901766

            if let Some((eq_result, _)) = simplify_reflexive_comparison_with_mode(x, y, mode) {

1032

33669

                Ok(RuleEffect::pure(Expr::Atomic(

1033

33669

                    Metadata::new(),

1034

33669

                    Atom::Literal(Lit::Bool(eq_result)),

1035

33669

)))

1036

78868097

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()

1037

1245782

                && comparison_domain_lookup_is_cheap(y, mode)

1038

911543

                && let Some((Some(eq_result), _)) = simplify_comparison_with_literal(y, lit)

1039

1040

58

                Ok(RuleEffect::pure(Expr::Atomic(

1041

58

                    Metadata::new(),

1042

58

                    Atom::Literal(Lit::Bool(eq_result)),

1043

58

)))

1044

78868039

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()

1045

59208764

                && comparison_domain_lookup_is_cheap(x, mode)

1046

27533327

                && let Some((Some(eq_result), _)) = simplify_comparison_with_literal(x, lit)

1047

1048

209119

                Ok(RuleEffect::pure(Expr::Atomic(

1049

209119

                    Metadata::new(),

1050

209119

                    Atom::Literal(Lit::Bool(eq_result)),

1051

209119

)))

1052

78658920

            } else if let Some(atom) = try_lower_bool_atom_eq_true(expr) {

1053

62295

                Ok(RuleEffect::pure(atom))

1054

            } else {

1055

78596625

                Err(RuleNotApplicable)

1056

1057

1058

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

1059

7969763

            if let Some((_, neq_result)) = simplify_reflexive_comparison_with_mode(x, y, mode) {

1060

18560

                Ok(RuleEffect::pure(Expr::Atomic(

1061

18560

                    Metadata::new(),

1062

18560

                    Atom::Literal(Lit::Bool(neq_result)),

1063

18560

)))

1064

7951203

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = x.as_ref()

1065

31310

                && comparison_domain_lookup_is_cheap(y, mode)

1066

11799

                && let Some((_, Some(neq_result))) = simplify_comparison_with_literal(y, lit)

1067

1068

406

                Ok(RuleEffect::pure(Expr::Atomic(

1069

406

                    Metadata::new(),

1070

406

                    Atom::Literal(Lit::Bool(neq_result)),

1071

406

)))

1072

7950797

            } else if let Expr::Atomic(_, Atom::Literal(lit)) = y.as_ref()

1073

5049470

                && comparison_domain_lookup_is_cheap(x, mode)

1074

3767048

                && let Some((_, Some(neq_result))) = simplify_comparison_with_literal(x, lit)

1075

1076

6181

                Ok(RuleEffect::pure(Expr::Atomic(

1077

6181

                    Metadata::new(),

1078

6181

                    Atom::Literal(Lit::Bool(neq_result)),

1079

6181

)))

1080

            } else {

1081

7944616

                Err(RuleNotApplicable)

1082

1083

1084

5764314

        Expr::Geq(_, _, _) => Err(RuleNotApplicable),

1085

35386822

        Expr::Leq(_, _, _) => Err(RuleNotApplicable),

1086

1877523

        Expr::Gt(_, _, _) => Err(RuleNotApplicable),

1087

10452775

        Expr::Lt(_, _, _) => Err(RuleNotApplicable),

1088

1089

        Expr::Pred(_, _) => Err(RuleNotApplicable),

1090

16

        Expr::Succ(_, _) => Err(RuleNotApplicable),

1091

1092

3438952

        Expr::SafeDiv(_, _, _) => Err(RuleNotApplicable),

1093

6210339

        Expr::UnsafeDiv(_, _, _) => Err(RuleNotApplicable),

1094

1743915

        Expr::Flatten(_, _, _) => Err(RuleNotApplicable), // TODO: check if anything can be done here

1095

        Expr::AllDiff(m, e) => {

1096

1593651

            let Some((vec, _)) = Moo::unwrap_or_clone(e.clone()).unwrap_matrix_unchecked() else {

1097

809653

                return Err(RuleNotApplicable);

1098

};

1099

1100

783998

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

1101

1102

            // A fully constant allDiff can be decided immediately.

1103

783998

            for expr in vec {

1104

789392

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

1105

780779

                    return Err(RuleNotApplicable);

1106

};

1107

8613

                if !consts.insert(lit) {

1108

2436

                    return Ok(RuleEffect::pure(Expr::Atomic(

1109

2436

                        m.clone(),

1110

2436

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

1111

2436

                    )));

1112

6177

1113

1114

1115

783

            Ok(RuleEffect::pure(Expr::Atomic(

1116

783

                m.clone(),

1117

783

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

1118

783

)))

1119

1120

401248

        Expr::Neg(_, _) => Err(RuleNotApplicable),

1121

        Expr::Factorial(_, _) => Err(RuleNotApplicable),

1122

13528210

        Expr::AuxDeclaration(_, _, _) => Err(RuleNotApplicable),

1123

7119557

        Expr::UnsafeMod(_, _, _) => Err(RuleNotApplicable),

1124

4270994

        Expr::SafeMod(_, _, _) => Err(RuleNotApplicable),

1125

290175

        Expr::UnsafePow(_, _, _) => Err(RuleNotApplicable),

1126

        Expr::SafePow(_, base, exponent) => {

1127

217953

            let base = cheap_singleton_int_value(base).ok_or(RuleNotApplicable)?;

1128

874

            let exponent = cheap_singleton_int_value(exponent).ok_or(RuleNotApplicable)?;

1129

874

            if exponent < 0 || (base == 0 && exponent == 0) {

1130

2

                return Err(RuleNotApplicable);

1131

872

1132

872

            let value = base.checked_pow(exponent as u32).ok_or(RuleNotApplicable)?;

1133

871

            Ok(RuleEffect::pure(Expr::from(value)))

1134

1135

1504481

        Expr::Minus(_, _, _) => Err(RuleNotApplicable),

1136

117973

        Expr::Card(_, _) => Err(RuleNotApplicable),

1137

1138

        // As these are in a low level solver form, I'm assuming that these have already been

1139

        // simplified and partially evaluated.

1140

7523

        Expr::FlatAllDiff(_, _) => Err(RuleNotApplicable),

1141

11049

        Expr::SmtDistinct(_, _) => Err(RuleNotApplicable),

1142

435

        Expr::FlatAbsEq(_, _, _) => Err(RuleNotApplicable),

1143

319

        Expr::FlatMinEq(_, _, _) => Err(RuleNotApplicable),

1144

444535

        Expr::FlatIneq(_, _, _, _) => Err(RuleNotApplicable),

1145

1856

        Expr::FlatMinusEq(_, _, _) => Err(RuleNotApplicable),

1146

7732

        Expr::FlatProductEq(_, _, _, _) => Err(RuleNotApplicable),

1147

77440

        Expr::FlatSumLeq(_, _, _) => Err(RuleNotApplicable),

1148

94993

        Expr::FlatSumGeq(_, _, _) => Err(RuleNotApplicable),

1149

1260863

        Expr::FlatWatchedLiteral(_, _, _) => Err(RuleNotApplicable),

1150

13293

        Expr::FlatWeightedSumLeq(_, _, _, _) => Err(RuleNotApplicable),

1151

12684

        Expr::FlatWeightedSumGeq(_, _, _, _) => Err(RuleNotApplicable),

1152

122046

        Expr::MinionDivEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),

1153

124134

        Expr::MinionModuloEqUndefZero(_, _, _, _) => Err(RuleNotApplicable),

1154

449

        Expr::MinionPow(_, _, _, _) => Err(RuleNotApplicable),

1155

522683

        Expr::MinionReify(_, _, _) => Err(RuleNotApplicable),

1156

193428

        Expr::MinionReifyImply(_, _, _) => Err(RuleNotApplicable),

1157

609

        Expr::MinionWInIntervalSet(_, _, _) => Err(RuleNotApplicable),

1158

261

        Expr::MinionWInSet(_, _, _) => Err(RuleNotApplicable),

1159

24770

        Expr::MinionElementOne(_, _, _, _) => Err(RuleNotApplicable),

1160

31802119

        Expr::SatObjective(..) | Expr::SATInt(_, _, _, _) => Err(RuleNotApplicable),

1161

        Expr::PairwiseSum(_, _, _) => Err(RuleNotApplicable),

1162

        Expr::PairwiseProduct(_, _, _) => Err(RuleNotApplicable),

1163

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

1164

66991

            let active_alternative = match variant.as_ref() {

1165

1

                Expr::AbstractLiteral(_, AbstractLiteral::Variant(field)) => &field.name,

1166

                Expr::Atomic(

1167

_,

1168

                    Atom::Literal(Lit::AbstractLiteral(AbstractLiteral::Variant(field))),

1169

                ) => &field.name,

1170

66990

                _ => return Err(RuleNotApplicable),

1171

};

1172

1173

1

            Ok(RuleEffect::pure(Expr::Atomic(

1174

1

                m.clone(),

1175

1

                Lit::Bool(active_alternative == alternative).into(),

1176

1

)))

1177

1178

        // Semantic lowering for these lives in registered rules (function/set/mset/relation

1179

        // horizontal rules), not here; the partial evaluator only offers extra constant-folding,

1180

        // which `eval.rs`'s matching arms cover for the fully-constant case. Previously these

1181

        // were `todo!()`, which panicked unconditionally on every rewrite of the operator (not

1182

        // just constant ones), since `normalise_evaluator_local` calls this on every expression

1183

        // node — the same landmine already found and fixed for Subsequence/Substring.

1184

8961

        Expr::Defined(_, _) => Err(RuleNotApplicable),

1185

21344

        Expr::Range(_, _) => Err(RuleNotApplicable),

1186

457475

        Expr::Image(_, _, _) => Err(RuleNotApplicable),

1187

        Expr::ImageSet(_, _, _) => Err(RuleNotApplicable),

1188

        Expr::PreImage(_, _, _) => Err(RuleNotApplicable),

1189

1450

        Expr::Inverse(_, _, _) => Err(RuleNotApplicable),

1190

        Expr::PermInverse(_, _) => Err(RuleNotApplicable),

1191

        Expr::Compose(_, _, _) => Err(RuleNotApplicable),

1192

        Expr::Restrict(_, _, _) => Err(RuleNotApplicable),

1193

        Expr::ToSet(_, _) => Err(RuleNotApplicable),

1194

        Expr::ToMSet(_, _) => Err(RuleNotApplicable),

1195

        Expr::ToRelation(_, _) => Err(RuleNotApplicable),

1196

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

1197

        Expr::Apart(_, _, _) => Err(RuleNotApplicable),

1198

        Expr::Together(_, _, _) => Err(RuleNotApplicable),

1199

        Expr::Participants(_, _) => Err(RuleNotApplicable),

1200

        Expr::Party(_, _, _) => Err(RuleNotApplicable),

1201

        Expr::Parts(_, _) => Err(RuleNotApplicable),

1202

2523

        Expr::Subsequence(_, _, _) => Err(RuleNotApplicable),

1203

5307

        Expr::Substring(_, _, _) => Err(RuleNotApplicable),

1204

1723180

        Expr::LexLt(_, _, _) => Err(RuleNotApplicable),

1205

448804

        Expr::LexLeq(_, _, _) => Err(RuleNotApplicable),

1206

52374

        Expr::LexGt(_, _, _) => Err(RuleNotApplicable),

1207

104545

        Expr::LexGeq(_, _, _) => Err(RuleNotApplicable),

1208

8845

        Expr::FlatLexLt(_, _, _) => Err(RuleNotApplicable),

1209

3074

        Expr::FlatLexLeq(_, _, _) => Err(RuleNotApplicable),

1210

        Expr::AllDifferentExcept(_, _, _)

1211

        | Expr::ElementId(_, _, _)

1212

        | Expr::IndexOf(_, _, _)

1213

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

1214

5306449

        | Expr::SatAllDifferentComparisons(_, _) => Err(RuleNotApplicable),

1215

1216

1850344781

1217

1218

/// Whether an `and`/`or` operand is a matrix literal holding no elements.

1219

///

1220

/// This deliberately ignores the index domain: `unwrap_list*` only recognise the normalised

1221

/// `int(1..)`, and an empty `[]` parses to `[;int(1..0)]`. Matching the elements directly folds

1222

/// `and([])` / `or([])` before `matrix_to_list` normalises the domain, and so before any

1223

/// solver-family rule can fire on an expression that is already known to be constant.

1224

281218932

fn is_empty_matrix_operand(operand: &Expr) -> bool {

1225

281218932

    match operand {

1226

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

1227

12760

            is_empty_matrix_operand(inner)

1228

1229

274230538

        Expr::AbstractLiteral(_, AbstractLiteral::Matrix(elems, _)) => elems.is_empty(),

1230

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

1231

18299

            elems.is_empty()

1232

1233

6957335

        _ => false,

1234

1235

281218932

1236

1237

/// Extracts `lhs ▷ k` where `lhs` is atomic and `k` is an integer literal.

1238

3666905

fn as_constant_bound_comparison(expr: &Expr) -> Option<(Atom, ConstantBoundOp, i32)> {

1239

3666905

    as_constant_bound_comparison_ref(expr).map(|(lhs, op, rhs)| (lhs.clone(), op, rhs))

1240

3666905

1241

1242

/// Borrowing variant of [`as_constant_bound_comparison`], for the inspection pass.

1243

847888676

fn as_constant_bound_comparison_ref(expr: &Expr) -> Option<(&Atom, ConstantBoundOp, i32)> {

1244

847888676

    let (lhs, rhs, op) = match expr {

1245

194821

        Expr::Gt(_, lhs, rhs) => (lhs, rhs, ConstantBoundOp::Gt),

1246

5177925

        Expr::Geq(_, lhs, rhs) => (lhs, rhs, ConstantBoundOp::Geq),

1247

398518

        Expr::Lt(_, lhs, rhs) => (lhs, rhs, ConstantBoundOp::Lt),

1248

11582248

        Expr::Leq(_, lhs, rhs) => (lhs, rhs, ConstantBoundOp::Leq),

1249

830535164

        _ => return None,

1250

};

1251

1252

17353512

    let Expr::Atomic(_, Atom::Literal(Lit::Int(rhs_value))) = rhs.as_ref() else {

1253

5390753

        return None;

1254

};

1255

11962759

    let Expr::Atomic(_, lhs_atom) = lhs.as_ref() else {

1256

11325198

        return None;

1257

};

1258

637561

    Some((lhs_atom, op, *rhs_value))

1259

847888676

1260

1261

/// Rebuilds a constant bound comparison from its dominated components.

1262

9427

fn make_constant_bound_comparison(lhs: Atom, op: ConstantBoundOp, rhs: i32) -> Expr {

1263

9427

    let lhs = Expr::Atomic(Metadata::new(), lhs);

1264

9427

    let rhs = Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Int(rhs)));

1265

9427

    match op {

1266

2118

        ConstantBoundOp::Gt => Expr::Gt(Metadata::new(), Moo::new(lhs), Moo::new(rhs)),

1267

145

        ConstantBoundOp::Geq => Expr::Geq(Metadata::new(), Moo::new(lhs), Moo::new(rhs)),

1268

3016

        ConstantBoundOp::Lt => Expr::Lt(Metadata::new(), Moo::new(lhs), Moo::new(rhs)),

1269

4148

        ConstantBoundOp::Leq => Expr::Leq(Metadata::new(), Moo::new(lhs), Moo::new(rhs)),

1270

1271

9427

1272

1273

/// Keeps the strongest RHS for `(lhs, op)` under conjunction, preserving first-seen order.

1274

///

1275

/// Bounds are keyed rather than searched, so merging `n` bounds over distinct atoms -- the shape

1276

/// unrolling `forAll i : D. x[i] >= k` produces -- is linear in `n` rather than quadratic.

1277

/// `IndexMap` gives the lookup while keeping first-seen order.

1278

106812

fn merge_constant_bound(

1279

106812

    bounds: &mut IndexMap<(Atom, ConstantBoundOp), i32>,

1280

106812

    lhs: Atom,

1281

106812

    op: ConstantBoundOp,

1282

106812

    rhs: i32,

1283

106812

) {

1284

106812

    match bounds.entry((lhs, op)) {

1285

        indexmap::map::Entry::Occupied(mut entry) => {

1286

97385

            let existing = entry.get_mut();

1287

97385

            if op.prefers_larger_rhs() {

1288

93150

                if rhs > *existing {

1289

16937

                    *existing = rhs;

1290

76213

1291

4235

            } else if rhs < *existing {

1292

1

                *existing = rhs;

1293

4234

1294

1295

        indexmap::map::Entry::Vacant(entry) => {

1296

9427

            entry.insert(rhs);

1297

1298

1299

106812

1300

1301

/// Checks for tautologies involving pairs of terms inside an or, returning true if one is found.

1302

///

1303

/// This applies the following rules:

1304

///

1305

/// ```text

1306

/// (p->q) \/ (q->p) ~> true    [totality of implication]

1307

/// (p->q) \/ (p-> !q) ~> true  [conditional excluded middle]

1308

/// ```

1309

///

1310

211923413

fn check_pairwise_or_tautologies(or_terms: &[Expr]) -> bool {

1311

    // `identical_atom_to` can only succeed when both sides are atomic, so index the atomic pairs

1312

    // and look each candidate up. This is expected O(n), not the O(n^2) of comparing every pair.

1313

    #[allow(clippy::mutable_key_type)]

1314

211923413

    let mut p_implies_q: HashSet<(&Atom, &Atom)> = HashSet::new();

1315

    #[allow(clippy::mutable_key_type)]

1316

211923413

    let mut p_implies_not_q: HashSet<(&Atom, &Atom)> = HashSet::new();

1317

1318

211923413

    for term in or_terms {

1319

502763014

        if let Expr::Imply(_, p, q) = term {

1320

1663063

            if let Expr::Not(_, q_1) = q.as_ref() {

1321

311257

                if let (Expr::Atomic(_, p), Expr::Atomic(_, q)) = (p.as_ref(), q_1.as_ref()) {

1322

2146

                    p_implies_not_q.insert((p, q));

1323

309111

1324

1351806

            } else if let (Expr::Atomic(_, p), Expr::Atomic(_, q)) = (p.as_ref(), q.as_ref()) {

1325

26796

                p_implies_q.insert((p, q));

1326

1325010

1327

501099951

1328

1329

1330

    // `(p->q) \/ (q->p) ~> true    [totality of implication]`

1331

211923413

    for &(p, q) in &p_implies_q {

1332

24650

        if p_implies_q.contains(&(q, p)) {

1333

2146

            return true;

1334

22504

1335

1336

1337

    // `(p->q) \/ (p-> !q) ~> true`    [conditional excluded middle]

1338

211921267

    p_implies_not_q

1339

211921267

        .iter()

1340

2146

        .any(|pair| p_implies_q.contains(pair))

1341

211923413

1342

1343

#[cfg(test)]

1344

mod tests {

1345

    use super::*;

1346

    use crate::ast::{DeclarationPtr, Domain, Name};

1347

1348

20

    fn int_lit(value: i32) -> Expr {

1349

20

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

1350

20

1351

1352

9

    fn bool_lit(value: bool) -> Expr {

1353

9

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

1354

9

1355

1356

7

    fn atom_ref(name: &str) -> Expr {

1357

7

        Expr::Atomic(

1358

7

            Metadata::new(),

1359

7

            Atom::Reference(crate::ast::Reference::new(DeclarationPtr::new_find(

1360

7

                Name::user(name),

1361

7

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

1362

7

            ))),

1363

7

1364

7

1365

1366

1

    fn singleton_ref(name: &str, value: i32) -> Expr {

1367

1

        Expr::Atomic(

1368

1

            Metadata::new(),

1369

1

            Atom::Reference(crate::ast::Reference::new(DeclarationPtr::new_find(

1370

1

                Name::user(name),

1371

1

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

1372

1

            ))),

1373

1

1374

1

1375

1376

5

    fn safe_pow(base: Expr, exponent: Expr) -> Expr {

1377

5

        Expr::SafePow(Metadata::new(), Moo::new(base), Moo::new(exponent))

1378

5

1379

1380

    #[test]

1381

1

    fn in_domain_simplification_does_not_expand_large_integer_domains() {

1382

1

        let domain = Domain::int(vec![Range::Bounded(-1_000_000_000, 1_000_000_000)]);

1383

        let variable: Expr =

1384

1

            crate::ast::Reference::new(DeclarationPtr::new_find(Name::user("wide"), domain)).into();

1385

1

        for evaluate in [run_partial_evaluator, run_partial_evaluator_local] {

1386

2

            for (target, expected) in [

1387

2

                (Domain::int(vec![Range::Bounded(i32::MIN, i32::MAX)]), true),

1388

2

1389

2

                    Domain::int(vec![Range::Bounded(1_000_000_001, i32::MAX)]),

1390

2

                    false,

1391

2

),

1392

2

] {

1393

                let expression =

1394

4

                    Expr::InDomain(Metadata::new(), Moo::new(variable.clone()), target);

1395

4

                assert_eq!(

1396

4

                    evaluate(&expression).unwrap().new_expression,

1397

4

                    bool_lit(expected)

1398

);

1399

1400

2

            let expression = Expr::InDomain(

1401

2

                Metadata::new(),

1402

2

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

1403

2

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

1404

2

);

1405

2

            assert!(evaluate(&expression).is_err());

1406

1407

1

1408

1409

    /// A power folds when both operands are singletons, taking the base from a declaration domain.

1410

    #[test]

1411

1

    fn safe_pow_folds_singleton_operands() {

1412

1

        let reduced = run_partial_evaluator_local(&safe_pow(singleton_ref("x", 2), int_lit(3)))

1413

1

            .expect("evaluates")

1414

1

            .new_expression;

1415

1

        assert_eq!(reduced, int_lit(8));

1416

1

1417

1418

    /// A non-singleton operand leaves the power alone: its value is not yet known.

1419

    #[test]

1420

1

    fn safe_pow_keeps_non_singleton_operands() {

1421

1

        assert!(run_partial_evaluator_local(&safe_pow(atom_ref("x"), int_lit(3))).is_err());

1422

1

1423

1424

    /// `0 ** 0` is undefined, and a negative exponent has no integer result.

1425

    #[test]

1426

1

    fn safe_pow_leaves_undefined_powers_alone() {

1427

1

        assert!(run_partial_evaluator_local(&safe_pow(int_lit(0), int_lit(0))).is_err());

1428

1

        assert!(run_partial_evaluator_local(&safe_pow(int_lit(2), int_lit(-1))).is_err());

1429

1

1430

1431

    /// Overflow is not folded: the model keeps the power rather than wrapping.

1432

    #[test]

1433

1

    fn safe_pow_leaves_overflowing_powers_alone() {

1434

1

        assert!(run_partial_evaluator_local(&safe_pow(int_lit(i32::MAX), int_lit(2))).is_err());

1435

1

1436

1437

5

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

1438

5

        Expr::And(Metadata::new(), Moo::new(into_matrix_expr![exprs]))

1439

5

1440

1441

1

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

1442

1

        Expr::Or(Metadata::new(), Moo::new(into_matrix_expr![exprs]))

1443

1

1444

1445

    /// An empty conjunction is the identity of `and`.

1446

///

1447

    /// The partial evaluator is the only thing that implements this: its hook runs after every

1448

    /// rewrite, so it reaches an empty `and`/`or` before any rule can.

1449

    #[test]

1450

1

    fn empty_and_is_true() {

1451

1

        let reduced = run_partial_evaluator_local(&and(vec![]))

1452

1

            .expect("evaluates")

1453

1

            .new_expression;

1454

1

        assert_eq!(reduced, bool_lit(true));

1455

1

1456

1457

    /// An empty disjunction is the identity of `or`. See [`empty_and_is_true`].

1458

    #[test]

1459

1

    fn empty_or_is_false() {

1460

1

        let reduced = run_partial_evaluator_local(&or(vec![]))

1461

1

            .expect("evaluates")

1462

1

            .new_expression;

1463

1

        assert_eq!(reduced, bool_lit(false));

1464

1

1465

1466

    /// An empty matrix written as `[]` parses with the *empty* index domain `int(1..0)`, not the

1467

    /// normalised `int(1..)` that `unwrap_list` looks for. The evaluator must fold it regardless,

1468

    /// so that no solver-family rule sees an expression that is already known to be constant.

1469

2

    fn empty_matrix_with_empty_index_domain() -> Expr {

1470

2

        Expr::AbstractLiteral(

1471

2

            Metadata::new(),

1472

2

            AbstractLiteral::Matrix(

1473

2

                vec![],

1474

2

                DomainPtr::from(Domain::int(vec![Range::Bounded(1, 0)])),

1475

2

),

1476

2

1477

2

1478

1479

    #[test]

1480

1

    fn empty_and_with_empty_index_domain_is_true() {

1481

1

        let expr = Expr::And(

1482

1

            Metadata::new(),

1483

1

            Moo::new(empty_matrix_with_empty_index_domain()),

1484

1

);

1485

1

        let reduced = run_partial_evaluator_local(&expr)

1486

1

            .expect("evaluates")

1487

1

            .new_expression;

1488

1

        assert_eq!(reduced, bool_lit(true));

1489

1

1490

1491

    #[test]

1492

1

    fn empty_or_with_empty_index_domain_is_false() {

1493

1

        let expr = Expr::Or(

1494

1

            Metadata::new(),

1495

1

            Moo::new(empty_matrix_with_empty_index_domain()),

1496

1

);

1497

1

        let reduced = run_partial_evaluator_local(&expr)

1498

1

            .expect("evaluates")

1499

1

            .new_expression;

1500

1

        assert_eq!(reduced, bool_lit(false));

1501

1

1502

1503

    #[test]

1504

1

    fn non_empty_and_is_not_collapsed_to_a_boolean() {

1505

1

        let x = atom_ref("x");

1506

1

        let expr = and(vec![Expr::Gt(

1507

1

            Metadata::new(),

1508

1

            Moo::new(x),

1509

1

            Moo::new(int_lit(3)),

1510

1

        )]);

1511

        // Either it does not apply, or it rewrites to something that is not a bare boolean.

1512

1

        if let Ok(reduced) = run_partial_evaluator_local(&expr) {

1513

            assert_ne!(reduced.new_expression, bool_lit(true));

1514

            assert_ne!(reduced.new_expression, bool_lit(false));

1515

1

1516

1

1517

1518

    #[test]

1519

1

    fn and_dominates_constant_lower_bounds_on_same_atom() {

1520

1

        let x = atom_ref("x");

1521

1

        let expr = and(vec![

1522

1

            Expr::Gt(Metadata::new(), Moo::new(x.clone()), Moo::new(int_lit(3))),

1523

1

            bool_lit(true),

1524

1

            Expr::Gt(Metadata::new(), Moo::new(x.clone()), Moo::new(int_lit(9))),

1525

1

            Expr::Gt(Metadata::new(), Moo::new(x), Moo::new(int_lit(1))),

1526

1

]);

1527

1528

1

        let reduced = run_partial_evaluator_local(&expr).unwrap().new_expression;

1529

1

        let Expr::And(_, operands) = reduced else {

1530

            panic!("expected And, got {reduced}");

1531

};

1532

1

        let list = Moo::unwrap_or_clone(operands).unwrap_list().unwrap();

1533

1

        assert_eq!(list.len(), 1);

1534

1

        assert!(matches!(

1535

1

            &list[0],

1536

            Expr::Gt(_, lhs, rhs)

1537

1

                if matches!(rhs.as_ref(), Expr::Atomic(_, Atom::Literal(Lit::Int(9))))

1538

1

                    && matches!(lhs.as_ref(), Expr::Atomic(_, Atom::Reference(_)))

1539

));

1540

1

1541

1542

    #[test]

1543

1

    fn and_dominates_constant_upper_bounds_on_same_atom() {

1544

1

        let x = atom_ref("x");

1545

1

        let expr = and(vec![

1546

1

            Expr::Leq(Metadata::new(), Moo::new(x.clone()), Moo::new(int_lit(8))),

1547

1

            Expr::Leq(Metadata::new(), Moo::new(x), Moo::new(int_lit(4))),

1548

1

]);

1549

1550

1

        let reduced = run_partial_evaluator_local(&expr).unwrap().new_expression;

1551

1

        let Expr::And(_, operands) = reduced else {

1552

            panic!("expected And, got {reduced}");

1553

};

1554

1

        let list = Moo::unwrap_or_clone(operands).unwrap_list().unwrap();

1555

1

        assert_eq!(list.len(), 1);

1556

1

        assert!(matches!(

1557

1

            &list[0],

1558

            Expr::Leq(_, _, rhs)

1559

1

                if matches!(rhs.as_ref(), Expr::Atomic(_, Atom::Literal(Lit::Int(4))))

1560

));

1561

1

1562

1563

    #[test]

1564

1

    fn and_does_not_merge_a_single_constant_bound() {

1565

1

        let x = atom_ref("x");

1566

1

        let expr = and(vec![Expr::Gt(

1567

1

            Metadata::new(),

1568

1

            Moo::new(x),

1569

1

            Moo::new(int_lit(3)),

1570

1

        )]);

1571

1

        assert!(run_partial_evaluator_local(&expr).is_err());

1572

1

1573

1574

3

    fn product(factors: Vec<Expr>) -> Expr {

1575

3

        Expr::Product(Metadata::new(), Moo::new(into_matrix_expr![factors]))

1576

3

1577

1578

    /// Local evaluation must not move a lone zero factor to the end of a product.

1579

///

1580

    /// That reshuffle undoes `reorder_product`'s constant-first form and causes an infinite

1581

    /// rewrite loop on models such as `savilerow/diet` (`x[i] * 0`).

1582

    #[test]

1583

1

    fn local_product_does_not_reshuffle_zero_factor() {

1584

1

        let x = atom_ref("x");

1585

1

        let constant_first = product(vec![int_lit(0), x.clone()]);

1586

1

        let variable_first = product(vec![x, int_lit(0)]);

1587

1

        assert!(run_partial_evaluator_local(&constant_first).is_err());

1588

1

        assert!(run_partial_evaluator_local(&variable_first).is_err());

1589

1

1590

1591

    /// Deep evaluation still collapses a safe `0 * x` product to the literal zero.

1592

    #[test]

1593

1

    fn deep_product_collapses_safe_zero_factor() {

1594

1

        let expr = product(vec![int_lit(0), atom_ref("x")]);

1595

1

        let reduced = run_partial_evaluator(&expr).unwrap().new_expression;

1596

1

        assert_eq!(reduced, int_lit(0));

1597

1

1598

1599

    #[test]

1600

1

    fn symbolic_cardinality_is_left_for_representation_rules() {

1601

1

        let set = Expr::Atomic(

1602

1

            Metadata::new(),

1603

1

            Atom::Reference(crate::ast::Reference::new(DeclarationPtr::new_find(

1604

1

                Name::user("s"),

1605

1

                Domain::set(

1606

1

                    crate::ast::SetAttr::new_max_size(2),

1607

1

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

1608

1

),

1609

1

            ))),

1610

1

);

1611

1

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

1612

1613

1

        assert!(run_partial_evaluator_local(&cardinality).is_err());

1614

1

1615