Grcov report - sat.rs

1

use conjure_core::matrix_expr;

2

use conjure_oxide::ast::{

3

    Atom::Reference, Declaration, Domain::BoolDomain, Domain::IntDomain, Expression::*, Name, Range,

4

};

5

use conjure_oxide::solver::adaptors::sat_common::CNFModel;

6

use conjure_oxide::solver::SolverError;

7

use conjure_oxide::utils::testing::assert_eq_any_order;

8

use conjure_oxide::{Metadata, Model as ConjureModel};

9

10

#[test]

11

1

fn test_single_var() {

12

1

    // x -> [[1]]

13

1

14

1

    let mut model: ConjureModel = ConjureModel::default();

15

1

    let submodel = model.as_submodel_mut();

16

1

17

1

    let x: Name = Name::UserName(String::from('x'));

18

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

19

1

    submodel.add_constraint(Atomic(Metadata::new(), Reference(x.clone())));

20

1

21

1

    let res: Result<CNFModel, SolverError> = CNFModel::from_conjure(model);

22

1

    assert!(res.is_ok());

23

24

1

    let cnf = res.unwrap();

25

1

26

1

    assert_eq!(cnf.get_index(&x), Some(1));

27

1

    assert!(cnf.get_name(1).is_some());

28

1

    assert_eq!(cnf.get_name(1).unwrap(), &x);

29

30

1

    assert_eq!(cnf.clauses, vec![vec![1]]);

31

1

32

33

#[test]

34

1

fn test_single_not() {

35

1

    // Not(x) -> [[-1]]

36

1

37

1

    let mut model: ConjureModel = ConjureModel::default();

38

1

    let submodel = model.as_submodel_mut();

39

1

40

1

    let x: Name = Name::UserName(String::from('x'));

41

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

42

1

    submodel.add_constraint(Not(

43

1

        Metadata::new(),

44

1

        Box::from(Atomic(Metadata::new(), Reference(x.clone()))),

45

1

));

46

1

47

1

    let cnf: CNFModel = CNFModel::from_conjure(model).unwrap();

48

1

    assert_eq!(cnf.get_index(&x), Some(1));

49

1

    assert_eq!(cnf.clauses, vec![vec![-1]]);

50

51

1

    assert_eq!(

52

1

        cnf.as_expression().unwrap(),

53

1

        And(

54

1

            Metadata::new(),

55

1

            Box::new(matrix_expr![Or(

56

1

                Metadata::new(),

57

1

                Box::new(matrix_expr![Not(

58

1

                    Metadata::new(),

59

1

                    Box::from(Atomic(Metadata::new(), Reference(x.clone())))

60

1

)])

61

1

)])

62

1

63

1

64

1

65

66

#[test]

67

1

fn test_single_or() {

68

1

    // Or(x, y) -> [[1, 2]]

69

1

70

1

    let mut model: ConjureModel = ConjureModel::default();

71

1

    let submodel = model.as_submodel_mut();

72

1

73

1

    let x: Name = Name::UserName(String::from('x'));

74

1

    let y: Name = Name::UserName(String::from('y'));

75

1

76

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

77

1

    submodel.add_symbol(Declaration::new_var(y.clone(), BoolDomain));

78

1

    submodel.add_constraint(Or(

79

1

        Metadata::new(),

80

1

        Box::new(matrix_expr![

81

1

            Atomic(Metadata::new(), Reference(x.clone())),

82

1

            Atomic(Metadata::new(), Reference(y.clone())),

83

1

]),

84

1

));

85

1

86

1

    let cnf: CNFModel = CNFModel::from_conjure(model).unwrap();

87

1

88

1

    let xi = cnf.get_index(&x).unwrap();

89

1

    let yi = cnf.get_index(&y).unwrap();

90

1

    assert_eq_any_order(&cnf.clauses, &vec![vec![xi, yi]]);

91

1

92

1

    assert_eq!(

93

1

        cnf.as_expression().unwrap(),

94

1

        And(

95

1

            Metadata::new(),

96

1

            Box::new(matrix_expr![Or(

97

1

                Metadata::new(),

98

1

                Box::new(matrix_expr![

99

1

                    Atomic(Metadata::new(), Reference(x.clone())),

100

1

                    Atomic(Metadata::new(), Reference(y.clone())),

101

1

]),

102

1

)])

103

1

104

1

105

1

106

107

#[test]

108

1

fn test_or_not() {

109

1

    // Or(x, Not(y)) -> [[1, -2]]

110

1

111

1

    let mut model: ConjureModel = ConjureModel::default();

112

1

    let submodel = model.as_submodel_mut();

113

1

114

1

    let x: Name = Name::UserName(String::from('x'));

115

1

    let y: Name = Name::UserName(String::from('y'));

116

1

117

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

118

1

    submodel.add_symbol(Declaration::new_var(y.clone(), BoolDomain));

119

1

    submodel.add_constraint(Or(

120

1

        Metadata::new(),

121

1

        Box::new(matrix_expr![

122

1

            Atomic(Metadata::new(), Reference(x.clone())),

123

1

            Not(

124

1

                Metadata::new(),

125

1

                Box::from(Atomic(Metadata::new(), Reference(y.clone()))),

126

1

),

127

1

]),

128

1

));

129

1

130

1

    let cnf: CNFModel = CNFModel::from_conjure(model).unwrap();

131

1

132

1

    let xi = cnf.get_index(&x).unwrap();

133

1

    let yi = cnf.get_index(&y).unwrap();

134

1

    assert_eq_any_order(&cnf.clauses, &vec![vec![xi, -yi]]);

135

1

136

1

    assert_eq!(

137

1

        cnf.as_expression().unwrap(),

138

1

        And(

139

1

            Metadata::new(),

140

1

            Box::new(matrix_expr![Or(

141

1

                Metadata::new(),

142

1

                Box::new(matrix_expr![

143

1

                    Atomic(Metadata::new(), Reference(x.clone())),

144

1

                    Not(

145

1

                        Metadata::new(),

146

1

                        Box::from(Atomic(Metadata::new(), Reference(y.clone())))

147

1

),

148

1

])

149

1

)])

150

1

151

1

152

1

153

154

#[test]

155

1

fn test_multiple() {

156

1

    // [x, y] - equivalent to And(x, y) -> [[1], [2]]

157

1

158

1

    let mut model: ConjureModel = ConjureModel::default();

159

1

    let submodel = model.as_submodel_mut();

160

1

161

1

    let x: Name = Name::UserName(String::from('x'));

162

1

    let y: Name = Name::UserName(String::from('y'));

163

1

164

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

165

1

    submodel.add_symbol(Declaration::new_var(y.clone(), BoolDomain));

166

1

    submodel.add_constraint(Atomic(Metadata::new(), Reference(x.clone())));

167

1

    submodel.add_constraint(Atomic(Metadata::new(), Reference(y.clone())));

168

1

169

1

    let cnf: CNFModel = CNFModel::from_conjure(model).unwrap();

170

1

171

1

    let xi = cnf.get_index(&x).unwrap();

172

1

    let yi = cnf.get_index(&y).unwrap();

173

1

    assert_eq_any_order(&cnf.clauses, &vec![vec![xi], vec![yi]]);

174

1

175

1

    assert_eq!(

176

1

        cnf.as_expression().unwrap(),

177

1

        And(

178

1

            Metadata::new(),

179

1

            Box::new(matrix_expr![

180

1

Or(

181

1

                    Metadata::new(),

182

1

                    Box::new(matrix_expr![Atomic(Metadata::new(), Reference(x.clone()))])

183

1

),

184

1

Or(

185

1

                    Metadata::new(),

186

1

                    Box::new(matrix_expr![Atomic(Metadata::new(), Reference(y.clone()))])

187

1

188

1

])

189

1

190

1

191

1

192

193

#[test]

194

1

fn test_and() {

195

1

    // And(x, y) -> [[1], [2]]

196

1

197

1

    let mut model: ConjureModel = ConjureModel::default();

198

1

    let submodel = model.as_submodel_mut();

199

1

200

1

    let x: Name = Name::UserName(String::from('x'));

201

1

    let y: Name = Name::UserName(String::from('y'));

202

1

203

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

204

1

    submodel.add_symbol(Declaration::new_var(y.clone(), BoolDomain));

205

1

    submodel.add_constraint(And(

206

1

        Metadata::new(),

207

1

        Box::new(matrix_expr![

208

1

            Atomic(Metadata::new(), Reference(x.clone())),

209

1

            Atomic(Metadata::new(), Reference(y.clone())),

210

1

]),

211

1

));

212

1

213

1

    let cnf: CNFModel = CNFModel::from_conjure(model).unwrap();

214

1

215

1

    let xi = cnf.get_index(&x).unwrap();

216

1

    let yi = cnf.get_index(&y).unwrap();

217

1

    assert_eq_any_order(&cnf.clauses, &vec![vec![xi], vec![yi]]);

218

1

219

1

    assert_eq!(

220

1

        cnf.as_expression().unwrap(),

221

1

        And(

222

1

            Metadata::new(),

223

1

            Box::new(matrix_expr![

224

1

Or(

225

1

                    Metadata::new(),

226

1

                    Box::new(matrix_expr![Atomic(Metadata::new(), Reference(x.clone())),])

227

1

),

228

1

Or(

229

1

                    Metadata::new(),

230

1

                    Box::new(matrix_expr![Atomic(Metadata::new(), Reference(y.clone())),])

231

1

232

1

])

233

1

234

1

235

1

236

237

#[test]

238

1

fn test_nested_ors() {

239

1

    // Or(x, Or(y, z)) -> [[1, 2, 3]]

240

1

241

1

    let mut model: ConjureModel = ConjureModel::default();

242

1

    let submodel = model.as_submodel_mut();

243

1

244

1

    let x: Name = Name::UserName(String::from('x'));

245

1

    let y: Name = Name::UserName(String::from('y'));

246

1

    let z: Name = Name::UserName(String::from('z'));

247

1

248

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

249

1

    submodel.add_symbol(Declaration::new_var(y.clone(), BoolDomain));

250

1

    submodel.add_symbol(Declaration::new_var(z.clone(), BoolDomain));

251

1

252

1

    submodel.add_constraint(Or(

253

1

        Metadata::new(),

254

1

        Box::new(matrix_expr![

255

1

            Atomic(Metadata::new(), Reference(x.clone())),

256

1

Or(

257

1

                Metadata::new(),

258

1

                Box::new(matrix_expr![

259

1

                    Atomic(Metadata::new(), Reference(y.clone())),

260

1

                    Atomic(Metadata::new(), Reference(z.clone())),

261

1

]),

262

1

),

263

1

]),

264

1

));

265

1

266

1

    let cnf: CNFModel = CNFModel::from_conjure(model).unwrap();

267

1

268

1

    let xi = cnf.get_index(&x).unwrap();

269

1

    let yi = cnf.get_index(&y).unwrap();

270

1

    let zi = cnf.get_index(&z).unwrap();

271

1

    assert_eq_any_order(&cnf.clauses, &vec![vec![xi, yi, zi]]);

272

1

273

1

    assert_eq!(

274

1

        cnf.as_expression().unwrap(),

275

1

        And(

276

1

            Metadata::new(),

277

1

            Box::new(matrix_expr![Or(

278

1

                Metadata::new(),

279

1

                Box::new(matrix_expr![

280

1

                    Atomic(Metadata::new(), Reference(x.clone())),

281

1

                    Atomic(Metadata::new(), Reference(y.clone())),

282

1

                    Atomic(Metadata::new(), Reference(z.clone())),

283

1

])

284

1

)])

285

1

286

1

287

1

288

289

#[test]

290

1

fn test_int() {

291

1

    // y is an IntDomain - only booleans should be allowed

292

1

293

1

    let mut model: ConjureModel = ConjureModel::default();

294

1

    let submodel = model.as_submodel_mut();

295

1

296

1

    let x: Name = Name::UserName(String::from('x'));

297

1

    let y: Name = Name::UserName(String::from('y'));

298

1

299

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

300

1

    submodel.add_symbol(Declaration::new_var(

301

1

        y.clone(),

302

1

        IntDomain(vec![Range::Bounded(1, 2)]),

303

1

));

304

1

305

1

    submodel.add_constraint(Atomic(Metadata::new(), Reference(x.clone())));

306

1

    submodel.add_constraint(Atomic(Metadata::new(), Reference(y.clone())));

307

1

308

1

    let cnf: Result<CNFModel, SolverError> = CNFModel::from_conjure(model);

309

1

    assert!(cnf.is_err());

310

1

311

312

#[test]

313

1

fn test_eq() {

314

1

    // Eq(x, y) - this operation is not allowed

315

1

316

1

    let mut model: ConjureModel = ConjureModel::default();

317

1

    let submodel = model.as_submodel_mut();

318

1

319

1

    let x: Name = Name::UserName(String::from('x'));

320

1

    let y: Name = Name::UserName(String::from('y'));

321

1

322

1

    submodel.add_symbol(Declaration::new_var(x.clone(), BoolDomain));

323

1

    submodel.add_symbol(Declaration::new_var(y.clone(), BoolDomain));

324

1

325

1

    submodel.add_constraint(Eq(

326

1

        Metadata::new(),

327

1

        Box::from(Atomic(Metadata::new(), Reference(x.clone()))),

328

1

        Box::from(Atomic(Metadata::new(), Reference(y.clone()))),

329

1

));

330

1

331

1

    let cnf: Result<CNFModel, SolverError> = CNFModel::from_conjure(model);

332

1

    assert!(cnf.is_err());

333

1