Document term db (#1220)

* Document TermDb and related classes. Minor changes to quantifiers utils and their interface.  Address some comments left over from PR 1206.

* Minor

* Minor

* Change namespace style.

* Address review

* Fix incorrectly merged portion that led to regression failures.

* New clang format, fully document relevant domain.

* Clang format again.

* Minor

1 files changed, 19 insertions, 11 deletions

diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index c9a7f07ab..d02ad667e 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -22,11 +22,12 @@
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
-using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
 
 QuantAttributes::QuantAttributes( QuantifiersEngine * qe ) : 
 d_quantEngine(qe) {
@@ -94,7 +95,10 @@ bool QuantAttributes::checkRewriteRule( Node q ) {
 }
 
 Node QuantAttributes::getRewriteRule( Node q ) {
-  if( q.getKind()==FORALL && q.getNumChildren()==3 && q[2].getNumChildren()>0 && q[2][0][0].getKind()==REWRITE_RULE ){
+  if (q.getKind() == FORALL && q.getNumChildren() == 3
+      && q[2][0].getNumChildren() > 0
+      && q[2][0][0].getKind() == REWRITE_RULE)
+  {
     return q[2][0][0];
   }else{
     return Node::null();
@@ -121,12 +125,13 @@ bool QuantAttributes::checkFunDefAnnotation( Node ipl ) {
 Node QuantAttributes::getFunDefHead( Node q ) {
   //&& q[1].getKind()==EQUAL && q[1][0].getKind()==APPLY_UF &&
   if( q.getKind()==FORALL && q.getNumChildren()==3 ){
-
-    for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
-      if( q[2][i].getKind()==INST_ATTRIBUTE ){
-        if( q[2][i][0].getAttribute(FunDefAttribute()) ){
-          return q[2][i][0];
-        }
+    Node ipl = q[2];
+    for (unsigned i = 0; i < ipl.getNumChildren(); i++)
+    {
+      if (ipl[i].getKind() == INST_ATTRIBUTE
+          && ipl[i][0].getAttribute(FunDefAttribute()))
+      {
+        return ipl[i][0];
       }
     }
   }
@@ -197,7 +202,7 @@ void QuantAttributes::computeAttributes( Node q ) {
     Node f = d_qattr[q].d_fundef_f;
     if( d_fun_defs.find( f )!=d_fun_defs.end() ){
       Message() << "Cannot define function " << f << " more than once." << std::endl;
-      exit( 1 );
+      AlwaysAssert(false);
     }
     d_fun_defs[f] = true;
     d_quantEngine->setOwner( q, d_quantEngine->getFunDefEngine(), 2 );
@@ -383,3 +388,6 @@ Node QuantAttributes::getQuantIdNumNode( Node q ) {
   }
 }
 
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */