CBMC: /home/runner/work/cbmc/cbmc/src/solvers/sat/cnf.cpp Source File

23 void cnft::gate_and(literalt a, literalt b, literalt o)

24{

25 // a*b=c <==> (a + o')( b + o')(a'+b'+o)

26 bvt lits(2);

27

28 lits[0]=pos(a);

29 lits[1]=neg(o);

30 lcnf(lits);

31

32 lits[0]=pos(b);

33 lits[1]=neg(o);

34 lcnf(lits);

35

36 lits.clear();

37 lits.reserve(3);

38 lits.push_back(neg(a));

39 lits.push_back(neg(b));

40 lits.push_back(pos(o));

41 lcnf(lits);

42}

46 void cnft::gate_or(literalt a, literalt b, literalt o)

47{

48 // a+b=c <==> (a' + c)( b' + c)(a + b + c')

49 bvt lits(2);

50

51 lits[0]=neg(a);

52 lits[1]=pos(o);

53 lcnf(lits);

54

55 lits[0]=neg(b);

56 lits[1]=pos(o);

57 lcnf(lits);

58

59 lits.resize(3);

60 lits[0]=pos(a);

61 lits[1]=pos(b);

62 lits[2]=neg(o);

63 lcnf(lits);

64}

68 void cnft::gate_xor(literalt a, literalt b, literalt o)

69{

70 // a xor b = o <==> (a' + b' + o')

71 // (a + b + o' )

72 // (a' + b + o)

73 // (a + b' + o)

74 bvt lits(3);

75

76 lits[0]=neg(a);

77 lits[1]=neg(b);

78 lits[2]=neg(o);

79 lcnf(lits);

80

81 lits[0]=pos(a);

82 lits[1]=pos(b);

83 lits[2]=neg(o);

84 lcnf(lits);

85

86 lits[0]=neg(a);

87 lits[1]=pos(b);

88 lits[2]=pos(o);

89 lcnf(lits);

90

91 lits[0]=pos(a);

92 lits[1]=neg(b);

93 lits[2]=pos(o);

94 lcnf(lits);

95}

99 void cnft::gate_nand(literalt a, literalt b, literalt o)

100{

101 // a Nand b = o <==> (a + o)( b + o)(a' + b' + o')

102 bvt lits(2);

103

104 lits[0]=pos(a);

105 lits[1]=pos(o);

106 lcnf(lits);

107

108 lits[0]=pos(b);

109 lits[1]=pos(o);

110 lcnf(lits);

111

112 lits.resize(3);

113 lits[0]=neg(a);

114 lits[1]=neg(b);

115 lits[2]=neg(o);

116 lcnf(lits);

117}

121 void cnft::gate_nor(literalt a, literalt b, literalt o)

122{

123 // a Nor b = o <==> (a' + o')( b' + o')(a + b + o)

124 bvt lits(2);

125

126 lits[0]=neg(a);

127 lits[1]=neg(o);

128 lcnf(lits);

129

130 lits[0]=neg(b);

131 lits[1]=neg(o);

132 lcnf(lits);

133

134 lits.resize(3);

135 lits[0]=pos(a);

136 lits[1]=pos(b);

137 lits[2]=pos(o);

138 lcnf(lits);

139}

143 void cnft::gate_equal(literalt a, literalt b, literalt o)

144{

145 gate_xor(a, b, !o);

146}

150 void cnft::gate_implies(literalt a, literalt b, literalt o)

151{

152 gate_or(!a, b, o);

153}

158 literalt cnft::land(const bvt &bv)

159{

160 if(bv.empty())

161 return const_literal(true);

162 if(bv.size()==1)

163 return bv[0];

164 if(bv.size()==2)

165 return land(bv[0], bv[1]);

166

167 for(const auto &l : bv)

168 if(l.is_false())

169 return l;

170

171 if(is_all(bv, const_literal(true)))

172 return const_literal(true);

173

174 bvt new_bv=eliminate_duplicates(bv);

175

176 bvt lits(2);

177 literalt literal=new_variable();

178 lits[1]=neg(literal);

179

180 for(const auto &l : new_bv)

181 {

182 lits[0]=pos(l);

183 lcnf(lits);

184 }

185

186 lits.clear();

187 lits.reserve(new_bv.size()+1);

188

189 for(const auto &l : new_bv)

190 lits.push_back(neg(l));

191

192 lits.push_back(pos(literal));

193 lcnf(lits);

194

195 return literal;

196}

201 literalt cnft::lor(const bvt &bv)

