Grcov report - select_representation.rs

1

use conjure_cp::{

2

    ast::{Atom, Expression as Expr, GroundDomain, Metadata, Name, SymbolTable, serde::HasId},

3

    bug,

4

    representation::Representation,

5

    rule_engine::{

6

        ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,

7

        register_rule_set,

8

},

9

    settings::SolverFamily,

10

};

11

use itertools::Itertools;

12

use std::sync::Arc;

13

use std::sync::atomic::AtomicBool;

14

use std::sync::atomic::Ordering;

15

use uniplate::Biplate;

16

17

#[cfg(feature = "smt")]

18

use conjure_cp::solver::adaptors::smt::{MatrixTheory, TheoryConfig};

19

20

register_rule_set!("Representations", ("Base"), |f: &SolverFamily| {

21

    #[cfg(feature = "smt")]

22

4845

    if matches!(

23

405

f,

24

        SolverFamily::Smt(TheoryConfig {

25

            matrices: MatrixTheory::Atomic,

26

..

27

})

28

) {

29

        return true;

30

4845

31

4845

    matches!(f, SolverFamily::Sat(_) | SolverFamily::Minion)

32

4845

});

33

34

// special case rule to select representations for matrices in one go.

35

//

36

// we know that they only have one possible representation, so this rule adds a representation for all matrices in the model.

37

#[register_rule(("Representations", 8001))]

38

707283

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

39

707283

    let Expr::Root(_, _) = expr else {

40

678918

        return Err(RuleNotApplicable);

41

};

42

43

    // cannot create representations on non-local variables, so use lookup_local.

44

718155

    let matrix_vars = symbols.clone().into_iter_local().filter_map(|(n, decl)| {

45

718155

        let id = decl.id();

46

718155

        let var = decl.as_find()?.clone();

47

711261

        let resolved_domain = var.domain.resolve()?;

48

49

711261

        let GroundDomain::Matrix(valdom, indexdoms) = resolved_domain.as_ref() else {

50

673974

            return None;

51

};

52

53

        // TODO: loosen these requirements once we are able to

54

37287

        if !matches!(valdom.as_ref(), GroundDomain::Bool | GroundDomain::Int(_)) {

55

            return None;

56

37287

57

58

37287

        if indexdoms

59

37287

            .iter()

60

57996

            .any(|x| !matches!(x.as_ref(), GroundDomain::Bool | GroundDomain::Int(_)))

61

62

            return None;

63

37287

64

65

37287

        Some((n, id))

66

718155

});

67

68

28365

    let mut symbols = symbols.clone();

69

28365

    let mut expr = expr.clone();

70

28365

    let has_changed = Arc::new(AtomicBool::new(false));

71

37317

    for (name, _id) in matrix_vars {

72

        // Even if we have no references to this matrix, still give it the matrix_to_atom

73

        // representation, as we still currently need to give it to minion even if its unused.

74

//

75

        // If this var has no represnetation yet, the below call to get_or_add will modify the

76

        // symbol table by adding the representation and represented variable declarations to the

77

        // symbol table.

78

37287

        if symbols.representations_for(&name).unwrap().is_empty() {

79

1161

            has_changed.store(true, Ordering::Relaxed);

80

36126

81

82

        // (creates the represented variables as a side effect)

83

37287

        let _ = symbols

84

37287

            .get_or_add_representation(&name, &["matrix_to_atom"])

85

37287

            .unwrap();

86

87

37287

        let old_name = name.clone();

88

37287

        let new_name =

89

37287

            Name::WithRepresentation(Box::new(old_name.clone()), vec!["matrix_to_atom".into()]);

90

        // give all references to this matrix this representation

91

        // also do this inside subscopes, as long as they dont define their own variable that shadows this

92

        // one.

93

94

37287

        let old_name_2 = old_name.clone();

95

37287

        let new_name_2 = new_name.clone();

96

37287

        let has_changed_ptr = Arc::clone(&has_changed);

97

747099

        expr = expr.transform_bi(&move |n: Name| {

98

747099

            if n == old_name_2 {

99

2808

                has_changed_ptr.store(true, Ordering::SeqCst);

100

2808

                new_name_2.clone()

101

            } else {

102

744291

103

104

747099

});

105

106

107

28365

    if has_changed.load(Ordering::Relaxed) {

108

1233

        Ok(Reduction::with_symbols(expr, symbols))

109

    } else {

110

27132

        Err(RuleNotApplicable)

111

112

707283

113

114

#[register_rule(("Representations", 8000))]

115

704961

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

116

    // thing we are representing must be a reference

117

333090

    let Expr::Atomic(_, Atom::Reference(decl)) = expr else {

118

476283

        return Err(RuleNotApplicable);

119

};

120

121

228678

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

122

123

    // thing we are representing must be a variable

124

125

228678

        let guard = decl.ptr().as_find().ok_or(RuleNotApplicable)?;

126

228678

        drop(guard);

127

128

129

228678

    if !needs_representation(&name, symbols) {

130

227742

        return Err(RuleNotApplicable);

131

936

132

133

936

    let mut symbols = symbols.clone();

134

117

    let representation =

135

936

        get_or_create_representation(&name, &mut symbols).ok_or(RuleNotApplicable)?;

136

137

117

    let representation_names = representation

138

117

        .into_iter()

139

117

        .map(|x| x.repr_name().into())

140

117

        .collect_vec();

141

142

117

    let new_name = Name::WithRepresentation(Box::new(name.clone()), representation_names);

143

144

    // HACK: this is suspicious, but hopefully will work until we clean up representations

145

    // properly...

146

//

147

    // In general, we should not use names atall anymore, including for representations /

148

    // represented variables.

149

//

150

    // * instead of storing the link from a variable that has a representation to the variable it

151

    // is representing in the name as WithRepresentation, we should use declaration pointers instead.

152

//

153

//

154

    // see: issue #932

155

117

    let mut decl_ptr = decl.clone().into_ptr().detach();

156

117

    decl_ptr.replace_name(new_name);

157

158

117

    Ok(Reduction::with_symbols(

159

117

        Expr::Atomic(

160

117

            Metadata::new(),

161

117

            Atom::Reference(conjure_cp::ast::Reference::new(decl_ptr)),

162

117

),

163

117

        symbols,

164

117

))

165

704961

166

167

/// Returns whether `name` needs representing.

168

///

169

/// # Panics

170

///

171

///   + If `name` is not in `symbols`.

172

228678

fn needs_representation(name: &Name, symbols: &SymbolTable) -> bool {

173

    // if name already has a representation, false

174

228678

    if let Name::Represented(_) = name {

175

118827

        return false;

176

109851

177

    // might be more logic here in the future?

178

109851

    domain_needs_representation(&symbols.resolve_domain(name).unwrap())

179

228678

180

181

/// Returns whether `domain` needs representing.

182

111723

fn domain_needs_representation(domain: &GroundDomain) -> bool {

183

    // very simple implementation for nows

184

111723

    match domain {

185

78036

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

186

32751

        GroundDomain::Matrix(_, _) => false, // we special case these elsewhere

187

        GroundDomain::Set(_, _)

188

        | GroundDomain::MSet(_, _)

189

        | GroundDomain::Tuple(_)

190

        | GroundDomain::Record(_)

191

936

        | GroundDomain::Function(_, _, _) => true,

192

        GroundDomain::Empty(_) => false,

193

194

111723

195

196

/// Returns representations for `name`, creating them if they don't exist.

197

///

198

///

199

/// Returns None if there is no valid representation for `name`.

200

///

201

/// # Panics

202

///

203

///   + If `name` is not in `symbols`.

204

312

fn get_or_create_representation(

205

312

    name: &Name,

206

312

    symbols: &mut SymbolTable,

207

312

) -> Option<Vec<Box<dyn Representation>>> {

208

    // TODO: pick representations recursively for nested abstract domains: e.g. sets in sets.

209

210

312

    let dom = symbols.resolve_domain(name).unwrap();

211

312

    match dom.as_ref() {

212

        GroundDomain::Set(_, _) => None, // has no representations yet!

213

144

        GroundDomain::Tuple(elem_domains) => {

214

144

            if elem_domains

215

144

                .iter()

216

288

                .any(|d| domain_needs_representation(d.as_ref()))

217

218

                bug!("representing nested abstract domains is not implemented");

219

144

220

221

144

            symbols.get_or_add_representation(name, &["tuple_to_atom"])

222

223

168

        GroundDomain::Record(entries) => {

224

168

            if entries

225

168

                .iter()

226

336

                .any(|entry| domain_needs_representation(&entry.domain))

227

228

                bug!("representing nested abstract domains is not implemented");

229

168

230

231

168

            symbols.get_or_add_representation(name, &["record_to_atom"])

232

233

        _ => unreachable!("non abstract domains should never need representations"),

234

235

312