Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential design for later. Resolves bug 113, invalidates bugs 93 and 94.

12 files changed, 49 insertions, 177 deletions

diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds
index 5ce38f5fd..50b858b31 100644
--- a/src/expr/builtin_kinds
+++ b/src/expr/builtin_kinds
@@ -17,13 +17,10 @@
 #     SKOLEM.
 #
 #   operator K #children ["comment"]
-#   nonatomic_operator K #children ["comment"]
 #
 #     Declares a "built-in" operator kind K.  Really this is the same
 #     as "variable" except that it has an operator (automatically
-#     generated by NodeManager).  These two commands are identical,
-#     except that kinds declared with nonatomic_operator answer false
-#     to Node::isAtomic().
+#     generated by NodeManager).
 #
 #     You can specify an exact # of children required as the second
 #     argument to the operator command.  In debug mode, assertions are
@@ -134,4 +131,4 @@ constant BITVECTOR_TYPE \
 	"::CVC4::UnsignedHashStrategy< ::CVC4::BitVectorSize >" \
 	"util/bitvector.h" \
 	"bit-vector type" 
-	
\ No newline at end of file
+	
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 876b400fe..5c4e30a0c 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -182,12 +182,6 @@ bool Expr::isConst() const {
   return d_node->isConst();
 }
 
-bool Expr::isAtomic() const {
-  ExprManagerScope ems(*this);
-  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
-  return d_node->isAtomic();
-}
-
 void Expr::toStream(std::ostream& out) const {
   ExprManagerScope ems(*this);
   d_node->toStream(out);
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 99b57b0c2..08dd1d25f 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -211,11 +211,19 @@ public:
    */
   bool isConst() const;
 
-  /**
-   * Check if this is an expression representing a constant.
-   * @return true if a constant expression
-   */
-  bool isAtomic() const;
+  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
+   *
+   * It has been decided for now to hold off on implementations of
+   * these functions, as they may only be needed in CNF conversion,
+   * where it's pointless to do a lazy isAtomic determination by
+   * searching through the DAG, and storing it, since the result will
+   * only be used once.  For more details see the 4/27/2010 CVC4
+   * developer's meeting notes at:
+   *
+   * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
+   */
+  // bool containsDecision(); // is "atomic"
+  // bool properlyContainsDecision(); // maybe not atomic but all children are
 
   /** Extract a constant of type T */
   template <class T>
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 5b0ac150b..3c17507cf 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -127,22 +127,6 @@ ${metakind_kinds}
 }/* metaKindOf(k) */
 
 /**
- * Determine if a particular kind can be atomic or not.  Some kinds
- * are never atomic (OR, NOT, ITE...), some can be atomic depending on
- * their children (PLUS might have an ITE under it, for instance).
- */
-static inline bool kindCanBeAtomic(Kind k) {
-  static const bool canBeAtomic[] = {
-    false, /* NULL_EXPR */
-${metakind_canbeatomic}
-    false /* LAST_KIND */
-  };/* canBeAtomic[] */
-
-  return canBeAtomic[k];
-}/* kindCanBeAtomic(k) */
-
-
-/**
  * Map a kind of the operator to the kind of the enclosing expression. For
  * example, since the kind of functions is just VARIABLE, it should map
  * VARIABLE to APPLY_UF.
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index f59388def..35a245a84 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -104,14 +104,6 @@ function operator {
   check_theory_seen
 }
 
-function nonatomic_operator {
-  # nonatomic_operator K #children ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  check_theory_seen
-}
-
 function parameterized {
   # parameterized K #children ["comment"]
 
diff --git a/src/expr/mkkind b/src/expr/mkkind
index d9c64b660..a417b7871 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -83,15 +83,6 @@ function operator {
   register_kind "$1" "$2" "$3"
 }
 
-function nonatomic_operator {
-  # nonatomic_operator K #children ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  check_theory_seen
-  register_kind "$1" "$2" "$3"
-}
-
 function parameterized {
   # parameterized K1 K2 #children ["comment"]
 
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 4915a17ec..cf3fb1e97 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -99,15 +99,6 @@ function operator {
   register_metakind OPERATOR "$1" "$2"
 }
 
-function nonatomic_operator {
-  # nonatomic_operator K #children ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  check_theory_seen
-  register_metakind NONATOMIC_OPERATOR "$1" "$2"
-}
-
 function parameterized {
   # parameterized K1 K2 #children ["comment"]
 
@@ -217,16 +208,6 @@ function register_metakind {
   k=$2
   nc=$3
 
-
-  if [ $mk = NONATOMIC_OPERATOR ]; then
-    metakind_canbeatomic="${metakind_canbeatomic}    false, /* $k */
-";
-    mk=OPERATOR
-  else
-    metakind_canbeatomic="${metakind_canbeatomic}    true, /* $k */
-";
-  fi
-
   metakind_kinds="${metakind_kinds}    metakind::$mk, /* $k */
 ";
 
