GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/cnf_stream.cpp Lines: 381 408 93.4 %
Date: 2021-03-23 Branches: 729 1940 37.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cnf_stream.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Haniel Barbosa, Liana Hadarean
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief A CNF converter that takes in asserts and has the side effect
13
 ** of given an equisatisfiable stream of assertions to PropEngine.
14
 **
15
 ** A CNF converter that takes in asserts and has the side effect
16
 ** of given an equisatisfiable stream of assertions to PropEngine.
17
 **/
18
#include "prop/cnf_stream.h"
19
20
#include <queue>
21
22
#include "base/check.h"
23
#include "base/output.h"
24
#include "expr/node.h"
25
#include "options/bv_options.h"
26
#include "proof/clause_id.h"
27
#include "proof/cnf_proof.h"
28
#include "proof/proof_manager.h"
29
#include "proof/sat_proof.h"
30
#include "prop/minisat/minisat.h"
31
#include "prop/prop_engine.h"
32
#include "prop/theory_proxy.h"
33
#include "smt/dump.h"
34
#include "smt/smt_engine.h"
35
#include "printer/printer.h"
36
#include "smt/smt_engine_scope.h"
37
#include "theory/theory.h"
38
#include "theory/theory_engine.h"
39
40
namespace CVC4 {
41
namespace prop {
42
43
18038
CnfStream::CnfStream(SatSolver* satSolver,
44
                     Registrar* registrar,
45
                     context::Context* context,
46
                     OutputManager* outMgr,
47
                     ResourceManager* rm,
48
                     FormulaLitPolicy flpol,
49
18038
                     std::string name)
50
    : d_satSolver(satSolver),
51
      d_outMgr(outMgr),
52
      d_booleanVariables(context),
53
      d_notifyFormulas(context),
54
      d_nodeToLiteralMap(context),
55
      d_literalToNodeMap(context),
56
      d_flitPolicy(flpol),
57
      d_registrar(registrar),
58
      d_name(name),
59
      d_cnfProof(nullptr),
60
      d_removable(false),
61
18038
      d_resourceManager(rm)
62
{
63
18038
}
64
65
9021217
bool CnfStream::assertClause(TNode node, SatClause& c)
66
{
67
9021217
  Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n";
68
9021217
  if (Dump.isOn("clauses") && d_outMgr != nullptr)
69
  {
70
    const Printer& printer = d_outMgr->getPrinter();
71
    std::ostream& out = d_outMgr->getDumpOut();
72
    if (c.size() == 1)
73
    {
74
      printer.toStreamCmdAssert(out, getNode(c[0]));
75
    }
76
    else
77
    {
78
      Assert(c.size() > 1);
79
      NodeBuilder<> b(kind::OR);
80
      for (unsigned i = 0; i < c.size(); ++i)
81
      {
82
        b << getNode(c[i]);
83
      }
84
      Node n = b;
85
      printer.toStreamCmdAssert(out, n);
86
    }
87
  }
88
89
9021217
  ClauseId clauseId = d_satSolver->addClause(c, d_removable);
90
91
9021217
  if (d_cnfProof && clauseId != ClauseIdUndef)
92
  {
93
250012
    d_cnfProof->registerConvertedClause(clauseId);
94
  }
95
9021217
  return clauseId != ClauseIdUndef;
96
}
97
98
243409
bool CnfStream::assertClause(TNode node, SatLiteral a)
99
{
100
486818
  SatClause clause(1);
101
243409
  clause[0] = a;
102
486818
  return assertClause(node, clause);
103
}
104
105
3747955
bool CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b)
106
{
107
7495910
  SatClause clause(2);
108
3747955
  clause[0] = a;
109
3747955
  clause[1] = b;
110
7495910
  return assertClause(node, clause);
111
}
112
113
2973735
bool CnfStream::assertClause(TNode node,
114
                             SatLiteral a,
115
                             SatLiteral b,
116
                             SatLiteral c)
117
{
118
5947470
  SatClause clause(3);
119
2973735
  clause[0] = a;
120
2973735
  clause[1] = b;
121
2973735
  clause[2] = c;
122
5947470
  return assertClause(node, clause);
123
}
124
125
95126335
bool CnfStream::hasLiteral(TNode n) const {
126
95126335
  NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n);
127
95126335
  return find != d_nodeToLiteralMap.end();
128
}
129
130
173259
void CnfStream::ensureMappingForLiteral(TNode n)
131
{
132
173259
  SatLiteral lit = getLiteral(n);
133
173259
  if (!d_literalToNodeMap.contains(lit))
134
  {
135
    // Store backward-mappings
136
    d_literalToNodeMap.insert(lit, n);
137
    d_literalToNodeMap.insert(~lit, n.notNode());
138
  }
139
173259
}
140
141
234457
void CnfStream::ensureLiteral(TNode n)
142
{
143
234457
  AlwaysAssertArgument(
144
      hasLiteral(n) || n.getType().isBoolean(),
145
      n,
146
      "ProofCnfStream::ensureLiteral() requires a node of Boolean type.\n"
147
      "got node: %s\n"
148
      "its type: %s\n",
149
      n.toString().c_str(),
150
      n.getType().toString().c_str());
151
234457
  Trace("cnf") << "ensureLiteral(" << n << ")\n";
152
234457
  if (hasLiteral(n))
153
  {
154
155005
    ensureMappingForLiteral(n);
155
155005
    return;
156
  }
157
  // remove top level negation
158
79452
  n = n.getKind() == kind::NOT ? n[0] : n;
159
79452
  if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
160
  {
161
    // If we were called with something other than a theory atom (or
162
    // Boolean variable), we get a SatLiteral that is definitionally
163
    // equal to it.
164
    //
165
    // We are setting the current assertion to be null. This is because `toCNF`
166
    // may add clauses to the SAT solver and we look up the current assertion
167
    // in that case. Setting it to null ensures that the assertion stack is
168
    // non-empty and that we are not associating a bogus assertion with the
169
    // clause. This should be ok because we use the mapping back to assertions
170
    // for clauses from input assertions only.
171
79
    if (d_cnfProof)
172
    {
173
4
      d_cnfProof->pushCurrentAssertion(Node::null());
174
    }
175
    // These are not removable and have no proof ID
176
79
    d_removable = false;
177
178
79
    SatLiteral lit = toCNF(n, false);
179
180
79
    if (d_cnfProof)
181
    {
182
4
      d_cnfProof->popCurrentAssertion();
183
    }
184
185
    // Store backward-mappings
186
    // These may already exist
187
79
    d_literalToNodeMap.insert_safe(lit, n);
188
79
    d_literalToNodeMap.insert_safe(~lit, n.notNode());
189
  }
190
  else
191
  {
192
    // We have a theory atom or variable.
193
79373
    convertAtom(n);
194
  }
195
}
196
197
2646556
SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) {
198
5293112
  Trace("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom
199
2646556
               << ")\n"
200
2646556
               << push;
201
2646556
  Assert(node.getKind() != kind::NOT);
202
203
  // if we are tracking formulas, everything is a theory atom
204
2646556
  if (!isTheoryAtom && d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY)
205
  {
206
    isTheoryAtom = true;
207
    d_notifyFormulas.insert(node);
208
  }
209
210
  // Get the literal for this node
211
2646556
  SatLiteral lit;
212
2646556
  if (!hasLiteral(node)) {
213
2646547
    Trace("cnf") << d_name << "::newLiteral: node already registered\n";
214
    // If no literal, we'll make one
215
2646547
    if (node.getKind() == kind::CONST_BOOLEAN) {
216
18427
      Trace("cnf") << d_name << "::newLiteral: boolean const\n";
217
18427
      if (node.getConst<bool>()) {
218
9168
        lit = SatLiteral(d_satSolver->trueVar());
219
      } else {
220
9259
        lit = SatLiteral(d_satSolver->falseVar());
221
      }
222
    } else {
223
2628120
      Trace("cnf") << d_name << "::newLiteral: new var\n";
224
2628120
      lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate));
225
    }
226
2646547
    d_nodeToLiteralMap.insert(node, lit);
227
2646547
    d_nodeToLiteralMap.insert(node.notNode(), ~lit);
228
  } else {
229
9
    lit = getLiteral(node);
230
  }
