From 2b01fbf16475e4122bc37a77c4822716ec049e1f Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 19 Dec 2024 14:23:03 -0600 Subject: [PATCH] Sort term overload --- src/parser/commands.cpp | 4 ++-- src/parser/parser_state.cpp | 41 +++++++++------------------------- src/parser/parser_state.h | 16 +++++-------- src/parser/smt2/smt2_state.cpp | 28 +++++++++++------------ src/parser/sym_manager.cpp | 14 +++++++----- src/parser/sym_manager.h | 8 +++++-- src/parser/symbol_table.cpp | 4 ++-- src/parser/symbol_table.h | 8 +++++-- 8 files changed, 54 insertions(+), 69 deletions(-) diff --git a/src/parser/commands.cpp b/src/parser/commands.cpp index 11619e831bf..e980ebc84c8 100644 --- a/src/parser/commands.cpp +++ b/src/parser/commands.cpp @@ -1078,7 +1078,7 @@ void DeclareSortCommand::invoke(cvc5::Solver* solver, SymManager* sm) // determine if this will be a fresh declaration bool fresh = sm->getFreshDeclarations(); Sort sort = solver->declareSort(d_symbol, d_arity, fresh); - sm->bindType(d_symbol, std::vector(d_arity), sort); + sm->bindType(d_symbol, std::vector(d_arity), sort, true); // mark that it will be printed in the model, if it is an uninterpreted // sort (arity 0) if (d_arity == 0) @@ -1124,7 +1124,7 @@ cvc5::Sort DefineSortCommand::getSort() const { return d_sort; } void DefineSortCommand::invoke(cvc5::Solver* solver, SymManager* sm) { // This name is not its own distinct sort, it's an alias. - sm->bindType(d_symbol, d_params, d_sort); + sm->bindType(d_symbol, d_params, d_sort, true); d_commandStatus = CommandSuccess::instance(); } diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp index d1322cada31..6dbe5b4efc3 100644 --- a/src/parser/parser_state.cpp +++ b/src/parser/parser_state.cpp @@ -304,50 +304,31 @@ void ParserState::defineVar(const std::string& name, void ParserState::defineType(const std::string& name, const Sort& type, - bool skipExisting) + bool isUser) { - if (skipExisting && isDeclared(name, SYM_SORT)) + if (!isUser && isDeclared(name, SYM_SORT)) { Assert(d_symtab->lookupType(name) == type); return; } - d_symtab->bindType(name, type); + d_symtab->bindType(name, type, isUser); Assert(isDeclared(name, SYM_SORT)); } void ParserState::defineType(const std::string& name, const std::vector& params, - const Sort& type) + const Sort& type, + bool isUser) { - d_symtab->bindType(name, params, type); + d_symtab->bindType(name, params, type, isUser); Assert(isDeclared(name, SYM_SORT)); } -void ParserState::defineParameterizedType(const std::string& name, - const std::vector& params, - const Sort& type) -{ - if (TraceIsOn("parser")) - { - Trace("parser") << "defineParameterizedType(" << name << ", " - << params.size() << ", ["; - if (params.size() > 0) - { - copy(params.begin(), - params.end() - 1, - ostream_iterator(Trace("parser"), ", ")); - Trace("parser") << params.back(); - } - Trace("parser") << "], " << type << ")" << std::endl; - } - defineType(name, params, type); -} - Sort ParserState::mkSort(const std::string& name) { Trace("parser") << "newSort(" << name << ")" << std::endl; Sort type = d_tm.mkUninterpretedSort(name); - defineType(name, type); + defineType(name, type, true); return type; } @@ -356,14 +337,14 @@ Sort ParserState::mkSortConstructor(const std::string& name, size_t arity) Trace("parser") << "newSortConstructor(" << name << ", " << arity << ")" << std::endl; Sort type = d_tm.mkUninterpretedSortConstructorSort(arity, name); - defineType(name, vector(arity), type); + defineType(name, vector(arity), type, true); return type; } Sort ParserState::mkUnresolvedType(const std::string& name) { Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name); - defineType(name, unresolved); + defineType(name, unresolved, true); return unresolved; } @@ -371,7 +352,7 @@ Sort ParserState::mkUnresolvedTypeConstructor(const std::string& name, size_t arity) { Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name, arity); - defineType(name, vector(arity), unresolved); + defineType(name, vector(arity), unresolved, true); return unresolved; } @@ -381,7 +362,7 @@ Sort ParserState::mkUnresolvedTypeConstructor(const std::string& name, Trace("parser") << "newSortConstructor(P)(" << name << ", " << params.size() << ")" << std::endl; Sort unresolved = d_tm.mkUnresolvedDatatypeSort(name, params.size()); - defineType(name, params, unresolved); + defineType(name, params, unresolved, true); Sort t = getParametricSort(name, params); return unresolved; } diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 008824f5f02..2b778a2f3b8 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -286,13 +286,11 @@ class CVC5_EXPORT ParserState * * @param name The name of the type * @param type The type that should be associated with the name - * @param skipExisting If true, the type definition is ignored if the same - * symbol has already been defined. It is assumed that - * the definition is the exact same as the existing one. + * @param isUser does this correspond to a user sort */ void defineType(const std::string& name, const Sort& type, - bool skipExisting = false); + bool isUser); /** * Create a new (parameterized) type definition. @@ -300,16 +298,12 @@ class CVC5_EXPORT ParserState * @param name The name of the type * @param params The type parameters * @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 std::vector& params, - const Sort& type); - - /** Create a new type definition (e.g., from an SMT-LIBv2 define-sort). */ - void defineParameterizedType(const std::string& name, - const std::vector& params, - const Sort& type); - + const Sort& type, + bool isUser); /** * Creates a new sort with the given name. */ diff --git a/src/parser/smt2/smt2_state.cpp b/src/parser/smt2/smt2_state.cpp index 53ec665b11d..686383349b6 100644 --- a/src/parser/smt2/smt2_state.cpp +++ b/src/parser/smt2/smt2_state.cpp @@ -296,10 +296,10 @@ void Smt2State::addSepOperators() void Smt2State::addCoreSymbols() { - defineType("Bool", d_tm.getBooleanSort(), true); + defineType("Bool", d_tm.getBooleanSort(), false); Sort tupleSort = d_tm.mkTupleSort({}); - defineType("Relation", d_tm.mkSetSort(tupleSort), true); - defineType("Table", d_tm.mkBagSort(tupleSort), true); + defineType("Relation", d_tm.mkSetSort(tupleSort), false); + defineType("Table", d_tm.mkBagSort(tupleSort), false); defineVar("true", d_tm.mkTrue(), true); defineVar("false", d_tm.mkFalse(), true); addOperator(Kind::AND, "and"); @@ -799,7 +799,7 @@ void Smt2State::setLogic(std::string name) { if (d_logic.areIntegersUsed()) { - defineType("Int", d_tm.getIntegerSort(), true); + defineType("Int", d_tm.getIntegerSort(), false); addArithmeticOperators(); if (!strictModeEnabled() || !d_logic.isLinear()) { @@ -817,7 +817,7 @@ void Smt2State::setLogic(std::string name) if (d_logic.areRealsUsed()) { - defineType("Real", d_tm.getRealSort(), true); + defineType("Real", d_tm.getRealSort(), false); addArithmeticOperators(); addOperator(Kind::DIVISION, "/"); if (!strictModeEnabled()) @@ -872,7 +872,7 @@ void Smt2State::setLogic(std::string name) if (d_logic.isTheoryEnabled(internal::theory::THEORY_DATATYPES)) { const std::vector types; - defineType("UnitTuple", d_tm.mkTupleSort(types), true); + defineType("UnitTuple", d_tm.mkTupleSort(types), false); addDatatypesOperators(); } @@ -956,9 +956,9 @@ void Smt2State::setLogic(std::string name) } if (d_logic.isTheoryEnabled(internal::theory::THEORY_STRINGS)) { - defineType("String", d_tm.getStringSort(), true); - defineType("RegLan", d_tm.getRegExpSort(), true); - defineType("Int", d_tm.getIntegerSort(), true); + defineType("String", d_tm.getStringSort(), false); + defineType("RegLan", d_tm.getRegExpSort(), false); + defineType("Int", d_tm.getIntegerSort(), false); defineVar("re.none", d_tm.mkRegexpNone()); defineVar("re.allchar", d_tm.mkRegexpAllchar()); @@ -976,11 +976,11 @@ void Smt2State::setLogic(std::string name) if (d_logic.isTheoryEnabled(internal::theory::THEORY_FP)) { - defineType("RoundingMode", d_tm.getRoundingModeSort(), true); - defineType("Float16", d_tm.mkFloatingPointSort(5, 11), true); - defineType("Float32", d_tm.mkFloatingPointSort(8, 24), true); - defineType("Float64", d_tm.mkFloatingPointSort(11, 53), true); - defineType("Float128", d_tm.mkFloatingPointSort(15, 113), true); + defineType("RoundingMode", d_tm.getRoundingModeSort(), false); + defineType("Float16", d_tm.mkFloatingPointSort(5, 11), false); + defineType("Float32", d_tm.mkFloatingPointSort(8, 24), false); + defineType("Float64", d_tm.mkFloatingPointSort(11, 53), false); + defineType("Float128", d_tm.mkFloatingPointSort(15, 113), false); defineVar("RNE", d_tm.mkRoundingMode(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN)); diff --git a/src/parser/sym_manager.cpp b/src/parser/sym_manager.cpp index 30c5a51d933..7a902e23229 100644 --- a/src/parser/sym_manager.cpp +++ b/src/parser/sym_manager.cpp @@ -332,9 +332,10 @@ bool SymManager::bind(const std::string& name, cvc5::Term obj, bool doOverload) return d_implementation->getSymbolTable().bind(name, obj, doOverload); } -void SymManager::bindType(const std::string& name, cvc5::Sort t) +void SymManager::bindType(const std::string& name, cvc5::Sort t, + bool isUser) { - return d_implementation->getSymbolTable().bindType(name, t); + return d_implementation->getSymbolTable().bindType(name, t, isUser); } bool SymManager::bindMutualDatatypeTypes( @@ -349,11 +350,11 @@ bool SymManager::bindMutualDatatypeTypes( if (dt.isParametric()) { std::vector paramTypes = dt.getParameters(); - bindType(name, paramTypes, t); + bindType(name, paramTypes, t, true); } else { - bindType(name, t); + bindType(name, t, true); } for (size_t j = 0, ncons = dt.getNumConstructors(); j < ncons; j++) { @@ -403,9 +404,10 @@ bool SymManager::bindMutualDatatypeTypes( void SymManager::bindType(const std::string& name, const std::vector& params, - cvc5::Sort t) + cvc5::Sort t, + bool isUser) { - return d_implementation->getSymbolTable().bindType(name, params, t); + return d_implementation->getSymbolTable().bindType(name, params, t, isUser); } NamingResult SymManager::setExpressionName(cvc5::Term t, diff --git a/src/parser/sym_manager.h b/src/parser/sym_manager.h index e750aa01421..fa66c670d84 100644 --- a/src/parser/sym_manager.h +++ b/src/parser/sym_manager.h @@ -93,8 +93,10 @@ class CVC5_EXPORT SymManager * * @param name an identifier * @param t the type to bind to name + * @param isUser does this correspond to a user sort? */ - void bindType(const std::string& name, cvc5::Sort t); + void bindType(const std::string& name, cvc5::Sort t, + bool isUser); /** * Bind a type to a name in the current scope. If name @@ -106,10 +108,12 @@ class CVC5_EXPORT SymManager * @param name an identifier * @param params the parameters to the type * @param t the type to bind to name + * @param isUser does this correspond to a user sort? */ void bindType(const std::string& name, const std::vector& params, - cvc5::Sort t); + cvc5::Sort t, + bool isUser); /** * Binds sorts of a list of mutually-recursive datatype declarations. * diff --git a/src/parser/symbol_table.cpp b/src/parser/symbol_table.cpp index faba4b5f45d..2896522e958 100644 --- a/src/parser/symbol_table.cpp +++ b/src/parser/symbol_table.cpp @@ -654,14 +654,14 @@ bool SymbolTable::bind(const string& name, Term obj, bool doOverload) return d_implementation->bind(name, obj, doOverload); } -void SymbolTable::bindType(const string& name, Sort t) +void SymbolTable::bindType(const string& name, Sort t, bool isUser) { d_implementation->bindType(name, t); } void SymbolTable::bindType(const string& name, const vector& params, - Sort t) + Sort t, bool isUser) { d_implementation->bindType(name, params, t); } diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 667c0deeaf3..b5cd7d95804 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -82,8 +82,10 @@ class CVC5_EXPORT SymbolTable * * @param name an identifier * @param t the type to bind to name + * @param isUser does this correspond to a user sort */ - void bindType(const std::string& name, cvc5::Sort t); + void bindType(const std::string& name, cvc5::Sort t, + bool isUser); /** * Bind a type to a name in the current scope. If name @@ -95,10 +97,12 @@ class CVC5_EXPORT SymbolTable * @param name an identifier * @param params the parameters to the type * @param t the type to bind to name + * @param isUser does this correspond to a user sort */ void bindType(const std::string& name, const std::vector& params, - cvc5::Sort t); + cvc5::Sort t, + bool isUser); /** * Check whether a name is bound to an expression with bind().