202{

203 if(bv.empty())

204 return const_literal(false);

205 if(bv.size()==1)

206 return bv[0];

207 if(bv.size()==2)

208 return lor(bv[0], bv[1]);

209

210 for(const auto &l : bv)

211 if(l.is_true())

212 return l;

213

214 if(is_all(bv, const_literal(false)))

215 return const_literal(false);

216

217 bvt new_bv=eliminate_duplicates(bv);

218

219 bvt lits(2);

220 literalt literal=new_variable();

221 lits[1]=pos(literal);

222

223 for(const auto &l : new_bv)

224 {

225 lits[0]=neg(l);

226 lcnf(lits);

227 }

228

229 lits.clear();

230 lits.reserve(new_bv.size()+1);

231

232 for(const auto &l : new_bv)

233 lits.push_back(pos(l));

234

235 lits.push_back(neg(literal));

236 lcnf(lits);

237

238 return literal;

239}

244 literalt cnft::lxor(const bvt &bv)

245{

246 if(bv.empty())

247 return const_literal(false);

248 if(bv.size()==1)

249 return bv[0];

250 if(bv.size()==2)

251 return lxor(bv[0], bv[1]);

252

253 literalt literal=const_literal(false);

254

255 for(const auto &l : bv)

256 literal=lxor(l, literal);

257

258 return literal;

259}

263 literalt cnft::land(literalt a, literalt b)

264{

265 if(a.is_true() || b.is_false())

266 return b;

267 if(b.is_true() || a.is_false())

268 return a;

269 if(a==b)

270 return a;

271

272 literalt o=new_variable();

273 gate_and(a, b, o);

274 return o;

275}

279 literalt cnft::lor(literalt a, literalt b)

280{

281 if(a.is_false() || b.is_true())

282 return b;

283 if(b.is_false() || a.is_true())

284 return a;

285 if(a==b)

286 return a;

287

288 literalt o=new_variable();

289 gate_or(a, b, o);

290 return o;

291}

295 literalt cnft::lxor(literalt a, literalt b)

296{

297 if(a.is_false())

298 return b;

299 if(b.is_false())

300 return a;

301 if(a.is_true())

302 return !b;

303 if(b.is_true())

304 return !a;

305 if(a==b)

306 return const_literal(false);

307 if(a==!b)

308 return const_literal(true);

309

310 literalt o=new_variable();

311 gate_xor(a, b, o);

312 return o;

313}

317 literalt cnft::lnand(literalt a, literalt b)

318{

319 return !land(a, b);

320}

324 literalt cnft::lnor(literalt a, literalt b)

325{

326 return !lor(a, b);

327}

329 literalt cnft::lequal(literalt a, literalt b)

330{

331 return !lxor(a, b);

332}

334 literalt cnft::limplies(literalt a, literalt b)

335{

336 return lor(!a, b);

337}

344 literalt cnft::lselect(literalt a, literalt b, literalt c)

345{

346 // a?b:c = (a AND b) OR (/a AND c)

347 if(a.is_constant())

348 return a.sign() ? b : c;

349 if(b==c)

350 return b;

351

352 if(b.is_constant())

353 return b.sign() ? lor(a, c) : land(!a, c);

354 if(c.is_constant())

355 return c.sign() ? lor(!a, b) : land(a, b);

356

357 #ifdef COMPACT_ITE

358

359 // (a+c'+o) (a+c+o') (a'+b'+o) (a'+b+o')

360

361 literalt o=new_variable();

362

363 bvt lits;

364

365 lcnf(a, !c, o);

366 lcnf(a, c, !o);

367 lcnf(!a, !b, o);

368 lcnf(!a, b, !o);

369

370 #ifdef OPTIMAL_COMPACT_ITE

371 // additional clauses to enable better propagation

372 lcnf(b, c, !o);

373 lcnf(!b, !c, o);

374 #endif

375

376 return o;

377

378 #else

379 return lor(land(a, b), land(!a, c));

380 #endif

381}

385 literalt cnft::new_variable()

386{

387 literalt l(_no_variables, false);

388

389 set_no_variables(_no_variables+1);

390

391 return l;

392}

396 bvt cnft::new_variables(std::size_t width)

397{

398 bvt result;

399 result.reserve(width);

400

401 for(std::size_t i = _no_variables; i < _no_variables + width; ++i)

402 result.emplace_back(i, false);

403

404 set_no_variables(_no_variables + width);

405

406 return result;

407}

412 bvt cnft::eliminate_duplicates(const bvt &bv)

413{

414 bvt dest = bv;

415 std::sort(dest.begin(), dest.end());

416 auto last = std::unique(dest.begin(), dest.end());

417 dest.erase(last, dest.end());

418

419 return dest;

420}

424 bool cnft::process_clause(const bvt &bv, bvt &dest) const