231
232
  // If it's a theory literal, need to store it for back queries
233
4506092
  if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK
234
4235043
      || (Dump.isOn("clauses")))
235
  {
236
1058069
    d_literalToNodeMap.insert_safe(lit, node);
237
1058069
    d_literalToNodeMap.insert_safe(~lit, node.notNode());
238
  }
239
240
  // If a theory literal, we pre-register it
241
2646556
  if (preRegister) {
242
    // In case we are re-entered due to lemmas, save our state
243
787020
    bool backupRemovable = d_removable;
244
    // Should be fine since cnfProof current assertion is stack based.
245
787024
    d_registrar->preRegister(node);
246
787016
    d_removable = backupRemovable;
247
  }
248
  // Here, you can have it
249
2646552
  Trace("cnf") << "newLiteral(" << node << ") => " << lit << "\n" << pop;
250
2646552
  return lit;
251
}
252
253
17397734
TNode CnfStream::getNode(const SatLiteral& literal) {
254
17397734
  Trace("cnf") << "getNode(" << literal << ")\n";
255
34795468
  Trace("cnf") << "getNode(" << literal << ") => "
256
17397734
               << d_literalToNodeMap[literal] << "\n";
257
17397734
  return d_literalToNodeMap[literal];
258
}
259
260
3508353
const CnfStream::NodeToLiteralMap& CnfStream::getTranslationCache() const
261
{
262
3508353
  return d_nodeToLiteralMap;
263
}
264
265
34735201
const CnfStream::LiteralToNodeMap& CnfStream::getNodeCache() const
266
{
267
34735201
  return d_literalToNodeMap;
268
}
269
270
18959
void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
271
18959
  context::CDList<TNode>::const_iterator it, it_end;
