Grcov report - random

1

use rand::Rng;

2

use rand::RngExt;

3

use rand::seq::IndexedRandom;

4

5

use crate::DataExpr;

6

use crate::DataExprBinaryOp;

7

use crate::FixedPointOperator;

8

use crate::IdDecl;

9

use crate::PbesEquation;

10

use crate::PbesExpr;

11

use crate::PbesExprBinaryOp;

12

use crate::PropVarDecl;

13

use crate::PropVarInst;

14

use crate::Quantifier;

15

use crate::Sort;

16

use crate::SortExpression;

17

use crate::Span;

18

use crate::UntypedPbes;

19

use crate::random_boolean_data_expression;

20

use crate::random_integer_data_expression;

21

22

const PRED_INTS: &[&str] = &["m", "n"];

23

const PRED_BOOLS: &[&str] = &["b", "c"];

24

const QUANT_INTS: &[&str] = &["t", "u", "v", "w"];

25

26

/// Parameters held constant throughout the random PBES generation.

27

struct PbesGenConfig<'a> {

28

    /// The predicate variables available for instantiation in leaves.

29

    predicate_vars: &'a [PredVar],

30

31

    /// Whether quantifiers may be generated.

32

    use_quantifiers: bool,

33

34

    /// Probability that a leaf is a predicate variable instantiation rather than

35

    /// a `val(...)` atom.

36

    propvar_probability: f64,

37

38

39

/// Generates a random PBES.

40

///

41

/// `atom_count` and `propvar_count` together control the expression size: their sum determines the

42

/// recursion depth, and their ratio determines how often a leaf is a predicate variable instantiation

43

/// versus a `val(...)` atom.

44

100

