Grcov report - boolean.rs

1

use conjure_cp::essence_expr;

2

use conjure_cp::rule_engine::register_rule_set;

3

use conjure_cp::solver::SolverFamily;

4

5

use conjure_cp::ast::Metadata;

6

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

7

use conjure_cp::rule_engine::{

8

    ApplicationError::RuleNotApplicable, ApplicationResult, Reduction, register_rule,

9

};

10

11

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

12

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

13

14

use crate::utils::is_literal;

15

16

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

17

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

18

19

    symbols.insert(name.clone());

20

21

    Expr::Atomic(

22

        Metadata::new(),

23

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

24

25

26

27

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

28

    let mut new_terms = vec![];

29

    for expr in exprs {

30

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

31

            // true ~~> entire or is true

32

            // false ~~> remove false from the or

33

            if x {

34

                return None;

35

36

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

37

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

38

                // check for nested literal

39

                if !x {

40

                    return None;

41

42

            } else {

43

                new_terms.push(expr);

44

45

        } else {

46

            new_terms.push(expr);

47

48

49

50

    Some(CnfClause::new(new_terms))

51

52

53

// TODO: Optimize all logic operators for constants

54

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

55

56

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

57

pub fn tseytin_and(

58

    exprs: &Vec<Expr>,

59

    clauses: &mut Vec<CnfClause>,

60

    symbols: &mut SymbolTable,

61

) -> Expr {

62

    let new_expr = create_bool_aux(symbols);

63

64

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

65

66

    for x in exprs {

67

        clauses.extend(create_clause(vec![

68

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

69

            x.clone(),

70

        ]));

71

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

72

73

    clauses.extend(create_clause(full_conj));

74

75

    new_expr

76

77

78

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

79

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

80

    let new_expr = create_bool_aux(symbols);

81

82

    clauses.extend(create_clause(vec![

83

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

84

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

85

    ]));

86

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

87

88

    new_expr

89

90

91

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

92

pub fn tseytin_or(

93

    exprs: &Vec<Expr>,

94

    clauses: &mut Vec<CnfClause>,

95

    symbols: &mut SymbolTable,

96

) -> Expr {

97

    let new_expr = create_bool_aux(symbols);

98

99

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

100

101

    for x in exprs {

102

        clauses.extend(create_clause(vec![

103

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

104

            new_expr.clone(),

105

        ]));

106

        full_conj.push(x.clone());

107

108

109

    clauses.extend(create_clause(full_conj));

110

111

    new_expr

112

113

114

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

115

pub fn tseytin_iff(

116

    x: Expr,

117

    y: Expr,

118

    clauses: &mut Vec<CnfClause>,

119

    symbols: &mut SymbolTable,

120

) -> Expr {

121

    let new_expr = create_bool_aux(symbols);

122

123

    clauses.extend(create_clause(vec![

124

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

125

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

126

        new_expr.clone(),

127

    ]));

128

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

129

    clauses.extend(create_clause(vec![

130

        x.clone(),

131

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

132

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

133

    ]));

134

    clauses.extend(create_clause(vec![

135

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

136

y,

137

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

138

    ]));

139

140

    new_expr

141

142

143

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

144

pub fn tseytin_imply(

145

    x: Expr,

146

    y: Expr,

147

    clauses: &mut Vec<CnfClause>,

148

    symbols: &mut SymbolTable,

149

) -> Expr {

150

    let new_expr = create_bool_aux(symbols);

151

152

    clauses.extend(create_clause(vec![

153

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

154

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

155

        y.clone(),

156

    ]));

157

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

158

    clauses.extend(create_clause(vec![

159

        new_expr.clone(),

160

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

161

    ]));

162

163

    new_expr

164

165

166

/// Applies the Tseytin multiplex transformation

167

/// cond ? b : a

168

///

169

/// cond = 1 => b

170

/// cond = 0 => a

171

#[allow(dead_code)]

172

pub fn tseytin_mux(

173

    cond: Expr,

174

    a: Expr,

175

    b: Expr,

176

    clauses: &mut Vec<CnfClause>,

177

    symbols: &mut SymbolTable,

178

) -> Expr {

179

    let new_expr = create_bool_aux(symbols);

180

181

    clauses.extend(create_clause(vec![

182

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

183

        cond.clone(),

184

        a.clone(),

185

    ]));

186

    clauses.extend(create_clause(vec![

187

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

188

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

189

        b.clone(),

190

    ]));

191

    clauses.extend(create_clause(vec![

192

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

193

        a.clone(),

194

        b.clone(),

195

    ]));

196

197

    clauses.extend(create_clause(vec![

198

        new_expr.clone(),

199

        cond.clone(),

200

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

201

    ]));

202

    clauses.extend(create_clause(vec![

203

        new_expr.clone(),

204

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

205

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

206

    ]));

207

    clauses.extend(create_clause(vec![

208

        new_expr.clone(),

209

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

210

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

211

    ]));

212

213

    new_expr

214

215

216

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

217

#[allow(dead_code)]

218

pub fn tseytin_xor(

219

    x: Expr,

220

    y: Expr,

221

    clauses: &mut Vec<CnfClause>,

222

    symbols: &mut SymbolTable,

223

) -> Expr {

224

    let new_expr = create_bool_aux(symbols);

225

226

    clauses.extend(create_clause(vec![

227

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

228

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

229

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

230

    ]));

231

    clauses.extend(create_clause(vec![

232

        x.clone(),

233

        y.clone(),

234

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

235

    ]));

236

    clauses.extend(create_clause(vec![

237

        x.clone(),

238

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

239

        new_expr.clone(),

240

    ]));

241

    clauses.extend(create_clause(vec![

242

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

243

y,

244

        new_expr.clone(),

245

    ]));

246

247

    new_expr

248

249

250

// BOOLEAN SAT ENCODING RULES:

251

252

register_rule_set!("SAT", ("Base"), |f: &SolverFamily| matches!(

253

f,

254

    SolverFamily::Sat

255

));

256

257

/// Converts a single boolean atom to a clause

258

///

259

/// ```text

260

///  a

261

///  ~~>

262

///

263

///  new clauses:

264

///  clause(a)

265

/// ```

266

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

267

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

268

    // The single atom must not be within another expression

269

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

270

        return Err(RuleNotApplicable);

271

};

272

273

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

274

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

275

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

276

    ) else {

277

        return Err(RuleNotApplicable);

278

};

279

280

    // Clone the children since expr is borrowed immutably

281

    let mut new_children = children.clone();

282

283

    let removed = new_children.remove(pos);

284

285

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

286

287

    // If now empty, replace with `true`

288

    if new_children.is_empty() {

289

        new_children.push(essence_expr!(true));

290

291

292

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

293

294

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

295

296

297

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

298

///

299

/// ```text

300

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

301

///  ~~>

302

///  __0

303

///

304

///  new variables:

305

///  find __0: bool

306

///

307

///  new clauses:

308

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

309

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

310

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

311

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

312

///  ...

313

///

314

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

315

///

316

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

317

///  ~~>

318

///  __0

319

///

320

///  new variables:

321

///  find __0: bool

322

///

323

///  new clauses:

324

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

325

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

326

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

327

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

328

///  ...

329

/// ```

330

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

331

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

332

    let exprs = match expr {

333

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

334

        _ => return Err(RuleNotApplicable),

335

};

336

337

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

338

        return Err(RuleNotApplicable);

339

};

340

341

    for x in exprs_list {

342

        if !is_literal(x) {

343

            return Err(RuleNotApplicable);

344

};

345

346

347

    let new_expr;

348

    let mut new_clauses = vec![];

349

    let mut new_symbols = symbols.clone();

350

351

    match expr {

352

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

353

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

354

355

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

356

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

357

358

        _ => return Err(RuleNotApplicable),

359

};

360

361

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

362

363

364

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

365

///

366

/// ```text

367

///  not(a)

368

///  ~~>

369

///  __0

370

///

371

///  new variables:

372

///  find __0: bool

373

///

374

///  new clauses:

375

///  clause(__0, a)

376

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

377

/// ```

378

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

379

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

380

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

381

        return Err(RuleNotApplicable);

382

};

383

384

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

385

        return Err(RuleNotApplicable);

386

};

387

388

    if !is_literal(x.as_ref()) {

389

        return Err(RuleNotApplicable);

390

};

391

392

    let mut new_clauses = vec![];

393

    let mut new_symbols = symbols.clone();

394

395

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

396

397

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

398

399

400

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

401

///

402

/// ```text

403

///  a <-> b

404

///  ~~>

405

///  __0

406

///

407

///  new clauses:

408

///  find __0: bool

409

///

410

///  new clauses:

411

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

412

///  clause(a, b, __0)

413

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

414

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

415

/// ```

416

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

417

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

418

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

419

        return Err(RuleNotApplicable);

420

};

421

422

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

423

        return Err(RuleNotApplicable);

424

};

425

426

    let mut new_clauses = vec![];

427

    let mut new_symbols = symbols.clone();

428

429

    let new_expr = tseytin_iff(

430

        x.as_ref().clone(),

431

        y.as_ref().clone(),

432

        &mut new_clauses,

433

        &mut new_symbols,

434

);

435

436

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

437

438

439

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

440

///

441

/// ```text

442

///  a -> b

443

///  ~~>

444

///  __0

445

///

446

///  new variables:

447

///  find __0: bool

448

///

449

///  new clauses:

450

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

451

///  clause(__0, a)

452

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

453

/// ```

454

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

455

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

456

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

457

        return Err(RuleNotApplicable);

458

};

459

460

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

461

        return Err(RuleNotApplicable);

462

};

463

464

    let new_expr;

465

    let mut new_clauses = vec![];

466

    let mut new_symbols = symbols.clone();

467

468

    new_expr = tseytin_imply(

469

        x.as_ref().clone(),

470

        y.as_ref().clone(),

471

        &mut new_clauses,

472

        &mut new_symbols,

473

);

474

475

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

476