Grcov report - expressions.rs

1

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

2

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

3

use tracing::trace;

4

5

use crate::ast::Name;

6

use crate::ast::ReturnType;

7

use crate::ast::SetAttr;

8

use crate::ast::literals::AbstractLiteral;

9

use crate::ast::literals::Literal;

10

use crate::ast::pretty::{pretty_expressions_as_top_level, pretty_vec};

11

use crate::ast::{Atom, DomainPtr};

12

use crate::ast::{GroundDomain, Metadata, UnresolvedDomain};

13

use crate::ast::{IntVal, Moo};

14

use crate::bug;

15

use conjure_cp_enum_compatibility_macro::document_compatibility;

16

use itertools::Itertools;

17

use serde::{Deserialize, Serialize};

18

use ustr::Ustr;

19

20

use polyquine::Quine;

21

use uniplate::{Biplate, Uniplate};

22

23

use super::ac_operators::ACOperatorKind;

24

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

25

use super::comprehension::Comprehension;

26

use super::domains::HasDomain as _;

27

use super::records::RecordValue;

28

use super::{DeclarationPtr, Domain, Range, Reference, SubModel, Typeable};

29

30

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

31

//

32

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

33

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

34

// stuff in boxes.

35

//

36

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

37

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

38

//

39

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

40

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

41

//

42

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

43

//

44

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

45

46

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

47

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

48

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

49

// boxed ~niklasdewally

50

51

// expect size of Expression to be 112 bytes

52

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

53

54

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

55

///

56

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

57

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

58

#[document_compatibility]

59

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

60

#[biplate(to=Metadata)]

61

#[biplate(to=Atom)]

62

#[biplate(to=DeclarationPtr)]

63

#[biplate(to=Name)]

64

#[biplate(to=Reference)]

65

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

66

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

67

#[biplate(to=SubModel)]

68

#[biplate(to=Comprehension)]

69

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

70

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

71

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

72

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

73

#[biplate(to=Literal)]

74

#[biplate(to=DomainPtr)]

75

#[path_prefix(conjure_cp::ast)]

76

pub enum Expression {

77

    AbstractLiteral(Metadata, AbstractLiteral<Expression>),

78

    /// The top of the model

79

    Root(Metadata, Vec<Expression>),

80

81

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

82

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

83

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

84

85

    /// A comprehension.

86

///

87

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

88

    // todo (gskorokhod): Comprehension contains a SubModel which contains a bunch of Rc pointers.

89

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

90

    #[polyquine_skip]

91

    Comprehension(Metadata, Moo<Comprehension>),

92

93

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

94

    DominanceRelation(Metadata, Moo<Expression>),

95

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

96

    FromSolution(Metadata, Moo<Atom>),

97

98

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

99

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

100

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

101

})]

102

    Metavar(Metadata, Ustr),

103

104

    Atomic(Metadata, Atom),

105

106

    /// A matrix index.

107

///

108

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

109

    #[compatible(JsonInput)]

110

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

111

112

    /// A safe matrix index.

113

///

114

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

115

    #[compatible(SMT)]

116

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

117

118

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

119

///

120

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

121

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

122

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

123

///

124

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

125

///

126

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

127

    #[compatible(JsonInput)]

128

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

129

130

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

131

///

132

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

133

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

134

135

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

136

///

137

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

138

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

139

    /// `SafeSlice` respectively.

140

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

141

142

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

143

///

144

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

145

///

146

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

147

    #[compatible(SMT)]

148

    ToInt(Metadata, Moo<Expression>),

149

150

    // todo (gskorokhod): Same reason as for Comprehension

151

    #[polyquine_skip]

152

    Scope(Metadata, Moo<SubModel>),

153

154

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

155

    #[compatible(JsonInput, SMT)]

156

    Abs(Metadata, Moo<Expression>),

157

158

    /// `sum(<vec_expr>)`

159

    #[compatible(JsonInput, SMT)]

160

    Sum(Metadata, Moo<Expression>),

161

162

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

163

    #[compatible(JsonInput, SMT)]

164

    Product(Metadata, Moo<Expression>),

165

166

    /// `min(<vec_expr>)`

167

    #[compatible(JsonInput, SMT)]

168

    Min(Metadata, Moo<Expression>),

169

170

    /// `max(<vec_expr>)`

171

    #[compatible(JsonInput, SMT)]

172

    Max(Metadata, Moo<Expression>),

173

174

    /// `not(a)`

175

    #[compatible(JsonInput, SAT, SMT)]

176

    Not(Metadata, Moo<Expression>),

177

178

    /// `or(<vec_expr>)`

179

    #[compatible(JsonInput, SAT, SMT)]

180

    Or(Metadata, Moo<Expression>),

181

182

    /// `and(<vec_expr>)`

183

    #[compatible(JsonInput, SAT, SMT)]

184

    And(Metadata, Moo<Expression>),

185

186

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

187

    #[compatible(JsonInput, SMT)]

188

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

189

190

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

191

    #[compatible(JsonInput, SMT)]

192

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

193

194

    #[compatible(JsonInput)]

195

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

196

197

    #[compatible(JsonInput)]

198

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

199

