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

2 files changed, 7 insertions, 17 deletions

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"]