1 /********************* */
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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
12 ** \brief This class transforms a sequence of formulas into clauses.
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.
19 ** Unlike other parts of the system it is aware of the PropEngine's
20 ** internals such as the representation and translation of [??? -Chris]
23 #include "cvc4_private.h"
25 #ifndef CVC4__PROP__CNF_STREAM_H
26 #define CVC4__PROP__CNF_STREAM_H
28 #include "context/cdinsert_hashmap.h"
29 #include "context/cdlist.h"
30 #include "expr/node.h"
31 #include "proof/proof_manager.h"
32 #include "prop/registrar.h"
33 #include "prop/theory_proxy.h"
42 * Comments for the behavior of the whole class... [??? -Chris]
43 * @author Tim King <taking@cs.nyu.edu>
47 /** Cache of what nodes have been registered to a literal. */
48 typedef context::CDInsertHashMap
<SatLiteral
, TNode
, SatLiteralHashFunction
>
51 /** Cache of what literals have been registered to a node. */
52 typedef context::CDInsertHashMap
<Node
, SatLiteral
, NodeHashFunction
>
56 /** The SAT solver we will be using */
57 SatSolver
* d_satSolver
;
59 /** Boolean variables that we translated */
60 context::CDList
<TNode
> d_booleanVariables
;
62 /** Map from nodes to literals */
63 NodeToLiteralMap d_nodeToLiteralMap
;
65 /** Map from literals to nodes */
66 LiteralToNodeMap d_literalToNodeMap
;
69 * True if the lit-to-Node map should be kept for all lits, not just
70 * theory lits. This is true if e.g. replay logging is on, which
71 * dumps the Nodes corresponding to decision literals.
73 const bool d_fullLitToNodeMap
;
76 * Counter for resource limiting that is used to spend a resource
77 * every ResourceManager::resourceCounter calls to convertAndAssert.
79 unsigned long d_convertAndAssertCounter
;
81 /** The "registrar" for pre-registration of terms */
82 Registrar
* d_registrar
;
84 /** The name of this CNF stream*/
87 /** Pointer to the proof corresponding to this CnfStream */
90 /** Remove nots from the node */
91 TNode
stripNot(TNode node
) {
92 while (node
.getKind() == kind::NOT
) {
99 * Are we asserting a removable clause (true) or a permanent clause (false).
100 * This is set at the beginning of convertAndAssert so that it doesn't
101 * need to be passed on over the stack. Only pure clauses can be asserted
107 * Asserts the given clause to the sat solver.
108 * @param node the node giving rise to this clause
109 * @param clause the clause to assert
111 void assertClause(TNode node
, SatClause
& clause
);
114 * Asserts the unit clause to the sat solver.
115 * @param node the node giving rise to this clause
116 * @param a the unit literal of the clause
118 void assertClause(TNode node
, SatLiteral a
);
121 * Asserts the binary clause to the sat solver.
122 * @param node the node giving rise to this clause
123 * @param a the first literal in the clause
124 * @param b the second literal in the clause
126 void assertClause(TNode node
, SatLiteral a
, SatLiteral b
);
129 * Asserts the ternary clause to the sat solver.
130 * @param node the node giving rise to this clause
131 * @param a the first literal in the clause
132 * @param b the second literal in the clause
133 * @param c the thirs literal in the clause
135 void assertClause(TNode node
, SatLiteral a
, SatLiteral b
, SatLiteral c
);
138 * Acquires a new variable from the SAT solver to represent the node
139 * and inserts the necessary data it into the mapping tables.
140 * @param node a formula
141 * @param isTheoryAtom is this a theory atom that needs to be asserted to
143 * @param preRegister whether to preregister the atom with the theory
144 * @param canEliminate whether the sat solver can safely eliminate this
146 * @return the literal corresponding to the formula
148 SatLiteral
newLiteral(TNode node
, bool isTheoryAtom
= false,
149 bool preRegister
= false, bool canEliminate
= true);
152 * Constructs a new literal for an atom and returns it. Calls
155 * @param node the node to convert; there should be no boolean
156 * structure in this expression. Assumed to not be in the
159 SatLiteral
convertAtom(TNode node
, bool noPreprocessing
= false);
163 * Constructs a CnfStream that sends constructs an equi-satisfiable
164 * set of clauses and sends them to the given sat solver. This does not take
165 * ownership of satSolver, registrar, or context.
166 * @param satSolver the sat solver to use.
167 * @param registrar the entity that takes care of preregistration of Nodes.
168 * @param context the context that the CNF should respect.
169 * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
170 * @param name string identifier to distinguish between different instances
171 * even for non-theory literals.
173 CnfStream(SatSolver
* satSolver
, Registrar
* registrar
,
174 context::Context
* context
, bool fullLitToNodeMap
= false,
175 std::string name
= "");
178 * Destructs a CnfStream. This implementation does nothing, but we
179 * need a virtual destructor for safety in case subclasses have a
182 virtual ~CnfStream() {}
185 * Converts and asserts a formula.
186 * @param node node to convert and assert
187 * @param removable whether the sat solver can choose to remove the clauses
188 * @param negated whether we are asserting the node negated
190 virtual void convertAndAssert(TNode node
, bool removable
, bool negated
,
192 TNode from
= TNode::null()) = 0;
195 * Get the node that is represented by the given SatLiteral.
196 * @param literal the literal from the sat solver
197 * @return the actual node
199 TNode
getNode(const SatLiteral
& literal
);
202 * Returns true iff the node has an assigned literal (it might not be
204 * @param node the node
206 bool hasLiteral(TNode node
) const;
209 * Ensure that the given node will have a designated SAT literal that is
210 * definitionally equal to it. The result of this function is that the Node
211 * can be queried via getSatValue(). Essentially, this is like a "convert-but-
212 * don't-assert" version of convertAndAssert().
214 virtual void ensureLiteral(TNode n
, bool noPreregistration
= false) = 0;
217 * Returns the literal that represents the given node in the SAT CNF
219 * @param node [Presumably there are some constraints on the kind of
220 * node? E.g., it needs to be a boolean? -Chris]
222 SatLiteral
getLiteral(TNode node
);
225 * Returns the Boolean variables from the input problem.
227 void getBooleanVariables(std::vector
<TNode
>& outputVariables
) const;
229 const NodeToLiteralMap
& getTranslationCache() const {
230 return d_nodeToLiteralMap
;
233 const LiteralToNodeMap
& getNodeCache() const { return d_literalToNodeMap
; }
235 void setProof(CnfProof
* proof
);
236 }; /* class CnfStream */
239 * TseitinCnfStream is based on the following recursive algorithm
240 * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
241 * The general idea is to introduce a new literal that
242 * will be equivalent to each subexpression in the constructed equi-satisfiable
243 * formula, then substitute the new literal for the formula, and so on,
246 * This implementation does this in a single recursive pass. [??? -Chris]
248 class TseitinCnfStream
: public CnfStream
{
251 * Constructs the stream to use the given sat solver. This does not take
252 * ownership of satSolver, registrar, or context.
253 * @param satSolver the sat solver to use
254 * @param registrar the entity that takes care of pre-registration of Nodes
255 * @param context the context that the CNF should respect.
256 * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
257 * even for non-theory literals
259 TseitinCnfStream(SatSolver
* satSolver
, Registrar
* registrar
,
260 context::Context
* context
, bool fullLitToNodeMap
= false,
261 std::string name
= "");
264 * Convert a given formula to CNF and assert it to the SAT solver.
265 * @param node the formula to assert
266 * @param removable is this something that can be erased
267 * @param negated true if negated
269 void convertAndAssert(TNode node
,
273 TNode from
= TNode::null()) override
;
277 * Same as above, except that removable is remembered.
279 void convertAndAssert(TNode node
, bool negated
);
281 // Each of these formulas handles takes care of a Node of each Kind.
283 // Each handleX(Node &n) is responsible for:
284 // - constructing a new literal, l (if necessary)
285 // - calling registerNode(n,l)
286 // - adding clauses assure that l is equivalent to the Node
287 // - calling toCNF on its children (if necessary)
290 // handleX( n ) can assume that n is not in d_translationCache
291 SatLiteral
handleNot(TNode node
);
292 SatLiteral
handleXor(TNode node
);
293 SatLiteral
handleImplies(TNode node
);
294 SatLiteral
handleIff(TNode node
);
295 SatLiteral
handleIte(TNode node
);
296 SatLiteral
handleAnd(TNode node
);
297 SatLiteral
handleOr(TNode node
);
299 void convertAndAssertAnd(TNode node
, bool negated
);
300 void convertAndAssertOr(TNode node
, bool negated
);
301 void convertAndAssertXor(TNode node
, bool negated
);
302 void convertAndAssertIff(TNode node
, bool negated
);
303 void convertAndAssertImplies(TNode node
, bool negated
);
304 void convertAndAssertIte(TNode node
, bool negated
);
307 * Transforms the node into CNF recursively.
308 * @param node the formula to transform
309 * @param negated whether the literal is negated
310 * @return the literal representing the root of the formula
312 SatLiteral
toCNF(TNode node
, bool negated
= false);
314 void ensureLiteral(TNode n
, bool noPreregistration
= false) override
;
316 }; /* class TseitinCnfStream */
318 } /* CVC4::prop namespace */
319 } /* CVC4 namespace */
321 #endif /* CVC4__PROP__CNF_STREAM_H */