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, RuleEffect, register_rule},

12

};

13

14

use ApplicationError::RuleNotApplicable;

15

16

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

17

type VisitingStack = Vec<Name>;

18

19

/// Rewrites variables in domains.

20

///

21

/// 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.

22

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

23

1601843

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

24

1601843

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

25

5406

        return Err(RuleNotApplicable);

26

};

27

28

    // Fast path: models whose finds are already ground never need widening, and this rule is

29

    // attempted at the root after every rewrite, so keep the symbol-table scan behind a cheap

30

    // test.

31

1596437

    if !symbols_need_domain_widening(symbols) {

32

1594402

        return Err(RuleNotApplicable);

33

2035

34

35

2035

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

36

2035

    let mut domain_guards = Vec::new();

37

2035

    let mut declaration_updates = Vec::new();

38

39

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

40

2035

    let declarations: Vec<_> = symbols

41

2035

        .clone()

42

2035

        .into_iter_local()

43

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

44

        .collect();

45

46

2035

    for decl in declarations {

47

17013

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

48

4

            continue;

49

};

50

51

17009

        if let Some(bounds) =

52

17009

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

53

54

5669

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

55

11340

56

57

17009

        if domain.resolve().is_ok() {

58

14467

            continue;

59

2542

60

61

        let Some(widened_domain) =

62

2542

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

63

        else {

64

            return Err(RuleNotApplicable);

65

};

66

67

2542

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

68

            return Err(RuleNotApplicable);

69

};

70

71

2542

        domain_guards.extend(guards);

72

2542

        let updated_kind = if decl.is_find_auxiliary() {

73

511

            DeclarationKind::FindAuxiliary(DecisionVariable::new(widened_domain))

74

        } else {

75

2031

            DeclarationKind::Find(DecisionVariable::new(widened_domain))

76

};

77

2542

        declaration_updates.push((decl, updated_kind));

78

79

80

2035

    if declaration_updates.is_empty() {

81

4

        return Err(RuleNotApplicable);

82

2031

83

84

2031

Ok(

85

2031

        RuleEffect::new(expr.clone(), domain_guards, SymbolTable::new())

86

2031

            .with_declaration_updates(declaration_updates),

87

2031

88

1601843

89

90

/// Returns true iff some local declaration still has a non-ground domain.

91

///

92

/// Only unresolved domains can need widening / consistency guards. Ground integer finds must not

93

/// trigger the expensive symbol-table scan in [`handle_variables_in_domains`].

94

1596439

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

95

785486755

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

96

785486755

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

97

            // `Domain::Unresolved` only means "not yet resolved", not "unresolvable": a domain

98

            // written against a `letting` is unresolved but resolves fine. Widening is needed only

99

            // when resolution actually fails, which is the condition the body acts on below.

100

            // Testing that here keeps the O(declarations) pass off every Root attempt in models

101

            // that merely name a domain letting.

102

785486755

            matches!(domain.as_ref(), Domain::Unresolved(_)) && domain.resolve().is_err()

103

785486755

})

104

785486755

})

105

1596439

106

107

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

108

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

109

5580

