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::FieldValue;

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=FieldValue<Expression>)]

89

#[biplate(to=FieldValue<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

    /// A matrix index.

131

///

132

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

133

    #[compatible(JsonInput)]

134

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

135

136

    /// A safe matrix index.

137

///

138

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

139

    #[compatible(SMT)]

140

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

141

142

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

143

///

144

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

145

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

146

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

147

///

148

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

149

///

150

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

151

    #[compatible(JsonInput)]

152

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

153

154

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

155

///

156

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

157

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

158

159

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

160

///

161

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

162

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

163

    /// `SafeSlice` respectively.

164

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

165

166

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

167

///

168

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

169

///

170

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

171

    #[compatible(SMT)]

172

    ToInt(Metadata, Moo<Expression>),

173

174

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

175

    #[compatible(JsonInput, SMT)]

176

    Abs(Metadata, Moo<Expression>),

177

178

    /// `sum(<vec_expr>)`

179

    #[compatible(JsonInput, SMT)]

180

    Sum(Metadata, Moo<Expression>),

181

182

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

183

    #[compatible(JsonInput, SMT)]

184

    Product(Metadata, Moo<Expression>),

185

186

    /// `min(<vec_expr>)`

187

    #[compatible(JsonInput, SMT)]

188

    Min(Metadata, Moo<Expression>),

189

190

    /// `max(<vec_expr>)`

191

    #[compatible(JsonInput, SMT)]

192

    Max(Metadata, Moo<Expression>),

193

194

    /// `not(a)`

195

    #[compatible(JsonInput, SAT, SMT)]

196

    Not(Metadata, Moo<Expression>),

197

198

    /// `or(<vec_expr>)`

199

    #[compatible(JsonInput, SAT, SMT)]

200

    Or(Metadata, Moo<Expression>),

201

202

    /// `and(<vec_expr>)`

203

    #[compatible(JsonInput, SAT, SMT)]

204

    And(Metadata, Moo<Expression>),

205

206

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

207

    #[compatible(JsonInput, SMT)]

208

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

209

210

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

211

    #[compatible(JsonInput, SMT)]

212

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

213

214

    #[compatible(JsonInput)]

215

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

216

217

    #[compatible(JsonInput)]

218

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

219

220

    #[compatible(JsonInput)]

221

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

222

223

    #[compatible(JsonInput)]

224

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

225

226

    #[compatible(JsonInput)]

227

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

228

229

    #[compatible(JsonInput)]

230

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

231

232

    #[compatible(JsonInput)]

233

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

234

235

    #[compatible(JsonInput, SMT)]

236

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

237

238

    #[compatible(JsonInput, SMT)]

239

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

240

241

    #[compatible(JsonInput, SMT)]

242

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

243

244

    #[compatible(JsonInput, SMT)]

245

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

246

247

    #[compatible(JsonInput, SMT)]

248

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

249

250

    #[compatible(JsonInput, SMT)]

251

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

252

253

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

254

    /// in the list of values taken by t

255

    #[compatible(JsonInput)]

256

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

257

258

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

259

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

260

    #[compatible(JsonInput)]

261

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

262

263

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

264

    #[compatible(SMT)]

265

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

266

267

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

268

    #[compatible(JsonInput)]

269

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

270

271

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

272

    #[compatible(SMT)]

273

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

274

275

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

276

    #[compatible(JsonInput)]

277

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

278

279

    /// Negation: `-x`

280

    #[compatible(JsonInput, SMT)]

281

    Neg(Metadata, Moo<Expression>),

282

283

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

284

    #[compatible(JsonInput)]

285

    Factorial(Metadata, Moo<Expression>),

286

287

    /// Set of domain values function is defined for

288

    #[compatible(JsonInput)]

289

    Defined(Metadata, Moo<Expression>),

290

291

    /// Set of codomain values function is defined for

292

    #[compatible(JsonInput)]

293

    Range(Metadata, Moo<Expression>),

294

295

    #[compatible(JsonInput)]

296

    ToSet(Metadata, Moo<Expression>),

297

298

    #[compatible(JsonInput)]

299

    ToMSet(Metadata, Moo<Expression>),

300

301

    #[compatible(JsonInput)]

302

    ToRelation(Metadata, Moo<Expression>),

303

304

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

305

///

306

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

307

    #[compatible(JsonInput)]

308

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

309

310

    /// `UnsafePow` after preventing undefinedness

311

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

312

313

    /// Flatten matrix operator

314

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

315

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

316

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

317

318

    /// `allDiff(<vec_expr>)`

319

    #[compatible(JsonInput)]

320

    AllDiff(Metadata, Moo<Expression>),

321

322

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

323

///

324

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

325

    /// allowed rows.

326

    #[compatible(JsonInput)]

327

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

328

329

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

330

///

331

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

332

    /// forbidden rows.

333

    #[compatible(JsonInput)]

334

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

335

    /// Binary subtraction operator

336

///

337

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

338

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

339

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

340

    #[compatible(JsonInput)]

341

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

342

343

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

344

    /// First Expr Arg is a list of elements

345

    /// Second Expr Arg is the partition

346

    #[compatible(JsonInput)]

347

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

348

349

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

350

    /// Expr Arg is a partition

351

    #[compatible(JsonInput)]

352

    Participants(Metadata, Moo<Expression>),

353

354

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

355

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

356

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

357

    #[compatible(JsonInput)]

358

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

359

360

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

361

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

362

    #[compatible(JsonInput)]

363

    Parts(Metadata, Moo<Expression>),

364

365

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

366

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

367

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

368

    #[compatible(JsonInput)]

369

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

370

371

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

372

///

373

    /// Low-level Minion constraint.

374

///

375

    /// # See also

376

///

377

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

378

    #[compatible(Minion)]

379

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

380

381

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

382

///

383

    /// Low-level Minion constraint.

384

///

385

    /// # See also

386

///

387

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

388

    #[compatible(Minion)]

389

    FlatAllDiff(Metadata, Vec<Atom>),

390

391

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

392

///

393

    /// Low-level Minion constraint.

394

///

395

    /// # See also

396

///

397

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

398

    #[compatible(Minion)]