425{

426 dest.clear();

427

428 // empty clause! this is UNSAT

429 if(bv.empty())

430 return false;

431

432 // first check simple things

433

434 for(const auto &l : bv)

435 {

436 // we never use index 0

437 INVARIANT(l.var_no() != 0, "variable 0 must not be used");

438

439 // we never use 'unused_var_no'

440 INVARIANT(

441 l.var_no() != literalt::unused_var_no(),

442 "variable 'unused_var_no' must not be used");

443

444 if(l.is_true())

445 return true; // clause satisfied

446

447 if(l.is_false())

448 continue; // will remove later

449

450 INVARIANT(

451 l.var_no() < _no_variables,

452 "unknown variable " + std::to_string(l.var_no()) +

453 " (no_variables = " + std::to_string(_no_variables) + " )");

454 }

455

456 // now copy

457 dest.clear();

458 dest.reserve(bv.size());

459

460 for(const auto &l : bv)

461 {

462 if(l.is_false())

463 continue; // remove

464

465 dest.push_back(l);

466 }

467

468 // now sort

469 std::sort(dest.begin(), dest.end());

470

471 // eliminate duplicates and find occurrences of a variable

472 // and its negation

473

474 if(dest.size()>=2)

475 {

476 bvt::iterator it=dest.begin();

477 literalt previous=*it;

478

479 for(it++;

480 it!=dest.end();

481 ) // no it++

482 {

483 literalt l=*it;

484

485 // prevent duplicate literals

486 if(l==previous)

487 it=dest.erase(it);

488 else if(previous==!l)

489 return true; // clause satisfied trivially

490 else

491 {

492 previous=l;

493 it++;

494 }

495 }

496 }

497

498 return false;

499}

ai_baset::clear

virtual void clear()

Reset the abstract state.

Definition ai.h:269

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

cnft::is_all

static bool is_all(const bvt &bv, literalt l)

Definition cnf.h:61

cnft::gate_equal

void gate_equal(literalt a, literalt b, literalt o)

Tseitin encoding of equality between two literals.

Definition cnf.cpp:143

cnft::process_clause

bool process_clause(const bvt &bv, bvt &dest) const

filter 'true' from clause, eliminate duplicates, recognise trivially satisfied clauses

Definition cnf.cpp:424

cnft::new_variables

bvt new_variables(std::size_t width) override

Generate a vector of new variables.

Definition cnf.cpp:396

cnft::gate_or

void gate_or(literalt a, literalt b, literalt o)

Tseitin encoding of disjunction of two literals.

Definition cnf.cpp:46

cnft::limplies

virtual literalt limplies(literalt a, literalt b) override

Definition cnf.cpp:334

cnft::lselect

virtual literalt lselect(literalt a, literalt b, literalt c) override

Definition cnf.cpp:344

cnft::set_no_variables

virtual void set_no_variables(size_t no)

Definition cnf.h:43

cnft::eliminate_duplicates

static bvt eliminate_duplicates(const bvt &)

eliminate duplicates from given vector of literals

Definition cnf.cpp:412

cnft::gate_nand

void gate_nand(literalt a, literalt b, literalt o)

Tseitin encoding of NAND of two literals.

Definition cnf.cpp:99

cnft::new_variable

virtual literalt new_variable() override

Generate a new variable and return it as a literal.

Definition cnf.cpp:385

cnft::gate_xor

void gate_xor(literalt a, literalt b, literalt o)

Tseitin encoding of XOR of two literals.

Definition cnf.cpp:68

cnft::gate_nor

void gate_nor(literalt a, literalt b, literalt o)

Tseitin encoding of NOR of two literals.

Definition cnf.cpp:121

cnft::_no_variables

size_t _no_variables

Definition cnf.h:57

cnft::lequal

virtual literalt lequal(literalt a, literalt b) override

Definition cnf.cpp:329

cnft::land

virtual literalt land(literalt a, literalt b) override

Definition cnf.cpp:263

cnft::gate_implies

void gate_implies(literalt a, literalt b, literalt o)

Tseitin encoding of implication between two literals.

Definition cnf.cpp:150

cnft::lxor

virtual literalt lxor(const bvt &bv) override

Tseitin encoding of XOR between multiple literals.

Definition cnf.cpp:244

cnft::gate_and

void gate_and(literalt a, literalt b, literalt o)

Tseitin encoding of conjunction of two literals.

Definition cnf.cpp:23

cnft::lnand

virtual literalt lnand(literalt a, literalt b) override

Definition cnf.cpp:317

cnft::lnor

virtual literalt lnor(literalt a, literalt b) override

Definition cnf.cpp:324

cnft::lor

virtual literalt lor(literalt a, literalt b) override

Definition cnf.cpp:279

literalt

Definition literal.h:26

literalt::unused_var_no

static var_not unused_var_no()

Definition literal.h:176

propt::lcnf

void lcnf(literalt l0, literalt l1)

Definition prop.h:58

cnf.h

CNF Generation, via Tseitin.

neg

literalt neg(literalt a)

Definition literal.h:193

bvt

std::vector< literalt > bvt

Definition literal.h:201

const_literal

literalt const_literal(bool value)

Definition literal.h:188

pos

literalt pos(literalt a)

Definition literal.h:194

invariant.h

INVARIANT

#define INVARIANT(CONDITION, REASON)

This macro uses the wrapper function 'invariant_violated_string'.

Definition invariant.h:423