diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-05-27 21:19:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-05-27 21:19:36 +0000 |
commit | 6ac90a806f563981bc25fe06bb0dde35d62da7a9 (patch) | |
tree | cbf5f3b1d4877cd6a7469356cfabbea5242d1d8f /src/theory | |
parent | 671a3d6d5ae8a89a1bb846a78f5ec9c064edc655 (diff) |
Remove isAtomic() as per 4/27/2010 meeting. Add comments about its potential design for later. Resolves bug 113, invalidates bugs 93 and 94.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/booleans/kinds | 16 | ||||
-rwxr-xr-x | src/theory/mktheoryof | 8 |
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"] |