Grcov report - attribute_as

1

//! Lifts Conjure's attribute-as-constraint predicate syntax (`reflexive(r)`, `size(s, 3)`, ...)

2

//! into the declaration domain attributes of its target, when the target is a plain reference to

3

//! a locally declared `find`/`given` and the attribute can be losslessly merged into the domain.

4

//! Mirrors Conjure's `attributeAsConstraints_OnStmts` (`Process/AttributeAsConstraints.hs`).

5

//!

6

//! Only [`GroundDomain::Set`], [`GroundDomain::MSet`], [`GroundDomain::Function`] and

7

//! [`GroundDomain::Relation`] are covered, matching every domain kind Conjure's own

8

//! `attributeToConstraint` dispatch table supports (it has no case for `DomainSequence`, which

9

//! does not exist in vanilla Conjure -- Oxide's `Sequence` is its own campaign type with no

10

//! Conjure AAC equivalent to port). `Partition` is excluded because it has not been started as an

11

//! Oxide campaign type at all: there is no domain/representation support to hang partition-specific

12

//! attributes off of.

13

//!

14

//! Anything that cannot be safely lifted (a symbolic value, an unresolved domain, a target that

15

//! isn't a bare top-level reference to a `find`/`given`, or an attribute/domain-kind combination

16

//! this does not cover) is left in place for the fallback expansion rule

17

//! ([`crate::passes::attribute_as_constraint_fallback`]) to turn into an equivalent formula.

18

19

use std::collections::HashMap;

20

21

use conjure_cp::{

22

    ast::{

23

        Atom, BinaryAttr, DecisionVariable, DeclarationKind, DeclarationPtr, Domain, DomainPtr,

24

        Expression as Expr, GroundDomain, JectivityAttr, Literal as Lit, Moo, Name, PartialityAttr,

25

        Range, SymbolTable, eval_constant,

26

},

27

    rule_engine::{ApplicationError, ApplicationResult, RuleEffect, register_rule},

28

};

29

30

use ApplicationError::RuleNotApplicable;

31

32

type Int = i32;

33

34

/// Lifts every top-level `AttributeAsConstraint` whose target can be merged into a declaration

35

/// domain, dropping it from the constraint list and updating the declaration in its place.

36

#[register_rule("Base", 10300, [Root])]

37

4365069

