Grcov report - attribute_as_constraint

1

//! Expands any `AttributeAsConstraint` node that [`crate::passes::attribute_as_constraint`]

2

//! could not lift into its target's declaration domain, into an equivalent formula built from

3

//! ordinary operators. Mirrors Conjure's `mkAttributeToConstraint` (`Language/EvaluateOp.hs`),

4

//! which produces the same formula the lifting path would have merged, for exactly the same

5

//! reason: a bare `attr(x)`/`attr(x, val)` predicate can appear anywhere a bool expression can,

6

//! not only as a bare top-level constraint.

7

//!

8

//! Coverage is narrower than Conjure's own dispatch table in one respect: `size`/`minSize`/

9

//! `maxSize`/`minOccur`/`maxOccur` expand via [`Expression::Card`], and binary relation attributes

10

//! expand via the same [`binary_relation_constraints`] helper every relation representation's own

11

//! structural constraints already share -- both routes only work because `Card` and `In` already

12

//! have rules for every relevant representation (Set, MSet, Relation). Function jectivity/

13

//! totality and MSet's per-element occurrence bound have no such representation-independent

14

//! realisation in this codebase (`Image`/`Defined` have no rules for any function representation,

15

//! and there is no generic "count of x in mset" operator), so those combinations are only usable

16

//! via the lifting path; if lifting declines them too (e.g. because the target isn't a bare

17

//! top-level reference), the model fails to translate rather than being silently wrong.

18

19

use conjure_cp::{

20

    ast::{

21

        Atom, BinaryAttr, Domain, DomainPtr, Expression as Expr, GroundDomain, Literal as Lit,

22

        Metadata, Moo, UnresolvedDomain,

23

},

24

    into_matrix_expr,

25

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

26

};

27

28

use crate::types::relation::binary_attrs::{binary_relation_constraints, tuple2};

29

30

use ApplicationError::RuleNotApplicable;

31

32

enum SizeCmp {

33

Eq,

34

    Geq,

35

