Grcov report - representation.rs

1

use crate::guard;

2

use crate::shared::utils::as_cmp_or_lex_op;

3

use crate::types::int::{

4

    IntBinaryOffset, IntBinaryRank, IntBinarySignMagnitude, IntBinaryTwosComplement, IntDirect,

5

    IntOrder, SmtBv, SmtLia,

6

};

7

use conjure_cp::ast::pretty::pretty_find_with_representation;

8

use conjure_cp::ast::{Domain, DomainPtr, HasDomain, UnresolvedDomain};

9

use conjure_cp::representation::ReprRule;

10

use conjure_cp::settings::{

11

    Channelling, Heuristic, channelling, heuristic, next_heuristic_all_index,

12

    next_heuristic_interactive_index, next_heuristic_random_index,

13

};

14

use conjure_cp::{

15

    ast::{Atom, DeclarationPtr, Expression as Expr, GroundDomain, Moo, SymbolTable},

16

    representation::{ReprRulePtr, get_applicable_repr_by_short_name, get_repr_rules},

17

    rule_engine::{

18

        ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect as Reduction,

19

        register_rule, register_rule_set,

20

},

21

};

22

use itertools::any;

23

use std::collections::VecDeque;

24

use uniplate::Uniplate;

25

26

// Representations of Essence abstract types down to Essence'

27

// Applies for all solvers

28

register_rule_set!("ReprGeneral", ("Base"), |_| true);

29

30

/// Select a representation named in a `: domain` or `:: type` annotation.

31

///

32

/// Example: `1 in (x :: set (representation packed) of int)` selects the packed representation for this use of `x`.

33

/// Using different representations at different call sites requires channelling (`--channelling yes`).

34

#[register_rule("ReprGeneral", 10200, [In, TypeAnnotation, DomainAnnotation])]

35

298753