200

    #[compatible(JsonInput)]

201

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

202

203

    #[compatible(JsonInput)]

204

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

205

206

    #[compatible(JsonInput)]

207

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

208

209

    #[compatible(JsonInput)]

210

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

211

212

    #[compatible(JsonInput)]

213

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

214

215

    #[compatible(JsonInput, SMT)]

216

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

217

218

    #[compatible(JsonInput, SMT)]

219

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

220

221

    #[compatible(JsonInput, SMT)]

222

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

223

224

    #[compatible(JsonInput, SMT)]

225

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

226

227

    #[compatible(JsonInput, SMT)]

228

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

229

230

    #[compatible(JsonInput, SMT)]

231

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

232

233

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

234

    #[compatible(SMT)]

235

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

236

237

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

238

    #[compatible(JsonInput)]

239

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

240

241

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

242

    #[compatible(SMT)]

243

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

244

245

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

246

    #[compatible(JsonInput)]

247

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

248

249

    /// Negation: `-x`

250

    #[compatible(JsonInput, SMT)]

251

    Neg(Metadata, Moo<Expression>),

252

253

    /// Set of domain values function is defined for

254

    #[compatible(JsonInput)]

255

    Defined(Metadata, Moo<Expression>),

256

257

    /// Set of codomain values function is defined for

258

    #[compatible(JsonInput)]

259

    Range(Metadata, Moo<Expression>),

260

261

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

262

///

263

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

264

    #[compatible(JsonInput)]

265

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

266

267

    /// `UnsafePow` after preventing undefinedness

268

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

269

270

    /// Flatten matrix operator

271

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

272

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

273

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

274

275

    /// `allDiff(<vec_expr>)`

276

    #[compatible(JsonInput)]

277

    AllDiff(Metadata, Moo<Expression>),

278

279

    /// Binary subtraction operator

280

///

281

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

282

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

283

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

284

    #[compatible(JsonInput)]

285

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

286

287

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

288

///

289

    /// Low-level Minion constraint.

290

///

291

    /// # See also

292

///

293

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

294

    #[compatible(Minion)]

295

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

296

297

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

298

///

299

    /// Low-level Minion constraint.

300

///

301

    /// # See also

302

///

303

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

304

    #[compatible(Minion)]

305

    FlatAllDiff(Metadata, Vec<Atom>),

306

307

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

308

///

309

    /// Low-level Minion constraint.

310

///

311

    /// # See also

312

///

313

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

314

    #[compatible(Minion)]

315

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

316

317

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

318

///

319

    /// Low-level Minion constraint.

320

///

321

    /// # See also

322

///

323

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

324

    #[compatible(Minion)]

325

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

326

327

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

328

///

329

    /// Low-level Minion constraint.

330

///

331

    /// # See also

332

///

333

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

334

    #[compatible(Minion)]

335

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

336

337

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

338

///

339

    /// Low-level Minion constraint.

340

///

341

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

342

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

343

    /// watched-and and watched-or.

344

///

345

    /// # See also

346

///

347

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

348

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

349

    #[compatible(Minion)]

350

    #[polyquine_skip]

351

    FlatWatchedLiteral(Metadata, Reference, Literal),

352

353

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

354

    /// product of cs and xs.

355

///

356

    /// Low-level Minion constraint.

357

///

358

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

359

///

360

    /// # See also

361

///

362

    /// + [Minion

363

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

364

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

365

366

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

367

    /// product of cs and xs.

368

///

369

    /// Low-level Minion constraint.

370

///

371

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

372

///

373

    /// # See also

374

///

375

    /// + [Minion

376

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

377

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

378

379

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

380

///

381

    /// Low-level Minion constraint.

382

///

383

    /// # See also

384

///

385

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

386

    #[compatible(Minion)]

387

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

388

389

    /// Ensures that x*y=z.

390

///

391

    /// Low-level Minion constraint.

392

///

393

    /// # See also

394

///

395

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

396

    #[compatible(Minion)]

397

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

398

399

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

400

///

401

    /// Low-level Minion constraint.

402

///

403

    /// # See also

404

///

405

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

406

    #[compatible(Minion)]

407

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

408

409

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

410

///

411

    /// Low-level Minion constraint.

412

///

413

    /// # See also

414

///

415

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

416

    #[compatible(Minion)]

417

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

418

419

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

420

///

421

    /// Low-level Minion constraint.

422

///

423

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

424

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

425

///

426

    /// # See also

427

///

428

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

429

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

430

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

431

432

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

433

    /// variable.

434

///

435

    /// Low-level Minion constraint.

436

///

437

    /// # See also

438

///

439

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

440

    #[compatible(Minion)]

441

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

442

443

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

444

    /// variable.

445

///

446

    /// Low-level Minion constraint.

447

///

448

    /// # See also

449

///

450

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

451

    #[compatible(Minion)]

452

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

453

454

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

455

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

456

///

457

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

458

///

459

    /// Low-level Minion constraint.

460

///

461

    /// # See also

462

    ///>

463

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

464

    #[compatible(Minion)]

465

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

466

467

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

468

///

469

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

470

///

471

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

472

///

473

    /// Low-level Minion constraint.

474