pub fn random_pbes<R: Rng>(

45

100

    rng: &mut R,

46

100

    equation_count: usize,

47

100

    atom_count: usize,

48

100

    propvar_count: usize,

49

100

    use_quantifiers: bool,

50

100

    use_integers: bool,

51

100

) -> UntypedPbes {

52

100

    let pred_vars: Vec<PredVar> = (0..equation_count)

53

300

        .map(|i| make_pred_var(rng, i, use_integers))

54

100

        .collect();

55

56

100

    let total = (atom_count + propvar_count).max(1);

57

100

    let propvar_prob = propvar_count as f64 / total as f64;

58

100

    let depth = total.ilog2() as usize + 1;

59

60

100

    let config = PbesGenConfig {

61

100

        predicate_vars: &pred_vars,

62

100

        use_quantifiers,

63

100

        propvar_probability: propvar_prob,

64

100

};

65

66

100

    let mut equations = Vec::new();

67

300

    for pv in &pred_vars {

68

300

        let freevars = pv.expr_freevars();

69

300

        let formula = random_pbes_expr(rng, depth, &freevars, &config, false);

70

300

        let operator = if rng.random_bool(0.5) {

71

158

            FixedPointOperator::Least

72

        } else {

73

142

            FixedPointOperator::Greatest

74

};

75

300

        equations.push(PbesEquation::new(operator, pv.to_decl(), formula));

76

77

78

100

    let first = &pred_vars[0];

79

100

    let init_args: Vec<DataExpr> = first

80

100

        .params

81

100

        .iter()

82

100

        .map(|p| {

83

96

            if is_bool_var(p) {

84

63

                DataExpr::Bool(true)

85

            } else {

86

33

                DataExpr::Number("0".to_string())

87

88

96

})

89

100

        .collect();

90

100

    let init = PropVarInst::new(first.name.clone(), init_args);

91

92

100

    UntypedPbes {

93

100

        data_specification: Default::default(),

94

100

        global_variables: Vec::new(),

95

100

        equations,

96

100

        init,

97

100

98

100

99

100

2428

fn random_leaf<R: Rng>(rng: &mut R, freevars: &[IdDecl], config: &PbesGenConfig, negated: bool) -> PbesExpr {

101

2428

    if !config.predicate_vars.is_empty() && rng.random_bool(config.propvar_probability) {

102

1234

        let pv = config.predicate_vars.choose(rng).unwrap();

103

1234

        let args = pv

104

1234

            .params

105

1234

            .iter()

106

1234

            .map(|p| {

107

1134

                if is_bool_var(p) {

108

827

                    random_boolean_data_expression(rng, freevars)

109

                } else {

110

307

                    random_integer_data_expression(rng, freevars)

111

112

1134

})

113

1234

            .collect();

114

1234

        let inst = PropVarInst::new(pv.name.clone(), args);

115

1234

        if negated {

116

623

            PbesExpr::Negation(Box::new(PbesExpr::PropVarInst(inst)))

117

        } else {

118

611

            PbesExpr::PropVarInst(inst)

119

120

    } else {

121

1194

        PbesExpr::DataValExpr(random_boolean_data_expression(rng, freevars))

122

123

2428

124

125

/// Generates a random PBES expression with the given parameters.

126

///

127

/// `depth` controls the maximum depth of the generated expression, and

128

/// `propvar_probability` controls how likely a leaf is to be a predicate variable

129

/// instantiation versus a `val(...)` atom.  If `use_quantifiers` is false, no

130

/// quantifiers will be generated.  If `negated` is true, the top-level polarity

131

/// is negative, which biases the generator to produce more negations and

132

/// implications, which flip polarity.

133

5547

fn random_pbes_expr<R: Rng>(

134

5547

    rng: &mut R,

135

5547

    depth: usize,

136

5547

    freevars: &[IdDecl],

137

5547

    config: &PbesGenConfig,

138

5547

    negated: bool,

139

5547

) -> PbesExpr {

140

5547

    if depth == 0 {

141

2428

        return random_leaf(rng, freevars, config, negated);

142

3119

143

144

    // Binary operators are over-represented to bias toward non-trivial trees.

145

3119

    let op_table: &[u8] = if config.use_quantifiers {

146

1478

        &[0, 1, 2, 3, 0, 1, 2, 3, 4, 5]

147

    } else {

148

1641

        &[0, 1, 2, 3]

149

};

150

3119

    let op = *op_table.choose(rng).unwrap();

151

152

3119

    match op {

153

        0 => {

154

707

            let inner = random_pbes_expr(rng, depth - 1, freevars, config, !negated);

155

707

            PbesExpr::Negation(Box::new(inner))

156

157

        1 => {

158

691

            let l = random_pbes_expr(rng, depth - 1, freevars, config, negated);

159

691

            let r = random_pbes_expr(rng, depth - 1, freevars, config, negated);

160

691

            PbesExpr::Binary {

161

691

                op: PbesExprBinaryOp::Conjunction,

162

691

                lhs: Box::new(l),

163

691

                rhs: Box::new(r),

164

691

165

166

        2 => {

167

684

            let l = random_pbes_expr(rng, depth - 1, freevars, config, negated);

168

684

            let r = random_pbes_expr(rng, depth - 1, freevars, config, negated);

169

684

            PbesExpr::Binary {

170

684

                op: PbesExprBinaryOp::Disjunction,

171

684

                lhs: Box::new(l),

172

684

                rhs: Box::new(r),

173

684

174

175

        3 => {

176

            // Antecedent flips polarity for monotonicity.

177

753

            let l = random_pbes_expr(rng, depth - 1, freevars, config, !negated);

178

753

            let r = random_pbes_expr(rng, depth - 1, freevars, config, negated);

179

753

            PbesExpr::Binary {

180

753

                op: PbesExprBinaryOp::Implies,

181

753

                lhs: Box::new(l),

182

753

                rhs: Box::new(r),

183

753

184

185

128

        4 => random_quantifier(rng, Quantifier::Forall, depth - 1, freevars, config, negated),

186

156

        5 => random_quantifier(rng, Quantifier::Exists, depth - 1, freevars, config, negated),

187

        _ => unreachable!(),

188

189

5547

190

191

/// Generates a random quantifier expression.  The quantifier variable is always

192

/// of type Nat and is artificially bounded (e.g. `forall t. t < 3 => body`) to

193

/// ensure termination of the generator.  The variable is added to `freevars`

194

/// when generating the body, so it may be used there.  If `negated` is true,

195

/// the quantifier is generated with negative polarity, which biases the

196

/// generator to produce more negations and implications, which flip polarity.

197

284

fn random_quantifier<R: Rng>(

198

284

    rng: &mut R,

199

284

    quantifier: Quantifier,

200

284

    depth: usize,

201

284

    freevars: &[IdDecl],

202

284

    config: &PbesGenConfig,

203

284

    negated: bool,

204

284

) -> PbesExpr {

205

284

    let available: Vec<&str> = QUANT_INTS

206

284

        .iter()

207

1431

        .filter(|&&q| !freevars.iter().any(|fv| fv.identifier == q))

208

284

        .copied()

209

284

        .collect();

210

211

284

    if available.is_empty() {

212

        return random_leaf(rng, freevars, config, negated);

213

284

214

215

284

    let var_name = (*available.choose(rng).expect("available is non-empty")).to_string();

216

284

    let var_decl = IdDecl::new(var_name.clone(), SortExpression::Simple(Sort::Nat), Span::default());

217

218

284

    let mut new_freevars = freevars.to_vec();

219

284

    new_freevars.push(as_expr_decl(&var_name));

220

221

284

    let body = random_pbes_expr(rng, depth, &new_freevars, config, negated);

222

223

    // Bound the quantifier variable to ensure termination: forall t. t < 3 => body  /  exists t. t < 3 && body

224

284

    let bound = PbesExpr::DataValExpr(DataExpr::Binary {

225

284

        op: DataExprBinaryOp::LessThan,

226

284

        lhs: Box::new(DataExpr::Id(var_name)),

227

284

        rhs: Box::new(DataExpr::Number("3".to_string())),

228

284

});

229

284

    let bounded_body = match quantifier {

230

128

        Quantifier::Forall => PbesExpr::Binary {

231

128

            op: PbesExprBinaryOp::Implies,

232

128

            lhs: Box::new(bound),

233

128

            rhs: Box::new(body),

234

128

},

235

156

        Quantifier::Exists => PbesExpr::Binary {

236

156

            op: PbesExprBinaryOp::Conjunction,

237

156

            lhs: Box::new(bound),

238

156

            rhs: Box::new(body),

239

156

},

240

};

241

242

284

    PbesExpr::Quantifier {

243

284

        quantifier,

244

284

        variables: vec![var_decl],

245

284

        body: Box::new(bounded_body),

246

284

247

284

248

249

20820

fn is_bool_var(name: &str) -> bool {

250

20820

    PRED_BOOLS.contains(&name)

251

20820

252

253

5680

fn as_expr_decl(name: &str) -> IdDecl {

254

5680

    let sort = if is_bool_var(name) { Sort::Bool } else { Sort::Nat };

255

5680

    IdDecl::new(name.to_string(), SortExpression::Simple(sort), Span::default())

256

5680

257

258

struct PredVar {

259

    name: String,

260

    params: Vec<String>,

261

262

263

impl PredVar {

264

3000

    fn to_decl(&self) -> PropVarDecl {

265

3000

        let params = self

266

3000

            .params

267

3000

            .iter()

268

3000

            .map(|p| {

269

2840

                let sort = if is_bool_var(p) { Sort::Bool } else { Sort::Nat };

270

2840

                IdDecl::new(p.clone(), SortExpression::Simple(sort), Span::default())

271

2840

})

272

3000

            .collect();

273

3000

        PropVarDecl::new(self.name.clone(), params)

274

3000

275

276

3000

    fn expr_freevars(&self) -> Vec<IdDecl> {

277

3000

        self.params.iter().map(|p| as_expr_decl(p)).collect()

278

3000

279

280

281

300

fn make_pred_var<R: Rng>(rng: &mut R, index: usize, use_integers: bool) -> PredVar {

282

300

    let size = rng.random_range(0..=2usize);

283

300

    let mut pool: Vec<&str> = if use_integers {

284

156

        PRED_INTS.iter().chain(PRED_BOOLS.iter()).copied().collect()

285

    } else {

286

144

        PRED_BOOLS.to_vec()

287

};

288

300

    let mut params = Vec::new();

289

300

    for _ in 0..size {

290

284

        if pool.is_empty() {

291

            break;

292

284

293

284

        let idx = rng.random_range(0..pool.len());

294

284

        params.push(pool.remove(idx).to_string());

295

296

300

    PredVar {

297

300

        name: format!("X{index}"),

298

300

        params,

299

300