Grcov report - expressions.rs

1

use std::collections::{HashSet, VecDeque};

2

use std::fmt::{Display, Formatter};

3

use std::hash::{DefaultHasher, Hash, Hasher};

4

use std::sync::atomic::{AtomicU64, Ordering};

5

6

static HASH_HITS: AtomicU64 = AtomicU64::new(0);

7

static HASH_MISSES: AtomicU64 = AtomicU64::new(0);

8

9

pub fn print_hash_stats() {

10

    println!(

11

        "Expression hash stats: hits={}, misses={}",

12

        HASH_HITS.load(Ordering::Relaxed),

13

        HASH_MISSES.load(Ordering::Relaxed)

14

);

15

16

use tracing::trace;

17

18

use conjure_cp_enum_compatibility_macro::{document_compatibility, generate_discriminants};

19

use itertools::Itertools;

20

use serde::{Deserialize, Serialize};

21

use tree_morph::cache::CacheHashable;

22

use ustr::Ustr;

23

24

use polyquine::Quine;

25

use uniplate::{Biplate, Uniplate};

26

27

use crate::ast::FuncAttr;

28

use crate::ast::metadata::NO_HASH;

29

use crate::bug;

30

31

use super::abstract_comprehension::AbstractComprehension;

32

use super::ac_operators::ACOperatorKind;

33

use super::categories::{Category, CategoryOf};

34

use super::comprehension::Comprehension;

35

use super::declaration::DeclarationKind;

36

use super::domains::HasDomain as _;

37

use super::pretty::{pretty_expressions_as_top_level, pretty_vec};

38

use super::records::Field;

39

use super::sat_encoding::SATIntEncoding;

40

use super::{

41

    AbstractLiteral, Atom, DeclarationPtr, Domain, DomainPtr, GroundDomain, IntVal, JectivityAttr,

42

    Literal, MSetAttr, Metadata, Model, Moo, Name, PartialityAttr, Range, Reference, RelAttr,

43

    ReturnType, SetAttr, SymbolTable, SymbolTablePtr, Typeable, UnresolvedDomain, matrix,

44

};

45

46

// Ensure that this type doesn't get too big

47

//

48

// If you triggered this assertion, you either made a variant of this enum that is too big, or you

49

// made Name,Literal,AbstractLiteral,Atom bigger, which made this bigger! To fix this, put some

50

// stuff in boxes.

51

//

52

// Enums take the size of their largest variant, so an enum with mostly small variants and a few

53

// large ones wastes memory... A larger Expression type also slows down Oxide.

54

//

55

// For more information, and more details on type sizes and how to measure them, see the commit

56

// message for 6012de809 (perf: reduce size of AST types, 2025-06-18).

57

//

58

// You can also see type sizes in the rustdoc documentation, generated by ./tools/gen_docs.sh

59

//

60

// https://github.com/conjure-cp/conjure-oxide/commit/6012de8096ca491ded91ecec61352fdf4e994f2e

61

62

// TODO: box all usages of Metadata to bring this down a bit more - I have added variants to

63

// ReturnType, and Metadata contains ReturnType, so Metadata has got bigger. Metadata will get a

64

// lot bigger still when we start using it for memoisation, so it should really be

65

// boxed ~niklasdewally

66

67

// expect size of Expression to be 112 bytes

68

static_assertions::assert_eq_size!([u8; 112], Expression);

69

70

/// Represents different types of expressions used to define rules and constraints in the model.

71

///

72

/// The `Expression` enum includes operations, constants, and variable references

73

/// used to build rules and conditions for the model.

74

#[generate_discriminants]

75

#[document_compatibility]

76

#[derive(Clone, Debug, Hash, PartialEq, Eq, Serialize, Deserialize, Uniplate, Quine)]

77

#[biplate(to=AbstractComprehension)]

78

#[biplate(to=AbstractLiteral<Expression>)]

79

#[biplate(to=AbstractLiteral<Literal>)]

80

#[biplate(to=Atom)]

81

#[biplate(to=Comprehension)]

82

#[biplate(to=DeclarationPtr)]

83

#[biplate(to=DomainPtr)]

84

#[biplate(to=Literal)]

85

#[biplate(to=Metadata)]

86

#[biplate(to=Name)]

87

#[biplate(to=Option<Expression>)]

88

#[biplate(to=Field<Expression>)]

89

#[biplate(to=Field<Literal>)]

90

#[biplate(to=Reference)]

91

#[biplate(to=Model)]

92

#[biplate(to=SymbolTable)]

93

#[biplate(to=SymbolTablePtr)]

94

#[biplate(to=Vec<Expression>)]

95

#[path_prefix(conjure_cp::ast)]

96

pub enum Expression {

97

    AbstractLiteral(Metadata, AbstractLiteral<Expression>),

98

    /// The top of the model

99

    Root(Metadata, Vec<Expression>),

100

101

    /// An expression representing "A is valid as long as B is true"

102

    /// Turns into a conjunction when it reaches a boolean context

103

    Bubble(Metadata, Moo<Expression>, Moo<Expression>),

104

105

    /// A comprehension.

106

///

107

    /// The inside of the comprehension opens a new scope.

108

    // todo (gskorokhod): Comprehension contains a symbol table which contains a bunch of pointers.

109

    // This makes implementing Quine tricky (it doesnt support Rc, by design). Skip it for now.

110

    #[polyquine_skip]

111

    Comprehension(Metadata, Moo<Comprehension>),

112

113

    /// Higher-level abstract comprehension

114

    #[polyquine_skip] // no idea what this is lol but it stops rustc screaming at me

115

    AbstractComprehension(Metadata, Moo<AbstractComprehension>),

116

117

    /// Defines dominance ("Solution A is preferred over Solution B")

118

    DominanceRelation(Metadata, Moo<Expression>),

119

    /// `fromSolution(name)` - Used in dominance relation definitions

120

    FromSolution(Metadata, Moo<Atom>),

121

122

    #[polyquine_with(arm = (_, name) => {

123

        let ident = proc_macro2::Ident::new(name.as_str(), proc_macro2::Span::call_site());

124

        quote::quote! { #ident.clone().into() }

125

})]

126

    Metavar(Metadata, Ustr),

127

128

    Atomic(Metadata, Atom),

129

130

    /// Asserts that the given variant of a variant expression is in use.

131

    /// See also: [GroundDomain::Variant]

132

    #[compatible(JsonInput)]

133

    Active(Metadata, Moo<Expression>, Name),

134

135

    /// Indexing into a record expression, e.g `{foo = 1, bar = true}[foo]`

136

    /// See also: [GroundDomain::Record]

137

    #[compatible(JsonInput)]

138

    RecordField(Metadata, Moo<Expression>, Name),

139

140

    /// A matrix index.

141

///

142

    /// Defined iff the indices are within their respective index domains.

143

    #[compatible(JsonInput)]

144

    UnsafeIndex(Metadata, Moo<Expression>, Vec<Expression>),

145

146

    /// A safe matrix index.

147

///

148

    /// See [`Expression::UnsafeIndex`]

149

    #[compatible(SMT)]

150

    SafeIndex(Metadata, Moo<Expression>, Vec<Expression>),

151

152

    /// A matrix slice: `a[indices]`.

153

///

154

    /// One of the indicies may be `None`, representing the dimension of the matrix we want to take

155

    /// a slice of. For example, for some 3d matrix a, `a[1,..,2]` has the indices

156

    /// `Some(1),None,Some(2)`.

157

///

158

    /// It is assumed that the slice only has one "wild-card" dimension and thus is 1 dimensional.

159

///

160

    /// Defined iff the defined indices are within their respective index domains.

161

    #[compatible(JsonInput)]

162

    UnsafeSlice(Metadata, Moo<Expression>, Vec<Option<Expression>>),

163

164

    /// A safe matrix slice: `a[indices]`.

165

///

166

    /// See [`Expression::UnsafeSlice`].

167

    SafeSlice(Metadata, Moo<Expression>, Vec<Option<Expression>>),

168

169

    /// `inDomain(x,domain)` iff `x` is in the domain `domain`.

170

///

171

    /// This cannot be constructed from Essence input, nor passed to a solver: this expression is

172

    /// mainly used during the conversion of `UnsafeIndex` and `UnsafeSlice` to `SafeIndex` and

173

    /// `SafeSlice` respectively.

174

    InDomain(Metadata, Moo<Expression>, DomainPtr),

175

176

    /// `toInt(b)` casts boolean expression b to an integer.

177

///

178

    /// - If b is false, then `toInt(b) == 0`

179

///

180

    /// - If b is true, then `toInt(b) == 1`

181

    #[compatible(SMT)]

182

    ToInt(Metadata, Moo<Expression>),

183

184

    /// `|x|` - absolute value of `x`

185

    #[compatible(JsonInput, SMT)]

186

    Abs(Metadata, Moo<Expression>),

187

188

    /// `sum(<vec_expr>)`

189

    #[compatible(JsonInput, SMT)]

190

    Sum(Metadata, Moo<Expression>),

191

192

    /// `a * b * c * ...`

193

    #[compatible(JsonInput, SMT)]

194

    Product(Metadata, Moo<Expression>),

195

196

    /// `min(<vec_expr>)`

197

    #[compatible(JsonInput, SMT)]

198

    Min(Metadata, Moo<Expression>),

199

200

    /// `max(<vec_expr>)`

201

    #[compatible(JsonInput, SMT)]

202

    Max(Metadata, Moo<Expression>),

203

204

    /// `not(a)`

205

    #[compatible(JsonInput, SAT, SMT)]

206

    Not(Metadata, Moo<Expression>),

207

208

    /// `or(<vec_expr>)`

209

    #[compatible(JsonInput, SAT, SMT)]

210

    Or(Metadata, Moo<Expression>),

211

212

    /// `and(<vec_expr>)`

213

    #[compatible(JsonInput, SAT, SMT)]

214

    And(Metadata, Moo<Expression>),

215

216

    /// Ensures that `a->b` (material implication).

217

    #[compatible(JsonInput, SMT)]

218

    Imply(Metadata, Moo<Expression>, Moo<Expression>),

219

220

    /// `iff(a, b)` a <-> b

221

    #[compatible(JsonInput, SMT)]

222

    Iff(Metadata, Moo<Expression>, Moo<Expression>),

223

224

    #[compatible(JsonInput)]

225

    Union(Metadata, Moo<Expression>, Moo<Expression>),

226

227

    #[compatible(JsonInput)]

228

    In(Metadata, Moo<Expression>, Moo<Expression>),

229

230

    #[compatible(JsonInput)]

231

    Intersect(Metadata, Moo<Expression>, Moo<Expression>),

232

233

    #[compatible(JsonInput)]

234

    Supset(Metadata, Moo<Expression>, Moo<Expression>),

235

236

    #[compatible(JsonInput)]

237

    SupsetEq(Metadata, Moo<Expression>, Moo<Expression>),

238

239

    #[compatible(JsonInput)]

240

    Subset(Metadata, Moo<Expression>, Moo<Expression>),

241

242

    #[compatible(JsonInput)]

243

    SubsetEq(Metadata, Moo<Expression>, Moo<Expression>),

244

245

    #[compatible(JsonInput, SMT)]

246

    Eq(Metadata, Moo<Expression>, Moo<Expression>),

247

248

    #[compatible(JsonInput, SMT)]

249

    Neq(Metadata, Moo<Expression>, Moo<Expression>),

250

251

    #[compatible(JsonInput, SMT)]

252

    Geq(Metadata, Moo<Expression>, Moo<Expression>),

253

254

    #[compatible(JsonInput, SMT)]

255

    Leq(Metadata, Moo<Expression>, Moo<Expression>),

256

257

    #[compatible(JsonInput, SMT)]

258

    Gt(Metadata, Moo<Expression>, Moo<Expression>),

259

260

    #[compatible(JsonInput, SMT)]

261

    Lt(Metadata, Moo<Expression>, Moo<Expression>),

262

263

    /// `s subsequence t` tests whether the list of values taken by s occurs in the same order

264

    /// in the list of values taken by t

265

    #[compatible(JsonInput)]

266

    Subsequence(Metadata, Moo<Expression>, Moo<Expression>),

267

268

    /// `s substring t` tests whether the list of values taken by s occurs in the same order

269

    /// and contiguously in the list of values taken by t

270

    #[compatible(JsonInput)]

271

    Substring(Metadata, Moo<Expression>, Moo<Expression>),

272

273

    /// Division after preventing division by zero, usually with a bubble

274

    #[compatible(SMT)]

275

    SafeDiv(Metadata, Moo<Expression>, Moo<Expression>),

276

277

    /// Division with a possibly undefined value (division by 0)

278

    #[compatible(JsonInput)]

279

    UnsafeDiv(Metadata, Moo<Expression>, Moo<Expression>),

280

281

    /// Modulo after preventing mod 0, usually with a bubble

282

    #[compatible(SMT)]

283

    SafeMod(Metadata, Moo<Expression>, Moo<Expression>),

284

285

    /// Modulo with a possibly undefined value (mod 0)

286

    #[compatible(JsonInput)]

287

    UnsafeMod(Metadata, Moo<Expression>, Moo<Expression>),

288

289

    /// Negation: `-x`

290

    #[compatible(JsonInput, SMT)]

291

    Neg(Metadata, Moo<Expression>),

292

293

    /// Factorial: `x!` or 'factorial(x)`

294

    #[compatible(JsonInput)]

295

    Factorial(Metadata, Moo<Expression>),

296

297

    /// Set of domain values function is defined for

298

    #[compatible(JsonInput)]

299

    Defined(Metadata, Moo<Expression>),

300

301

    /// Set of codomain values function is defined for

302

    #[compatible(JsonInput)]

303

    Range(Metadata, Moo<Expression>),

304

305

    #[compatible(JsonInput)]

306

    ToSet(Metadata, Moo<Expression>),

307

308

    #[compatible(JsonInput)]

309

    ToMSet(Metadata, Moo<Expression>),

310

311

    #[compatible(JsonInput)]

312

    ToRelation(Metadata, Moo<Expression>),

313

314

    /// Unsafe power`x**y` (possibly undefined)

315

///

316

    /// Defined when (X!=0 \\/ Y!=0) /\ Y>=0

317

    #[compatible(JsonInput)]

318

    UnsafePow(Metadata, Moo<Expression>, Moo<Expression>),

319

320

    /// `UnsafePow` after preventing undefinedness

321

    SafePow(Metadata, Moo<Expression>, Moo<Expression>),

322

323

    /// Flatten matrix operator

324

    /// `flatten(M)` or `flatten(n, M)`

325

    /// where M is a matrix and n is an optional integer argument indicating depth of flattening

326

    Flatten(Metadata, Option<Moo<Expression>>, Moo<Expression>),

327

328

    /// `allDiff(<vec_expr>)`

329

    #[compatible(JsonInput)]

330

    AllDiff(Metadata, Moo<Expression>),

331

332

    /// `table([x1, x2, ...], [[r11, r12, ...], [r21, r22, ...], ...])`

333

///

334

    /// Represents a positive table constraint: the tuple `[x1, x2, ...]` must match one of the

335

    /// allowed rows.

336

    #[compatible(JsonInput)]

337

    Table(Metadata, Moo<Expression>, Moo<Expression>),

338

339

    /// `negativeTable([x1, x2, ...], [[r11, r12, ...], [r21, r22, ...], ...])`

340

///

341

    /// Represents a negative table constraint: the tuple `[x1, x2, ...]` must NOT match any of the

342

    /// forbidden rows.

343

    #[compatible(JsonInput)]

344

    NegativeTable(Metadata, Moo<Expression>, Moo<Expression>),

345

    /// Binary subtraction operator

346

///

347

    /// This is a parser-level construct, and is immediately normalised to `Sum([a,-b])`.

348

    /// TODO: make this compatible with Set Difference calculations - need to change return type and domain for this expression and write a set comprehension rule.

349

    /// have already edited minus_to_sum to prevent this from applying to sets

350

    #[compatible(JsonInput)]

351

    Minus(Metadata, Moo<Expression>, Moo<Expression>),

352

353

    /// Partition Operator: test if a list of elements are not all contained in one part of the partition

354

    /// First Expr Arg is a list of elements

355

    /// Second Expr Arg is the partition

356

    #[compatible(JsonInput)]

357

    Apart(Metadata, Moo<Expression>, Moo<Expression>),

358

359

    /// Partition Operator: union of all parts of a partition

360

    /// Expr Arg is a partition

361

    #[compatible(JsonInput)]

362

    Participants(Metadata, Moo<Expression>),

363

364

    /// Partition Operator: part of partition that contains specified element

365

    /// First Expr Arg is an element that should be contained

366

    /// Second Expr Arg is the partition that should contain that element

367

    #[compatible(JsonInput)]

368

    Party(Metadata, Moo<Expression>, Moo<Expression>),

369

370

    /// Partition Operator: partition to its set of parts

371

    /// Expr Arg is the partition from which the parts come from

372

    #[compatible(JsonInput)]

373

    Parts(Metadata, Moo<Expression>),

374

375

    /// Partition Operator: test if a list of elements are all in the same part of the partition

376

    /// First Expr Arg is the list of elements to test with

377

    /// Second Expr Arg is the partition to test on