@@ -297,9 +278,6 @@ while [ $# -gt 0 ]; do
   metakind_kinds="${metakind_kinds}
     /* from $b */
 "
-  metakind_canbeatomic="${metakind_canbeatomic}
-    /* from $b */
-"
   metakind_operatorKinds="${metakind_operatorKinds}
     /* from $b */
 "
@@ -315,7 +293,6 @@ text=$(cat "$template")
 for var in \
     metakind_includes \
     metakind_kinds \
-    metakind_canbeatomic \
     metakind_constantMaps \
     metakind_compares \
     metakind_constHashes \
diff --git a/src/expr/node.h b/src/expr/node.h
index 2abe762ed..0daa3f58c 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -253,11 +253,19 @@ public:
     return NodeTemplate(d_nv->getChild(i));
   }
 
-  /**
-   * Returns true if this node is atomic (has no more Boolean structure)
-   * @return true if atomic
+  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
+   *
+   * It has been decided for now to hold off on implementations of
+   * these functions, as they may only be needed in CNF conversion,
+   * where it's pointless to do a lazy isAtomic determination by
+   * searching through the DAG, and storing it, since the result will
+   * only be used once.  For more details see the 4/27/2010 CVC4
+   * developer's meeting notes at:
+   *
+   * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
    */
-  inline bool isAtomic() const;
+  // bool containsDecision(); // is "atomic"
+  // bool properlyContainsDecision(); // maybe not atomic but all children are
 
   /**
    * Returns true if this node represents a constant
@@ -686,15 +694,6 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
 template <bool ref_count>
 NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null);
 
-template <bool ref_count>
-inline bool NodeTemplate<ref_count>::isAtomic() const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
-  return NodeManager::currentNM()->isAtomic(*this);
-}
-
 // FIXME: escape from type system convenient but is there a better
 // way?  Nodes conceptually don't change their expr values but of
 // course they do modify the refcount.  But it's nice to be able to
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 35e73842e..098694c3d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -211,39 +211,24 @@ class NodeManager {
 
   // attribute tags
   struct TypeTag {};
-  struct AtomicTag {};
 
   // NodeManager's attributes.  These aren't exposed outside of this
   // class; use the getters.
   typedef expr::Attribute<TypeTag, TypeNode> TypeAttr;
-  typedef expr::Attribute<AtomicTag, bool> AtomicAttr;
 
-  /**
-   * Returns true if this node is atomic (has no more Boolean
-   * structure).  This is the NodeValue version for NodeManager's
-   * internal use.  There's a public version of this function below
-   * that takes a TNode.
-   * @param nv the node to check for atomicity
-   * @return true if atomic
-   */
-  inline bool isAtomic(expr::NodeValue* nv) const {
-    // The kindCanBeAtomic() and metakind checking are just optimizations
-    // (to avoid the hashtable lookup).  We assume that all nodes have
-    // the atomic attribute pre-computed and set at their time of
-    // creation.  This is because:
-    // (1) it's super cheap to do it bottom-up.
-    // (2) if we computed it lazily, we'd need a second attribute to
-    //     tell us whether we had computed it yet or not.
-    // The pre-computation and registration occurs in poolInsert().
-    AssertArgument(nv->getMetaKind() != kind::metakind::INVALID, *nv,
-                   "NodeManager::isAtomic() called on INVALID node (%s)",
-                   kind::kindToString(nv->getKind()).c_str());
-    return
-      nv->getMetaKind() == kind::metakind::VARIABLE ||
-      nv->getMetaKind() == kind::metakind::CONSTANT ||
-      ( kind::kindCanBeAtomic(nv->getKind()) &&
-        getAttribute(nv, AtomicAttr()) );
-  }
+  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
+   *
+   * It has been decided for now to hold off on implementations of
+   * these functions, as they may only be needed in CNF conversion,
+   * where it's pointless to do a lazy isAtomic determination by
+   * searching through the DAG, and storing it, since the result will
+   * only be used once.  For more details see the 4/27/2010 CVC4
+   * developer's meeting notes at:
+   *
+   * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
+   */
+  // bool containsDecision(TNode); // is "atomic"
+  // bool properlyContainsDecision(TNode); // all children are atomic
 
 public:
 
