* Node::isAtomic() now looks at an "atomic" attribute of arguments

  instead of assuming it's atomic based on kind.  Atomicity is
  determined at node building time.  Fixes bug #81.  If this is
  determined to make node building too slow, we can allocate another
  attribute "AtomicHasBeenComputed" to lazily compute atomicity.

* TheoryImpl<> has gone away.  Theory implementations now derive from
  Theory directly and share a single RegisteredAttr attribute for term
  registration (which shouldn't overlap: every term is "owned" by
  exactly one Theory).  Fixes bug #79.

* Additional atomicity tests in ExprBlack unit test.

* More appropriate whitebox testing for attribute ID assignment
  (AttributeWhite unit test).

* Better (and more correct) assertion checking in NodeBuilderBlack.

* run-regression script now checks exit status against what's provided
  in "% EXIT: " gesture in .cvc input files, and stderr against
  "% EXPECT-ERROR: ".  These can be used to support intended failures.
  Fixes bug #84.  Also add "% EXIT: " gestures to all .cvc regressions
  in repository.

* Solved some "control reaches end of non-void function" warnings in
  src/parser/bounded_token_buffer.cpp by replacing
  "AlwaysAssert(false)" with "Unreachable()" (which is known
  statically to never return normally).

* Regression tests now use the cvc4 binary under
  builds/$(CURRENT_BUILD)/src/main instead of the one in bin/ which
  may not be properly installed yet at that point of the build.
  (Partially fixes bug #46.)

* -fvisibility=hidden is now included by configure.ac instead of each
   Makefile.am, which will make it easier to support platforms
   (e.g. cygwin) that do things a different way.

* TheoryUF code formatting.  (re: my code review bug #64)

* CDMap<> is leaking memory again, pending a fix for bug #85 in the
  context subsystem.  (To avoid serious errors, can't free context
  objects.)

* add ContextWhite unit test for bug #85 (though it's currently
  "defanged," awaiting the bugfix)

* Minor documentation, other cleanup.

1 files changed, 20 insertions, 20 deletions

diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp
index 1418e8f3c..29006b343 100644
--- a/src/parser/bounded_token_buffer.cpp
+++ b/src/parser/bounded_token_buffer.cpp
@@ -281,13 +281,13 @@ dbgTokLT  (pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k)
 static pANTLR3_COMMON_TOKEN
 LB(pANTLR3_COMMON_TOKEN_STREAM cts, ANTLR3_INT32 k)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_COMMON_TOKEN 
 get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_TOKEN_SOURCE 
@@ -306,19 +306,19 @@ setTokenSource	(   pANTLR3_TOKEN_STREAM ts,
 static pANTLR3_STRING	    
 toString    (pANTLR3_TOKEN_STREAM ts)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_STRING
 toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_STRING	    
 toStringTT  (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 /** Move the input pointer to the next incoming token.  The stream
@@ -395,13 +395,13 @@ discardOffChannel   (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_BOOLEAN dis
 static pANTLR3_VECTOR	    
 getTokens   (pANTLR3_COMMON_TOKEN_STREAM tokenStream)
 {
-    AlwaysAssert(false);
+    Unreachable();
 }
 
 static pANTLR3_LIST	    
 getTokenRange	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }                                                   
 /** Given a start and stop index, return a List of all tokens in
  *  the token type BitSet.  Return null if no tokens were found.  This
@@ -410,19 +410,19 @@ getTokenRange	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANT
 static pANTLR3_LIST	    
 getTokensSet	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, pANTLR3_BITSET types)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_LIST	    
 getTokensList	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, pANTLR3_LIST list)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_LIST	    
 getTokensType	(pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, ANTLR3_UINT32 type)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static ANTLR3_UINT32	    
@@ -450,13 +450,13 @@ _LA  (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
 static ANTLR3_UINT32	    
 dbgLA  (pANTLR3_INT_STREAM is, ANTLR3_INT32 i)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static ANTLR3_MARKER
 mark	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 /// As per mark() but with a call to tell the debugger we are doing this
@@ -464,7 +464,7 @@ mark	(pANTLR3_INT_STREAM is)
 static ANTLR3_MARKER
 dbgMark	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static void		    
@@ -476,7 +476,7 @@ release	(pANTLR3_INT_STREAM is, ANTLR3_MARKER mark)
 static ANTLR3_UINT32	    
 size	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static ANTLR3_MARKER   
@@ -496,33 +496,33 @@ tindex	(pANTLR3_INT_STREAM is)
 static void		    
 dbgRewindLast	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 static void		    
 rewindLast	(pANTLR3_INT_STREAM is)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 static void		    
 rewindStream	(pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 static void		    
 dbgRewindStream	(pANTLR3_INT_STREAM is, ANTLR3_MARKER marker)
 {
-   AlwaysAssert(false);
+   Unreachable();
 }
 
 static void		    
 seek	(pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
 {
-    AlwaysAssert(false);
+    Unreachable();
 }
 static void		    
 dbgSeek	(pANTLR3_INT_STREAM is, ANTLR3_MARKER index)
 {
-  AlwaysAssert(false);
+  Unreachable();
 }
 
 static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) {