fn resolve_or_widen_int_domain(

110

5580

    domain: &DomainPtr,

111

5580

    symbols: &SymbolTable,

112

5580

    known_int_bounds: &mut IntBoundsCache,

113

5580

    visiting: &mut VisitingStack,

114

5580

) -> Option<DomainPtr> {

115

5580

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

116

3038

        return Some(resolved.into());

117

2542

118

119

2542

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

120

2542

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

121

2542

        .iter()

122

3053

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

123

3053

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

124

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

125

126

2542

    Some(Domain::int_ground(widened_ranges))

127

5580

128

129

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

130

20047

fn int_domain_bounds_from_domain(

131

20047

    domain: &DomainPtr,

132

20047

    symbols: &SymbolTable,

133

20047

    known_int_bounds: &mut IntBoundsCache,

134

20047

    visiting: &mut VisitingStack,

135

20047

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

136

20047

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

137

8707

    let mut lower = i32::MAX;

138

8707

    let mut upper = i32::MIN;

139

140

8707

    for range in ranges {

141

10268

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

142

10268

        lower = lower.min(lo);

143

10268

        upper = upper.max(hi);

144

145

146

8707

    Some((lower, upper))

147

20047

148

149

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

150

13321

fn int_range_bounds(

151

13321

    range: &Range<IntVal>,

152

13321

    symbols: &SymbolTable,

153

13321

    known_int_bounds: &mut IntBoundsCache,

154

13321

    visiting: &mut VisitingStack,

155

13321

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

156

13321

    match range {

157

994

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

158

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

159

12327

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

160

12327

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

161

12327

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

162

163

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

164

165

13321

166

167

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

168

25648

fn int_val_bounds(

169

25648

    value: &IntVal,

170

25648

    symbols: &SymbolTable,

171

25648

    known_int_bounds: &mut IntBoundsCache,

172

25648

    visiting: &mut VisitingStack,

173

25648

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

174

25648

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

175

18520

        return Some((v, v));

176

7128

177

178

7128

    match value {

179

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

180

        IntVal::Reference(reference) => {

181

4090

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

182

4090

            int_bounds_for_name(&name, symbols, known_int_bounds, visiting)

183

184

        IntVal::Expr(expr) => {

185

3038

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

186

3038

            int_domain_bounds_from_domain(&domain, symbols, known_int_bounds, visiting)

187

188

189

25648

190

191

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

192

4090

fn int_bounds_for_name(

193

4090

    name: &Name,

194

4090

    symbols: &SymbolTable,

195

4090

    known_int_bounds: &mut IntBoundsCache,

196

4090

    visiting: &mut VisitingStack,

197

4090

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

198

4090

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

199

4090

        return Some(bounds);

200

201

202

    if visiting.contains(name) {

203

        return None;

204

205

206

    visiting.push(name.clone());

207

    let maybe_bounds = symbols

208

        .lookup(name)

209

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

210

        .and_then(|domain| {

211

            int_domain_bounds_from_domain(&domain, symbols, known_int_bounds, visiting)

212

});

213

    visiting.pop();

214

    let bounds = maybe_bounds?;

215

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

216

    Some(bounds)

217

4090

218

219

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

220

3038

fn expression_int_bounds(

221

3038

    expr: &Moo<Expr>,

222

3038

    symbols: &SymbolTable,

223

3038

    known_int_bounds: &mut IntBoundsCache,

224

3038

    visiting: &mut VisitingStack,

225

3038

) -> Option<DomainPtr> {

226

3038

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

227

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

228

3038

229

230

3038

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

231

3038

    resolve_or_widen_int_domain(&domain, symbols, known_int_bounds, visiting)

232

3038

233

234

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

235

2542

fn domain_consistency_constraints(

236

2542

    declaration: &conjure_cp::ast::DeclarationPtr,

237

2542

    original_domain: &DomainPtr,

238

2542

) -> Option<Vec<Expr>> {

239

2542

    if original_domain.resolve().is_ok() {

240

        return Some(Vec::new());

241

2542

242

243

2542

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

244

2542

    if ranges.is_empty() {

245

        return None;

246

2542

247

248

2542

    let var_expr = Expr::Atomic(

249

2542

        Metadata::new(),

250

2542

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

251

2542

);

252

2542

    let mut allowed_intervals = Vec::new();

253

254

    let make_expr =

255

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

256

257

2542

    for range in ranges {

258

3053

        let interval = match range {

259

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

260

                Metadata::new(),

261

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

262

                Moo::new(make_expr(v)),

263

),

264

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

265

3053

                let geq = Expr::Geq(

266

3053

                    Metadata::new(),

267

3053

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

268

3053

                    Moo::new(make_expr(l)),

269

3053

);

270

3053

                let leq = Expr::Leq(

271

3053

                    Metadata::new(),

272

3053

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

273

3053

                    Moo::new(make_expr(r)),

274

3053

);

275

3053

                Expr::And(

276

3053

                    Metadata::new(),

277

3053

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

278

3053

279

280

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

281

};

282

3053

        allowed_intervals.push(interval);

283

284

285

2542

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

286

2031

        allowed_intervals.remove(0)

287

    } else {

288

511

        Expr::Or(

289

511

            Metadata::new(),

290

511

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

291

511

292

};

293

294

2542

    Some(vec![guard])

295

2542

296

297

#[cfg(test)]

298

mod tests {

299

    use super::*;

300

    use conjure_cp::ast::{DeclarationPtr, Expression};

301

    use conjure_cp::rule_engine::{ApplicationError, get_rule_by_name};

302

303

    /// Builds a Root expression with no constraints (domain widening only looks at symbols).

304

2

    fn empty_root() -> Expression {

305

2

        Expression::Root(Metadata::new(), vec![])

306

2

307

308

    #[test]

309

1

    fn symbols_need_domain_widening_false_for_ground_int_finds() {

310

1

        let mut symbols = SymbolTable::new();

311

1

        let x = DeclarationPtr::new_find(Name::user("x"), Domain::int(vec![Range::Bounded(1, 3)]));

312

1

        symbols.insert(x).expect("insert x");

313

1

        assert!(!symbols_need_domain_widening(&symbols));

314

1

315

316

    #[test]

317

1

    fn symbols_need_domain_widening_true_for_unresolved_int_find() {

318

1

        let mut symbols = SymbolTable::new();

319

1

        let x = DeclarationPtr::new_find(Name::user("x"), Domain::int(vec![Range::Bounded(1, 3)]));

320

1

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

321

1

        let y_domain = Domain::int(vec![Range::Bounded(

322

1

            IntVal::Const(1),

323

1

            IntVal::Reference(Reference::new(x)),

324

1

        )]);

325

1

        let y = DeclarationPtr::new_find(Name::user("y"), y_domain);

326

1

        symbols.insert(y).expect("insert y");

327

1

        assert!(symbols_need_domain_widening(&symbols));

328

1

329

330

    #[test]

331

1

    fn handle_variables_in_domains_skips_ground_only_models() {

332

1

        let mut symbols = SymbolTable::new();

333

1

        let x = DeclarationPtr::new_find(Name::user("x"), Domain::int(vec![Range::Bounded(1, 3)]));

334

1

        symbols.insert(x).expect("insert x");

335

1

        let rule = get_rule_by_name("handle_variables_in_domains").expect("rule registered");

336

1

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

337

1

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

338

1

339

340

    #[test]

341

1

    fn handle_variables_in_domains_widens_unresolved_int_find() {

342

1

        let mut symbols = SymbolTable::new();

343

1

        let x = DeclarationPtr::new_find(Name::user("x"), Domain::int(vec![Range::Bounded(1, 3)]));

344

1

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

345

1

        let y_domain = Domain::int(vec![Range::Bounded(

346

1

            IntVal::Const(1),

347

1

            IntVal::Reference(Reference::new(x)),

348

1

        )]);

349

1

        let y = DeclarationPtr::new_find(Name::user("y"), y_domain);

350

1

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

351

352

1

        let rule = get_rule_by_name("handle_variables_in_domains").expect("rule registered");

353

1

        let result = rule.apply(&empty_root(), &symbols).expect("should widen y");

354

1

        let updated: Vec<_> = result.updated_declaration_names().collect();

355

1

        assert!(

356

1

            updated.contains(&Name::user("y")),

357

            "expected declaration update for unresolved find y, got {updated:?}"

358

);

359

1

        assert!(

360

1

            !result.new_top.is_empty(),

361

            "expected consistency guards for widened domain"

362

);

363

1

364