fn select_representation_from_annotation(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

36

298753

    match expr {

37

        Expr::In(meta, left, right) => {

38

            let Some((selected, symbols, constraints)) =

39

293369

                select_repr_from_annotated_expr(right.as_ref())?

40

            else {

41

293365

                return Err(RuleNotApplicable);

42

};

43

4

            Ok(Reduction::new(

44

4

                Expr::In(meta.clone(), left.clone(), Moo::new(selected)),

45

4

                constraints,

46

4

                symbols,

47

4

))

48

49

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

50

1

            let Some((selected, symbols, constraints)) = select_repr_from_annotated_expr(expr)?

51

            else {

52

                return Err(RuleNotApplicable);

53

};

54

1

            Ok(Reduction::new(selected, constraints, symbols))

55

56

5383

        _ => Err(RuleNotApplicable),

57

58

298753

59

60

/// If `expr` is a type/domain annotation that names a representation on a reference, select it.

61

293370

fn select_repr_from_annotated_expr(

62

293370

    expr: &Expr,

63

293370

) -> Result<Option<(Expr, SymbolTable, Vec<Expr>)>, conjure_cp::rule_engine::ApplicationError> {

64

293370

    let (inner, domain) = match expr {

65

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

66

5

            (inner, domain)

67

68

293365

        _ => return Ok(None),

69

};

70

71

5

    let Some(pref) = domain.representation_preference() else {

72

        return Ok(None);

73

};

74

75

5

    let Expr::Atomic(_, Atom::Reference(re)) = inner.as_ref() else {

76

        return Ok(None);

77

};

78

79

5

    if let Some(existing) = re.repr

80

        && existing.short_name() == pref

81

82

        return Ok(Some((re.clone().into(), SymbolTable::new(), Vec::new())));

83

5

84

85

5

    let Some(rule) = get_applicable_repr_by_short_name(re.ptr(), pref) else {

86

        return Ok(None);

87

};

88

89

5

    let mut re = re.clone();

90

5

    let (_, symbols, constraints) = re

91

5

        .update_or_init_repr_via(rule)

92

        .map_err(|_| RuleNotApplicable)?;

93

5

    Ok(Some((re.into(), symbols, constraints)))

94

293370

95

96

/// Select a representation for abstract domains

97

#[register_rule("ReprGeneral", 10000, [Atomic / Reference])]

98

42591395

fn select_representation(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {

99

42587824

    guard!(

100

42591395

        let Expr::Atomic(_, Atom::Reference(re)) = expr &&

101

42587824

        domain_needs_representation(&re.domain_of()) &&

102

14338916

        re.repr.is_none()

103

        else {

104

28248908

            return Err(RuleNotApplicable)

105

106

);

107

108

4343005

    let mut re = re.clone();

109

4343005

    let Some(rule) = choose_representation_rule(re.ptr(), symtab) else {

110

167002

        return Err(RuleNotApplicable);

111

};

112

4176003

    let (_, new_symbols, new_constraints) = re

113

4176003

        .select_or_init_repr_via(rule)

114

        .map_err(|_| RuleNotApplicable)?;

115

4176003

    Ok(Reduction::new(re.into(), new_constraints, new_symbols))

116

42591395

117

118

/// Select the representation on an auxiliary declaration's result reference as well as on its

119

/// declaration. Unlike ordinary references, this reference is stored outside the expression's

120

/// child list and is therefore not visited by `select_representation` above.

121

#[register_rule("ReprGeneral", 10000, [AuxDeclaration])]

122

1383653

fn select_aux_declaration_representation(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {

123

1383653

    let Expr::AuxDeclaration(meta, reference, inner) = expr else {

124

5281

        return Err(RuleNotApplicable);

125

};

126

1378372

    guard!(

127

1378372

        domain_needs_representation(&reference.domain_of()) && reference.repr.is_none()

128

        else {

129

142318

            return Err(RuleNotApplicable);

130

131

);

132

133

40664

    let mut reference = reference.clone();

134

40664

    let Some(rule) = choose_representation_rule(reference.ptr(), symtab) else {

135

        return Err(RuleNotApplicable);

136

};

137

40664

    let (_, new_symbols, new_constraints) = reference

138

40664

        .select_or_init_repr_via(rule)

139

        .map_err(|_| RuleNotApplicable)?;

140

40664

    Ok(Reduction::new(

141

40664

        Expr::AuxDeclaration(meta.clone(), reference, inner.clone()),

142

40664

        new_constraints,

143

40664

        new_symbols,

144

40664

))

145

1383653

146

147

/// Select a representation for unconstrained finds with abstract domains

148

#[register_rule("ReprGeneral", 9900, [Root], symbols_only)]

149

1885188

fn select_representation_unconstrained(expr: &Expr, symtab: &SymbolTable) -> ApplicationResult {

150

1885188

    let Expr::Root(..) = expr else {

151

4993

        return Err(RuleNotApplicable);

152

};

153

154

    // Copy the symbol table only once something is actually going to change: this rule is

155

    // attempted every time the root is visited, and almost always declines, so cloning up front

156

    // charged every visit the size of the whole table.

157

1880195

    let mut symbols: Option<SymbolTable> = None;

158

1880195

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

159

1880195

    for (_, decl) in symtab.iter_local() {

160

        // We want unrepresented decision vars!

161

803588730

        guard!(

162

803588730

            decl.as_find().is_some()          &&

163

800757269

            decl.reprs().is_empty()           &&

164

786415835

            let Some(dom) = decl.domain()     &&

165

786415835

            domain_needs_representation(&dom)

166

            else {

167

2831461

                continue;

168

169

);

170

171

619331

        let Some(rule) = choose_representation_rule(decl, symbols.as_ref().unwrap_or(symtab))

172

        else {

173

40739

            continue;

174

};

175

578592

        let mut decl = decl.clone();

176

578592

        let Ok((new_symbols, new_constraints)) = rule.init_for(&mut decl) else {

177

            continue;

178

};

179

578592

        let symbols = symbols.get_or_insert_with(|| symtab.clone());

180

578592

        symbols.update_insert(decl);

181

578592

        symbols.extend(new_symbols);

182

578592

        constraints.extend(new_constraints);

183

184

185

    // Representation initialisation may introduce no constraints and DeclarationPtr clone-on-write

186

    // updates are not reliably observable through SymbolTable equality. A copied symbol table

187

    // records successful initialisation explicitly, so zero-constraint layouts (matrix

188

    // components/packed) still dirty the root and expose their auxiliary declarations.

189

1880195

    let Some(symbols) = symbols else {

190

1678929

        return Err(RuleNotApplicable);

191

};

192

201266

    Ok(Reduction::new(expr.clone(), constraints, symbols))

193

1885188

194

195

/// Chooses one applicable representation without mutating the declaration.

196

///

197

/// With channelling disabled, declarations that share an identical abstract domain reuse the

198

/// representation already chosen for that domain. This mirrors Conjure applying one nested

199

/// representation to a whole matrix-of-sets, rather than letting each matrix component pick

200

/// independently under the `x` heuristic.

201

5003005

fn choose_representation_rule(decl: &DeclarationPtr, symbols: &SymbolTable) -> Option<ReprRulePtr> {

202

    // A declaration left holding the whole value of the one it represents has its shape settled

203

    // already -- an SMT array is the solver's variable, not a step towards one. The only choice

204

    // still open for it is how its integers are held, and once that is chosen there is nothing

205

    // left to decide. This comes first because the shortcuts below would otherwise hand it the

206

    // very layout that produced it, and it would be wrapped again, forever.

207

5003005

    let settled_layout = holds_whole_value_of_source(decl);

208

5003005

    if settled_layout && source_has_encoding_repr(decl) {

209

171414

        return None;

210

4831591

211

212

4831591

    if channelling() != Channelling::Yes

213

4831587

        && let Some(existing) = decl.reprs().iter().next().map(|(_, state)| state.rule())

214

215

3563522

        return Some(existing);

216

1268069

217

218

1268069

    if !settled_layout

219

1234571

        && channelling() == Channelling::No

220

22429

        && let Some(dom) = decl.domain()

221

22429

        && let Some(rule) = representation_for_identical_domain(decl, &dom, symbols)

222

223

4511

        return Some(rule);

224

1263558

225

226

1263558

    let mut candidates: Vec<_> = get_repr_rules()

227

46751646

        .filter_map(|rule| rule.probe_for(decl).ok().map(|score| (rule, score)))

228

        .collect();

229

6221560

    candidates.sort_by_key(|(rule, _)| rule.name());

230

231

    // A declaration left holding the whole value of the one it represents has its shape settled

232

    // already -- an SMT array is the solver's variable, not a step towards one. The only choice

233

    // still open for it is how its integers are held, and once that is chosen there is nothing

234

    // left to decide. Without this a whole-value layout would be offered to itself forever.

235

1263558

    if settled_layout {

236

68373

        candidates.retain(|(rule, _)| is_encoding_repr(*rule));

237

1230060

    } else if decl.domain().is_some_and(|dom| is_matrix_domain(&dom)) {

238

        // A matrix decides its layout first. Whether its integers are held as machine words or as

239

        // mathematical integers is a question for whatever that layout leaves behind: one variable

240

        // per entry under `components`, a single packed integer under `packed`, or the matrix

241

        // itself under `array`. Offering both questions at once would make them look like one.

242

133871

        candidates.retain(|(rule, _)| !is_encoding_repr(*rule));

243

1102267

244

245

1263558

    if channelling() == Channelling::Uniform

246

1213573

        && let Some(dom) = decl.domain()

247

1213573

        && let Some(selected) = conjure_cp::representation::uniform::selected(

248

1213573

            &dom,

249

1213573

            settled_layout || is_int_domain(&dom),

250

251

252

        // Do not silently fall back when the model's choice cannot represent this domain.

253

727932

        return candidates

254

727932

            .iter()

255

722941

            .find(|(rule, _)| rule.id() == selected.id())

256

722941

            .map(|(rule, _)| *rule);

257

535626

258

259

    // User-specified representation preference on the domain (e.g. set (representation packed)) defaults the choice

260

    // when that representation is applicable.

261

535626

    if let Some(dom) = decl.domain()

262

535626

        && let Some(pref) = dom.representation_preference()

263

166

        && let Some((rule, _)) = candidates

264

166

            .iter()

265

378

            .find(|(rule, _)| rule.short_name() == pref)

266

267

166

        return Some(*rule);

268

535460

269

270

535460

    if candidates.len() == 1 {

271

96599

        return candidates.first().map(|(rule, _)| *rule);

272

438861

273

274

438861

    match heuristic() {

275

987

        Heuristic::First => candidates.first().map(|(rule, _)| *rule),

276

412650

        Heuristic::All if !candidates.is_empty() => {

277

2045211

            let names: Vec<_> = candidates.iter().map(|(rule, _)| rule.name()).collect();

278

405377

            candidates

279

405377

                .get(next_heuristic_all_index(&names))

280

405377

                .map(|(rule, _)| *rule)

281

282

7273

        Heuristic::All => None,

283

        Heuristic::Interactive if !candidates.is_empty() => {

284

            let labels: Vec<_> = candidates

285

                .iter()

286

                .map(|(rule, _)| {

287

                    pretty_find_with_representation(decl, rule.short_name())

288

                        .unwrap_or_else(|| rule.name().to_string())

289

})

290

                .collect();

291

            let label_refs: Vec<_> = labels.iter().map(String::as_str).collect();

292

            candidates

293

                .get(next_heuristic_interactive_index(&label_refs))

294

                .map(|(rule, _)| *rule)

295

296

        Heuristic::Interactive => None,

297

        Heuristic::Random if !candidates.is_empty() => candidates

298

            .get(next_heuristic_random_index(candidates.len()))

299

            .map(|(rule, _)| *rule),

300

        Heuristic::Random => None,

301

25224

        Heuristic::Compact => super::representation_cost::choose(decl, &candidates)

302

25091

            .or_else(|| compact_representation_choice(&candidates)),

303

304

5003005

305

306

/// Stable preference order for breaking compactness ties, including scores saturated at

307

/// `usize::MAX`. Each family lists its preferred layout or encoding first. Unknown extensions

308

/// follow the built-ins and use their names as a final deterministic tie-break.

309

///

310

/// Prefer explicit function values over a packed integer or a relation graph, and mathematical

311

/// SMT integers over bit vectors. These preferences apply whenever costs tie, without inspecting

312

/// the declaration or treating overflow as a separate case.

313

9191

pub(super) fn representation_fallback_rank(rule: ReprRulePtr) -> usize {

314

    use crate::types::{

315

        function::{FunctionAsRelation, FunctionExplicit, FunctionPacked},

316

        matrix::{MatrixArray, MatrixComponents, MatrixPacked},

317

        mset::{MSetCounts, MSetOccurrence, MSetPacked, MSetRepetition},

318

        partition::{PartitionAsSet, PartitionOccurrence, PartitionPacked},

319

        permutation::PermutationAsFunction,

320

        record::{RecordComponents, RecordPacked},

321

        relation::{RelationAsSet, RelationOccurrence, RelationPacked},

322

        sequence::{SequenceExplicit, SequencePacked},

323

        set::{SetExplicit, SetOccurrence, SetPacked},

324

        tuple::{TupleComponents, TuplePacked},

325

        unnamed::UnnamedAsInt,

326

        variant::{VariantComponents, VariantPacked},

327

};

328

329

9191

    let order = [

330

9191

        FunctionExplicit::id(),

331

9191

        FunctionAsRelation::id(),

332

9191

        FunctionPacked::id(),

333

9191

        IntBinaryOffset::id(),

334

9191

        IntBinaryRank::id(),

335

9191

        IntBinarySignMagnitude::id(),

336

9191

        IntBinaryTwosComplement::id(),

337

9191

        IntDirect::id(),

338

9191

        IntOrder::id(),

339

9191

        SmtLia::id(),

340

9191

        SmtBv::id(),

341

9191

        MatrixArray::id(),

342

9191

        MatrixComponents::id(),

343

9191

        MatrixPacked::id(),

344

9191

        MSetCounts::id(),

345

9191

        MSetOccurrence::id(),

346

9191

        MSetRepetition::id(),

347

9191

        MSetPacked::id(),

348

9191

        PartitionAsSet::id(),

349

9191

        PartitionOccurrence::id(),

350

9191

        PartitionPacked::id(),

351

9191

        PermutationAsFunction::id(),

352

9191

        RecordComponents::id(),

353

9191

        RecordPacked::id(),

354

9191

        RelationAsSet::id(),

355

9191

        RelationOccurrence::id(),

356

9191

        RelationPacked::id(),

357

9191

        SequenceExplicit::id(),

358

9191

        SequencePacked::id(),

359

9191

        SetExplicit::id(),

360

9191

        SetOccurrence::id(),

361

9191

        SetPacked::id(),

362

9191

        TupleComponents::id(),

363

9191

        TuplePacked::id(),

364

9191

        UnnamedAsInt::id(),

365

9191

        VariantComponents::id(),

366

9191

        VariantPacked::id(),

367

9191

];

368

9191

    order

369

9191

        .iter()

370

112559

        .position(|id| *id == rule.id())

371

9191

        .unwrap_or(usize::MAX)

372

9191

373

374

/// Prefer non-packed layouts, then choose the lowest domain score and built-in tie-break rank.

375

26183

fn compact_representation_choice(candidates: &[(ReprRulePtr, usize)]) -> Option<ReprRulePtr> {

376

26183

    candidates

377

26183

        .iter()

378

8792

        .min_by_key(|(rule, score)| {

379

8792

380

8792

                rule.short_name() == "packed",

381

8792

                *score,

382

8792

                representation_fallback_rank(*rule),

383

8792

                rule.name(),

384

8792

385

8792

})

386

2840

        .map(|(rule, _)| *rule)

387

26183

388

389

/// Representations that record only how a declaration's integers are held, leaving its shape and

390

/// domain untouched.

391

///

392

/// Every other representation lays a value out differently -- decomposing it, packing it, changing

393

/// what the solver sees -- and so answers a different question. Keeping the two apart is what lets

394

/// a matrix choose `array` and its integers choose `bv` as two independent decisions rather than

395

/// one combined `bv-array`.

396

425531

fn is_encoding_repr(rule: ReprRulePtr) -> bool {

397

425531

398

425531

        SmtLia::id(),

399

425531

        SmtBv::id(),

400

425531

        IntBinaryTwosComplement::id(),

401

425531

        IntBinaryOffset::id(),

402

425531

        IntBinaryRank::id(),

403

425531

        IntBinarySignMagnitude::id(),

404

425531

        IntDirect::id(),

405

425531

        IntOrder::id(),

406

425531

407

425531

    .contains(&rule.id())

408

425531

409

410

/// True if `decl` was introduced by a representation that left it holding the whole value, rather

411

/// than a piece of one -- recognisable because it kept the source's domain.

412

6539353

pub(crate) fn holds_whole_value_of_source(decl: &DeclarationPtr) -> bool {

413

6539353

    let source = decl.source().clone();

414

6539353

    let Some(source) = source else {

415

2289982

        return false;

416

};

417

    // Compare resolved forms: a representation stores the domain it was initialised with, which

418

    // has already been resolved, while the declaration it came from may still name a letting.

419

8498742

    let resolved = |decl: &DeclarationPtr| {

420

8498742

        decl.domain()

421

8498742

            .and_then(|dom| dom.resolve().ok().map(DomainPtr::from).or(Some(dom)))

422

8498742

};

423

4249371

    match (resolved(decl), resolved(&source)) {

424

4249371

        (Some(mine), Some(theirs)) => mine == theirs,

425

        _ => false,

426

427

6539353

428

429

/// True if the declaration `decl` represents has already had its integer encoding chosen.

430

223287

fn source_has_encoding_repr(decl: &DeclarationPtr) -> bool {

431

223287

    let source = decl.source().clone();

432

223287

    let Some(source) = source else {

433

        return false;

434

};

435

223287

    source

436

223287

        .reprs()

437

223287

        .iter()

438

223287

        .any(|(_, state)| is_encoding_repr(state.rule()))

439

223287

440

441

/// Find a representation already chosen for another declaration with the same domain.

442

///

443

/// Any representation the sibling settled on is worth copying, component layouts included: a

444

/// matrix chooses between `components`, `packed` and `array`, so `components` is a modelling

445

/// choice like any other rather than a decomposition to see past.

446

22429

fn representation_for_identical_domain(

447

22429

    decl: &DeclarationPtr,

448

22429

    dom: &DomainPtr,

449

22429

    symbols: &SymbolTable,

450

22429

) -> Option<ReprRulePtr> {

451

22429

    for (name, other) in symbols.iter_local() {

452

112734

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

453

17986

            continue;

454

94748

455

94748

        let Some(other_dom) = other.domain() else {

456

            continue;

457

};

458

94748

        if &other_dom != dom {

459

85579

            continue;

460

9169

461

9169

        for (_, state) in other.reprs().iter() {

462

4511

            let rule = state.rule();

463

4511

            if rule.probe_for(decl).is_ok() {

464

4511

                return Some(rule);

465

466

467

468

17918

    None

469

22429

470

471

/// In a comparison operation, it is probably a good idea for the LHS and RHS to

472

/// have the same representation, if applicable; E.g:

473

/// ```plain

474

/// x#MyRepr > y

475

/// ~>

476

/// x#MyRepr > y#MyRepr

477

/// ```

478

#[register_rule("ReprGeneral", 10100, [Eq, Neq, Lt, Gt, Leq, Geq, LexLt, LexLeq, LexGt, LexGeq])]

479

12431381

fn uniform_repr_in_comparison_op(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

480

    guard! {

481

12431381

        let Some((lhs, rhs)) = as_cmp_or_lex_op(expr)               &&

482

12426700

        let Expr::Atomic(_, Atom::Reference(lhs_re)) = lhs.as_ref() &&

483

2499826

        let Expr::Atomic(_, Atom::Reference(rhs_re)) = rhs.as_ref()

484

        else {

485

1931777

            return Err(RuleNotApplicable)

486

487

488

489

    // A variable left holding the whole value of another has its representation settled by the

490

    // rules above; propagating another one onto it would wrap it again, and again.

491

568049

    if holds_whole_value_of_source(lhs_re.ptr()) || holds_whole_value_of_source(rhs_re.ptr()) {

492

9751

        return Err(RuleNotApplicable);

493

558298

494

495

    // A representation written on the declaration's domain is the user's choice; matching the

496

    // other side must not override it.

497

    let has_preference =

498

27720

        |re: &conjure_cp::ast::Reference| re.domain_of().representation_preference().is_some();

499

500

558298

    match (lhs_re.get_repr(), rhs_re.get_repr()) {

501

26691

        (Some((lhs_rule, _)), None) if !has_preference(rhs_re) => {

502

26684

            let mut new_rhs = rhs_re.clone();

503

26684

            let (_, symbols, constraints) = new_rhs

504

26684

                .select_or_init_repr_via(lhs_rule)

505

                .map_err(|_| RuleNotApplicable)?;

506

            let new_expr =

507

26684

                expr.with_children(VecDeque::from([lhs.as_ref().clone(), new_rhs.into()]));

508

26684

            Ok(Reduction::new(new_expr, constraints, symbols))

509

510

1029

        (None, Some((rhs_rule, _))) if !has_preference(lhs_re) => {

511

1029

            let mut new_lhs = lhs_re.clone();

512

1029

            let (_, symbols, constraints) = new_lhs

513

1029

                .select_or_init_repr_via(rhs_rule)

514

                .map_err(|_| RuleNotApplicable)?;

515

            let new_expr =

516

1029

                expr.with_children(VecDeque::from([new_lhs.into(), rhs.as_ref().clone()]));

517

1029

            Ok(Reduction::new(new_expr, constraints, symbols))

518

519

530585

        _ => Err(RuleNotApplicable),

520

521

12431381

522

523

/// True if integers are an abstract type for the solver being targeted.

524

///

525

/// SAT has no integers: an int variable is encoded as a vector of Booleans, and which encoding it

526

/// gets is a modelling choice like any other representation. Solvers with native integers leave

527

/// them alone.

528

13078899

fn int_needs_representation() -> bool {

529

13078899

    conjure_cp::settings::ints_need_representation()

530

13078899

531

532

/// True if a declaration with this domain needs a representation chosen for it.

533

///

534

/// Three separate reasons: the domain is abstract in Essence' terms (a set, a tuple, ...), it is a

535

/// matrix and so has a layout to choose, or it is an integer and the solver has no integers of its

536

/// own to hold it.

537

///

538

/// The integer reason deliberately does not look inside a matrix. How a matrix is laid out and how

539

/// its integers are held are independent choices: pick `components` and each entry becomes its own

540

/// integer declaration which then picks its own encoding, pick a whole-matrix layout and the

541

/// encoding choice lands on the matrix that layout leaves behind. Folding the two together would

542

/// mean one decision pretending to be two.

543

830411438

pub(crate) fn domain_needs_representation(domain: &DomainPtr) -> bool {

544

830411438

    is_abstract_domain(domain)

545

827949370

        || is_matrix_domain(domain)

546

821691780

        || (is_int_domain(domain) && int_needs_representation())

547

830411438

548

549

/// True if this domain is a matrix one, following domain lettings.

550

///

551

/// Every matrix has a layout to choose -- one variable per entry, the whole thing packed into a

552

/// single integer, or for a solver with arrays, the whole thing as an array -- so matrices go

553

/// through representation selection like any other type, and the heuristic weighs the options

554

/// against each other.

555

829208536

fn is_matrix_domain(domain: &DomainPtr) -> bool {

556

829208536

    match domain.as_ref() {

557

828389302

        Domain::Ground(gd) => matches!(gd.as_ref(), GroundDomain::Matrix(..)),

558

819234

        Domain::Unresolved(ud) => match ud.as_ref() {

559

724651

            UnresolvedDomain::Matrix(..) => true,

560

29106

            UnresolvedDomain::Reference(re) => is_matrix_domain(&re.domain_of()),

561

65477

            _ => false,

562

},

563

564

829208536

565

566

/// True if the domain is abstract w.r.t Essence', ignoring how the solver holds integers and how a

567

/// matrix is laid out.

568

///

569

/// This is the narrower question of whether a *type* is compound -- a set, a tuple, a record. Ask

570

/// it when what matters is the shape of the values themselves; ask

571

/// [`domain_needs_representation`] when what matters is whether a declaration still has a choice

572

/// to make.

573

#[allow(clippy::match_like_matches_macro)]

574

846610764

pub(crate) fn is_abstract_domain(domain: &DomainPtr) -> bool {

575

846610764

    match domain.as_ref() {

576

842593774

        Domain::Ground(gd) => match gd.as_ref() {

577

            // These domains are concrete for all solvers

578

833649477

            GroundDomain::Empty(..) | GroundDomain::Bool | GroundDomain::Int(_, _) => false,

579

            // Represent matrices if they have abstract types inside them;

580

            // Matrices of concrete types are handled separately by the

581

            // `ReprMatrixComponents`rule set

582

            GroundDomain::Matrix(inner_dom, idx_doms, _) => {

583

6484868

                is_abstract_domain(&inner_dom.into())

584

6085416

                    || any(idx_doms, |d| is_abstract_domain(&d.into()))

585

586

            // All other domains are abstract

587

2459429

            _ => true,

588

},

589

4016990

        Domain::Unresolved(ud) => match ud.as_ref() {

590

1818669

            UnresolvedDomain::Int(..) => false,

591

            // Represent matrices if they have abstract types inside them;

592

            // Matrices of concrete types are handled separately by the

593

            // `ReprMatrixComponents`rule set

594

            UnresolvedDomain::Matrix(inner_dom, idx_doms, _) => {

595

710639

                is_abstract_domain(inner_dom) || any(idx_doms, is_abstract_domain)

596

597

            // Recurse into domain letting

598

1485036

            UnresolvedDomain::Reference(re) => is_abstract_domain(&re.domain_of()),

599

            // All other domains are abstract

600

2646

            _ => true,

601

},

602

603

846610764

604

605

/// True if this domain is an integer one, following domain lettings.

606

822932331

fn is_int_domain(domain: &DomainPtr) -> bool {

607

822932331

    match domain.as_ref() {

608

822825521

        Domain::Ground(gd) => matches!(gd.as_ref(), GroundDomain::Int(_, _)),

609

106810

        Domain::Unresolved(ud) => match ud.as_ref() {

610

62759

            UnresolvedDomain::Int(..) => true,

611

28413

            UnresolvedDomain::Reference(re) => is_int_domain(&re.domain_of()),

612

15638

            _ => false,

613

},

614

615

822932331

616

617

#[cfg(test)]

618

mod tests {

619

    use super::*;

620

    use conjure_cp::ast::{Domain, MSetAttr, SetAttr};

621

    use conjure_cp::settings::set_heuristic;

622

    use conjure_cp::{domain_int, range};

623

624

    #[test]

625

1

    fn compact_fallback_prefers_non_packed_even_with_a_larger_domain_score() {

626

1

        let packed: Vec<_> = get_repr_rules()

627

37

            .filter(|rule| rule.short_name() == "packed")

628

            .collect();

629

1

        let non_packed: Vec<_> = get_repr_rules()

630

37

            .filter(|rule| rule.short_name() != "packed")

631

            .collect();

632

1

        assert!(!packed.is_empty() && !non_packed.is_empty());

633

1

        for packed in packed {

634

10

            for &other in &non_packed {

635

270

                for score in [0, usize::MAX] {

636

540

                    for candidates in [

637

540

                        [(packed, score), (other, usize::MAX)],

638

540

                        [(other, usize::MAX), (packed, score)],

639

540

] {

640

1080

                        assert_eq!(

641

1080

                            compact_representation_choice(&candidates).unwrap().id(),

642

1080

                            other.id()

643

);

644

645

646

647

10

            assert_eq!(

648

10

                compact_representation_choice(&[(packed, 0)]).unwrap().id(),

649

10

                packed.id()

650

);

651

652

1

        assert!(compact_representation_choice(&[]).is_none());

653

1

654

655

    #[test]

656

1

    fn compact_prefers_lia_when_smt_integer_scores_saturate() {

657

1

        let lia = get_repr_rules()

658

13

            .find(|rule| rule.id() == SmtLia::id())

659

1

            .expect("SmtLia representation should be registered");

660

1

        let bv = get_repr_rules()

661

14

            .find(|rule| rule.id() == SmtBv::id())

662

1

            .expect("SmtBv representation should be registered");

663

664

1

        assert_eq!(

665

1

            compact_representation_choice(&[(bv, usize::MAX), (lia, usize::MAX)])

666

1

                .unwrap()

667

1

                .name(),

668

1

            "SmtLia"

669

);

670

1

671

672

    #[test]

673

1

    fn domain_representation_preference_defaults_the_choice() {

674

        use conjure_cp::representation::get_applicable_repr_by_short_name;

675

676

1

        set_heuristic(Heuristic::First);

677

1

        let mut symbols = SymbolTable::new();

678

1

        let declaration = symbols.gen_find(&Domain::set(

679

1

            SetAttr::new_min_max_size(1, 2).with_representation("packed"),

680

1

            domain_int!(1..3),

681

1

));

682

683

1

        assert_eq!(

684

1

            choose_representation_rule(&declaration, &symbols)

685

1

                .unwrap()

686

1

                .short_name(),

687

1

            "packed"

688

);

689

690

1

        let declaration = symbols.gen_find(&Domain::set(

691

1

            SetAttr::new_min_max_size(1, 2).with_representation("explicit"),

692

1

            domain_int!(1..3),

693

1

));

694

695

1

        assert_eq!(

696

1

            choose_representation_rule(&declaration, &symbols)

697

1

                .unwrap()

698

1

                .short_name(),

699

1

            "explicit"

700

);

701

702

1

        let declaration = symbols.gen_find(&Domain::mset(

703

1

            MSetAttr::new_max_size(3).with_representation("occurrence"),

704

1

            domain_int!(1..3),

705

1

));

706

707

1

        assert_eq!(

708

1

            choose_representation_rule(&declaration, &symbols)

709

1

                .unwrap()

710

1

                .short_name(),

711

1

            "occurrence"

712

);

713

714

1

        let declaration = symbols.gen_find(&Domain::mset(

715

1

            MSetAttr::new_max_size(3).with_representation("counts"),

716

1

            domain_int!(1..3),

717

1

));

718

719

1

        assert_eq!(

720

1

            choose_representation_rule(&declaration, &symbols)

721

1

                .unwrap()

722

1

                .short_name(),

723

1

            "counts"

724

);

725

726

1

        let declaration = symbols.gen_find(&Domain::mset(

727

1

            MSetAttr::new_max_size(3).with_representation("repetition"),

728

1

            domain_int!(1..3),

729

1

));

730

731

1

        assert_eq!(

732

1

            choose_representation_rule(&declaration, &symbols)

733

1

                .unwrap()

734

1

                .short_name(),

735

1

            "repetition"

736

);

737

738

1

        assert!(get_applicable_repr_by_short_name(&declaration, "explicit").is_none());

739

1

740

741

    #[test]

742

1

    fn auxiliary_declaration_reference_selects_the_initialised_representation() {

743

        use conjure_cp::ast::{AbstractLiteral, Expression, Metadata, Moo, Reference};

744

745

1

        let mut symbols = SymbolTable::new();

746

1

        let declaration = symbols.gen_find_auxiliary(&Domain::mset(

747

1

            MSetAttr::new_max_size(2).with_representation("counts"),

748

1

            domain_int!(1..3),

749

1

));

750

1

        let auxiliary = Expression::AuxDeclaration(

751

1

            Metadata::new(),

752

1

            Reference::new(declaration),

753

1

            Moo::new(Expression::AbstractLiteral(

754

1

                Metadata::new(),

755

1

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

756

1

)),

757

1

);

758

759

1

        let rewritten = select_aux_declaration_representation(&auxiliary, &symbols)

760

1

            .unwrap()

761

1

            .new_expression;

762

1

        let Expression::AuxDeclaration(_, selected, _) = rewritten else {

763

            panic!("expected an auxiliary declaration, got {rewritten}");

764

};

765

1

        assert_eq!(selected.get_repr().unwrap().0.short_name(), "counts");

766

1

767

768

    #[test]

769

1

    fn annotation_selects_packed_representation() {

770

        use conjure_cp::ast::{Atom, Expression, Metadata, Moo, Reference};

771

        use conjure_cp::representation::get_applicable_repr_by_short_name;

772

773

1

        set_heuristic(Heuristic::First);

774

1

        let mut symbols = SymbolTable::new();

775

        let declaration =

776

1

            symbols.gen_find(&Domain::set(SetAttr::new_max_size(3), domain_int!(1..4)));

777

1

        let re = Reference::new(declaration.clone());

778

1

        let annotated = Expression::TypeAnnotation(

779

1

            Metadata::new(),

780

1

            Moo::new(re.into()),

781

1

            Domain::set(

782

1

                SetAttr::<i32>::default().with_representation("packed"),

783

1

                domain_int!(1..4),

784

1

),

785

1

);

786

787

1

        let result = select_representation_from_annotation(&annotated, &symbols).unwrap();

788

1

        let Expression::Atomic(_, Atom::Reference(selected)) = result.new_expression else {

789

            panic!("expected a reference, got {}", result.new_expression);

790

};

791

1

        assert_eq!(selected.get_repr().unwrap().0.short_name(), "packed");

792

1

        assert_eq!(

793

1

            get_applicable_repr_by_short_name(&declaration, "packed")

794

1

                .unwrap()

795

1

                .name(),

796

1

            "SetPacked"

797

);

798

1

799