Grcov report - variables_in

1

//! Rules for variables in domains.

2

3

use std::collections::HashMap;

4

5

use conjure_cp::{

6

    ast::{

7

        Atom, DecisionVariable, DeclarationKind, Domain, DomainPtr, Expression as Expr, HasDomain,

8

        IntVal, Literal as Lit, Metadata, Moo, Name, Range, Reference, SymbolTable,

9

},

10

    bug,

11

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

12

};

13

use uniplate::Biplate;

14

15

use ApplicationError::RuleNotApplicable;

16

17

type IntBoundsCache = HashMap<Name, (i32, i32)>;

18

type VisitingStack = Vec<Name>;

19

20

/// Rewrites variables in domains.

21

///

22

/// Solvers require variable declarations to have ground domains. For integer domains that contain variables in them, we widen to a finite ground superset-domain and add constraints that enforce membership in the original (possibly variable-dependent) domain.

23

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

24

2514045

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

25

2514045

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

26

2450361

        return Err(RuleNotApplicable);

27

};

28

29

63684

    if !symbols_have_decision_variable_references(symbols) {

30

10906

        return Err(RuleNotApplicable);

31

52778

32

33

52778

    let mut known_int_bounds: IntBoundsCache = HashMap::new();

34

52778

    let mut domain_guards = Vec::new();

35

52778

    let mut changed = false;

36

37

    // Collect declarations first to avoid iterator invalidation while mutating declarations.

38

52778

    let declarations: Vec<_> = symbols

39

52778

        .clone()

40

52778

        .into_iter_local()

41

52778

        .map(|(_, decl)| decl)

42

52778

        .collect();

43

44

5596831

    for mut decl in declarations {

45

5596831

        let Some(domain) = decl.as_find().map(|var| var.domain_of()) else {

46

30606

            continue;

47

};

48

49

483618

        if let Some(bounds) =

50

5566225

            int_domain_bounds_from_domain(&domain, symbols, &mut known_int_bounds, &mut Vec::new())

51

483618

52

483618

            known_int_bounds.insert(decl.name().clone(), bounds);

53

5082607

54

55

5566225

        if domain.resolve().is_ok() {

56

5566135

            continue;

57

90

58

59

90

        let Some(widened_domain) =

60

90

            resolve_or_widen_int_domain(&domain, symbols, &mut known_int_bounds, &mut Vec::new())

61

        else {

62

            return Err(RuleNotApplicable);

63

};

64

65

90

        let Some(guards) = domain_consistency_constraints(&decl, &domain) else {

66

            return Err(RuleNotApplicable);

67

};

68

69

90

        domain_guards.extend(guards);

70

90

        let _ = decl.replace_kind(DeclarationKind::Find(DecisionVariable::new(widened_domain)));

71

90

        changed = true;

72

73

74

52778

    if !changed {

75

52700

        return Err(RuleNotApplicable);

76

78

77

78

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

79

2514045

80

81

/// Returns true iff at least one local symbol contains a reference to a decision variable.

82

63684

fn symbols_have_decision_variable_references(symbols: &SymbolTable) -> bool {

83

63684

    let is_decision_reference = |reference: &Reference| {

84

14022

        reference.ptr().as_find().is_some()

85

14022

            || symbols

86

14022

                .lookup(&reference.name().clone())

87

14022

                .is_some_and(|decl| decl.as_find().is_some())

88

14022

};

89

90

160026

    symbols.iter_local().any(|(_, declaration)| {

91

160026

        declaration.domain().is_some_and(|domain| {

92

160014

            Biplate::<Reference>::universe_bi(domain.as_ref())

93

160014

                .iter()

94

160014

                .any(&is_decision_reference)

95

160014

                || Biplate::<IntVal>::universe_bi(domain.as_ref())

96

160014

                    .iter()

97

160014

                    .any(|int_val| match int_val {

98

                        IntVal::Const(_) => false,

99

                        IntVal::Reference(reference) => is_decision_reference(reference),

100

                        IntVal::Expr(expr) => Biplate::<Atom>::universe_bi(expr.as_ref())

101

                            .iter()

102

                            .any(|atom| {

103

                                matches!(atom, Atom::Reference(reference) if is_decision_reference(reference))

104

}),

105

})

106

160026

        }) || declaration.as_find().is_some_and(|find| {

107

124834

            let domain = find.domain_of();

108

124834

            domain.resolve().is_ok() && domain.as_ref().as_int().is_some()

109

124834

})

110

160026

})

111

63684

112

113

/// Resolves an integer domain when possible; otherwise computes a finite widened domain

114

/// by replacing symbolic bounds with conservative numeric bounds.

115

294

fn resolve_or_widen_int_domain(

116

294

    domain: &DomainPtr,

117

294

    symbols: &SymbolTable,

118

294

    known_int_bounds: &mut IntBoundsCache,

119

294

    visiting: &mut VisitingStack,

120

294

) -> Option<DomainPtr> {

121

294

    if let Ok(resolved) = domain.resolve() {

122

204

        return Some(resolved.into());

123

90

124

125

90

    let ranges = domain.as_ref().as_int()?;

126

90

    let widened_ranges: Vec<Range<i32>> = ranges

127

90

        .iter()

128

102

        .map(|range| int_range_bounds(range, symbols, known_int_bounds, visiting))

129

102

        .map(|bounds| bounds.map(|(lo, hi)| Range::new(Some(lo), Some(hi))))

130

90

        .collect::<Option<Vec<_>>>()?;

131

132

90

    Some(Domain::int_ground(widened_ranges))

133

294

134

135

/// Returns overall numeric bounds for an unresolved integer domain.

136

5566429

fn int_domain_bounds_from_domain(

137

5566429

    domain: &DomainPtr,

138

5566429

    symbols: &SymbolTable,

139

5566429

    known_int_bounds: &mut IntBoundsCache,

140

5566429

    visiting: &mut VisitingStack,

141

5566429

) -> Option<(i32, i32)> {

142

5566429

    let ranges = domain.as_ref().as_int()?;

143

483822

    let mut lower = i32::MAX;

144

483822

    let mut upper = i32::MIN;

145

146

495124

    for range in ranges {

147

495124

        let (lo, hi) = int_range_bounds(&range, symbols, known_int_bounds, visiting)?;

148

495124

        lower = lower.min(lo);

149

495124

        upper = upper.max(hi);

150

151

152

483822

    Some((lower, upper))

153

5566429

154

155

/// Computes numeric bounds for a possibly symbolic integer range.

156

495226

fn int_range_bounds(

157

495226

    range: &Range<IntVal>,

158

495226

    symbols: &SymbolTable,

159

495226

    known_int_bounds: &mut IntBoundsCache,

160

495226

    visiting: &mut VisitingStack,

161

495226

) -> Option<(i32, i32)> {

162

495226

    match range {

163

19668

        Range::Single(v) => int_val_bounds(v, symbols, known_int_bounds, visiting),

164

475558

        Range::Bounded(l, r) => {

165

475558

            let (ll, lh) = int_val_bounds(l, symbols, known_int_bounds, visiting)?;

166

475558

            let (rl, rh) = int_val_bounds(r, symbols, known_int_bounds, visiting)?;

167

475558

            Some((ll.min(lh), rl.max(rh)))

168

169

        Range::Unbounded | Range::UnboundedL(_) | Range::UnboundedR(_) => None,

170

171

495226

172

173

/// Computes numeric bounds for an unresolved integer value.

174

970784

fn int_val_bounds(

175

970784

    value: &IntVal,

176

970784

    symbols: &SymbolTable,

177

970784

    known_int_bounds: &mut IntBoundsCache,

178

970784

    visiting: &mut VisitingStack,

179

970784

) -> Option<(i32, i32)> {

180

970784

    if let Ok(v) = value.resolve() {

181

970484

        return Some((v, v));

182

300

183

184

300

    match value {

185

        IntVal::Const(v) => Some((*v as i32, *v as i32)),

186

96

        IntVal::Reference(reference) => {

187

96

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

188

96

            int_bounds_for_name(&name, symbols, known_int_bounds, visiting)

189

190

204

        IntVal::Expr(expr) => {

191

204

            let domain = expression_int_bounds(expr, symbols, known_int_bounds, visiting)?;

192

204

            int_domain_bounds_from_domain(&domain, symbols, known_int_bounds, visiting)

193

194

195

970784

196

197

/// Resolves cached or derived bounds for a declaration by name.

198

96

fn int_bounds_for_name(

199

96

    name: &Name,

200

96

    symbols: &SymbolTable,

201

96

    known_int_bounds: &mut IntBoundsCache,

202

96

    visiting: &mut VisitingStack,

203

96

) -> Option<(i32, i32)> {

204

96

    if let Some(bounds) = known_int_bounds.get(name).copied() {

205

96

        return Some(bounds);

206

207

208

    if visiting.contains(name) {

209

        return None;

210

211

212

    visiting.push(name.clone());

213

    let maybe_bounds = symbols

214

        .lookup(name)

215

        .and_then(|decl| decl.domain())

216

        .and_then(|domain| {

217

            int_domain_bounds_from_domain(&domain, symbols, known_int_bounds, visiting)

218

});

219

    visiting.pop();

220

    let bounds = maybe_bounds?;

221

    known_int_bounds.insert(name.clone(), bounds);

222

    Some(bounds)

223

96

224

225

/// Computes a conservative ground integer domain for an expression.

226

204

fn expression_int_bounds(

227

204

    expr: &Moo<Expr>,

228

204

    symbols: &SymbolTable,

229

204

    known_int_bounds: &mut IntBoundsCache,

230

204

    visiting: &mut VisitingStack,

231

204

) -> Option<DomainPtr> {

232

204

    if let Some(Lit::Int(v)) = conjure_cp::ast::eval_constant(expr) {

233

        return Some(Domain::int_ground(vec![Range::Single(v)]));

234

204

235

236

204

    let domain = expr.as_ref().domain_of()?;

237

204

    resolve_or_widen_int_domain(&domain, symbols, known_int_bounds, visiting)

238

204

239

240

/// Builds guards ensuring widened integer find domains still satisfy original symbolic bounds.

241

90

fn domain_consistency_constraints(

242

90

    declaration: &conjure_cp::ast::DeclarationPtr,

243

90

    original_domain: &DomainPtr,

244

90

) -> Option<Vec<Expr>> {

245

90

    if original_domain.resolve().is_ok() {

246

        return Some(Vec::new());

247

90

248

249

90

    let ranges = original_domain.as_ref().as_int()?;

250

90

    if ranges.is_empty() {

251

        return None;

252

90

253

254

90

    let var_expr = Expr::Atomic(

255

90

        Metadata::new(),

256

90

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

257

90

);

258

90

    let mut allowed_intervals = Vec::new();

259

260

90

    let make_expr =

261

        |iv: IntVal| Expr::try_from(iv).unwrap_or_else(|e| bug!("invalid int domain range: {e}"));

262

263

102

    for range in ranges {

264

102

        let interval = match range {

265

            Range::Single(v) => Expr::Eq(

266

                Metadata::new(),

267

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

268

                Moo::new(make_expr(v)),

269

),

270

102

            Range::Bounded(l, r) => {

271

102

                let geq = Expr::Geq(

272

102

                    Metadata::new(),

273

102

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

274

102

                    Moo::new(make_expr(l)),

275

102

);

276

102

                let leq = Expr::Leq(

277

102

                    Metadata::new(),

278

102

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

279

102

                    Moo::new(make_expr(r)),

280

102

);

281

102

                Expr::And(

282

102

                    Metadata::new(),

283

102

                    Moo::new(conjure_cp::into_matrix_expr!(vec![geq, leq])),

284

102

285

286

            Range::Unbounded | Range::UnboundedL(_) | Range::UnboundedR(_) => return None,

287

};

288

102

        allowed_intervals.push(interval);

289

290

291

90

    let guard = if allowed_intervals.len() == 1 {

292

78

        allowed_intervals.remove(0)

293

    } else {

294

12

        Expr::Or(

295

12

            Metadata::new(),

296

12

            Moo::new(conjure_cp::into_matrix_expr!(allowed_intervals)),

297

12

298

};

299

300

90

    Some(vec![guard])

301

90