272
86977
  for (it = d_booleanVariables.begin(); it != d_booleanVariables.end(); ++ it) {
273
68018
    outputVariables.push_back(*it);
274
  }
275
18959
}
276
277
bool CnfStream::isNotifyFormula(TNode node) const
278
{
279
  return d_notifyFormulas.find(node) != d_notifyFormulas.end();
280
}
281
282
1826
void CnfStream::setProof(CnfProof* proof) {
283
1826
  Assert(d_cnfProof == NULL);
284
1826
  d_cnfProof = proof;
285
1826
}
286
287
866957
SatLiteral CnfStream::convertAtom(TNode node)
288
{
289
866957
  Trace("cnf") << "convertAtom(" << node << ")\n";
290
291
866957
  Assert(!hasLiteral(node)) << "atom already mapped!";
292
293
866957
  bool theoryLiteral = false;
294
866957
  bool canEliminate = true;
295
866957
  bool preRegister = false;
296
297
  // Is this a variable add it to the list
298
866957
  if (node.isVar() && node.getKind() != kind::BOOLEAN_TERM_VARIABLE)
299
  {
300
79937
    d_booleanVariables.push_back(node);
301
  }
302
  else
303
  {
304
787020
    theoryLiteral = true;
305
787020
    canEliminate = false;
306
787020
    preRegister = true;
307
  }
308
309
  // Make a new literal (variables are not considered theory literals)
310
866961
  SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
311
  // Return the resulting literal
312
866953
  return lit;
313
}
314
315
67636351
SatLiteral CnfStream::getLiteral(TNode node) {
316
67636351
  Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node";
317
318
135272702
  Assert(d_nodeToLiteralMap.contains(node))
319
67636351
      << "Literal not in the CNF Cache: " << node << "\n";
320
321
67636351
  SatLiteral literal = d_nodeToLiteralMap[node];
322
135272702
  Trace("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal
323
67636351
               << "\n";
324
67636351
  return literal;
325
}
326
327
266535
SatLiteral CnfStream::handleXor(TNode xorNode)
328
{
329
266535
  Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
330
266535
  Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!";
331
266535
  Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
332
266535
  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
333
266535
  Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n";
334
335
266535
  SatLiteral a = toCNF(xorNode[0]);
336
266535
  SatLiteral b = toCNF(xorNode[1]);
337
338
266535
  SatLiteral xorLit = newLiteral(xorNode);
339
340
266535
  assertClause(xorNode.negate(), a, b, ~xorLit);
341
266535
  assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
342
266535
  assertClause(xorNode, a, ~b, xorLit);
343
266535
  assertClause(xorNode, ~a, b, xorLit);
344
345
266535
  return xorLit;
346
}
347
348
339963
SatLiteral CnfStream::handleOr(TNode orNode)
349
{
350
339963
  Assert(!hasLiteral(orNode)) << "Atom already mapped!";
351
339963
  Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!";
352
339963
  Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
353
339963
  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
354
339963
  Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n";
355
356
  // Number of children
357
339963
  unsigned n_children = orNode.getNumChildren();
358
359
  // Transform all the children first
360
339963
  TNode::const_iterator node_it = orNode.begin();
361
339963
  TNode::const_iterator node_it_end = orNode.end();
362
679926
  SatClause clause(n_children + 1);
363
1130406
  for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
364
790443
    clause[i] = toCNF(*node_it);
365
  }
366
367
  // Get the literal for this node
368
339963
  SatLiteral orLit = newLiteral(orNode);
369
370
  // lit <- (a_1 | a_2 | a_3 | ... | a_n)
371
  // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
372
  // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
373
1130406
  for(unsigned i = 0; i < n_children; ++i) {
374
790443
    assertClause(orNode, orLit, ~clause[i]);
375
  }
376
377
  // lit -> (a_1 | a_2 | a_3 | ... | a_n)
378
  // ~lit | a_1 | a_2 | a_3 | ... | a_n
379
339963
  clause[n_children] = ~orLit;
380
  // This needs to go last, as the clause might get modified by the SAT solver
381
339963
  assertClause(orNode.negate(), clause);
382
383
  // Return the literal
384
679926
  return orLit;
385
}
386
387
695331
SatLiteral CnfStream::handleAnd(TNode andNode)
388
{
389
695331
  Assert(!hasLiteral(andNode)) << "Atom already mapped!";
390
695331
  Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!";
391
695331
  Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
392
695331
  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
393
695331
  Trace("cnf") << "handleAnd(" << andNode << ")\n";
394
395
  // Number of children
396
695331
  unsigned n_children = andNode.getNumChildren();
397
398
  // Transform all the children first (remembering the negation)
399
695331
  TNode::const_iterator node_it = andNode.begin();
400
695331
  TNode::const_iterator node_it_end = andNode.end();
401
1390662
  SatClause clause(n_children + 1);
402
3548317
  for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
403
2852986
    clause[i] = ~toCNF(*node_it);
404
  }