fn lift_attribute_as_constraints(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

38

4365069

    let Expr::Root(meta, children) = expr else {

39

5598

        return Err(RuleNotApplicable);

40

};

41

42

4359471

    let mut kept_children = Vec::with_capacity(children.len());

43

    // Keyed by declaration name so several AACs targeting the same declaration (e.g.

44

    // `minSize(s, 1)` and `maxSize(s, 3)`) narrow the same domain in sequence rather than

45

    // clobbering each other.

46

4359471

    let mut updated: HashMap<Name, (DeclarationPtr, DomainPtr)> = HashMap::new();

47

48

4359471

    for child in children {

49

68771526

        let Expr::AttributeAsConstraint(_, target, attr, value) = child else {

50

68771519

            kept_children.push(child.clone());

51

68771519

            continue;

52

};

53

54

7

        match try_lift(target, attr.as_str(), value.as_deref(), symbols, &updated) {

55

            Some((decl, new_domain)) => {

56

4

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

57

4

                updated.insert(name, (decl, new_domain));

58

59

3

            None => kept_children.push(child.clone()),

60

61

62

63

4359471

    if updated.is_empty() {

64

4359468

        return Err(RuleNotApplicable);

65

3

66

67

3

    let declaration_updates: Vec<(DeclarationPtr, DeclarationKind)> = updated

68

3

        .into_values()

69

3

        .map(|(decl, new_domain)| {

70

3

            let updated_kind = match &*decl.kind() {

71

                DeclarationKind::Find(_) => {

72

3

                    DeclarationKind::Find(DecisionVariable::new(new_domain))

73

74

                DeclarationKind::FindAuxiliary(_) => {

75

                    DeclarationKind::FindAuxiliary(DecisionVariable::new(new_domain))

76

77

                DeclarationKind::Given(_) => DeclarationKind::Given(new_domain),

78

                other => conjure_cp::bug!(

79

                    "try_lift only returns Find/FindAuxiliary/Given declarations, got {other:?}"

80

),

81

};

82

3

            (decl, updated_kind)

83

3

})

84

        .collect();

85

86

3

    Ok(RuleEffect::new(

87

3

        Expr::Root(meta.clone(), kept_children),

88

3

        vec![],

89

3

        SymbolTable::new(),

90

3

91

3

    .with_declaration_updates(declaration_updates))

92

4365069

93

94

/// Attempts to merge one `AttributeAsConstraint` into its target's declaration domain, returning

95

/// the declaration and its updated domain on success.

96

7

fn try_lift(

97

7

    target: &Expr,

98

7

    attr_name: &str,

99

7

    value: Option<&Expr>,

100

7

    symbols: &SymbolTable,

101

7

    already_updated: &HashMap<Name, (DeclarationPtr, DomainPtr)>,

102

7

) -> Option<(DeclarationPtr, DomainPtr)> {

103

7

    let Expr::Atomic(_, Atom::Reference(reference)) = target else {

104

1

        return None;

105

};

106

107

6

    let name = reference.name().clone();

108

6

    let decl = symbols.lookup_local(&name)?;

109

110

6

    if !matches!(

111

6

        &*decl.kind(),

112

6

        DeclarationKind::Find(_) | DeclarationKind::FindAuxiliary(_) | DeclarationKind::Given(_)

113

6

) {

114

        return None;

115

6

116

117

6

    let current_domain = match already_updated.get(&name) {

118

1

        Some((_, dom)) => dom.clone(),

119

5

        None => decl.domain()?,

120

};

121

122

6

    let Domain::Ground(ground) = current_domain.as_ref() else {

123

        // Unresolved domains (e.g. a size bound referring to another variable) cannot be safely

124

        // narrowed here; fall back to expanding the AAC to an explicit formula instead.

125

        return None;

126

};

127

128

6

    let value = match value {

129

4

        Some(value_expr) => match eval_constant(value_expr)? {

130

3

            Lit::Int(v) => Some(v),

131

            _ => return None,

132

},

133

2

        None => None,

134

};

135

136

5

    let new_ground = merge_attribute_into_ground_domain(ground.as_ref(), attr_name, value)?;

137

4

    let new_domain = Moo::new(Domain::Ground(Moo::new(new_ground)));

138

4

    Some((decl, new_domain))

139

7

140

141

/// Merges one attribute into a ground domain's attributes, returning `None` if the attribute does

142

/// not apply to this domain kind, or if merging it would conflict with an existing bound (in which

143

/// case the caller should fall back to expanding the AAC as an explicit, possibly-unsatisfiable,

144

/// constraint rather than silently dropping information).

145

5

fn merge_attribute_into_ground_domain(

146

5

    domain: &GroundDomain,

147

5

    attr_name: &str,

148

5

    value: Option<Int>,

149

5

) -> Option<GroundDomain> {

150

5

    match domain {

151

        GroundDomain::Set(attr, inner) => {

152

3

            let mut attr = attr.clone();

153

3

            attr.size = merge_size_range(&attr.size, attr_name, value?)?;

154

3

            Some(GroundDomain::Set(attr, inner.clone()))

155

156

        GroundDomain::MSet(attr, inner) => {

157

            let mut attr = attr.clone();

158

            match attr_name {

159

                "size" | "minSize" | "maxSize" => {

160

                    attr.size = merge_size_range(&attr.size, attr_name, value?)?;

161

162

                "minOccur" | "maxOccur" => {

163

                    attr.occurrence = merge_size_range(&attr.occurrence, attr_name, value?)?;

164

165

                _ => return None,

166

167

            Some(GroundDomain::MSet(attr, inner.clone()))

168

169

        GroundDomain::Function(attr, dom, cdom) => {

170

            let mut attr = attr.clone();

171

            match attr_name {

172

                "size" | "minSize" | "maxSize" => {

173

                    attr.size = merge_size_range(&attr.size, attr_name, value?)?;

174

175

                "total" => attr.partiality = PartialityAttr::Total,

176

                "injective" | "surjective" | "bijective" => {

177

                    attr.jectivity = merge_jectivity(&attr.jectivity, attr_name)?;

178

179

                _ => return None,

180

181

            Some(GroundDomain::Function(attr, dom.clone(), cdom.clone()))

182

183

        GroundDomain::Relation(attr, inners) => {

184

2

            let mut attr = attr.clone();

185

2

            match attr_name {

186

                "size" | "minSize" | "maxSize" => {

187

                    attr.size = merge_size_range(&attr.size, attr_name, value?)?;

188

189

                _ => {

190

                    // Binary attributes only make sense (and are only ever validated by Conjure)

191

                    // on arity-2 relations.

192

2

                    let bin_attr = BinaryAttr::from_keyword(attr_name)?;

193

2

                    if inners.len() != 2 {

194

1

                        return None;

195

1

196

1

                    if !attr.binary.contains(&bin_attr) {

197

1

                        attr.binary.push(bin_attr);

198

199

200

201

1

            Some(GroundDomain::Relation(attr, inners.clone()))

202

203

        _ => None,

204

205

5

206

207

/// Narrows a `size`/`minSize`/`maxSize`-shaped range attribute, returning `None` if the new bound

208

/// would conflict with the existing one (so the caller falls back to an explicit, and in that case

209

/// necessarily unsatisfiable, constraint rather than silently discarding the conflict).

210

3

fn merge_size_range(current: &Range<Int>, kind: &str, value: Int) -> Option<Range<Int>> {

211

3

    let mut lo = current.low().copied();

212

3

    let mut hi = current.high().copied();

213

3

    match kind {

214

        "size" => {

215

1

            if !current.contains(&value) {

216

                return None;

217

1

218

1

            lo = Some(value);

219

1

            hi = Some(value);

220

221

        "minSize" | "minOccur" => {

222

1

            lo = Some(lo.map_or(value, |l| l.max(value)));

223

224

        "maxSize" | "maxOccur" => {

225

1

            hi = Some(hi.map_or(value, |h| h.min(value)));

226

227

        _ => return None,

228

229

3

    if let (Some(l), Some(h)) = (lo, hi)

230

2

        && l > h

231

232

        return None;

233

3

234

3

    Some(Range::new(lo, hi))

235

3

236

237

/// Narrows a function's jectivity attribute, returning `None` for a genuine conflict (e.g.

238

/// requesting `injective` on a domain already narrowed some other, incompatible way -- there is

239

/// none today since `None`/`Injective`/`Surjective`/`Bijective` only ever combine towards

240

/// `Bijective`, but the explicit `None` keeps this total if that ever changes).

241

fn merge_jectivity(current: &JectivityAttr, attr_name: &str) -> Option<JectivityAttr> {

242

    let requested = match attr_name {

243

        "injective" => JectivityAttr::Injective,

244

        "surjective" => JectivityAttr::Surjective,

245

        "bijective" => JectivityAttr::Bijective,

246

        _ => return None,

247

};

248

    Some(match (current, &requested) {

249

        (JectivityAttr::None, _) => requested,

250

        (c, r) if *c == *r => requested,

251

        (JectivityAttr::Bijective, _) | (_, JectivityAttr::Bijective) => JectivityAttr::Bijective,

252

        (JectivityAttr::Injective, JectivityAttr::Surjective)

253

        | (JectivityAttr::Surjective, JectivityAttr::Injective) => JectivityAttr::Bijective,

254

        #[allow(unreachable_patterns)]

255

        _ => return None,

256

})

257

258

259

#[cfg(test)]

260

mod tests {

261

    use super::*;

262

    use conjure_cp::ast::{DeclarationPtr, Metadata, Reference, RelAttr, SetAttr};

263

    use conjure_cp::rule_engine::get_rule_by_name;

264

    use conjure_cp::{domain_int, range};

265

    use ustr::Ustr;

266

267

6

    fn root(children: Vec<Expr>) -> Expr {

268

6

        Expr::Root(Metadata::new(), children)

269

6

270

271

7

    fn attr_expr(target: Expr, attr: &str, value: Option<Expr>) -> Expr {

272

7

        Expr::AttributeAsConstraint(

273

7

            Metadata::new(),

274

7

            Moo::new(target),

275

7

            Ustr::from(attr),

276

7

            value.map(Moo::new),

277

7

278

7

279

280

7

    fn ref_expr(decl: &DeclarationPtr) -> Expr {

281

7

        Expr::Atomic(

282

7

            Metadata::new(),

283

7

            Atom::Reference(Reference::new(decl.clone())),

284

7

285

7

286

287

4

    fn int_lit(v: i32) -> Expr {

288

4

        Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Int(v)))

289

4

290

291

6

    fn rule() -> &'static conjure_cp::rule_engine::Rule<'static> {

292

6

        get_rule_by_name("lift_attribute_as_constraints").expect("rule registered")

293

6

294

295

    #[test]

296

1

    fn lifts_size_into_set_attr() {

297

1

        let mut symbols = SymbolTable::new();

298

1

        let s = DeclarationPtr::new_find(

299

1

            Name::user("s"),

300

1

            Domain::set(SetAttr::<Int>::default(), domain_int!(1..5)),

301

1

);

302

1

        symbols.insert(s.clone()).expect("insert s");

303

304

1

        let tree = root(vec![attr_expr(ref_expr(&s), "size", Some(int_lit(3)))]);

305

1

        let result = rule().apply(&tree, &symbols).expect("should lift size");

306

307

1

        let Expr::Root(_, kept) = &result.new_expression else {

308

            panic!("expected Root")

309

};

310

1

        assert!(

311

1

            kept.is_empty(),

312

            "the lifted AAC should be removed from the constraint list"

313

);

314

1

        assert_eq!(

315

1

            result.updated_declaration_names().collect::<Vec<_>>(),

316

1

            vec![Name::user("s")]

317

);

318

1

319

320

    #[test]

321

1

    fn lifts_minsize_and_maxsize_from_two_separate_aacs_on_the_same_declaration() {

322

1

        let mut symbols = SymbolTable::new();

323

1

        let s = DeclarationPtr::new_find(

324

1

            Name::user("s"),

325

1

            Domain::set(SetAttr::<Int>::default(), domain_int!(1..5)),

326

1

);

327

1

        symbols.insert(s.clone()).expect("insert s");

328

329

1

        let tree = root(vec![

330

1

            attr_expr(ref_expr(&s), "minSize", Some(int_lit(2))),

331

1

            attr_expr(ref_expr(&s), "maxSize", Some(int_lit(4))),

332

1

]);

333

1

        let result = rule().apply(&tree, &symbols).expect("should lift both");

334

335

1

        let Expr::Root(_, kept) = &result.new_expression else {

336

            panic!("expected Root")

337

};

338

1

        assert!(kept.is_empty());

339

        // Only one declaration update should be recorded for `s`, reflecting both narrowings.

340

1

        assert_eq!(

341

1

            result.updated_declaration_names().collect::<Vec<_>>(),

342

1

            vec![Name::user("s")]

343

);

344

1

345

346

    #[test]

347

1

    fn declines_when_target_is_not_a_bare_reference() {

348

1

        let symbols = SymbolTable::new();

349

1

        let non_reference_target = Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Bool(true)));

350

1

        let tree = root(vec![attr_expr(

351

1

            non_reference_target,

352

1

            "size",

353

1

            Some(int_lit(3)),

354

1

        )]);

355

356

1

        let err = rule().apply(&tree, &symbols).unwrap_err();

357

1

        assert!(matches!(err, ApplicationError::RuleNotApplicable));

358

1

359

360

    #[test]

361

1

    fn declines_when_value_is_not_a_constant() {

362

1

        let mut symbols = SymbolTable::new();

363

1

        let bound = DeclarationPtr::new_find(Name::user("n"), domain_int!(1..5));

364

1

        symbols.insert(bound.clone()).expect("insert n");

365

1

        let s = DeclarationPtr::new_find(

366

1

            Name::user("s"),

367

1

            Domain::set(SetAttr::<Int>::default(), domain_int!(1..5)),

368

1

);

369

1

        symbols.insert(s.clone()).expect("insert s");

370

371

1

        let tree = root(vec![attr_expr(

372

1

            ref_expr(&s),

373

1

            "size",

374

1

            Some(ref_expr(&bound)),

375

1

        )]);

376

1

        let err = rule().apply(&tree, &symbols).unwrap_err();

377

1

        assert!(matches!(err, ApplicationError::RuleNotApplicable));

378

1

379

380

    #[test]

381

1

    fn lifts_reflexive_into_relation_binary_attrs() {

382

1

        let mut symbols = SymbolTable::new();

383

1

        let r = DeclarationPtr::new_find(

384

1

            Name::user("r"),

385

1

            Domain::relation(

386

1

                RelAttr::<Int>::default(),

387

1

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

388

1

),

389

1

);

390

1

        symbols.insert(r.clone()).expect("insert r");

391

392

1

        let tree = root(vec![attr_expr(ref_expr(&r), "reflexive", None)]);

393

1

        let result = rule()

394

1

            .apply(&tree, &symbols)

395

1

            .expect("should lift reflexive");

396

397

1

        let Expr::Root(_, kept) = &result.new_expression else {

398

            panic!("expected Root")

399

};

400

1

        assert!(kept.is_empty());

401

1

402

403

    #[test]

404

1

    fn declines_binary_attr_lift_when_relation_arity_is_not_two() {

405

1

        let mut symbols = SymbolTable::new();

406

1

        let r = DeclarationPtr::new_find(

407

1

            Name::user("r"),

408

1

            Domain::relation(

409

1

                RelAttr::<Int>::default(),

410

1

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

411

1

),

412

1

);

413

1

        symbols.insert(r.clone()).expect("insert r");

414

415

1

        let tree = root(vec![attr_expr(ref_expr(&r), "reflexive", None)]);

416

1

        let err = rule().apply(&tree, &symbols).unwrap_err();

417

1

        assert!(matches!(err, ApplicationError::RuleNotApplicable));

418

1

419