Applying clang-format to parser.cpp.

1 files changed, 156 insertions, 174 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index c3c533576..ac93c93d2 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -41,39 +41,39 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace parser {
 
-Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode, bool parseOnly) :
-  d_exprManager(exprManager),
-  d_resourceManager(d_exprManager->getResourceManager()),
-  d_input(input),
-  d_symtabAllocated(),
-  d_symtab(&d_symtabAllocated),
-  d_assertionLevel(0),
-  d_globalDeclarations(false),
-  d_anonymousFunctionCount(0),
-  d_done(false),
-  d_checksEnabled(true),
-  d_strictMode(strictMode),
-  d_parseOnly(parseOnly),
-  d_canIncludeFile(true),
-  d_logicIsForced(false),
-  d_forcedLogic() {
+Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode,
+               bool parseOnly)
+    : d_exprManager(exprManager),
+      d_resourceManager(d_exprManager->getResourceManager()),
+      d_input(input),
+      d_symtabAllocated(),
+      d_symtab(&d_symtabAllocated),
+      d_assertionLevel(0),
+      d_globalDeclarations(false),
+      d_anonymousFunctionCount(0),
+      d_done(false),
+      d_checksEnabled(true),
+      d_strictMode(strictMode),
+      d_parseOnly(parseOnly),
+      d_canIncludeFile(true),
+      d_logicIsForced(false),
+      d_forcedLogic() {
   d_input->setParser(*this);
 }
 
 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
   checkDeclaration(name, CHECK_DECLARED, type);
-  assert( isDeclared(name, type) );
+  assert(isDeclared(name, type));
 
-  if(type == SYM_VARIABLE) {
+  if (type == SYM_VARIABLE) {
     // Functions share var namespace
     return d_symtab->lookup(name);
   }
 
-  assert(false);//Unhandled(type);
+  assert(false);  // Unhandled(type);
   return Expr();
 }
 
