1 files changed, 165 insertions, 0 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
new file mode 100644
index 000000000..c0a70730a
--- /dev/null
+++ b/src/prop/cnf_stream.h
@@ -0,0 +1,165 @@
+/*********************                                           -*- C++ -*-  */
+/** cnf_stream.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** This class takes a sequence of formulas.
+ ** It outputs a stream of clauses that is propositional
+ ** equisatisfiable with the conjunction of the formulas.
+ ** This stream is maintained in an online fashion.
+ **
+ ** Unlike other parts of the system it is aware of the PropEngine's
+ ** internals such as the representation and translation of 
+ **/
+
+
+#ifndef __CVC4__CNF_STREAM_H
+#define __CVC4__CNF_STREAM_H
+
+//TODO: Why am i including this? Who knows...
+#include "cvc4_config.h"
+
+#include "expr/node.h"
+#include "prop/minisat/simp/SimpSolver.h"
+#include "prop/minisat/core/SolverTypes.h"
+#include "prop/prop_engine.h"
+
+#include <map>
+
+namespace CVC4 {
+  class PropEngine;
+}
+
+
+namespace CVC4 {
+namespace prop {
+
+class CnfStream {
+
+private:
+  /**
+   * d_propEngine is the PropEngine that the CnfStream interacts with directly through
+   * the follwoing functions:
+   *    - insertClauseIntoStream
+   *    - acquireFreshLit
+   *    - registerMapping
+   */
+  PropEngine *d_propEngine;
+
+  /**Cache of what literal have been registered to a node.
+   *Not strictly needed for correctness.
+   *This can be flushed when memory is under pressure.
+   */
+  std::map<Node,minisat::Lit> d_translationCache;
+  
+protected:
+
+  /**
+   * Uniform interface for sending a clause back to d_propEngine.
+   * May want to have internal datastructures later on
+   */
+  void insertClauseIntoStream(minisat::vec<minisat::Lit> & c);
+  void insertClauseIntoStream(minisat::Lit a);
+  void insertClauseIntoStream(minisat::Lit a,minisat::Lit b);
+  void insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c);
+  
+
+  //utilities for the translation cache;
+  bool isCached(const Node & n) const;
+  minisat::Lit lookupInCache(const Node & n) const;
+
+  /**
+   * Empties the internal translation cache.
+   */
+  void flushCache();
+
+  //negotiates the mapping of atoms to literals with PropEngine
+  void registerMapping(const Node & node, minisat::Lit lit, bool atom = false);
+  minisat::Lit acquireFreshLit(const Node & n);
+  minisat::Lit aquireAndRegister(const Node & n, bool atom = false);
+
+public:
+  /**
+   * Constructs a CnfStream that sends constructs an equisatisfiable set of clauses
+   * and sends them to pe.
+   */
+  CnfStream(CVC4::PropEngine *pe);
+
+
+  /**
+   * Converts and asserts a formula.
+   * @param n node to convert and assert
+   */
+  virtual void convertAndAssert(const Node & n) = 0;
+
+}; /* class CnfStream */
+
+
+/**
+ * TseitinCnfStream is based on the following recursive algorithm
+ * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
+ * The general gist of the algorithm is to introduce a new literal that 
+ * will be equivalent to each subexpression in the constructed equisatisfiable formula
+ * then subsistute the new literal for the formula, and to do this recursively.
+ * 
+ * This implementation does this in a single recursive pass.
+ */
+class TseitinCnfStream : public CnfStream {
+
+public:
+  void convertAndAssert(const Node & n);
+  TseitinCnfStream(CVC4::PropEngine *pe);
+
+private:
+
+  /* Each of these formulas handles takes care of a Node of each Kind.
+   *
+   * Each handleX(Node &n) is responsibile for:
+   *   - constructing a new literal, l (if nessecary)
+   *   - calling registerNode(n,l)
+   *   - adding clauses asure that l is equivalent to the Node
+   *   - calling recTransform on its children (if nessecary)
+   *   - returning l
+   *
+   * handleX( n ) can assume that n is not in d_translationCache
+   */
+  minisat::Lit handleAtom(const Node & n);
+  minisat::Lit handleNot(const Node & n);
+  minisat::Lit handleXor(const Node & n);
+  minisat::Lit handleImplies(const Node & n);
+  minisat::Lit handleIff(const Node & n);
+  minisat::Lit handleIte(const Node & n);
+
+  minisat::Lit handleAnd(const Node& n);
+  minisat::Lit handleOr(const Node& n);
+
+    
+  /**
+   *Maps recTransform over the children of a node.
+   *This is very useful for n-ary Kinds (OR, AND).
+   *
+   *Non n-ary kinds (IMPLIES) should avoid using this as it requires a
+   *tiny bit of extra overhead, and it leads to less readable code.
+   *
+   * precondition: target.size() == n.getNumChildren()
+   */
+  void mapRecTransformOverChildren(const Node& n, minisat::vec<minisat::Lit> & target);
+
+  //Recurisively dispatches the various Kinds to the appropriate handler.
+  minisat::Lit recTransform(const Node & n);
+
+}; /* class TseitinCnfStream */
+
+}/* prop namespace */
+}/* CVC4 namespace */
+
+
+
+#endif /* __CVC4__CNF_STREAM_H */