378

    #[compatible(JsonInput)]

379

    Together(Metadata, Moo<Expression>, Moo<Expression>),

380

381

    /// Ensures that x=|y| i.e. x is the absolute value of y.

382

///

383

    /// Low-level Minion constraint.

384

///

385

    /// # See also

386

///

387

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#abs)

388

    #[compatible(Minion)]

389

    FlatAbsEq(Metadata, Moo<Atom>, Moo<Atom>),

390

391

    /// Ensures that `alldiff([a,b,...])`.

392

///

393

    /// Low-level Minion constraint.

394

///

395

    /// # See also

396

///

397

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#alldiff)

398

    #[compatible(Minion)]

399

    FlatAllDiff(Metadata, Vec<Atom>),

400

401

    /// Ensures that sum(vec) >= x.

402

///

403

    /// Low-level Minion constraint.

404

///

405

    /// # See also

406

///

407

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#sumgeq)

408

    #[compatible(Minion)]

409

    FlatSumGeq(Metadata, Vec<Atom>, Atom),

410

411

    /// Ensures that sum(vec) <= x.

412

///

413

    /// Low-level Minion constraint.

414

///

415

    /// # See also

416

///

417

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#sumleq)

418

    #[compatible(Minion)]

419

    FlatSumLeq(Metadata, Vec<Atom>, Atom),

420

421

    /// `ineq(x,y,k)` ensures that x <= y + k.

422

///

423

    /// Low-level Minion constraint.

424

///

425

    /// # See also

426

///

427

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#ineq)

428

    #[compatible(Minion)]

429

    FlatIneq(Metadata, Moo<Atom>, Moo<Atom>, Box<Literal>),

430

431

    /// `w-literal(x,k)` ensures that x == k, where x is a variable and k a constant.

432

///

433

    /// Low-level Minion constraint.

434

///

435

    /// This is a low-level Minion constraint and you should probably use Eq instead. The main use

436

    /// of w-literal is to convert boolean variables to constraints so that they can be used inside

437

    /// watched-and and watched-or.

438

///

439

    /// # See also

440

///

441

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#minuseq)

442

    /// + `rules::minion::boolean_literal_to_wliteral`.

443

    #[compatible(Minion)]

444

    #[polyquine_skip]

445

    FlatWatchedLiteral(Metadata, Reference, Literal),

446

447

    /// `weightedsumleq(cs,xs,total)` ensures that cs.xs <= total, where cs.xs is the scalar dot

448

    /// product of cs and xs.

449

///

450

    /// Low-level Minion constraint.

451

///

452

    /// Represents a weighted sum of the form `ax + by + cz + ...`

453

///

454

    /// # See also

455

///

456

    /// + [Minion

457

    /// documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#weightedsumleq)

458

    FlatWeightedSumLeq(Metadata, Vec<Literal>, Vec<Atom>, Moo<Atom>),

459

460

    /// `weightedsumgeq(cs,xs,total)` ensures that cs.xs >= total, where cs.xs is the scalar dot

461

    /// product of cs and xs.

462

///

463

    /// Low-level Minion constraint.

464

///

465

    /// Represents a weighted sum of the form `ax + by + cz + ...`

466

///

467

    /// # See also

468

///

469

    /// + [Minion

470

    /// documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#weightedsumleq)

471

    FlatWeightedSumGeq(Metadata, Vec<Literal>, Vec<Atom>, Moo<Atom>),

472

473

    /// Ensures that x =-y, where x and y are atoms.

474

///

475

    /// Low-level Minion constraint.

476

///

477

    /// # See also

478

///

479

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#minuseq)

480

    #[compatible(Minion)]

481

    FlatMinusEq(Metadata, Moo<Atom>, Moo<Atom>),

482

483

    /// Ensures that x*y=z.

484

///

485

    /// Low-level Minion constraint.

486

///

487

    /// # See also

488

///

489

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#product)

490

    #[compatible(Minion)]

