Format

src/parser/commands.cpp

@@ -1081,7 +1081,8 @@ void DeclareSortCommand::invoke(cvc5::Solver* solver, SymManager* sm)
   if (!sm->bindType(d_symbol, std::vector<Sort>(d_arity), sort, true))
   {
     std::stringstream ss;
-    ss << "Cannot bind " << d_symbol << " to sort, maybe it has already been defined?";
+    ss << "Cannot bind " << d_symbol
+       << " to sort, maybe it has already been defined?";
     d_commandStatus = new CommandFailure(ss.str());
     return;
   }
@@ -1133,7 +1134,8 @@ void DefineSortCommand::invoke(cvc5::Solver* solver, SymManager* sm)
   if (!sm->bindType(d_symbol, d_params, d_sort, true))
   {
     std::stringstream ss;
-    ss << "Cannot bind " << d_symbol << " to sort, maybe it has already been defined?";
+    ss << "Cannot bind " << d_symbol
+       << " to sort, maybe it has already been defined?";
     d_commandStatus = new CommandFailure(ss.str());
     return;
   }

src/parser/parser_state.h

@@ -288,9 +288,7 @@ class CVC5_EXPORT ParserState
    * @param type The type that should be associated with the name
    * @param isUser does this correspond to a user sort
    */
-  void defineType(const std::string& name,
-                  const Sort& type,
-                  bool isUser);
+  void defineType(const std::string& name, const Sort& type, bool isUser);
 
   /**
    * Create a new (parameterized) type definition.

src/parser/sym_manager.cpp

@@ -334,8 +334,7 @@ bool SymManager::bind(const std::string& name, cvc5::Term obj, bool doOverload)
   return d_implementation->getSymbolTable().bind(name, obj, doOverload);
 }
 
-bool SymManager::bindType(const std::string& name, cvc5::Sort t,
-                bool isUser)
+bool SymManager::bindType(const std::string& name, cvc5::Sort t, bool isUser)
 {
   if (isUser && !d_termSortOverload)
   {
@@ -422,7 +421,7 @@ bool SymManager::bindMutualDatatypeTypes(
 bool SymManager::bindType(const std::string& name,
                           const std::vector<cvc5::Sort>& params,
                           cvc5::Sort t,
-                bool isUser)
+                          bool isUser)
 {
   if (isUser && !d_termSortOverload)
   {
@@ -533,7 +532,7 @@ bool SymManager::getFreshDeclarations() const { return d_freshDeclarations; }
 
 void SymManager::setTermSortOverload(bool flag) { d_termSortOverload = flag; }
 bool SymManager::getTermSortOverload() const { return d_termSortOverload; }
-  
+
 void SymManager::setLastSynthName(const std::string& name)
 {
   d_implementation->setLastSynthName(name);
@@ -570,5 +569,5 @@ bool SymManager::isLogicForced() const { return d_logicIsForced; }
 bool SymManager::isLogicSet() const { return d_logicIsSet; }
 
 const std::string& SymManager::getLogic() const { return d_logic; }
-  
+
 }  // namespace cvc5::parser

src/parser/sym_manager.h

@@ -95,8 +95,7 @@ class CVC5_EXPORT SymManager
    * @param isUser does this correspond to a user sort?
    * @return false if the binding was invalid.
    */
-  bool bindType(const std::string& name, cvc5::Sort t,
-                bool isUser);
+  bool bindType(const std::string& name, cvc5::Sort t, bool isUser);
 
   /**
    * Bind a type to a name in the current scope.  If <code>name</code>

src/parser/symbol_table.cpp

@@ -429,14 +429,15 @@ bool SymbolTable::Implementation::bind(const string& name,
   return true;
 }
 
-bool SymbolTable::Implementation::bindDummySortTerm(const std::string& name, Term t)
+bool SymbolTable::Implementation::bindDummySortTerm(const std::string& name,
+                                                    Term t)
 {
   if (!bind(name, t, false))
   {
     return false;
   }
   // remember its sort
-  Assert (d_dummyType.isNull() || d_dummyType==t.getSort());
+  Assert(d_dummyType.isNull() || d_dummyType == t.getSort());
   d_dummyType = t.getSort();
   return true;
 }
@@ -638,7 +639,7 @@ bool SymbolTable::Implementation::bindWithOverloading(const string& name,
     {
       // If the type of the previous overloaded symbol was d_dummyType, this
       // indicates it is a sort. We fail unconditionally in this case.
-      if (prev_bound_obj.getSort()==d_dummyType)
+      if (prev_bound_obj.getSort() == d_dummyType)
       {
         return false;
       }
@@ -723,5 +724,5 @@ void SymbolTable::pushScope() { d_implementation->pushScope(); }
 size_t SymbolTable::getLevel() const { return d_implementation->getLevel(); }
 void SymbolTable::reset() { d_implementation->reset(); }
 void SymbolTable::resetAssertions() { d_implementation->resetAssertions(); }
-  
+
 }  // namespace cvc5::internal::parser