for tim

4 files changed, 171 insertions, 165 deletions

diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h
index 924cae063..1d0ac50bb 100644
--- a/src/prop/cnf_conversion.h
+++ b/src/prop/cnf_conversion.h
@@ -19,11 +19,14 @@
 namespace CVC4 {
 
 enum CnfConversion {
+  /** TODO: explanation of DIRECT_EXPONENTIAL (is this implemented?) */
   CNF_DIRECT_EXPONENTIAL = 0,
+  /** Explanation of CNF_VAR_INTRODUCTION */
   CNF_VAR_INTRODUCTION = 1
 };
 
 inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC;
+
 inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) {
   using namespace CVC4;
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 73c3f6c01..0a7774129 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -24,33 +24,34 @@
 using namespace CVC4::prop::minisat;
 using namespace std;
 
-
 namespace CVC4 {
 namespace prop {
 
 CnfStream::CnfStream(PropEngine *pe) :
-  d_propEngine(pe){}
-  
-TseitinCnfStream::TseitinCnfStream(PropEngine *pe):
-  CnfStream(pe){}
+  d_propEngine(pe) {
+}
 
+TseitinCnfStream::TseitinCnfStream(PropEngine *pe) :
+  CnfStream(pe) {
+}
 
-void CnfStream::insertClauseIntoStream(vec<Lit> & c){
+void CnfStream::insertClauseIntoStream(vec<Lit> & c) {
   d_propEngine->assertClause(c);
 }
 
-void CnfStream::insertClauseIntoStream(minisat::Lit a){
+void CnfStream::insertClauseIntoStream(minisat::Lit a) {
   vec<Lit> clause(1);
   clause[0] = a;
   insertClauseIntoStream(clause);
 }
-void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b){
+void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b) {
   vec<Lit> clause(2);
   clause[0] = a;
   clause[1] = b;
   insertClauseIntoStream(clause);
 }
-void CnfStream::insertClauseIntoStream(minisat::Lit a,minisat::Lit b, minisat::Lit c){
+void CnfStream::insertClauseIntoStream(minisat::Lit a, minisat::Lit b,
+                                       minisat::Lit c) {
   vec<Lit> clause(3);
   clause[0] = a;
   clause[1] = b;
@@ -67,22 +68,22 @@ Lit CnfStream::lookupInCache(const Node & n) const {
   return d_translationCache.find(n)->second;
 }
 
-void CnfStream::flushCache(){
+void CnfStream::flushCache() {
   d_translationCache.clear();
 }
 
-void CnfStream::registerMapping(const Node & node, Lit lit, bool atom){
+void CnfStream::registerMapping(const Node & node, Lit lit, bool atom) {
   //Prop engine does not need to know this mapping
-  d_translationCache.insert(make_pair(node,lit));
+  d_translationCache.insert(make_pair(node, lit));
   if(atom)
     d_propEngine->registerAtom(node, lit);
 }
 
-Lit CnfStream::acquireFreshLit(const Node & n){
+Lit CnfStream::acquireFreshLit(const Node & n) {
   return d_propEngine->requestFreshLit();
 }
 
-Lit CnfStream::aquireAndRegister(const Node & node, bool atom){
+Lit CnfStream::aquireAndRegister(const Node & node, bool atom) {
   Lit l = acquireFreshLit(node);
   registerMapping(node, l, atom);
   return l;
@@ -94,14 +95,14 @@ Lit CnfStream::aquireAndRegister(const Node & node, bool atom){
 /***********************************************/
 /***********************************************/
 
-Lit TseitinCnfStream::handleAtom(const Node & n){
+Lit TseitinCnfStream::handleAtom(const Node & n) {
   Lit l = aquireAndRegister(n, true);
-  switch(n.getKind()){ /* TRUE and FALSE are handled specially. */
+  switch(n.getKind()) { /* TRUE and FALSE are handled specially. */
   case TRUE:
-    insertClauseIntoStream( l );
+    insertClauseIntoStream(l);
     break;
   case FALSE:
-    insertClauseIntoStream( ~l );
+    insertClauseIntoStream(~l);
     break;
   default: //Does nothing else
     break;
@@ -109,45 +110,47 @@ Lit TseitinCnfStream::handleAtom(const Node & n){
   return l;
 }
 
-Lit TseitinCnfStream::handleXor(const Node & n){
+Lit TseitinCnfStream::handleXor(const Node & n) {
   // n: a XOR b
-  
+
   Lit a = recTransform(n[0]);
   Lit b = recTransform(n[1]);
-  
+
   Lit l = aquireAndRegister(n);
-  
-  insertClauseIntoStream( a,  b, ~l);
-  insertClauseIntoStream( a, ~b,  l);
-  insertClauseIntoStream(~a,  b,  l);
+
+  insertClauseIntoStream(a, b, ~l);
+  insertClauseIntoStream(a, ~b, l);
+  insertClauseIntoStream(~a, b, l);
   insertClauseIntoStream(~a, ~b, ~l);
-  
+
   return l;
 }
 
-  /* For a small efficiency boost target needs to already be allocated to have
-     size of the number of children of n.
-  */
-void  TseitinCnfStream::mapRecTransformOverChildren(const Node& n, vec<Lit> & target){
+/* For a small efficiency boost target needs to already be allocated to have
+ size of the number of children of n.
+ */
+void TseitinCnfStream::mapRecTransformOverChildren(const Node& n,
+                                                   vec<Lit> & target) {
   Assert(target.size() == n.getNumChildren());
 
   int i = 0;
   Node::iterator subExprIter = n.begin();
-  
-  while(subExprIter != n.end()){
+
+  while(subExprIter != n.end()) {
     Lit equivalentLit = recTransform(*subExprIter);
     target[i] = equivalentLit;
-    ++subExprIter; ++i;
+    ++subExprIter;
+    ++i;
   }
 }
 
-Lit TseitinCnfStream::handleOr(const Node& n){
+Lit TseitinCnfStream::handleOr(const Node& n) {
   //child_literals
   vec<Lit> lits(n.getNumChildren());
   mapRecTransformOverChildren(n, lits);
-  
+
   Lit e = aquireAndRegister(n);
-  
+
   /* e <-> (a1 | a2 | a3 | ...)
    *: e -> (a1 | a2 | a3 | ...)
    * : ~e | (
@@ -161,31 +164,29 @@ Lit TseitinCnfStream::handleOr(const Node& n){
 
   vec<Lit> c;
   c.push(~e);
-  
-  for( int index = 0; index < lits.size(); ++index){
+
+  for(int index = 0; index < lits.size(); ++index) {
     Lit a = lits[index];
     c.push(a);
-    insertClauseIntoStream( e, ~a);
+    insertClauseIntoStream(e, ~a);
   }
   insertClauseIntoStream(c);
-  
+
   return e;
 }
 
-
 /* TODO: this only supports 2-ary <=> nodes atm.
  * Should this be changed?
  */
-Lit TseitinCnfStream::handleIff(const Node& n){
-  Assert(n.getKind() == IFF);
-  Assert(n.getNumChildren() == 2);
+Lit TseitinCnfStream::handleIff(const Node& n) {
+  Assert(n.getKind() == IFF); Assert(n.getNumChildren() == 2);
   // n: a <=> b;
 
   Lit a = recTransform(n[0]);
   Lit b = recTransform(n[1]);
-    
+
   Lit l = aquireAndRegister(n);
-    
+
   /* l <-> (a<->b)
    * : l -> ((a-> b) & (b->a))
    * : ~l | ((~a | b) & (~b |a))
@@ -197,21 +198,21 @@ Lit TseitinCnfStream::handleIff(const Node& n){
    * : ((~a | ~b) & (a | b)) | l
    * : (~a | ~b | l) & (a | b | l)
    */
-    
-  insertClauseIntoStream( ~a, b,~l);
-  insertClauseIntoStream(  a,~b,~l);
-  insertClauseIntoStream( ~a,~b, l);
-  insertClauseIntoStream(  a, b, l);
-  
+
+  insertClauseIntoStream(~a, b, ~l);
+  insertClauseIntoStream(a, ~b, ~l);
+  insertClauseIntoStream(~a, ~b, l);
+  insertClauseIntoStream(a, b, l);
+
   return l;
 }
 
-Lit TseitinCnfStream::handleAnd(const Node& n){
+Lit TseitinCnfStream::handleAnd(const Node& n) {
   //TODO: we know the exact size of the this.
   //Dynamically allocated array would have less overhead no?
   vec<Lit> lits(n.getNumChildren());
   mapRecTransformOverChildren(n, lits);
-    
+
   Lit e = aquireAndRegister(n);
 
   /* e <-> (a1 & a2 & a3 & ...)
@@ -227,25 +228,25 @@ Lit TseitinCnfStream::handleAnd(const Node& n){
 
   vec<Lit> c;
   c.push(e);
-  for(int index = 0; index < lits.size(); ++index){
+  for(int index = 0; index < lits.size(); ++index) {
     Lit a = lits[index];
     c.push(~a);
-    insertClauseIntoStream( ~e, a );
+    insertClauseIntoStream(~e, a);
   }
   insertClauseIntoStream(c);
-  
+
   return e;
 }
 
-Lit TseitinCnfStream::handleImplies(const Node & n){
+Lit TseitinCnfStream::handleImplies(const Node & n) {
   Assert(n.getKind() == IMPLIES);
   // n: a => b;
 
   Lit a = recTransform(n[0]);
   Lit b = recTransform(n[1]);
-  
+
   Lit l = aquireAndRegister(n);
-  
+
   /* l <-> (a->b)
    * (l -> (a->b)) & (l <- (a->b))
    *  : l -> (a -> b)
@@ -258,17 +259,17 @@ Lit TseitinCnfStream::handleImplies(const Node & n){
    *  : (a | l) & (~b | l)
    * (~l | ~a | b) & (a | l) & (~b | l)
    */
-    
-  insertClauseIntoStream(  a, l);
-  insertClauseIntoStream( ~b, l);
-  insertClauseIntoStream( ~l, ~a, b);
-  
+
+  insertClauseIntoStream(a, l);
+  insertClauseIntoStream(~b, l);
+  insertClauseIntoStream(~l, ~a, b);
+
   return l;
 }
 
-Lit TseitinCnfStream::handleNot(const Node & n){
+Lit TseitinCnfStream::handleNot(const Node & n) {
   Assert(n.getKind() == NOT);
-  
+
   // n : NOT m
   Node m = n[0];
   Lit equivM = recTransform(m);
@@ -280,14 +281,14 @@ Lit TseitinCnfStream::handleNot(const Node & n){
 
 //FIXME: This function is a major hack! Should be changed ASAP
 //Assumes binary no else if branchs, and that ITEs 
-Lit TseitinCnfStream::handleIte(const Node & n){
+Lit TseitinCnfStream::handleIte(const Node & n) {
   Assert(n.getKind() == ITE);
-  
+
   // n : IF c THEN t ELSE f ENDIF;
   Lit c = recTransform(n[0]);
   Lit t = recTransform(n[1]);
   Lit f = recTransform(n[2]);
-  
+
   // d <-> IF c THEN tB ELSE fb
   // : d -> (c & tB) | (~c & fB)
   // : ~d | ( (c & tB) | (~c & fB) )
@@ -306,20 +307,20 @@ Lit TseitinCnfStream::handleIte(const Node & n){
 
   Lit d = aquireAndRegister(n);
 
-  insertClauseIntoStream(~d , ~c , t);
-  insertClauseIntoStream(~d ,  c , f);
-  insertClauseIntoStream(~d ,  f , t);
-  insertClauseIntoStream(~c , ~t , d);
-  insertClauseIntoStream( c , ~f , d);
+  insertClauseIntoStream(~d, ~c, t);
+  insertClauseIntoStream(~d, c, f);
+  insertClauseIntoStream(~d, f, t);
+  insertClauseIntoStream(~c, ~t, d);
+  insertClauseIntoStream(c, ~f, d);
 
   return d;
 }
 
 //FIXME: This function is a major hack! Should be changed ASAP
 //TODO: Should be moved. Not sure where...
-//TODO: Should use positive defintion, i.e. what kinds are atomic.
-bool atomic(const Node & n){
-  switch(n.getKind()){
+//TODO: Should use positive definition, i.e. what kinds are atomic.
+bool atomic(const Node & n) {
+  switch(n.getKind()) {
   case NOT:
   case XOR:
   case ITE:
@@ -334,16 +335,16 @@ bool atomic(const Node & n){
 
 //TODO: The following code assumes everthing is either
 // an atom or is a logical connective. This ignores quantifiers and lambdas.
-Lit TseitinCnfStream::recTransform(const Node & n){
-  if(isCached(n)){
+Lit TseitinCnfStream::recTransform(const Node & n) {
+  if(isCached(n)) {
     return lookupInCache(n);
   }
-  
-  if(atomic(n)){
+
+  if(atomic(n)) {
     return handleAtom(n);
-  }else{
+  } else {
     //Assume n is a logical connective
-    switch(n.getKind()){
+    switch(n.getKind()) {
     case NOT:
       return handleNot(n);
     case XOR:
@@ -361,61 +362,58 @@ Lit TseitinCnfStream::recTransform(const Node & n){
     }
   }
 }
-  
-void TseitinCnfStream::convertAndAssert(const Node & n){
+
+void TseitinCnfStream::convertAndAssert(const Node & n) {
   //n has already been mapped so use the previous result
-  if(isCached(n)){
+  if(isCached(n)) {
     Lit l = lookupInCache(n);
     insertClauseIntoStream(l);
     return;
   }
-  
+
   Lit e = recTransform(n);
-  insertClauseIntoStream( e );
+  insertClauseIntoStream(e);
 
   //I've commented the following section out because it uses a bit too much intelligence.
 
   /*
-  if(n.getKind() == AND){
-    // this code is required to efficiently flatten and
-    // assert each part of the node.
-    // This would be rendered unnessecary if the input was given differently
-    queue<Node> and_queue;
-    and_queue.push(n);
-
-    //This was changed to use a queue due to pressure on the C stack.
-
-    //TODO: this does no cacheing of what has been asserted.
-    //Low hanging fruit
-    while(!and_queue.empty()){
-      Node curr = and_queue.front();
-      and_queue.pop();
-      if(curr.getKind() == AND){
-	for(Node::iterator i = curr.begin(); i != curr.end(); ++i){
-	  and_queue.push(*i);
-	}
-      }else{
-	convertAndAssert(curr);
-      }
-    }
-  }else if(n.getKind() == OR){
-    //This is special cased so minimal translation is done for things that
-    //are already in CNF so minimal work is done on clauses.
-    vec<Lit> c;
-    for(Node::iterator i = n.begin(); i != n.end(); ++i){
-      Lit cl = recTransform(*i);
-      c.push(cl);
-    }
-    insertClauseIntoStream(c);
-  }else{
-    Lit e = recTransform(n);
-    insertClauseIntoStream( e );
-  }
-  */
+   if(n.getKind() == AND){
+   // this code is required to efficiently flatten and
+   // assert each part of the node.
+   // This would be rendered unnessecary if the input was given differently
+   queue<Node> and_queue;
+   and_queue.push(n);
+
+   //This was changed to use a queue due to pressure on the C stack.
+
+   //TODO: this does no cacheing of what has been asserted.
+   //Low hanging fruit
+   while(!and_queue.empty()){
+   Node curr = and_queue.front();
+   and_queue.pop();
+   if(curr.getKind() == AND){
+   for(Node::iterator i = curr.begin(); i != curr.end(); ++i){
+   and_queue.push(*i);
+   }
+   }else{
+   convertAndAssert(curr);
+   }
+   }
+   }else if(n.getKind() == OR){
+   //This is special cased so minimal translation is done for things that
+   //are already in CNF so minimal work is done on clauses.
+   vec<Lit> c;
+   for(Node::iterator i = n.begin(); i != n.end(); ++i){
+   Lit cl = recTransform(*i);
+   c.push(cl);
+   }
+   insertClauseIntoStream(c);
+   }else{
+   Lit e = recTransform(n);
+   insertClauseIntoStream( e );
+   }
+   */
 }
 
-
-
-
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index c0a70730a..131ac98dc 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -19,13 +19,9 @@
  ** 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"
@@ -34,45 +30,55 @@
 #include <map>
 
 namespace CVC4 {
-  class PropEngine;
+class PropEngine;
 }
 
-
 namespace CVC4 {
 namespace prop {
 
+/**
+ * Comments for the behavior of the whole class...
+ * @author Tim King <taking@cs.nyu.edu>
+ */
 class CnfStream {
 
 private:
+
   /**
-   * d_propEngine is the PropEngine that the CnfStream interacts with directly through
-   * the follwoing functions:
+   * d_propEngine is the PropEngine that the CnfStream interacts with directly
+   * through the following 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.
+  /**
+   * Cache of what literal have been registered to a node. Not strictly needed
+   * for correctness. This can be flushed when memory is under pressure.
+   * TODO: Use attributes when they arrive
    */
-  std::map<Node,minisat::Lit> d_translationCache;
-  
+  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
+   * May want to have internal data-structures 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);
-  
+  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;
+
+  /**
+   * Method comments...
+   * @param n
+   * @return returns ...
+   */
   minisat::Lit lookupInCache(const Node & n) const;
 
   /**
@@ -88,11 +94,11 @@ protected:
 public:
   /**
    * Constructs a CnfStream that sends constructs an equisatisfiable set of clauses
-   * and sends them to pe.
+   * and sends them to the given PropEngine.
+   * @param pe
    */
   CnfStream(CVC4::PropEngine *pe);
 
-
   /**
    * Converts and asserts a formula.
    * @param n node to convert and assert
@@ -101,13 +107,13 @@ public:
 
 }; /* 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.
+ * will be equivalent to each subexpression in the constructed equisatisfiable
+ * formula then substitute the new literal for the formula, and to do this
+ * recursively.
  * 
  * This implementation does this in a single recursive pass.
  */
@@ -121,11 +127,11 @@ 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)
+   * Each handleX(Node &n) is responsible for:
+   *   - constructing a new literal, l (if necessary)
    *   - calling registerNode(n,l)
-   *   - adding clauses asure that l is equivalent to the Node
-   *   - calling recTransform on its children (if nessecary)
+   *   - adding clauses assure that l is equivalent to the Node
+   *   - calling recTransform on its children (if necessary)
    *   - returning l
    *
    * handleX( n ) can assume that n is not in d_translationCache
@@ -140,19 +146,20 @@ private:
   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.
+   * 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()
+   * @param n ...
+   * @param target ...
    */
-  void mapRecTransformOverChildren(const Node& n, minisat::vec<minisat::Lit> & target);
+  void mapRecTransformOverChildren(const Node& n,
+                                   minisat::vec<minisat::Lit> & target);
 
-  //Recurisively dispatches the various Kinds to the appropriate handler.
+  //Recursively dispatches the various Kinds to the appropriate handler.
   minisat::Lit recTransform(const Node & n);
 
 }; /* class TseitinCnfStream */
@@ -160,6 +167,4 @@ private:
 }/* prop namespace */
 }/* CVC4 namespace */
 
-
-
 #endif /* __CVC4__CNF_STREAM_H */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 097500833..59eddccf0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -59,7 +59,7 @@ public:
   SmtEngine(ExprManager* em, Options* opts) throw();
 
   /**
-   * Destruct the smt engine.
+   * Destruct the SMT engine.
    */
   ~SmtEngine();