GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/cnf_stream.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cnf_stream.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Haniel Barbosa, Tim King
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 This class transforms a sequence of formulas into clauses.
13
 **
14
 ** This class takes a sequence of formulas.
15
 ** It outputs a stream of clauses that is propositionally
16
 ** equi-satisfiable with the conjunction of the formulas.
17
 ** This stream is maintained in an online fashion.
18
 **
19
 ** Unlike other parts of the system it is aware of the PropEngine's
20
 ** internals such as the representation and translation of [??? -Chris]
21
 **/
22
23
#include "cvc4_private.h"
24
25
#ifndef CVC4__PROP__CNF_STREAM_H
26
#define CVC4__PROP__CNF_STREAM_H
27
28
#include "context/cdhashset.h"
29
#include "context/cdinsert_hashmap.h"
30
#include "context/cdlist.h"
31
#include "expr/node.h"
32
#include "proof/proof_manager.h"
33
#include "prop/proof_cnf_stream.h"
34
#include "prop/registrar.h"
35
#include "prop/sat_solver_types.h"
36
37
namespace CVC4 {
38
39
class OutputManager;
40
41
namespace prop {
42
43
class ProofCnfStream;
44
class PropEngine;
45
class SatSolver;
46
47
/** A policy for how literals for formulas are handled in cnf_stream */
48
enum class FormulaLitPolicy : uint32_t
49
{
50
  // literals for formulas are notified
51
  TRACK_AND_NOTIFY,
52
  // literals for formulas are added to node map
53
  TRACK,
54
  // literals for formulas are kept internal (default)
55
  INTERNAL,
56
};
57
58
/**
59
 * Implements the following recursive algorithm
60
 * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
61
 * in a single pass.
62
 *
63
 * The general idea is to introduce a new literal that will be equivalent to
64
 * each subexpression in the constructed equi-satisfiable formula, then
65
 * substitute the new literal for the formula, and so on, recursively.
66
 */
67
18028
class CnfStream {
68
  friend PropEngine;
69
  friend ProofCnfStream;
70
71
 public:
72
  /** Cache of what nodes have been registered to a literal. */
73
  typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction>
74
      LiteralToNodeMap;
75
76
  /** Cache of what literals have been registered to a node. */
77
  typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction>
78
      NodeToLiteralMap;
79
80
  /**
81
   * Constructs a CnfStream that performs equisatisfiable CNF transformations
82
   * and sends the generated clauses and to the given SAT solver. This does not
83
   * take ownership of satSolver, registrar, or context.
84
   *
85
   * @param satSolver the sat solver to use.
86
   * @param registrar the entity that takes care of preregistration of Nodes.
87
   * @param context the context that the CNF should respect.
88
   * @param outMgr Reference to the output manager of the smt engine. Assertions
89
   * will not be dumped if outMgr == nullptr.
90
   * @param rm the resource manager of the CNF stream
91
   * @param flpol policy for literals corresponding to formulas (those that are
92
   * not-theory literals).
93
   * @param name string identifier to distinguish between different instances
94
   * even for non-theory literals.
95
   */
96
  CnfStream(SatSolver* satSolver,
97
            Registrar* registrar,
98
            context::Context* context,
99
            OutputManager* outMgr,
100
            ResourceManager* rm,
101
            FormulaLitPolicy flpol = FormulaLitPolicy::INTERNAL,
102
            std::string name = "");
103
  /**
104
   * Convert a given formula to CNF and assert it to the SAT solver.
105
   *
106
   * @param node node to convert and assert
107
   * @param removable whether the sat solver can choose to remove the clauses
108
   * @param negated whether we are asserting the node negated
109
   * @param input whether it is an input assertion (rather than a lemma). This
110
   * information is only relevant for unsat core tracking.
111
   */
112
  void convertAndAssert(TNode node,
113
                        bool removable,
114
                        bool negated,
115
                        bool input = false);
116
  /**
117
   * Get the node that is represented by the given SatLiteral.
118
   * @param literal the literal from the sat solver
119
   * @return the actual node
120
   */
121
  TNode getNode(const SatLiteral& literal);
122
123
  /**
124
   * Returns true iff the node has an assigned literal (it might not be
125
   * translated).
126
   * @param node the node
127
   */
128
  bool hasLiteral(TNode node) const;
129
130
  /**
131
   * Ensure that the given node will have a designated SAT literal that is
132
   * definitionally equal to it.  The result of this function is that the Node
133
   * can be queried via getSatValue(). Essentially, this is like a "convert-but-
134
   * don't-assert" version of convertAndAssert().
135
   */
136
  void ensureLiteral(TNode n);
137
138
  /**
139
   * Returns the literal that represents the given node in the SAT CNF
140
   * representation.
141
   * @param node [Presumably there are some constraints on the kind of
142
   * node? E.g., it needs to be a boolean? -Chris]
143
   */
144
  SatLiteral getLiteral(TNode node);
145
146
  /**
147
   * Returns the Boolean variables from the input problem.
148
   */
149
  void getBooleanVariables(std::vector<TNode>& outputVariables) const;
150
151
  /**
152
   * For SAT/theory relevancy. Returns true if node is a "notify formula".
153
   * Returns true if node is formula that we are being notified about that
154
   * is not a theory atom.
155
   *
156
   * Note this is only ever true when the policy passed to this class is
157
   * FormulaLitPolicy::TRACK_AND_NOTIFY.
158
   */
159
  bool isNotifyFormula(TNode node) const;
160
161
  /** Retrieves map from nodes to literals. */
162
  const CnfStream::NodeToLiteralMap& getTranslationCache() const;
163
164
  /** Retrieves map from literals to nodes. */
165
  const CnfStream::LiteralToNodeMap& getNodeCache() const;
166
167
  void setProof(CnfProof* proof);
168
169
 protected:
170
  /**
171
   * Same as above, except that uses the saved d_removable flag. It calls the
172
   * dedicated converter for the possible formula kinds.
173
   */
174
  void convertAndAssert(TNode node, bool negated);
175
  /** Specific converters for each formula kind. */
176
  void convertAndAssertAnd(TNode node, bool negated);
177
  void convertAndAssertOr(TNode node, bool negated);
178
  void convertAndAssertXor(TNode node, bool negated);
179
  void convertAndAssertIff(TNode node, bool negated);
180
  void convertAndAssertImplies(TNode node, bool negated);
181
  void convertAndAssertIte(TNode node, bool negated);
182
183
  /**
184
   * Transforms the node into CNF recursively and yields a literal
185
   * definitionally equal to it.
186
   *
187
   * This method also populates caches, kept in d_cnfStream, between formulas
188
   * and literals to avoid redundant work and to retrieve formulas from literals
189
   * and vice-versa.
190
   *
191
   * @param node the formula to transform
192
   * @param negated whether the literal is negated
193
   * @return the literal representing the root of the formula
194
   */
195
  SatLiteral toCNF(TNode node, bool negated = false);
196
197
  /** Specific clausifiers, based on the formula kinds, that clausify a formula,
198
   * by calling toCNF into each of the formula's children under the respective
199
   * kind, and introduce a literal definitionally equal to it. */
200
  SatLiteral handleNot(TNode node);
201
  SatLiteral handleXor(TNode node);
202
  SatLiteral handleImplies(TNode node);
203
  SatLiteral handleIff(TNode node);
204
  SatLiteral handleIte(TNode node);
205
  SatLiteral handleAnd(TNode node);
206
  SatLiteral handleOr(TNode node);
207
208
  /** Stores the literal of the given node in d_literalToNodeMap.
209
   *
210
   * Note that n must already have a literal associated to it in
211
   * d_nodeToLiteralMap.
212
   */
213
  void ensureMappingForLiteral(TNode n);
214
215
  /** The SAT solver we will be using */
216
  SatSolver* d_satSolver;
217
218
  /** Reference to the output manager of the smt engine */
219
  OutputManager* d_outMgr;
220
221
  /** Boolean variables that we translated */
222
  context::CDList<TNode> d_booleanVariables;
223
224
  /** Formulas that we translated that we are notifying */
225
  context::CDHashSet<Node, NodeHashFunction> d_notifyFormulas;
226
227
  /** Map from nodes to literals */
228
  NodeToLiteralMap d_nodeToLiteralMap;
229
230
  /** Map from literals to nodes */
231
  LiteralToNodeMap d_literalToNodeMap;
232
233
  /**
234
   * True if the lit-to-Node map should be kept for all lits, not just
235
   * theory lits.  This is true if e.g. replay logging is on, which
236
   * dumps the Nodes corresponding to decision literals.
237
   */
238
  const FormulaLitPolicy d_flitPolicy;
239
240
  /** The "registrar" for pre-registration of terms */
241
  Registrar* d_registrar;
242
243
  /** The name of this CNF stream*/
244
  std::string d_name;
245
246
  /** Pointer to the proof corresponding to this CnfStream */
247
  CnfProof* d_cnfProof;
248
249
  /**
250
   * Are we asserting a removable clause (true) or a permanent clause (false).
251
   * This is set at the beginning of convertAndAssert so that it doesn't
252
   * need to be passed on over the stack.  Only pure clauses can be asserted
253
   * as removable.
254
   */
255
  bool d_removable;
256
257
  /**
258
   * Asserts the given clause to the sat solver.
259
   * @param node the node giving rise to this clause
260
   * @param clause the clause to assert
261
   * @return whether the clause was asserted in the SAT solver.
262
   */
263
  bool assertClause(TNode node, SatClause& clause);
264
265
  /**
266
   * Asserts the unit clause to the sat solver.
267
   * @param node the node giving rise to this clause
268
   * @param a the unit literal of the clause
269
   * @return whether the clause was asserted in the SAT solver.
270
   */
271
  bool assertClause(TNode node, SatLiteral a);
272
273
  /**
274
   * Asserts the binary clause to the sat solver.
275
   * @param node the node giving rise to this clause
276
   * @param a the first literal in the clause
277
   * @param b the second literal in the clause
278
   * @return whether the clause was asserted in the SAT solver.
279
   */
280
  bool assertClause(TNode node, SatLiteral a, SatLiteral b);
281
282
  /**
283
   * Asserts the ternary clause to the sat solver.
284
   * @param node the node giving rise to this clause
285
   * @param a the first literal in the clause
286
   * @param b the second literal in the clause
287
   * @param c the thirs literal in the clause
288
   * @return whether the clause was asserted in the SAT solver.
289
   */
290
  bool assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
291
292
  /**
293
   * Acquires a new variable from the SAT solver to represent the node
294
   * and inserts the necessary data it into the mapping tables.
295
   * @param node a formula
296
   * @param isTheoryAtom is this a theory atom that needs to be asserted to
297
   * theory.
298
   * @param preRegister whether to preregister the atom with the theory
299
   * @param canEliminate whether the sat solver can safely eliminate this
300
   * variable.
301
   * @return the literal corresponding to the formula
302
   */
303
  SatLiteral newLiteral(TNode node, bool isTheoryAtom = false,
304
                        bool preRegister = false, bool canEliminate = true);
305
306
  /**
307
   * Constructs a new literal for an atom and returns it.  Calls
308
   * newLiteral().
309
   *
310
   * @param node the node to convert; there should be no boolean
311
   * structure in this expression.  Assumed to not be in the
312
   * translation cache.
313
   */
314
  SatLiteral convertAtom(TNode node);
315
316
  /** Pointer to resource manager for associated SmtEngine */
317
  ResourceManager* d_resourceManager;
318
}; /* class CnfStream */
319
320
}  // namespace prop
321
}  // namespace CVC4
322
323
#endif /* CVC4__PROP__CNF_STREAM_H */