///

475

    /// # See also

476

///

477

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

478

    #[compatible(Minion)]

479

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

480

481

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

482

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

483

///

484

    /// Low-level Minion constraint.

485

///

486

    /// # See also

487

///

488

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

489

    #[compatible(Minion)]

490

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

491

492

    /// Declaration of an auxiliary variable.

493

///

494

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

495

    #[compatible(Minion)]

496

    #[polyquine_skip]

497

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

498

499

    /// This expression is for encoding i32 ints as a vector of boolean expressions for cnf - using 2s complement

500

    #[compatible(SAT)]

501

    SATInt(Metadata, Moo<Expression>),

502

503

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

504

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

505

    #[compatible(SMT)]

506

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

507

508

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

509

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

510

    #[compatible(SMT)]

511

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

512

513

    #[compatible(JsonInput)]

514

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

515

516

    #[compatible(JsonInput)]

517

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

518

519

    #[compatible(JsonInput)]

520

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

521

522

    #[compatible(JsonInput)]

523

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

524

525

    #[compatible(JsonInput)]

526

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

527

528

    /// Lexicographical < between two matrices.

529

///

530

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

531

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

532

    /// then j comes after i.

533

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

534

///

535

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

536

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

537

538

    /// Lexicographical <= between two matrices

539

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

540

541

    /// Lexicographical > between two matrices

542

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

543

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

544

545

    /// Lexicographical >= between two matrices

546

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

547

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

548

549

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

550

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

551

552

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

553

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

554

555

556

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

557

// child expression.

558

//

559

// Op must be monotonic.

560

//

561

// Returns none if unbounded

562

