Grcov report - operations.rs

1

use conjure_cp::ast::{Atom, Expression as Expr, Literal};

2

use conjure_cp::ast::{SATIntEncoding, SymbolTable};

3

use conjure_cp::rule_engine::ApplicationError;

4

use conjure_cp::rule_engine::{

5

    ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect, register_rule,

6

};

7

8

use conjure_cp::ast::Metadata;

9

use conjure_cp::ast::Moo;

10

use conjure_cp::into_matrix_expr;

11

12

use crate::backends::sat::boolean::tseytin_or;

13

14

use conjure_cp::ast::SatEncodingDecision;

15

/// This function confirms that all of the input expressions are direct SATInts, and returns vectors for each input of their bits

16

/// This function also normalizes direct SATInt operands to a common value range by zero-padding.

17

29869

pub fn validate_direct_int_operands(

18

29869

    exprs: Vec<Expr>,

19

29869

) -> Result<(Vec<Vec<Expr>>, i32, i32), ApplicationError> {

20

    // TODO: In the future it may be possible to optimize operations between integers with different bit sizes

21

    // Collect inner bit vectors from each SATInt

22

23

    // Iterate over all inputs

24

    // Check they are direct and calulate a lower and upper bound

25

29869

    let mut global_min: i32 = i32::MAX;

26

29869

    let mut global_max: i32 = i32::MIN;

27

28

29869

    for operand in &exprs {

29

29869

        let Expr::SATInt(_, SATIntEncoding::Direct, _, (local_min, local_max)) = operand else {

30

24199

            return Err(RuleNotApplicable);

31

};

32

5670

        global_min = global_min.min(*local_min);

33

5670

        global_max = global_max.max(*local_max);

34

35

36

    // build out by iterating over each operand and expanding it to match the new bounds

37

38

5670

    let out: Vec<Vec<Expr>> = exprs

39

5670

        .into_iter()

40

5670

        .map(|expr| {

41

5670

            let Expr::SATInt(_, SATIntEncoding::Direct, inner, (local_min, local_max)) = expr

42

            else {

43

                return Err(RuleNotApplicable);

44

};

45

46

5670

            let Some(v) = inner.as_ref().clone().into_list() else {

47

                return Err(RuleNotApplicable);

48

};

49

50

            // calulcate how many zeroes to prepend/append

51

5670

            let prefix_len = (local_min - global_min) as usize;

52

5670

            let postfix_len = (global_max - local_max) as usize;

53

54

5670

            let mut bits = Vec::with_capacity(v.len() + prefix_len + postfix_len);

55

56

            // add 0s to start

57

5670

            bits.extend(std::iter::repeat_n(

58

5670

                Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

59

5670

                prefix_len,

60

5670

));

61

62

5670

            bits.extend(v);

63

64

            // add 0s to end

65

5670

            bits.extend(std::iter::repeat_n(

66

5670

                Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

67

5670

                postfix_len,

68

5670

));

69

70

5670

            Ok(bits)

71

5670

})

72

        .collect::<Result<_, _>>()?;

73

74

5670

    Ok((out, global_min, global_max))

75

29869

76

77

/// Converts a - expression for a SATInt to a new SATInt

78

///

79

/// ```text

80

/// -SATInt(a) ~> SATInt(b)

81

///

82

/// ```

83

#[register_rule("SAT", 9100, [Neg])]

84

17591

fn neg_sat_direct(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

85

17591

    let Expr::Neg(_, value) = expr else {

86

21

        return Err(RuleNotApplicable);

87

};

88

89

17570

    let (binding, old_min, old_max) = validate_direct_int_operands(vec![value.as_ref().clone()])?;

90

1260

    let [val_bits] = binding.as_slice() else {

91

        return Err(RuleNotApplicable);

92

};

93

94

1260

    let new_min = -old_max;

95

1260

    let new_max = -old_min;

96

97

1260

    let mut out = val_bits.clone();

98

1260

    out.reverse();

99

100

1260

    Ok(RuleEffect::pure(Expr::SATInt(

101

1260

        Metadata::new(),

102

1260

        SATIntEncoding::Direct,

103

1260

        Moo::new(into_matrix_expr!(out)),

104

1260

        (new_min, new_max),

105

1260

)))

106

17591

107

108

use super::super::floor_div;

109

110

/// Converts a / expression between two direct SATInts to a new direct SATInt

111

/// using the "lookup table" method.

112

///

113

/// ```text

114

/// SafeDiv(SATInt(a), SATInt(b)) ~> SATInt(c)

115

///

116

/// ```

117

#[register_rule("SAT", 9100, [SafeDiv])]

118

341922

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

119

341922

    let Expr::SafeDiv(_, numer_expr, denom_expr) = expr else {

120

21

        return Err(RuleNotApplicable);

121

};

122

123

    let Expr::SATInt(_, SATIntEncoding::Direct, numer_inner, (numer_min, numer_max)) =

124

341901

        numer_expr.as_ref()

125

    else {

126

241731

        return Err(RuleNotApplicable);

127

};

128

100170

    let Some(numer_bits) = numer_inner.as_ref().clone().into_list() else {

129

        return Err(RuleNotApplicable);

130

};

131

132

    let Expr::SATInt(_, SATIntEncoding::Direct, denom_inner, (denom_min, denom_max)) =

133

100170

        denom_expr.as_ref()

134

    else {

135

        return Err(RuleNotApplicable);

136

};

137

138

100170

    let Some(denom_bits) = denom_inner.as_ref().clone().into_list() else {

139

        return Err(RuleNotApplicable);

140

};

141

142

100170

    let mut quot_min = i32::MAX;

143

100170

    let mut quot_max = i32::MIN;

144

145

100170

    for i in *numer_min..=*numer_max {

146

1070055

        for j in *denom_min..=*denom_max {

147

1237320

            let k = if j == 0 {

148

27720

149

            } else {

150

1209600

                floor_div(i, j).ok_or(RuleNotApplicable)?

151

};

152

1237320

            quot_min = quot_min.min(k);

153

1237320

            quot_max = quot_max.max(k);

154

155

156

157

100170

    let mut new_symbols = symbols.clone();

158

100170

    let mut quot_bits = Vec::new();

159

160

    // generate boolean variables for all possible quotients

161

100170

    for _ in quot_min..=quot_max {

162

541800

        let decl = new_symbols.gen_find_auxiliary(&conjure_cp::ast::Domain::bool());

163

541800

        quot_bits.push(Expr::Atomic(

164

541800

            Metadata::new(),

165

541800

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

166

541800

));

167

168

169

100170

    let mut new_sat_decisions = vec![];

170

171

    // Record lookup-table implications: (n_i AND d_j) => q_k

172

100170

    for i in *numer_min..=*numer_max {

173

1070055

        let numer_bit = &numer_bits[(i - numer_min) as usize];

174

1070055

        for j in *denom_min..=*denom_max {

175

1237320

            let denom_bit = &denom_bits[(j - denom_min) as usize];

176

177

1237320

            let k = if j == 0 {

178

27720

179

            } else {

180

1209600

                floor_div(i, j).ok_or(RuleNotApplicable)?

181

};

182

183

1237320

            let quot_bit = &quot_bits[(k - quot_min) as usize];

184

185

1237320

            let premise = Expr::And(

186

1237320

                Metadata::new(),

187

1237320

                Moo::new(into_matrix_expr!(vec![

188

1237320

                    numer_bit.clone(),

189

1237320

                    denom_bit.clone()

190

1237320

                ])),

191

1237320

);

192

1237320

            new_sat_decisions.push(SatEncodingDecision::Assert(Expr::Imply(

193

1237320

                Metadata::new(),

194

1237320

                Moo::new(premise),

195

1237320

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

196

1237320

            )));

197

198

199

200

100170

    new_sat_decisions.push(SatEncodingDecision::AtMostOne {

201

100170

        inputs: quot_bits.clone(),

202

100170

        encoding: None,

203

100170

});

204

205

100170

    let quot_int = Expr::SATInt(

206

100170

        Metadata::new(),

207

100170

        SATIntEncoding::Direct,

208

100170

        Moo::new(into_matrix_expr!(quot_bits)),

209

100170

        (quot_min, quot_max),

210

100170

);

211

212

100170

    Ok(RuleEffect::sat(quot_int, new_sat_decisions, new_symbols))

213

341922

214

215

/// Matches a `|SATInt|` with an absolute value operation and rewrites it to a direct-encoded absolute-value `SATInt` by grouping input indicator bits by `|value|` and OR-ing each group (named here as buckets) into the corresponding output bit.

216

#[register_rule("SAT", 9100, [Abs])]

217

12320

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

218

12320

    let Expr::Abs(_, value_expr) = expr else {

219

21

        return Err(RuleNotApplicable);

220

};

221

222

    let (binding, old_min, old_max) =

223

12299

        validate_direct_int_operands(vec![value_expr.as_ref().clone()])?;

224

225

4410

    let [val_bits] = binding.as_slice() else {

226

        return Err(RuleNotApplicable);

227

};

228

229

    // The new range is from the minimum absolute value to the maximum absolute value. The minimum absolute value is either 0 if the old range includes 0, or the smaller of the absolute values of the old min and max if the old range does not include 0. The maximum absolute value is the larger of the absolute values of the old min and max.

230

4410

    let new_min = if old_min <= 0 && old_max >= 0 {

231

3780

232

    } else {

233

630

        old_min.abs().min(old_max.abs())

234

};

235

4410

    let new_max = old_min.abs().max(old_max.abs());

236

237

4410

    let mut new_symbols = symbols.clone();

238

4410

    let mut new_sat_decisions = vec![];

239

240

4410

    let bucket_count = (new_max - new_min + 1) as usize;

241

4410

    let mut buckets: Vec<Vec<Expr>> = vec![Vec::new(); bucket_count];

242

243

    // Iterates over all possible input values, calculate their absolute value, and place them in the corresponding bucket. Each bucket corresponds to a possible output value, and contains the disjunction of all input bits that could produce that output.

244

4410

    for value in old_min..=old_max {

245

47565

        let input_bit = val_bits[(value - old_min) as usize].clone();

246

47565

        let abs_value = value.abs();

247

47565

        let bucket_idx = (abs_value - new_min) as usize;

248

47565

        buckets[bucket_idx].push(input_bit);

249

250

251

    // For each bucket, if it's empty then the output bit is false, if it contains one element then the output bit is that element, and if it contains multiple elements then the output bit is the OR of all elements in the bucket.

252

4410

    let mut abs_bits = Vec::with_capacity(bucket_count);

253

4410

    for bucket in buckets {

254

29295

        let out_bit = match bucket.len() {

255

            0 => Expr::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(false))),

256

11025

            1 => bucket[0].clone(),

257

18270

            _ => tseytin_or(&bucket, &mut new_sat_decisions, &mut new_symbols),

258

};

259

260

29295

        abs_bits.push(out_bit);

261

262

263

4410

    let abs_int = Expr::SATInt(

264

4410

        Metadata::new(),

265

4410

        SATIntEncoding::Direct,

266

4410

        Moo::new(into_matrix_expr!(abs_bits)),

267

4410

        (new_min, new_max),

268

4410

);

269

270

4410

    Ok(RuleEffect::sat(abs_int, new_sat_decisions, new_symbols))

271

12320