Grcov report - boolean.rs

1

use conjure_cp::essence_expr;

2

3

use conjure_cp::ast::Metadata;

4

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

5

use conjure_cp::rule_engine::{

6

    ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,

7

};

8

9

use conjure_cp::ast::AbstractLiteral::Matrix;

10

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

11

12

use crate::utils::is_literal;

13

14

523665

fn create_bool_aux(symbols: &mut SymbolTable) -> Expr {

15

523665

    let name = symbols.gen_find(&Domain::bool());

16

17

523665

    symbols.insert(name.clone());

18

19

523665

    Expr::Atomic(

20

523665

        Metadata::new(),

21

523665

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

22

523665

23

523665

24

25

1546824

fn create_clause(exprs: Vec<Expr>) -> Option<CnfClause> {

26

1546824

    let mut new_terms = vec![];

27

3514257

    for expr in exprs {

28

235692

        if let Expr::Atomic(_, Atom::Literal(Literal::Bool(x))) = expr {

29

            // true ~~> entire or is true

30

            // false ~~> remove false from the or

31

235692

            if x {

32

24219

                return None;

33

211473

34

3278565

        } else if let Expr::Not(_, ref inner) = expr {

35

1751379

            if let Expr::Atomic(_, Atom::Literal(Literal::Bool(x))) = inner.as_ref() {

36

                // check for nested literal

37

226422

                if !x {

38

202311

                    return None;

39

24111

40

1524957

            } else {

41

1524957

                new_terms.push(expr);

42

1524957

43

1527186

        } else {

44

1527186

            new_terms.push(expr);

45

1527186

46

47

48

1320294

    Some(CnfClause::new(new_terms))

49

1546824

50

51

// TODO: Optimize all logic operators for constants

52

// TODO: If a clause simplifies to false, it should skip the solver and give no solutions

53

54

/// Applies the Tseytin and transformation to series of variables, returns the new expression, symbol table and clauses

55

208248

pub fn tseytin_and(

56

208248

    exprs: &Vec<Expr>,

57

208248

    clauses: &mut Vec<CnfClause>,

58

208248

    symbols: &mut SymbolTable,

59

208248

) -> Expr {

60

208248

    let new_expr = create_bool_aux(symbols);

61

62

208248

    let mut full_conj: Vec<Expr> = vec![new_expr.clone()];

63

64

416508

    for x in exprs {

65

416508

        clauses.extend(create_clause(vec![

66

416508

            Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

67

416508

            x.clone(),

68

416508

        ]));

69

416508

        full_conj.push(Expr::Not(Metadata::new(), Moo::new(x.clone())));

70

416508

71

208248

    clauses.extend(create_clause(full_conj));

72

73

208248

    new_expr

74

208248

75

76

/// Applies the Tseytin not transformation to a variable, returns the new expression, symbol table and clauses

77

60300

pub fn tseytin_not(x: Expr, clauses: &mut Vec<CnfClause>, symbols: &mut SymbolTable) -> Expr {

78

60300

    let new_expr = create_bool_aux(symbols);

79

80

60300

    clauses.extend(create_clause(vec![

81

60300

        Expr::Not(Metadata::new(), Moo::new(x.clone())),

82

60300

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

83

    ]));

84

60300

    clauses.extend(create_clause(vec![x, new_expr.clone()]));

85

86

60300

    new_expr

87

60300

88

89

/// Applies the Tseytin or transformation to series of variables, returns the new expression, symbol table and clauses

90

218100

pub fn tseytin_or(

91

218100

    exprs: &Vec<Expr>,

92

218100

    clauses: &mut Vec<CnfClause>,

93

218100

    symbols: &mut SymbolTable,

94

218100

) -> Expr {

95

218100

    let new_expr = create_bool_aux(symbols);

96

97

218100

    let mut full_conj: Vec<Expr> = vec![Expr::Not(Metadata::new(), Moo::new(new_expr.clone()))];

98

99

436536

    for x in exprs {

100

436536

        clauses.extend(create_clause(vec![

101

436536

            Expr::Not(Metadata::new(), Moo::new(x.clone())),

102

436536

            new_expr.clone(),

103

436536

        ]));

104

436536

        full_conj.push(x.clone());

105

436536

106

107

218100

    clauses.extend(create_clause(full_conj));

108

109

218100

    new_expr

110

218100

111

112

/// Applies the Tseytin iff transformation to two variables, returns the new expression, symbol table and clauses

113

28401

pub fn tseytin_iff(

114

28401

    x: Expr,

115

28401

    y: Expr,

116

28401

    clauses: &mut Vec<CnfClause>,

117

28401

    symbols: &mut SymbolTable,

118

28401

) -> Expr {

119

28401

    let new_expr = create_bool_aux(symbols);

120

121

28401

    clauses.extend(create_clause(vec![

122

28401

        Expr::Not(Metadata::new(), Moo::new(x.clone())),

123

28401

        Expr::Not(Metadata::new(), Moo::new(y.clone())),

124

28401

        new_expr.clone(),

125

    ]));

126

28401

    clauses.extend(create_clause(vec![x.clone(), y.clone(), new_expr.clone()]));

127

28401

    clauses.extend(create_clause(vec![

128

28401

        x.clone(),

129

28401

        Expr::Not(Metadata::new(), Moo::new(y.clone())),

130

28401

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

131

    ]));

132

28401

    clauses.extend(create_clause(vec![

133

28401

        Expr::Not(Metadata::new(), Moo::new(x)),

134

28401

y,

135

28401

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

136

    ]));

137

138

28401

    new_expr

139

28401

140

141

/// Applies the Tseytin imply transformation to two variables, returns the new expression, symbol table and clauses

142

2196

pub fn tseytin_imply(

143

2196

    x: Expr,

144

2196

    y: Expr,

145

2196

    clauses: &mut Vec<CnfClause>,

146

2196

    symbols: &mut SymbolTable,

147

2196

) -> Expr {

148

2196

    let new_expr = create_bool_aux(symbols);

149

150

2196

    clauses.extend(create_clause(vec![

151

2196

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

152

2196

        Expr::Not(Metadata::new(), Moo::new(x.clone())),

153

2196

        y.clone(),

154

    ]));

155

2196

    clauses.extend(create_clause(vec![new_expr.clone(), x]));

156

2196

    clauses.extend(create_clause(vec![

157

2196

        new_expr.clone(),

158

2196

        Expr::Not(Metadata::new(), Moo::new(y)),

159

    ]));

160

161

2196

    new_expr

162

2196

163

164

/// Applies the Tseytin multiplex transformation

165

/// cond ? b : a

166

///

167

/// cond = 1 => b

168

/// cond = 0 => a

169

#[allow(dead_code)]

170

480

pub fn tseytin_mux(

171

480

    cond: Expr,

172

480

    a: Expr,

173

480

    b: Expr,

174

480

    clauses: &mut Vec<CnfClause>,

175

480

    symbols: &mut SymbolTable,

176

480

) -> Expr {

177

480

    let new_expr = create_bool_aux(symbols);

178

179

480

    clauses.extend(create_clause(vec![

180

480

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

181

480

        cond.clone(),

182

480

        a.clone(),

183

    ]));

184

480

    clauses.extend(create_clause(vec![

185

480

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

186

480

        Expr::Not(Metadata::new(), Moo::new(cond.clone())),

187

480

        b.clone(),

188

    ]));

189

480

    clauses.extend(create_clause(vec![

190

480

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

191

480

        a.clone(),

192

480

        b.clone(),

193

    ]));

194

195

480

    clauses.extend(create_clause(vec![

196

480

        new_expr.clone(),

197

480

        cond.clone(),

198

480

        Expr::Not(Metadata::new(), Moo::new(a.clone())),

199

    ]));

200

480

    clauses.extend(create_clause(vec![

201

480

        new_expr.clone(),

202

480

        Expr::Not(Metadata::new(), Moo::new(cond)),

203

480

        Expr::Not(Metadata::new(), Moo::new(b.clone())),

204

    ]));

205

480

    clauses.extend(create_clause(vec![

206

480

        new_expr.clone(),

207

480

        Expr::Not(Metadata::new(), Moo::new(a)),

208

480

        Expr::Not(Metadata::new(), Moo::new(b)),

209

    ]));

210

211

480

    new_expr

212

480

213

214

/// Applies the Tseytin xor transformation to two variables, returns the new expression, symbol table and clauses

215

#[allow(dead_code)]

216

5940

pub fn tseytin_xor(

217

5940

    x: Expr,

218

5940

    y: Expr,

219

5940

    clauses: &mut Vec<CnfClause>,

220

5940

    symbols: &mut SymbolTable,

221

5940

) -> Expr {

222

5940

    let new_expr = create_bool_aux(symbols);

223

224

5940

    clauses.extend(create_clause(vec![

225

5940

        Expr::Not(Metadata::new(), Moo::new(x.clone())),

226

5940

        Expr::Not(Metadata::new(), Moo::new(y.clone())),

227

5940

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

228

    ]));

229

5940

    clauses.extend(create_clause(vec![

230

5940

        x.clone(),

231

5940

        y.clone(),

232

5940

        Expr::Not(Metadata::new(), Moo::new(new_expr.clone())),

233

    ]));

234

5940

    clauses.extend(create_clause(vec![

235

5940

        x.clone(),

236

5940

        Expr::Not(Metadata::new(), Moo::new(y.clone())),

237

5940

        new_expr.clone(),

238

    ]));

239

5940

    clauses.extend(create_clause(vec![

240

5940

        Expr::Not(Metadata::new(), Moo::new(x)),

241

5940

y,

242

5940

        new_expr.clone(),

243

    ]));

244

245

5940

    new_expr

246

5940

247

248

/// Converts a single boolean atom to a clause

249

///

250

/// ```text

251

///  a

252

///  ~~>

253

///

254

///  new clauses:

255

///  clause(a)

256

/// ```

257

#[register_rule("SAT", 8400, [Root])]

258

156024

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

259

    // The single atom must not be within another expression

260

156024

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

261

139152

        return Err(RuleNotApplicable);

262

};

263

264

    // Find the position of the first reference atom with boolean domain

265

16872

    let Some(pos) = children.iter().position(

266

11007

        |e| matches!(e, Expr::Atomic(_, Atom::Reference(x)) if x.domain().is_some_and(|d| d.is_bool())),

267

    ) else {

268

5865

        return Err(RuleNotApplicable);

269

};

270

271

    // Clone the children since expr is borrowed immutably

272

11007

    let mut new_children = children.clone();

273

274

11007

    let removed = new_children.remove(pos);

275

276

11007

    let new_clauses = vec![CnfClause::new(vec![removed])];

277

278

    // If now empty, replace with `true`

279

11007

    if new_children.is_empty() {

280

1854

        new_children.push(essence_expr!(true));

281

9153

282

283

11007

    let new_expr = Expr::Root(Metadata::new(), new_children);

284

285

11007

    Ok(Reduction::cnf(new_expr, new_clauses, symbols.clone()))

286

156024

287

288

/// Converts an and/or expression to an aux variable, using the tseytin transformation

289

///

290

/// ```text

291

///  and(a, b, c, ...)

292

///  ~~>

293

///  __0

294

///

295

///  new variables:

296

///  find __0: bool

297

///

298

///  new clauses:

299

///  clause(__0, not(a), not(b), not(c), ...)

300

///  clause(not(__0), a)

301

///  clause(not(__0), b)

302

///  clause(not(__0), c)

303

///  ...

304

///

305

///  ---------------------------------------

306

///

307

///  clause(a, b, c, ...)

308

///  ~~>

309

///  __0

310

///

311

///  new variables:

312

///  find __0: bool

313

///

314

///  new clauses:

315

///  clause(not(__0), a, b, c, ...)

316

///  clause(__0, not(a))

317

///  clause(__0, not(b))

318

///  clause(__0, not(c))

319

///  ...

320

/// ```

321

#[register_rule("SAT", 8500, [And, Or])]

322

375615

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

323

375615

    let exprs = match expr {

324

1926

        Expr::And(_, exprs) | Expr::Or(_, exprs) => exprs,

325

373689

        _ => return Err(RuleNotApplicable),

326

};

327

328

1926

    let Expr::AbstractLiteral(_, Matrix(exprs_list, _)) = exprs.as_ref() else {

329

96

        return Err(RuleNotApplicable);

330

};

331

332

3924

    for x in exprs_list {

333

3924

        if !is_literal(x) {

334

141

            return Err(RuleNotApplicable);

335

3783

};

336

337

338

    let new_expr;

339

1689

    let mut new_clauses = vec![];

340

1689

    let mut new_symbols = symbols.clone();

341

342

1689

    match expr {

343

441

        Expr::And(_, _) => {

344

441

            new_expr = tseytin_and(exprs_list, &mut new_clauses, &mut new_symbols);

345

441

346

1248

        Expr::Or(_, _) => {

347

1248

            new_expr = tseytin_or(exprs_list, &mut new_clauses, &mut new_symbols);

348

1248

349

        _ => return Err(RuleNotApplicable),

350

};

351

352

1689

    Ok(Reduction::cnf(new_expr, new_clauses, new_symbols))

353

375615

354

355

/// Converts a not expression to an aux variable, using the tseytin transformation

356

///

357

/// ```text

358

///  not(a)

359

///  ~~>

360

///  __0

361

///

362

///  new variables:

363

///  find __0: bool

364

///

365

///  new clauses:

366

///  clause(__0, a)

367

///  clause(not(__0), not(a))

368

/// ```

369

#[register_rule("SAT", 9005, [Not])]

370

785304

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

371

785304

    let Expr::Not(_, x) = expr else {

372

781980

        return Err(RuleNotApplicable);

373

};

374

375

3324

    let Expr::Atomic(_, _) = x.as_ref() else {

376

2760

        return Err(RuleNotApplicable);

377

};

378

379

564

    if !is_literal(x.as_ref()) {

380

        return Err(RuleNotApplicable);

381

564

};

382

383

564

    let mut new_clauses = vec![];

384

564

    let mut new_symbols = symbols.clone();

385

386

564

    let new_expr = tseytin_not(x.as_ref().clone(), &mut new_clauses, &mut new_symbols);

387

388

564

    Ok(Reduction::cnf(new_expr, new_clauses, new_symbols))

389

785304

390

391

/// Converts an iff/boolean equality expression to an aux variable, using the tseytin transformation

392

///

393

/// ```text

394

/// find a, b : bool

395

///  a <-> b OR a = b

396

///  ~~>

397

///  __0

398

///

399

///  new clauses:

400

///  find __0: bool

401

///

402

///  new clauses:

403

///  clause(not(a), not(b), __0)

404

///  clause(a, b, __0)

405

///  clause(a, not(b), not(__0))

406

///  clause(not(a), b, not(__0))

407

/// ```

408

#[register_rule("SAT", 8500, [Iff, Eq])]

409

375615

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

410

    // Check for iff or eq

411

375615

    let (x, y) = match expr {

412

2427

        Expr::Iff(_, x, y) | Expr::Eq(_, x, y) => (x, y),

413

373188

        _ => return Err(RuleNotApplicable),

414

};

415

416

2427

    if !is_literal(x.as_ref()) || !is_literal(y.as_ref()) {

417

2391

        return Err(RuleNotApplicable);

418

36

};

419

420

36

    let mut new_clauses = vec![];

421

36

    let mut new_symbols = symbols.clone();

422

423

36

    let new_expr = tseytin_iff(

424

36

        x.as_ref().clone(),

425

36

        y.as_ref().clone(),

426

36

        &mut new_clauses,

427

36

        &mut new_symbols,

428

);

429

430

36

    Ok(Reduction::cnf(new_expr, new_clauses, new_symbols))

431

375615

432

433

/// Converts an implication expression to an aux variable, using the tseytin transformation

434

///

435

/// ```text

436

///  a -> b

437

///  ~~>

438

///  __0

439

///

440

///  new variables:

441

///  find __0: bool

442

///

443

///  new clauses:

444

///  clause(not(__0), not(a), b)

445

///  clause(__0, a)

446

///  clause(__0, not(b))

447

/// ```

448

#[register_rule("SAT", 8500, [Imply])]

449

375615

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

450

375615

    let Expr::Imply(_, x, y) = expr else {

451

375315

        return Err(RuleNotApplicable);

452

};

453

454

300

    if !is_literal(x.as_ref()) || !is_literal(y.as_ref()) {

455

144

        return Err(RuleNotApplicable);

456

156

};

457

458

    let new_expr;

459

156

    let mut new_clauses = vec![];

460

156

    let mut new_symbols = symbols.clone();

461

462

156

    new_expr = tseytin_imply(

463

156

        x.as_ref().clone(),

464

156

        y.as_ref().clone(),

465

156

        &mut new_clauses,

466

156

        &mut new_symbols,

467

);

468

469

156

    Ok(Reduction::cnf(new_expr, new_clauses, new_symbols))

470

375615

471

472

/// Converts a boolean != expression to an aux variable, using the tseytin transformation

473

///

474

/// ```text

475

///  find a, b : bool

476

///  a != b

477

///  ~~>

478

///  __0

479

///

480

///  new clauses:

481

///  find __0: bool

482

///

483

///  new clauses:

484

///  clause(not(a), not(b), not(__0))

485

///  clause(a, b, not(__0))

486

///  clause(a, not(b), __0)

487

///  clause(not(a), b, __0)

488

/// ```

489

#[register_rule("SAT", 8500, [Neq])]

490

375615

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

491

375615

    let Expr::Neq(_, x, y) = expr else {

492

374199

        return Err(RuleNotApplicable);

493

};

494

495

1416

    if !is_literal(x.as_ref()) || !is_literal(y.as_ref()) {

496

1380

        return Err(RuleNotApplicable);

497

36

};

498

499

36

    let mut new_clauses = vec![];

500

36

    let mut new_symbols = symbols.clone();

501

502

36

    let new_expr = tseytin_xor(

503

36

        x.as_ref().clone(),

504

36

        y.as_ref().clone(),

505

36

        &mut new_clauses,

506

36

        &mut new_symbols,

507

);

508

509

36

    Ok(Reduction::cnf(new_expr, new_clauses, new_symbols))

510

375615