Grcov report - representations.rs

1

use conjure_cp::ast::records::Field;

2

use conjure_cp::ast::{

3

    AbstractLiteral, BinaryAttr, Domain, Expression, FuncAttr, GroundDomain, JectivityAttr,

4

    Literal, MSetAttr, Metadata, Moo, Name, PartialityAttr, PartitionAttr, PermutationAttr,

5

    Reference, RelAttr, SequenceAttr, SetAttr, SymbolTable,

6

};

7

use conjure_cp::representation::{ReprAssignment, ReprDomainLevel, ReprRule};

8

use conjure_cp::{domain_int, into_matrix, range};

9

use conjure_cp_rules::representation::{

10

    FunctionAsRelation, FunctionExplicit, FunctionPacked, MSetCounts, MSetOccurrence, MSetPacked,

11

    MSetRepetition, MatrixComponents, MatrixPacked, PartitionAsSet, PartitionOccurrence,

12

    PartitionPacked, PermutationAsFunction, RecordComponents, RecordPacked, RelationAsSet,

13

    RelationOccurrence, RelationPacked, SequenceExplicit, SequencePacked, SetExplicit,

14

    SetOccurrence, SetPacked, TupleComponents, TuplePacked, VariantComponents, VariantPacked,

15

};

16

use uniplate::Uniplate;

17

18

#[test]

19

1