405
406
  // Get the literal for this node
407
695331
  SatLiteral andLit = newLiteral(andNode);
408
409
  // lit -> (a_1 & a_2 & a_3 & ... & a_n)
410
  // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
411
  // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
412
3548317
  for(unsigned i = 0; i < n_children; ++i) {
413
2852986
    assertClause(andNode.negate(), ~andLit, ~clause[i]);
414
  }
415
416
  // lit <- (a_1 & a_2 & a_3 & ... a_n)
417
  // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
418
  // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
419
695331
  clause[n_children] = andLit;
420
  // This needs to go last, as the clause might get modified by the SAT solver
421
695331
  assertClause(andNode, clause);
422
423
1390662
  return andLit;
424
}
425
426
6519
SatLiteral CnfStream::handleImplies(TNode impliesNode)
427
{
428
6519
  Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
429
6519
  Assert(impliesNode.getKind() == kind::IMPLIES)
430
      << "Expecting an IMPLIES expression!";
431
6519
  Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
432
6519
  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
433
6519
  Trace("cnf") << "handleImplies(" << impliesNode << ")\n";
434
435
  // Convert the children to cnf
436
6519
  SatLiteral a = toCNF(impliesNode[0]);
437
6519
  SatLiteral b = toCNF(impliesNode[1]);
438
439
6519
  SatLiteral impliesLit = newLiteral(impliesNode);
440
441
  // lit -> (a->b)
442
  // ~lit | ~ a | b
443
6519
  assertClause(impliesNode.negate(), ~impliesLit, ~a, b);
444
445
  // (a->b) -> lit
446
  // ~(~a | b) | lit
447
  // (a | l) & (~b | l)
448
6519
  assertClause(impliesNode, a, impliesLit);
449
6519
  assertClause(impliesNode, ~b, impliesLit);
450
451
6519
  return impliesLit;
452
}
453
454
371244
SatLiteral CnfStream::handleIff(TNode iffNode)
455
{
456
371244
  Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
457
371244
  Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!";
458
371244
  Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
459
371244
  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
460
371244
  Trace("cnf") << "handleIff(" << iffNode << ")\n";
461
462
  // Convert the children to CNF
463
371244
  SatLiteral a = toCNF(iffNode[0]);
464
371244
  SatLiteral b = toCNF(iffNode[1]);
465
466
  // Get the now literal
467
371244
  SatLiteral iffLit = newLiteral(iffNode);
468
469
  // lit -> ((a-> b) & (b->a))
470
  // ~lit | ((~a | b) & (~b | a))
471
  // (~a | b | ~lit) & (~b | a | ~lit)
472
371244
  assertClause(iffNode.negate(), ~a, b, ~iffLit);
473
371244
  assertClause(iffNode.negate(), a, ~b, ~iffLit);
474
475
  // (a<->b) -> lit
476
  // ~((a & b) | (~a & ~b)) | lit
477
  // (~(a & b)) & (~(~a & ~b)) | lit
478
  // ((~a | ~b) & (a | b)) | lit
479
  // (~a | ~b | lit) & (a | b | lit)
480
371244
  assertClause(iffNode, ~a, ~b, iffLit);
481
371244
  assertClause(iffNode, a, b, iffLit);
482
483
371244
  return iffLit;
484
}
485
486
66363
SatLiteral CnfStream::handleIte(TNode iteNode)
487
{
488
66363
  Assert(!hasLiteral(iteNode)) << "Atom already mapped!";
489
66363
  Assert(iteNode.getKind() == kind::ITE);
490
66363
  Assert(iteNode.getNumChildren() == 3);
491
66363
  Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
492
132726
  Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " "
493
66363
               << iteNode[2] << ")\n";
494
495
66363
  SatLiteral condLit = toCNF(iteNode[0]);
496
66363
  SatLiteral thenLit = toCNF(iteNode[1]);
497
66363
  SatLiteral elseLit = toCNF(iteNode[2]);
498
499
66363
  SatLiteral iteLit = newLiteral(iteNode);
500
501
  // If ITE is true then one of the branches is true and the condition
502
  // implies which one
503
  // lit -> (ite b t e)
504
  // lit -> (t | e) & (b -> t) & (!b -> e)
505
  // lit -> (t | e) & (!b | t) & (b | e)
506
  // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
507
66363
  assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit);
