From 827f84b4cbac8e7e0cb90220642bdce0d41b58b2 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 19 Dec 2024 15:01:35 -0600 Subject: [PATCH] Format --- src/parser/commands.cpp | 6 ++++-- src/parser/parser_state.h | 4 +--- src/parser/sym_manager.cpp | 9 ++++----- src/parser/sym_manager.h | 3 +-- src/parser/symbol_table.cpp | 9 +++++---- 5 files changed, 15 insertions(+), 16 deletions(-) diff --git a/src/parser/commands.cpp b/src/parser/commands.cpp index 816ab81de2a..e3aab5bafed 100644 --- a/src/parser/commands.cpp +++ b/src/parser/commands.cpp @@ -1081,7 +1081,8 @@ void DeclareSortCommand::invoke(cvc5::Solver* solver, SymManager* sm) if (!sm->bindType(d_symbol, std::vector(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; } diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 2b778a2f3b8..2d1c0126c83 100644 --- a/src/parser/parser_state.h +++ b/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. diff --git a/src/parser/sym_manager.cpp b/src/parser/sym_manager.cpp index 86b2881b028..a2211a85224 100644 --- a/src/parser/sym_manager.cpp +++ b/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& 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 diff --git a/src/parser/sym_manager.h b/src/parser/sym_manager.h index 58cc66e1937..c945ac01ec3 100644 --- a/src/parser/sym_manager.h +++ b/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 name diff --git a/src/parser/symbol_table.cpp b/src/parser/symbol_table.cpp index 7fc940569ee..3a71d7cf341 100644 --- a/src/parser/symbol_table.cpp +++ b/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