fn representation_short_names_describe_the_generated_layout() {

20

1

    assert_eq!(MatrixComponents::SHORT_NAME, "components");

21

1

    assert_eq!(MatrixPacked::SHORT_NAME, "packed");

22

1

    assert_eq!(TupleComponents::SHORT_NAME, "components");

23

1

    assert_eq!(SetPacked::SHORT_NAME, "packed");

24

1

    assert_eq!(TuplePacked::SHORT_NAME, "packed");

25

1

    assert_eq!(SetExplicit::SHORT_NAME, "explicit");

26

1

    assert_eq!(SetOccurrence::SHORT_NAME, "occurrence");

27

1

    assert_eq!(RecordComponents::SHORT_NAME, "components");

28

1

    assert_eq!(RecordPacked::SHORT_NAME, "packed");

29

1

    assert_eq!(VariantComponents::SHORT_NAME, "components");

30

1

    assert_eq!(VariantPacked::SHORT_NAME, "packed");

31

1

    assert_eq!(SequenceExplicit::SHORT_NAME, "explicit");

32

1

    assert_eq!(SequencePacked::SHORT_NAME, "packed");

33

1

    assert_eq!(RelationAsSet::SHORT_NAME, "as_set");

34

1

    assert_eq!(FunctionAsRelation::SHORT_NAME, "as_relation");

35

1

    assert_eq!(FunctionExplicit::SHORT_NAME, "explicit");

36

1

    assert_eq!(MSetRepetition::SHORT_NAME, "repetition");

37

1

    assert_eq!(MSetCounts::SHORT_NAME, "counts");

38

1

    assert_eq!(MSetOccurrence::SHORT_NAME, "occurrence");

39

1

    assert_eq!(MSetPacked::SHORT_NAME, "packed");

40

1

41

42

#[test]

43

1

fn counts_equality_compares_canonical_slots_instead_of_enumerating_values() {

44

2

    let domain = |max_size| Domain::mset(MSetAttr::new_max_size(max_size), domain_int!(1..999));

45

1

    let mut symbols = SymbolTable::new();

46

1

    let mut lhs = symbols.gen_find(&domain(6));

47

1

    let mut rhs = symbols.gen_find(&domain(8));

48

1

    MSetCounts::init_for(&mut lhs).unwrap();

49

1

    MSetCounts::init_for(&mut rhs).unwrap();

50

51

1

    let equality = lhs

52

1

        .get_repr::<MSetCounts>()

53

1

        .unwrap()

54

1

        .equality_expr(&rhs.get_repr::<MSetCounts>().unwrap());

55

1

    let universe = equality.universe();

56

57

    // Six shared slots compare count and value; the two unmatched slots must have count zero.

58

1

    assert_eq!(

59

1

        universe

60

1

            .iter()

61

96

            .filter(|expr| matches!(expr, Expression::Eq(..)))

62

            .count(),

63

1

64

);

65

1

    assert!(

66

1

        universe

67

1

            .iter()

68

96

            .all(|expr| !matches!(expr, Expression::Sum(..) | Expression::Product(..)))

69

);

70

1

71

72

#[test]

73

1

fn mset_union_domain_preserves_the_selected_reference_representation() {

74

1

    let domain = Domain::mset(MSetAttr::new_max_size(6), domain_int!(1..999));

75

1

    let mut symbols = SymbolTable::new();

76

1

    let mut declaration = symbols.gen_find(&domain);

77

1

    MSetCounts::init_for(&mut declaration).unwrap();

78

79

1

    let union = Expression::Union(

80

1

        Metadata::new(),

81

1

        Moo::new(Expression::from(Reference {

82

1

            ptr: declaration,

83

1

            repr: Some(MSetCounts::STORED),

84

1

        })),

85

1

        Moo::new(Expression::AbstractLiteral(

86

1

            Metadata::new(),

87

1

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

88

1

)),

89

1

);

90

91

1

    let result = union.domain_of().unwrap();

92

1

    let (attrs, _) = result.as_mset_ground().unwrap();

93

1

    assert_eq!(attrs.size, range!(2..8));

94

1

    assert_eq!(attrs.representation.as_deref(), Some("counts"));

95

1

96

97

#[test]

98

1

fn variant_components_and_packed_round_trip() {

99

1

    let domain = Domain::variant(vec![

100

1

        Field {

101

1

            name: Name::user("flag"),

102

1

            value: Domain::bool(),

103

1

},

104

1

        Field {

105

1

            name: Name::user("value"),

106

1

            value: domain_int!(2..4),

107

1

},

108

1

]);

109

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Variant(Moo::new(Field {

110

1

        name: Name::user("value"),

111

1

        value: Literal::Int(3),

112

1

    })));

113

114

1

    let components = <VariantComponents as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

115

1

    let component_assignment = components.down(value.clone()).unwrap();

116

1

    assert_eq!(component_assignment.tag, Literal::Int(2));

117

1

    assert_eq!(component_assignment.fields[0], Literal::Bool(false));

118

1

    assert_eq!(component_assignment.up(), value);

119

120

1

    let packed = <VariantPacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

121

1

    let packed_assignment = packed.down(value.clone()).unwrap();

122

1

    assert_eq!(packed_assignment.packed, Literal::Int(3));

123

1

    assert_eq!(packed_assignment.up(), value);

124

1

    assert_eq!(VariantPacked::compactness_score(domain).unwrap(), 5);

125

1

126

127

#[test]

128

1

fn packed_matrix_round_trips_primitive_values_and_weird_indices() {

129

1

    let inner_indices = GroundDomain::Int(

130

1

        vec![

131

1

            conjure_cp::ast::Range::Single(1),

132

1

            conjure_cp::ast::Range::Single(3),

133

1

],

134

1

        None,

135

1

);

136

1

    let domain = Domain::matrix(

137

1

        domain_int!(2..4),

138

1

        vec![Domain::bool(), Domain::from(inner_indices.clone()).into()],

139

1

);

140

2

    let row = |values| {

141

2

        Literal::AbstractLiteral(AbstractLiteral::Matrix(

142

2

            values,

143

2

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

144

2

))

145

2

};

146

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Matrix(

147

1

        vec![

148

1

            row(vec![Literal::Int(2), Literal::Int(4)]),

149

1

            row(vec![Literal::Int(3), Literal::Int(2)]),

150

1

],

151

1

        Moo::new(GroundDomain::Bool),

152

1

));

153

154

1

    let state = <MatrixPacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

155

1

    let assignment = state.down(value.clone()).unwrap();

156

1

    assert_eq!(assignment.packed, Literal::Int(21));

157

1

    assert_eq!(assignment.up(), value);

158

1

    assert_eq!(MatrixPacked::compactness_score(domain.clone()).unwrap(), 81);

159

160

1

    let mut symbols = SymbolTable::new();

161

1

    let mut declaration = symbols.gen_find(&domain);

162

1

    let (new_symbols, constraints) = MatrixPacked::init_for(&mut declaration).unwrap();

163

1

    assert_eq!(new_symbols.iter_local().count(), 1);

164

1

    assert!(constraints.is_empty());

165

1

    let decoded = declaration

166

1

        .get_repr::<MatrixPacked>()

167

1

        .unwrap()

168

1

        .decoded_matrix();

169

1

    assert_eq!(

170

1

        decoded

171

1

            .universe()

172

1

            .iter()

173

53

            .filter(|expr| matches!(expr, Expression::SafeIndex(..)))

174

            .count(),

175

1

176

);

177

1

178

179

#[test]

180

1

fn packed_matrix_orders_booleans_false_before_true() {

181

1

    let domain = Domain::matrix(Domain::bool(), vec![domain_int!(1..2)]);

182

1

    let state = <MatrixPacked as ReprRule>::DomainLevel::init(domain).unwrap();

183

1

    assert_eq!(

184

1

        state.values.as_ref(),

185

1

        &[Literal::Bool(false), Literal::Bool(true)]

186

);

187

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Matrix(

188

1

        vec![Literal::Bool(true), Literal::Bool(false)],

189

1

        Moo::new(GroundDomain::Int(

190

1

            vec![conjure_cp::ast::Range::Bounded(1, 2)],

191

1

            None,

192

1

)),

193

1

));

194

1

    let assignment = state.down(value.clone()).unwrap();

195

1

    assert_eq!(assignment.packed, Literal::Int(2));

196

1

    assert_eq!(assignment.up(), value);

197

1

198

199

#[test]

200

1

fn matrix_representation_initialises_and_maps_indices() {

201

1

    let domain = Domain::matrix(

202

1

        Domain::bool(),

203

1

        vec![Domain::bool(), domain_int!(1, 3, 5, 7)],

204

1

);

205

206

1

    let domain_state = <MatrixComponents as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

207

1

    assert_eq!(domain_state.dimensions, vec![2, 4]);

208

1

    assert_eq!(domain_state.strides, vec![4, 1]);

209

1

    assert_eq!(

210

1

        domain_state

211

1

            .indices_lits_to_flat(&[Literal::Bool(true), Literal::Int(5)])

212

1

            .unwrap(),

213

1

214

);

215

216

1

    let mut symbols = SymbolTable::new();

217

1

    let mut declaration = symbols.gen_find(&domain);

218

1

    let (new_symbols, constraints) = MatrixComponents::init_for(&mut declaration).unwrap();

219

1

    assert!(constraints.is_empty());

220

1

    assert_eq!(new_symbols.iter_local().count(), 8);

221

1

    assert!(

222

1

        new_symbols

223

1

            .iter_local()

224

8

            .all(|(name, _)| name.to_string().contains("#components_"))

225

);

226

1

    assert!(declaration.get_repr::<MatrixComponents>().is_some());

227

228

1

    let detached = declaration.detach();

229

1

    assert!(detached.get_repr::<MatrixComponents>().is_some());

230

1

231

232

#[test]

233

1

fn matrix_components_instantiate_uses_per_cell_element_domains() {

234

1

    let inner = Domain::sequence(sequence_attr(range!(0..10)), domain_int!(1..9));

235

1

    let domain = Domain::matrix(inner, vec![domain_int!(1..2)]);

236

1

    let mut symbols = SymbolTable::new();

237

1

    let mut declaration = symbols.gen_find(&domain);

238

239

1

        let mut var = declaration.as_find_mut().expect("find");

240

1

        var.element_domains = Some(vec![

241

1

            Domain::sequence(sequence_attr(range!(3)), domain_int!(1..9)).into(),

242

1

            Domain::sequence(sequence_attr(range!(5)), domain_int!(1..9)).into(),

243

1

]);

244

245

246

1

    MatrixComponents::init_for(&mut declaration).unwrap();

247

1

    let components = declaration

248

1

        .get_repr::<MatrixComponents>()

249

1

        .expect("MatrixComponents");

250

1

    let sizes: Vec<_> = components

251

1

        .elements

252

1

        .iter()

253

2

        .map(|elem| {

254

2

            let domain = elem.domain().unwrap();

255

2

            let GroundDomain::Sequence(attr, _) = domain.as_ground().unwrap() else {

256

                panic!("expected a sequence component domain, got {domain}");

257

};

258

2

            attr.size.clone()

259

2

})

260

        .collect();

261

1

    assert_eq!(sizes, vec![range!(3), range!(5)]);

262

1

263

264

#[test]

265

1

fn record_components_round_trip_values_in_canonical_field_order() {

266

1

    let domain = Domain::record(vec![

267

1

        Field {

268

1

            name: Name::user("z"),

269

1

            value: Domain::bool(),

270

1

},

271

1

        Field {

272

1

            name: Name::user("a"),

273

1

            value: domain_int!(1..3),

274

1

},

275

1

]);

276

1

    let state = <RecordComponents as ReprRule>::DomainLevel::init(domain).unwrap();

277

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Record(vec![

278

1

        Field {

279

1

            name: Name::user("z"),

280

1

            value: Literal::Bool(true),

281

1

},

282

1

        Field {

283

1

            name: Name::user("a"),

284

1

            value: Literal::Int(2),

285

1

},

286

1

    ]));

287

288

1

    let assignment = state.down(value).unwrap();

289

1

    assert_eq!(

290

1

        assignment.up(),

291

1

        Literal::AbstractLiteral(AbstractLiteral::Record(vec![

292

1

            Field {

293

1

                name: Name::user("a"),

294

1

                value: Literal::Int(2),

295

1

},

296

1

            Field {

297

1

                name: Name::user("z"),

298

1

                value: Literal::Bool(true),

299

1

},

300

1

]))

301

);

302

1

303

304

#[test]

305

1

fn packed_record_round_trips_boolean_integer_and_nested_record_fields() {

306

1

    let domain = Domain::record(vec![

307

1

        Field {

308

1

            name: Name::user("z"),

309

1

            value: Domain::record(vec![

310

1

                Field {

311

1

                    name: Name::user("flag"),

312

1

                    value: Domain::bool(),

313

1

},

314

1

                Field {

315

1

                    name: Name::user("value"),

316

1

                    value: domain_int!(1, 3),

317

1

},

318

1

]),

319

1

},

320

1

        Field {

321

1

            name: Name::user("a"),

322

1

            value: Domain::bool(),

323

1

},

324

1

]);

325

1

    let state = <RecordPacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

326

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Record(vec![

327

1

        Field {

328

1

            name: Name::user("z"),

329

1

            value: Literal::AbstractLiteral(AbstractLiteral::Record(vec![

330

1

                Field {

331

1

                    name: Name::user("value"),

332

1

                    value: Literal::Int(3),

333

1

},

334

1

                Field {

335

1

                    name: Name::user("flag"),

336

1

                    value: Literal::Bool(false),

337

1

},

338

1

            ])),

339

1

},

340

1

        Field {

341

1

            name: Name::user("a"),

342

1

            value: Literal::Bool(false),

343

1

},

344

1

    ]));

345

346

1

    let assignment = state.down(value).unwrap();

347

1

    assert_eq!(assignment.packed, Literal::Int(1));

348

1

    assert_eq!(

349

1

        assignment.up(),

350

1

        Literal::AbstractLiteral(AbstractLiteral::Record(vec![

351

1

            Field {

352

1

                name: Name::user("a"),

353

1

                value: Literal::Bool(false),

354

1

},

355

1

            Field {

356

1

                name: Name::user("z"),

357

1

                value: Literal::AbstractLiteral(AbstractLiteral::Record(vec![

358

1

                    Field {

359

1

                        name: Name::user("flag"),

360

1

                        value: Literal::Bool(false),

361

1

},

362

1

                    Field {

363

1

                        name: Name::user("value"),

364

1

                        value: Literal::Int(3),

365

1

},

366

1

                ])),

367

1

},

368

1

]))

369

);

370

1

    assert_eq!(RecordPacked::compactness_score(domain).unwrap(), 8);

371

1

372

373

#[test]

374

1

fn packed_tuple_round_trips_integer_values() {

375

1

    let domain = Domain::tuple(vec![domain_int!(2..4), domain_int!(10..12)]);

376

1

    let state = <TuplePacked as ReprRule>::DomainLevel::init(domain).unwrap();

377

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Tuple(vec![

378

1

        Literal::Int(3),

379

1

        Literal::Int(11),

380

1

    ]));

381

382

1

    let assignment = state.down(value.clone()).unwrap();

383

1

    assert_eq!(assignment.packed, Literal::Int(4));

384

1

    assert_eq!(assignment.up(), value);

385

1

386

387

#[test]

388

1

fn packed_tuple_round_trips_boolean_and_nested_values() {

389

1

    let domain = Domain::tuple(vec![

390

1

        Domain::bool(),

391

1

        Domain::tuple(vec![Domain::bool(), domain_int!(1..2)]),

392

1

]);

393

1

    let state = <TuplePacked as ReprRule>::DomainLevel::init(domain).unwrap();

394

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Tuple(vec![

395

1

        Literal::Bool(false),

396

1

        Literal::AbstractLiteral(AbstractLiteral::Tuple(vec![

397

1

            Literal::Bool(true),

398

1

            Literal::Int(2),

399

1

        ])),

400

1

    ]));

401

402

1

    let assignment = state.down(value.clone()).unwrap();

403

1

    assert_eq!(assignment.packed, Literal::Int(3));

404

1

    assert_eq!(assignment.up(), value);

405

1

    assert_eq!(

406

1

        state.values[0],

407

1

        vec![Literal::Bool(false), Literal::Bool(true)]

408

);

409

1

410

411

#[test]

412

1

fn packed_tuple_uses_dense_holey_integer_digits() {

413

1

    let domain = Domain::tuple(vec![domain_int!(1, 3), domain_int!(5..6)]);

414

1

    let mut symbols = SymbolTable::new();

415

1

    let mut declaration = symbols.gen_find(&domain);

416

1

    let (_, constraints) = TuplePacked::init_for(&mut declaration).unwrap();

417

418

1

    assert!(constraints.is_empty());

419

1

    assert_eq!(TuplePacked::compactness_score(domain).unwrap(), 4);

420

1

421

422

#[test]

423

1

fn packed_tuple_supports_the_nullary_tuple() {

424

1

    let domain = Domain::tuple(vec![]);

425

1

    let state = <TuplePacked as ReprRule>::DomainLevel::init(domain).unwrap();

426

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Tuple(vec![]));

427

428

1

    let assignment = state.down(value.clone()).unwrap();

429

1

    assert_eq!(assignment.packed, Literal::Int(0));

430

1

    assert_eq!(assignment.up(), value);

431

1

432

433

#[test]

434

1

fn occurrence_set_round_trips_and_enforces_cardinality() {

435

1

    let domain = Domain::set(SetAttr::new_min_max_size(1, 2), domain_int!(1..3));

436

1

    let state = <SetOccurrence as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

437

    let value =

438

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(3), Literal::Int(1)]));

439

440

1

    let assignment = state.down(value).unwrap();

441

1

    assert_eq!(

442

1

        assignment.up(),

443

1

        Literal::AbstractLiteral(AbstractLiteral::Set(

444

1

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

445

1

))

446

);

447

448

1

    let mut symbols = SymbolTable::new();

449

1

    let mut declaration = symbols.gen_find(&domain);

450

1

    let (new_symbols, constraints) = SetOccurrence::init_for(&mut declaration).unwrap();

451

1

    assert_eq!(new_symbols.iter_local().count(), 3);

452

1

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

453

1

454

455

#[test]

456

1

fn occurrence_set_supports_non_integer_elements() {

457

1

    let element_domain = Domain::tuple(vec![Domain::bool(), domain_int!(1..2)]);

458

1

    let domain = Domain::set(SetAttr::new_size(1), element_domain);

459

1

    let state = <SetOccurrence as ReprRule>::DomainLevel::init(domain).unwrap();

460

1

    let element = Literal::AbstractLiteral(AbstractLiteral::Tuple(vec![

461

1

        Literal::Bool(true),

462

1

        Literal::Int(2),

463

1

    ]));

464

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Set(vec![element]));

465

466

1

    assert_eq!(state.down(value.clone()).unwrap().up(), value);

467

1

    assert!(

468

1

        state

469

1

            .occurs

470

1

            .iter()

471

4

            .all(|(key, _)| matches!(key, Literal::AbstractLiteral(AbstractLiteral::Tuple(_))))

472

);

473

1

474

475

#[test]

476

1

fn explicit_set_round_trips_with_padding() {

477

1

    let domain = Domain::set(SetAttr::new_min_max_size(1, 3), domain_int!(1..4));

478

1

    let state = <SetExplicit as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

479

    let value =

480

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(4), Literal::Int(2)]));

481

482

1

    let assignment = state.down(value).unwrap();

483

1

    assert_eq!(assignment.set_size, Some(Literal::Int(2)));

484

1

    assert_eq!(

485

1

        assignment.elems_matrix,

486

1

        Literal::from(conjure_cp::into_matrix!(vec![

487

1

            Literal::Int(2),

488

1

            Literal::Int(4),

489

1

            Literal::Int(1),

490

1

]))

491

);

492

1

    assert_eq!(

493

1

        assignment.up(),

494

1

        Literal::AbstractLiteral(AbstractLiteral::Set(

495

1

            vec![Literal::Int(2), Literal::Int(4),]

496

1

))

497

);

498

499

1

    let mut symbols = SymbolTable::new();

500

1

    let mut declaration = symbols.gen_find(&domain);

501

1

    let (new_symbols, constraints) = SetExplicit::init_for(&mut declaration).unwrap();

502

1

    assert_eq!(new_symbols.iter_local().count(), 2);

503

1

    assert_eq!(constraints.len(), 5);

504

1

    assert_eq!(

505

1

        constraints

506

1

            .iter()

507

1

            .flat_map(Uniplate::universe)

508

58

            .filter(|expr| matches!(expr, Expression::SafeIndex(..)))

509

            .count(),

510

1

511

);

512

1

513

514

#[test]

515

1

fn fixed_explicit_set_omits_the_cardinality_marker() {

516

1

    let domain = Domain::set(SetAttr::new_size(2), domain_int!(1..3));

517

1

    let state = <SetExplicit as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

518

    let value =

519

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(3), Literal::Int(1)]));