508
66363
  assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit);
509
66363
  assertClause(iteNode.negate(), ~iteLit, condLit, elseLit);
510
511
  // If ITE is false then one of the branches is false and the condition
512
  // implies which one
513
  // !lit -> !(ite b t e)
514
  // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
515
  // !lit -> (!t | !e) & (!b | !t) & (b | !e)
516
  // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
517
66363
  assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
518
66363
  assertClause(iteNode, iteLit, ~condLit, ~thenLit);
519
66363
  assertClause(iteNode, iteLit, condLit, ~elseLit);
520
521
66363
  return iteLit;
522
}
523
524
8866984
SatLiteral CnfStream::toCNF(TNode node, bool negated)
525
{
526
17733968
  Trace("cnf") << "toCNF(" << node
527
8866984
               << ", negated = " << (negated ? "true" : "false") << ")\n";
528
8866984
  SatLiteral nodeLit;
529
17733968
  Node negatedNode = node.notNode();
530
531
  // If the non-negated node has already been translated, get the translation
532
8866984
  if(hasLiteral(node)) {
533
6234311
    Trace("cnf") << "toCNF(): already translated\n";
534
6234311
    nodeLit = getLiteral(node);
535
    // Return the (maybe negated) literal
536
6234311
    return !negated ? nodeLit : ~nodeLit;
537
  }
538
  // Handle each Boolean operator case
539
2632673
  switch (node.getKind())
540
  {
541
177087
    case kind::NOT: nodeLit = ~toCNF(node[0]); break;
542
266535
    case kind::XOR: nodeLit = handleXor(node); break;
543
66363
    case kind::ITE: nodeLit = handleIte(node); break;
544
6519
    case kind::IMPLIES: nodeLit = handleImplies(node); break;
545
339963
    case kind::OR: nodeLit = handleOr(node); break;
546
695331
    case kind::AND: nodeLit = handleAnd(node); break;
547
606003
    case kind::EQUAL:
548
1212006
      nodeLit =
549
1818009
          node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node);
550
606003
      break;
551
474872
    default:
552
    {
553
474876
      nodeLit = convertAtom(node);
554
    }
555
474868
    break;
556
  }