491

    FlatProductEq(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

492

493

    /// Ensures that floor(x/y)=z. Always true when y=0.

494

///

495

    /// Low-level Minion constraint.

496

///

497

    /// # See also

498

///

499

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#div_undefzero)

500

    #[compatible(Minion)]

501

    MinionDivEqUndefZero(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

502

503

    /// Ensures that x%y=z. Always true when y=0.

504

///

505

    /// Low-level Minion constraint.

506

///

507

    /// # See also

508

///

509

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#mod_undefzero)

510

    #[compatible(Minion)]

511

    MinionModuloEqUndefZero(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

512

513

    /// Ensures that `x**y = z`.

514

///

515

    /// Low-level Minion constraint.

516

///

517

    /// This constraint is false when `y<0` except for `1**y=1` and `(-1)**y=z` (where z is 1 if y

518

    /// is odd and z is -1 if y is even).

519

///

520

    /// # See also

521

///

522

    /// + [Github comment about `pow` semantics](https://github.com/minion/minion/issues/40#issuecomment-2595914891)

523

    /// + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#pow)

524

    MinionPow(Metadata, Moo<Atom>, Moo<Atom>, Moo<Atom>),

525

526

    /// `reify(constraint,r)` ensures that r=1 iff `constraint` is satisfied, where r is a 0/1

527

    /// variable.

528

///

529

    /// Low-level Minion constraint.

530

///

531

    /// # See also

532

///

533

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#reify)

534

    #[compatible(Minion)]

535

    MinionReify(Metadata, Moo<Expression>, Atom),

536

537

    /// `reifyimply(constraint,r)` ensures that `r->constraint`, where r is a 0/1 variable.

538

    /// variable.

539

///

540

    /// Low-level Minion constraint.

541

///

542

    /// # See also

543

///

544

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#reifyimply)

545

    #[compatible(Minion)]

546

    MinionReifyImply(Metadata, Moo<Expression>, Atom),

547

548

    /// `w-inintervalset(x, [a1,a2, b1,b2, … ])` ensures that the value of x belongs to one of the

549

    /// intervals {a1,…,a2}, {b1,…,b2} etc.

550

///

551

    /// The list of intervals must be given in numerical order.

552

///

553

    /// Low-level Minion constraint.

554

///

555

    /// # See also

556

    ///>

557

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#w-inintervalset)

558

    #[compatible(Minion)]

559

    MinionWInIntervalSet(Metadata, Atom, Vec<i32>),

560

561

    /// `w-inset(x, [v1, v2, … ])` ensures that the value of `x` is one of the explicitly given values `v1`, `v2`, etc.

562

///

563

    /// This constraint enforces membership in a specific set of discrete values rather than intervals.

564

///

565

    /// The list of values must be given in numerical order.

566

///

567

    /// Low-level Minion constraint.

568

///

569

    /// # See also

570

///

571

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#w-inset)

572

    #[compatible(Minion)]

573

    MinionWInSet(Metadata, Atom, Vec<i32>),

574

575

    /// `element_one(vec, i, e)` specifies that `vec[i] = e`. This implies that i is

576

    /// in the range `[1..len(vec)]`.

577

///

578

    /// Low-level Minion constraint.

579

///

580

    /// # See also

581

///

582

    ///  + [Minion documentation](https://minion-solver.readthedocs.io/en/stable/usage/constraints.html#element_one)

583

    #[compatible(Minion)]

584

    MinionElementOne(Metadata, Vec<Atom>, Moo<Atom>, Moo<Atom>),

585

586

    /// Declaration of an auxiliary variable.

587

///

588

    /// As with Savile Row, we semantically distinguish this from `Eq`.

589

    #[compatible(Minion)]

590

    #[polyquine_skip]

591

    AuxDeclaration(Metadata, Reference, Moo<Expression>),

592

593

    /// This expression is for encoding ints for the SAT solver, it stores the encoding type, the vector of booleans and the min/max for the int.

594

    #[compatible(SAT)]

595

    SATInt(Metadata, SATIntEncoding, Moo<Expression>, (i32, i32)),

596

597

    /// Addition over a pair of expressions (i.e. a + b) rather than a vec-expr like Expression::Sum.

598

    /// This is for compatibility with backends that do not support addition over vectors.

599

    #[compatible(SMT)]

600

    PairwiseSum(Metadata, Moo<Expression>, Moo<Expression>),

601

602

    /// Multiplication over a pair of expressions (i.e. a * b) rather than a vec-expr like Expression::Product.

603

    /// This is for compatibility with backends that do not support multiplication over vectors.

604

    #[compatible(SMT)]

605

    PairwiseProduct(Metadata, Moo<Expression>, Moo<Expression>),

606

607

    #[compatible(JsonInput)]

608

    Image(Metadata, Moo<Expression>, Moo<Expression>),

609

610

    #[compatible(JsonInput)]

611

    ImageSet(Metadata, Moo<Expression>, Moo<Expression>),

612

613

    #[compatible(JsonInput)]

614

    PreImage(Metadata, Moo<Expression>, Moo<Expression>),

615

616

    #[compatible(JsonInput)]

617

    Inverse(Metadata, Moo<Expression>, Moo<Expression>),

618

619

    #[compatible(JsonInput)]

620

    Restrict(Metadata, Moo<Expression>, Moo<Expression>),

621

622

    /// Lexicographical < between two matrices.

623

///

624

    /// A <lex B iff: A[i] < B[i] for some i /\ (A[j] > B[j] for some j -> i < j)

625

    /// I.e. A must be less than B at some index i, and if it is greater than B at another index j,

626

    /// then j comes after i.

627

    /// I.e. A must be greater than B at the first index where they differ.

628

///

629

    /// E.g. [1, 1] <lex [2, 1] and [1, 1] <lex [1, 2]

630

    LexLt(Metadata, Moo<Expression>, Moo<Expression>),

631

632

    /// Lexicographical <= between two matrices

633

    LexLeq(Metadata, Moo<Expression>, Moo<Expression>),

634

635

    /// Lexicographical > between two matrices

636

    /// This is a parser-level construct, and is immediately normalised to LexLt(b, a)

637

    LexGt(Metadata, Moo<Expression>, Moo<Expression>),

638

639

    /// Lexicographical >= between two matrices

640

    /// This is a parser-level construct, and is immediately normalised to LexLeq(b, a)

641

    LexGeq(Metadata, Moo<Expression>, Moo<Expression>),

642

643

    /// Low-level minion constraint. See Expression::LexLt

644

    FlatLexLt(Metadata, Vec<Atom>, Vec<Atom>),

645

646

    /// Low-level minion constraint. See Expression::LexLeq

647

    FlatLexLeq(Metadata, Vec<Atom>, Vec<Atom>),

648

649

    /// Alters the shape of relations by projection

650

    #[compatible(JsonInput)]

651

    RelationProj(Metadata, Moo<Expression>, Vec<Option<Expression>>),

652

653

    /// Cardinality of a collection type

654

    #[compatible(JsonInput)]

655

    Card(Metadata, Moo<Expression>),

656

657

658

// for the given matrix literal, return a bounded domain from the min to max of applying op to each

659

// child expression.

660

//

661

// Op must be monotonic.

662

//

663

// Returns none if unbounded

664

1832227

fn bounded_i32_domain_for_matrix_literal_monotonic(

665

1832227

    e: &Expression,

666

1832227

    op: fn(i32, i32) -> Option<i32>,

667

1832227

) -> Option<DomainPtr> {

668

    // only care about the elements, not the indices

669

1832227

    let (mut exprs, _) = e.clone().unwrap_matrix_unchecked()?;

670

671

    // fold each element's domain into one using op.

672

//

673

    // here, I assume that op is monotone. This means that the bounds of op([a1,a2],[b1,b2])  for

674

    // the ranges [a1,a2], [b1,b2] will be

675

    // [min(op(a1,b1),op(a2,b1),op(a1,b2),op(a2,b2)),max(op(a1,b1),op(a2,b1),op(a1,b2),op(a2,b2))].

676

//

677

    // We used to not assume this, and work out the bounds by applying op on the Cartesian product

678

    // of A and B; however, this caused a combinatorial explosion and my computer to run out of

679

    // memory (on the hakank_eprime_xkcd test)...

680

    //Int

681

    // For example, to find the bounds of the intervals [1,4], [1,5] combined using op, we used to do

682

    //  [min(op(1,1), op(1,2),op(1,3),op(1,4),op(1,5),op(2,1)..

683

//

684

    // +,-,/,* are all monotone, so this assumption should be fine for now...

685

686

1810123

    let expr = exprs.pop()?;

687

1810122

    let dom = expr.domain_of()?;

688

1807362

    let resolved = dom.resolve().ok()?;

689

1807002

    let GroundDomain::Int(ranges) = resolved.as_ref() else {

690

25

        return None;

691

};

692

693

1806977

    let (mut current_min, mut current_max) = range_vec_bounds_i32(ranges)?;

694

695

2056109

    for expr in exprs {

696

2056109

        let dom = expr.domain_of()?;

697

2055749

        let resolved = dom.resolve().ok()?;

698

2055629

        let GroundDomain::Int(ranges) = resolved.as_ref() else {

699

            return None;

700

};

701

702

2055629

        let (min, max) = range_vec_bounds_i32(ranges)?;

703

704

        // all the possible new values for current_min / current_max

705

2055629

        let minmax = op(min, current_max)?;

706

2055629

        let minmin = op(min, current_min)?;

707

2055629

        let maxmin = op(max, current_min)?;

708

2055629

        let maxmax = op(max, current_max)?;

709

2055629

        let vals = [minmax, minmin, maxmin, maxmax];

710

711

2055629

        current_min = *vals

712

2055629

            .iter()

713

2055629

            .min()

714

2055629

            .expect("vals iterator should not be empty, and should have a minimum.");

715

2055629

        current_max = *vals

716

2055629

            .iter()

717

2055629

            .max()

718

2055629

            .expect("vals iterator should not be empty, and should have a maximum.");

719

720

721

1806497

    if current_min == current_max {

722

1061

        Some(Domain::int(vec![Range::Single(current_min)]))

723

    } else {

724

1805436

        Some(Domain::int(vec![Range::Bounded(current_min, current_max)]))

725

726

1832227

727

728

20

fn matrix_element_domain(e: &Expression) -> Option<DomainPtr> {

729

20

    let (elem_domain, _) = e.domain_of()?.as_matrix()?;

730

20

    elem_domain.as_ref().as_int()?;

731

20

    Some(elem_domain)

732

20

733

734

// Returns none if unbounded

735

3862606

fn range_vec_bounds_i32(ranges: &Vec<Range<i32>>) -> Option<(i32, i32)> {

736

3862606

    let mut min = i32::MAX;

737

3862606

    let mut max = i32::MIN;

738

3881822

    for r in ranges {

739

3881822

        match r {

740

1387650

            Range::Single(i) => {

741

1387650

                if *i < min {

742

1368434

                    min = *i;

743

1368434

744

1387650

                if *i > max {

745

1387650

                    max = *i;

746

1387650

747

748

2494172

            Range::Bounded(i, j) => {

749

2494172

                if *i < min {

750

2494172

                    min = *i;

751

2494172

752

2494172

                if *j > max {

753

2494172

                    max = *j;

754

2494172

755

756

            Range::UnboundedR(_) | Range::UnboundedL(_) | Range::Unbounded => return None,

757

758

759

3862606

    Some((min, max))

760

3862606

761

762

impl Expression {

763

    /// Returns the possible values of the expression, recursing to leaf expressions

764

9402452

    pub fn domain_of(&self) -> Option<DomainPtr> {

765

9402452

        match self {

766

112

            Expression::Union(_, a, b) => Some(Domain::set(

767

112

                SetAttr::<IntVal>::default(),

768

112

                a.domain_of()?.union(&b.domain_of()?).ok()?,

769

)),

770

100

            Expression::Intersect(_, a, b) => Some(Domain::set(

771

100

                SetAttr::<IntVal>::default(),

772

100

                a.domain_of()?.intersect(&b.domain_of()?).ok()?,

773

)),

774

            Expression::In(_, _, _) => Some(Domain::bool()),

775

            Expression::Supset(_, _, _) => Some(Domain::bool()),

776

            Expression::SupsetEq(_, _, _) => Some(Domain::bool()),

777

            Expression::Subset(_, _, _) => Some(Domain::bool()),

778

12

            Expression::SubsetEq(_, _, _) => Some(Domain::bool()),

779

242420

            Expression::AbstractLiteral(_, abslit) => abslit.domain_of(),

780

            Expression::DominanceRelation(_, _) => Some(Domain::bool()),

781

            Expression::FromSolution(_, expr) => Some(expr.domain_of()),

782

144

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

783

52

            Expression::Comprehension(_, comprehension) => comprehension.domain_of(),

784

            Expression::AbstractComprehension(_, comprehension) => comprehension.domain_of(),

785

5760

            Expression::RecordField(_, rec, field_name) => {

786

5760

                let rec_ents = rec.domain_of()?.as_record()?;

787

                for ent in rec_ents {

788

                    if ent.name.eq(field_name) {

789

                        return Some(ent.value);

790

791

792

                None

793

794

731348

            Expression::UnsafeIndex(_, matrix, index) | Expression::SafeIndex(_, matrix, index) => {

795

752664

                let dom = matrix.domain_of()?;

796

752664

                if let Some((elem_domain, _)) = dom.as_matrix() {

797

752664

                    return Some(elem_domain);

798

799

800

                // may actually use the value in the future

801

                #[allow(clippy::redundant_pattern_matching)]

802

                if let Some(_) = dom.as_tuple() {

803

                    // TODO: We can implement proper indexing for tuples

804

                    return None;

805

806

807

                if let Some(doms) = dom.as_variant().or(dom.as_record()) {

808

                    let index_expr = index.first()?;

809

                    return match index_expr {

810

                        Expression::Atomic(_, atom) => {

811

                            let decl = atom.clone().into_declaration();

812

                            for inner_dom in doms {

813

                                if *decl.name() == inner_dom.name {

814

                                    return Some(inner_dom.value);

815

816

817

                            None

818

819

                        _ => None,

820

};

821

822

823

                bug!(

824

                    "subject of an index operation should support indexing, but got {matrix}: {dom}"

825

826

827

            Expression::UnsafeSlice(_, matrix, indices)

828

480

            | Expression::SafeSlice(_, matrix, indices) => {

829

480

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

830

831

480

                let dom = matrix.domain_of()?;

832

480

                let Some((elem_domain, index_domains)) = dom.as_matrix() else {

833

                    bug!("subject of an index operation should be a matrix");

834

};

835

836

480

                match sliced_dimension {

837

480

                    Some(dimension) => Some(Domain::matrix(

838

480

                        elem_domain,

839

480

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

840

480

)),

841

842

                    // same as index

843

                    None => Some(elem_domain),

844

845

846

            Expression::InDomain(_, _, _) => Some(Domain::bool()),

847

6067797

            Expression::Atomic(_, atom) => Some(atom.domain_of()),

848

1233279

            Expression::Sum(_, e) => {

849

5859972

                bounded_i32_domain_for_matrix_literal_monotonic(e, |x, y| Some(x + y))

850

851

591488

            Expression::Product(_, e) => {

852

2321264

                bounded_i32_domain_for_matrix_literal_monotonic(e, |x, y| Some(x * y))

853

854

24960

            Expression::Min(_, e) => bounded_i32_domain_for_matrix_literal_monotonic(e, |x, y| {

855

24960

                Some(if x < y { x } else { y })

856

24960

})

857

4240

            .or_else(|| matrix_element_domain(e)),

858

16340

            Expression::Max(_, e) => bounded_i32_domain_for_matrix_literal_monotonic(e, |x, y| {

859

16320

                Some(if x > y { x } else { y })

860

16320

})

861

3220

            .or_else(|| matrix_element_domain(e)),

862

2120

            Expression::UnsafeDiv(_, a, b) => a

863

2120

                .domain_of()?

864

2120

                .resolve()

865

2120

                .ok()?

866

2120

                .apply_i32(

867

                    // rust integer division is truncating; however, we want to always round down,

868

                    // including for negative numbers.

869

56800

                    |x, y| {

870

56800

                        if y != 0 {

871

49720

                            Some((x as f32 / y as f32).floor() as i32)

872

                        } else {

873

7080

                            None

874

875

56800

},

876

2120

                    b.domain_of()?.resolve().ok()?.as_ref(),

877

878

2120

                .map(DomainPtr::from)

879

2120

                .ok(),

880

21720

            Expression::SafeDiv(_, a, b) => {

881

                // rust integer division is truncating; however, we want to always round down

882

                // including for negative numbers.

883

21720

                let domain = a

884

21720

                    .domain_of()?

885

21720

                    .resolve()

886

21720

                    .ok()?

887

21720

                    .apply_i32(

888

897680

                        |x, y| {

889

897680

                            if y != 0 {

890

780040

                                Some((x as f32 / y as f32).floor() as i32)

891

                            } else {

892

117640

                                None

893

894

897680

},

895

21720

                        b.domain_of()?.resolve().ok()?.as_ref(),

896

897

                    .unwrap_or_else(|err| bug!("Got {err} when computing domain of {self}"));

898

899

21720

                if let GroundDomain::Int(ranges) = domain {

900

21720

                    let mut ranges = ranges;

901

21720

                    ranges.push(Range::Single(0));

902

21720

                    Some(Domain::int(ranges))

903

                } else {

904

                    bug!("Domain of {self} was not integer")

905

906

907

800

            Expression::UnsafeMod(_, a, b) => a

908

800

                .domain_of()?

909

800

                .resolve()

910

800

                .ok()?

911

800

                .apply_i32(

912

12040

                    |x, y| if y != 0 { Some(x % y) } else { None },

913

800

                    b.domain_of()?.resolve().ok()?.as_ref(),

914

915

800

                .map(DomainPtr::from)

916

800

                .ok(),

917

6960

            Expression::SafeMod(_, a, b) => {

918

6960

                let domain = a

919

6960

                    .domain_of()?

920

6960

                    .resolve()

921

6960

                    .ok()?

922

6960

                    .apply_i32(

923

250320

                        |x, y| if y != 0 { Some(x % y) } else { None },

924

6960

                        b.domain_of()?.resolve().ok()?.as_ref(),

925

926

                    .unwrap_or_else(|err| bug!("Got {err} when computing domain of {self}"));

927

928

6960

                if let GroundDomain::Int(ranges) = domain {

929

6960

                    let mut ranges = ranges;

930

6960

                    ranges.push(Range::Single(0));

931

6960

                    Some(Domain::int(ranges))

932

                } else {

933

                    bug!("Domain of {self} was not integer")

934

935

936

5380

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

937

5380

                .domain_of()?

938

5380

                .resolve()

939

5380

                .ok()?

940

5380

                .apply_i32(

941

162920

                    |x, y| {

942

162920

                        if (x != 0 || y != 0) && y >= 0 {

943

147720

                            Some(x.pow(y as u32))

944

                        } else {

945

15200

                            None

946

947

162920

},

948

5380

                    b.domain_of()?.resolve().ok()?.as_ref(),

949

950

5380

                .map(DomainPtr::from)

951

5380

                .ok(),

952

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

953

320

            Expression::Bubble(_, inner, _) => inner.domain_of(),

954

            Expression::AuxDeclaration(_, _, _) => Some(Domain::bool()),

955

31432

            Expression::And(_, _) => Some(Domain::bool()),

956

400

            Expression::Not(_, _) => Some(Domain::bool()),

957

320

            Expression::Or(_, _) => Some(Domain::bool()),

958

4416

            Expression::Imply(_, _, _) => Some(Domain::bool()),

959

            Expression::Iff(_, _, _) => Some(Domain::bool()),

960

16236

            Expression::Eq(_, _, _) => Some(Domain::bool()),

961

            Expression::Neq(_, _, _) => Some(Domain::bool()),

962

            Expression::Geq(_, _, _) => Some(Domain::bool()),

963

1720

            Expression::Leq(_, _, _) => Some(Domain::bool()),

964

84

            Expression::Gt(_, _, _) => Some(Domain::bool()),

965

4

            Expression::Lt(_, _, _) => Some(Domain::bool()),

966

            Expression::Factorial(_, _) => None, // not implemented

967

            Expression::FlatAbsEq(_, _, _) => Some(Domain::bool()),

968

80

            Expression::FlatSumGeq(_, _, _) => Some(Domain::bool()),

969

            Expression::FlatSumLeq(_, _, _) => Some(Domain::bool()),

970

            Expression::MinionDivEqUndefZero(_, _, _, _) => Some(Domain::bool()),

971

            Expression::MinionModuloEqUndefZero(_, _, _, _) => Some(Domain::bool()),

972

360

            Expression::FlatIneq(_, _, _, _) => Some(Domain::bool()),

973

808

            Expression::Flatten(_, n, m) => {

974

808

                if let Some(expr) = n {

975

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

976

                        // TODO: handle flatten with depth argument

977

                        return None;

978

979

                } else {

980

                    // TODO: currently only works for matrices

981

808

                    let dom = m.domain_of()?.resolve().ok()?;

982

800

                    let (val_dom, idx_doms) = match dom.as_ref() {

983

800

                        GroundDomain::Matrix(val, idx) => (val, idx),

984

                        _ => return None,

985

};

986

800

                    let num_elems = matrix::num_elements(idx_doms).ok()? as i32;

987

988

800

                    let new_index_domain = Domain::int(vec![Range::Bounded(1, num_elems)]);

989

800

                    return Some(Domain::matrix(

990

800

                        val_dom.clone().into(),

991

800

                        vec![new_index_domain],

992

800

));

993

994

                None

995

996

            Expression::AllDiff(_, _) => Some(Domain::bool()),

997

            Expression::Table(_, _, _) => Some(Domain::bool()),

998

            Expression::NegativeTable(_, _, _) => Some(Domain::bool()),

999

            Expression::FlatWatchedLiteral(_, _, _) => Some(Domain::bool()),

1000

            Expression::MinionReify(_, _, _) => Some(Domain::bool()),

1001

4820

            Expression::MinionReifyImply(_, _, _) => Some(Domain::bool()),

1002

            Expression::MinionWInIntervalSet(_, _, _) => Some(Domain::bool()),

1003

            Expression::MinionWInSet(_, _, _) => Some(Domain::bool()),

1004

            Expression::MinionElementOne(_, _, _, _) => Some(Domain::bool()),

1005

7532

            Expression::Neg(_, x) => {

1006

7532

                let dom = x.domain_of()?;

1007

7532

                let mut ranges = dom.as_int()?;

1008

1009

4772

                ranges = ranges

1010

4772

                    .into_iter()

1011

4772

                    .map(|r| match r {

1012

840

                        Range::Single(x) => Range::Single(-x),

1013

3932

                        Range::Bounded(x, y) => Range::Bounded(-y, -x),

1014

                        Range::UnboundedR(i) => Range::UnboundedL(-i),

1015

                        Range::UnboundedL(i) => Range::UnboundedR(-i),

1016

                        Range::Unbounded => Range::Unbounded,

1017

4772

})

1018

4772

                    .collect();

1019

1020

4772

                Some(Domain::int(ranges))

1021

1022

376348

            Expression::Minus(_, a, b) => {

1023

376348

                let a_resolved = a.domain_of()?.resolve().ok()?;

1024

376348

                let b_resolved = b.domain_of()?.resolve().ok()?;

1025

1026

376344

                if matches!(a_resolved.as_ref(), GroundDomain::Int(_))

1027

376344

                    && matches!(b_resolved.as_ref(), GroundDomain::Int(_))

1028

1029

376344

                    a_resolved

1030

1206220

                        .apply_i32(|x, y| Some(x - y), b_resolved.as_ref())

1031

376344

                        .map(DomainPtr::from)

1032

376344

                        .ok()

1033

                } else if matches!(a_resolved.as_ref(), GroundDomain::Set(_, _))

1034

                    && matches!(b_resolved.as_ref(), GroundDomain::Set(_, _))

1035

1036

                    Some(DomainPtr::from(a_resolved))

1037

                } else {

1038

                    None

1039

1040

1041

            Expression::FlatAllDiff(_, _) => Some(Domain::bool()),

1042

            Expression::FlatMinusEq(_, _, _) => Some(Domain::bool()),

1043

            Expression::FlatProductEq(_, _, _, _) => Some(Domain::bool()),

1044

            Expression::FlatWeightedSumLeq(_, _, _, _) => Some(Domain::bool()),

1045

            Expression::FlatWeightedSumGeq(_, _, _, _) => Some(Domain::bool()),

1046

5640

            Expression::Abs(_, a) => a

1047

5640

                .domain_of()?

1048

5640

                .resolve()

1049

5640

                .ok()?

1050

5640

                .apply_i32(

1051

953360

                    |a, _| Some(a.abs()),

1052

5640

                    a.domain_of()?.resolve().ok()?.as_ref(),

1053

1054

5640

                .map(DomainPtr::from)

1055

5640

                .ok(),

1056

            Expression::MinionPow(_, _, _, _) => Some(Domain::bool()),

1057

6088

            Expression::ToInt(_, _) => Some(Domain::int(vec![Range::Bounded(0, 1)])),

1058

3840

            Expression::SATInt(_, _, _, (low, high)) => {

1059

3840

                Some(Domain::int_ground(vec![Range::Bounded(*low, *high)]))

1060

1061

            Expression::PairwiseSum(_, a, b) => a

1062

                .domain_of()?

1063

                .resolve()

1064

                .ok()?

1065

                .apply_i32(|a, b| Some(a + b), b.domain_of()?.resolve().ok()?.as_ref())

1066

                .map(DomainPtr::from)

1067

                .ok(),

1068

            Expression::PairwiseProduct(_, a, b) => a

1069

                .domain_of()?

1070

                .resolve()

1071

                .ok()?

1072

                .apply_i32(|a, b| Some(a * b), b.domain_of()?.resolve().ok()?.as_ref())

1073

                .map(DomainPtr::from)

1074

                .ok(),

1075

32

            Expression::Defined(_, function) => {

1076

32

                let (attrs, domain, codomain) = function.domain_of()?.as_function()?;

1077

32

                let size = Self::function_elements_size(attrs, &domain, &codomain);

1078

32

                if let Some(size) = size {

1079

28

                    Some(Domain::set(SetAttr::new(size), domain))

1080

                } else {

1081

4

                    Some(Domain::empty(ReturnType::Set(Box::new(

1082

4

                        domain.return_type(),

1083

4

                    ))))

1084

1085

1086

44

            Expression::Range(_, function) => {

1087

44

                let (attrs, domain, codomain) = function.domain_of()?.as_function()?;

1088

44

                let jectivity = attrs.resolve().ok()?.jectivity;

1089

1090

44

                let size_size = attrs.resolve().ok()?.size;

1091

44

                let size_size = match size_size {

1092

20

                    Range::Unbounded => Range::UnboundedR(0),

1093

                    // If lower bound we can guarantee one mapping (unless size = 0)

1094

8

                    Range::Single(x) => match jectivity {

1095

4

                        JectivityAttr::Injective | JectivityAttr::Surjective => Range::Single(x),

1096

4

                        _ => Range::Bounded(Ord::min(1, x), x),

1097

},

1098

                    // Upper bound guarantees the same upper bound

1099

4

                    Range::UnboundedL(x) => Range::Bounded(0, x),

1100

                    // If not bounded by 0 can guarantee min 1

1101

8

                    Range::UnboundedR(x) => match jectivity {

1102

                        JectivityAttr::Injective | JectivityAttr::Surjective => {

1103

4

                            Range::UnboundedR(x)

1104

1105

4

                        _ => Range::UnboundedR(Ord::min(1, x)),

1106

},

1107

4

                    Range::Bounded(x, y) => Range::Bounded(Ord::min(1, x), y),

1108

};

1109

1110

                // Gets the size imposed by the partiality and jectivity attributes

1111

44

                let partiality = attrs.resolve().ok()?.partiality;

1112

44

                let codomain_length = codomain.length_signed();

1113

44

                let attr_size = match jectivity {

1114

                    // Bijective and surjective functions must have every element in the codomain mapped to

1115

12

                    JectivityAttr::Bijective | JectivityAttr::Surjective => match codomain_length {

1116

12

                        Ok(co_len) => Some(Range::Single(co_len)),

1117

                        Err(_) => None,

1118

},

1119

                    JectivityAttr::Injective => {

1120

16

                        let domain_length = domain.length_signed();

1121

16

                        match domain_length {

1122

16

                            Ok(len) => match codomain_length {

1123

16

                                Ok(co_len) => match partiality {

1124

                                    // When its injective we can guarantee 1 to 1, so the maximum domain length is a single bound

1125

                                    PartialityAttr::Total => {

1126

4

                                        Some(Range::Single(Ord::min(len, co_len)))

1127

1128

                                    PartialityAttr::Partial => {

1129

12

                                        Some(Range::Bounded(0, Ord::min(len, co_len)))

1130

1131

},

1132

                                Err(_) => None,

1133

},

1134

                            Err(_) => None,

1135

1136

1137

                    JectivityAttr::None => {

1138

16

                        let domain_length = domain.length_signed();

1139

16

                        match domain_length {

1140

                            // This is the general case, where we know there cannot be more codomain elements mapped to that domain elements

1141

16

                            Ok(len) => Some(Range::Bounded(0, len)),

1142

                            Err(_) => None,

1143

1144

1145

};

1146

1147

44

                let size = match attr_size {

1148

44

                    Some(attr_size) => {

1149

44

                        let unsafe_range = Range::minimal(&[size_size, attr_size]);

1150

44

                        match unsafe_range {

1151

44

                            Ok(range) => range,

1152

                            Err(_) => {

1153

                                return Some(Domain::empty(ReturnType::Set(Box::new(

1154

                                    domain.return_type(),

1155

                                ))));

1156

1157

1158

1159

                    None => size_size,

1160

};

1161

44

                Some(Domain::set(SetAttr::new(size), codomain))

1162

1163

            Expression::Image(_, function, _) => get_function_codomain(function),

1164

            Expression::ImageSet(_, function, _) => {

1165

                let codomain = get_function_codomain(function);

1166

                // An imageSet is the converted to a set, and can be empty

1167

                codomain.map(|inner_dom| Domain::set(SetAttr::new(Range::Bounded(0, 1)), inner_dom))

1168

1169

44

            Expression::PreImage(_, function, _) => {

1170

44

                let (attrs, domain, codomain) = function.domain_of()?.as_function()?;

1171

1172

44

                let size_size = attrs.resolve().ok()?.size;

1173

44

                let size_size = match size_size {

1174

                    // Our only guarantee is an upper bound is the same

1175

20

                    Range::Unbounded => Range::UnboundedR(0),

1176

8

                    Range::Single(x) => Range::Bounded(0, x),

1177

4

                    Range::UnboundedL(x) => Range::Bounded(0, x),

1178

8

                    Range::UnboundedR(_) => Range::UnboundedR(0),

1179

4

                    Range::Bounded(_, y) => Range::Bounded(0, y),

1180

};

1181

1182

44

                let jectivity = attrs.resolve().ok()?.jectivity;

1183

44

                let codomain_length = codomain.length_signed();

1184

44

                let attr_size = match jectivity {

1185

                    // When there is 1-to-1 mapping we can guarantee no more than 1 occurrence

1186

4

                    JectivityAttr::Bijective => Some(Range::Single(1)),

1187

16

                    JectivityAttr::Injective => match size_size {

1188

4

                        Range::Single(x) | Range::UnboundedL(x) | Range::Bounded(x, _) => {

1189

4

                            match codomain_length {

1190

4

                                Ok(co_len) => {

1191

4

                                    if x >= co_len {

1192

                                        Some(Range::Single(1))

1193

                                    } else {

1194

4

                                        Some(Range::Bounded(0, 1))

1195

1196

1197

                                Err(_) => Some(Range::Bounded(0, 1)),

1198

1199

1200

12

                        _ => Some(Range::Bounded(0, 1)),

1201

},

1202

                    JectivityAttr::Surjective => {

1203

8

                        let domain_length = domain.length_signed();

1204

8

                        match domain_length {

1205

8

                            Ok(len) => match codomain_length {

1206

                                // We know the element is mapped but not how many times

1207

                                // Every element must be mapped so it cannot be every element of domain

1208

8

                                Ok(co_len) => match size_size {

1209

4

                                    Range::Bounded(_, x)

1210

                                    | Range::UnboundedL(x)

1211

4

                                    | Range::Single(x) => Some(Range::Bounded(

1212

4

1,

1213

4

                                        Ord::max(Ord::min(len, x) - co_len + 1, 0),

1214

4

)),

1215

4

                                    _ => Some(Range::Bounded(1, Ord::max(len - co_len + 1, 0))),

1216

},

1217

                                Err(_) => Some(Range::UnboundedR(1)),

1218

},

1219

                            Err(_) => Some(Range::UnboundedR(1)),

1220

1221

1222

                    JectivityAttr::None => {

1223

16

                        let domain_length = domain.length_signed();

1224

16

                        match domain_length {

1225

16

                            Ok(len) => Some(Range::Bounded(0, len)),

1226

                            Err(_) => Some(Range::UnboundedR(0)),

1227

1228

1229

};

1230

1231

44

                let size = match attr_size {

1232

44

                    Some(attr_size) => {

1233

44

                        let unsafe_range = Range::minimal(&[size_size, attr_size]);

1234

44

                        match unsafe_range {

1235

44

                            Ok(range) => range,

1236

                            Err(_) => {

1237

                                return Some(Domain::empty(ReturnType::Set(Box::new(

1238

                                    domain.return_type(),

1239

                                ))));

1240

1241

1242

1243

                    None => size_size,

1244

};

1245

44

                Some(Domain::set(SetAttr::new(size), domain))

1246

1247

16

            Expression::Restrict(_, function, new_domain) => {

1248

16

                let mut domain = function.domain_of()?;

1249

16

                let (attrs_mut, dom, codom_mut) = domain.as_function_mut()?;

1250

1251

                // Stops other references being mutable

1252

16

                let attrs: &FuncAttr<IntVal> = attrs_mut;

1253

16

                let codom: &Moo<Domain> = codom_mut;

1254

1255

                // Gets the minimal range between the old domain and new domain

1256

16

                let mut new_dom = new_domain.domain_of()?;

1257

                // If domains cannot be resolved we just stick to the restricted one

1258

16

                if let Some(new_rng) = new_dom.as_int_ground_mut()

1259

16

                    && let Some(old_rng) = dom.as_int_ground_mut()

1260

1261

16

                    new_rng.append(old_rng);

1262

16

                    if let Ok(rng) = Range::minimal(new_rng) {

1263

16

                        let ranges = vec![rng];

1264

16

                        new_dom = Domain::int(ranges);

1265

16

1266

1267

16

                let attr_size = attrs.resolve().ok()?.size;

1268

16

                let new_size = match new_dom.length_signed() {

1269

                    // Combines current size attributes with length of new domain

1270

16

                    Ok(len) => match Range::minimal(&[attr_size, Range::Bounded(0, len)]) {

1271

12

                        Ok(size) => size,

1272

                        Err(_) => {

1273

                            // Means the restriction is impossible

1274

4

                            return Some(Domain::empty(ReturnType::Function(

1275

4

                                Box::new(new_dom.return_type()),

1276

4

                                Box::new(codom.return_type()),

1277

4

                            )));

1278

1279

},

1280

                    Err(_) => attr_size,

1281

};

1282

12

                let jectivity = attrs.jectivity.clone();

1283

12

                let partiality = attrs.partiality.clone();

1284

12

                let new_attrs = FuncAttr {

1285

12

                    size: new_size,

1286

12

                    jectivity,

1287

12

                    partiality,

1288

12

};

1289

12

                Some(Domain::function(new_attrs, new_dom, codom.clone()))

1290

1291

            Expression::Subsequence(_, _, _) => Some(Domain::bool()),

1292

            Expression::Substring(_, _, _) => Some(Domain::bool()),

1293

            Expression::Inverse(..) => Some(Domain::bool()),

1294

            Expression::LexLt(..) => Some(Domain::bool()),

1295

3080

            Expression::LexLeq(..) => Some(Domain::bool()),

1296

            Expression::LexGt(..) => Some(Domain::bool()),

1297

            Expression::LexGeq(..) => Some(Domain::bool()),

1298

            Expression::FlatLexLt(..) => Some(Domain::bool()),

1299

            Expression::FlatLexLeq(..) => Some(Domain::bool()),

1300

            Expression::Active(..) => Some(Domain::bool()),

1301

            Expression::ToSet(_, other) => {

1302

                if let Some((attrs, dom, codom)) = other.domain_of()?.as_function() {

1303

                    let set_attrs = SetAttr { size: attrs.size };

1304

                    Some(Domain::set(set_attrs, Domain::tuple(vec![dom, codom])))

1305

                } else if let Some((attrs, doms)) = other.domain_of()?.as_relation() {

1306

                    let set_attrs = SetAttr { size: attrs.size };

1307

                    Some(Domain::set(set_attrs, Domain::tuple(doms)))

1308

                } else if let Some((attrs, dom)) = other.domain_of()?.as_mset() {

1309

                    let set_attrs = SetAttr { size: attrs.size };

1310

                    Some(Domain::set(set_attrs, dom))

1311

                } else if let Some((dom, dimensions)) = other.domain_of()?.as_matrix() {

1312

                    // We combine all matrix domains into a tuple

1313

                    let mut doms = vec![];

1314

                    for _ in dimensions {

1315

                        doms.push(dom.clone());

1316

1317

                    let doms_sizes: Result<Vec<i32>, _> =

1318

                        doms.iter().map(|x| x.length_signed()).collect();

1319

                    let attr = match doms_sizes {

1320

                        Ok(vals) => {

1321

                            if let Some(&size) = vals.iter().min() {

1322

                                SetAttr::new(Range::Single(size))

1323

                            } else {

1324

                                SetAttr::<i32>::default()

1325

1326

1327

                        // We do not know the ground dimensions yet so default is chosen

1328

                        Err(_) => SetAttr::<i32>::default(),

1329

};

1330

                    Some(Domain::set(attr, Domain::tuple(doms)))

1331

                } else {

1332

                    bug!(

1333

                        "Domain of {self} needed to be a function, relation, mset, or matrix for ToSet"

1334

1335

1336

1337

            Expression::ToMSet(_, other) => {

1338

                if let Some((attrs, dom, codom)) = other.domain_of()?.as_function() {

1339

                    let set_attrs = MSetAttr {

1340

                        size: attrs.size,

1341

                        occurrence: Range::Single(IntVal::Const(1)),

1342

};

1343

                    Some(Domain::mset(set_attrs, Domain::tuple(vec![dom, codom])))

1344

                } else if let Some((attrs, doms)) = other.domain_of()?.as_relation() {

1345

                    let set_attrs = MSetAttr {

1346

                        size: attrs.size,

1347

                        occurrence: Range::Single(IntVal::Const(1)),

1348

};

1349

                    Some(Domain::mset(set_attrs, Domain::tuple(doms)))

1350

                } else if let Some((attrs, dom)) = other.domain_of()?.as_set() {

1351

                    let set_attrs = MSetAttr {

1352

                        size: attrs.size,

1353

                        occurrence: Range::Single(IntVal::Const(1)),

1354

};

1355

                    Some(Domain::mset(set_attrs, dom))

1356

                } else {

1357

                    bug!("Domain of {self} needed to be a function, relation, or set for ToMSet")

1358

1359

1360

            Expression::ToRelation(_, function) => {

1361

                let (attrs, domain, codomain) = function.domain_of()?.as_function()?;

1362

                // Function attributes apply to the relation

1363

                let rel_attrs = RelAttr {

1364

                    size: attrs.size,

1365

                    binary: vec![],

1366

};

1367

                Some(Domain::relation(rel_attrs, vec![domain, codomain]))

1368

1369

4

            Expression::RelationProj(_, relation, projections) => {

1370

4

                let (_, domains) = relation.domain_of()?.as_relation()?;

1371

4

                let new_doms = domains

1372

4

                    .iter()

1373

4

                    .zip(projections.iter())

1374

12

                    .filter_map(|(domain, included)| {

1375

12

                        if included.is_none() {

1376

                            // The domains corresponding to projections which are None remain in the relation

1377

8

                            Some(domain.clone())

1378

                        } else {

1379

4

                            None

1380

1381

12

})

1382

4

                    .collect();

1383

4

                Some(Domain::relation(RelAttr::<IntVal>::default(), new_doms))

1384

1385

            Expression::Apart(_, _, _) => Some(Domain::bool()),

1386

            Expression::Together(_, _, _) => Some(Domain::bool()),

1387

8

            Expression::Participants(_, p) => {

1388

                // Every single element of the domain _must_ be in the set, so fixed size on that.

1389

8

                let (attr, inner) = p.domain_of()?.as_partition()?;

1390

8

                let len = inner.length_signed().ok()?;

1391

1392

8

                let p_parts = attr.resolve().ok()?.num_parts;

1393

8

                let p_card = attr.resolve().ok()?.part_len;

1394

1395

                // if

1396

8

                match (p_parts.low(), p_parts.high(), p_card.low(), p_card.high()) {

1397

4

                    (Some(p), Some(q), Some(r), Some(s)) => {

1398

4

                        let lo = p * r;

1399

4

                        let hi = q * s;

1400

4

                        if len < lo || len > hi {

1401

4

                            return Some(Domain::empty(ReturnType::Set(Box::new(

1402

4

                                inner.return_type(),

1403

4

                            ))));

1404

1405

1406

1407

                    (None, Some(q), None, Some(s)) => {

1408

                        let hi = q * s;

1409

                        if len > hi {

1410

                            return Some(Domain::empty(ReturnType::Set(Box::new(

1411

                                inner.return_type(),

1412

                            ))));

1413

1414

1415

1416

                    (Some(p), None, Some(r), None) => {

1417

                        let lo = p * r;

1418

                        if len < lo {

1419

                            return Some(Domain::empty(ReturnType::Set(Box::new(

1420

                                inner.return_type(),

1421

                            ))));

1422

1423

1424

1425

4

                    _ => {}

1426

1427

1428

4

                Some(Domain::set(

1429

4

                    SetAttr::new_size(len),

1430

4

                    Domain::int(inner.as_int()?),

1431

))

1432

1433

4

            Expression::Party(_, _, p) => {

1434

                // Will pick a part, so set will share same attrs

1435

4

                let (attr, inner) = p.domain_of()?.as_partition()?;

1436

1437

4

                Some(Domain::set(SetAttr::new(attr.part_len), inner))

1438

1439

8

            Expression::Parts(_, p) => {

1440

8

                let (attr, inner) = p.domain_of()?.as_partition()?;

1441

1442

8

                Some(Domain::set(

1443

8

                    SetAttr::new(attr.num_parts.clone()),

1444

8

                    Domain::set(SetAttr::new(attr.part_len), inner),

1445

8

))

1446

1447

16

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

1448

16

                let domain = collection.domain_of()?;

1449

16

                if let Some((_, dimensions)) = domain.as_matrix() {

1450

                    let doms_ground: Result<Vec<i32>, _> =

1451

                        dimensions.iter().map(|x| x.length_signed()).collect();

1452

                    if let Ok(doms_ground) = doms_ground {

1453

                        let size: Range<i32> = Range::Single(doms_ground.iter().product());

1454

                        Some(Domain::int(vec![size]))

1455

                    } else {

1456

                        Some(Domain::int(vec![Range::<i32>::Unbounded]))

1457

1458

16

                } else if let Some((attr, dom)) = domain.as_set() {

1459

4

                    let attr_size = attr.resolve().ok()?.size;

1460

4

                    if let Ok(length) = dom.length_signed() {

1461

4

                        let unsafe_range = Range::minimal(&[attr_size, Range::Bounded(0, length)]);

1462

4

                        return match unsafe_range {

1463

4

                            Ok(range) => Some(Domain::int(vec![range])),

1464

                            Err(_) => None,

1465

};

1466

1467

                    // If the domain is not known we just need to go off of attributes

1468

                    Some(Domain::int(vec![attr_size]))

1469

12

                } else if let Some((attrs, dom)) = domain.as_mset() {

1470

4

                    let attrs_gd = attrs.resolve().ok()?;

1471

                    // Gets maximum value of the occurrence

1472

4

                    let attr_occ = match attrs_gd.occurrence {

1473

                        Range::Single(x) => Some(x),

1474

                        Range::Unbounded | Range::UnboundedR(_) => None,

1475

                        Range::Bounded(_, x) => Some(x),

1476

4

                        Range::UnboundedL(x) => Some(x),

1477

};

1478

4

                    if let Some(occ) = attr_occ {

1479

4

                        if let Ok(length) = dom.length_signed() {

1480

4

                            let unsafe_range =

1481

4

                                Range::minimal(&[attrs_gd.size, Range::Bounded(0, length * occ)]);

1482

4

                            match unsafe_range {

1483

4

                                Ok(range) => Some(Domain::int(vec![range])),

1484

                                Err(_) => None,

1485

1486

                        } else {

1487

                            // If the domain is not known we just need to go off of attributes

1488

                            Some(Domain::int(vec![attrs_gd.size]))

1489

1490

                    } else {

1491

                        // If no occurrence is provided then it must have bounded size

1492

                        Some(Domain::int(vec![attrs_gd.size]))

1493

1494

8

                } else if let Some((attrs, doms)) = domain.as_relation() {

1495

                    // TODO: Further inference may be possible using the binary attributes

1496

1497

4

                    let attrs_gd = attrs.resolve().ok()?;

1498

                    // See if all domains are ground

1499

4

                    let doms_sizes: Result<Vec<i32>, _> =

1500

12

                        doms.iter().map(|x| x.length_signed()).collect();

1501

4

                    if let Ok(doms_sizes) = doms_sizes {

1502

4

                        let length = Range::Bounded(0, doms_sizes.iter().product());

1503

                        // Combine the attributes and the domain possibilities

1504

4

                        let unsafe_range = Range::minimal(&[attrs_gd.size, length]);

1505

4

                        return match unsafe_range {

1506

4

                            Ok(range) => Some(Domain::int(vec![range])),

1507

                            Err(_) => None,

1508

};

1509

1510

                    // If the domain is not known we just need to go off of attributes

1511

                    Some(Domain::int(vec![attrs_gd.size]))

1512

4

                } else if let Some((attrs, dom, codom)) = domain.as_function() {

1513

4

                    let size = Self::function_elements_size(attrs, &dom, &codom);

1514

4

                    size.map(|size| Domain::int(vec![size]))

1515

                } else {

1516

                    bug!(

1517

                        "Domain of {self} needed to be a matrix, set, mset, relation, or function for cardinality"

1518

1519

1520

1521

1522

9402452

1523

1524

    // Gets the number of domain elements mapped in a function. This is the cardinality and also the defined

1525

36

    fn function_elements_size(

1526

36

        attrs: FuncAttr<IntVal>,

1527

36

        domain: &DomainPtr,

1528

36

        codomain: &DomainPtr,

1529

36

    ) -> Option<Range> {

1530

36

        let attrs_gd = attrs.resolve().ok()?;

1531

36

        let domain_length = domain.length_signed();

1532

        // We can only infer if the domain is ground and the length is known

1533

36

        let attr_size = match domain_length {

1534

36

            Ok(len) => match attrs_gd.partiality {

1535

4

                PartialityAttr::Total => Some(Range::Single(len)),

1536

                PartialityAttr::Partial => {

1537

                    // When partial we also need the codomain to be ground and known

1538

32

                    let codomain_length = codomain.length_signed();

1539

32

                    match codomain_length {

1540

32

                        Ok(co_len) => match attrs_gd.jectivity {

1541

8

                            JectivityAttr::Bijective => Some(Range::Single(co_len)),

1542

8

                            JectivityAttr::Surjective => Some(Range::Bounded(co_len, len)),

1543

                            JectivityAttr::Injective => {

1544

12

                                Some(Range::Bounded(0, Ord::min(len, co_len)))

1545

1546

4

                            JectivityAttr::None => Some(Range::Bounded(0, len)),

1547

},

1548

                        Err(_) => None,

1549

1550

1551

},

1552

            Err(_) => None,

1553

};

1554

        // We combine the sizes:

1555

        // attrs_gd.size relates to size constraints imposed by the size attributes of the function

1556

        // attr_size relates to size constraints imposed by the jectivity and partiality attributes.

1557

        //       This uses inference from the domain and codomain lengths.

1558

        // If the attributes clash the function is unsolveable, and an empty domain is returned

1559

36

        match attr_size {

1560

36

            Some(attr_size) => {

1561

36

                let unsafe_range = Range::minimal(&[attrs_gd.size, attr_size]);

1562

36

                unsafe_range.ok()

1563

1564

            None => Some(attrs_gd.size),

1565

1566

36

1567

1568

    /// Returns a reference to this expression's metadata without cloning.

1569

    pub fn meta_ref(&self) -> &Metadata {

1570

        macro_rules! match_meta_ref {

1571

            ($($variant:ident),* $(,)?) => {

1572

                match self {

1573

                    $(Expression::$variant(meta, ..) => meta,)*

1574

1575

};

1576

1577

        match_meta_ref!(

1578

            AbstractLiteral,

1579

            Root,

1580

            Bubble,

1581

            Comprehension,

1582

            AbstractComprehension,

1583

            DominanceRelation,

1584

            FromSolution,

1585

            Metavar,

1586

            Atomic,

1587

            RecordField,

1588

            UnsafeIndex,

1589

            SafeIndex,

1590

            UnsafeSlice,

1591

            SafeSlice,

1592

            InDomain,

1593

            ToInt,

1594

            Abs,

1595

            Sum,

1596

            Product,

1597

            Min,

1598

            Max,

1599

            Not,

1600

Or,

1601

            And,

1602

            Imply,

1603

            Iff,

1604

            Union,

1605

In,

1606

            Intersect,

1607

            Supset,

1608

            SupsetEq,

1609

            Subset,

1610

            SubsetEq,

1611

Eq,

1612

            Neq,

1613

            Geq,

1614

            Leq,

1615

Gt,

1616

Lt,

1617

            SafeDiv,

1618

            UnsafeDiv,

1619

            SafeMod,

1620

            UnsafeMod,

1621

            Apart,

1622

            Together,

1623

            Participants,

1624

            Party,

1625

            Parts,

1626

            Neg,

1627

            Defined,

1628

            Range,

1629

            UnsafePow,

1630

            SafePow,

1631

            Flatten,

1632

            AllDiff,

1633

            Minus,

1634

            Factorial,

1635

            FlatAbsEq,

1636

            FlatAllDiff,

1637

            FlatSumGeq,

1638

            FlatSumLeq,

1639

            FlatIneq,

1640

            FlatWatchedLiteral,

1641

            FlatWeightedSumLeq,

1642

            FlatWeightedSumGeq,

1643

            FlatMinusEq,

1644

            FlatProductEq,

1645

            MinionDivEqUndefZero,

1646

            MinionModuloEqUndefZero,

1647

            MinionPow,

1648

            MinionReify,

1649

            MinionReifyImply,

1650

            MinionWInIntervalSet,

1651

            MinionWInSet,

1652

            MinionElementOne,

1653

            AuxDeclaration,

1654

            SATInt,

1655

            PairwiseSum,

1656

            PairwiseProduct,

1657

            Image,

1658

            ImageSet,

1659

            PreImage,

1660

            Inverse,

1661

            Restrict,

1662

            LexLt,

1663

            LexLeq,

1664

            LexGt,

1665

            LexGeq,

1666

            FlatLexLt,

1667

            FlatLexLeq,

1668

            NegativeTable,

1669

            Table,

1670

            Active,

1671

            ToSet,

1672

            ToMSet,

1673

            ToRelation,

1674

            RelationProj,

1675

            Card,

1676

            Subsequence,

1677

            Substring,

1678

1679

1680

1681

    pub fn get_meta(&self) -> Metadata {

1682

        let metas: VecDeque<Metadata> = self.children_bi();

1683

        metas[0].clone()

1684

1685

1686

    pub fn set_meta(&self, meta: Metadata) {

1687

        self.transform_bi(&|_| meta.clone());

1688

1689

1690

    /// Checks whether this expression is safe.

1691

///

1692

    /// An expression is unsafe if can be undefined, or if any of its children can be undefined.

1693

///

1694

    /// Unsafe expressions are (typically) prefixed with Unsafe in our AST, and can be made

1695

    /// safe through the use of bubble rules.

1696

5369768

    pub fn is_safe(&self) -> bool {

1697

        // TODO: memoise in Metadata

1698

43226432

        for expr in self.universe() {

1699

43226432

            match expr {

1700

                Expression::UnsafeDiv(_, _, _)

1701

                | Expression::UnsafeMod(_, _, _)

1702

                | Expression::UnsafePow(_, _, _)

1703

                | Expression::UnsafeIndex(_, _, _)

1704

                | Expression::Bubble(_, _, _)

1705

                | Expression::UnsafeSlice(_, _, _) => {

1706

833008

                    return false;

1707

1708

42393424

                _ => {}

1709

1710

1711

4536760

        true

1712

5369768

1713

1714

    /// True if the expression is an associative and commutative operator

1715

14902372

    pub fn is_associative_commutative_operator(&self) -> bool {

1716

14902372

        TryInto::<ACOperatorKind>::try_into(self).is_ok()

1717

14902372

1718

1719

    /// True if the expression is a matrix literal.

1720

///

1721

    /// This is true for both forms of matrix literals: those with elements of type [`Literal`] and

1722

    /// [`Expression`].

1723

8280

    pub fn is_matrix_literal(&self) -> bool {

1724

        matches!(

1725

8280

            self,

1726

            Expression::AbstractLiteral(_, AbstractLiteral::Matrix(_, _))

1727

                | Expression::Atomic(

1728

_,

1729

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

1730

1731

1732

8280

1733

1734

    /// True iff self and other are both atomic and identical.

1735

///

1736

    /// This method is useful to cheaply check equivalence. Assuming CSE is enabled, any unifiable

1737

    /// expressions will be rewritten to a common variable. This is much cheaper than checking the

1738

    /// entire subtrees of `self` and `other`.

1739

2595632

    pub fn identical_atom_to(&self, other: &Expression) -> bool {

1740

2595632

        let atom1: Result<&Atom, _> = self.try_into();

1741

2595632

        let atom2: Result<&Atom, _> = other.try_into();

1742

1743

2595632

        if let (Ok(atom1), Ok(atom2)) = (atom1, atom2) {

1744

572992

            atom2 == atom1

1745

        } else {

1746

2022640

            false

1747

1748

2595632

1749

1750

    /// If the expression is a list, returns a *copied* vector of the inner expressions.

1751

///

1752

    /// A list is any a matrix with the domain `int(1..)`. This includes matrix literals without

1753

    /// any explicitly specified domain.

1754

9074624

    pub fn unwrap_list(&self) -> Option<Vec<Expression>> {

1755

7716296

        match self {

1756

7716296

            Expression::AbstractLiteral(_, matrix @ AbstractLiteral::Matrix(_, _)) => {

1757

7716296

                matrix.unwrap_list().cloned()

1758

1759

            Expression::Atomic(

1760

_,

1761

27748

                Atom::Literal(Literal::AbstractLiteral(matrix @ AbstractLiteral::Matrix(_, _))),

1762

27748

            ) => matrix.unwrap_list().map(|elems| {

1763

23568

                elems

1764

23568

                    .clone()

1765

23568

                    .into_iter()

1766

64376

                    .map(|x: Literal| Expression::Atomic(Metadata::new(), Atom::Literal(x)))

1767

23568

                    .collect_vec()

1768

23568

}),

1769

1330580

            _ => None,

1770

1771

9074624

1772

1773

    /// If the expression is a matrix, gets it elements and index domain.

1774

///

1775

    /// **Consider using the safer [`Expression::unwrap_list`] instead.**

1776

///

1777

    /// It is generally undefined to edit the length of a matrix unless it is a list (as defined by

1778

    /// [`Expression::unwrap_list`]). Users of this function should ensure that, if the matrix is

1779

    /// reconstructed, the index domain and the number of elements in the matrix remain the same.

1780

12329495

    pub fn unwrap_matrix_unchecked(self) -> Option<(Vec<Expression>, DomainPtr)> {

1781

8413239

        match self {

1782

8413239

            Expression::AbstractLiteral(_, AbstractLiteral::Matrix(elems, domain)) => {

1783

8413239

                Some((elems, domain))

1784

1785

            Expression::Atomic(

1786

_,

1787

457664

                Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Matrix(elems, domain))),

1788

            ) => Some((

1789

457664

                elems

1790

457664

                    .into_iter()

1791

1092024

                    .map(|x: Literal| Expression::Atomic(Metadata::new(), Atom::Literal(x)))

1792

457664

                    .collect_vec(),

1793

457664

                domain.into(),

1794

)),

1795

1796

3458592

            _ => None,

1797

1798

12329495

1799

1800

    /// For a Root expression, extends the inner vec with the given vec.

1801

///

1802

    /// # Panics

1803

    /// Panics if the expression is not Root.

1804

27940

    pub fn extend_root(self, exprs: Vec<Expression>) -> Expression {

1805

27940

        match self {

1806

27940

            Expression::Root(meta, mut children) => {

1807

27940

                children.extend(exprs);

1808

27940

                Expression::Root(meta, children)

1809

1810

            _ => panic!("extend_root called on a non-Root expression"),

1811

1812

27940

1813

1814

    /// Converts the expression to a literal, if possible.

1815

161060

    pub fn into_literal(self) -> Option<Literal> {

1816

151500

        match self {

1817

141172

            Expression::Atomic(_, Atom::Literal(lit)) => Some(lit),

1818

            Expression::AbstractLiteral(_, abslit) => {

1819

                Some(Literal::AbstractLiteral(abslit.into_literals()?))

1820

1821

6104

            Expression::Neg(_, e) => {

1822

6104

                let Literal::Int(i) = Moo::unwrap_or_clone(e).into_literal()? else {

1823

                    bug!("negated literal should be an int");

1824

};

1825

1826

6100

                Some(Literal::Int(-i))

1827

1828

1829

13784

            _ => None,

1830

1831

161060

1832

1833

    /// If this expression is an associative-commutative operator, return its [ACOperatorKind].

1834

16143252

    pub fn to_ac_operator_kind(&self) -> Option<ACOperatorKind> {

1835

16143252

        TryFrom::try_from(self).ok()

1836

16143252

1837

1838

    /// Returns the categories of all sub-expressions of self.

1839

92212

    pub fn universe_categories(&self) -> HashSet<Category> {

1840

92212

        self.universe()

1841

92212

            .into_iter()

1842

1095664

            .map(|x| x.category_of())

1843

92212

            .collect()

1844

92212

1845

1846

1847

pub fn get_function_codomain(function: &Moo<Expression>) -> Option<DomainPtr> {

1848

    let function_domain = function.domain_of()?;

1849

    match function_domain.resolve().as_ref() {

1850

        Ok(d) => {

1851

            match d.as_ref() {

1852

                GroundDomain::Function(_, _, codomain) => Some(codomain.clone().into()),

1853

                // Not defined for anything other than a function

1854

                _ => None,

1855

1856

1857

        Err(_) => {

1858

            match function_domain.as_unresolved()? {

1859

                UnresolvedDomain::Function(_, _, codomain) => Some(codomain.clone()),

1860

                // Not defined for anything other than a function

1861

                _ => None,

1862

1863

1864

1865

1866

1867

impl TryFrom<&Expression> for i32 {

1868

    type Error = ();

1869

1870

989260

    fn try_from(value: &Expression) -> Result<Self, Self::Error> {

1871

989260

        let Expression::Atomic(_, atom) = value else {

1872

742756

            return Err(());

1873

};

1874

1875

246504

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

1876

245184

            return Err(());

1877

};

1878

1879

1320

        let Literal::Int(i) = lit else {

1880

            return Err(());

1881

};

1882

1883

1320

        Ok(*i)

1884

989260

1885

1886

1887

impl TryFrom<Expression> for i32 {

1888

    type Error = ();

1889

1890

    fn try_from(value: Expression) -> Result<Self, Self::Error> {

1891

        TryFrom::<&Expression>::try_from(&value)

1892

1893

1894

impl From<i32> for Expression {

1895

70944

    fn from(i: i32) -> Self {

1896

70944

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

1897

70944

1898

1899

1900

impl From<bool> for Expression {

1901

38484

    fn from(b: bool) -> Self {

1902

38484

        Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(b)))

1903

38484

1904

1905

1906

impl From<Atom> for Expression {

1907

5548

    fn from(value: Atom) -> Self {

1908

5548

        Expression::Atomic(Metadata::new(), value)

1909

5548

1910

1911

1912

impl From<Literal> for Expression {

1913

7040

    fn from(value: Literal) -> Self {

1914

7040

        Expression::Atomic(Metadata::new(), value.into())

1915

7040

1916

1917

1918

impl From<AbstractLiteral<Expression>> for Expression {

1919

    fn from(value: AbstractLiteral<Expression>) -> Self {

1920

        Expression::AbstractLiteral(Metadata::new(), value)

1921

1922

1923

1924

impl From<Moo<Expression>> for Expression {

1925

87788

    fn from(val: Moo<Expression>) -> Self {

1926

87788

        val.as_ref().clone()

1927

87788

1928

1929

1930

impl CategoryOf for Expression {

1931

1391196

    fn category_of(&self) -> Category {

1932

        // take highest category of all the expressions children

1933

5389436

        let category = self.cata(&move |x,children| {

1934

1935

5389436

            if let Some(max_category) = children.iter().max() {

1936

                // if this expression contains subexpressions, return the maximum category of the

1937

                // subexpressions

1938

1664536

                *max_category

1939

            } else {

1940

                // this expression has no children

1941

3724900

                let mut max_category = Category::Bottom;

1942

1943

                // calculate the category by looking at all atoms, submodels, comprehensions, and

1944

                // declarationptrs inside this expression

1945

1946

                // this should generically cover all leaf types we currently have in oxide.

1947

1948

                // if x contains submodels (including comprehensions)

1949

3724900

                if !Biplate::<Model>::universe_bi(&x).is_empty() {

1950

                    // assume that the category is decision

1951

                    return Category::Decision;

1952

3724900

1953

1954

                // if x contains atoms

1955

3779580

                if let Some(max_atom_category) = Biplate::<Atom>::universe_bi(&x).iter().map(|x| x.category_of()).max()

1956

                // and those atoms have a higher category than we already know about

1957

3724860

                && max_atom_category > max_category{

1958

                    // update category

1959

3724860

                    max_category = max_atom_category;

1960

3724860

1961

1962

                // if x contains declarationPtrs

1963

3724900

                if let Some(max_declaration_category) = Biplate::<DeclarationPtr>::universe_bi(&x).iter().map(|x| x.category_of()).max()

1964

                // and those pointers have a higher category than we already know about

1965

2835292

                && max_declaration_category > max_category{

1966

                    // update category

1967

1228

                    max_category = max_declaration_category;

1968

3723672

1969

3724900

                max_category

1970

1971

1972

5389436

});

1973

1974

1391196

        if cfg!(debug_assertions) {

1975

1391196

            trace!(

1976

                category= %category,

1977

                expression= %self,

1978

                "Called Expression::category_of()"

1979

);

1980

};

1981

1391196

        category

1982

1391196

1983

1984

1985

impl Display for Expression {

1986

81866092

    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {

1987

81866092

        match &self {

1988

448

            Expression::Union(_, box1, box2) => {

1989

448

                write!(f, "({} union {})", box1.clone(), box2.clone())

1990

1991

3120

            Expression::In(_, e1, e2) => {

1992

3120

                write!(f, "{e1} in {e2}")

1993

1994

400

            Expression::Intersect(_, box1, box2) => {

1995

400

                write!(f, "({} intersect {})", box1.clone(), box2.clone())

1996

1997

480

            Expression::Supset(_, box1, box2) => {

1998

480

                write!(f, "({} supset {})", box1.clone(), box2.clone())

1999

2000

480

            Expression::SupsetEq(_, box1, box2) => {

2001

480

                write!(f, "({} supsetEq {})", box1.clone(), box2.clone())

2002

2003

600

            Expression::Subset(_, box1, box2) => {

2004

600

                write!(f, "({} subset {})", box1.clone(), box2.clone())

2005

2006

540

            Expression::SubsetEq(_, box1, box2) => {

2007

540

                write!(f, "({} subsetEq {})", box1.clone(), box2.clone())

2008

2009

2010

3079520

            Expression::AbstractLiteral(_, l) => l.fmt(f),

2011

31928

            Expression::Comprehension(_, c) => c.fmt(f),

2012

            Expression::AbstractComprehension(_, c) => c.fmt(f),

2013

409468

            Expression::UnsafeIndex(_, e1, e2) => write!(f, "{e1}{}", pretty_vec(e2)),

2014

1800

            Expression::RecordField(_, r, fld) => {

2015

1800

                write!(f, "{r}[{fld}]")

2016

2017

992960

            Expression::SafeIndex(_, e1, e2) => write!(f, "SafeIndex({e1},{})", pretty_vec(e2)),

2018

20320

            Expression::UnsafeSlice(_, e1, es) => {

2019

20320

                let args = es

2020

20320

                    .iter()

2021

40400

                    .map(|x| match x {

2022

20080

                        Some(x) => format!("{x}"),

2023

20320

                        None => "..".into(),

2024

40400

})

2025

20320

                    .join(",");

2026

2027

20320

                write!(f, "{e1}[{args}]")

2028

2029

13760

            Expression::SafeSlice(_, e1, es) => {

2030

13760

                let args = es

2031

13760

                    .iter()

2032

26960

                    .map(|x| match x {

2033

13200

                        Some(x) => format!("{x}"),

2034

13760

                        None => "..".into(),

2035

26960

})

2036

13760

                    .join(",");

2037

2038

13760

                write!(f, "SafeSlice({e1},[{args}])")

2039

2040

3480

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

2041

3480

                write!(f, "__inDomain({e},{domain})")

2042

2043

229920

            Expression::Root(_, exprs) => {

2044

229920

                write!(f, "{}", pretty_expressions_as_top_level(exprs))

2045

2046

            Expression::DominanceRelation(_, expr) => write!(f, "DominanceRelation({expr})"),

2047

            Expression::FromSolution(_, expr) => write!(f, "FromSolution({expr})"),

2048

            Expression::Metavar(_, name) => write!(f, "&{name}"),

2049

70505120

            Expression::Atomic(_, atom) => atom.fmt(f),

2050

8392

            Expression::Abs(_, a) | Expression::Card(_, a) => write!(f, "|{a}|"),

2051

953644

            Expression::Sum(_, e) => {

2052

953644

                write!(f, "sum({e})")

2053

2054

112976

            Expression::Product(_, e) => {

2055

112976

                write!(f, "product({e})")

2056

2057

14840

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

2058

14840

                write!(f, "min({e})")

2059

2060

14968

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

2061

14968

                write!(f, "max({e})")

2062

2063

44780

            Expression::Not(_, expr_box) => {

2064

44780

                write!(f, "!({})", expr_box.clone())

2065

2066

330640

            Expression::Or(_, e) => {

2067

330640

                write!(f, "or({e})")

2068

2069

312316

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

2070

312316

                write!(f, "and({e})")

2071

2072

61392

            Expression::Imply(_, box1, box2) => {

2073

61392

                write!(f, "({box1}) -> ({box2})")

2074

2075

1680

            Expression::Iff(_, box1, box2) => {

2076

1680

                write!(f, "({box1}) <-> ({box2})")

2077

2078

437264

            Expression::Eq(_, box1, box2) => {

2079

437264

                write!(f, "({} = {})", box1.clone(), box2.clone())

2080

2081

832072

            Expression::Neq(_, box1, box2) => {

2082

832072

                write!(f, "({} != {})", box1.clone(), box2.clone())

2083

2084

141348

            Expression::Geq(_, box1, box2) => {

2085

141348

                write!(f, "({} >= {})", box1.clone(), box2.clone())

2086

2087

454992

            Expression::Leq(_, box1, box2) => {

2088

454992

                write!(f, "({} <= {})", box1.clone(), box2.clone())

2089

2090

7568

            Expression::Gt(_, box1, box2) => {

2091

7568

                write!(f, "({} > {})", box1.clone(), box2.clone())

2092

2093

45568

            Expression::Lt(_, box1, box2) => {

2094

45568

                write!(f, "({} < {})", box1.clone(), box2.clone())

2095

2096

40

            Expression::Apart(_, list, partition) => {

2097

40

                write!(f, "apart({list}, {partition})")

2098

2099

40

            Expression::Together(_, list, partition) => {

2100

40

                write!(f, "together({list}, {partition})")

2101

2102

56

            Expression::Participants(_, partition) => {

2103

56

                write!(f, "participants({partition})")

2104

2105

48

            Expression::Party(_, element, partition) => {

2106

48

                write!(f, "party({element}, {partition})")

2107

2108

56

            Expression::Parts(_, partition) => {

2109

56

                write!(f, "parts({partition})")

2110

2111

246260

            Expression::FlatSumGeq(_, box1, box2) => {

2112

246260

                write!(f, "SumGeq({}, {})", pretty_vec(box1), box2.clone())

2113

2114

241140

            Expression::FlatSumLeq(_, box1, box2) => {

2115

241140

                write!(f, "SumLeq({}, {})", pretty_vec(box1), box2.clone())

2116

2117

84864

            Expression::FlatIneq(_, box1, box2, box3) => write!(

2118

84864

f,

2119

                "Ineq({}, {}, {})",

2120

84864

                box1.clone(),

2121

84864

                box2.clone(),

2122

84864

                box3.clone()

2123

),

2124

2028

            Expression::Flatten(_, n, m) => {

2125

2028

                if let Some(n) = n {

2126

                    write!(f, "flatten({n}, {m})")

2127

                } else {

2128

2028

                    write!(f, "flatten({m})")

2129

2130

2131

14912

            Expression::AllDiff(_, e) => {

2132

14912

                write!(f, "allDiff({e})")

2133

2134

1200

            Expression::Table(_, tuple_expr, rows_expr) => {

2135

1200

                write!(f, "table({tuple_expr}, {rows_expr})")

2136

2137

200

            Expression::NegativeTable(_, tuple_expr, rows_expr) => {

2138

200

                write!(f, "negativeTable({tuple_expr}, {rows_expr})")

2139

2140

13648

            Expression::Bubble(_, box1, box2) => {

2141

13648

                write!(f, "{{{} @ {}}}", box1.clone(), box2.clone())

2142

2143

19960

            Expression::SafeDiv(_, box1, box2) => {

2144

19960

                write!(f, "SafeDiv({}, {})", box1.clone(), box2.clone())

2145

2146

21560

            Expression::UnsafeDiv(_, box1, box2) => {

2147

21560

                write!(f, "({} / {})", box1.clone(), box2.clone())

2148

2149

46992

            Expression::UnsafePow(_, box1, box2) => {

2150

46992

                write!(f, "({} ** {})", box1.clone(), box2.clone())

2151

2152

555884

            Expression::SafePow(_, box1, box2) => {

2153

555884

                write!(f, "SafePow({}, {})", box1.clone(), box2.clone())

2154

2155

            Expression::Subsequence(_, s, t) => {

2156

                write!(f, "{} subsequence {}", s.clone(), t.clone())

2157

2158

80

            Expression::Substring(_, s, t) => {

2159

80

                write!(f, "{} substring {}", s.clone(), t.clone())

2160

2161

4220

            Expression::MinionDivEqUndefZero(_, box1, box2, box3) => {

2162

4220

                write!(

2163

4220

f,

2164

                    "DivEq({}, {}, {})",

2165

4220

                    box1.clone(),

2166

4220

                    box2.clone(),

2167

4220

                    box3.clone()

2168

2169

2170

1320

            Expression::MinionModuloEqUndefZero(_, box1, box2, box3) => {

2171

1320

                write!(

2172

1320

f,

2173

                    "ModEq({}, {}, {})",

2174

1320

                    box1.clone(),

2175

1320

                    box2.clone(),

2176

1320

                    box3.clone()

2177

2178

2179

4348

            Expression::FlatWatchedLiteral(_, x, l) => {

2180

4348

                write!(f, "WatchedLiteral({x},{l})")

2181

2182

109692

            Expression::MinionReify(_, box1, box2) => {

2183

109692

                write!(f, "Reify({}, {})", box1.clone(), box2.clone())

2184

2185

71556

            Expression::MinionReifyImply(_, box1, box2) => {

2186

71556

                write!(f, "ReifyImply({}, {})", box1.clone(), box2.clone())

2187

2188

760

            Expression::MinionWInIntervalSet(_, atom, intervals) => {

2189

760

                let intervals = intervals.iter().join(",");

2190

760

                write!(f, "__minion_w_inintervalset({atom},[{intervals}])")

2191

2192

480

            Expression::MinionWInSet(_, atom, values) => {

2193

480

                let values = values.iter().join(",");

2194

480

                write!(f, "__minion_w_inset({atom},[{values}])")

2195

2196

105044

            Expression::AuxDeclaration(_, reference, e) => {

2197

105044

                write!(f, "{} =aux {}", reference, e.clone())

2198

2199

3880

            Expression::UnsafeMod(_, a, b) => {

2200

3880

                write!(f, "{} % {}", a.clone(), b.clone())

2201

2202

6720

            Expression::SafeMod(_, a, b) => {

2203

6720

                write!(f, "SafeMod({},{})", a.clone(), b.clone())

2204

2205

61820

            Expression::Neg(_, a) => {

2206

61820

                write!(f, "-({})", a.clone())

2207

2208

            Expression::Factorial(_, a) => {

2209

                write!(f, "({})!", a.clone())

2210

2211

266424

            Expression::Minus(_, a, b) => {

2212

266424

                write!(f, "({} - {})", a.clone(), b.clone())

2213

2214

10488

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

2215

10488

                write!(f, "__flat_alldiff({})", pretty_vec(es))

2216

2217

1600

            Expression::FlatAbsEq(_, a, b) => {

2218

1600

                write!(f, "AbsEq({},{})", a.clone(), b.clone())

2219

2220

720

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

2221

720

                write!(f, "MinusEq({},{})", a.clone(), b.clone())

2222

2223

2300

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

2224

2300

                write!(

2225

2300

f,

2226

                    "FlatProductEq({},{},{})",

2227

2300

                    a.clone(),

2228

2300

                    b.clone(),

2229

2300

                    c.clone()

2230

2231

2232

18700

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

2233

18700

                write!(

2234

18700

f,

2235

                    "FlatWeightedSumLeq({},{},{})",

2236

18700

                    pretty_vec(cs),

2237

18700

                    pretty_vec(vs),

2238

18700

                    total.clone()

2239

2240

2241

18900

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

2242

18900

                write!(

2243

18900

f,

2244

                    "FlatWeightedSumGeq({},{},{})",

2245

18900

                    pretty_vec(cs),

2246

18900

                    pretty_vec(vs),

2247

18900

                    total.clone()

2248

2249

2250

17240

            Expression::MinionPow(_, atom, atom1, atom2) => {

2251

17240

                write!(f, "MinionPow({atom},{atom1},{atom2})")

2252

2253

169216

            Expression::MinionElementOne(_, atoms, atom, atom1) => {

2254

169216

                let atoms = atoms.iter().join(",");

2255

169216

                write!(f, "__minion_element_one([{atoms}],{atom},{atom1})")

2256

2257

2258

1192

            Expression::ToInt(_, expr) => {

2259

1192

                write!(f, "toInt({expr})")

2260

2261

2262

655720

            Expression::SATInt(_, encoding, bits, (min, max)) => {

2263

655720

                write!(f, "SATInt({encoding:?}, {bits} [{min}, {max}])")

2264

2265

2266

            Expression::PairwiseSum(_, a, b) => write!(f, "PairwiseSum({a}, {b})"),

2267

            Expression::PairwiseProduct(_, a, b) => write!(f, "PairwiseProduct({a}, {b})"),

2268

2269

104

            Expression::Defined(_, function) => write!(f, "defined({function})"),

2270

128

            Expression::Range(_, function) => write!(f, "range({function})"),

2271

40

            Expression::Image(_, function, elems) => write!(f, "image({function},{elems})"),

2272

40

            Expression::ImageSet(_, function, elems) => write!(f, "imageSet({function},{elems})"),

2273

128

            Expression::PreImage(_, function, elems) => write!(f, "preImage({function},{elems})"),

2274

40

            Expression::Inverse(_, a, b) => write!(f, "inverse({a},{b})"),

2275

72

            Expression::Restrict(_, function, domain) => write!(f, "restrict({function},{domain})"),

2276

2277

1360

            Expression::LexLt(_, a, b) => write!(f, "({a} <lex {b})"),

2278

12820

            Expression::LexLeq(_, a, b) => write!(f, "({a} <=lex {b})"),

2279

120

            Expression::LexGt(_, a, b) => write!(f, "({a} >lex {b})"),

2280

180

            Expression::LexGeq(_, a, b) => write!(f, "({a} >=lex {b})"),

2281

240

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

2282

240

                write!(f, "FlatLexLt({}, {})", pretty_vec(a), pretty_vec(b))

2283

2284

400

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

2285

400

                write!(f, "FlatLexLeq({}, {})", pretty_vec(a), pretty_vec(b))

2286

2287

40

            Expression::Active(_, variant, field_name) => {

2288

40

                write!(f, "active({variant}, {field_name})")

2289

2290

120

            Expression::ToSet(_, other) => write!(f, "toSet({other})"),

2291

80

            Expression::ToMSet(_, other) => write!(f, "toMSet({other})"),

2292

40

            Expression::ToRelation(_, function) => write!(f, "toRelation({function})"),

2293

48

            Expression::RelationProj(_, relation, projections) => {

2294

48

                let projections_str = projections

2295

48

                    .iter()

2296

144

                    .map(|x| {

2297

144

                        if let Some(x) = x {

2298

48

                            x.to_string()

2299

                        } else {

2300

96

                            String::from("_")

2301

2302

144

})

2303

48

                    .join(", ");

2304

48

                write!(f, "{relation}({projections_str})")

2305

2306

2307

81866092

2308

2309

2310

3280

fn minus_operand_return_type(expr: &Expression) -> ReturnType {

2311

1988

    match expr {

2312

1148

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

2313

1148

            let decl_kind = reference.ptr.kind().clone();

2314

1148

            match decl_kind {

2315

444

                DeclarationKind::Find(var) => var.return_type(),

2316

                DeclarationKind::Given(domain)

2317

                | DeclarationKind::DomainLetting(domain) => domain.return_type(),

2318

280

                DeclarationKind::Quantified(inner) => inner.domain().return_type(),

2319

                DeclarationKind::QuantifiedExpr(inner)

2320

                | DeclarationKind::TemporaryValueLetting(inner)

2321

                // not sure if i should ever be looking at the domain ptr but seems to work

2322

424

                | DeclarationKind::ValueLetting(inner, _) => inner.return_type(),

2323

2324

2325

2132

        _ => expr.return_type(),

2326

2327

3280

2328

2329

impl Typeable for Expression {

2330

2292197

    fn return_type(&self) -> ReturnType {

2331

2292197

        match self {

2332

            Expression::Union(_, subject, _) => ReturnType::Set(Box::new(subject.return_type())),

2333

            Expression::Intersect(_, subject, _) => {

2334

                ReturnType::Set(Box::new(subject.return_type()))

2335

2336

600

            Expression::In(_, _, _) => ReturnType::Bool,

2337

            Expression::Supset(_, _, _) => ReturnType::Bool,

2338

            Expression::SupsetEq(_, _, _) => ReturnType::Bool,

2339

            Expression::Subset(_, _, _) => ReturnType::Bool,

2340

            Expression::SubsetEq(_, _, _) => ReturnType::Bool,

2341

135440

            Expression::AbstractLiteral(_, lit) => lit.return_type(),

2342

2480

            Expression::RecordField(_, rec, field_name) => {

2343

2480

                if let ReturnType::Record(ents) = rec.return_type() {

2344

4080

                    for Field { name, value } in ents {

2345

4080

                        if name.eq(field_name) {

2346

2480

                            return value;

2347

1600

2348

2349

2350

                ReturnType::Unknown

2351

2352

233504

            Expression::UnsafeIndex(_, subject, idx) | Expression::SafeIndex(_, subject, idx) => {

2353

311144

                let subject_ty = subject.return_type();

2354

311144

                match subject_ty {

2355

                    ReturnType::Matrix(_) => {

2356

                        // For n-dimensional matrices, unwrap the element type until

2357

                        // we either get to the innermost element type or the last index

2358

305384

                        let mut elem_typ = subject_ty;

2359

305384

                        let mut idx_len = idx.len();

2360

611236

                        while idx_len > 0

2361

362120

                            && let ReturnType::Matrix(new_elem_typ) = &elem_typ

2362

305852

2363

305852

                            elem_typ = *new_elem_typ.clone();

2364

305852

                            idx_len -= 1;

2365

305852

2366

305384

                        elem_typ

2367

2368

                    // TODO: We can implement indexing for these eventually

2369

                    ReturnType::Record(_) | ReturnType::Tuple(_) | ReturnType::Variant(_) => {

2370

5760

                        ReturnType::Unknown

2371

2372

                    _ => bug!(

2373

                        "Invalid indexing operation: expected the operand to be a collection, got {self}: {subject_ty}"

2374

),

2375

2376

2377

480

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

2378

640

                ReturnType::Matrix(Box::new(subject.return_type()))

2379

2380

            Expression::InDomain(_, _, _) => ReturnType::Bool,

2381

8

            Expression::Comprehension(_, comp) => comp.return_type(),

2382

            Expression::AbstractComprehension(_, comp) => comp.return_type(),

2383

            Expression::Root(_, _) => ReturnType::Bool,

2384

            Expression::DominanceRelation(_, _) => ReturnType::Bool,

2385

            Expression::FromSolution(_, expr) => expr.return_type(),

2386

            Expression::Metavar(_, _) => ReturnType::Unknown,

2387

1625717

            Expression::Atomic(_, atom) => atom.return_type(),

2388

1120

            Expression::Abs(_, _) => ReturnType::Int,

2389

106008

            Expression::Sum(_, _) => ReturnType::Int,

2390

10924

            Expression::Product(_, _) => ReturnType::Int,

2391

1920

            Expression::Min(_, _) => ReturnType::Int,

2392

2020

            Expression::Max(_, _) => ReturnType::Int,

2393

160

            Expression::Not(_, _) => ReturnType::Bool,

2394

428

            Expression::Or(_, _) => ReturnType::Bool,

2395

1304

            Expression::Imply(_, _, _) => ReturnType::Bool,

2396

            Expression::Iff(_, _, _) => ReturnType::Bool,

2397

8276

            Expression::And(_, _) => ReturnType::Bool,

2398

8704

            Expression::Eq(_, _, _) => ReturnType::Bool,

2399

1520

            Expression::Neq(_, _, _) => ReturnType::Bool,

2400

            Expression::Geq(_, _, _) => ReturnType::Bool,

2401

2200

            Expression::Leq(_, _, _) => ReturnType::Bool,

2402

            Expression::Gt(_, _, _) => ReturnType::Bool,

2403

            Expression::Lt(_, _, _) => ReturnType::Bool,

2404

            Expression::Apart(_, _, _) => ReturnType::Bool,

2405

            Expression::Together(_, _, _) => ReturnType::Bool,

2406

40

            Expression::Party(_, _, subject) => ReturnType::Set(Box::new(subject.return_type())),

2407

40

            Expression::Participants(_, subject) => {

2408

40

                ReturnType::Set(Box::new(subject.return_type()))

2409

2410

40

            Expression::Parts(_, subject) => {

2411

40

                ReturnType::Set(Box::new(ReturnType::Set(Box::new(subject.return_type()))))

2412

2413

13200

            Expression::SafeDiv(_, _, _) => ReturnType::Int,

2414

11400

            Expression::UnsafeDiv(_, _, _) => ReturnType::Int,

2415

            Expression::FlatAllDiff(_, _) => ReturnType::Bool,

2416

80

            Expression::FlatSumGeq(_, _, _) => ReturnType::Bool,

2417

            Expression::FlatSumLeq(_, _, _) => ReturnType::Bool,

2418

            Expression::MinionDivEqUndefZero(_, _, _, _) => ReturnType::Bool,

2419

680

            Expression::FlatIneq(_, _, _, _) => ReturnType::Bool,

2420

2560

            Expression::Flatten(_, _, matrix) => {

2421

2560

                let matrix_type = matrix.return_type();

2422

2560

                match matrix_type {

2423

                    ReturnType::Matrix(_) => {

2424

                        // unwrap until we get to innermost element

2425

2560

                        let mut elem_type = matrix_type;

2426

5120

                        while let ReturnType::Matrix(new_elem_type) = &elem_type {

2427

2560

                            elem_type = *new_elem_type.clone();

2428

2560

2429

2560

                        ReturnType::Matrix(Box::new(elem_type))

2430

2431

                    _ => bug!(

2432

                        "Invalid indexing operation: expected the operand to be a collection, got {self}: {matrix_type}"

2433

),

2434

2435

2436

160

            Expression::AllDiff(_, _) => ReturnType::Bool,

2437

            Expression::Table(_, _, _) => ReturnType::Bool,

2438

            Expression::NegativeTable(_, _, _) => ReturnType::Bool,

2439

3120

            Expression::Bubble(_, inner, _) => inner.return_type(),

2440

            Expression::FlatWatchedLiteral(_, _, _) => ReturnType::Bool,

2441

            Expression::MinionReify(_, _, _) => ReturnType::Bool,

2442

240

            Expression::MinionReifyImply(_, _, _) => ReturnType::Bool,

2443

            Expression::MinionWInIntervalSet(_, _, _) => ReturnType::Bool,

2444

            Expression::MinionWInSet(_, _, _) => ReturnType::Bool,

2445

            Expression::MinionElementOne(_, _, _, _) => ReturnType::Bool,

2446

            Expression::AuxDeclaration(_, _, _) => ReturnType::Bool,

2447

1520

            Expression::UnsafeMod(_, _, _) => ReturnType::Int,

2448

4320

            Expression::SafeMod(_, _, _) => ReturnType::Int,

2449

            Expression::MinionModuloEqUndefZero(_, _, _, _) => ReturnType::Bool,

2450

2884

            Expression::Neg(_, _) => ReturnType::Int,

2451

            Expression::Factorial(_, _) => ReturnType::Int,

2452

1012

            Expression::UnsafePow(_, _, _) => ReturnType::Int,

2453

2808

            Expression::SafePow(_, _, _) => ReturnType::Int,

2454

1640

            Expression::Minus(_, a, b) => {

2455

                // rather than calling .return_type on a and b which sometimes errors on references that don't have domains

2456

                // use custom function that extracts return type from atomic references based on each declaration variant

2457

1640

                let a_type = minus_operand_return_type(a);

2458

1640

                let b_type = minus_operand_return_type(b);

2459

2460

1640

                if a_type == ReturnType::Int && b_type == ReturnType::Int {

2461

1640

                    ReturnType::Int

2462

                } else if let ReturnType::Set(a_inner) = a_type

2463

                    && let ReturnType::Set(b_inner) = b_type

2464

                    && a_inner == b_inner

2465

2466

                    ReturnType::Set(a_inner)

2467

                } else {

2468

                    bug!(

2469

                        "Invalid minus operation: operands are of different or invalid types for this operation"

2470

2471

2472

2473

            Expression::FlatAbsEq(_, _, _) => ReturnType::Bool,

2474

            Expression::FlatMinusEq(_, _, _) => ReturnType::Bool,

2475

            Expression::FlatProductEq(_, _, _, _) => ReturnType::Bool,

2476

            Expression::FlatWeightedSumLeq(_, _, _, _) => ReturnType::Bool,

2477

160

            Expression::FlatWeightedSumGeq(_, _, _, _) => ReturnType::Bool,

2478

            Expression::MinionPow(_, _, _, _) => ReturnType::Bool,

2479

2360

            Expression::ToInt(_, _) => ReturnType::Int,

2480

21960

            Expression::SATInt(..) => ReturnType::Int,

2481

            Expression::PairwiseSum(_, _, _) => ReturnType::Int,

2482

            Expression::PairwiseProduct(_, _, _) => ReturnType::Int,

2483

            Expression::Defined(_, function) => {

2484

                let subject = function.return_type();

2485

                match subject {

2486

                    ReturnType::Function(domain, _) => ReturnType::Set(Box::new(*domain)),

2487

                    _ => bug!(

2488

                        "Invalid defined operation: expected the operand to be a function, got {self}: {subject}"

2489

),

2490

2491

2492

            Expression::Range(_, function) => {

2493

                let subject = function.return_type();

2494

                match subject {

2495

                    ReturnType::Function(_, codomain) => ReturnType::Set(Box::new(*codomain)),

2496

                    _ => bug!(

2497

                        "Invalid range operation: expected the operand to be a function, got {self}: {subject}"

2498

),

2499

2500

2501

            Expression::Image(_, function, _) => {

2502

                let subject = function.return_type();

2503

                match subject {

2504

                    ReturnType::Function(_, codomain) => *codomain,

2505

                    _ => bug!(

2506

                        "Invalid image operation: expected the operand to be a function, got {self}: {subject}"

2507

),

2508

2509

2510

            Expression::ImageSet(_, function, _) => {

2511

                let subject = function.return_type();

2512

                match subject {

2513

                    ReturnType::Function(_, codomain) => ReturnType::Set(Box::new(*codomain)),

2514

                    _ => bug!(

2515

                        "Invalid imageSet operation: expected the operand to be a function, got {self}: {subject}"

2516

),

2517

2518

2519

            Expression::PreImage(_, function, _) => {

2520

                let subject = function.return_type();

2521

                match subject {

2522

                    ReturnType::Function(domain, _) => ReturnType::Set(Box::new(*domain)),

2523

                    _ => bug!(

2524

                        "Invalid preImage operation: expected the operand to be a function, got {self}: {subject}"

2525

),

2526

2527

2528

            Expression::Restrict(_, function, new_domain) => {

2529

                let subject = function.return_type();

2530

                match subject {

2531

                    ReturnType::Function(_, codomain) => {

2532

                        ReturnType::Function(Box::new(new_domain.return_type()), codomain)

2533

2534

                    _ => bug!(

2535

                        "Invalid preImage operation: expected the operand to be a function, got {self}: {subject}"

2536

),

2537

2538

2539

            Expression::Inverse(..) => ReturnType::Bool,

2540

            Expression::LexLt(..) => ReturnType::Bool,

2541

            Expression::LexGt(..) => ReturnType::Bool,

2542

1360

            Expression::LexLeq(..) => ReturnType::Bool,

2543

            Expression::LexGeq(..) => ReturnType::Bool,

2544

            Expression::FlatLexLt(..) => ReturnType::Bool,

2545

            Expression::FlatLexLeq(..) => ReturnType::Bool,

2546

            Expression::Active(..) => ReturnType::Bool,

2547

            Expression::ToSet(_, other) => {

2548

                let subject = other.return_type();

2549

                match subject {

2550

                    ReturnType::Function(domain, codomain) => {

2551

                        ReturnType::Set(Box::new(ReturnType::Tuple(vec![*domain, *codomain])))

2552

2553

                    ReturnType::Relation(domains) => {

2554

                        ReturnType::Set(Box::new(ReturnType::Tuple(domains)))

2555

2556

                    ReturnType::MSet(domain) => ReturnType::Set(Box::new(*domain)),

2557

                    ReturnType::Matrix(domain) => ReturnType::Set(Box::new(*domain)),

2558

                    _ => bug!(

2559

                        "Invalid toSet operation: expected the operand to be a mset, matrix, relation, or function, got {self}: {subject}"

2560

),

2561

2562

2563

            Expression::ToMSet(_, other) => {

2564

                let subject = other.return_type();

2565

                match subject {

2566

                    ReturnType::Function(domain, codomain) => {

2567

                        ReturnType::MSet(Box::new(ReturnType::Tuple(vec![*domain, *codomain])))

2568

2569

                    ReturnType::Relation(domains) => {

2570

                        ReturnType::MSet(Box::new(ReturnType::Tuple(domains)))

2571

2572

                    ReturnType::Set(domain) => ReturnType::MSet(Box::new(*domain)),

2573

                    _ => bug!(

2574

                        "Invalid toMSet operation: expected the operand to be a set, relation, or function, got {self}: {subject}"

2575

),

2576

2577

2578

            Expression::ToRelation(_, function) => {

2579

                let subject = function.return_type();

2580

                match subject {

2581

                    ReturnType::Function(domain, codomain) => {

2582

                        ReturnType::Relation(vec![*domain, *codomain])

2583

2584

                    _ => bug!(

2585

                        "Invalid toRelation operation: expected the operand to be a function, got {self}: {subject}"

2586

),

2587

2588

2589

            Expression::RelationProj(_, relation, projections) => {

2590

                let subject = relation.return_type();

2591

                match subject {

2592

                    ReturnType::Relation(domains) => {

2593

                        let new_doms = domains

2594

                            .iter()

2595

                            .zip(projections.iter())

2596

                            .filter_map(|(domain, included)| {

2597

                                if included.is_none() {

2598

                                    // The domains corresponding to projections which are None remain in the relation

2599

                                    Some(domain.clone())

2600

                                } else {

2601

                                    None

2602

2603

})

2604

                            .collect();

2605

                        ReturnType::Relation(new_doms)

2606

2607

                    _ => bug!(

2608

                        "Invalid RelationProj operation: expected the operand to be a relation, got {self}: {subject}"

2609

),

2610

2611

2612

            Expression::Card(..) => ReturnType::Int,

2613

            Expression::Subsequence(_, _, _) => ReturnType::Bool,

2614

            Expression::Substring(_, _, _) => ReturnType::Bool,

2615

2616

2292197

2617

2618

2619

impl Expression {

2620

    /// Visit each direct `Expression` child by reference, without cloning.

2621

    fn for_each_expr_child(&self, f: &mut impl FnMut(&Expression)) {

2622

        match self {

2623

            // Special Case

2624

            Expression::AbstractLiteral(_, alit) => match alit {

2625

                AbstractLiteral::Set(v) | AbstractLiteral::MSet(v) | AbstractLiteral::Tuple(v) => {

2626

                    for expr in v {

2627

                        f(expr);

2628

2629

2630

                AbstractLiteral::Partition(two_d_v) => {

2631

                    for part in two_d_v {

2632

                        for expr in part {

2633

                            f(expr);

2634

2635

2636

2637

                AbstractLiteral::Matrix(v, _domain) => {

2638

                    for expr in v {

2639

                        f(expr);

2640

2641

2642

                AbstractLiteral::Record(rs) => {

2643

                    for r in rs {

2644

                        f(&r.value);

2645

2646

2647

                AbstractLiteral::Sequence(v) => {

2648

                    for expr in v {

2649

                        f(expr);

2650

2651

2652

                AbstractLiteral::Function(vs) => {

2653

                    for (a, b) in vs {

2654

                        f(a);

2655

                        f(b);

2656

2657

2658

                AbstractLiteral::Variant(v) => {

2659

                    f(&v.value);

2660

2661

                AbstractLiteral::Relation(vs) => {

2662

                    for exprs in vs {

2663

                        for expr in exprs {

2664

                            f(expr);

2665

2666

2667

2668

},

2669

            Expression::Root(_, vs) => {

2670

                for expr in vs {

2671

                    f(expr);

2672

2673

2674

2675

            // Moo<Expression>

2676

            Expression::DominanceRelation(_, m1)

2677

            | Expression::ToInt(_, m1)

2678

            | Expression::Abs(_, m1)

2679

            | Expression::Sum(_, m1)

2680

            | Expression::Product(_, m1)

2681

            | Expression::Min(_, m1)

2682

            | Expression::Max(_, m1)

2683

            | Expression::Not(_, m1)

2684

            | Expression::Or(_, m1)

2685

            | Expression::And(_, m1)

2686

            | Expression::Neg(_, m1)

2687

            | Expression::Defined(_, m1)

2688

            | Expression::AllDiff(_, m1)

2689

            | Expression::Factorial(_, m1)

2690

            | Expression::Range(_, m1)

2691

            | Expression::Participants(_, m1)

2692

            | Expression::Parts(_, m1)

2693

            | Expression::ToSet(_, m1)

2694

            | Expression::ToMSet(_, m1)

2695

            | Expression::ToRelation(_, m1)

2696

            | Expression::Card(_, m1)

2697

            | Expression::RecordField(_, m1, _)

2698

            | Expression::Active(_, m1, _) => {

2699

                f(m1);

2700

2701

2702

            // Moo<Expression> + Moo<Expression>

2703

            Expression::Table(_, m1, m2)

2704

            | Expression::NegativeTable(_, m1, m2)

2705

            | Expression::Bubble(_, m1, m2)

2706

            | Expression::Imply(_, m1, m2)

2707

            | Expression::Iff(_, m1, m2)

2708

            | Expression::Union(_, m1, m2)

2709

            | Expression::In(_, m1, m2)

2710

            | Expression::Intersect(_, m1, m2)

2711

            | Expression::Supset(_, m1, m2)

2712

            | Expression::SupsetEq(_, m1, m2)

2713

            | Expression::Subset(_, m1, m2)

2714

            | Expression::SubsetEq(_, m1, m2)

2715

            | Expression::Eq(_, m1, m2)

2716

            | Expression::Neq(_, m1, m2)

2717

            | Expression::Geq(_, m1, m2)

2718

            | Expression::Leq(_, m1, m2)

2719

            | Expression::Gt(_, m1, m2)

2720

            | Expression::Lt(_, m1, m2)

2721

            | Expression::SafeDiv(_, m1, m2)

2722

            | Expression::UnsafeDiv(_, m1, m2)

2723

            | Expression::SafeMod(_, m1, m2)

2724

            | Expression::UnsafeMod(_, m1, m2)

2725

            | Expression::UnsafePow(_, m1, m2)

2726

            | Expression::SafePow(_, m1, m2)

2727

            | Expression::Minus(_, m1, m2)

2728

            | Expression::PairwiseSum(_, m1, m2)

2729

            | Expression::PairwiseProduct(_, m1, m2)

2730

            | Expression::Image(_, m1, m2)

2731

            | Expression::ImageSet(_, m1, m2)

2732

            | Expression::PreImage(_, m1, m2)

2733

            | Expression::Inverse(_, m1, m2)

2734

            | Expression::Restrict(_, m1, m2)

2735

            | Expression::Apart(_, m1, m2)

2736

            | Expression::Together(_, m1, m2)

2737

            | Expression::Party(_, m1, m2)

2738

            | Expression::LexLt(_, m1, m2)

2739

            | Expression::LexLeq(_, m1, m2)

2740

            | Expression::LexGt(_, m1, m2)

2741

            | Expression::LexGeq(_, m1, m2)

2742

            | Expression::Subsequence(_, m1, m2)

2743

            | Expression::Substring(_, m1, m2) => {

2744

                f(m1);

2745

                f(m2);

2746

2747

2748

            // Moo<Expression> + Vec<Expression>

2749

            Expression::UnsafeIndex(_, m, vs) | Expression::SafeIndex(_, m, vs) => {

2750

                f(m);

2751

                for v in vs {

2752

                    f(v);

2753

2754

2755

            // Moo<Expression> + Vec<Option<Expression>>

2756

            Expression::UnsafeSlice(_, m, vs)

2757

            | Expression::SafeSlice(_, m, vs)

2758

            | Expression::RelationProj(_, m, vs) => {

2759

                f(m);

2760

                for e in vs.iter().flatten() {

2761

                    f(e);

2762

2763

2764

2765

            // Moo<Expression> + DomainPtr

2766

            Expression::InDomain(_, m, _) => {

2767

                f(m);

2768

2769

2770

            // Option<Moo<Expression>> + Moo<Expression>

2771

            Expression::Flatten(_, opt, m) => {

2772

                if let Some(e) = opt {

2773

                    f(e);

2774

2775

                f(m);

2776

2777

2778

            // Moo<Expression> + Atom

2779

            Expression::MinionReify(_, m, _) | Expression::MinionReifyImply(_, m, _) => {

2780

                f(m);

2781

2782

2783

            // Reference + Moo<Expression>

2784

            Expression::AuxDeclaration(_, _, m) => {

2785

                f(m);

2786

2787

2788

            // SATIntEncoding + Moo<Expression> + (i32, i32)

2789

            Expression::SATInt(_, _, m, _) => {

2790

                f(m);

2791

2792

2793

            // No Expression children

2794

            Expression::Comprehension(_, _)

2795

            | Expression::AbstractComprehension(_, _)

2796

            | Expression::Atomic(_, _)

2797

            | Expression::FromSolution(_, _)

2798

            | Expression::Metavar(_, _)

2799

            | Expression::FlatAbsEq(_, _, _)

2800

            | Expression::FlatMinusEq(_, _, _)

2801

            | Expression::FlatProductEq(_, _, _, _)

2802

            | Expression::MinionDivEqUndefZero(_, _, _, _)

2803

            | Expression::MinionModuloEqUndefZero(_, _, _, _)

2804

            | Expression::MinionPow(_, _, _, _)

2805

            | Expression::FlatAllDiff(_, _)

2806

            | Expression::FlatSumGeq(_, _, _)

2807

            | Expression::FlatSumLeq(_, _, _)

2808

            | Expression::FlatIneq(_, _, _, _)

2809

            | Expression::FlatWatchedLiteral(_, _, _)

2810

            | Expression::FlatWeightedSumLeq(_, _, _, _)

2811

            | Expression::FlatWeightedSumGeq(_, _, _, _)

2812

            | Expression::MinionWInIntervalSet(_, _, _)

2813

            | Expression::MinionWInSet(_, _, _)

2814

            | Expression::MinionElementOne(_, _, _, _)

2815

            | Expression::FlatLexLt(_, _, _)

2816

            | Expression::FlatLexLeq(_, _, _) => {}

2817

2818

2819

2820

2821

impl CacheHashable for Expression {

2822

    fn invalidate_cache(&self) {

2823

        self.meta_ref()

2824

            .stored_hash

2825

            .store(NO_HASH, Ordering::Relaxed);

2826

2827

2828

    fn invalidate_cache_recursive(&self) {

2829

        self.invalidate_cache();

2830

        self.for_each_expr_child(&mut |child| {

2831

            child.invalidate_cache_recursive();

2832

});

2833

2834

2835

    fn get_cached_hash(&self) -> u64 {

2836

        let stored = self.meta_ref().stored_hash.load(Ordering::Relaxed);

2837

        if stored != NO_HASH {

2838

            HASH_HITS.fetch_add(1, Ordering::Relaxed);

2839

            return stored;

2840

2841

        HASH_MISSES.fetch_add(1, Ordering::Relaxed);

2842

        self.calculate_hash()

2843

2844

2845

    fn calculate_hash(&self) -> u64 {

2846

        let mut hasher = DefaultHasher::new();

2847

        std::mem::discriminant(self).hash(&mut hasher);

2848

        match self {

2849

            // Special Case

2850

            Expression::AbstractLiteral(_, alit) => match alit {

2851

                AbstractLiteral::Set(v)

2852

                | AbstractLiteral::MSet(v)

2853

                | AbstractLiteral::Tuple(v)

2854

                | AbstractLiteral::Sequence(v) => {

2855

                    for expr in v {

2856

                        expr.get_cached_hash().hash(&mut hasher);

2857

2858

2859

                AbstractLiteral::Matrix(v, domain) => {

2860

                    domain.hash(&mut hasher);

2861

                    for expr in v {

2862

                        expr.get_cached_hash().hash(&mut hasher);

2863

2864

2865

                AbstractLiteral::Record(rs) => {

2866

                    for r in rs {

2867

                        r.name.hash(&mut hasher);

2868

                        r.value.get_cached_hash().hash(&mut hasher);

2869

2870

2871

                AbstractLiteral::Function(vs) => {

2872

                    for (a, b) in vs {

2873

                        a.get_cached_hash().hash(&mut hasher);

2874

                        b.get_cached_hash().hash(&mut hasher);

2875

2876

2877

                AbstractLiteral::Variant(v) => {

2878

                    v.name.hash(&mut hasher);

2879

                    v.value.get_cached_hash().hash(&mut hasher);

2880

2881

                AbstractLiteral::Relation(v) => {

2882

                    for exprs in v {

2883

                        for expr in exprs {

2884

                            expr.get_cached_hash().hash(&mut hasher);

2885

2886

2887

2888

                AbstractLiteral::Partition(v) => {

2889

                    for exprs in v {

2890

                        for expr in exprs {

2891

                            expr.get_cached_hash().hash(&mut hasher);

2892

2893

2894

2895

},

2896

            Expression::Root(_, vs) => {

2897

                for expr in vs {

2898

                    expr.get_cached_hash().hash(&mut hasher);

2899

2900

2901

2902

            // Moo<Expression>

2903

            Expression::DominanceRelation(_, m1)

2904

            | Expression::ToInt(_, m1)

2905

            | Expression::Abs(_, m1)

2906

            | Expression::Sum(_, m1)

2907

            | Expression::Product(_, m1)

2908

            | Expression::Min(_, m1)

2909

            | Expression::Max(_, m1)

2910

            | Expression::Not(_, m1)

2911

            | Expression::Or(_, m1)

2912

            | Expression::And(_, m1)

2913

            | Expression::Neg(_, m1)

2914

            | Expression::Defined(_, m1)

2915

            | Expression::AllDiff(_, m1)

2916

            | Expression::Factorial(_, m1)

2917

            | Expression::Participants(_, m1)

2918

            | Expression::Parts(_, m1)

2919

            | Expression::Range(_, m1)

2920

            | Expression::ToSet(_, m1)

2921

            | Expression::ToMSet(_, m1)

2922

            | Expression::ToRelation(_, m1)

2923

            | Expression::Card(_, m1) => {

2924

                m1.get_cached_hash().hash(&mut hasher);

2925

2926

2927

            // Moo<Expression> + Moo<Expression>

2928

            Expression::Table(_, m1, m2)

2929

            | Expression::NegativeTable(_, m1, m2)

2930

            | Expression::Bubble(_, m1, m2)

2931

            | Expression::Imply(_, m1, m2)

2932

            | Expression::Iff(_, m1, m2)

2933

            | Expression::Union(_, m1, m2)

2934

            | Expression::In(_, m1, m2)

2935

            | Expression::Intersect(_, m1, m2)

2936

            | Expression::Supset(_, m1, m2)

2937

            | Expression::SupsetEq(_, m1, m2)

2938

            | Expression::Subset(_, m1, m2)

2939

            | Expression::SubsetEq(_, m1, m2)

2940

            | Expression::Eq(_, m1, m2)

2941

            | Expression::Neq(_, m1, m2)

2942

            | Expression::Geq(_, m1, m2)

2943

            | Expression::Leq(_, m1, m2)

2944

            | Expression::Gt(_, m1, m2)

2945

            | Expression::Lt(_, m1, m2)

2946

            | Expression::Apart(_, m1, m2)

2947

            | Expression::Together(_, m1, m2)

2948

            | Expression::Party(_, m1, m2)

2949

            | Expression::SafeDiv(_, m1, m2)

2950

            | Expression::UnsafeDiv(_, m1, m2)

2951

            | Expression::SafeMod(_, m1, m2)

2952

            | Expression::UnsafeMod(_, m1, m2)

2953

            | Expression::UnsafePow(_, m1, m2)

2954

            | Expression::SafePow(_, m1, m2)

2955

            | Expression::Minus(_, m1, m2)

2956

            | Expression::PairwiseSum(_, m1, m2)

2957

            | Expression::PairwiseProduct(_, m1, m2)

2958

            | Expression::Image(_, m1, m2)

2959

            | Expression::ImageSet(_, m1, m2)

2960

            | Expression::PreImage(_, m1, m2)

2961

            | Expression::Inverse(_, m1, m2)

2962

            | Expression::Restrict(_, m1, m2)

2963

            | Expression::LexLt(_, m1, m2)

2964

            | Expression::LexLeq(_, m1, m2)

2965

            | Expression::LexGt(_, m1, m2)

2966

            | Expression::LexGeq(_, m1, m2)

2967

            | Expression::Subsequence(_, m1, m2)

2968

            | Expression::Substring(_, m1, m2) => {

2969

                m1.get_cached_hash().hash(&mut hasher);

2970

                m2.get_cached_hash().hash(&mut hasher);

2971

2972

            // Moo<Expression> + Vec<Expression>

2973

            Expression::UnsafeIndex(_, m, vs) | Expression::SafeIndex(_, m, vs) => {

2974

                m.get_cached_hash().hash(&mut hasher);

2975

                for v in vs {

2976

                    v.get_cached_hash().hash(&mut hasher);

2977

2978

2979

2980

            // Moo<Expression> + Vec<Option<Expression>>

2981

            Expression::UnsafeSlice(_, m, vs)

2982

            | Expression::SafeSlice(_, m, vs)

2983

            | Expression::RelationProj(_, m, vs) => {

2984

                m.get_cached_hash().hash(&mut hasher);

2985

                for v in vs {

2986

                    match v {

2987

                        Some(e) => e.get_cached_hash().hash(&mut hasher),

2988

                        None => 0u64.hash(&mut hasher),

2989

2990

2991

2992

2993

            // Moo<Expression> + Name

2994

            Expression::RecordField(_, m, n) | Expression::Active(_, m, n) => {

2995

                m.get_cached_hash().hash(&mut hasher);

2996

                n.hash(&mut hasher);

2997

2998

2999

            // Moo<Expression> + DomainPtr

3000

            Expression::InDomain(_, m, d) => {

3001

                m.get_cached_hash().hash(&mut hasher);

3002

                d.hash(&mut hasher);

3003

3004

3005

            // Option<Moo<Expression>> + Moo<Expression>

3006

            Expression::Flatten(_, opt, m) => {

3007

                if let Some(e) = opt {

3008

                    e.get_cached_hash().hash(&mut hasher);

3009

3010

                m.get_cached_hash().hash(&mut hasher);

3011

3012

3013

            // Moo<Expression> + Atom

3014

            Expression::MinionReify(_, m, a) | Expression::MinionReifyImply(_, m, a) => {

3015

                m.get_cached_hash().hash(&mut hasher);

3016

                a.hash(&mut hasher);

3017

3018

3019

            // Reference + Moo<Expression>

3020

            Expression::AuxDeclaration(_, r, m) => {

3021

                r.hash(&mut hasher);

3022

                m.get_cached_hash().hash(&mut hasher);

3023

3024

3025

            // SATIntEncoding + Moo<Expression> + (i32, i32)

3026

            Expression::SATInt(_, enc, m, bounds) => {

3027

                enc.hash(&mut hasher);

3028

                m.get_cached_hash().hash(&mut hasher);

3029

                bounds.hash(&mut hasher);

3030

3031

3032

            // Non-Expression Moo types - hash normally

3033

            Expression::Comprehension(_, c) => c.hash(&mut hasher),

3034

            Expression::AbstractComprehension(_, c) => c.hash(&mut hasher),

3035

3036

            // Leaf types - no Expression children

3037

            Expression::Atomic(_, a) => a.hash(&mut hasher),

3038

            Expression::FromSolution(_, a) => a.hash(&mut hasher),

3039

            Expression::Metavar(_, u) => u.hash(&mut hasher),

3040

3041

            // Two Moo<Atom>

3042

            Expression::FlatAbsEq(_, a1, a2) | Expression::FlatMinusEq(_, a1, a2) => {

3043

                a1.hash(&mut hasher);

3044

                a2.hash(&mut hasher);

3045

3046

3047

            // Three Moo<Atom>

3048

            Expression::FlatProductEq(_, a1, a2, a3)

3049

            | Expression::MinionDivEqUndefZero(_, a1, a2, a3)

3050

            | Expression::MinionModuloEqUndefZero(_, a1, a2, a3)

3051

            | Expression::MinionPow(_, a1, a2, a3) => {

3052

                a1.hash(&mut hasher);

3053

                a2.hash(&mut hasher);

3054

                a3.hash(&mut hasher);

3055

3056

3057

            // Vec<Atom>

3058

            Expression::FlatAllDiff(_, vs) => {

3059

                for v in vs {

3060

                    v.hash(&mut hasher);

3061

3062

3063

3064

            // Vec<Atom> + Atom

3065

            Expression::FlatSumGeq(_, vs, a) | Expression::FlatSumLeq(_, vs, a) => {

3066

                for v in vs {

3067

                    v.hash(&mut hasher);

3068

3069

                a.hash(&mut hasher);

3070

3071

3072

            // Moo<Atom> + Moo<Atom> + Box<Literal>

3073

            Expression::FlatIneq(_, a1, a2, lit) => {

3074

                a1.hash(&mut hasher);

3075

                a2.hash(&mut hasher);

3076

                lit.hash(&mut hasher);

3077

3078

3079

            // Reference + Literal

3080

            Expression::FlatWatchedLiteral(_, r, l) => {

3081

                r.hash(&mut hasher);

3082

                l.hash(&mut hasher);

3083

3084

3085

            // Vec<Literal> + Vec<Atom> + Moo<Atom>

3086

            Expression::FlatWeightedSumLeq(_, lits, atoms, a)

3087

            | Expression::FlatWeightedSumGeq(_, lits, atoms, a) => {

3088

                for l in lits {

3089

                    l.hash(&mut hasher);

3090

3091

                for at in atoms {

3092

                    at.hash(&mut hasher);

3093

3094

                a.hash(&mut hasher);

3095

3096

3097

            // Atom + Vec<i32>

3098

            Expression::MinionWInIntervalSet(_, a, vs) | Expression::MinionWInSet(_, a, vs) => {

3099

                a.hash(&mut hasher);

3100

                for v in vs {

3101

                    v.hash(&mut hasher);

3102

3103

3104

3105

            // Vec<Atom> + Moo<Atom> + Moo<Atom>

3106

            Expression::MinionElementOne(_, vs, a1, a2) => {

3107

                for v in vs {

3108

                    v.hash(&mut hasher);

3109

3110

                a1.hash(&mut hasher);

3111

                a2.hash(&mut hasher);

3112

3113

3114

            // Vec<Atom> + Vec<Atom>

3115

            Expression::FlatLexLt(_, v1, v2) | Expression::FlatLexLeq(_, v1, v2) => {

3116

                for v in v1 {

3117

                    v.hash(&mut hasher);

3118

3119

                for v in v2 {

3120

                    v.hash(&mut hasher);

3121

3122

3123

};

3124

3125

        let result = hasher.finish();

3126

        self.meta_ref().stored_hash.swap(result, Ordering::Relaxed);

3127

        result

3128

3129

3130

3131

#[cfg(test)]

3132

mod tests {

3133

    use crate::matrix_expr;

3134

3135

    use super::*;

3136

3137

    #[test]

3138

1

    fn test_domain_of_constant_sum() {

3139

1

        let c1 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));

3140

1

        let c2 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2)));

3141

1

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![c1, c2]));

3142

1

        assert_eq!(sum.domain_of(), Some(Domain::int(vec![Range::Single(3)])));

3143

1

3144

3145

    #[test]

3146

1

    fn test_domain_of_constant_invalid_type() {

3147

1

        let c1 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));

3148

1

        let c2 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true)));

3149

1

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![c1, c2]));

3150

1

        assert_eq!(sum.domain_of(), None);

3151

1

3152

3153

    #[test]

3154

1

    fn test_domain_of_empty_sum() {

3155

1

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![]));

3156

1

        assert_eq!(sum.domain_of(), None);

3157

1

3158