Grcov report - utils.rs

1

use std::collections::VecDeque;

2

3

use conjure_cp::ast::{

4

    AbstractLiteral, Atom, DeclarationPtr, Expression as Expr, Literal, Metadata, Moo, Name,

5

    SymbolTable,

6

    categories::Category,

7

    comprehension::{Comprehension, ComprehensionQualifier},

8

};

9

10

use tracing::{instrument, trace};

11

use uniplate::{Biplate, Uniplate};

12

13

/// True iff `expr` is an `Atom`.

14

72998

pub fn is_atom(expr: &Expr) -> bool {

15

72998

    matches!(expr, Expr::Atomic(_, _))

16

72998

17

18

/// True iff `expr` is an `Atom` or `Not(Atom)`.

19

8985

pub fn is_literal(expr: &Expr) -> bool {

20

8985

    match expr {

21

4851

        Expr::Atomic(_, _) => true,

22

        Expr::Not(_, inner) => matches!(**inner, Expr::Atomic(_, _)),

23

4134

        _ => false,

24

25

8985

26

27

/// True if `expr` is flat; i.e. it only contains atoms.

28

pub fn is_flat(expr: &Expr) -> bool {

29

    expr.children().iter().all(is_atom)

30

31

32

/// Rewrites the direct expression children of `expr`, preserving the number of children.

33

///

34

/// Returns the rebuilt expression and the number of children marked as changed by `rewrite`.

35

2277066

pub fn rewrite_children(

36

2277066

    expr: &Expr,

37

2277066

    mut rewrite: impl FnMut(Expr) -> (Expr, bool),

38

2277066

) -> (Expr, usize) {

39

2277066

    let mut num_changed = 0;

40

2277066

    let children: VecDeque<Expr> = expr

41

2277066

        .children()

42

2277066

        .into_iter()

43

2277066

        .map(|child| {

44

2012888

            let (new_child, changed) = rewrite(child);

45

2012888

            if changed {

46

9419

                num_changed += 1;

47

2003469

48

2012888

            new_child

49

2012888

})

50

2277066

        .collect();

51

52

2277066

    (expr.with_children(children), num_changed)

53

2277066

54

55

/// Returns the only direct `Vec<Expr>` child of `expr`, if it has exactly one.

56

392104

pub fn single_vec_child(expr: &Expr) -> Option<Vec<Expr>> {

57

392104

    let mut child_vecs: VecDeque<Vec<Expr>> = expr.children_bi();

58

392104

    if child_vecs.len() == 1 {

59

372806

        child_vecs.pop_front()

60

    } else {

61

19298

        None

62

63

392104

64

65

/// Rebuilds `expr` with a replacement for its only direct `Vec<Expr>` child.

66

1982

pub fn with_single_vec_child(expr: &Expr, child: Vec<Expr>) -> Expr {

67

1982

    expr.with_children_bi(VecDeque::from([child]))

68

1982

69

70

/// Returns the arity of a tuple constant expression, if this expression is one.

71

60

pub fn constant_tuple_len(expr: &Expr) -> Option<usize> {

72

    match expr {

73

        Expr::AbstractLiteral(_, AbstractLiteral::Tuple(elems)) => Some(elems.len()),

74

24

        Expr::Atomic(_, Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Tuple(elems)))) => {

75

24

            Some(elems.len())

76

77

36

        _ => None,

78

79

60

80

81

/// Returns record field names of a record constant expression, if this expression is one.

82

24

pub fn constant_record_names(expr: &Expr) -> Option<Vec<Name>> {

83

    match expr {

84

        Expr::AbstractLiteral(_, AbstractLiteral::Record(entries)) => {

85

            Some(entries.iter().map(|x| x.name.clone()).collect())

86

87

        Expr::Atomic(

88

_,

89

12

            Atom::Literal(Literal::AbstractLiteral(AbstractLiteral::Record(entries))),

90

24

        ) => Some(entries.iter().map(|x| x.name.clone()).collect()),

91

12

        _ => None,

92

93

24

94

95

/// True if the entire AST is constants.

96

3818091

pub fn is_all_constant(expression: &Expr) -> bool {

97

3818091

    expression

98

3818091

        .universe_bi()

99

3818091

        .into_iter()

100

4156590

        .all(|atom| matches!(atom, Atom::Literal(_)))

101

3818091

102

103

/// Converts a vector of expressions to a vector of atoms.

104

///

105

/// # Returns

106

///

107

/// `Some(Vec<Atom>)` if the vectors direct children expressions are all atomic, otherwise `None`.

108

#[allow(dead_code)]

109

pub fn expressions_to_atoms(exprs: &Vec<Expr>) -> Option<Vec<Atom>> {

110

    let mut atoms: Vec<Atom> = vec![];

111

    for expr in exprs {

112

        let Expr::Atomic(_, atom) = expr else {

113

            return None;

114

};

115

        atoms.push(atom.clone());

116

117

118

    Some(atoms)

119

120

121

/// Creates a new auxiliary variable using the given expression.

122

///

123

/// # Returns

124

///

125

/// * `None` if `Expr` is a `Atom`, or `Expr` does not have a domain (for example, if it is a `Bubble`).

126

///

127

/// * `Some(ToAuxVarOutput)` if successful, containing:

128

///

129

///     + A new symbol table, modified to include the auxiliary variable.

130

///     + A new top level expression, containing the declaration of the auxiliary variable.

131

///     + A reference to the auxiliary variable to replace the existing expression with.

132

///

133

#[instrument(skip_all, fields(expr = %expr))]

134

72998

pub fn to_aux_var(expr: &Expr, symbols: &SymbolTable) -> Option<ToAuxVarOutput> {

135

72998

    let mut symbols = symbols.clone();

136

137

    // No need to put an atom in an aux_var

138

72998

    if is_atom(expr) {

139

55640

        if cfg!(debug_assertions) {

140

55640

            trace!(why = "expression is an atom", "to_aux_var() failed");

141

142

55640

        return None;

143

17358

144

145

    // Anything that should be bubbled, bubble

146

17358

    if !expr.is_safe() {

147

536

        if cfg!(debug_assertions) {

148

536

            trace!(why = "expression is unsafe", "to_aux_var() failed");

149

150

536

        return None;

151

16822

152

153

    // Do not put abstract literals containing expressions into aux vars.

154

//

155

    // e.g. for `[1,2,3,f/2,e][e]`, the lhs should not be put in an aux var.

156

//

157

    // instead, we should flatten the elements inside this abstract literal, or wait for it to be

158

    // turned into an atom, or an abstract literal containing only literals - e.g. through an index

159

    // or slice operation.

160

//

161

16822

    if let Expr::AbstractLiteral(_, _) = expr {

162

2559

        if cfg!(debug_assertions) {

163

2559

            trace!(

164

                why = "expression is an abstract literal",

165

                "to_aux_var() failed"

166

);

167

168

2559

        return None;

169

14263

170

171

    // Only flatten an expression if it contains decision variables or decision variables with some

172

    // constants.

173

//

174

    // i.e. dont flatten things containing givens, quantified variables, just constants, etc.

175

14263

    let categories = expr.universe_categories();

176

177

14263

    assert!(!categories.is_empty());

178

179

14263

    if !(categories.len() == 1 && categories.contains(&Category::Decision)

180

10337

        || categories.len() == 2

181

10067

            && categories.contains(&Category::Decision)

182

9878

            && categories.contains(&Category::Constant))

183

184

1002

        if cfg!(debug_assertions) {

185

1002

            trace!(

186

                why = "expression has sub-expressions that are not in the decision category",

187

                "to_aux_var() failed"

188

);

189

190

1002

        return None;

191

13261

192

193

    // Avoid introducing auxvars for generic matrix indexing (can create many redundant auxvars

194

    // before comprehension expansion). However, keep list indexing eligible so Minion lowering

195

    // can introduce `element` constraints in non-equality contexts.

196

13261

    if let Expr::SafeIndex(_, subject, indices) = expr {

197

6381

        let can_lower_via_element = subject.clone().unwrap_list().is_some()

198

5985

            && indices.iter().all(|i| matches!(i, Expr::Atomic(_, _)));

199

200

6381

        if !can_lower_via_element {

201

4536

            if cfg!(debug_assertions) {

202

4536

                trace!(expr=%expr, why = "matrix indexing is not element-lowerable", "to_aux_var() failed");

203

204

4536

            return None;

205

1845

206

6880

207

208

8725

    let Some(domain) = expr.domain_of() else {

209

538

        if cfg!(debug_assertions) {

210

538

            trace!(expr=%expr, why = "could not find the domain of the expression", "to_aux_var() failed");

211

212

538

        return None;

213

};

214

215

8187

    let decl = symbols.gen_find(&domain);

216

217

8187

    if cfg!(debug_assertions) {

218

8187

        trace!(expr=%expr, "to_auxvar() succeeded in putting expr into an auxvar");

219

220

221

8187

    Some(ToAuxVarOutput {

222

8187

        aux_declaration: decl.clone(),

223

8187

        aux_expression: Expr::AuxDeclaration(

224

8187

            Metadata::new(),

225

8187

            conjure_cp::ast::Reference::new(decl),

226

8187

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

227

8187

),

228

8187

        symbols,

229

8187

        _unconstructable: (),

230

8187

})

231

72998

232

233

/// Output data of `to_aux_var`.

234

pub struct ToAuxVarOutput {

235

    aux_declaration: DeclarationPtr,

236

    aux_expression: Expr,

237

    symbols: SymbolTable,

238

    _unconstructable: (),

239

240

241

impl ToAuxVarOutput {

242

    /// Returns the new auxiliary variable as an `Atom`.

243

8187

    pub fn as_atom(&self) -> Atom {

244

8187

        Atom::Reference(conjure_cp::ast::Reference::new(

245

8187

            self.aux_declaration.clone(),

246

8187

))

247

8187

248

249

    /// Returns the new auxiliary variable as an `Expression`.

250

///

251

    /// This expression will have default `Metadata`.

252

6544

    pub fn as_expr(&self) -> Expr {

253

6544

        Expr::Atomic(Metadata::new(), self.as_atom())

254

6544

255

256

    /// Returns the top level `Expression` to add to the model.

257

8187

    pub fn top_level_expr(&self) -> Expr {

258

8187

        self.aux_expression.clone()

259

8187

260

261

    /// Returns the new `SymbolTable`, modified to contain this auxiliary variable in the symbol table.

262

8187

    pub fn symbols(&self) -> SymbolTable {

263

8187

        self.symbols.clone()

264

8187

265

266

267

/// Clone comprehension with expression generator into its own detached comprehension scope

268

/// and rewrite all uses of the original quantified declaration to a fresh branch-local

269

/// expression generator.

270

22

pub fn replace_expression_generator_source(

271

22

    comp: &Comprehension,

272

22

    gen_decl: &DeclarationPtr,

273

22

    replacement_expr: Expr,

274

22

) -> (Comprehension, DeclarationPtr) {

275

22

    let replacement_ptr =

276

22

        DeclarationPtr::new_quantified_expr(gen_decl.name().clone(), replacement_expr);

277

22

    let mut comprehension = comp.clone();

278

279

    // detach the scope so rewriting this branch does not mutate the original

280

    // comprehension through shared pointers

281

22

    comprehension.symbols = comprehension.symbols.detach();

282

283

    // rewrite all uses of the original quantified declaration to the branch-local

284

    // generator declaration

285

22

    comprehension.return_expression =

286

22

        comprehension

287

22

            .return_expression

288

98

            .transform_bi(&|decl: DeclarationPtr| {

289

98

                if decl == *gen_decl {

290

22

                    replacement_ptr.clone()

291

                } else {

292

76

                    decl

293

294

98

});

295

296

22

    comprehension.qualifiers = comprehension

297

22

        .qualifiers

298

22

        .into_iter()

299

42

        .map(|qualifier| {

300

110

            qualifier.transform_bi(&|decl: DeclarationPtr| {

301

110

                if decl == *gen_decl {

302

22

                    replacement_ptr.clone()

303

                } else {

304

88

                    decl

305

306

110

})

307

42

})

308

22

        .collect();

309

310

    // keep the detached local scope in sync with the rewritten generator

311

    // declarations used by this branch

312

22

    comprehension

313

22

        .symbols

314

22

        .write()

315

22

        .update_insert(replacement_ptr.clone());

316

42

    for qualifier in &comprehension.qualifiers {

317

42

        match qualifier {

318

34

            ComprehensionQualifier::ExpressionGenerator { ptr }

319

38

            | ComprehensionQualifier::Generator { ptr } => {

320

38

                comprehension.symbols.write().update_insert(ptr.clone());

321

38

322

4

            ComprehensionQualifier::Condition(_) => {}

323

324

325

326

22

    (comprehension, replacement_ptr)

327

22