557
  // Return the (maybe negated) literal
558
5265338
  Trace("cnf") << "toCNF(): resulting literal: "
559
2632669
               << (!negated ? nodeLit : ~nodeLit) << "\n";
560
2632669
  return !negated ? nodeLit : ~nodeLit;
561
}
562
563
130106
void CnfStream::convertAndAssertAnd(TNode node, bool negated)
564
{
565
130106
  Assert(node.getKind() == kind::AND);
566
260212
  Trace("cnf") << "CnfStream::convertAndAssertAnd(" << node
567
130106
               << ", negated = " << (negated ? "true" : "false") << ")\n";
568
130106
  if (!negated) {
569
    // If the node is a conjunction, we handle each conjunct separately
570
442504
    for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
571
442504
        conjunct != node_end; ++conjunct ) {
572
428237
      convertAndAssert(*conjunct, false);
573
    }
574
  } else {
575
    // If the node is a disjunction, we construct a clause and assert it
576
115837
    int nChildren = node.getNumChildren();
577
231674
    SatClause clause(nChildren);
578
115837
    TNode::const_iterator disjunct = node.begin();
579
1584785
    for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
580
1468948
      Assert(disjunct != node.end());
581
1468948
      clause[i] = toCNF(*disjunct, true);
582
    }
583
115837
    Assert(disjunct == node.end());
584
115837
    assertClause(node.negate(), clause);
585
  }
586
130105
}
587
588
523058
void CnfStream::convertAndAssertOr(TNode node, bool negated)
589
{
590
523058
  Assert(node.getKind() == kind::OR);
591
1046116
  Trace("cnf") << "CnfStream::convertAndAssertOr(" << node
592
523058
               << ", negated = " << (negated ? "true" : "false") << ")\n";
593
523058
  if (!negated) {
594
    // If the node is a disjunction, we construct a clause and assert it
595
522574
    int nChildren = node.getNumChildren();
596
1045148
    SatClause clause(nChildren);
597
522574
    TNode::const_iterator disjunct = node.begin();
598
2049495
    for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
599
1526921
      Assert(disjunct != node.end());
600
1526921
      clause[i] = toCNF(*disjunct, false);
601
    }
602
522574
    Assert(disjunct == node.end());
603
522574
    assertClause(node, clause);
604
  } else {
605
    // If the node is a conjunction, we handle each conjunct separately
606
4132
    for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
607
4132
        conjunct != node_end; ++conjunct ) {
608
3648
      convertAndAssert(*conjunct, true);
609
    }