520

521

1

    let assignment = state.down(value.clone()).unwrap();

522

1

    assert_eq!(assignment.set_size, None);

523

1

    assert_eq!(

524

1

        assignment.up(),

525

1

        Literal::AbstractLiteral(AbstractLiteral::Set(

526

1

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

527

1

))

528

);

529

530

1

    let mut symbols = SymbolTable::new();

531

1

    let mut declaration = symbols.gen_find(&domain);

532

1

    let (new_symbols, _) = SetExplicit::init_for(&mut declaration).unwrap();

533

1

    assert_eq!(new_symbols.iter_local().count(), 1);

534

1

    assert!(

535

1

        declaration

536

1

            .get_repr::<SetExplicit>()

537

1

            .unwrap()

538

1

            .set_size

539

1

            .is_none()

540

);

541

1

542

543

#[test]

544

1

fn packed_set_round_trips_and_enforces_cardinality() {

545

1

    let domain = Domain::set(SetAttr::new_min_max_size(1, 2), domain_int!(1..3));

546

1

    let state = <SetPacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

547

    let value =

548

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(3), Literal::Int(1)]));

549

550

1

    let assignment = state.down(value).unwrap();

551

1

    assert_eq!(assignment.packed, Literal::Int(5));

552

1

    assert_eq!(

553

1

        assignment.up(),

554

1

        Literal::AbstractLiteral(AbstractLiteral::Set(

555

1

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

556

1

))

557

);

558

559

1

    let mut symbols = SymbolTable::new();

560

1

    let mut declaration = symbols.gen_find(&domain);

561

1

    let (new_symbols, constraints) = SetPacked::init_for(&mut declaration).unwrap();

562

1

    assert_eq!(new_symbols.iter_local().count(), 1);

563

1

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

564

565

1

    let representation = declaration.get_repr::<SetPacked>().unwrap();

566

1

    let membership = representation.membership_expr(Expression::from(2));

567

1

    assert!(

568

1

        membership

569

1

            .universe()

570

1

            .iter()

571

2

            .any(|expr| matches!(expr, Expression::UnsafeMod(..)))

572

);

573

1

    assert!(

574

1

        membership

575

1

            .universe()

576

1

            .iter()

577

7

            .all(|expr| !matches!(expr, Expression::MinionWInSet(..)))

578

);

579

580

1

    assert_eq!(SetPacked::compactness_score(domain.clone()).unwrap(), 6);

581

1

    assert_eq!(SetOccurrence::compactness_score(domain).unwrap(), 8);

582

1

583

584

#[test]

585

1

fn packed_set_supports_non_integer_elements() {

586

1

    let domain = Domain::set(SetAttr::new_min_max_size(1, 2), Domain::bool());

587

1

    let state = <SetPacked as ReprRule>::DomainLevel::init(domain).unwrap();

588

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Bool(true)]));

589

590

1

    let assignment = state.down(value.clone()).unwrap();

591

1

    assert_eq!(assignment.packed, Literal::Int(2));

592

1

    assert_eq!(assignment.up(), value);

593

1

594

595

#[test]

596

1