    Leq,

36

37

38

6

fn size_cmp(attr_name: &str) -> Option<SizeCmp> {

39

6

    match attr_name {

40

1

        "size" => Some(SizeCmp::Eq),

41

1

        "minSize" | "minOccur" => Some(SizeCmp::Geq),

42

1

        "maxSize" | "maxOccur" => Some(SizeCmp::Leq),

43

3

        _ => None,

44

45

6

46

47

/// Expands one un-lifted `AttributeAsConstraint` node in place.

48

#[register_rule("Base", 9800, [AttributeAsConstraint])]

49

5640

fn expand_attribute_as_constraint(

50

5640

    expr: &Expr,

51

5640

    _symbols: &conjure_cp::ast::SymbolTable,

52

5640

) -> ApplicationResult {

53

5640

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

54

5634

        return Err(RuleNotApplicable);

55

};

56

6

    let attr_name = attr.as_str();

57

58

6

    if let Some(cmp) = size_cmp(attr_name) {

59

3

        let value_expr = value.clone().ok_or(RuleNotApplicable)?;

60

3

        let card = Moo::new(Expr::Card(Metadata::new(), target.clone()));

61

3

        let formula = match cmp {

62

1

            SizeCmp::Eq => Expr::Eq(Metadata::new(), card, value_expr),

63

1

            SizeCmp::Geq => Expr::Geq(Metadata::new(), card, value_expr),

64

1

            SizeCmp::Leq => Expr::Leq(Metadata::new(), card, value_expr),

65

};

66

3

        return Ok(RuleEffect::pure(formula));

67

3

68

69

3

    if let Some(bin_attr) = BinaryAttr::from_keyword(attr_name) {

70

2

        let domain = target.as_ref().domain_of().ok_or(RuleNotApplicable)?;

71

2

        let col_domain = binary_relation_column_domain(&domain).ok_or(RuleNotApplicable)?;

72

1

        let target = target.clone();

73

1

        let member = move |x: &Expr, y: &Expr| {

74

1

            Expr::In(Metadata::new(), Moo::new(tuple2(x, y)), target.clone())

75

1

};

76

77

        let constraints =

78

1

            binary_relation_constraints(&col_domain, std::slice::from_ref(&bin_attr), &member);

79

1

        let formula = match constraints.len() {

80

            0 => Expr::Atomic(Metadata::new(), Atom::Literal(Lit::Bool(true))),

81

1

            1 => constraints.into_iter().next().expect("checked len == 1"),

82

            _ => Expr::And(Metadata::new(), Moo::new(into_matrix_expr!(constraints))),

83

};

84

1

        return Ok(RuleEffect::pure(formula));

85

1

86

87

1

    Err(RuleNotApplicable)

88

5640

89

90

/// Returns the shared column domain of a binary (arity-2, equal-column) relation domain, or

91

/// `None` if `domain` isn't shaped like one -- binary relation attributes are only ever validated

92

/// (by Conjure and this campaign alike) on relations whose two columns share a domain.

93

2

fn binary_relation_column_domain(domain: &DomainPtr) -> Option<DomainPtr> {

94

2

    match domain.as_ref() {

95

2

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

96

2

            GroundDomain::Relation(_, inners) if inners.len() == 2 && inners[0] == inners[1] => {

97

1

                Some(Moo::new(Domain::Ground(inners[0].clone())))

98

99

1

            _ => None,

100

},

101

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

102

            UnresolvedDomain::Relation(_, inners)

103

                if inners.len() == 2 && inners[0] == inners[1] =>

104

105

                Some(inners[0].clone())

106

107

            _ => None,

108

},

109

110

2

111

112

#[cfg(test)]

113

mod tests {

114

    use super::*;

115

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

116

    use conjure_cp::rule_engine::get_rule_by_name;

117

    use conjure_cp::{domain_int, range};

118

    use ustr::Ustr;

119

120

6

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

121

6

        Expr::AttributeAsConstraint(

122

6

            Metadata::new(),

123

6

            Moo::new(target),

124

6

            Ustr::from(attr),

125

6

            value.map(Moo::new),

126

6

127

6

128

129

6

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

130

6

        Expr::Atomic(

131

6

            Metadata::new(),

132

6

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

133

6

134

6

135

136

3

    fn int_lit(v: i32) -> Expr {

137

3

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

138

3

139

140

6

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

141

6

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

142

6

143

144

    #[test]

145

1

    fn expands_size_into_a_card_equality() {

146

1

        let mut symbols = SymbolTable::new();

147

1

        let s = DeclarationPtr::new_find(

148

1

            Name::user("s"),

149

1

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

150

1

);

151

1

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

152

153

1

        let expr = attr_expr(ref_expr(&s), "size", Some(int_lit(3)));

154

1

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

155

1

        assert!(matches!(result.new_expression, Expr::Eq(_, _, _)));

156

1

157

158

    #[test]

159

1

    fn expands_minsize_into_a_card_geq_and_maxsize_into_a_card_leq() {

160

1

        let mut symbols = SymbolTable::new();

161

1

        let s = DeclarationPtr::new_find(

162

1

            Name::user("s"),

163

1

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

164

1

);

165

1

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

166

167

1

        let min_result = rule()

168

1

            .apply(

169

1

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

170

1

                &symbols,

171

1

172

1

            .expect("should expand minSize");

173

1

        assert!(matches!(min_result.new_expression, Expr::Geq(_, _, _)));

174

175

1

        let max_result = rule()

176

1

            .apply(

177

1

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

178

1

                &symbols,

179

1

180

1

            .expect("should expand maxSize");

181

1

        assert!(matches!(max_result.new_expression, Expr::Leq(_, _, _)));

182

1

183

184

    #[test]

185

1

    fn expands_reflexive_into_a_quantified_formula() {

186

1

        let mut symbols = SymbolTable::new();

187

1

        let r = DeclarationPtr::new_find(

188

1

            Name::user("r"),

189

1

            Domain::relation(

190

1

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

191

1

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

192

1

),

193

1

);

194

1

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

195

196

1

        let expr = attr_expr(ref_expr(&r), "reflexive", None);

197

1

        let result = rule()

198

1

            .apply(&expr, &symbols)

199

1

            .expect("should expand reflexive");

200

1

        assert!(matches!(result.new_expression, Expr::And(_, _)));

201

1

202

203

    #[test]

204

1

    fn declines_binary_attr_expansion_when_relation_arity_is_not_two() {

205

1

        let mut symbols = SymbolTable::new();

206

1

        let r = DeclarationPtr::new_find(

207

1

            Name::user("r"),

208

1

            Domain::relation(

209

1

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

210

1

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

211

1

),

212

1

);

213

1

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

214

215

1

        let expr = attr_expr(ref_expr(&r), "reflexive", None);

216

1

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

217

1

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

218

1

219

220

    #[test]

221

1

    fn declines_when_no_expansion_route_exists() {

222

1

        let mut symbols = SymbolTable::new();

223

1

        let f = DeclarationPtr::new_find(

224

1

            Name::user("f"),

225

1

            conjure_cp::ast::Domain::function(

226

1

                conjure_cp::ast::FuncAttr::<i32>::default(),

227

1

                domain_int!(1..3),

228

1

                domain_int!(1..3),

229

1

),

230

1

);

231

1

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

232

233

1

        let expr = attr_expr(ref_expr(&f), "injective", None);

234

1

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

235

1

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

236

1

237