610
  }
611
523058
}
612
613
67
void CnfStream::convertAndAssertXor(TNode node, bool negated)
614
{
615
67
  Assert(node.getKind() == kind::XOR);
616
134
  Trace("cnf") << "CnfStream::convertAndAssertXor(" << node
617
67
               << ", negated = " << (negated ? "true" : "false") << ")\n";
618
67
  if (!negated) {
619
    // p XOR q
620
67
    SatLiteral p = toCNF(node[0], false);
621
67
    SatLiteral q = toCNF(node[1], false);
622
    // Construct the clauses (p => !q) and (!q => p)
623
134
    SatClause clause1(2);
624
67
    clause1[0] = ~p;
625
67
    clause1[1] = ~q;
626
67
    assertClause(node, clause1);
627
134
    SatClause clause2(2);
628
67
    clause2[0] = p;
629
67
    clause2[1] = q;
630
67
    assertClause(node, clause2);
631
  } else {
632
    // !(p XOR q) is the same as p <=> q
633
    SatLiteral p = toCNF(node[0], false);
634
    SatLiteral q = toCNF(node[1], false);
635
    // Construct the clauses (p => q) and (q => p)
636
    SatClause clause1(2);
637
    clause1[0] = ~p;
638
    clause1[1] = q;
639
    assertClause(node.negate(), clause1);
640
    SatClause clause2(2);
641
    clause2[0] = p;
642
    clause2[1] = ~q;
643
    assertClause(node.negate(), clause2);
644
  }
645
67
}
646
647
81473
void CnfStream::convertAndAssertIff(TNode node, bool negated)
648
{
649
81473
  Assert(node.getKind() == kind::EQUAL);
650
162946
  Trace("cnf") << "CnfStream::convertAndAssertIff(" << node
651
81473
               << ", negated = " << (negated ? "true" : "false") << ")\n";
652
81473
  if (!negated) {
653
    // p <=> q
654
80893
    SatLiteral p = toCNF(node[0], false);
655
80893
    SatLiteral q = toCNF(node[1], false);
656
    // Construct the clauses (p => q) and (q => p)
657
161786
    SatClause clause1(2);
658
80893
    clause1[0] = ~p;
659
80893
    clause1[1] = q;
660
80893
    assertClause(node, clause1);
661
161786
    SatClause clause2(2);
662
80893
    clause2[0] = p;
663
80893
    clause2[1] = ~q;
664
80893
    assertClause(node, clause2);
665
  } else {
666
    // !(p <=> q) is the same as p XOR q
667
580
    SatLiteral p = toCNF(node[0], false);
668
580
    SatLiteral q = toCNF(node[1], false);
669
    // Construct the clauses (p => !q) and (!q => p)
670
1160
    SatClause clause1(2);
671
580
    clause1[0] = ~p;
672
580
    clause1[1] = ~q;
673
580
    assertClause(node.negate(), clause1);
674
1160
    SatClause clause2(2);
675
580
    clause2[0] = p;
676
580
    clause2[1] = q;
677
580
    assertClause(node.negate(), clause2);
678
  }
679
81473
}
680
681
60614
void CnfStream::convertAndAssertImplies(TNode node, bool negated)
682
{
683
60614
  Assert(node.getKind() == kind::IMPLIES);
684
121228
  Trace("cnf") << "CnfStream::convertAndAssertImplies(" << node
685
60614
               << ", negated = " << (negated ? "true" : "false") << ")\n";
686
60614
  if (!negated) {
687
    // p => q
688
60183
    SatLiteral p = toCNF(node[0], false);
689
60183
    SatLiteral q = toCNF(node[1], false);
690
    // Construct the clause ~p || q
691
120366
    SatClause clause(2);
692
60183
    clause[0] = ~p;
693
60183
    clause[1] = q;
694
60183
    assertClause(node, clause);
695
  } else {// Construct the
696
    // !(p => q) is the same as (p && ~q)
697
431
    convertAndAssert(node[0], false);
698
431
    convertAndAssert(node[1], true);
699
  }
700
60614
}
701
702
25512
void CnfStream::convertAndAssertIte(TNode node, bool negated)
703
{
704
25512
  Assert(node.getKind() == kind::ITE);
705
51024
  Trace("cnf") << "CnfStream::convertAndAssertIte(" << node
706
25512
               << ", negated = " << (negated ? "true" : "false") << ")\n";
707
  // ITE(p, q, r)
708
25512
  SatLiteral p = toCNF(node[0], false);
709
25512
  SatLiteral q = toCNF(node[1], negated);
710
25512
  SatLiteral r = toCNF(node[2], negated);
711
  // Construct the clauses:
712
  // (p => q) and (!p => r)
713
  //
714
  // Note that below q and r can be used directly because whether they are
715
  // negated has been push to the literal definitions above
716
51024
  Node nnode = node;
717
25512
  if( negated ){
718
79
    nnode = node.negate();
719
  }
720
51024
  SatClause clause1(2);
721
25512
  clause1[0] = ~p;
722
25512
  clause1[1] = q;
723
25512
  assertClause(nnode, clause1);
724
51024
  SatClause clause2(2);
725
25512
  clause2[0] = p;
726
25512
  clause2[1] = r;
727
25512
  assertClause(nnode, clause2);
728
25512
}
729
730
// At the top level we must ensure that all clauses that are asserted are
731
// not unit, except for the direct assertions. This allows us to remove the
732
// clauses later when they are not needed anymore (lemmas for example).
733
590937
void CnfStream::convertAndAssert(TNode node,
734
                                 bool removable,
735
                                 bool negated,
736
                                 bool input)