fn repetition_mset_round_trips_and_omits_fixed_size_marker() {

597

1

    let domain = Domain::mset(MSetAttr::new(range!(3), range!(0..2)), domain_int!(1..2));

598

1

    let state = <MSetRepetition as ReprRule>::DomainLevel::init(domain).unwrap();

599

1

    let value = Literal::AbstractLiteral(AbstractLiteral::MSet(vec![

600

1

        Literal::Int(2),

601

1

        Literal::Int(1),

602

1

        Literal::Int(2),

603

1

    ]));

604

605

1

    let assignment = state.down(value).unwrap();

606

1

    assert!(assignment.mset_size.is_none());

607

1

    assert_eq!(

608

1

        assignment.up(),

609

1

        Literal::AbstractLiteral(AbstractLiteral::MSet(vec![

610

1

            Literal::Int(1),

611

1

            Literal::Int(2),

612

1

            Literal::Int(2),

613

1

]))

614

);

615

1

616

617

#[test]

618

1

fn counts_mset_round_trips_distinct_values_and_multiplicities() {

619

1

    let domain = Domain::mset(MSetAttr::new(range!(0..4), range!(0..3)), domain_int!(0..2));

620

1

    let state = <MSetCounts as ReprRule>::DomainLevel::init(domain).unwrap();

621

1

    let value = Literal::AbstractLiteral(AbstractLiteral::MSet(vec![

622

1

        Literal::Int(1),

623

1

        Literal::Int(1),

624

1

        Literal::Int(2),

625

1

    ]));

626

627

1

    let assignment = state.down(value.clone()).unwrap();

628

1

    assert_eq!(

629

1

        assignment.values_matrix,

630

1

        Literal::from(into_matrix!(vec![

631

1

            Literal::Int(1),

632

1

            Literal::Int(2),

633

1

            Literal::Int(0)

634

1

]))

635

);

636

1

    assert_eq!(

637

1

        assignment.counts_matrix,

638

1

        Literal::from(into_matrix!(vec![

639

1

            Literal::Int(2),

640

1

            Literal::Int(1),

641

1

            Literal::Int(0)

642

1

]))

643

);

644

1

    assert_eq!(assignment.up(), value);

645

1

646

647

#[test]

648

1

fn mset_min_occurrence_only_constrains_values_that_are_present() {

649

1

    let domain = Domain::mset(MSetAttr::new(range!(0..6), range!(2..3)), domain_int!(1..2));

650

1

    let valid = Literal::AbstractLiteral(AbstractLiteral::MSet(vec![

651

1

        Literal::Int(1),

652

1

        Literal::Int(1),

653

1

    ]));

654

1

    let invalid = Literal::AbstractLiteral(AbstractLiteral::MSet(vec![Literal::Int(1)]));

655

656

1

    let repetition = <MSetRepetition as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

657

1

    let counts = <MSetCounts as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

658

1

    let occurrence = <MSetOccurrence as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

659

1

    let packed = <MSetPacked as ReprRule>::DomainLevel::init(domain).unwrap();

660

661

1

    assert_eq!(repetition.down(valid.clone()).unwrap().up(), valid);

662

1

    assert!(repetition.down(invalid.clone()).is_err());

663

1

    assert_eq!(counts.down(valid.clone()).unwrap().up(), valid);

664

1

    assert!(counts.down(invalid.clone()).is_err());

665

1

    assert_eq!(occurrence.down(valid.clone()).unwrap().up(), valid);

666

1

    assert!(occurrence.down(invalid.clone()).is_err());

667

1

    assert_eq!(packed.down(valid.clone()).unwrap().up(), valid);

668

1

    assert!(packed.down(invalid).is_err());

669

1

670

671

#[test]

672

1

fn occurrence_mset_supports_non_integer_elements() {

673

1

    let domain = Domain::mset(

674

1

        MSetAttr::new(range!(0..3), range!(0..2)),

675

1

        Domain::tuple(vec![Domain::bool(), domain_int!(1..2)]),

676

1

);

677

1

    let state = <MSetOccurrence as ReprRule>::DomainLevel::init(domain).unwrap();

678

1

    let element = Literal::AbstractLiteral(AbstractLiteral::Tuple(vec![

679

1

        Literal::Bool(true),

680

1

        Literal::Int(2),

681

1

    ]));

682

1

    let value = Literal::AbstractLiteral(AbstractLiteral::MSet(vec![element.clone(), element]));

683

684

1

    assert_eq!(state.down(value.clone()).unwrap().up(), value);

685

1

    assert!(

686

1

        state

687

1

            .occurs

688

1

            .iter()

689

4

            .all(|(key, _)| matches!(key, Literal::AbstractLiteral(AbstractLiteral::Tuple(_))))

690

);

691

1

692

693

#[test]

694

1

fn packed_mset_round_trips_mixed_radix_counts() {

695

1

    let domain = Domain::mset(MSetAttr::new(range!(1..4), range!(0..2)), Domain::bool());

696

1

    let state = <MSetPacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

697

1

    let value = Literal::AbstractLiteral(AbstractLiteral::MSet(vec![

698

1

        Literal::Bool(false),

699

1

        Literal::Bool(true),

700

1

        Literal::Bool(true),

701

1

    ]));

702

703

1

    let assignment = state.down(value.clone()).unwrap();

704

1

    assert_eq!(assignment.packed, Literal::Int(7));

705

1

    assert_eq!(assignment.up(), value);

706

1

    assert_eq!(MSetPacked::compactness_score(domain).unwrap(), 8);

707

1

708

709

8

fn sequence_attr(size: conjure_cp::ast::Range<i32>) -> SequenceAttr {

710

8

    SequenceAttr {

711

8

        size,

712

8

        jectivity: conjure_cp::ast::JectivityAttr::None,

713

8

        representation: None,

714

8

715

8

716

717

#[test]

718

1

fn explicit_sequence_round_trips_fixed_length() {

719

1

    let domain = Domain::sequence(sequence_attr(range!(2)), domain_int!(1..3));

720

1

    let state = <SequenceExplicit as ReprRule>::DomainLevel::init(domain).unwrap();

721

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Sequence(vec![

722

1

        Literal::Int(3),

723

1

        Literal::Int(1),

724

1

    ]));

725

726

1

    let assignment = state.down(value.clone()).unwrap();

727

1

    assert!(assignment.length.is_none());

728

1

    assert_eq!(assignment.up(), value);

729

1

730

731

#[test]

732

1

fn explicit_sequence_pads_variable_length_with_the_first_domain_value() {

733

1

    let domain = Domain::sequence(sequence_attr(range!(0..3)), domain_int!(1..3));

734

1

    let state = <SequenceExplicit as ReprRule>::DomainLevel::init(domain).unwrap();

735

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Sequence(vec![Literal::Int(2)]));

736

737

1

    let assignment = state.down(value.clone()).unwrap();

738

1

    assert_eq!(assignment.length, Some(Literal::Int(1)));

739

1

    let Literal::AbstractLiteral(AbstractLiteral::Matrix(elems, _)) = &assignment.values_matrix

740

    else {

741

        panic!("expected a matrix");

742

};

743

    // Order is preserved; inactive positions are padded with the domain's first value (not

744

    // sorted, unlike a set's canonical symmetry-breaking padding).

745

1

    assert_eq!(

746

1

        elems,

747

1

        &vec![Literal::Int(2), Literal::Int(1), Literal::Int(1)]

748

);

749

1

    assert_eq!(assignment.up(), value);

750

1

751

752

#[test]

753

1

fn packed_sequence_round_trips_and_preserves_order() {

754

1

    let domain = Domain::sequence(sequence_attr(range!(0..2)), domain_int!(1..3));

755

1

    let state = <SequencePacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

756

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Sequence(vec![

757

1

        Literal::Int(3),

758

1

        Literal::Int(1),

759

1

    ]));

760

761

1

    let assignment = state.down(value.clone()).unwrap();

762

1

    let packed = assignment.packed.clone();

763

1

    assert_eq!(assignment.up(), value);

764

765

    // A different order must encode to a different packed value.

766

1

    let reversed = Literal::AbstractLiteral(AbstractLiteral::Sequence(vec![

767

1

        Literal::Int(1),

768

1

        Literal::Int(3),

769

1

    ]));

770

1

    let reversed_assignment = state.down(reversed.clone()).unwrap();

771

1

    assert_ne!(packed, reversed_assignment.packed);

772

1

    assert_eq!(reversed_assignment.up(), reversed);

773

774

    // length digit (0..=2, radix 3) * two value digits (int(1..3), radix 3 each)

775

1

    assert_eq!(

776

1

        SequencePacked::compactness_score(domain).unwrap(),

777

1

        3 * 3 * 3

778

);

779

1

780

781

#[test]

782

1

fn packed_sequence_supports_a_fixed_length_with_no_length_digit() {

783

1

    let domain = Domain::sequence(sequence_attr(range!(2)), Domain::bool());

784

1

    let state = <SequencePacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

785

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Sequence(vec![

786

1

        Literal::Bool(false),

787

1

        Literal::Bool(true),

788

1

    ]));

789

790

1

    let assignment = state.down(value.clone()).unwrap();

791

1

    assert_eq!(assignment.up(), value);

792

1

    assert_eq!(SequencePacked::compactness_score(domain).unwrap(), 4);

793

1

794

795

#[test]

796

1

fn explicit_sequence_rejects_unbounded_size() {

797

1

    let domain = Domain::sequence(

798

1

        sequence_attr(conjure_cp::ast::Range::Unbounded),

799

1

        domain_int!(1..3),

800

1

);

801

1

    assert!(<SequenceExplicit as ReprRule>::DomainLevel::init(domain).is_err());

802

1

803

804

#[test]

805

1

fn relation_as_set_round_trips_binary_pairs() {

806

1

    let domain = Domain::relation(

807

1

        RelAttr {

808

1

            representation: None,

809

1

            size: range!(2),

810

1

            binary: vec![],

811

1

},

812

1

        vec![domain_int!(1..3), domain_int!(4..6)],

813

1

);

814

1

    let state = <RelationAsSet as ReprRule>::DomainLevel::init(domain).unwrap();

815

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Relation(vec![

816

1

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

817

1

        vec![Literal::Int(2), Literal::Int(5)],

818

1

    ]));

819

820

1

    let assignment = state.down(value.clone()).unwrap();

821

1

    assert_eq!(assignment.up(), value);

822

1

823

824

#[test]

825

1

fn relation_as_set_round_trips_ternary_relations() {

826

    // Arity is no longer restricted to binary; only binary *attributes* (reflexive/symmetric/

827

    // etc) require exactly two columns, checked separately below.

828

1

    let domain = Domain::relation(

829

1

        RelAttr {

830

1

            representation: None,

831

1

            size: range!(1),

832

1

            binary: vec![],

833

1

},

834

1

        vec![domain_int!(1..3), domain_int!(1..3), domain_int!(1..3)],

835

1

);

836

1

    let state = <RelationAsSet as ReprRule>::DomainLevel::init(domain).unwrap();

837

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Relation(vec![vec![

838

1

        Literal::Int(1),

839

1

        Literal::Int(2),

840

1

        Literal::Int(3),

841

1

    ]]));

842

843

1

    let assignment = state.down(value.clone()).unwrap();

844

1

    assert_eq!(assignment.up(), value);

845

1

846

847

#[test]

848

1

fn relation_as_set_rejects_binary_attributes_on_a_ternary_relation() {

849

1

    let domain = Domain::relation(

850

1

        RelAttr {

851

1

            representation: None,

852

1

            size: range!(1),

853

1

            binary: vec![BinaryAttr::Reflexive],

854

1

},

855

1

        vec![domain_int!(1..3), domain_int!(1..3), domain_int!(1..3)],

856

1

);

857

1

    assert!(<RelationAsSet as ReprRule>::DomainLevel::init(domain).is_err());

858

1

859

860

#[test]

861

1

fn relation_as_set_rejects_binary_attributes_when_columns_differ() {

862

1

    let domain = Domain::relation(

863

1

        RelAttr {

864

1

            representation: None,

865

1

            size: range!(1),

866

1

            binary: vec![BinaryAttr::Reflexive],

867

1

},

868

1

        vec![domain_int!(1..3), domain_int!(4..6)],

869

1

);

870

1

    assert!(<RelationAsSet as ReprRule>::DomainLevel::init(domain).is_err());

871

1

872

873

#[test]

874

1

fn relation_as_set_reflexive_builds_one_structural_constraint() {

875

1

    let domain = Domain::relation(

876

1

        RelAttr {

877

1

            representation: None,

878

1

            size: range!(3),

879

1

            binary: vec![BinaryAttr::Reflexive],

880

1

},

881

1

        vec![domain_int!(1..3), domain_int!(1..3)],

882

1

);

883

1

    let mut symbols = SymbolTable::new();

884

1

    let mut declaration = symbols.gen_find(&domain);

885

1

    let (_, constraints) = RelationAsSet::init_for(&mut declaration).unwrap();

886

1

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

887

1

888

889

6

fn binary_attr_constraint_count(binary: Vec<BinaryAttr>) -> usize {

890

6

    let domain = Domain::relation(

891

6

        RelAttr {

892

6

            representation: None,

893

6

            size: range!(3),

894

6

            binary,

895

6

},

896

6

        vec![domain_int!(1..3), domain_int!(1..3)],

897

6

);

898

6

    let mut symbols = SymbolTable::new();

899

6

    let mut declaration = symbols.gen_find(&domain);

900

6

    let (_, constraints) = RelationAsSet::init_for(&mut declaration).unwrap();

901

6

    constraints.len()

902

6

903

904

#[test]

905

1

fn relation_left_total_and_right_total_each_build_one_structural_constraint() {

906

1

    assert_eq!(binary_attr_constraint_count(vec![BinaryAttr::LeftTotal]), 1);

907

1

    assert_eq!(

908

1

        binary_attr_constraint_count(vec![BinaryAttr::RightTotal]),

909

1

910

);

911

1

912

913

#[test]

914

1

fn relation_derived_binary_attrs_expand_to_their_base_formula_count() {

915

    // LinearOrder = Total + AntiSymmetric + Transitive

916

1

    assert_eq!(

917

1

        binary_attr_constraint_count(vec![BinaryAttr::LinearOrder]),

918

1

919

);

920

    // WeakOrder = Total + Transitive

921

1

    assert_eq!(binary_attr_constraint_count(vec![BinaryAttr::WeakOrder]), 2);

922

    // PreOrder = Reflexive + Transitive

923

1

    assert_eq!(binary_attr_constraint_count(vec![BinaryAttr::PreOrder]), 2);

924

    // StrictPartialOrder = Irreflexive + ASymmetric + Transitive

925

1

    assert_eq!(

926

1

        binary_attr_constraint_count(vec![BinaryAttr::StrictPartialOrder]),

927

1

928

);

929

1

930

931

#[test]

932

1

fn relation_occurrence_round_trips_binary_pairs() {

933

1

    let domain = Domain::relation(

934

1

        RelAttr {

935

1

            representation: None,

936

1

            size: range!(2),

937

1

            binary: vec![],

938

1

},

939

1

        vec![domain_int!(1..3), domain_int!(1..2)],

940

1

);

941

1

    let state = <RelationOccurrence as ReprRule>::DomainLevel::init(domain).unwrap();

942

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Relation(vec![

943

1

        vec![Literal::Int(1), Literal::Int(1)],

944

1

        vec![Literal::Int(2), Literal::Int(2)],

945

1

    ]));

946

947

1

    let assignment = state.down(value.clone()).unwrap();

948

1

    assert_eq!(assignment.up(), value);

949

1

950

951

#[test]

952

1

fn relation_occurrence_round_trips_ternary_relations() {

953

1

    let domain = Domain::relation(

954

1

        RelAttr {

955

1

            representation: None,

956

1

            size: range!(1),

957

1

            binary: vec![],

958

1

},

959

1

        vec![domain_int!(1..2), domain_int!(1..2), Domain::bool()],

960

1

);

961

1

    let state = <RelationOccurrence as ReprRule>::DomainLevel::init(domain).unwrap();

962

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Relation(vec![vec![

963

1

        Literal::Int(2),

964

1

        Literal::Int(1),

965

1

        Literal::Bool(true),

966

1

    ]]));

967

968

1

    let assignment = state.down(value.clone()).unwrap();

969

1

    assert_eq!(assignment.up(), value);

970

1

971

972

#[test]

973

1

fn relation_occurrence_rejects_a_compound_column() {

974

    // A set-typed column can't index a matrix; only `RelationAsSet` supports it.

975

1

    let domain = Domain::relation(

976

1

        RelAttr {

977

1

            representation: None,

978

1

            size: range!(1),

979

1

            binary: vec![],

980

1

},

981

1

        vec![

982

1

            domain_int!(1..2),

983

1

            Domain::set(SetAttr::new(range!(2)), domain_int!(1..3)),

984

1

],

985

1

);

986

1

    assert!(<RelationOccurrence as ReprRule>::DomainLevel::init(domain).is_err());

987

1

988

989

#[test]

990

1

fn relation_occurrence_reflexive_and_symmetric_build_two_structural_constraints_plus_cardinality() {

991

1

    let domain = Domain::relation(

992

1

        RelAttr {

993

1

            representation: None,

994

1

            size: conjure_cp::ast::Range::<i32>::Unbounded,

995

1

            binary: vec![BinaryAttr::Reflexive, BinaryAttr::Symmetric],

996

1

},

997

1

        vec![domain_int!(1..3), domain_int!(1..3)],

998

1

);

999

1

    let mut symbols = SymbolTable::new();

1000

1

    let mut declaration = symbols.gen_find(&domain);

1001

1

    let (_, constraints) = RelationOccurrence::init_for(&mut declaration).unwrap();

1002

    // One cardinality range constraint (size is unbounded, so min != max) plus one formula per

1003

    // binary attribute.

1004

1

    assert_eq!(constraints.len(), 3);

1005

1

1006

1007

#[test]

1008

1

fn relation_occurrence_fixed_size_builds_an_equality_cardinality_constraint() {

1009

1

    let domain = Domain::relation(

1010

1

        RelAttr {

1011

1

            representation: None,

1012

1

            size: range!(2),

1013

1

            binary: vec![],

1014

1

},

1015

1

        vec![domain_int!(1..3), domain_int!(1..2)],

1016

1

);

1017

1

    let mut symbols = SymbolTable::new();

1018

1

    let mut declaration = symbols.gen_find(&domain);

1019

1

    let (_, constraints) = RelationOccurrence::init_for(&mut declaration).unwrap();

1020

1

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

1021

1

1022

1023

#[test]

1024

1

fn relation_packed_round_trips_binary_pairs() {

1025

1

    let domain = Domain::relation(

1026

1

        RelAttr {

1027

1

            representation: None,

1028

1

            size: range!(2),

1029

1

            binary: vec![],

1030

1

},

1031

1

        vec![domain_int!(1..3), domain_int!(1..2)],

1032

1

);

1033

1

    let state = <RelationPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1034

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Relation(vec![

1035

1

        vec![Literal::Int(1), Literal::Int(1)],

1036

1

        vec![Literal::Int(2), Literal::Int(2)],

1037

1

    ]));

1038

1039

1

    let assignment = state.down(value.clone()).unwrap();

1040

1

    assert_eq!(assignment.up(), value);

1041

1

1042

1043

#[test]

1044

1

fn relation_packed_round_trips_a_set_typed_column() {

1045

    // More general than RelationOccurrence: any enumerable column works, not just

1046

    // matrix-indexable ones, as long as the combined cartesian product stays small.

1047

1

    let domain = Domain::relation(

1048

1

        RelAttr {

1049

1

            representation: None,

1050

1

            size: range!(2),

1051

1

            binary: vec![],

1052

1

},

1053

1

        vec![

1054

1

            domain_int!(1..2),

1055

1

            Domain::set(SetAttr::new(range!(2)), domain_int!(1..3)),

1056

1

],

1057

1

);

1058

1

    let state = <RelationPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1059

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Relation(vec![

1060

1

        vec![

1061

1

            Literal::Int(1),

1062

1

            Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(1), Literal::Int(2)])),

1063

1

],

1064

1

        vec![

1065

1

            Literal::Int(1),

1066

1

            Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(1), Literal::Int(3)])),

1067

1

],

1068

1

    ]));

1069

1070

1

    let assignment = state.down(value.clone()).unwrap();

1071

1

    assert_eq!(assignment.up(), value);

1072

1

1073

1074

#[test]

1075

1

fn relation_packed_rejects_a_too_large_cartesian_product() {

1076

    // 6 columns of int(1..3) is 3^6 = 729 possible tuples, far over the 30-bit cap.

1077

1

    let domain = Domain::relation(

1078

1

        RelAttr {

1079

1

            representation: None,

1080

1

            size: range!(2),

1081

1

            binary: vec![],

1082

1

},

1083

1

        vec![domain_int!(1..3); 6],

1084

1

);

1085

1

    assert!(<RelationPacked as ReprRule>::DomainLevel::init(domain).is_err());

1086

1

1087

1088

#[test]

1089

1

fn relation_packed_reflexive_builds_a_cardinality_and_a_structural_constraint() {

1090

    // Unlike RelationAsSet (which delegates cardinality entirely to set_decl's own eventual

1091

    // representation), RelationPacked always emits its own cardinality constraint directly, so a

1092

    // fixed size plus one binary attribute gives two constraints, not one.

1093

1

    let domain = Domain::relation(

1094

1

        RelAttr {

1095

1

            representation: None,

1096

1

            size: range!(3),

1097

1

            binary: vec![BinaryAttr::Reflexive],

1098

1

},

1099

1

        vec![domain_int!(1..3), domain_int!(1..3)],

1100

1

);

1101

1

    let mut symbols = SymbolTable::new();

1102

1

    let mut declaration = symbols.gen_find(&domain);

1103

1

    let (_, constraints) = RelationPacked::init_for(&mut declaration).unwrap();

1104

1

    assert_eq!(constraints.len(), 2);

1105

1

1106

1107

#[test]

1108

1

fn relation_packed_is_more_compact_than_occurrence_for_a_bounded_size() {

1109

    // Both represent every possible relation value, so for an *unbounded* size their compactness

1110

    // is mathematically identical (sum_k C(n,k) == 2^n); packed only wins once the size is

1111

    // bounded narrowly enough for the binomial sum to undercut 2^n.

1112

1

    let domain = Domain::relation(

1113

1

        RelAttr {

1114

1

            representation: None,

1115

1

            size: range!(2),

1116

1

            binary: vec![],

1117

1

},

1118

1

        vec![domain_int!(1..3), domain_int!(1..3)],

1119

1

);

1120

1

    assert!(

1121

1

        RelationPacked::compactness_score(domain.clone()).unwrap()

1122

1

            < RelationOccurrence::compactness_score(domain).unwrap()

1123

);

1124

1

1125

1126

14

fn func_attr(

1127

14

    size: conjure_cp::ast::Range<i32>,

1128

14

    partiality: PartialityAttr,

1129

14

    jectivity: JectivityAttr,

1130

14

) -> FuncAttr {

1131

14

    FuncAttr {

1132

14

        representation: None,

1133

14

        size,

1134

14

        partiality,

1135

14

        jectivity,

1136

14

1137

14

1138

1139

#[test]

1140

1

fn function_as_relation_round_trips_pairs() {

1141

1

    let domain = Domain::function(

1142

1

        func_attr(range!(0..2), PartialityAttr::Partial, JectivityAttr::None),

1143

1

        domain_int!(1..5),

1144

1

        Domain::bool(),

1145

1

);

1146

1

    let state = <FunctionAsRelation as ReprRule>::DomainLevel::init(domain).unwrap();

1147

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Function(vec![

1148

1

        (Literal::Int(2), Literal::Bool(true)),

1149

1

        (Literal::Int(4), Literal::Bool(false)),

1150

1

    ]));

1151

1152

1

    let assignment = state.down(value.clone()).unwrap();

1153

1

    assert_eq!(assignment.up(), value);

1154

1

1155

1156

#[test]

1157

1

fn function_as_relation_total_function_builds_only_the_well_formedness_constraint() {

1158

1

    let domain = Domain::function(

1159

1

        func_attr(

1160

1

            conjure_cp::ast::Range::Unbounded,

1161

1

            PartialityAttr::Total,

1162

1

            JectivityAttr::None,

1163

1

),

1164

1

        domain_int!(1..3),

1165

1

        Domain::bool(),

1166

1

);

1167

1

    let mut symbols = SymbolTable::new();

1168

1

    let mut declaration = symbols.gen_find(&domain);

1169

1

    let (_, constraints) = FunctionAsRelation::init_for(&mut declaration).unwrap();

1170

    // Well-formedness, and nothing else: totality follows from it together with the relation's

1171

    // fixed size, and `image` reads the relation directly rather than a forward lookup table.

1172

1

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

1173

1

1174

1175

#[test]

1176

1

fn function_as_relation_bijective_adds_injective_and_surjective_constraints() {

1177

1

    let domain = Domain::function(

1178

1

        func_attr(range!(3), PartialityAttr::Total, JectivityAttr::Bijective),

1179

1

        domain_int!(1..3),

1180

1

        domain_int!(1..3),

1181

1

);

1182

1

    let mut symbols = SymbolTable::new();

1183

1

    let mut declaration = symbols.gen_find(&domain);

1184

1

    let (_, constraints) = FunctionAsRelation::init_for(&mut declaration).unwrap();

1185

    // well-formedness + injective (pairwise) + one surjectivity witness pair (In + Eq) per

1186

    // codomain value.

1187

1

    assert_eq!(constraints.len(), 1 + 1 + 2 * 3);

1188

1

1189

1190

#[test]

1191

1

fn explicit_function_round_trips_total_function() {

1192

1

    let domain = Domain::function(

1193

1

        func_attr(range!(3), PartialityAttr::Total, JectivityAttr::None),

1194

1

        domain_int!(1..3),

1195

1

        Domain::bool(),

1196

1

);

1197

1

    let state = <FunctionExplicit as ReprRule>::DomainLevel::init(domain).unwrap();

1198

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Function(vec![

1199

1

        (Literal::Int(1), Literal::Bool(true)),

1200

1

        (Literal::Int(2), Literal::Bool(false)),

1201

1

        (Literal::Int(3), Literal::Bool(true)),

1202

1

    ]));

1203

1204

1

    let assignment = state.down(value.clone()).unwrap();

1205

1

    assert_eq!(assignment.up(), value);

1206

1

1207

1208

#[test]

1209

1

fn explicit_function_round_trips_partial_function_and_pads_undefined_positions() {

1210

1

    let domain = Domain::function(

1211

1

        func_attr(range!(0..2), PartialityAttr::Partial, JectivityAttr::None),

1212

1

        domain_int!(1..3),

1213

1

        domain_int!(10..12),

1214

1

);

1215

1

    let state = <FunctionExplicit as ReprRule>::DomainLevel::init(domain).unwrap();

1216

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Function(vec![(

1217

1

        Literal::Int(2),

1218

1

        Literal::Int(11),

1219

1

    )]));

1220

1221

1

    let assignment = state.down(value.clone()).unwrap();

1222

1

    assert_eq!(assignment.up(), value);

1223

1

1224

1225

#[test]

1226

1

fn explicit_function_total_bijective_builds_alldiff_and_surjective_constraints() {

1227

1

    let domain = Domain::function(

1228

1

        func_attr(range!(3), PartialityAttr::Total, JectivityAttr::Bijective),

1229

1

        domain_int!(1..3),

1230

1

        domain_int!(1..3),

1231

1

);

1232

1

    let mut symbols = SymbolTable::new();

1233

1

    let mut declaration = symbols.gen_find(&domain);

1234

1

    let (_, constraints) = FunctionExplicit::init_for(&mut declaration).unwrap();

1235

    // one allDiff (injective, total) + one surjective "or" per codomain value.

1236

1

    assert_eq!(constraints.len(), 1 + 3);

1237

1

1238

1239

#[test]

1240

1

fn explicit_function_partial_injective_builds_guarded_pairwise_constraints() {

1241

1

    let domain = Domain::function(

1242

1

        func_attr(

1243

1

            range!(0..3),

1244

1

            PartialityAttr::Partial,

1245

1

            JectivityAttr::Injective,

1246

1

),

1247

1

        domain_int!(1..3),

1248

1

        domain_int!(1..3),

1249

1

);

1250

1

    let mut symbols = SymbolTable::new();

1251

1

    let mut declaration = symbols.gen_find(&domain);

1252

1

    let (_, constraints) = FunctionExplicit::init_for(&mut declaration).unwrap();

1253

    // one cardinality bound (maxSize 3 is not Unbounded) + one canonical-padding constraint per

1254

    // domain position + guarded pairwise over 3 domain positions: C(3,2) = 3 constraints.

1255

1

    assert_eq!(constraints.len(), 1 + 3 + 3);

1256

1

1257

1258

#[test]

1259

1

fn compactness_prefers_function_as_relation_for_a_sparse_partial_function() {

1260

    // A large domain (100 values) with at most 2 entries: the relation only needs to size

1261

    // itself for those 2 entries, while the explicit matrix needs one atom per domain value.

1262

1

    let domain = Domain::function(

1263

1

        func_attr(range!(0..2), PartialityAttr::Partial, JectivityAttr::None),

1264

1

        domain_int!(1..100),

1265

1

        Domain::bool(),

1266

1

);

1267

1

    assert!(

1268

1

        FunctionAsRelation::compactness_score(domain.clone()).unwrap()

1269

1

            < FunctionExplicit::compactness_score(domain).unwrap()

1270

);

1271

1

1272

1273

#[test]

1274

1

fn compactness_prefers_function_explicit_for_a_total_function() {

1275

    // A small total function: both score similarly (entries == domain size), but explicit

1276

    // avoids the relation's extra tuple-key overhead, so it should not score worse.

1277

1

    let domain = Domain::function(

1278

1

        func_attr(range!(3), PartialityAttr::Total, JectivityAttr::None),

1279

1

        domain_int!(1..3),

1280

1

        Domain::bool(),

1281

1

);

1282

1

    assert!(

1283

1

        FunctionExplicit::compactness_score(domain.clone()).unwrap()

1284

1

            <= FunctionAsRelation::compactness_score(domain).unwrap()

1285

);

1286

1

1287

1288

22

fn partition_attr(

1289

22

    num_parts: conjure_cp::ast::Range<i32>,

1290

22

    part_len: conjure_cp::ast::Range<i32>,

1291

22

    is_regular: bool,

1292

22

) -> PartitionAttr {

1293

22

    PartitionAttr {

1294

22

        representation: None,

1295

22

        num_parts,

1296

22

        part_len,

1297

22

        is_regular,

1298

22

1299

22

1300

1301

#[test]

1302

1

fn partition_as_set_round_trips_values() {

1303

1

    let domain = Domain::partition(

1304

1

        partition_attr(range!(2), range!(3), true),

1305

1

        domain_int!(1..6),

1306

1

);

1307

1

    let state = <PartitionAsSet as ReprRule>::DomainLevel::init(domain).unwrap();

1308

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1309

1

        vec![Literal::Int(1), Literal::Int(2), Literal::Int(3)],

1310

1

        vec![Literal::Int(4), Literal::Int(5), Literal::Int(6)],

1311

1

    ]));

1312

1313

1

    let assignment = state.down(value.clone()).unwrap();

1314

1

    assert_eq!(assignment.up(), value);

1315

1

1316

1317

#[test]

1318

1

fn partition_as_set_round_trips_a_set_typed_inner_domain() {

1319

1

    let inner = Domain::set(SetAttr::new(range!(1)), domain_int!(1..3));

1320

1

    let domain = Domain::partition(partition_attr(range!(1), range!(2), false), inner);

1321

1

    let state = <PartitionAsSet as ReprRule>::DomainLevel::init(domain).unwrap();

1322

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![vec![

1323

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(1)])),

1324

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(2)])),

1325

1

    ]]));

1326

1327

1

    let assignment = state.down(value.clone()).unwrap();

1328

1

    assert_eq!(assignment.up(), value);

1329

1

1330

1331

#[test]

1332

1

fn partition_as_set_rejects_a_non_partition_domain() {

1333

1

    let domain = domain_int!(1..3);

1334

1

    assert!(<PartitionAsSet as ReprRule>::DomainLevel::init(domain).is_err());

1335

1

1336

1337

#[test]

1338

1

fn partition_as_set_non_regular_builds_exactly_once_and_non_empty_constraints() {

1339

1

    let domain = Domain::partition(

1340

1

        partition_attr(range!(2), conjure_cp::ast::Range::Unbounded, false),

1341

1

        domain_int!(1..6),

1342

1

);

1343

1

    let mut symbols = SymbolTable::new();

1344

1

    let mut declaration = symbols.gen_find(&domain);

1345

1

    let (_, constraints) = PartitionAsSet::init_for(&mut declaration).unwrap();

1346

1

    assert_eq!(constraints.len(), 2);

1347

1

1348

1349

#[test]

1350

1

fn partition_as_set_regular_infers_a_fixed_part_size_from_a_fixed_num_parts() {

1351

1

    let domain = Domain::partition(

1352

1

        partition_attr(range!(2), conjure_cp::ast::Range::Unbounded, true),

1353

1

        domain_int!(1..6),

1354

1

);

1355

1

    let mut symbols = SymbolTable::new();

1356

1

    let mut declaration = symbols.gen_find(&domain);

1357

1

    let (_, constraints) = PartitionAsSet::init_for(&mut declaration).unwrap();

1358

1

    assert_eq!(constraints.len(), 2);

1359

1

1360

1361

#[test]

1362

1

fn partition_as_set_regular_infers_a_fixed_num_parts_from_a_fixed_part_size() {

1363

1

    let domain = Domain::partition(

1364

1

        partition_attr(conjure_cp::ast::Range::Unbounded, range!(3), true),

1365

1

        domain_int!(1..6),

1366

1

);

1367

1

    let mut symbols = SymbolTable::new();

1368

1

    let mut declaration = symbols.gen_find(&domain);

1369

1

    let (_, constraints) = PartitionAsSet::init_for(&mut declaration).unwrap();

1370

1

    assert_eq!(constraints.len(), 2);

1371

1

1372

1373

#[test]

1374

1

fn partition_as_set_regular_adds_a_third_constraint_when_part_size_is_not_fixed() {

1375

    // Neither `numParts` nor `partSize` is pinned to a single value here, so the regular ->

1376

    // fixed-size inference (`numParts` or `partSize` singleton + `regular` forces the other)

1377

    // cannot kick in, and the pairwise "all parts equal size" constraint is genuinely needed.

1378

1

    let domain = Domain::partition(

1379

1

        partition_attr(

1380

1

            conjure_cp::ast::Range::Unbounded,

1381

1

            conjure_cp::ast::Range::Unbounded,

1382

1

            true,

1383

1

),

1384

1

        domain_int!(1..6),

1385

1

);

1386

1

    let mut symbols = SymbolTable::new();

1387

1

    let mut declaration = symbols.gen_find(&domain);

1388

1

    let (_, constraints) = PartitionAsSet::init_for(&mut declaration).unwrap();

1389

1

    assert_eq!(constraints.len(), 3);

1390

1

1391

1392

#[test]

1393

1

fn partition_as_set_regular_is_redundant_when_part_size_is_already_fixed() {

1394

    // `regular` is automatically implied once `partSize` fixes an exact size, so stating it

1395

    // again should not add a third structural constraint (mirrors Conjure's own `fixedPartSize`

1396

    // guard in `PartitionAsSet.hs`).

1397

1

    let domain = Domain::partition(

1398

1

        partition_attr(range!(2), range!(3), true),

1399

1

        domain_int!(1..6),

1400

1

);

1401

1

    let mut symbols = SymbolTable::new();

1402

1

    let mut declaration = symbols.gen_find(&domain);

1403

1

    let (_, constraints) = PartitionAsSet::init_for(&mut declaration).unwrap();

1404

1

    assert_eq!(constraints.len(), 2);

1405

1

1406

1407

#[test]

1408

1

fn partition_occurrence_round_trips_values() {

1409

1

    let domain = Domain::partition(

1410

1

        partition_attr(range!(2), range!(3), true),

1411

1

        domain_int!(1..6),

1412

1

);

1413

1

    let state = <PartitionOccurrence as ReprRule>::DomainLevel::init(domain).unwrap();

1414

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1415

1

        vec![Literal::Int(1), Literal::Int(2), Literal::Int(3)],

1416

1

        vec![Literal::Int(4), Literal::Int(5), Literal::Int(6)],

1417

1

    ]));

1418

1419

1

    let assignment = state.down(value.clone()).unwrap();

1420

1

    assert_eq!(assignment.up(), value);

1421

1

1422

1423

#[test]

1424

1

fn partition_occurrence_canonicalises_part_order() {

1425

    // Parts are relabelled in first-occurrence (domain scan) order, regardless of the order the

1426

    // literal itself lists them in -- this must agree with `symmetry_breaking_expr`'s own

1427

    // ordering, or a valid literal could fail the very constraint meant to allow it.

1428

1

    let domain = Domain::partition(

1429

1

        partition_attr(range!(2), range!(3), false),

1430

1

        domain_int!(1..6),

1431

1

);

1432

1

    let state = <PartitionOccurrence as ReprRule>::DomainLevel::init(domain).unwrap();

1433

1

    let given = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1434

1

        vec![Literal::Int(4), Literal::Int(5), Literal::Int(6)],

1435

1

        vec![Literal::Int(1), Literal::Int(2), Literal::Int(3)],

1436

1

    ]));

1437

1

    let canonical = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1438

1

        vec![Literal::Int(1), Literal::Int(2), Literal::Int(3)],

1439

1

        vec![Literal::Int(4), Literal::Int(5), Literal::Int(6)],

1440

1

    ]));

1441

1442

1

    let assignment = state.down(given).unwrap();

1443

1

    assert_eq!(assignment.up(), canonical);

1444

1

1445

1446

#[test]

1447

1

fn partition_occurrence_round_trips_uneven_part_sizes() {

1448

1

    let domain = Domain::partition(

1449

1

        partition_attr(

1450

1

            conjure_cp::ast::Range::Unbounded,

1451

1

            conjure_cp::ast::Range::Unbounded,

1452

1

            false,

1453

1

),

1454

1

        domain_int!(1..5),

1455

1

);

1456

1

    let state = <PartitionOccurrence as ReprRule>::DomainLevel::init(domain).unwrap();

1457

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1458

1

        vec![Literal::Int(1)],

1459

1

        vec![Literal::Int(2), Literal::Int(3), Literal::Int(4)],

1460

1

        vec![Literal::Int(5)],

1461

1

    ]));

1462

1463

1

    let assignment = state.down(value.clone()).unwrap();

1464

1

    assert_eq!(assignment.up(), value);

1465

1

1466

1467

#[test]

1468

1

fn partition_occurrence_rejects_a_non_partition_domain() {

1469

1

    let domain = domain_int!(1..3);

1470

1

    assert!(<PartitionOccurrence as ReprRule>::DomainLevel::init(domain).is_err());

1471

1

1472

1473

#[test]

1474

1

fn partition_occurrence_rejects_a_non_int_inner_domain() {

1475

1

    let inner = Domain::set(SetAttr::new(range!(1)), domain_int!(1..3));

1476

1

    let domain = Domain::partition(partition_attr(range!(1), range!(2), false), inner);

1477

1

    assert!(<PartitionOccurrence as ReprRule>::DomainLevel::init(domain).is_err());

1478

1

1479

1480

#[test]

1481

1

fn partition_occurrence_non_regular_builds_five_structural_constraints() {

1482

1

    let domain = Domain::partition(

1483

1

        partition_attr(range!(2), conjure_cp::ast::Range::Unbounded, false),

1484

1

        domain_int!(1..6),

1485

1

);

1486

1

    let mut symbols = SymbolTable::new();

1487

1

    let mut declaration = symbols.gen_find(&domain);

1488

1

    let (_, constraints) = PartitionOccurrence::init_for(&mut declaration).unwrap();

1489

1

    assert_eq!(constraints.len(), 5);

1490

1

1491

1492

#[test]

1493

1

fn partition_occurrence_regular_adds_a_sixth_constraint_when_part_size_is_not_fixed() {

1494

1

    let domain = Domain::partition(

1495

1

        partition_attr(

1496

1

            conjure_cp::ast::Range::Unbounded,

1497

1

            conjure_cp::ast::Range::Unbounded,

1498

1

            true,

1499

1

),

1500

1

        domain_int!(1..6),

1501

1

);

1502

1

    let mut symbols = SymbolTable::new();

1503

1

    let mut declaration = symbols.gen_find(&domain);

1504

1

    let (_, constraints) = PartitionOccurrence::init_for(&mut declaration).unwrap();

1505

1

    assert_eq!(constraints.len(), 6);

1506

1

1507

1508

#[test]

1509

1

fn partition_occurrence_regular_infers_a_fixed_part_size_from_a_fixed_num_parts() {

1510

1

    let domain = Domain::partition(

1511

1

        partition_attr(range!(2), conjure_cp::ast::Range::Unbounded, true),

1512

1

        domain_int!(1..6),

1513

1

);

1514

1

    let mut symbols = SymbolTable::new();

1515

1

    let mut declaration = symbols.gen_find(&domain);

1516

1

    let (_, constraints) = PartitionOccurrence::init_for(&mut declaration).unwrap();

1517

1

    assert_eq!(constraints.len(), 5);

1518

1

1519

1520

#[test]

1521

1

fn partition_packed_round_trips_values() {

1522

1

    let domain = Domain::partition(

1523

1

        partition_attr(range!(2), range!(3), true),

1524

1

        domain_int!(1..6),

1525

1

);

1526

1

    let state = <PartitionPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1527

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1528

1

        vec![Literal::Int(1), Literal::Int(2), Literal::Int(3)],

1529

1

        vec![Literal::Int(4), Literal::Int(5), Literal::Int(6)],

1530

1

    ]));

1531

1532

1

    let assignment = state.down(value.clone()).unwrap();

1533

1

    assert_eq!(assignment.up(), value);

1534

1

1535

1536

#[test]

1537

1

fn partition_packed_canonicalises_part_order() {

1538

1

    let domain = Domain::partition(

1539

1

        partition_attr(range!(2), range!(3), false),

1540

1

        domain_int!(1..6),

1541

1

);

1542

1

    let state = <PartitionPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1543

1

    let given = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1544

1

        vec![Literal::Int(4), Literal::Int(5), Literal::Int(6)],

1545

1

        vec![Literal::Int(1), Literal::Int(2), Literal::Int(3)],

1546

1

    ]));

1547

1

    let canonical = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1548

1

        vec![Literal::Int(1), Literal::Int(2), Literal::Int(3)],

1549

1

        vec![Literal::Int(4), Literal::Int(5), Literal::Int(6)],

1550

1

    ]));

1551

1552

1

    let assignment = state.down(given).unwrap();

1553

1

    assert_eq!(assignment.up(), canonical);

1554

1

1555

1556

#[test]

1557

1

fn partition_packed_round_trips_uneven_part_sizes() {

1558

1

    let domain = Domain::partition(

1559

1

        partition_attr(

1560

1

            conjure_cp::ast::Range::Unbounded,

1561

1

            conjure_cp::ast::Range::Unbounded,

1562

1

            false,

1563

1

),

1564

1

        domain_int!(1..5),

1565

1

);

1566

1

    let state = <PartitionPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1567

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![

1568

1

        vec![Literal::Int(1)],

1569

1

        vec![Literal::Int(2), Literal::Int(3), Literal::Int(4)],

1570

1

        vec![Literal::Int(5)],

1571

1

    ]));

1572

1573

1

    let assignment = state.down(value.clone()).unwrap();

1574

1

    assert_eq!(assignment.up(), value);

1575

1

1576

1577

#[test]

1578

1

fn partition_packed_round_trips_a_set_typed_inner_domain() {

1579

    // Unlike PartitionOccurrence, packing only needs an enumerable inner domain, not a

1580

    // matrix-indexable one. The inner domain has exactly 2 values ({1} and {2}), so a single

1581

    // size-2 part covers it completely.

1582

1

    let inner = Domain::set(SetAttr::new(range!(1)), domain_int!(1..2));

1583

1

    let domain = Domain::partition(partition_attr(range!(1), range!(2), false), inner);

1584

1

    let state = <PartitionPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1585

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Partition(vec![vec![

1586

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(1)])),

1587

1

        Literal::AbstractLiteral(AbstractLiteral::Set(vec![Literal::Int(2)])),

1588

1

    ]]));

1589

1590

1

    let assignment = state.down(value.clone()).unwrap();

1591

1

    assert_eq!(assignment.up(), value);

1592

1

1593

1594

#[test]

1595

1

fn partition_packed_rejects_a_non_partition_domain() {

1596

1

    let domain = domain_int!(1..3);

1597

1

    assert!(<PartitionPacked as ReprRule>::DomainLevel::init(domain).is_err());

1598

1

1599

1600

#[test]

1601

1

fn partition_packed_non_regular_builds_five_structural_constraints() {

1602

1

    let domain = Domain::partition(

1603

1

        partition_attr(range!(2), conjure_cp::ast::Range::Unbounded, false),

1604

1

        domain_int!(1..6),

1605

1

);

1606

1

    let mut symbols = SymbolTable::new();

1607

1

    let mut declaration = symbols.gen_find(&domain);

1608

1

    let (_, constraints) = PartitionPacked::init_for(&mut declaration).unwrap();

1609

1

    assert_eq!(constraints.len(), 5);

1610

1

1611

1612

#[test]

1613

1

fn partition_packed_regular_adds_a_sixth_constraint_when_part_size_is_not_fixed() {

1614

1

    let domain = Domain::partition(

1615

1

        partition_attr(

1616

1

            conjure_cp::ast::Range::Unbounded,

1617

1

            conjure_cp::ast::Range::Unbounded,

1618

1

            true,

1619

1

),

1620

1

        domain_int!(1..6),

1621

1

);

1622

1

    let mut symbols = SymbolTable::new();

1623

1

    let mut declaration = symbols.gen_find(&domain);

1624

1

    let (_, constraints) = PartitionPacked::init_for(&mut declaration).unwrap();

1625

1

    assert_eq!(constraints.len(), 6);

1626

1

1627

1628

#[test]

1629

1

fn partition_packed_regular_infers_a_fixed_part_size_from_a_fixed_num_parts() {

1630

1

    let domain = Domain::partition(

1631

1

        partition_attr(range!(2), conjure_cp::ast::Range::Unbounded, true),

1632

1

        domain_int!(1..6),

1633

1

);

1634

1

    let mut symbols = SymbolTable::new();

1635

1

    let mut declaration = symbols.gen_find(&domain);

1636

1

    let (_, constraints) = PartitionPacked::init_for(&mut declaration).unwrap();

1637

1

    assert_eq!(constraints.len(), 5);

1638

1

1639

1640

#[test]

1641

1

fn partition_packed_is_more_compact_than_occurrence_for_a_bounded_size() {

1642

    // Both use the same maxNumParts, but PartitionOccurrence's WhichPart lives in its own

1643

    // n-cell matrix domain (compactness counts each cell), while PartitionPacked folds the same

1644

    // n digits into one int -- so packed's domain-size compactness score should never exceed

1645

    // occurrence's for the same partition domain.

1646

1

    let domain = Domain::partition(

1647

1

        partition_attr(range!(2), conjure_cp::ast::Range::Unbounded, false),

1648

1

        domain_int!(1..6),

1649

1

);

1650

1

    assert!(

1651

1

        PartitionPacked::compactness_score(domain.clone()).unwrap()

1652

1

            <= PartitionOccurrence::compactness_score(domain).unwrap()

1653

);

1654

1

1655

1656

6

fn permutation_attr(num_moved: conjure_cp::ast::Range<i32>) -> PermutationAttr {

1657

6

    PermutationAttr {

1658

6

        representation: None,

1659

6

        num_moved,

1660

6

1661

6

1662

1663

#[test]

1664

1

fn permutation_as_function_round_trips_a_single_cycle() {

1665

1

    let domain = Domain::permutation(

1666

1

        permutation_attr(conjure_cp::ast::Range::Unbounded),

1667

1

        domain_int!(1..5),

1668

1

);

1669

1

    let state = <PermutationAsFunction as ReprRule>::DomainLevel::init(domain).unwrap();

1670

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Permutation(vec![vec![

1671

1

        Literal::Int(1),

1672

1

        Literal::Int(3),

1673

1

        Literal::Int(5),

1674

1

    ]]));

1675

1676

1

    let assignment = state.down(value.clone()).unwrap();

1677

1

    assert_eq!(assignment.up(), value);

1678

1

1679

1680

#[test]

1681

1

fn permutation_as_function_round_trips_multiple_disjoint_cycles() {

1682

1

    let domain = Domain::permutation(

1683

1

        permutation_attr(conjure_cp::ast::Range::Unbounded),

1684

1

        domain_int!(1..6),

1685

1

);

1686

1

    let state = <PermutationAsFunction as ReprRule>::DomainLevel::init(domain).unwrap();

1687

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Permutation(vec![

1688

1

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

1689

1

        vec![Literal::Int(3), Literal::Int(4), Literal::Int(5)],

1690

1

    ]));

1691

1692

1

    let assignment = state.down(value.clone()).unwrap();

1693

1

    assert_eq!(assignment.up(), value);

1694

1

1695

1696

#[test]

1697

1

fn permutation_as_function_round_trips_the_identity() {

1698

    // Every element is an (implicit) fixed point: the literal has no cycles at all.

1699

1

    let domain = Domain::permutation(

1700

1

        permutation_attr(conjure_cp::ast::Range::Unbounded),

1701

1

        domain_int!(1..4),

1702

1

);

1703

1

    let state = <PermutationAsFunction as ReprRule>::DomainLevel::init(domain).unwrap();

1704

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Permutation(vec![]));

1705

1706

1

    let assignment = state.down(value.clone()).unwrap();

1707

1

    assert_eq!(assignment.up(), value);

1708

1

1709

1710

#[test]

1711

1

fn permutation_as_function_rejects_a_cycle_element_outside_its_domain() {

1712

1

    let domain = Domain::permutation(

1713

1

        permutation_attr(conjure_cp::ast::Range::Unbounded),

1714

1

        domain_int!(1..3),

1715

1

);

1716

1

    let state = <PermutationAsFunction as ReprRule>::DomainLevel::init(domain).unwrap();

1717

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Permutation(vec![vec![

1718

1

        Literal::Int(1),

1719

1

        Literal::Int(99),

1720

1

    ]]));

1721

1722

1

    assert!(state.down(value).is_err());

1723

1

1724

1725

#[test]

1726

1

fn permutation_as_function_rejects_an_element_appearing_in_two_cycles() {

1727

1

    let domain = Domain::permutation(

1728

1

        permutation_attr(conjure_cp::ast::Range::Unbounded),

1729

1

        domain_int!(1..4),

1730

1

);

1731

1

    let state = <PermutationAsFunction as ReprRule>::DomainLevel::init(domain).unwrap();

1732

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Permutation(vec![

1733

1

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

1734

1

        vec![Literal::Int(2), Literal::Int(3)],

1735

1

    ]));

1736

1737

1

    assert!(state.down(value).is_err());

1738

1

1739

1740

#[test]

1741

1

fn permutation_as_function_rejects_a_non_permutation_domain() {

1742

1

    let domain = domain_int!(1..3);

1743

1

    assert!(<PermutationAsFunction as ReprRule>::DomainLevel::init(domain).is_err());

1744

1

1745

1746

#[test]

1747

1

fn permutation_as_function_builds_three_structural_constraints() {

1748

    // numMoved's range check, plus the two round-trip constraints (backwards . forwards = id and

1749

    // forwards . backwards = id). Nested constraints from whatever representation gets chosen for

1750

    // the forwards/backwards Function-typed aux declarations themselves are added by a later pass

1751

    // over those new declarations, not eagerly folded into this count.

1752

1

    let domain = Domain::permutation(

1753

1

        permutation_attr(conjure_cp::ast::Range::Unbounded),

1754

1

        domain_int!(1..4),

1755

1

);

1756

1

    let mut symbols = SymbolTable::new();

1757

1

    let mut declaration = symbols.gen_find(&domain);

1758

1

    let (_, constraints) = PermutationAsFunction::init_for(&mut declaration).unwrap();

1759

1

    assert_eq!(constraints.len(), 3);

1760

1

1761

1762

#[test]

1763

1

fn packed_function_round_trips_a_total_function() {

1764

1

    let domain = Domain::function(

1765

1

        func_attr(range!(3), PartialityAttr::Total, JectivityAttr::None),

1766

1

        domain_int!(1..3),

1767

1

        domain_int!(7..8),

1768

1

);

1769

1

    let state = <FunctionPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1770

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Function(vec![

1771

1

        (Literal::Int(1), Literal::Int(8)),

1772

1

        (Literal::Int(2), Literal::Int(7)),

1773

1

        (Literal::Int(3), Literal::Int(8)),

1774

1

    ]));

1775

1

    let down = state.down(value.clone()).unwrap();

1776

1

    assert!(matches!(down.packed, Literal::Int(_)));

1777

1

    assert_eq!(down.up(), value);

1778

1

1779

1780

/// A partial function's digits carry definedness themselves: digit 0 means "defines nothing here",

1781

/// so the domain has exactly `(codomain + 1) ** |domain|` values and an undefined key round-trips

1782

/// by being absent rather than by holding some padding value.

1783

#[test]

1784

1

fn packed_function_round_trips_a_partial_function() {

1785

1

    let domain = Domain::function(

1786

1

        func_attr(

1787

1

            conjure_cp::ast::Range::Unbounded,

1788

1

            PartialityAttr::Partial,

1789

1

            JectivityAttr::None,

1790

1

),

1791

1

        domain_int!(1..3),

1792

1

        domain_int!(7..8),

1793

1

);

1794

1

    let state = <FunctionPacked as ReprRule>::DomainLevel::init(domain.clone()).unwrap();

1795

1

    assert_eq!(FunctionPacked::compactness_score(domain).unwrap(), 27);

1796

1797

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Function(vec![

1798

1

        (Literal::Int(1), Literal::Int(8)),

1799

1

        (Literal::Int(3), Literal::Int(7)),

1800

1

    ]));

1801

1

    let down = state.down(value.clone()).unwrap();

1802

1

    assert_eq!(down.up(), value);

1803

1

1804

1805

#[test]

1806

1

fn packed_function_rejects_a_total_function_missing_a_key() {

1807

1

    let domain = Domain::function(

1808

1

        func_attr(range!(3), PartialityAttr::Total, JectivityAttr::None),

1809

1

        domain_int!(1..3),

1810

1

        domain_int!(7..8),

1811

1

);

1812

1

    let state = <FunctionPacked as ReprRule>::DomainLevel::init(domain).unwrap();

1813

1

    let value = Literal::AbstractLiteral(AbstractLiteral::Function(vec![(

1814

1

        Literal::Int(1),

1815

1

        Literal::Int(8),

1816

1

    )]));

1817

1

    assert!(state.down(value).is_err());

1818

1

1819

1820

#[test]

1821

1

fn packed_function_partial_builds_a_cardinality_constraint() {

1822

1

    let domain = Domain::function(

1823

1

        func_attr(range!(2), PartialityAttr::Partial, JectivityAttr::None),

1824

1

        domain_int!(1..3),

1825

1

        domain_int!(7..8),

1826

1

);

1827

1

    let mut symbols = SymbolTable::new();

1828

1

    let mut declaration = symbols.gen_find(&domain);

1829

1

    let (_, constraints) = FunctionPacked::init_for(&mut declaration).unwrap();

1830

    // Exactly the `size` constraint: nothing else is structural for a plain partial function.

1831

1

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

1832

1

1833

1834

#[test]

1835

1

fn packed_function_bijective_builds_injective_and_surjective_constraints() {

1836

1

    let domain = Domain::function(

1837

1

        func_attr(range!(2), PartialityAttr::Total, JectivityAttr::Bijective),

1838

1

        domain_int!(1..2),

1839

1

        domain_int!(7..8),

1840

1

);

1841

1

    let mut symbols = SymbolTable::new();

1842

1

    let mut declaration = symbols.gen_find(&domain);

1843

1

    let (_, constraints) = FunctionPacked::init_for(&mut declaration).unwrap();

1844

    // One pairwise distinctness constraint, plus one coverage constraint per codomain value.

1845

1

    assert_eq!(constraints.len(), 1 + 2);

1846

1