fn bounded_i32_domain_for_matrix_literal_monotonic(

563

    e: &Expression,

564

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

565

) -> Option<DomainPtr> {

566

    // only care about the elements, not the indices

567

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

568

569

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

570

//

571

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

572

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

573

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

574

//

575

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

576

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

577

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

578

    //Int

579

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

580

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

581

//

582

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

583

584

    let expr = exprs.pop()?;

585

    let dom = expr.domain_of()?;

586

    let Some(GroundDomain::Int(ranges)) = dom.as_ground() else {

587

        return None;

588

};

589

590

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

591

592

    for expr in exprs {

593

        let dom = expr.domain_of()?;

594

        let Some(GroundDomain::Int(ranges)) = dom.as_ground() else {

595

            return None;

596

};

597

598

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

599

600

        // all the possible new values for current_min / current_max

601

        let minmax = op(min, current_max)?;

602

        let minmin = op(min, current_min)?;

603

        let maxmin = op(max, current_min)?;

604

        let maxmax = op(max, current_max)?;

605

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

606

607

        current_min = *vals

608

            .iter()

609

            .min()

610

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

611

        current_max = *vals

612

            .iter()

613

            .max()

614

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

615

616

617

    if current_min == current_max {

618

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

619

    } else {

620

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

621

622

623

624

// Returns none if unbounded

625

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

626

    let mut min = i32::MAX;

627

    let mut max = i32::MIN;

628

    for r in ranges {

629

        match r {

630

            Range::Single(i) => {

631

                if *i < min {

632

                    min = *i;

633

634

                if *i > max {

635

                    max = *i;

636

637

638

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

639

                if *i < min {

640

                    min = *i;

641

642

                if *j > max {

643

                    max = *j;

644

645

646

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

647

648

649

    Some((min, max))

650

651

652

impl Expression {

653

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

654

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

655

        //println!("domain_of {self}");

656

        let ret = match self {

657

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

658

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

659

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

660

)),

661

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

662

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

663

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

664

)),

665

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

666

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

667

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

668

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

669

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

670

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

671

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

672

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

673

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

674

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

675

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

676

                let dom = matrix.domain_of()?;

677

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

678

                    return Some(elem_domain);

679

680

681

                // may actually use the value in the future

682

                #[allow(clippy::redundant_pattern_matching)]

683

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

684

                    // TODO: We can implement proper indexing for tuples

685

                    return None;

686

687

688

                // may actually use the value in the future

689

                #[allow(clippy::redundant_pattern_matching)]

690

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

691

                    // TODO: We can implement proper indexing for records

692

                    return None;

693

694

695

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

696

697

            Expression::UnsafeSlice(_, matrix, indices)

698

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

699

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

700

701

                let dom = matrix.domain_of()?;

702

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

703

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

704

};

705

706

                match sliced_dimension {

707

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

708

                        elem_domain,

709

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

710

)),

711

712

                    // same as index

713

                    None => Some(elem_domain),

714

715

716

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

717

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

718

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

719

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

720

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

721

722

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

723

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

724

725

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

726

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

727

}),

728

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

729

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

730

}),

731

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

732

                .domain_of()?

733

                .resolve()?

734

                .apply_i32(

735

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

736

                    // including for negative numbers.

737

                    |x, y| {

738

                        if y != 0 {

739

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

740

                        } else {

741

                            None

742

743

},

744

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

745

746

                .map(DomainPtr::from)

747

                .ok(),

748

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

749

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

750

                // including for negative numbers.

751

                let domain = a

752

                    .domain_of()?

753

                    .resolve()?

754

                    .apply_i32(

755

                        |x, y| {

756

                            if y != 0 {

757

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

758

                            } else {

759

                                None

760

761

},

762

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

763

764

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

765

766

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

767

                    let mut ranges = ranges;

768

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

769

                    return Some(Domain::int(ranges));

770

                } else {

771

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

772

773

774

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

775

                .domain_of()?

776

                .resolve()?

777

                .apply_i32(

778

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

779

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

780

781

                .map(DomainPtr::from)

782

                .ok(),

783

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

784

                let domain = a

785

                    .domain_of()?

786

                    .resolve()?

787

                    .apply_i32(

788

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

789

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

790

791

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

792

793

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

794

                    let mut ranges = ranges;

795

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

796

                    return Some(Domain::int(ranges));

797

                } else {

798

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

799

800

801

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

802

                .domain_of()?

803

                .resolve()?

804

                .apply_i32(

805

                    |x, y| {

806

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

807

                            Some(x.pow(y as u32))

808

                        } else {

809

                            None

810

811

},

812

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

813

814

                .map(DomainPtr::from)

815

                .ok(),

816

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

817

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

818

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

819

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

820

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

821

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

822

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

823

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

824

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

825

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

826

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

827

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

828

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

829

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

830

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

831

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

832

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

833

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

834

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

835

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

836

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

837

                if let Some(expr) = n {

838

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

839

                        // TODO: handle flatten with depth argument

840

                        return None;

841

842

                } else {

843

                    let domain = m.domain_of()?;

844

                    let mut total_size = 1;

845

                    let index_domains: Vec<Domain> = Vec::new();

846

847

                    // calculate total flattened size

848

                    for i in &index_domains {

849

                        total_size *= i.length().ok()?;

850

851

                    let new_index_domain =

852

                        Domain::int(vec![Range::Bounded(1, total_size.try_into().unwrap())]);

853

                    return Some(Domain::matrix(domain, vec![new_index_domain]));

854

855

                None

856

857

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

858

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

859

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

860

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

861

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

862

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

863

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

864

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

865

                let dom = x.domain_of()?;

866

                let mut ranges = dom.as_int()?;

867

868

                ranges = ranges

869

                    .into_iter()

870

                    .map(|r| match r {

871

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

872

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

873

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

874

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

875

                        Range::Unbounded => Range::Unbounded,

876

})

877

                    .collect();

878

879

                Some(Domain::int(ranges))

880

881

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

882

                .domain_of()?

883

                .resolve()?

884

                .apply_i32(|x, y| Some(x - y), b.domain_of()?.resolve()?.as_ref())

885

                .map(DomainPtr::from)

886

                .ok(),

887

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

888

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

889

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

890

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

891

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

892

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

893

                .domain_of()?

894

                .resolve()?

895

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

896

                .map(DomainPtr::from)

897

                .ok(),

898

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

899

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

900

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

901

                Some(Domain::int_ground(vec![Range::Bounded(

902

                    i8::MIN.into(),

903

                    i8::MAX.into(),

904

                )])) // BITS

905

            } // A CnfInt can represent any i8 integer at the moment

906

            // A CnfInt contains multiple boolean expressions and represents the integer

907

            // formed when these booleans are treated as the bits in an integer encoding.

908

            // So the 'domain of' should be an integer

909

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

910

                .domain_of()?

911

                .resolve()?

912

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

913

                .map(DomainPtr::from)

914

                .ok(),

915

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

916

                .domain_of()?

917

                .resolve()?

918

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

919

                .map(DomainPtr::from)

920

                .ok(),

921

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

922

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

923

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

924

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

925

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

926

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

927

                let function_domain = function.domain_of()?;

928

                match function_domain.resolve().as_ref() {

929

                    Some(d) => {

930

                        match d.as_ref() {

931

                            GroundDomain::Function(attrs, _, codomain) => Some(Domain::function(

932

                                attrs.clone(),

933

                                new_domain.domain_of()?,

934

                                codomain.clone().into(),

935

)),

936

                            // Not defined for anything other than a function

937

                            _ => None,

938

939

940

                    None => {

941

                        match function_domain.as_unresolved()? {

942

                            UnresolvedDomain::Function(attrs, _, codomain) => {

943

                                Some(Domain::function(

944

                                    attrs.clone(),

945

                                    new_domain.domain_of()?,

946

                                    codomain.clone(),

947

))

948

949

                            // Not defined for anything other than a function

950

                            _ => None,

951

952

953

954

955

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

956

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

957

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

958

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

959

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

960

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

961

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

962

};

963

        if let Some(dom) = &ret

964

            && let Some(ranges) = dom.as_int_ground()

965

            && ranges.len() > 1

966

967

            // TODO: (flm8) the Minion bindings currently only support single ranges for domains, so we use the min/max bounds

968

            // Once they support a full domain as we define it, we can remove this conversion

969

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

970

            return Some(Domain::int(vec![Range::Bounded(min, max)]));

971

972

ret

973

974

975

    pub fn get_meta(&self) -> Metadata {

976

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

977

        metas[0].clone()

978

979

980

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

981

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

982

983

984

    /// Checks whether this expression is safe.

985

///

986

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

987

///

988

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

989

    /// safe through the use of bubble rules.

990

    pub fn is_safe(&self) -> bool {

991

        // TODO: memoise in Metadata

992

        for expr in self.universe() {

993

            match expr {

994

                Expression::UnsafeDiv(_, _, _)

995

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

996

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

997

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

998

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

999

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

1000

                    return false;

1001

1002

                _ => {}

1003

1004

1005

        true

1006

1007

1008

    pub fn is_clean(&self) -> bool {

1009

        let metadata = self.get_meta();

1010

        metadata.clean

1011

1012

1013

    pub fn set_clean(&mut self, bool_value: bool) {

1014

        let mut metadata = self.get_meta();

1015

        metadata.clean = bool_value;

1016

        self.set_meta(metadata);

1017

1018

1019

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

1020

    pub fn is_associative_commutative_operator(&self) -> bool {

1021

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

1022

1023

1024

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

1025

///

1026

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

1027

    /// [`Expression`].

1028

    pub fn is_matrix_literal(&self) -> bool {

1029

        matches!(

1030

            self,

1031

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

1032

                | Expression::Atomic(

1033

_,

1034

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

1035

1036

1037

1038

1039

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

1040

///

1041

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

1042

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

1043

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

1044

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

1045

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

1046

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

1047

1048

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

1049

            atom2 == atom1

1050

        } else {

1051

            false

1052

1053

1054

1055

    /// If the expression is a list, returns the inner expressions.

1056

///

1057

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

1058

    /// any explicitly specified domain.

1059

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

1060

        match self {

1061

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

1062

                matrix.unwrap_list().cloned()

1063

1064

            Expression::Atomic(

1065

_,

1066

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

1067

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

1068

                elems

1069

                    .clone()

1070

                    .into_iter()

1071

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

1072

                    .collect_vec()

1073

}),

1074

            _ => None,

1075

1076

1077

1078

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

1079

///

1080

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

1081

///

1082

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

1083

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

1084

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

1085

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

1086

        match self {

1087

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

1088

                Some((elems, domain))

1089

1090

            Expression::Atomic(

1091

_,

1092

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

1093

            ) => Some((

1094

                elems

1095

                    .into_iter()

1096

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

1097

                    .collect_vec(),

1098

                domain.into(),

1099

)),

1100

1101

            _ => None,

1102

1103

1104

1105

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

1106

///

1107

    /// # Panics

1108

    /// Panics if the expression is not Root.

1109

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

1110

        match self {

1111

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

1112

                children.extend(exprs);

1113

                Expression::Root(meta, children)

1114

1115

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

1116

1117

1118

1119

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

1120

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

1121

        match self {

1122

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

1123

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

1124

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

1125

1126

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

1127

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

1128

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

1129

};

1130

1131

                Some(Literal::Int(-i))

1132

1133

1134

            _ => None,

1135

1136

1137

1138

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

1139

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

1140

        TryFrom::try_from(self).ok()

1141

1142

1143

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

1144

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

1145

        self.universe()

1146

            .into_iter()

1147

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

1148

            .collect()

1149

1150

1151

1152

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

1153

    let function_domain = function.domain_of()?;

1154

    match function_domain.resolve().as_ref() {

1155

        Some(d) => {

1156

            match d.as_ref() {

1157

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

1158

                // Not defined for anything other than a function

1159

                _ => None,

1160

1161

1162

        None => {

1163

            match function_domain.as_unresolved()? {

1164

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

1165

                // Not defined for anything other than a function

1166

                _ => None,

1167

1168

1169

1170

1171

1172

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

1173

    let function_domain = function.domain_of()?;

1174

    match function_domain.resolve().as_ref() {

1175

        Some(d) => {

1176

            match d.as_ref() {

1177

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

1178

                // Not defined for anything other than a function

1179

                _ => None,

1180

1181

1182

        None => {

1183

            match function_domain.as_unresolved()? {

1184

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

1185

                // Not defined for anything other than a function

1186

                _ => None,

1187

1188

1189

1190

1191

1192

impl TryFrom<&Expression> for i32 {

1193

    type Error = ();

1194

1195

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

1196

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

1197

            return Err(());

1198

};

1199

1200

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

1201

            return Err(());

1202

};

1203

1204

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

1205

            return Err(());

1206

};

1207

1208

        Ok(*i)

1209

1210

1211

1212

impl TryFrom<Expression> for i32 {

1213

    type Error = ();

1214

1215

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

1216

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

1217

1218

1219

impl From<i32> for Expression {

1220

    fn from(i: i32) -> Self {

1221

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

1222

1223

1224

1225

impl From<bool> for Expression {

1226

    fn from(b: bool) -> Self {

1227

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

1228

1229

1230

1231

impl From<Atom> for Expression {

1232

    fn from(value: Atom) -> Self {

1233

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

1234

1235

1236

1237

impl From<Literal> for Expression {

1238

    fn from(value: Literal) -> Self {

1239

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

1240

1241

1242

1243

impl From<Moo<Expression>> for Expression {

1244

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

1245

        val.as_ref().clone()

1246

1247

1248

1249

impl CategoryOf for Expression {

1250

    fn category_of(&self) -> Category {

1251

        // take highest category of all the expressions children

1252

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

1253

1254

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

1255

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

1256

                // subexpressions

1257

                *max_category

1258

            } else {

1259

                // this expression has no children

1260

                let mut max_category = Category::Bottom;

1261

1262

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

1263

                // declarationptrs inside this expression

1264

1265

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

1266

1267

                // if x contains submodels (including comprehensions)

1268

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

1269

                    // assume that the category is decision

1270

                    return Category::Decision;

1271

1272

1273

                // if x contains atoms

1274

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

1275

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

1276

                && max_atom_category > max_category{

1277

                    // update category

1278

                    max_category = max_atom_category;

1279

1280

1281

                // if x contains declarationPtrs

1282

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

1283

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

1284

                && max_declaration_category > max_category{

1285

                    // update category

1286

                    max_category = max_declaration_category;

1287

1288

                max_category

1289

1290

1291

});

1292

1293

        if cfg!(debug_assertions) {

1294

            trace!(

1295

                category= %category,

1296

                expression= %self,

1297

                "Called Expression::category_of()"

1298

);

1299

};

1300

        category

1301

1302

1303

1304

impl Display for Expression {

1305

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

1306

        match &self {

1307

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

1308

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

1309

1310

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

1311

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

1312

1313

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

1314

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

1315

1316

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

1317

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

1318

1319

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

1320

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

1321

1322

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

1323

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

1324

1325

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

1326

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

1327

1328

1329

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

1330

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

1331

            Expression::UnsafeIndex(_, e1, e2) | Expression::SafeIndex(_, e1, e2) => {

1332

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

1333

1334

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

1335

                let args = es

1336

                    .iter()

1337

                    .map(|x| match x {

1338

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

1339

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

1340

})

1341

                    .join(",");

1342

1343

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

1344

1345

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

1346

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

1347

1348

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

1349

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

1350

1351

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

1352

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

1353

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

1354

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

1355

            Expression::Scope(_, submodel) => write!(f, "{{\n{submodel}\n}}"),

1356

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

1357

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

1358

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

1359

1360

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

1361

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

1362

1363

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

1364

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

1365

1366

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

1367

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

1368

1369

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

1370

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

1371

1372

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

1373

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

1374

1375

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

1376

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

1377

1378

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

1379

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

1380

1381

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

1382

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

1383

1384

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

1385

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

1386

1387

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

1388

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

1389

1390

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

1391

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

1392

1393

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

1394

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

1395

1396

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

1397

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

1398

1399

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

1400

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

1401

1402

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

1403

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

1404

1405

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

1406

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

1407

1408

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

1409

f,

1410

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

1411

                box1.clone(),

1412

                box2.clone(),

1413

                box3.clone()

1414

),

1415

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

1416

                if let Some(n) = n {

1417

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

1418

                } else {

1419

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

1420

1421

1422

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

1423

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

1424

1425

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

1426

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

1427

1428

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

1429

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

1430

1431

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

1432

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

1433

1434

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

1435

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

1436

1437

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

1438

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

1439

1440

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

1441

                write!(

1442

f,

1443

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

1444

                    box1.clone(),

1445

                    box2.clone(),

1446

                    box3.clone()

1447

1448

1449

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

1450

                write!(

1451

f,

1452

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

1453

                    box1.clone(),

1454

                    box2.clone(),

1455

                    box3.clone()

1456

1457

1458

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

1459

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

1460

1461

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

1462

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

1463

1464

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

1465

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

1466

1467

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

1468

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

1469

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

1470

1471

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

1472

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

1473

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

1474

1475

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

1476

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

1477

1478

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

1479

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

1480

1481

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

1482

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

1483

1484

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

1485

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

1486

1487

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

1488

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

1489

1490

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

1491

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

1492

1493

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

1494

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

1495

1496

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

1497

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

1498

1499

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

1500

                write!(

1501

f,

1502

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

1503

                    a.clone(),

1504

                    b.clone(),

1505

                    c.clone()

1506

1507

1508

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

1509

                write!(

1510

f,

1511

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

1512

                    pretty_vec(cs),

1513

                    pretty_vec(vs),

1514

                    total.clone()

1515

1516

1517

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

1518

                write!(

1519

f,

1520

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

1521

                    pretty_vec(cs),

1522

                    pretty_vec(vs),

1523

                    total.clone()

1524

1525

1526

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

1527

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

1528

1529

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

1530

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

1531

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

1532

1533

1534

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

1535

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

1536

1537

1538

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

1539

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

1540

1541

1542

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

1543

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

1544

1545

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

1546

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

1547

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

1548

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

1549

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

1550

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

1551

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

1552

1553

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

1554

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

1555

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

1556

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

1557

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

1558

                write!(f, "FlatLexLt({}, {})", pretty_vec(a), pretty_vec(b))

1559

1560

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

1561

                write!(f, "FlatLexLeq({}, {})", pretty_vec(a), pretty_vec(b))

1562

1563

1564

1565

1566

1567

impl Typeable for Expression {

1568

    fn return_type(&self) -> ReturnType {

1569

        match self {

1570

            Expression::Union(_, subject, _) => ReturnType::Set(Box::new(subject.return_type())),

1571

            Expression::Intersect(_, subject, _) => {

1572

                ReturnType::Set(Box::new(subject.return_type()))

1573

1574

            Expression::In(_, _, _) => ReturnType::Bool,

1575

            Expression::Supset(_, _, _) => ReturnType::Bool,

1576

            Expression::SupsetEq(_, _, _) => ReturnType::Bool,

1577

            Expression::Subset(_, _, _) => ReturnType::Bool,

1578

            Expression::SubsetEq(_, _, _) => ReturnType::Bool,

1579

            Expression::AbstractLiteral(_, lit) => lit.return_type(),

1580

            Expression::UnsafeIndex(_, subject, idx) | Expression::SafeIndex(_, subject, idx) => {

1581

                let subject_ty = subject.return_type();

1582

                match subject_ty {

1583

                    ReturnType::Matrix(_) => {

1584

                        // For n-dimensional matrices, unwrap the element type until

1585

                        // we either get to the innermost element type or the last index

1586

                        let mut elem_typ = subject_ty;

1587

                        let mut idx_len = idx.len();

1588

                        while idx_len > 0

1589

                            && let ReturnType::Matrix(new_elem_typ) = &elem_typ

1590

1591

                            elem_typ = *new_elem_typ.clone();

1592

                            idx_len -= 1;

1593

1594

                        elem_typ

1595

1596

                    // TODO: We can implement indexing for these eventually

1597

                    ReturnType::Record(_) | ReturnType::Tuple(_) => ReturnType::Unknown,

1598

                    _ => bug!(

1599

                        "Invalid indexing operation: expected the operand to be a collection, got {self}: {subject_ty}"

1600

),

1601

1602

1603

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

1604

                ReturnType::Matrix(Box::new(subject.return_type()))

1605

1606

            Expression::InDomain(_, _, _) => ReturnType::Bool,

1607

            Expression::Comprehension(_, comp) => comp.return_type(),

1608

            Expression::Root(_, _) => ReturnType::Bool,

1609

            Expression::DominanceRelation(_, _) => ReturnType::Bool,

1610

            Expression::FromSolution(_, expr) => expr.return_type(),

1611

            Expression::Metavar(_, _) => ReturnType::Unknown,

1612

            Expression::Atomic(_, atom) => atom.return_type(),

1613

            Expression::Scope(_, scope) => scope.return_type(),

1614

            Expression::Abs(_, _) => ReturnType::Int,

1615

            Expression::Sum(_, _) => ReturnType::Int,

1616

            Expression::Product(_, _) => ReturnType::Int,

1617

            Expression::Min(_, _) => ReturnType::Int,

1618

            Expression::Max(_, _) => ReturnType::Int,

1619

            Expression::Not(_, _) => ReturnType::Bool,

1620

            Expression::Or(_, _) => ReturnType::Bool,

1621

            Expression::Imply(_, _, _) => ReturnType::Bool,

1622

            Expression::Iff(_, _, _) => ReturnType::Bool,

1623

            Expression::And(_, _) => ReturnType::Bool,

1624

            Expression::Eq(_, _, _) => ReturnType::Bool,

1625

            Expression::Neq(_, _, _) => ReturnType::Bool,

1626

            Expression::Geq(_, _, _) => ReturnType::Bool,

1627

            Expression::Leq(_, _, _) => ReturnType::Bool,

1628

            Expression::Gt(_, _, _) => ReturnType::Bool,

1629

            Expression::Lt(_, _, _) => ReturnType::Bool,

1630

            Expression::SafeDiv(_, _, _) => ReturnType::Int,

1631

            Expression::UnsafeDiv(_, _, _) => ReturnType::Int,

1632

            Expression::FlatAllDiff(_, _) => ReturnType::Bool,

1633

            Expression::FlatSumGeq(_, _, _) => ReturnType::Bool,

1634

            Expression::FlatSumLeq(_, _, _) => ReturnType::Bool,

1635

            Expression::MinionDivEqUndefZero(_, _, _, _) => ReturnType::Bool,

1636

            Expression::FlatIneq(_, _, _, _) => ReturnType::Bool,

1637

            Expression::Flatten(_, _, matrix) => {

1638

                let matrix_type = matrix.return_type();

1639

                match matrix_type {

1640

                    ReturnType::Matrix(_) => {

1641

                        // unwrap until we get to innermost element

1642

                        let mut elem_type = matrix_type;

1643

                        while let ReturnType::Matrix(new_elem_type) = &elem_type {

1644

                            elem_type = *new_elem_type.clone();

1645

1646

                        ReturnType::Matrix(Box::new(elem_type))

1647

1648

                    _ => bug!(

1649

                        "Invalid indexing operation: expected the operand to be a collection, got {self}: {matrix_type}"

1650

),

1651

1652

1653

            Expression::AllDiff(_, _) => ReturnType::Bool,

1654

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

1655

            Expression::FlatWatchedLiteral(_, _, _) => ReturnType::Bool,

1656

            Expression::MinionReify(_, _, _) => ReturnType::Bool,

1657

            Expression::MinionReifyImply(_, _, _) => ReturnType::Bool,

1658

            Expression::MinionWInIntervalSet(_, _, _) => ReturnType::Bool,

1659

            Expression::MinionWInSet(_, _, _) => ReturnType::Bool,

1660

            Expression::MinionElementOne(_, _, _, _) => ReturnType::Bool,

1661

            Expression::AuxDeclaration(_, _, _) => ReturnType::Bool,

1662

            Expression::UnsafeMod(_, _, _) => ReturnType::Int,

1663

            Expression::SafeMod(_, _, _) => ReturnType::Int,

1664

            Expression::MinionModuloEqUndefZero(_, _, _, _) => ReturnType::Bool,

1665

            Expression::Neg(_, _) => ReturnType::Int,

1666

            Expression::UnsafePow(_, _, _) => ReturnType::Int,

1667

            Expression::SafePow(_, _, _) => ReturnType::Int,

1668

            Expression::Minus(_, _, _) => ReturnType::Int,

1669

            Expression::FlatAbsEq(_, _, _) => ReturnType::Bool,

1670

            Expression::FlatMinusEq(_, _, _) => ReturnType::Bool,

1671

            Expression::FlatProductEq(_, _, _, _) => ReturnType::Bool,

1672

            Expression::FlatWeightedSumLeq(_, _, _, _) => ReturnType::Bool,

1673

            Expression::FlatWeightedSumGeq(_, _, _, _) => ReturnType::Bool,

1674

            Expression::MinionPow(_, _, _, _) => ReturnType::Bool,

1675

            Expression::ToInt(_, _) => ReturnType::Int,

1676

            Expression::SATInt(_, _) => ReturnType::Int,

1677

            Expression::PairwiseSum(_, _, _) => ReturnType::Int,

1678

            Expression::PairwiseProduct(_, _, _) => ReturnType::Int,

1679

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

1680

                let subject = function.return_type();

1681

                match subject {

1682

                    ReturnType::Function(domain, _) => *domain,

1683

                    _ => bug!(

1684

                        "Invalid defined operation: expected the operand to be a function, got {self}: {subject}"

1685

),

1686

1687

1688

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

1689

                let subject = function.return_type();

1690

                match subject {

1691

                    ReturnType::Function(_, codomain) => *codomain,

1692

                    _ => bug!(

1693

                        "Invalid range operation: expected the operand to be a function, got {self}: {subject}"

1694

),

1695

1696

1697

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

1698

                let subject = function.return_type();

1699

                match subject {

1700

                    ReturnType::Function(_, codomain) => *codomain,

1701

                    _ => bug!(

1702

                        "Invalid image operation: expected the operand to be a function, got {self}: {subject}"

1703

),

1704

1705

1706

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

1707

                let subject = function.return_type();

1708

                match subject {

1709

                    ReturnType::Function(_, codomain) => *codomain,

1710

                    _ => bug!(

1711

                        "Invalid imageSet operation: expected the operand to be a function, got {self}: {subject}"

1712

),

1713

1714

1715

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

1716

                let subject = function.return_type();

1717

                match subject {

1718

                    ReturnType::Function(domain, _) => *domain,

1719

                    _ => bug!(

1720

                        "Invalid preImage operation: expected the operand to be a function, got {self}: {subject}"

1721

),

1722

1723

1724

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

1725

                let subject = function.return_type();

1726

                match subject {

1727

                    ReturnType::Function(_, codomain) => {

1728

                        ReturnType::Function(Box::new(new_domain.return_type()), codomain)

1729

1730

                    _ => bug!(

1731

                        "Invalid preImage operation: expected the operand to be a function, got {self}: {subject}"

1732

),

1733

1734

1735

            Expression::Inverse(..) => ReturnType::Bool,

1736

            Expression::LexLt(..) => ReturnType::Bool,

1737

            Expression::LexGt(..) => ReturnType::Bool,

1738

            Expression::LexLeq(..) => ReturnType::Bool,

1739

            Expression::LexGeq(..) => ReturnType::Bool,

1740

            Expression::FlatLexLt(..) => ReturnType::Bool,

1741

            Expression::FlatLexLeq(..) => ReturnType::Bool,

1742

1743

1744

1745

1746

#[cfg(test)]

1747

mod tests {

1748

1749

    use crate::matrix_expr;

1750

1751

    use super::*;

1752

1753

    #[test]

1754

    fn test_domain_of_constant_sum() {

1755

        let c1 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));

1756

        let c2 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(2)));

1757

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![c1, c2]));

1758

        assert_eq!(sum.domain_of(), Some(Domain::int(vec![Range::Single(3)])));

1759

1760

1761

    #[test]

1762

    fn test_domain_of_constant_invalid_type() {

1763

        let c1 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(1)));

1764

        let c2 = Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(true)));

1765

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![c1, c2]));

1766

        assert_eq!(sum.domain_of(), None);

1767

1768

1769

    #[test]

1770

    fn test_domain_of_empty_sum() {

1771

        let sum = Expression::Sum(Metadata::new(), Moo::new(matrix_expr![]));

1772

        assert_eq!(sum.domain_of(), None);

1773

1774