737
{
738
1181874
  Trace("cnf") << "convertAndAssert(" << node
739
1181874
               << ", negated = " << (negated ? "true" : "false")
740
590937
               << ", removable = " << (removable ? "true" : "false") << ")\n";
741
590937
  d_removable = removable;
742
743
590937
  if (d_cnfProof)
744
  {
745
174016
    d_cnfProof->pushCurrentAssertion(negated ? node.notNode() : (Node)node,
746
                                     input);
747
  }
748
590941
  convertAndAssert(node, negated);
749
590933
  if (d_cnfProof)
750
  {
751
174016
    d_cnfProof->popCurrentAssertion();
752
  }
753
590933
}
754
755
1096805
void CnfStream::convertAndAssert(TNode node, bool negated)
756
{
757
2193610
  Trace("cnf") << "convertAndAssert(" << node
758
1096805
               << ", negated = " << (negated ? "true" : "false") << ")\n";
759
760
1096805
  d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
761
762
1096805
  switch(node.getKind()) {
763
130107
    case kind::AND: convertAndAssertAnd(node, negated); break;
764
523058
    case kind::OR: convertAndAssertOr(node, negated); break;
765
67
    case kind::XOR: convertAndAssertXor(node, negated); break;
766
60614
    case kind::IMPLIES: convertAndAssertImplies(node, negated); break;
767
25512
    case kind::ITE: convertAndAssertIte(node, negated); break;
768
73124
    case kind::NOT: convertAndAssert(node[0], !negated); break;
769
175973
    case kind::EQUAL:
770
175973
      if (node[0].getType().isBoolean())
771
      {
772
81473
        convertAndAssertIff(node, negated);
773
81473
        break;
774
      }
775
      CVC4_FALLTHROUGH;
776
    default:
777
    {
778
405706
      Node nnode = node;
779
202853
      if (negated)
780
      {
781
65772
        nnode = node.negate();
782
      }
783
      // Atoms
784
405706
      assertClause(nnode, toCNF(node, negated));
785
  }
786
202849
    break;
787
  }
788
1096798
}
789
790
}/* CVC4::prop namespace */
791
26685
}/* CVC4 namespace */