399

    FlatSumGeq(Metadata, Vec<Atom>, 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#sumleq)

408

    #[compatible(Minion)]

409

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

410

411

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

412

///

413

    /// Low-level Minion constraint.

414

///

415

    /// # See also

416

///

417

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

418

    #[compatible(Minion)]

419

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

420

421

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

422

///

423

    /// Low-level Minion constraint.

424

///

425

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

426

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

427

    /// watched-and and watched-or.

428

///

429

    /// # See also

430

///

431

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

432

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

433

    #[compatible(Minion)]

434

    #[polyquine_skip]

435

    FlatWatchedLiteral(Metadata, Reference, Literal),

436

437

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

438

    /// product of cs and xs.

439

///

440

    /// Low-level Minion constraint.

441

///

442

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

443

///

444

    /// # See also

445

///

446

    /// + [Minion

447

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

448

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

449

450

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

451

    /// product of cs and xs.

452

///

453

    /// Low-level Minion constraint.

454

///

455

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

456

///

457

    /// # See also

458

///

459

    /// + [Minion

460

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

461

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

462

463

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

464

///

465

    /// Low-level Minion constraint.

466

///

467

    /// # See also

468

///

469

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

470

    #[compatible(Minion)]

471

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

472

473

    /// Ensures that x*y=z.

474

///

475

    /// Low-level Minion constraint.

476

///

477

    /// # See also

478

///

479

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

480

    #[compatible(Minion)]

481

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

482

483

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

484

///

485

    /// Low-level Minion constraint.

486

///

487

    /// # See also

488

///

489

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

490

    #[compatible(Minion)]

491

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

492

493

    /// Ensures that 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#mod_undefzero)

500

    #[compatible(Minion)]

501

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

502

503

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

504

///

505

    /// Low-level Minion constraint.

506

///

507

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

508

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

509

///

510

    /// # See also

511

///

512

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

513

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

514

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

515

516

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

517

    /// variable.

518

///

519

    /// Low-level Minion constraint.

520

///

521

    /// # See also

522

///

523

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

524

    #[compatible(Minion)]

525

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

526

527

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

528

    /// variable.

529

///

530

    /// Low-level Minion constraint.

531

///

532

    /// # See also

533

///

534

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

535

    #[compatible(Minion)]

536

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

537

538

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

539

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

540

///

541

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

542

///

543

    /// Low-level Minion constraint.

544

///

545

    /// # See also

546

    ///>

547

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

548

    #[compatible(Minion)]

549

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

550

551

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

552

///

553

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

554

///

555

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

556

///

557

    /// Low-level Minion constraint.

558

///

559

    /// # See also

560

///

561

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

562

    #[compatible(Minion)]

563

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

564

565

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

566

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

567

///

568

    /// Low-level Minion constraint.

569

///

570

    /// # See also

571

///

572

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

573

    #[compatible(Minion)]

574

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

575

576

    /// Declaration of an auxiliary variable.

577

///

578

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

579

    #[compatible(Minion)]

580

    #[polyquine_skip]

581

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

582

583

    /// 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.

584

    #[compatible(SAT)]

585

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

586

587

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

588

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

589

    #[compatible(SMT)]

590

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

591

592

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

593

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

594

    #[compatible(SMT)]

595

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

596

597

    #[compatible(JsonInput)]

598

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

599

600

    #[compatible(JsonInput)]

601

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

602

603

    #[compatible(JsonInput)]

604

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

605

606

    #[compatible(JsonInput)]

607

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

608

609

    #[compatible(JsonInput)]

610

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

611

612

    /// Lexicographical < between two matrices.

613

///

614

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

615

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

616

    /// then j comes after i.

617

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

618

///

619

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

620

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

621

622

    /// Lexicographical <= between two matrices

623

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

624

625

    /// Lexicographical > between two matrices

626

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

627

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

628

629

    /// Lexicographical >= between two matrices

630

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

631

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

632

633

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

634

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

635

636

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

637

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

638

639

    /// To tell which field is used in a variant domain

640

    #[compatible(JsonInput)]

641

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

642

643

    /// Alters the shape of relations by projection

644

    #[compatible(JsonInput)]

645

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

646

647

    /// Cardinality of a collection type

648

    #[compatible(JsonInput)]

649

    Card(Metadata, Moo<Expression>),

650

651

652

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

653

// child expression.

654

//

655

// Op must be monotonic.

656

//

657

// Returns none if unbounded

658

1829355

fn bounded_i32_domain_for_matrix_literal_monotonic(

659

1829355

    e: &Expression,

660

1829355

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

661

1829355

) -> Option<DomainPtr> {

662

    // only care about the elements, not the indices

663

1829355

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

664

665

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

666

//

667

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

668

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

669

    // [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))].

670

//

671

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

672

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

673

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

674

    //Int

675

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

676

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

677

//

678

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

679

680

1807523

    let expr = exprs.pop()?;

681

1807522

    let dom = expr.domain_of()?;

682

1804762

    let resolved = dom.resolve()?;

683

1804402

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

684

13

        return None;

685

};

686

687

1804389

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

688

689

2053175

    for expr in exprs {

690

2053175

        let dom = expr.domain_of()?;

691

2052815

        let resolved = dom.resolve()?;

692

2052695

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

693

            return None;

694

};

695

696

2052695

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

697

698

        // all the possible new values for current_min / current_max

699

2052695

        let minmax = op(min, current_max)?;

700

2052695

        let minmin = op(min, current_min)?;

701

2052695

        let maxmin = op(max, current_min)?;

702

2052695

        let maxmax = op(max, current_max)?;

703

2052695

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

704

705

2052695

        current_min = *vals

706

2052695

            .iter()

707

2052695

            .min()

708

2052695

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

709

2052695

        current_max = *vals

710

2052695

            .iter()

711

2052695

            .max()

712

2052695

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

713

714

715

1803909

    if current_min == current_max {

716

1061

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

717

    } else {

718

1802848

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

719

720

1829355

721

722

10

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

723

10

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

724

10

    elem_domain.as_ref().as_int()?;

725

10

    Some(elem_domain)

726

10

727

728

// Returns none if unbounded

729

3857084

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

730

3857084

    let mut min = i32::MAX;

731

3857084

    let mut max = i32::MIN;

732

3876232

    for r in ranges {

733

3876232

        match r {

734

1385046

            Range::Single(i) => {

735

1385046

                if *i < min {

736

1365898

                    min = *i;

737

1365898

738

1385046

                if *i > max {

739

1385046

                    max = *i;

740

1385046

741

742

2491186

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

743

2491186

                if *i < min {

744

2491186

                    min = *i;

745

2491186

746

2491186

                if *j > max {

747

2491186

                    max = *j;

748

2491186

749

750

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

751

752

753

3857084

    Some((min, max))

754

3857084

755

756

impl Expression {

757

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

758

9102680

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

759

9102680

        match self {

760

96

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

761

96

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

762

96

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

763

)),

764

90

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

765

90

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

766

90

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

767

)),

768

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

769

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

770

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

771

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

772

6

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

773

198020

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

774

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

775

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

776

144

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

777

26

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

778

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

779

729804

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

780

750482

                let dom = matrix.domain_of()?;

781

750482

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

782

750482

                    return Some(elem_domain);

783

784

785

                // may actually use the value in the future

786

                #[allow(clippy::redundant_pattern_matching)]

787

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

788

                    // TODO: We can implement proper indexing for tuples

789

                    return None;

790

791

792

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

793

                    let index_expr = index.first()?;

794

                    return match index_expr {

795

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

796

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

797

                            for inner_dom in doms {

798

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

799

                                    return Some(inner_dom.domain);

800

801

802

                            None

803

804

                        _ => None,

805

};

806

807

808

                bug!("subject of an index operation should support indexing")

809

810

            Expression::UnsafeSlice(_, matrix, indices)

811

480

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

812

480

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

813

814

480

                let dom = matrix.domain_of()?;

815

480

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

816

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

817

};

818

819

480

                match sliced_dimension {

820

480

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

821

480

                        elem_domain,

822

480

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

823

480

)),

824

825

                    // same as index

826

                    None => Some(elem_domain),

827

828

829

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

830

5826319

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

831

1230431

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

832

5848268

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

833

834

591474

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

835

2321232

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

836

837

24960

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

838

24960

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

839

24960

})

840

4240

            .or_else(|| matrix_element_domain(e)),

841

16330

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

842

16320

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

843

16320

})

844

3210

            .or_else(|| matrix_element_domain(e)),

845

2120

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

846

2120

                .domain_of()?

847

2120

                .resolve()?

848

2120

                .apply_i32(

849

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

850

                    // including for negative numbers.

851

56800

                    |x, y| {

852

56800

                        if y != 0 {

853

49720

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

854

                        } else {

855

7080

                            None

856

857

56800

},

858

2120

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

859

860

2120

                .map(DomainPtr::from)

861

2120

                .ok(),

862

21720

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

863

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

864

                // including for negative numbers.

865

21720

                let domain = a

866

21720

                    .domain_of()?

867

21720

                    .resolve()?

868

21720

                    .apply_i32(

869

897680

                        |x, y| {

870

897680

                            if y != 0 {

871

780040

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

872

                            } else {

873

117640

                                None

874

875

897680

},

876

21720

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

877

878

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

879

880

21720

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

881

21720

                    let mut ranges = ranges;

882

21720

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

883

21720

                    Some(Domain::int(ranges))

884

                } else {

885

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

886

887

888

800

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

889

800

                .domain_of()?

890

800

                .resolve()?

891

800

                .apply_i32(

892

12040

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

893

800

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

894

895

800

                .map(DomainPtr::from)

896

800

                .ok(),

897

6960

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

898

6960

                let domain = a

899

6960

                    .domain_of()?

900

6960

                    .resolve()?

901

6960

                    .apply_i32(

902

250320

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

903

6960

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

904

905

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

906

907

6960

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

908

6960

                    let mut ranges = ranges;

909

6960

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

910

6960

                    Some(Domain::int(ranges))

911

                } else {

912

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

913

914

915

5350

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

916

5350

                .domain_of()?

917

5350

                .resolve()?

918

5350

                .apply_i32(

919

162720

                    |x, y| {

920

162720

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

921

147520

                            Some(x.pow(y as u32))

922

                        } else {

923

15200

                            None

924

925

162720

},

926

5350

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

927

928

5350

                .map(DomainPtr::from)

929

5350

                .ok(),

930

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

931

320

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

932

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

933

31366

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

934

400

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

935

320

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

936

4228

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

937

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

938

16138

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

939

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

940

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

941

1720

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

942

82

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

943

2

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

944

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

945

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

946

80

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

947

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

948

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

949

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

950

360

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

951

804

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

952

804

                if let Some(expr) = n {

953

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

954

                        // TODO: handle flatten with depth argument

955

                        return None;

956

957

                } else {

958

                    // TODO: currently only works for matrices

959

804

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

960

800

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

961

800

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

962

                        _ => return None,

963

};

964

800

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

965

966

800

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

967

800

                    return Some(Domain::matrix(

968

800

                        val_dom.clone().into(),

969

800

                        vec![new_index_domain],

970

800

));

971

972

                None

973

974

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

975

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

976

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

977

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

978

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

979

4820

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

980

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

981

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

982

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

983

7366

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

984

7366

                let dom = x.domain_of()?;

985

7366

                let mut ranges = dom.as_int()?;

986

987

4606

                ranges = ranges

988

4606

                    .into_iter()

989

4606

                    .map(|r| match r {

990

840

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

991

3766

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

992

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

993

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

994

                        Range::Unbounded => Range::Unbounded,

995

4606

})

996

4606

                    .collect();

997

998

4606

                Some(Domain::int(ranges))

999

1000

375854

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

1001

375854

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

1002

375854

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

1003

1004

375852

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

1005

375852

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

1006

1007

375852

                    a_resolved

1008

1203030

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

1009

375852

                        .map(DomainPtr::from)

1010

375852

                        .ok()

1011

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

1012

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

1013

1014

                    Some(DomainPtr::from(a_resolved))

1015

                } else {

1016

                    None

1017

1018

1019

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

1020

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

1021

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

1022

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

1023

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

1024

5640

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

1025

5640

                .domain_of()?

1026

5640

                .resolve()?

1027

953360

                .apply_i32(|a, _| Some(a.abs()), a.domain_of()?.resolve()?.as_ref())

1028

5640

                .map(DomainPtr::from)

1029

5640

                .ok(),

1030

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

1031

4204

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

1032

3840

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

1033

3840

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

1034

1035

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

1036

                .domain_of()?

1037

                .resolve()?

1038

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

1039

                .map(DomainPtr::from)

1040

                .ok(),

1041

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

1042

                .domain_of()?

1043

                .resolve()?

1044

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

1045

                .map(DomainPtr::from)

1046

                .ok(),

1047

16

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

1048

16

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

1049

16

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

1050

16

                if let Some(size) = size {

1051

14

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

1052

                } else {

1053

2

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

1054

2

                        domain.return_type(),

1055

2

                    ))))

1056

1057

1058

22

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

1059

22

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

1060

22

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

1061

1062

22

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

1063

22

                let size_size = match size_size {

1064

10

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

1065

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

1066

4

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

1067

2

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

1068

2

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

1069

},

1070

                    // Upper bound guarantees the same upper bound

1071

2

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

1072

                    // If not bounded by 0 can guarantee min 1

1073

4

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

1074

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

1075

2

                            Range::UnboundedR(x)

1076

1077

2

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

1078

},

1079

2

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

1080

};

1081

1082

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

1083

22

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

1084

22

                let codomain_length = codomain.length_signed();

1085

22

                let attr_size = match jectivity {

1086

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

1087

6

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

1088

6

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

1089

                        Err(_) => None,

1090

},

1091

                    JectivityAttr::Injective => {

1092

8

                        let domain_length = domain.length_signed();

1093

8

                        match domain_length {

1094

8

                            Ok(len) => match codomain_length {

1095

8

                                Ok(co_len) => match partiality {

1096

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

1097

                                    PartialityAttr::Total => {

1098

2

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

1099

1100

                                    PartialityAttr::Partial => {

1101

6

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

1102

1103

},

1104

                                Err(_) => None,

1105

},

1106

                            Err(_) => None,

1107

1108

1109

                    JectivityAttr::None => {

1110

8

                        let domain_length = domain.length_signed();

1111

8

                        match domain_length {

1112

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

1113

8

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

1114

                            Err(_) => None,

1115

1116

1117

};

1118

1119

22

                let size = match attr_size {

1120

22

                    Some(attr_size) => {

1121

22

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

1122

22

                        match unsafe_range {

1123

22

                            Ok(range) => range,

1124

                            Err(_) => {

1125

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

1126

                                    domain.return_type(),

1127

                                ))));

1128

1129

1130

1131

                    None => size_size,

1132

};

1133

22

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

1134

1135

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

1136

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

1137

                let codomain = get_function_codomain(function);

1138

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

1139

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

1140

1141

22

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

1142

22

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

1143

1144

22

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

1145

22

                let size_size = match size_size {

1146

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

1147

10

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

1148

4

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

1149

2

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

1150

4

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

1151

2

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

1152

};

1153

1154

22

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

1155

22

                let codomain_length = codomain.length_signed();

1156

22

                let attr_size = match jectivity {

1157

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

1158

2

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

1159

8

                    JectivityAttr::Injective => match size_size {

1160

2

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

1161

2

                            match codomain_length {

1162

2

                                Ok(co_len) => {

1163

2

                                    if x >= co_len {

1164

                                        Some(Range::Single(1))

1165

                                    } else {

1166

2

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

1167

1168

1169

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

1170

1171

1172

6

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

1173

},

1174

                    JectivityAttr::Surjective => {

1175

4

                        let domain_length = domain.length_signed();

1176

4

                        match domain_length {

1177

4

                            Ok(len) => match codomain_length {

1178

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

1179

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

1180

4

                                Ok(co_len) => match size_size {

1181

2

                                    Range::Bounded(_, x)

1182

                                    | Range::UnboundedL(x)

1183

2

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

1184

2

1,

1185

2

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

1186

2

)),

1187

2

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

1188

},

1189

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

1190

},

1191

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

1192

1193

1194

                    JectivityAttr::None => {

1195

8

                        let domain_length = domain.length_signed();

1196

8

                        match domain_length {

1197

8

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

1198

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

1199

1200

1201

};

1202

1203

22

                let size = match attr_size {

1204

22

                    Some(attr_size) => {

1205

22

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

1206

22

                        match unsafe_range {

1207

22

                            Ok(range) => range,

1208

                            Err(_) => {

1209

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

1210

                                    domain.return_type(),

1211

                                ))));

1212

1213

1214

1215

                    None => size_size,

1216

};

1217

22

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

1218

1219

8

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

1220

8

                let mut domain = function.domain_of()?;

1221

8

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

1222

1223

                // Stops other references being mutable

1224

8

                let attrs: &FuncAttr<IntVal> = attrs_mut;

1225

8

                let codom: &Moo<Domain> = codom_mut;

1226

1227

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

1228

8

                let mut new_dom = new_domain.domain_of()?;

1229

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

1230

8

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

1231

8

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

1232

1233

8

                    new_rng.append(old_rng);

1234

8

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

1235

8

                        let ranges = vec![rng];

1236

8

                        new_dom = Domain::int(ranges);

1237

8

1238

1239

8

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

1240

8

                let new_size = match new_dom.length_signed() {

1241

                    // Combines current size attributes with length of new domain

1242

8

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

1243

6

                        Ok(size) => size,

1244

                        Err(_) => {

1245

                            // Means the restriction is impossible

1246

2

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

1247

2

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

1248

2

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

1249

2

                            )));

1250

1251

},

1252

                    Err(_) => attr_size,

1253

};

1254

6

                let jectivity = attrs.jectivity.clone();

1255

6

                let partiality = attrs.partiality.clone();

1256

6

                let new_attrs = FuncAttr {

1257

6

                    size: new_size,

1258

6

                    jectivity,

1259

6

                    partiality,

1260

6

};

1261

6

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

1262

1263

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

1264

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

1265

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

1266

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

1267

3080

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

1268

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

1269

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

1270

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

1271

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

1272

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

1273

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

1274

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

1275

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

1276

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

1277

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

1278

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

1279

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

1280

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

1281

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

1282

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

1283

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

1284

                    // We combine all matrix domains into a tuple

1285

                    let mut doms = vec![];

1286

                    for _ in dimensions {

1287

                        doms.push(dom.clone());

1288

1289

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

1290

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

1291

                    let attr = match doms_sizes {

1292

                        Ok(vals) => {

1293

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

1294

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

1295

                            } else {

1296

                                SetAttr::<i32>::default()

1297

1298

1299

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

1300

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

1301

};

1302

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

1303

                } else {

1304

                    bug!(

1305

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

1306

1307

1308

1309

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

1310

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

1311

                    let set_attrs = MSetAttr {

1312

                        size: attrs.size,

1313

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

1314

};

1315

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

1316

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

1317

                    let set_attrs = MSetAttr {

1318

                        size: attrs.size,

1319

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

1320

};

1321

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

1322

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

1323

                    let set_attrs = MSetAttr {

1324

                        size: attrs.size,

1325

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

1326

};

1327

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

1328

                } else {

1329

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

1330

1331

1332

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

1333

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

1334

                // Function attributes apply to the relation

1335

                let rel_attrs = RelAttr {

1336

                    size: attrs.size,

1337

                    binary: vec![],

1338

};

1339

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

1340

1341

2

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

1342

2

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

1343

2

                let new_doms = domains

1344

2

                    .iter()

1345

2

                    .zip(projections.iter())

1346

6

                    .filter_map(|(domain, included)| {

1347

6

                        if included.is_none() {

1348

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

1349

4

                            Some(domain.clone())

1350

                        } else {

1351

2

                            None

1352

1353

6

})

1354

2

                    .collect();

1355

2

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

1356

1357

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

1358

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

1359

4

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

1360

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

1361

4

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

1362

4

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

1363

1364

4

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

1365

4

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

1366

1367

                // if

1368

4

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

1369

2

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

1370

2

                        let lo = p * r;

1371

2

                        let hi = q * s;

1372

2

                        if len < lo || len > hi {

1373

2

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

1374

2

                                inner.return_type(),

1375

2

                            ))));

1376

1377

1378

1379

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

1380

                        let hi = q * s;

1381

                        if len > hi {

1382

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

1383

                                inner.return_type(),

1384

                            ))));

1385

1386

1387

1388

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

1389

                        let lo = p * r;

1390

                        if len < lo {

1391

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

1392

                                inner.return_type(),

1393

                            ))));

1394

1395

1396

1397

2

                    _ => {}

1398

1399

1400

2

                Some(Domain::set(

1401

2

                    SetAttr::new_size(len),

1402

2

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

1403

))

1404

1405

2

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

1406

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

1407

2

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

1408

1409

2

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

1410

1411

4

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

1412

4

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

1413

1414

4

                Some(Domain::set(

1415

4

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

1416

4

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

1417

4

))

1418

1419

8

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

1420

8

                let domain = collection.domain_of()?;

1421

8

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

1422

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

1423

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

1424

                    if let Ok(doms_ground) = doms_ground {

1425

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

1426

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

1427

                    } else {

1428

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

1429

1430

8

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

1431

2

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

1432

2

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

1433

2

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

1434

2

                        match unsafe_range {

1435

2

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

1436

                            Err(_) => return None,

1437

1438

1439

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

1440

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

1441

6

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

1442

2

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

1443

2

                    let attr_occ_range = attrs.resolve()?.occurrence;

1444

                    // Gets maximum value of the occurrence

1445

2

                    let attr_occ = match attr_occ_range {

1446

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

1447

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

1448

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

1449

2

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

1450

};

1451

2

                    if let Some(occ) = attr_occ {

1452

2

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

1453

2

                            let unsafe_range =

1454

2

                                Range::minimal(&[attr_size, Range::Bounded(0, length * occ)]);

1455

2

                            match unsafe_range {

1456

2

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

1457

                                Err(_) => None,

1458

1459

                        } else {

1460

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

1461

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

1462

1463

                    } else {

1464

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

1465

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

1466

1467

4

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

1468

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

1469

1470

2

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

1471

                    // See if all domains are ground

1472

2

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

1473

6

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

1474

2

                    if let Ok(doms_sizes) = doms_sizes {

1475

2

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

1476

                        // Combine the attributes and the domain possibilities

1477

2

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

1478

2

                        match unsafe_range {

1479

2

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

1480

                            Err(_) => return None,

1481

1482

1483

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

1484

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

1485

2

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

1486

2

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

1487

2

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

1488

                } else {

1489

                    bug!(

1490

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

1491

1492

1493

1494

1495

9102680

1496

1497

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

1498

18

    fn function_elements_size(

1499

18

        attrs: FuncAttr<IntVal>,

1500

18

        domain: &DomainPtr,

1501

18

        codomain: &DomainPtr,

1502

18

    ) -> Option<Range> {

1503

        // Gets the size imposed by the size attribute

1504

        // The elements defined in the domain is the same as the size of the function itself

1505

18

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

1506

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

1507

18

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

1508

18

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

1509

18

        let domain_length = domain.length_signed();

1510

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

1511

18

        let attr_size = match domain_length {

1512

18

            Ok(len) => match partiality {

1513

2

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

1514

                PartialityAttr::Partial => {

1515

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

1516

16

                    let codomain_length = codomain.length_signed();

1517

16

                    match codomain_length {

1518

16

                        Ok(co_len) => match jectivity {

1519

4

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

1520

4

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

1521

                            JectivityAttr::Injective => {

1522

6

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

1523

1524

2

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

1525

},

1526

                        Err(_) => None,

1527

1528

1529

},

1530

            Err(_) => None,

1531

};

1532

        // We combine the sizes:

1533

        // size_size relates to size constraints imposed by the size attributes of the function

1534

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

1535

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

1536

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

1537

18

        match attr_size {

1538

18

            Some(attr_size) => {

1539

18

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

1540

18

                unsafe_range.ok()

1541

1542

            None => Some(size_size),

1543

1544

18

1545

1546

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

1547

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

1548

        macro_rules! match_meta_ref {

1549

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

1550

                match self {

1551

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

1552

1553

};

1554

1555

        match_meta_ref!(

1556

            AbstractLiteral,

1557

            Root,

1558

            Bubble,

1559

            Comprehension,

1560

            AbstractComprehension,

1561

            DominanceRelation,

1562

            FromSolution,

1563

            Metavar,

1564

            Atomic,

1565

            UnsafeIndex,

1566

            SafeIndex,

1567

            UnsafeSlice,

1568

            SafeSlice,

1569

            InDomain,

1570

            ToInt,

1571

            Abs,

1572

            Sum,

1573

            Product,

1574

            Min,

1575

            Max,

1576

            Not,

1577

Or,

1578

            And,

1579

            Imply,

1580

            Iff,

1581

            Union,

1582

In,

1583

            Intersect,

1584

            Supset,

1585

            SupsetEq,

1586

            Subset,

1587

            SubsetEq,

1588

Eq,

1589

            Neq,

1590

            Geq,

1591

            Leq,

1592

Gt,

1593

Lt,

1594

            SafeDiv,

1595

            UnsafeDiv,

1596

            SafeMod,

1597

            UnsafeMod,

1598

            Apart,

1599

            Together,

1600

            Participants,

1601

            Party,

1602

            Parts,

1603

            Neg,

1604

            Defined,

1605

            Range,

1606

            UnsafePow,

1607

            SafePow,

1608

            Flatten,

1609

            AllDiff,

1610

            Minus,

1611

            Factorial,

1612

            FlatAbsEq,

1613

            FlatAllDiff,

1614

            FlatSumGeq,

1615

            FlatSumLeq,

1616

            FlatIneq,

1617

            FlatWatchedLiteral,

1618

            FlatWeightedSumLeq,

1619

            FlatWeightedSumGeq,

1620

            FlatMinusEq,

1621

            FlatProductEq,

1622

            MinionDivEqUndefZero,

1623

            MinionModuloEqUndefZero,

1624

            MinionPow,

1625

            MinionReify,

1626

            MinionReifyImply,

1627

            MinionWInIntervalSet,

1628

            MinionWInSet,

1629

            MinionElementOne,

1630

            AuxDeclaration,

1631

            SATInt,

1632

            PairwiseSum,

1633

            PairwiseProduct,

1634

            Image,

1635

            ImageSet,

1636

            PreImage,

1637

            Inverse,

1638

            Restrict,

1639

            LexLt,

1640

            LexLeq,

1641

            LexGt,

1642

            LexGeq,

1643

            FlatLexLt,

1644

            FlatLexLeq,

1645

            NegativeTable,

1646

            Table,

1647

            Active,

1648

            ToSet,

1649

            ToMSet,

1650

            ToRelation,

1651

            RelationProj,

1652

            Card,

1653

            Subsequence,

1654

            Substring,

1655

1656

1657

1658

    pub fn get_meta(&self) -> Metadata {

1659

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

1660

        metas[0].clone()

1661

1662

1663

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

1664

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

1665

1666

1667

    /// Checks whether this expression is safe.

1668

///

1669

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

1670

///

1671

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

1672

    /// safe through the use of bubble rules.

1673

5266174

    pub fn is_safe(&self) -> bool {

1674

        // TODO: memoise in Metadata

1675

42781776

        for expr in self.universe() {

1676

42781776

            match expr {

1677

                Expression::UnsafeDiv(_, _, _)

1678

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

1679

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

1680

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

1681

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

1682

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

1683

807154

                    return false;

1684

1685

41974622

                _ => {}

1686

1687

1688

4459020

        true

1689

5266174

1690

1691

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

1692

14732496

    pub fn is_associative_commutative_operator(&self) -> bool {

1693

14732496

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

1694

14732496

1695

1696

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

1697

///

1698

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

1699

    /// [`Expression`].

1700

8280

    pub fn is_matrix_literal(&self) -> bool {

1701

        matches!(

1702

8280

            self,

1703

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

1704

                | Expression::Atomic(

1705

_,

1706

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

1707

1708

1709

8280

1710

1711

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

1712

///

1713

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

1714

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

1715

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

1716

2522436

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

1717

2522436

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

1718

2522436

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

1719

1720

2522436

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

1721

562996

            atom2 == atom1

1722

        } else {

1723

1959440

            false

1724

1725

2522436

1726

1727

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

1728

///

1729

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

1730

    /// any explicitly specified domain.

1731

8659214

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

1732

7448470

        match self {

1733

7448470

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

1734

7448470

                matrix.unwrap_list().cloned()

1735

1736

            Expression::Atomic(

1737

_,

1738

28024

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

1739

28024

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

1740

23844

                elems

1741

23844

                    .clone()

1742

23844

                    .into_iter()

1743

66018

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

1744

23844

                    .collect_vec()

1745

23844

}),

1746

1182720

            _ => None,

1747

1748

8659214

1749

1750

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

1751

///

1752

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

1753

///

1754

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

1755

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

1756

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

1757

11899709

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

1758

8198573

        match self {

1759

8198573

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

1760

8198573

                Some((elems, domain))

1761

1762

            Expression::Atomic(

1763

_,

1764

439672

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

1765

            ) => Some((

1766

439672

                elems

1767

439672

                    .into_iter()

1768

1015212

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

1769

439672

                    .collect_vec(),

1770

439672

                domain.into(),

1771

)),

1772

1773

3261464

            _ => None,

1774

1775

11899709

1776

1777

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

1778

///

1779

    /// # Panics

1780

    /// Panics if the expression is not Root.

1781

27980

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

1782

27980

        match self {

1783

27980

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

1784

27980

                children.extend(exprs);

1785

27980

                Expression::Root(meta, children)

1786

1787

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

1788

1789

27980

1790

1791

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

1792

158262

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

1793

148532

        match self {

1794

138578

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

1795

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

1796

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

1797

1798

6302

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

1799

6302

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

1800

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

1801

};

1802

1803

6300

                Some(Literal::Int(-i))

1804

1805

1806

13382

            _ => None,

1807

1808

158262

1809

1810

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

1811

15973716

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

1812

15973716

        TryFrom::try_from(self).ok()

1813

15973716

1814

1815

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

1816

91836

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

1817

91836

        self.universe()

1818

91836

            .into_iter()

1819

1093382

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

1820

91836

            .collect()

1821

91836

1822

1823

1824

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

1825

    let function_domain = function.domain_of()?;

1826

    match function_domain.resolve().as_ref() {

1827

        Some(d) => {

1828

            match d.as_ref() {

1829

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

1830

                // Not defined for anything other than a function

1831

                _ => None,

1832

1833

1834

        None => {

1835

            match function_domain.as_unresolved()? {

1836

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

1837

                // Not defined for anything other than a function

1838

                _ => None,

1839

1840

1841

1842

1843

1844

impl TryFrom<&Expression> for i32 {

1845

    type Error = ();

1846

1847

956470

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

1848

956470

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

1849

740038

            return Err(());

1850

};

1851

1852

216432

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

1853

215772

            return Err(());

1854

};

1855

1856

660

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

1857

            return Err(());

1858

};

1859

1860

660

        Ok(*i)

1861

956470

1862

1863

1864

impl TryFrom<Expression> for i32 {

1865

    type Error = ();

1866

1867

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

1868

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

1869

1870

1871

impl From<i32> for Expression {

1872

71096

    fn from(i: i32) -> Self {

1873

71096

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

1874

71096

1875

1876

1877

impl From<bool> for Expression {

1878

38222

    fn from(b: bool) -> Self {

1879

38222

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

1880

38222

1881

1882

1883

impl From<Atom> for Expression {

1884

5494

    fn from(value: Atom) -> Self {

1885

5494

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

1886

5494

1887

1888

1889

impl From<Literal> for Expression {

1890

7040

    fn from(value: Literal) -> Self {

1891

7040

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

1892

7040

1893

1894

1895

impl From<Moo<Expression>> for Expression {

1896

88114

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

1897

88114

        val.as_ref().clone()

1898

88114

1899

1900

1901

impl CategoryOf for Expression {

1902

1388848

    fn category_of(&self) -> Category {

1903

        // take highest category of all the expressions children

1904

5379038

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

1905

1906

5379038

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

1907

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

1908

                // subexpressions

1909

1660578

                *max_category

1910

            } else {

1911

                // this expression has no children

1912

3718460

                let mut max_category = Category::Bottom;

1913

1914

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

1915

                // declarationptrs inside this expression

1916

1917

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

1918

1919

                // if x contains submodels (including comprehensions)

1920

3718460

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

1921

                    // assume that the category is decision

1922

                    return Category::Decision;

1923

3718460

1924

1925

                // if x contains atoms

1926

3773140

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

1927

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

1928

3718440

                && max_atom_category > max_category{

1929

                    // update category

1930

3718440

                    max_category = max_atom_category;

1931

3718440

1932

1933

                // if x contains declarationPtrs

1934

3718460

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

1935

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

1936

2827886

                && max_declaration_category > max_category{

1937

                    // update category

1938

614

                    max_category = max_declaration_category;

1939

3717846

1940

3718460

                max_category

1941

1942

1943

5379038

});

1944

1945

1388848

        if cfg!(debug_assertions) {

1946

1388848

            trace!(

1947

                category= %category,

1948

                expression= %self,

1949

                "Called Expression::category_of()"

1950

);

1951

};

1952

1388848

        category

1953

1388848

1954

1955

1956

impl Display for Expression {

1957

73995320

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

1958

73995320

        match &self {

1959

404

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

1960

404

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

1961

1962

3050

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

1963

3050

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

1964

1965

380

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

1966

380

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

1967

1968

480

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

1969

480

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

1970

1971

480

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

1972

480

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

1973

1974

600

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

1975

600

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

1976

1977

510

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

1978

510

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

1979

1980

1981

2272850

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

1982

30286

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

1983

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

1984

274008

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

1985

653634

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

1986

20320

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

1987

20320

                let args = es

1988

20320

                    .iter()

1989

40400

                    .map(|x| match x {

1990

20080

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

1991

20320

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

1992

40400

})

1993

20320

                    .join(",");

1994

1995

20320

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

1996

1997

13760

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

1998

13760

                let args = es

1999

13760

                    .iter()

2000

26960

                    .map(|x| match x {

2001

13200

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

2002

13760

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

2003

26960

})

2004

13760

                    .join(",");

2005

2006

13760

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

2007

2008

3480

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

2009

3480

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

2010

2011

209926

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

2012

209926

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

2013

2014

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

2015

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

2016

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

2017

65704344

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

2018

8376

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

2019

638734

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

2020

638734

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

2021

2022

101974

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

2023

101974

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

2024

2025

14840

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

2026

14840

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

2027

2028

14964

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

2029

14964

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

2030

2031

44670

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

2032

44670

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

2033

2034

258256

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

2035

258256

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

2036

2037

258992

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

2038

258992

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

2039

2040

45876

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

2041

45876

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

2042

2043

1680

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

2044

1680

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

2045

2046

357166

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

2047

357166

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

2048

2049

464106

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

2050

464106

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

2051

2052

144964

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

2053

144964

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

2054

2055

325564

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

2056

325564

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

2057

2058

8004

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

2059

8004

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

2060

2061

45924

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

2062

45924

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

2063

2064

40

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

2065

40

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

2066

2067

40

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

2068

40

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

2069

2070

48

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

2071

48

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

2072

2073

44

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

2074

44

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

2075

2076

48

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

2077

48

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

2078

2079

162148

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

2080

162148

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

2081

2082

156908

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

2083

156908

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

2084

2085

60572

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

2086

60572

f,

2087

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

2088

60572

                box1.clone(),

2089

60572

                box2.clone(),

2090

60572

                box3.clone()

2091

),

2092

1994

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

2093

1994

                if let Some(n) = n {

2094

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

2095

                } else {

2096

1994

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

2097

2098

2099

14876

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

2100

14876

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

2101

2102

1200

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

2103

1200

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

2104

2105

200

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

2106

200

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

2107

2108

13784

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

2109

13784

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

2110

2111

19960

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

2112

19960

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

2113

2114

21560

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

2115

21560

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

2116

2117

26584

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

2118

26584

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

2119

2120

284134

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

2121

284134

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

2122

2123

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

2124

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

2125

2126

80

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

2127

80

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

2128

2129

4220

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

2130

4220

                write!(

2131

4220

f,

2132

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

2133

4220

                    box1.clone(),

2134

4220

                    box2.clone(),

2135

4220

                    box3.clone()

2136

2137

2138

1320

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

2139

1320

                write!(

2140

1320

f,

2141

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

2142

1320

                    box1.clone(),

2143

1320

                    box2.clone(),

2144

1320

                    box3.clone()

2145

2146

2147

4344

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

2148

4344

                write!(f, "WatchedLiteral({x},{l})")

2149

2150

67360

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

2151

67360

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

2152

2153

39920

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

2154

39920

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

2155

2156

760

            Expression::MinionWInIntervalSet(_, atom, intervals) => {

2157

760

                let intervals = intervals.iter().join(",");

2158

760

                write!(f, "__minion_w_inintervalset({atom},[{intervals}])")

2159

2160

480

            Expression::MinionWInSet(_, atom, values) => {

2161

480

                let values = values.iter().join(",");

2162

480

                write!(f, "__minion_w_inset({atom},[{values}])")

2163

2164

90370

            Expression::AuxDeclaration(_, reference, e) => {

2165

90370

                write!(f, "{} =aux {}", reference, e.clone())

2166

2167

3880

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

2168

3880

                write!(f, "{} % {}", a.clone(), b.clone())

2169

2170

6720

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

2171

6720

                write!(f, "SafeMod({},{})", a.clone(), b.clone())

2172

2173

49716

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

2174

49716

                write!(f, "-({})", a.clone())

2175

2176

            Expression::Factorial(_, a) => {

2177

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

2178

2179

195146

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

2180

195146

                write!(f, "({} - {})", a.clone(), b.clone())

2181

2182

10164

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

2183

10164

                write!(f, "__flat_alldiff({})", pretty_vec(es))

2184

2185

1600

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

2186

1600

                write!(f, "AbsEq({},{})", a.clone(), b.clone())

2187

2188

720

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

2189

720

                write!(f, "MinusEq({},{})", a.clone(), b.clone())

2190

2191

2300

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

2192

2300

                write!(

2193

2300

f,

2194

                    "FlatProductEq({},{},{})",

2195

2300

                    a.clone(),

2196

2300

                    b.clone(),

2197

2300

                    c.clone()

2198

2199

2200

18700

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

2201

18700

                write!(

2202

18700

f,

2203

                    "FlatWeightedSumLeq({},{},{})",

2204

18700

                    pretty_vec(cs),

2205

18700

                    pretty_vec(vs),

2206

18700

                    total.clone()

2207

2208

2209

18900

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

2210

18900

                write!(

2211

18900

f,

2212

                    "FlatWeightedSumGeq({},{},{})",

2213

18900

                    pretty_vec(cs),

2214

18900

                    pretty_vec(vs),

2215

18900

                    total.clone()

2216

2217

2218

9256

            Expression::MinionPow(_, atom, atom1, atom2) => {

2219

9256

                write!(f, "MinionPow({atom},{atom1},{atom2})")

2220

2221

94576

            Expression::MinionElementOne(_, atoms, atom, atom1) => {

2222

94576

                let atoms = atoms.iter().join(",");

2223

94576

                write!(f, "__minion_element_one([{atoms}],{atom},{atom1})")

2224

2225

2226

1146

            Expression::ToInt(_, expr) => {

2227

1146

                write!(f, "toInt({expr})")

2228

2229

2230

671040

            Expression::SATInt(_, encoding, bits, (min, max)) => {

2231

671040

                write!(f, "SATInt({encoding:?}, {bits} [{min}, {max}])")

2232

2233

2234

            Expression::PairwiseSum(_, a, b) => write!(f, "PairwiseSum({a}, {b})"),

2235

            Expression::PairwiseProduct(_, a, b) => write!(f, "PairwiseProduct({a}, {b})"),

2236

2237

72

            Expression::Defined(_, function) => write!(f, "defined({function})"),

2238

84

            Expression::Range(_, function) => write!(f, "range({function})"),

2239

40

            Expression::Image(_, function, elems) => write!(f, "image({function},{elems})"),

2240

40

            Expression::ImageSet(_, function, elems) => write!(f, "imageSet({function},{elems})"),

2241

84

            Expression::PreImage(_, function, elems) => write!(f, "preImage({function},{elems})"),

2242

40

            Expression::Inverse(_, a, b) => write!(f, "inverse({a},{b})"),

2243

56

            Expression::Restrict(_, function, domain) => write!(f, "restrict({function},{domain})"),

2244

2245

1360

            Expression::LexLt(_, a, b) => write!(f, "({a} <lex {b})"),

2246

12820

            Expression::LexLeq(_, a, b) => write!(f, "({a} <=lex {b})"),

2247

120

            Expression::LexGt(_, a, b) => write!(f, "({a} >lex {b})"),

2248

180

            Expression::LexGeq(_, a, b) => write!(f, "({a} >=lex {b})"),

2249

240

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

2250

240

                write!(f, "FlatLexLt({}, {})", pretty_vec(a), pretty_vec(b))

2251

2252

400

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

2253

400

                write!(f, "FlatLexLeq({}, {})", pretty_vec(a), pretty_vec(b))

2254

2255

40

            Expression::Active(_, variant, field_name) => {

2256

40

                write!(f, "active({variant}, {field_name})")

2257

2258

120

            Expression::ToSet(_, other) => write!(f, "toSet({other})"),

2259

80

            Expression::ToMSet(_, other) => write!(f, "toMSet({other})"),

2260

40

            Expression::ToRelation(_, function) => write!(f, "toRelation({function})"),

2261

44

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

2262

44

                let projections_str = projections

2263

44

                    .iter()

2264

132

                    .map(|x| {

2265

132

                        if let Some(x) = x {

2266

44

                            x.to_string()

2267

                        } else {

2268

88

                            String::from("_")

2269

2270

132

})

2271

44

                    .join(", ");

2272

44

                write!(f, "{relation}({projections_str})")

2273

2274

2275

73995320

2276

2277

2278

3200

fn minus_operand_return_type(expr: &Expression) -> ReturnType {

2279

1934

    match expr {

2280

1134

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

2281

1134

            let decl_kind = reference.ptr.kind().clone();

2282

1134

            match decl_kind {

2283

442

                DeclarationKind::Find(var) => var.return_type(),

2284

                DeclarationKind::Given(domain)

2285

                | DeclarationKind::DomainLetting(domain)

2286

                | DeclarationKind::Field(domain) => domain.return_type(),

2287

280

                DeclarationKind::Quantified(inner) => inner.domain().return_type(),

2288

                DeclarationKind::QuantifiedExpr(inner)

2289

                | DeclarationKind::TemporaryValueLetting(inner)

2290

                // not sure if i should ever be looking at the domain ptr but seems to work

2291

412

                | DeclarationKind::ValueLetting(inner, _) => inner.return_type(),

2292

2293

2294

2066

        _ => expr.return_type(),

2295

2296

3200

2297

2298

impl Typeable for Expression {

2299

2222638

    fn return_type(&self) -> ReturnType {

2300

2222638

        match self {

2301

            Expression::Union(_, subject, _) => ReturnType::Set(Box::new(subject.return_type())),

2302

            Expression::Intersect(_, subject, _) => {

2303

                ReturnType::Set(Box::new(subject.return_type()))

2304

2305

600

            Expression::In(_, _, _) => ReturnType::Bool,

2306

            Expression::Supset(_, _, _) => ReturnType::Bool,

2307

            Expression::SupsetEq(_, _, _) => ReturnType::Bool,

2308

            Expression::Subset(_, _, _) => ReturnType::Bool,

2309

            Expression::SubsetEq(_, _, _) => ReturnType::Bool,

2310

133590

            Expression::AbstractLiteral(_, lit) => lit.return_type(),

2311

229078

            Expression::UnsafeIndex(_, subject, idx) | Expression::SafeIndex(_, subject, idx) => {

2312

301998

                let subject_ty = subject.return_type();

2313

301998

                match subject_ty {

2314

                    ReturnType::Matrix(_) => {

2315

                        // For n-dimensional matrices, unwrap the element type until

2316

                        // we either get to the innermost element type or the last index

2317

292158

                        let mut elem_typ = subject_ty;

2318

292158

                        let mut idx_len = idx.len();

2319

584630

                        while idx_len > 0

2320

342946

                            && let ReturnType::Matrix(new_elem_typ) = &elem_typ

2321

292472

2322

292472

                            elem_typ = *new_elem_typ.clone();

2323

292472

                            idx_len -= 1;

2324

292472

2325

292158

                        elem_typ

2326

2327

                    // TODO: We can implement indexing for these eventually

2328

                    ReturnType::Record(_) | ReturnType::Tuple(_) | ReturnType::Variant(_) => {

2329

9840

                        ReturnType::Unknown

2330

2331

                    _ => bug!(

2332

                        "Invalid indexing operation: expected the operand to be a collection, got {self}: {subject_ty}"

2333

),

2334

2335

2336

160

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

2337

160

                ReturnType::Matrix(Box::new(subject.return_type()))

2338

2339

            Expression::InDomain(_, _, _) => ReturnType::Bool,

2340

4

            Expression::Comprehension(_, comp) => comp.return_type(),

2341

            Expression::AbstractComprehension(_, comp) => comp.return_type(),

2342

            Expression::Root(_, _) => ReturnType::Bool,

2343

            Expression::DominanceRelation(_, _) => ReturnType::Bool,

2344

            Expression::FromSolution(_, expr) => expr.return_type(),

2345

            Expression::Metavar(_, _) => ReturnType::Unknown,

2346

1575452

            Expression::Atomic(_, atom) => atom.return_type(),

2347

1120

            Expression::Abs(_, _) => ReturnType::Int,

2348

105244

            Expression::Sum(_, _) => ReturnType::Int,

2349

10762

            Expression::Product(_, _) => ReturnType::Int,

2350

1920

            Expression::Min(_, _) => ReturnType::Int,

2351

1870

            Expression::Max(_, _) => ReturnType::Int,

2352

160

            Expression::Not(_, _) => ReturnType::Bool,

2353

414

            Expression::Or(_, _) => ReturnType::Bool,

2354

1292

            Expression::Imply(_, _, _) => ReturnType::Bool,

2355

            Expression::Iff(_, _, _) => ReturnType::Bool,

2356

6518

            Expression::And(_, _) => ReturnType::Bool,

2357

8662

            Expression::Eq(_, _, _) => ReturnType::Bool,

2358

1080

            Expression::Neq(_, _, _) => ReturnType::Bool,

2359

            Expression::Geq(_, _, _) => ReturnType::Bool,

2360

2200

            Expression::Leq(_, _, _) => ReturnType::Bool,

2361

            Expression::Gt(_, _, _) => ReturnType::Bool,

2362

            Expression::Lt(_, _, _) => ReturnType::Bool,

2363

            Expression::Apart(_, _, _) => ReturnType::Bool,

2364

            Expression::Together(_, _, _) => ReturnType::Bool,

2365

40

            Expression::Party(_, _, subject) => ReturnType::Set(Box::new(subject.return_type())),

2366

40

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

2367

40

                ReturnType::Set(Box::new(subject.return_type()))

2368

2369

40

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

2370

40

                ReturnType::Set(Box::new(ReturnType::Set(Box::new(subject.return_type()))))

2371

2372

13200

            Expression::SafeDiv(_, _, _) => ReturnType::Int,

2373

11160

            Expression::UnsafeDiv(_, _, _) => ReturnType::Int,

2374

            Expression::FlatAllDiff(_, _) => ReturnType::Bool,

2375

80

            Expression::FlatSumGeq(_, _, _) => ReturnType::Bool,

2376

            Expression::FlatSumLeq(_, _, _) => ReturnType::Bool,

2377

            Expression::MinionDivEqUndefZero(_, _, _, _) => ReturnType::Bool,

2378

680

            Expression::FlatIneq(_, _, _, _) => ReturnType::Bool,

2379

1920

            Expression::Flatten(_, _, matrix) => {

2380

1920

                let matrix_type = matrix.return_type();

2381

1920

                match matrix_type {

2382

                    ReturnType::Matrix(_) => {

2383

                        // unwrap until we get to innermost element

2384

1920

                        let mut elem_type = matrix_type;

2385

3840

                        while let ReturnType::Matrix(new_elem_type) = &elem_type {

2386

1920

                            elem_type = *new_elem_type.clone();

2387

1920

2388

1920

                        ReturnType::Matrix(Box::new(elem_type))

2389

2390

                    _ => bug!(

2391

                        "Invalid indexing operation: expected the operand to be a collection, got {self}: {matrix_type}"

2392

),

2393

2394

2395

160

            Expression::AllDiff(_, _) => ReturnType::Bool,

2396

            Expression::Table(_, _, _) => ReturnType::Bool,

2397

            Expression::NegativeTable(_, _, _) => ReturnType::Bool,

2398

3120

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

2399

            Expression::FlatWatchedLiteral(_, _, _) => ReturnType::Bool,

2400

            Expression::MinionReify(_, _, _) => ReturnType::Bool,

2401

240

            Expression::MinionReifyImply(_, _, _) => ReturnType::Bool,

2402

            Expression::MinionWInIntervalSet(_, _, _) => ReturnType::Bool,

2403

            Expression::MinionWInSet(_, _, _) => ReturnType::Bool,

2404

            Expression::MinionElementOne(_, _, _, _) => ReturnType::Bool,

2405

            Expression::AuxDeclaration(_, _, _) => ReturnType::Bool,

2406

1520

            Expression::UnsafeMod(_, _, _) => ReturnType::Int,

2407

4320

            Expression::SafeMod(_, _, _) => ReturnType::Int,

2408

            Expression::MinionModuloEqUndefZero(_, _, _, _) => ReturnType::Bool,

2409

2882

            Expression::Neg(_, _) => ReturnType::Int,

2410

            Expression::Factorial(_, _) => ReturnType::Int,

2411

986

            Expression::UnsafePow(_, _, _) => ReturnType::Int,

2412

2784

            Expression::SafePow(_, _, _) => ReturnType::Int,

2413

1600

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

2414

                // rather than calling .return_type on a and b which sometimes errors on references that don't have domains

2415

                // use custom function that extracts return type from atomic references based on each declaration variant

2416

1600

                let a_type = minus_operand_return_type(a);

2417

1600

                let b_type = minus_operand_return_type(b);

2418

2419

1600

                if a_type == ReturnType::Int && b_type == ReturnType::Int {

2420

1600

                    ReturnType::Int

2421

                } else if let ReturnType::Set(a_inner) = a_type

2422

                    && let ReturnType::Set(b_inner) = b_type

2423

                    && a_inner == b_inner

2424

2425

                    ReturnType::Set(a_inner)

2426

                } else {

2427

                    bug!(

2428

                        "Invalid minus operation: operands are of different or invalid types for this operation"

2429

2430

2431

2432

            Expression::FlatAbsEq(_, _, _) => ReturnType::Bool,

2433

            Expression::FlatMinusEq(_, _, _) => ReturnType::Bool,

2434

            Expression::FlatProductEq(_, _, _, _) => ReturnType::Bool,

2435

            Expression::FlatWeightedSumLeq(_, _, _, _) => ReturnType::Bool,

2436

160

            Expression::FlatWeightedSumGeq(_, _, _, _) => ReturnType::Bool,

2437

            Expression::MinionPow(_, _, _, _) => ReturnType::Bool,

2438

1340

            Expression::ToInt(_, _) => ReturnType::Int,

2439

21960

            Expression::SATInt(..) => ReturnType::Int,

2440

            Expression::PairwiseSum(_, _, _) => ReturnType::Int,

2441

            Expression::PairwiseProduct(_, _, _) => ReturnType::Int,

2442

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

2443

                let subject = function.return_type();

2444

                match subject {

2445

                    ReturnType::Function(domain, _) => ReturnType::Set(Box::new(*domain)),

2446

                    _ => bug!(

2447

                        "Invalid defined operation: expected the operand to be a function, got {self}: {subject}"

2448

),

2449

2450

2451

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

2452

                let subject = function.return_type();

2453

                match subject {

2454

                    ReturnType::Function(_, codomain) => ReturnType::Set(Box::new(*codomain)),

2455

                    _ => bug!(

2456

                        "Invalid range operation: expected the operand to be a function, got {self}: {subject}"

2457

),

2458

2459

2460

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

2461

                let subject = function.return_type();

2462

                match subject {

2463

                    ReturnType::Function(_, codomain) => *codomain,

2464

                    _ => bug!(

2465

                        "Invalid image operation: expected the operand to be a function, got {self}: {subject}"

2466

),

2467

2468

2469

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

2470

                let subject = function.return_type();

2471

                match subject {

2472

                    ReturnType::Function(_, codomain) => ReturnType::Set(Box::new(*codomain)),

2473

                    _ => bug!(

2474

                        "Invalid imageSet operation: expected the operand to be a function, got {self}: {subject}"

2475

),

2476

2477

2478

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

2479

                let subject = function.return_type();

2480

                match subject {

2481

                    ReturnType::Function(domain, _) => ReturnType::Set(Box::new(*domain)),

2482

                    _ => bug!(

2483

                        "Invalid preImage operation: expected the operand to be a function, got {self}: {subject}"

2484

),

2485

2486

2487

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

2488

                let subject = function.return_type();

2489

                match subject {

2490

                    ReturnType::Function(_, codomain) => {

2491

                        ReturnType::Function(Box::new(new_domain.return_type()), codomain)

2492

2493

                    _ => bug!(

2494

                        "Invalid preImage operation: expected the operand to be a function, got {self}: {subject}"

2495

),

2496

2497

2498

            Expression::Inverse(..) => ReturnType::Bool,

2499

            Expression::LexLt(..) => ReturnType::Bool,

2500

            Expression::LexGt(..) => ReturnType::Bool,

2501

1360

            Expression::LexLeq(..) => ReturnType::Bool,

2502

            Expression::LexGeq(..) => ReturnType::Bool,

2503

            Expression::FlatLexLt(..) => ReturnType::Bool,

2504

            Expression::FlatLexLeq(..) => ReturnType::Bool,

2505

            Expression::Active(..) => ReturnType::Bool,

2506

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

2507

                let subject = other.return_type();

2508

                match subject {

2509

                    ReturnType::Function(domain, codomain) => {

2510

                        ReturnType::Set(Box::new(ReturnType::Tuple(vec![*domain, *codomain])))

2511

2512

                    ReturnType::Relation(domains) => {

2513

                        ReturnType::Set(Box::new(ReturnType::Tuple(domains)))

2514

2515

                    ReturnType::MSet(domain) => ReturnType::Set(Box::new(*domain)),

2516

                    ReturnType::Matrix(domain) => ReturnType::Set(Box::new(*domain)),

2517

                    _ => bug!(

2518

                        "Invalid toSet operation: expected the operand to be a mset, matrix, relation, or function, got {self}: {subject}"

2519

),

2520

2521

2522

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

2523

                let subject = other.return_type();

2524

                match subject {

2525

                    ReturnType::Function(domain, codomain) => {

2526

                        ReturnType::MSet(Box::new(ReturnType::Tuple(vec![*domain, *codomain])))

2527

2528

                    ReturnType::Relation(domains) => {

2529

                        ReturnType::MSet(Box::new(ReturnType::Tuple(domains)))

2530

2531

                    ReturnType::Set(domain) => ReturnType::MSet(Box::new(*domain)),

2532

                    _ => bug!(

2533

                        "Invalid toMSet operation: expected the operand to be a set, relation, or function, got {self}: {subject}"

2534

),

2535

2536

2537

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

2538

                let subject = function.return_type();

2539

                match subject {

2540

                    ReturnType::Function(domain, codomain) => {

2541

                        ReturnType::Relation(vec![*domain, *codomain])

2542

2543

                    _ => bug!(

2544

                        "Invalid toRelation operation: expected the operand to be a function, got {self}: {subject}"

2545

),

2546

2547

2548

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

2549

                let subject = relation.return_type();

2550

                match subject {

2551

                    ReturnType::Relation(domains) => {

2552

                        let new_doms = domains

2553

                            .iter()

2554

                            .zip(projections.iter())

2555

                            .filter_map(|(domain, included)| {

2556

                                if included.is_none() {

2557

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

2558

                                    Some(domain.clone())

2559

                                } else {

2560

                                    None

2561

2562

})

2563

                            .collect();

2564

                        ReturnType::Relation(new_doms)

2565

2566

                    _ => bug!(

2567

                        "Invalid RelationProj operation: expected the operand to be a relation, got {self}: {subject}"

2568

),

2569

2570

2571

            Expression::Card(..) => ReturnType::Int,

2572

            Expression::Subsequence(_, _, _) => ReturnType::Bool,

2573

            Expression::Substring(_, _, _) => ReturnType::Bool,

2574

2575

2222638

2576

2577

2578

impl Expression {

2579

    /// Visit each direct `Expression` child by reference, without cloning.

2580

    fn for_each_expr_child(&self, f: &mut impl FnMut(&Expression)) {

2581

        match self {

2582

            // Special Case

2583

            Expression::AbstractLiteral(_, alit) => match alit {

2584

                AbstractLiteral::Set(v) | AbstractLiteral::MSet(v) | AbstractLiteral::Tuple(v) => {

2585

                    for expr in v {

2586

                        f(expr);

2587

2588

2589

                AbstractLiteral::Partition(two_d_v) => {

2590

                    for part in two_d_v {

2591

                        for expr in part {

2592

                            f(expr);

2593

2594

2595

2596

                AbstractLiteral::Matrix(v, _domain) => {

2597

                    for expr in v {

2598

                        f(expr);

2599

2600

2601

                AbstractLiteral::Record(rs) => {

2602

                    for r in rs {

2603

                        f(&r.value);

2604

2605

2606

                AbstractLiteral::Sequence(v) => {

2607

                    for expr in v {

2608

                        f(expr);

2609

2610

2611

                AbstractLiteral::Function(vs) => {

2612

                    for (a, b) in vs {

2613

                        f(a);

2614

                        f(b);

2615

2616

2617

                AbstractLiteral::Variant(v) => {

2618

                    f(&v.value);

2619

2620

                AbstractLiteral::Relation(vs) => {

2621

                    for exprs in vs {

2622

                        for expr in exprs {

2623

                            f(expr);

2624

2625

2626

2627

},

2628

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

2629

                for expr in vs {

2630

                    f(expr);

2631

2632

2633

2634

            // Moo<Expression>

2635

            Expression::DominanceRelation(_, m1)

2636

            | Expression::ToInt(_, m1)

2637

            | Expression::Abs(_, m1)

2638

            | Expression::Sum(_, m1)

2639

            | Expression::Product(_, m1)

2640

            | Expression::Min(_, m1)

2641

            | Expression::Max(_, m1)

2642

            | Expression::Not(_, m1)

2643

            | Expression::Or(_, m1)

2644

            | Expression::And(_, m1)

2645

            | Expression::Neg(_, m1)

2646

            | Expression::Defined(_, m1)

2647

            | Expression::AllDiff(_, m1)

2648

            | Expression::Factorial(_, m1)

2649

            | Expression::Range(_, m1)

2650

            | Expression::Participants(_, m1)

2651

            | Expression::Parts(_, m1)

2652

            | Expression::ToSet(_, m1)

2653

            | Expression::ToMSet(_, m1)

2654

            | Expression::ToRelation(_, m1)

2655

            | Expression::Card(_, m1) => {

2656

                f(m1);

2657

2658

2659

            // Moo<Expression> + Moo<Expression>

2660

            Expression::Table(_, m1, m2)

2661

            | Expression::NegativeTable(_, m1, m2)

2662

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

2663

            | Expression::Imply(_, m1, m2)

2664

            | Expression::Iff(_, m1, m2)

2665

            | Expression::Union(_, m1, m2)

2666

            | Expression::In(_, m1, m2)

2667

            | Expression::Intersect(_, m1, m2)

2668

            | Expression::Supset(_, m1, m2)

2669

            | Expression::SupsetEq(_, m1, m2)

2670

            | Expression::Subset(_, m1, m2)

2671

            | Expression::SubsetEq(_, m1, m2)

2672

            | Expression::Eq(_, m1, m2)

2673

            | Expression::Neq(_, m1, m2)

2674

            | Expression::Geq(_, m1, m2)

2675

            | Expression::Leq(_, m1, m2)

2676

            | Expression::Gt(_, m1, m2)

2677

            | Expression::Lt(_, m1, m2)

2678

            | Expression::SafeDiv(_, m1, m2)

2679

            | Expression::UnsafeDiv(_, m1, m2)

2680

            | Expression::SafeMod(_, m1, m2)

2681

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

2682

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

2683

            | Expression::SafePow(_, m1, m2)

2684

            | Expression::Minus(_, m1, m2)

2685

            | Expression::PairwiseSum(_, m1, m2)

2686

            | Expression::PairwiseProduct(_, m1, m2)

2687

            | Expression::Image(_, m1, m2)

2688

            | Expression::ImageSet(_, m1, m2)

2689

            | Expression::PreImage(_, m1, m2)

2690

            | Expression::Inverse(_, m1, m2)

2691

            | Expression::Restrict(_, m1, m2)

2692

            | Expression::Apart(_, m1, m2)

2693

            | Expression::Together(_, m1, m2)

2694

            | Expression::Party(_, m1, m2)

2695

            | Expression::LexLt(_, m1, m2)

2696

            | Expression::LexLeq(_, m1, m2)

2697

            | Expression::LexGt(_, m1, m2)

2698

            | Expression::LexGeq(_, m1, m2)

2699

            | Expression::Active(_, m1, m2)

2700

            | Expression::Subsequence(_, m1, m2)

2701

            | Expression::Substring(_, m1, m2) => {

2702

                f(m1);

2703

                f(m2);

2704

2705

2706

            // Moo<Expression> + Vec<Expression>

2707

            Expression::UnsafeIndex(_, m, vs) | Expression::SafeIndex(_, m, vs) => {

2708

                f(m);

2709

                for v in vs {

2710

                    f(v);

2711

2712

2713

            // Moo<Expression> + Vec<Option<Expression>>

2714

            Expression::UnsafeSlice(_, m, vs)

2715

            | Expression::SafeSlice(_, m, vs)

2716

            | Expression::RelationProj(_, m, vs) => {

2717

                f(m);

2718

                for e in vs.iter().flatten() {

2719

                    f(e);

2720

2721

2722

2723

            // Moo<Expression> + DomainPtr

2724

            Expression::InDomain(_, m, _) => {

2725

                f(m);

2726

2727

2728

            // Option<Moo<Expression>> + Moo<Expression>

2729

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

2730

                if let Some(e) = opt {

2731

                    f(e);

2732

2733

                f(m);

2734

2735

2736

            // Moo<Expression> + Atom

2737

            Expression::MinionReify(_, m, _) | Expression::MinionReifyImply(_, m, _) => {

2738

                f(m);

2739

2740

2741

            // Reference + Moo<Expression>

2742

            Expression::AuxDeclaration(_, _, m) => {

2743

                f(m);

2744

2745

2746

            // SATIntEncoding + Moo<Expression> + (i32, i32)

2747

            Expression::SATInt(_, _, m, _) => {

2748

                f(m);

2749

2750

2751

            // No Expression children

2752

            Expression::Comprehension(_, _)

2753

            | Expression::AbstractComprehension(_, _)

2754

            | Expression::Atomic(_, _)

2755

            | Expression::FromSolution(_, _)

2756

            | Expression::Metavar(_, _)

2757

            | Expression::FlatAbsEq(_, _, _)

2758

            | Expression::FlatMinusEq(_, _, _)

2759

            | Expression::FlatProductEq(_, _, _, _)

2760

            | Expression::MinionDivEqUndefZero(_, _, _, _)

2761

            | Expression::MinionModuloEqUndefZero(_, _, _, _)

2762

            | Expression::MinionPow(_, _, _, _)

2763

            | Expression::FlatAllDiff(_, _)

2764

            | Expression::FlatSumGeq(_, _, _)

2765

            | Expression::FlatSumLeq(_, _, _)

2766

            | Expression::FlatIneq(_, _, _, _)

2767

            | Expression::FlatWatchedLiteral(_, _, _)

2768

            | Expression::FlatWeightedSumLeq(_, _, _, _)

2769

            | Expression::FlatWeightedSumGeq(_, _, _, _)

2770

            | Expression::MinionWInIntervalSet(_, _, _)

2771

            | Expression::MinionWInSet(_, _, _)

2772

            | Expression::MinionElementOne(_, _, _, _)

2773

            | Expression::FlatLexLt(_, _, _)

2774

            | Expression::FlatLexLeq(_, _, _) => {}

2775

2776

2777

2778

2779

impl CacheHashable for Expression {

2780

    fn invalidate_cache(&self) {

2781

        self.meta_ref()

2782

            .stored_hash

2783

            .store(NO_HASH, Ordering::Relaxed);

2784

2785

2786

    fn invalidate_cache_recursive(&self) {

2787

        self.invalidate_cache();

2788

        self.for_each_expr_child(&mut |child| {

2789

            child.invalidate_cache_recursive();

2790

});

2791

2792

2793

    fn get_cached_hash(&self) -> u64 {

2794

        let stored = self.meta_ref().stored_hash.load(Ordering::Relaxed);

2795

        if stored != NO_HASH {

2796

            HASH_HITS.fetch_add(1, Ordering::Relaxed);

2797

            return stored;

2798

2799

        HASH_MISSES.fetch_add(1, Ordering::Relaxed);

2800

        self.calculate_hash()

2801

2802

2803

    fn calculate_hash(&self) -> u64 {

2804

        let mut hasher = DefaultHasher::new();

2805

        std::mem::discriminant(self).hash(&mut hasher);

2806

        match self {

2807

            // Special Case

2808

            Expression::AbstractLiteral(_, alit) => match alit {

2809

                AbstractLiteral::Set(v)

2810

                | AbstractLiteral::MSet(v)

2811

                | AbstractLiteral::Tuple(v)

2812

                | AbstractLiteral::Sequence(v) => {

2813

                    for expr in v {

2814

                        expr.get_cached_hash().hash(&mut hasher);

2815

2816

2817

                AbstractLiteral::Matrix(v, domain) => {

2818

                    domain.hash(&mut hasher);

2819

                    for expr in v {

2820

                        expr.get_cached_hash().hash(&mut hasher);

2821

2822

2823

                AbstractLiteral::Record(rs) => {

2824

                    for r in rs {

2825

                        r.name.hash(&mut hasher);

2826

                        r.value.get_cached_hash().hash(&mut hasher);

2827

2828

2829

                AbstractLiteral::Function(vs) => {

2830

                    for (a, b) in vs {

2831

                        a.get_cached_hash().hash(&mut hasher);

2832

                        b.get_cached_hash().hash(&mut hasher);

2833

2834

2835

                AbstractLiteral::Variant(v) => {

2836

                    v.name.hash(&mut hasher);

2837

                    v.value.get_cached_hash().hash(&mut hasher);

2838

2839

                AbstractLiteral::Relation(v) => {

2840

                    for exprs in v {

2841

                        for expr in exprs {

2842

                            expr.get_cached_hash().hash(&mut hasher);

2843

2844

2845

2846

                AbstractLiteral::Partition(v) => {

2847

                    for exprs in v {

2848

                        for expr in exprs {

2849

                            expr.get_cached_hash().hash(&mut hasher);

2850

2851

2852

2853

},

2854

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

2855

                for expr in vs {

2856

                    expr.get_cached_hash().hash(&mut hasher);

2857

2858

2859

2860

            // Moo<Expression>

2861

            Expression::DominanceRelation(_, m1)

2862

            | Expression::ToInt(_, m1)

2863

            | Expression::Abs(_, m1)

2864

            | Expression::Sum(_, m1)

2865

            | Expression::Product(_, m1)

2866

            | Expression::Min(_, m1)

2867

            | Expression::Max(_, m1)

2868

            | Expression::Not(_, m1)

2869

            | Expression::Or(_, m1)

2870

            | Expression::And(_, m1)

2871

            | Expression::Neg(_, m1)

2872

            | Expression::Defined(_, m1)

2873

            | Expression::AllDiff(_, m1)

2874

            | Expression::Factorial(_, m1)

2875

            | Expression::Participants(_, m1)

2876

            | Expression::Parts(_, m1)

2877

            | Expression::Range(_, m1)

2878

            | Expression::ToSet(_, m1)

2879

            | Expression::ToMSet(_, m1)

2880

            | Expression::ToRelation(_, m1)

2881

            | Expression::Card(_, m1) => {

2882

                m1.get_cached_hash().hash(&mut hasher);

2883

2884

2885

            // Moo<Expression> + Moo<Expression>

2886

            Expression::Table(_, m1, m2)

2887

            | Expression::NegativeTable(_, m1, m2)

2888

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

2889

            | Expression::Imply(_, m1, m2)

2890

            | Expression::Iff(_, m1, m2)

2891

            | Expression::Union(_, m1, m2)

2892

            | Expression::In(_, m1, m2)

2893

            | Expression::Intersect(_, m1, m2)

2894

            | Expression::Supset(_, m1, m2)

2895

            | Expression::SupsetEq(_, m1, m2)

2896

            | Expression::Subset(_, m1, m2)

2897

            | Expression::SubsetEq(_, m1, m2)

2898

            | Expression::Eq(_, m1, m2)

2899

            | Expression::Neq(_, m1, m2)

2900

            | Expression::Geq(_, m1, m2)

2901

            | Expression::Leq(_, m1, m2)

2902

            | Expression::Gt(_, m1, m2)

2903

            | Expression::Lt(_, m1, m2)

2904

            | Expression::Apart(_, m1, m2)

2905

            | Expression::Together(_, m1, m2)

2906

            | Expression::Party(_, m1, m2)

2907

            | Expression::SafeDiv(_, m1, m2)

2908

            | Expression::UnsafeDiv(_, m1, m2)

2909

            | Expression::SafeMod(_, m1, m2)

2910

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

2911

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

2912

            | Expression::SafePow(_, m1, m2)

2913

            | Expression::Minus(_, m1, m2)

2914

            | Expression::PairwiseSum(_, m1, m2)

2915

            | Expression::PairwiseProduct(_, m1, m2)

2916

            | Expression::Image(_, m1, m2)

2917

            | Expression::ImageSet(_, m1, m2)

2918

            | Expression::PreImage(_, m1, m2)

2919

            | Expression::Inverse(_, m1, m2)

2920

            | Expression::Restrict(_, m1, m2)

2921

            | Expression::LexLt(_, m1, m2)

2922

            | Expression::LexLeq(_, m1, m2)

2923

            | Expression::LexGt(_, m1, m2)

2924

            | Expression::LexGeq(_, m1, m2)

2925

            | Expression::Active(_, m1, m2)

2926

            | Expression::Subsequence(_, m1, m2)

2927

            | Expression::Substring(_, m1, m2) => {

2928

                m1.get_cached_hash().hash(&mut hasher);

2929

                m2.get_cached_hash().hash(&mut hasher);

2930

2931

            // Moo<Expression> + Vec<Expression>

2932

            Expression::UnsafeIndex(_, m, vs) | Expression::SafeIndex(_, m, vs) => {

2933

                m.get_cached_hash().hash(&mut hasher);

2934

                for v in vs {

2935

                    v.get_cached_hash().hash(&mut hasher);

2936

2937

2938

2939

            // Moo<Expression> + Vec<Option<Expression>>

2940

            Expression::UnsafeSlice(_, m, vs)

2941

            | Expression::SafeSlice(_, m, vs)

2942

            | Expression::RelationProj(_, m, vs) => {

2943

                m.get_cached_hash().hash(&mut hasher);

2944

                for v in vs {

2945

                    match v {

2946

                        Some(e) => e.get_cached_hash().hash(&mut hasher),

2947

                        None => 0u64.hash(&mut hasher),

2948

2949

2950

2951

2952

            // Moo<Expression> + DomainPtr

2953

            Expression::InDomain(_, m, d) => {

2954

                m.get_cached_hash().hash(&mut hasher);

2955

                d.hash(&mut hasher);

2956

2957

2958

            // Option<Moo<Expression>> + Moo<Expression>

2959

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

2960

                if let Some(e) = opt {

2961

                    e.get_cached_hash().hash(&mut hasher);

2962

2963

                m.get_cached_hash().hash(&mut hasher);

2964

2965

2966

            // Moo<Expression> + Atom

2967

            Expression::MinionReify(_, m, a) | Expression::MinionReifyImply(_, m, a) => {

2968

                m.get_cached_hash().hash(&mut hasher);

2969

                a.hash(&mut hasher);

2970

2971

2972

            // Reference + Moo<Expression>

2973

            Expression::AuxDeclaration(_, r, m) => {

2974

                r.hash(&mut hasher);

2975

                m.get_cached_hash().hash(&mut hasher);

2976

2977

2978

            // SATIntEncoding + Moo<Expression> + (i32, i32)

2979

            Expression::SATInt(_, enc, m, bounds) => {

2980

                enc.hash(&mut hasher);

2981

                m.get_cached_hash().hash(&mut hasher);

2982

                bounds.hash(&mut hasher);

2983

2984

2985

            // Non-Expression Moo types - hash normally

2986

            Expression::Comprehension(_, c) => c.hash(&mut hasher),

2987

            Expression::AbstractComprehension(_, c) => c.hash(&mut hasher),

2988

2989

            // Leaf types - no Expression children

2990

            Expression::Atomic(_, a) => a.hash(&mut hasher),

2991

            Expression::FromSolution(_, a) => a.hash(&mut hasher),

2992

            Expression::Metavar(_, u) => u.hash(&mut hasher),

2993

2994

            // Two Moo<Atom>

2995

            Expression::FlatAbsEq(_, a1, a2) | Expression::FlatMinusEq(_, a1, a2) => {

2996

                a1.hash(&mut hasher);

2997

                a2.hash(&mut hasher);

2998

2999

3000

            // Three Moo<Atom>

3001

            Expression::FlatProductEq(_, a1, a2, a3)

3002

            | Expression::MinionDivEqUndefZero(_, a1, a2, a3)

3003

            | Expression::MinionModuloEqUndefZero(_, a1, a2, a3)

3004

            | Expression::MinionPow(_, a1, a2, a3) => {

3005

                a1.hash(&mut hasher);

3006

                a2.hash(&mut hasher);

3007

                a3.hash(&mut hasher);

3008

3009

3010

            // Vec<Atom>

3011

            Expression::FlatAllDiff(_, vs) => {

3012

                for v in vs {

3013

                    v.hash(&mut hasher);

3014

3015

3016

3017

            // Vec<Atom> + Atom

3018

            Expression::FlatSumGeq(_, vs, a) | Expression::FlatSumLeq(_, vs, a) => {

3019

                for v in vs {

3020

                    v.hash(&mut hasher);

3021

3022

                a.hash(&mut hasher);

3023

3024

3025

            // Moo<Atom> + Moo<Atom> + Box<Literal>

3026

            Expression::FlatIneq(_, a1, a2, lit) => {

3027

                a1.hash(&mut hasher);

3028

                a2.hash(&mut hasher);

3029

                lit.hash(&mut hasher);

3030

3031

3032

            // Reference + Literal

3033

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

3034

                r.hash(&mut hasher);

3035

                l.hash(&mut hasher);

3036

3037

3038

            // Vec<Literal> + Vec<Atom> + Moo<Atom>

3039

            Expression::FlatWeightedSumLeq(_, lits, atoms, a)

3040

            | Expression::FlatWeightedSumGeq(_, lits, atoms, a) => {

3041

                for l in lits {

3042

                    l.hash(&mut hasher);

3043

3044

                for at in atoms {

3045

                    at.hash(&mut hasher);

3046

3047

                a.hash(&mut hasher);

3048

3049

3050

            // Atom + Vec<i32>

3051

            Expression::MinionWInIntervalSet(_, a, vs) | Expression::MinionWInSet(_, a, vs) => {

3052

                a.hash(&mut hasher);

3053

                for v in vs {

3054

                    v.hash(&mut hasher);

3055

3056

3057

3058

            // Vec<Atom> + Moo<Atom> + Moo<Atom>

3059

            Expression::MinionElementOne(_, vs, a1, a2) => {

3060

                for v in vs {

3061

                    v.hash(&mut hasher);

3062

3063

                a1.hash(&mut hasher);

3064

                a2.hash(&mut hasher);

3065

3066

3067

            // Vec<Atom> + Vec<Atom>

3068

            Expression::FlatLexLt(_, v1, v2) | Expression::FlatLexLeq(_, v1, v2) => {

3069

                for v in v1 {

3070

                    v.hash(&mut hasher);

3071

3072

                for v in v2 {

3073

                    v.hash(&mut hasher);

3074

3075

3076

};

3077

3078

        let result = hasher.finish();

3079

        self.meta_ref().stored_hash.swap(result, Ordering::Relaxed);

3080

        result

3081

3082

3083

3084

#[cfg(test)]

3085

mod tests {

3086

    use crate::matrix_expr;

3087

3088

    use super::*;

3089

3090

    #[test]

3091

1

    fn test_domain_of_constant_sum() {

3092

1

        let c1 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));

3093

1

        let c2 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2)));

3094

1

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![c1, c2]));

3095

1

        assert_eq!(sum.domain_of(), Some(Domain::int(vec![Range::Single(3)])));

3096

1

3097

3098

    #[test]

3099

1

    fn test_domain_of_constant_invalid_type() {

3100

1

        let c1 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));

3101

1

        let c2 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true)));

3102

1

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![c1, c2]));

3103

1

        assert_eq!(sum.domain_of(), None);

3104

1

3105

3106

    #[test]

3107

1

    fn test_domain_of_empty_sum() {

3108

1

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![]));

3109

1

        assert_eq!(sum.domain_of(), None);

3110

1

3111