Minor refactorings and corrections to comments

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 53abdb70388070f695708cbe379a5dfcd619e142..fcfca5296a32e7361159a7481206f8314694f9b2 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -707,14 +707,10 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) {
       // assume it's atomic if its kind can be atomic, check children
       // to see if that is actually true
       bool atomic = kind::kindCanBeAtomic(nv->getKind());
-      if(atomic) {
-        for(expr::NodeValue::nv_iterator i = nv->nv_begin();
-            i != nv->nv_end();
-            ++i) {
-          if(!(atomic = isAtomic(*i))) {
-            break;
-          }
-        }
+      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
+          atomic && i != nv->nv_end();
+          ++i) {
+        atomic = isAtomic(*i);
       }
 
       setAttribute(nv, AtomicAttr(), atomic);

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 611689c2bcbc26b1a9e5dc79f828c024053a5644..25134b413a9afba82e3cf4910aa7161d23c1a7af 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -271,7 +271,7 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
 SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
   Assert(!isCached(notNode), "Atom already mapped!");
   Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
-  Assert(notNode.getNumChildren() == 1, "Expecting exactly 2 children!");
+  Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!");
 
   SatLiteral notLit = ~toCNF(notNode[0]);
 
@@ -341,29 +341,29 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
 
 void TseitinCnfStream::convertAndAssert(TNode node) {
   Debug("cnf") << "convertAndAssert(" << node << ")" << endl;
-  // If the node is a conjuntion, we handle each conjunct separatelu
   if(node.getKind() == AND) {
-    TNode::const_iterator conjunct = node.begin();
-    TNode::const_iterator node_end = node.end();
-    while(conjunct != node_end) {
+    // If the node is a conjunction, we handle each conjunct separately
+    for( TNode::const_iterator conjunct = node.begin(),
+         node_end = node.end();
+         conjunct != node_end;
+         ++conjunct ) {
       convertAndAssert(*conjunct);
-      ++ conjunct;
     }
-    return;
-  }
-  // If the node is a disjunction, we construct a clause and assert it
-  if(node.getKind() == OR) {
+  } else if(node.getKind() == OR) {
+    // If the node is a disjunction, we construct a clause and assert it
     int nChildren = node.getNumChildren();
     SatClause clause(nChildren);
     TNode::const_iterator disjunct = node.begin();
     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
+      Assert( disjunct != node.end() );
       clause[i] = toCNF(*disjunct);
     }
+    Assert( disjunct == node.end() );
     assertClause(clause);
-    return;
+  } else {
+    // Otherwise, we just convert using the definitional transformation
+    assertClause(toCNF(node));
   }
-  // Otherwise, we just convert using the definitional transformation
-  assertClause(toCNF(node));
 }
 
 }/* CVC4::prop namespace */

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 66cdaa730a28ae67f522e603ca0f032070182fe5..9a63c26f904c03b99250484c673c2de96e739523 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -11,12 +11,12 @@
  ** information.
  **
  ** This class takes a sequence of formulas.
- ** It outputs a stream of clauses that is propositional
- ** equisatisfiable with the conjunction of the formulas.
+ ** It outputs a stream of clauses that is propositionally
+ ** equi-satisfiable 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 
+ ** internals such as the representation and translation of [??? -Chris]
  **/
 
 #include "cvc4_private.h"
@@ -35,7 +35,7 @@ namespace prop {
 class PropEngine;
 
 /**
- * Comments for the behavior of the whole class...
+ * Comments for the behavior of the whole class... [??? -Chris]
  * @author Tim King <taking@cs.nyu.edu>
  */
 class CnfStream {
@@ -45,7 +45,7 @@ private:
   /** The SAT solver we will be using */
   SatSolver *d_satSolver;
 
-  /** Cache of what literal have been registered to a node. */
+  /** Cache of what literals have been registered to a node. */
   typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
   TranslationCache d_translationCache;
 
@@ -139,15 +139,17 @@ public:
   virtual void convertAndAssert(TNode node) = 0;
 
   /**
-   * Returns a node the is represented by a give SatLiteral literal.
+   * Get the node that is represented by the given SatLiteral.
    * @param literal the literal from the sat solver
    * @return the actual node
    */
   Node getNode(const SatLiteral& literal);
 
   /**
-   * Returns the literal the represents the given node in the SAT CNF
-   * representation.
+   * Returns the literal that represents the given node in the SAT CNF
+   * representation. [Presumably there are some constraints on the kind
+   * of node? E.g., it needs to be a boolean? -Chris]
+   *
    */
   SatLiteral getLiteral(TNode node);
 
@@ -156,12 +158,12 @@ public:
 /**
  * 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 substitute the new literal for the formula, and to do this
+ * The general idea is to introduce a new literal that
+ * will be equivalent to each subexpression in the constructed equi-satisfiable
+ * formula, then substitute the new literal for the formula, and so on,
  * recursively.
  * 
- * This implementation does this in a single recursive pass.
+ * This implementation does this in a single recursive pass. [??? -Chris]
  */
 class TseitinCnfStream : public CnfStream {