-
 Expr Parser::getVariable(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
@@ -82,32 +82,30 @@ Expr Parser::getFunction(const std::string& name) {
   return getSymbol(name, SYM_VARIABLE);
 }
 
-Type Parser::getType(const std::string& var_name,
-                     SymbolType type) {
+Type Parser::getType(const std::string& var_name, SymbolType type) {
   checkDeclaration(var_name, CHECK_DECLARED, type);
-  assert( isDeclared(var_name, type) );
+  assert(isDeclared(var_name, type));
   Type t = getSymbol(var_name, type).getType();
   return t;
 }
 
 Type Parser::getSort(const std::string& name) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
-  assert( isDeclared(name, SYM_SORT) );
+  assert(isDeclared(name, SYM_SORT));
   Type t = d_symtab->lookupType(name);
   return t;
 }
 
-Type Parser::getSort(const std::string& name,
-                     const std::vector<Type>& params) {
+Type Parser::getSort(const std::string& name, const std::vector<Type>& params) {
   checkDeclaration(name, CHECK_DECLARED, SYM_SORT);
-  assert( isDeclared(name, SYM_SORT) );
+  assert(isDeclared(name, SYM_SORT));
   Type t = d_symtab->lookupType(name, params);
   return t;
 }
 
-size_t Parser::getArity(const std::string& sort_name){
+size_t Parser::getArity(const std::string& sort_name) {
   checkDeclaration(sort_name, CHECK_DECLARED, SYM_SORT);
-  assert( isDeclared(sort_name, SYM_SORT) );
+  assert(isDeclared(sort_name, SYM_SORT));
   return d_symtab->lookupArity(sort_name);
 }
 
@@ -119,12 +117,12 @@ bool Parser::isBoolean(const std::string& name) {
 /* Returns true if name is bound to a function-like thing (function,
  * constructor, tester, or selector). */
 bool Parser::isFunctionLike(const std::string& name) {
-  if(!isDeclared(name, SYM_VARIABLE)) {
+  if (!isDeclared(name, SYM_VARIABLE)) {
     return false;
   }
   Type type = getType(name);
-  return type.isFunction() || type.isConstructor() ||
-    type.isTester() || type.isSelector();
+  return type.isFunction() || type.isConstructor() || type.isTester() ||
+         type.isSelector();
 }
 
 /* Returns true if name is bound to a defined function. */
@@ -146,9 +144,8 @@ bool Parser::isPredicate(const std::string& name) {
   return isDeclared(name, SYM_VARIABLE) && getType(name).isPredicate();
 }
 
-Expr
-Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
-  if(d_globalDeclarations) {
+Expr Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
+  if (d_globalDeclarations) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
@@ -157,17 +154,16 @@ Parser::mkVar(const std::string& name, const Type& type, uint32_t flags) {
   return expr;
 }
 
-Expr
-Parser::mkBoundVar(const std::string& name, const Type& type) {
+Expr Parser::mkBoundVar(const std::string& name, const Type& type) {
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
   Expr expr = d_exprManager->mkBoundVar(name, type);
   defineVar(name, expr, false);
   return expr;
 }
 
-Expr
-Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
-  if(d_globalDeclarations) {
+Expr Parser::mkFunction(const std::string& name, const Type& type,
+                        uint32_t flags) {
+  if (d_globalDeclarations) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "mkVar(" << name << ", " << type << ")" << std::endl;
@@ -176,9 +172,9 @@ Parser::mkFunction(const std::string& name, const Type& type, uint32_t flags) {
   return expr;
 }
 
-Expr
-Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_t flags) {
-  if(d_globalDeclarations) {
+Expr Parser::mkAnonymousFunction(const std::string& prefix, const Type& type,
+                                 uint32_t flags) {
+  if (d_globalDeclarations) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   stringstream name;
@@ -186,63 +182,60 @@ Parser::mkAnonymousFunction(const std::string& prefix, const Type& type, uint32_
   return d_exprManager->mkVar(name.str(), type, flags);
 }
 
-std::vector<Expr>
-Parser::mkVars(const std::vector<std::string> names, const Type& type, uint32_t flags) {
-  if(d_globalDeclarations) {
+std::vector<Expr> Parser::mkVars(const std::vector<std::string> names,
+                                 const Type& type, uint32_t flags) {
+  if (d_globalDeclarations) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   std::vector<Expr> vars;
-  for(unsigned i = 0; i < names.size(); ++i) {
+  for (unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkVar(names[i], type, flags));
   }
   return vars;
 }
 
-std::vector<Expr>
-Parser::mkBoundVars(const std::vector<std::string> names, const Type& type) {
+std::vector<Expr> Parser::mkBoundVars(const std::vector<std::string> names,
+                                      const Type& type) {
   std::vector<Expr> vars;
-  for(unsigned i = 0; i < names.size(); ++i) {
+  for (unsigned i = 0; i < names.size(); ++i) {
     vars.push_back(mkBoundVar(names[i], type));
   }
   return vars;
 }
 
-void
-Parser::defineVar(const std::string& name, const Expr& val, bool levelZero) {
-  Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;;
+void Parser::defineVar(const std::string& name, const Expr& val,
+                       bool levelZero) {
+  Debug("parser") << "defineVar( " << name << " := " << val << ")" << std::endl;
   d_symtab->bind(name, val, levelZero);
-  assert( isDeclared(name) );
+  assert(isDeclared(name));
 }
 
-void
-Parser::defineFunction(const std::string& name, const Expr& val, bool levelZero) {
+void Parser::defineFunction(const std::string& name, const Expr& val,
+                            bool levelZero) {
   d_symtab->bindDefinedFunction(name, val, levelZero);
-  assert( isDeclared(name) );
+  assert(isDeclared(name));
 }
 
-void
-Parser::defineType(const std::string& name, const Type& type) {
+void Parser::defineType(const std::string& name, const Type& type) {
   d_symtab->bindType(name, type);
-  assert( isDeclared(name, SYM_SORT) );
+  assert(isDeclared(name, SYM_SORT));
 }
 
-void
-Parser::defineType(const std::string& name,
-                   const std::vector<Type>& params,
-                   const Type& type) {
+void Parser::defineType(const std::string& name,
+                        const std::vector<Type>& params, const Type& type) {
   d_symtab->bindType(name, params, type);
-  assert( isDeclared(name, SYM_SORT) );
+  assert(isDeclared(name, SYM_SORT));
 }
 
-void
-Parser::defineParameterizedType(const std::string& name,
-                                const std::vector<Type>& params,
-                                const Type& type) {
-  if(Debug.isOn("parser")) {
-    Debug("parser") << "defineParameterizedType(" << name << ", " << params.size() << ", [";
-    if(params.size() > 0) {
+void Parser::defineParameterizedType(const std::string& name,
+                                     const std::vector<Type>& params,
+                                     const Type& type) {
+  if (Debug.isOn("parser")) {
+    Debug("parser") << "defineParameterizedType(" << name << ", "
+                    << params.size() << ", [";
+    if (params.size() > 0) {
       copy(params.begin(), params.end() - 1,
-           ostream_iterator<Type>(Debug("parser"), ", ") );
+           ostream_iterator<Type>(Debug("parser"), ", "));
       Debug("parser") << params.back();
     }
     Debug("parser") << "], " << type << ")" << std::endl;
@@ -250,9 +243,8 @@ Parser::defineParameterizedType(const std::string& name,
   defineType(name, params, type);
 }
 
-SortType
-Parser::mkSort(const std::string& name, uint32_t flags) {
-  if(d_globalDeclarations) {
+SortType Parser::mkSort(const std::string& name, uint32_t flags) {
+  if (d_globalDeclarations) {
     flags |= ExprManager::VAR_FLAG_GLOBAL;
   }
   Debug("parser") << "newSort(" << name << ")" << std::endl;
@@ -261,8 +253,8 @@ Parser::mkSort(const std::string& name, uint32_t flags) {
   return type;
 }
 
-SortConstructorType
-Parser::mkSortConstructor(const std::string& name, size_t arity) {
+SortConstructorType Parser::mkSortConstructor(const std::string& name,
+                                              size_t arity) {
   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
   SortConstructorType type = d_exprManager->mkSortConstructor(name, arity);
@@ -276,84 +268,79 @@ SortType Parser::mkUnresolvedType(const std::string& name) {
   return unresolved;
 }
 
-SortConstructorType
-Parser::mkUnresolvedTypeConstructor(const std::string& name,
-                                    size_t arity) {
+SortConstructorType Parser::mkUnresolvedTypeConstructor(const std::string& name,
+                                                        size_t arity) {
   SortConstructorType unresolved = mkSortConstructor(name, arity);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
 
-SortConstructorType
-Parser::mkUnresolvedTypeConstructor(const std::string& name,
-                                    const std::vector<Type>& params) {
-  Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")"
-                  << std::endl;
-  SortConstructorType unresolved = d_exprManager->mkSortConstructor(name, params.size());
+SortConstructorType Parser::mkUnresolvedTypeConstructor(
+    const std::string& name, const std::vector<Type>& params) {
+  Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
+                  << ")" << std::endl;
+  SortConstructorType unresolved =
+      d_exprManager->mkSortConstructor(name, params.size());
   defineType(name, params, unresolved);
-  Type t = getSort( name, params );
+  Type t = getSort(name, params);
   d_unresolved.insert(unresolved);
   return unresolved;
 }
 
 bool Parser::isUnresolvedType(const std::string& name) {
-  if(!isDeclared(name, SYM_SORT)) {
+  if (!isDeclared(name, SYM_SORT)) {
     return false;
   }
   return d_unresolved.find(getSort(name)) != d_unresolved.end();
 }
 
-std::vector<DatatypeType>
-Parser::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes) {
-
+std::vector<DatatypeType> Parser::mkMutualDatatypeTypes(
+    std::vector<Datatype>& datatypes) {
   try {
     std::vector<DatatypeType> types =
-      d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
+        d_exprManager->mkMutualDatatypeTypes(datatypes, d_unresolved);
 
     assert(datatypes.size() == types.size());
 
-    for(unsigned i = 0; i < datatypes.size(); ++i) {
+    for (unsigned i = 0; i < datatypes.size(); ++i) {
       DatatypeType t = types[i];
       const Datatype& dt = t.getDatatype();
       const std::string& name = dt.getName();
       Debug("parser-idt") << "define " << name << " as " << t << std::endl;
-      if(isDeclared(name, SYM_SORT)) {
+      if (isDeclared(name, SYM_SORT)) {
         throw ParserException(name + " already declared");
       }
-      if( t.isParametric() ) {
-        std::vector< Type > paramTypes = t.getParamTypes();
-        defineType(name, paramTypes, t );
+      if (t.isParametric()) {
+        std::vector<Type> paramTypes = t.getParamTypes();
+        defineType(name, paramTypes, t);
       } else {
         defineType(name, t);
       }
-      for(Datatype::const_iterator j = dt.begin(),
-            j_end = dt.end();
-          j != j_end;
-          ++j) {
+      for (Datatype::const_iterator j = dt.begin(), j_end = dt.end();
+           j != j_end; ++j) {
         const DatatypeConstructor& ctor = *j;
         expr::ExprPrintTypes::Scope pts(Debug("parser-idt"), true);
         Expr constructor = ctor.getConstructor();
         Debug("parser-idt") << "+ define " << constructor << std::endl;
         string constructorName = ctor.getName();
-        if(isDeclared(constructorName, SYM_VARIABLE)) {
+        if (isDeclared(constructorName, SYM_VARIABLE)) {
           throw ParserException(constructorName + " already declared");
         }
         defineVar(constructorName, constructor);
         Expr tester = ctor.getTester();
         Debug("parser-idt") << "+ define " << tester << std::endl;
         string testerName = ctor.getTesterName();
-        if(isDeclared(testerName, SYM_VARIABLE)) {
+        if (isDeclared(testerName, SYM_VARIABLE)) {
           throw ParserException(testerName + " already declared");
         }
         defineVar(testerName, tester);
-        for(DatatypeConstructor::const_iterator k = ctor.begin(),
-              k_end = ctor.end();
-            k != k_end;
-            ++k) {
+        for (DatatypeConstructor::const_iterator k = ctor.begin(),
+                                                 k_end = ctor.end();
+             k != k_end; ++k) {
           Expr selector = (*k).getSelector();
           Debug("parser-idt") << "+++ define " << selector << std::endl;
           string selectorName = (*k).getName();
-          if(isDeclared(selectorName, SYM_VARIABLE)) {
+          if (isDeclared(selectorName, SYM_VARIABLE)) {
             throw ParserException(selectorName + " already declared");
           }
           defineVar(selectorName, selector);
@@ -365,29 +352,30 @@ Parser::mkMutualDatatypeTypes(std::vector<Datatype>& datatypes) {
     // complained of a bad substitution if anything is left unresolved.
     // Clear out the set.
     d_unresolved.clear();
-    
-    //throw exception if any datatype is not well-founded
-    for(unsigned i = 0; i < datatypes.size(); ++i) {
+
+    // throw exception if any datatype is not well-founded
+    for (unsigned i = 0; i < datatypes.size(); ++i) {
       const Datatype& dt = types[i].getDatatype();
-      if( !dt.isCodatatype() && !dt.isWellFounded() ){
+      if (!dt.isCodatatype() && !dt.isWellFounded()) {
         throw ParserException(dt.getName() + " is not well-founded");
       }
     }
-    
+
     return types;
-  } catch(IllegalArgumentException& ie) {
+  } catch (IllegalArgumentException& ie) {
     throw ParserException(ie.getMessage());
   }
 }
 
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
-  switch(type) {
-  case SYM_VARIABLE:
-    return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name);
-  case SYM_SORT:
-    return d_symtab->isBoundType(name);
+  switch (type) {
+    case SYM_VARIABLE:
+      return d_reservedSymbols.find(name) != d_reservedSymbols.end() ||
+             d_symtab->isBound(name);
+    case SYM_SORT:
+      return d_symtab->isBoundType(name);
   }
-  assert(false);//Unhandled(type);
+  assert(false);  // Unhandled(type);
   return false;
 }
 
@@ -397,58 +385,55 @@ void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
 }
 
 void Parser::checkDeclaration(const std::string& varName,
-                              DeclarationCheck check,
-                              SymbolType type,
-                              std::string notes)
-    throw(ParserException) {
-  if(!d_checksEnabled) {
+                              DeclarationCheck check, SymbolType type,
+                              std::string notes) throw(ParserException) {
+  if (!d_checksEnabled) {
     return;
   }
 
-  switch(check) {
-  case CHECK_DECLARED:
-    if( !isDeclared(varName, type) ) {
-      parseError("Symbol '" + varName + "' not declared as a " +
-                 (type == SYM_VARIABLE ? "variable" : "type") +
-                 (notes.size() == 0 ? notes : "\n" + notes));
-    }
-    break;
+  switch (check) {
+    case CHECK_DECLARED:
+      if (!isDeclared(varName, type)) {
+        parseError("Symbol '" + varName + "' not declared as a " +
+                   (type == SYM_VARIABLE ? "variable" : "type") +
+                   (notes.size() == 0 ? notes : "\n" + notes));
+      }
+      break;
 
-  case CHECK_UNDECLARED:
-    if( isDeclared(varName, type) ) {
-      parseError("Symbol '" + varName + "' previously declared as a " +
-                 (type == SYM_VARIABLE ? "variable" : "type") +
-                 (notes.size() == 0 ? notes : "\n" + notes));
-    }
-    break;
+    case CHECK_UNDECLARED:
+      if (isDeclared(varName, type)) {
+        parseError("Symbol '" + varName + "' previously declared as a " +
+                   (type == SYM_VARIABLE ? "variable" : "type") +
+                   (notes.size() == 0 ? notes : "\n" + notes));
+      }
+      break;
 
-  case CHECK_NONE:
-    break;
+    case CHECK_NONE:
+      break;
 
-  default:
-    assert(false);//Unhandled(check);
+    default:
+      assert(false);  // Unhandled(check);
   }
 }
 
 void Parser::checkFunctionLike(const std::string& name) throw(ParserException) {
-  if(d_checksEnabled && !isFunctionLike(name)) {
+  if (d_checksEnabled && !isFunctionLike(name)) {
     parseError("Expecting function-like symbol, found '" + name + "'");
   }
 }
 
-void Parser::checkArity(Kind kind, unsigned numArgs)
-  throw(ParserException) {
-  if(!d_checksEnabled) {
+void Parser::checkArity(Kind kind, unsigned numArgs) throw(ParserException) {
+  if (!d_checksEnabled) {
     return;
   }
 
   unsigned min = d_exprManager->minArity(kind);
   unsigned max = d_exprManager->maxArity(kind);
 
-  if( numArgs < min || numArgs > max ) {
+  if (numArgs < min || numArgs > max) {
     stringstream ss;
     ss << "Expecting ";
-    if( numArgs < min ) {
+    if (numArgs < min) {
       ss << "at least " << min << " ";
     } else {
       ss << "at most " << max << " ";
@@ -460,24 +445,22 @@ void Parser::checkArity(Kind kind, unsigned numArgs)
 }
 
 void Parser::checkOperator(Kind kind, unsigned numArgs) throw(ParserException) {
-  if( d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end() ) {
-    parseError( "Operator is not defined in the current logic: " + kindToString(kind) );
+  if (d_strictMode && d_logicOperators.find(kind) == d_logicOperators.end()) {
+    parseError("Operator is not defined in the current logic: " +
+               kindToString(kind));
   }
   checkArity(kind, numArgs);
 }
 
-void Parser::addOperator(Kind kind) {
-  d_logicOperators.insert(kind);
-}
+void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); }
 
-void Parser::preemptCommand(Command* cmd) {
-  d_commandQueue.push_back(cmd);
-}
+void Parser::preemptCommand(Command* cmd) { d_commandQueue.push_back(cmd); }
 
-Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException) {
+Command* Parser::nextCommand() throw(ParserException,
+                                     UnsafeInterruptException) {
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;
-  if(!d_commandQueue.empty()) {
+  if (!d_commandQueue.empty()) {
     cmd = d_commandQueue.front();
     d_commandQueue.pop_front();
     setDone(cmd == NULL);
@@ -488,19 +471,17 @@ Command* Parser::nextCommand() throw(ParserException, UnsafeInterruptException)
       cmd = d_commandQueue.front();
       d_commandQueue.pop_front();
       setDone(cmd == NULL);
-    } catch(ParserException& e) {
+    } catch (ParserException& e) {
       setDone();
       throw;
-    } catch(exception& e) {
+    } catch (exception& e) {
       setDone();
       parseError(e.what());
     }
   }
   Debug("parser") << "nextCommand() => " << cmd << std::endl;
-  if (cmd != NULL &&
-      dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
-      dynamic_cast<QuitCommand*>(cmd) == NULL)
-  {
+  if (cmd != NULL && dynamic_cast<SetOptionCommand*>(cmd) == NULL &&
+      dynamic_cast<QuitCommand*>(cmd) == NULL) {
     // don't count set-option commands as to not get stuck in an infinite
     // loop of resourcing out
     const Options& options = d_exprManager->getOptions();
@@ -514,14 +495,14 @@ Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) {
   const Options& options = d_exprManager->getOptions();
   d_resourceManager->spendResource(options.getParseStep());
   Expr result;
-  if(!done()) {
+  if (!done()) {
     try {
       result = d_input->parseExpr();
       setDone(result.isNull());
-    } catch(ParserException& e) {
+    } catch (ParserException& e) {
       setDone();
       throw;
-    } catch(exception& e) {
+    } catch (exception& e) {
       setDone();
       parseError(e.what());
     }
@@ -531,13 +512,14 @@ Expr Parser::nextExpression() throw(ParserException, UnsafeInterruptException) {
 }
 
 void Parser::attributeNotSupported(const std::string& attr) {
-  if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
+  if (d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) {
     stringstream ss;
-    ss << "warning: Attribute '" << attr << "' not supported (ignoring this and all following uses)";
+    ss << "warning: Attribute '" << attr
+       << "' not supported (ignoring this and all following uses)";
     d_input->warning(ss.str());
     d_attributesWarnedAbout.insert(attr);
   }
 }
 
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+} /* CVC4::parser namespace */
+} /* CVC4 namespace */