@@ -529,15 +514,6 @@ public:
    * Get the type for the given node.
    */
   TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate);
-
-  /**
-   * Returns true if this node is atomic (has no more Boolean structure)
-   * @param n the node to check for atomicity
-   * @return true if atomic
-   */
-  inline bool isAtomic(TNode n) const {
-    return isAtomic(n.d_nv);
-  }
 };
 
 /**
@@ -707,35 +683,6 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) {
   Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
          "NodeValue already in the pool!");
   d_nodeValuePool.insert(nv);// FIXME multithreading
-
-  switch(nv->getMetaKind()) {
-  case kind::metakind::INVALID:
-  case kind::metakind::VARIABLE:
-  case kind::metakind::CONSTANT:
-    // nothing to do (don't bother setting the attribute, isAtomic()
-    // on VARIABLEs and CONSTANTs is always true)
-    break;
-
-  case kind::metakind::OPERATOR:
-  case kind::metakind::PARAMETERIZED:
-    {
-      // register this NodeValue as atomic or not; use nv_begin/end
-      // because we need to consider the operator too in the case of
-      // PARAMETERIZED-metakinded nodes (i.e. APPLYs); they could have a
-      // buried ITE.
-
-      // 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());
-      for(expr::NodeValue::nv_iterator i = nv->nv_begin();
-          atomic && i != nv->nv_end();
-          ++i) {
-        atomic = isAtomic(*i);
-      }
-
-      setAttribute(nv, AtomicAttr(), atomic);
-    }
-  }
 }
 
 inline void NodeManager::poolRemove(expr::NodeValue* nv) {
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index a245eb469..219c25399 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -115,11 +115,10 @@ const CnfStream::TranslationCache& CnfStream::getTranslationCache() const {
 }
 
 SatLiteral TseitinCnfStream::handleAtom(TNode node) {
-  Assert(node.isAtomic(), "handleAtom(n) expects n to be an atom");
   Assert(!isCached(node), "atom already mapped!");
 
   Debug("cnf") << "handleAtom(" << node << ")" << endl;
- 
+
   bool theoryLiteral = node.getKind() != kind::VARIABLE;
   SatLiteral lit = newLiteral(node, theoryLiteral);
 
@@ -378,11 +377,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
     return lookupInCache(node);
   }
 
-  // Atomic nodes are treated specially
-  if(node.isAtomic()) {
-    return handleAtom(node);
-  }
-
   // Handle each Boolean operator case
   switch(node.getKind()) {
   case NOT:
@@ -402,8 +396,7 @@ SatLiteral TseitinCnfStream::toCNF(TNode node) {
   default:
     {
       Node atomic = handleNonAtomicNode(node);
-      AlwaysAssert(isCached(atomic) || atomic.isAtomic());
-      return toCNF(atomic);
+      return isCached(atomic) ? lookupInCache(atomic) : handleAtom(atomic);
     }
   }
 }
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index bd85af69d..43c37f4b7 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -12,12 +12,10 @@ constant CONST_BOOLEAN \
     "util/bool.h" \
     "truth and falsity"
 
-# these are nonatomic because they have boolean structure.
-# i.e. nodes n with this kind return false for n.isAtomic()
-nonatomic_operator NOT 1 "logical not"
-nonatomic_operator AND 2: "logical and"
-nonatomic_operator IFF 2 "logical equivalence"
-nonatomic_operator IMPLIES 2 "logical implication"
-nonatomic_operator OR 2: "logical or"
-nonatomic_operator XOR 2 "exclusive or"
-nonatomic_operator ITE 3 "if-then-else"
+operator NOT 1 "logical not"
+operator AND 2: "logical and"
+operator IFF 2 "logical equivalence"
+operator IMPLIES 2 "logical implication"
+operator OR 2: "logical or"
+operator XOR 2 "exclusive or"
+operator ITE 3 "if-then-else"
diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof
index 842e02a07..227831451 100755
--- a/src/theory/mktheoryof
+++ b/src/theory/mktheoryof
@@ -84,14 +84,6 @@ function operator {
   do_theoryof "$1"
 }
 
-function nonatomic_operator {
-  # nonatomic_operator K #children ["comment"]
-
-  lineno=${BASH_LINENO[0]}
-
-  do_theoryof "$1"
-}
-
 function parameterized {
   # parameterized K #children ["comment"]