diff options
Diffstat (limited to 'src')
44 files changed, 500 insertions, 805 deletions
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index feacc8837..31a22b44a 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -898,7 +898,7 @@ const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors() std::ostream& operator<<(std::ostream& os, const DType& dt) { // can only output datatypes in the cvc5 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC); + language::SetLanguage::Scope ls(os, Language::LANG_CVC); dt.toStream(os); return os; } diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index b71f49e87..3603c776a 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -685,7 +685,7 @@ void DTypeConstructor::toStream(std::ostream& out) const std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor) { // can only output datatypes in the cvc5 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC); + language::SetLanguage::Scope ls(os, Language::LANG_CVC); ctor.toStream(os); return os; } diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp index c8497433b..1898a4186 100644 --- a/src/expr/dtype_selector.cpp +++ b/src/expr/dtype_selector.cpp @@ -84,7 +84,7 @@ void DTypeSelector::toStream(std::ostream& out) const std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg) { // can only output datatypes in the cvc5 native language - language::SetLanguage::Scope ls(os, language::output::LANG_CVC); + language::SetLanguage::Scope ls(os, Language::LANG_CVC); arg.toStream(os); return os; } diff --git a/src/expr/node.h b/src/expr/node.h index a406b3d13..1ce915472 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -826,11 +826,10 @@ public: * print it fully * @param language the language in which to output */ - inline void toStream( - std::ostream& out, - int toDepth = -1, - size_t dagThreshold = 1, - OutputLanguage language = language::output::LANG_AUTO) const + inline void toStream(std::ostream& out, + int toDepth = -1, + size_t dagThreshold = 1, + Language language = Language::LANG_AUTO) const { assertTNodeNotExpired(); d_nv->toStream(out, toDepth, dagThreshold, language); @@ -1483,17 +1482,13 @@ Node NodeTemplate<ref_count>::substitute( * to meet. A cleaner solution is welcomed. */ static void __attribute__((used)) debugPrintNode(const NodeTemplate<true>& n) { - Warning() << Node::setdepth(-1) - << Node::dag(true) - << Node::setlanguage(language::output::LANG_AST) - << n << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(true) + << Node::setlanguage(Language::LANG_AST) << n << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintNodeNoDag(const NodeTemplate<true>& n) { - Warning() << Node::setdepth(-1) - << Node::dag(false) - << Node::setlanguage(language::output::LANG_AST) - << n << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(false) + << Node::setlanguage(Language::LANG_AST) << n << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) { @@ -1502,17 +1497,13 @@ static void __attribute__((used)) debugPrintRawNode(const NodeTemplate<true>& n) } static void __attribute__((used)) debugPrintTNode(const NodeTemplate<false>& n) { - Warning() << Node::setdepth(-1) - << Node::dag(true) - << Node::setlanguage(language::output::LANG_AST) - << n << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(true) + << Node::setlanguage(Language::LANG_AST) << n << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintTNodeNoDag(const NodeTemplate<false>& n) { - Warning() << Node::setdepth(-1) - << Node::dag(false) - << Node::setlanguage(language::output::LANG_AST) - << n << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(false) + << Node::setlanguage(Language::LANG_AST) << n << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>& n) { diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 10e32ac71..46ba3d191 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -37,8 +37,8 @@ namespace expr { string NodeValue::toString() const { stringstream ss; - OutputLanguage outlang = (this == &null()) ? language::output::LANG_AUTO - : options::outputLanguage(); + Language outlang = + (this == &null()) ? Language::LANG_AUTO : options::outputLanguage(); toStream(ss, -1, false, outlang); return ss.str(); } @@ -46,7 +46,7 @@ string NodeValue::toString() const { void NodeValue::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { // Ensure that this node value is live for the length of this call. // It really breaks things badly if we don't have a nonzero ref diff --git a/src/expr/node_value.h b/src/expr/node_value.h index c86651648..ba30dc8fb 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -233,7 +233,7 @@ class NodeValue void toStream(std::ostream& out, int toDepth = -1, size_t dag = 1, - OutputLanguage = language::output::LANG_AUTO) const; + Language = Language::LANG_AUTO) const; void printAst(std::ostream& out, int indent = 0) const; @@ -525,17 +525,13 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) { * flushes the stream. */ static void __attribute__((used)) debugPrintNodeValue(const expr::NodeValue* nv) { - Warning() << Node::setdepth(-1) - << Node::dag(true) - << Node::setlanguage(language::output::LANG_AST) - << *nv << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(true) + << Node::setlanguage(Language::LANG_AST) << *nv << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintNodeValueNoDag(const expr::NodeValue* nv) { - Warning() << Node::setdepth(-1) - << Node::dag(false) - << Node::setlanguage(language::output::LANG_AST) - << *nv << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(false) + << Node::setlanguage(Language::LANG_AST) << *nv << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue* nv) { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 52a21040e..fa6a56c99 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -660,7 +660,8 @@ bool TypeNode::isSygusDatatype() const std::string TypeNode::toString() const { std::stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + Language outlang = + (this == &s_null) ? Language::LANG_AUTO : options::outputLanguage(); d_nv->toStream(ss, -1, 0, outlang); return ss.str(); } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 21e7b4d28..2f854f581 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -374,7 +374,9 @@ private: * @param out the stream to serialize this node to * @param language the language in which to output */ - inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AUTO) const { + inline void toStream(std::ostream& out, + Language language = Language::LANG_AUTO) const + { d_nv->toStream(out, -1, 0, language); } @@ -1029,17 +1031,13 @@ inline unsigned TypeNode::getFloatingPointSignificandSize() const { * to meet. A cleaner solution is welcomed. */ static void __attribute__((used)) debugPrintTypeNode(const TypeNode& n) { - Warning() << Node::setdepth(-1) - << Node::dag(true) - << Node::setlanguage(language::output::LANG_AST) - << n << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(true) + << Node::setlanguage(Language::LANG_AST) << n << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintTypeNodeNoDag(const TypeNode& n) { - Warning() << Node::setdepth(-1) - << Node::dag(false) - << Node::setlanguage(language::output::LANG_AST) - << n << std::endl; + Warning() << Node::setdepth(-1) << Node::dag(false) + << Node::setlanguage(Language::LANG_AST) << n << std::endl; Warning().flush(); } static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) { diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 9ceed82f7..de6f614e1 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -158,32 +158,32 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver) } const char* filename = filenameStr.c_str(); - if (opts->base.inputLanguage == language::input::LANG_AUTO) + if (opts->base.inputLanguage == Language::LANG_AUTO) { if( inputFromStdin ) { // We can't do any fancy detection on stdin - opts->base.inputLanguage = language::input::LANG_CVC; + opts->base.inputLanguage = Language::LANG_CVC; } else { size_t len = filenameStr.size(); if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - opts->base.inputLanguage = language::input::LANG_SMTLIB_V2_6; + opts->base.inputLanguage = Language::LANG_SMTLIB_V2_6; } else if((len >= 2 && !strcmp(".p", filename + len - 2)) || (len >= 5 && !strcmp(".tptp", filename + len - 5))) { - opts->base.inputLanguage = language::input::LANG_TPTP; + opts->base.inputLanguage = Language::LANG_TPTP; } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { - opts->base.inputLanguage = language::input::LANG_CVC; + opts->base.inputLanguage = Language::LANG_CVC; } else if((len >= 3 && !strcmp(".sy", filename + len - 3)) || (len >= 3 && !strcmp(".sl", filename + len - 3))) { // version 2 sygus is the default - opts->base.inputLanguage = language::input::LANG_SYGUS_V2; + opts->base.inputLanguage = Language::LANG_SYGUS_V2; } } } - if (opts->base.outputLanguage == language::output::LANG_AUTO) + if (opts->base.outputLanguage == Language::LANG_AUTO) { - opts->base.outputLanguage = language::toOutputLanguage(opts->base.inputLanguage); + opts->base.outputLanguage = opts->base.inputLanguage; } pExecutor->storeOptionsAsOriginal(); diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 7a1ee89ab..14a507aee 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -116,23 +116,22 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */ ::using_history(); - OutputLanguage lang = - toOutputLanguage(d_options.base.inputLanguage); + Language lang = d_options.base.inputLanguage; switch(lang) { - case output::LANG_CVC: + case Language::LANG_CVC: d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; commandsBegin = cvc_commands; commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); break; - case output::LANG_TPTP: + case Language::LANG_TPTP: d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp"; commandsBegin = tptp_commands; commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); break; default: - if (language::isOutputLang_smt2(lang)) + if (language::isLangSmt2(lang)) { d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2"; commandsBegin = smt2_commands; @@ -365,7 +364,7 @@ restart: } catch (ParserException& pe) { - if (language::isOutputLang_smt2(d_options.base.outputLanguage)) + if (language::isLangSmt2(d_options.base.outputLanguage)) { d_out << "(error \"" << pe << "\")" << endl; } diff --git a/src/main/main.cpp b/src/main/main.cpp index 6f109255f..5fedc53da 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -79,7 +79,7 @@ int main(int argc, char* argv[]) #ifdef CVC5_COMPETITION_MODE *solver->getOptions().base.out << "unknown" << endl; #endif - if (language::isOutputLang_smt2(solver->getOptions().base.outputLanguage)) + if (language::isLangSmt2(solver->getOptions().base.outputLanguage)) { *solver->getOptions().base.out << "(error \"" << e << "\")" << endl; } diff --git a/src/options/base_options.toml b/src/options/base_options.toml index 9a2d2f74e..a049348a6 100644 --- a/src/options/base_options.toml +++ b/src/options/base_options.toml @@ -34,9 +34,10 @@ public = true category = "common" short = "L" long = "lang=LANG" - type = "InputLanguage" - default = "language::input::LANG_AUTO" - handler = "stringToInputLanguage" + type = "Language" + default = "Language::LANG_AUTO" + handler = "stringToLanguage" + predicates = ["languageIsNotAST"] includes = ["options/language.h"] help = "force input language (default is \"auto\"; see --lang help)" @@ -45,9 +46,9 @@ public = true alias = ["output-language"] category = "common" long = "output-lang=LANG" - type = "OutputLanguage" - default = "language::output::LANG_AUTO" - handler = "stringToOutputLanguage" + type = "Language" + default = "Language::LANG_AUTO" + handler = "stringToLanguage" includes = ["options/language.h"] help = "force output language (default is \"auto\"; see --output-lang help)" diff --git a/src/options/language.cpp b/src/options/language.cpp index bf17e91f9..041debd67 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -15,167 +15,60 @@ #include "options/language.h" -#include <sstream> - -#include "base/exception.h" #include "options/option_exception.h" namespace cvc5 { -namespace language { - -/** define the end points of smt2 languages */ -namespace input { -Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6; -Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6; -} -namespace output { -Language LANG_SMTLIB_V2_START = LANG_SMTLIB_V2_6; -Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6; -} - -bool isInputLang_smt2(InputLanguage lang) -{ - return lang >= input::LANG_SMTLIB_V2_START - && lang <= input::LANG_SMTLIB_V2_END; -} - -bool isOutputLang_smt2(OutputLanguage lang) -{ - return lang >= output::LANG_SMTLIB_V2_START - && lang <= output::LANG_SMTLIB_V2_END; -} - -bool isInputLang_smt2_6(InputLanguage lang, bool exact) -{ - return exact ? lang == input::LANG_SMTLIB_V2_6 - : (lang >= input::LANG_SMTLIB_V2_6 - && lang <= input::LANG_SMTLIB_V2_END); -} - -bool isOutputLang_smt2_6(OutputLanguage lang, bool exact) -{ - return exact ? lang == output::LANG_SMTLIB_V2_6 - : (lang >= output::LANG_SMTLIB_V2_6 - && lang <= output::LANG_SMTLIB_V2_END); -} - -bool isInputLangSygus(InputLanguage lang) -{ - return lang == input::LANG_SYGUS_V2; -} -bool isOutputLangSygus(OutputLanguage lang) +std::ostream& operator<<(std::ostream& out, Language lang) { - return lang == output::LANG_SYGUS_V2; -} - -InputLanguage toInputLanguage(OutputLanguage language) { - switch(language) { - case output::LANG_SMTLIB_V2_6: - case output::LANG_TPTP: - case output::LANG_CVC: - case output::LANG_SYGUS_V2: - // these entries directly correspond (by design) - return InputLanguage(int(language)); - - default: { - std::stringstream ss; - ss << "Cannot map output language `" << language - << "' to an input language."; - throw cvc5::Exception(ss.str()); + switch (lang) + { + case Language::LANG_AUTO: out << "LANG_AUTO"; break; + case Language::LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; + case Language::LANG_TPTP: out << "LANG_TPTP"; break; + case Language::LANG_CVC: out << "LANG_CVC"; break; + case Language::LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; + default: out << "undefined_language"; } - }/* switch(language) */ -}/* toInputLanguage() */ - -OutputLanguage toOutputLanguage(InputLanguage language) { - switch(language) { - case input::LANG_SMTLIB_V2_6: - case input::LANG_TPTP: - case input::LANG_CVC: - case input::LANG_SYGUS_V2: - // these entries directly correspond (by design) - return OutputLanguage(int(language)); + return out; +} - default: - // Revert to the default (AST) language. - // - // We used to throw an exception here, but that's not quite right. - // We often call this while constructing exceptions, for one, and - // it's better to output SOMETHING related to the original - // exception rather than mask it with another exception. Also, - // the input language isn't always defined---e.g. during the - // initial phase of the main cvc5 driver while it determines which - // language is appropriate, and during unit tests. Also, when - // users are writing their own code against the library. - return output::LANG_AST; - }/* switch(language) */ -}/* toOutputLanguage() */ +namespace language { -OutputLanguage toOutputLanguage(std::string language) +Language toLanguage(const std::string& language) { if (language == "cvc" || language == "pl" || language == "presentation" || language == "native" || language == "LANG_CVC") { - return output::LANG_CVC; + return Language::LANG_CVC; } else if (language == "smtlib" || language == "smt" || language == "smtlib2" || language == "smt2" || language == "smtlib2.6" || language == "smt2.6" || language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") { - return output::LANG_SMTLIB_V2_6; + return Language::LANG_SMTLIB_V2_6; } else if (language == "tptp" || language == "LANG_TPTP") { - return output::LANG_TPTP; + return Language::LANG_TPTP; } else if (language == "sygus" || language == "LANG_SYGUS" || language == "sygus2" || language == "LANG_SYGUS_V2") { - return output::LANG_SYGUS_V2; + return Language::LANG_SYGUS_V2; } else if (language == "ast" || language == "LANG_AST") { - return output::LANG_AST; + return Language::LANG_AST; } else if (language == "auto" || language == "LANG_AUTO") { - return output::LANG_AUTO; + return Language::LANG_AUTO; } - throw OptionException( - std::string("unknown output language `" + language + "'")); + throw OptionException(std::string("unknown language `" + language + "'")); } -InputLanguage toInputLanguage(std::string language) { - if (language == "cvc" || language == "pl" || language == "presentation" - || language == "native" || language == "LANG_CVC") - { - return input::LANG_CVC; - } - else if (language == "smtlib" || language == "smt" || language == "smtlib2" - || language == "smt2" || language == "smtlib2.6" - || language == "smt2.6" || language == "LANG_SMTLIB_V2_6" - || language == "LANG_SMTLIB_V2") - { - return input::LANG_SMTLIB_V2_6; - } - else if (language == "tptp" || language == "LANG_TPTP") - { - return input::LANG_TPTP; - } - else if (language == "sygus" || language == "sygus2" - || language == "LANG_SYGUS" || language == "LANG_SYGUS_V2") - { - return input::LANG_SYGUS_V2; - } - else if (language == "auto" || language == "LANG_AUTO") - { - return input::LANG_AUTO; - } - - throw OptionException(std::string("unknown input language `" + language + "'")); -}/* toInputLanguage() */ - } // namespace language } // namespace cvc5 diff --git a/src/options/language.h b/src/options/language.h index 04182cdd9..6031a6487 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Definition of input and output languages. + * Definition of languages. */ #include "cvc5_public.h" @@ -24,147 +24,47 @@ #include "cvc5_export.h" namespace cvc5 { -namespace language { - -namespace input { -enum CVC5_EXPORT Language +enum class CVC5_EXPORT Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 /** Auto-detect the language */ LANG_AUTO = -1, - // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] - // AND SHOULD CORRESPOND IN PLACEMENT WITH OUTPUTLANGUAGE - // - // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR - // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, - // INCLUDE IT HERE - - /** The SMTLIB v2.6 input language, with support for the strings standard */ + /** The SMTLIB v2.6 language, with support for the strings standard */ LANG_SMTLIB_V2_6 = 0, - /** Backward-compatibility for enumeration naming */ - LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6, - /** The TPTP input language */ + /** The TPTP language */ LANG_TPTP, - /** The cvc5 input language */ + /** The cvc5 language */ LANG_CVC, - /** The SyGuS input language version 2.0 */ + /** The SyGuS language version 2.0 */ LANG_SYGUS_V2, - // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 - // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES - - /** LANG_MAX is > any valid InputLanguage id */ - LANG_MAX -}; /* enum Language */ - -inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT; -inline std::ostream& operator<<(std::ostream& out, Language lang) { - switch(lang) { - case LANG_AUTO: - out << "LANG_AUTO"; - break; - case LANG_SMTLIB_V2_6: - out << "LANG_SMTLIB_V2_6"; - break; - case LANG_TPTP: - out << "LANG_TPTP"; - break; - case LANG_CVC: out << "LANG_CVC"; break; - case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; - default: - out << "undefined_input_language"; - } - return out; -} - -} // namespace input - -namespace output { - -enum CVC5_EXPORT Language -{ - // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 - - /** Match the output language to the input language */ - LANG_AUTO = -1, + /** The AST (output) language */ + LANG_AST, - // COMMON INPUT AND OUTPUT LANGUAGES HAVE ENUM VALUES IN [0,9] - // AND SHOULD CORRESPOND IN PLACEMENT WITH INPUTLANGUAGE - // - // EVEN IF A LANGUAGE ISN'T CURRENTLY SUPPORTED AS AN INPUT OR - // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE, - // INCLUDE IT HERE - - /** The SMTLIB v2.6 output language, with support for the strings standard */ - LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6, - /** Backward-compatibility for enumeration naming */ - LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2, - /** The TPTP output language */ - LANG_TPTP = input::LANG_TPTP, - /** The cvc5 output language */ - LANG_CVC = input::LANG_CVC, - /** The sygus output language version 2.0 */ - LANG_SYGUS_V2 = input::LANG_SYGUS_V2, - - // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 - // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES - - /** The AST output language */ - LANG_AST = 10, - - /** LANG_MAX is > any valid OutputLanguage id */ + /** LANG_MAX is > any valid Language id */ LANG_MAX -}; /* enum Language */ - -inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT; -inline std::ostream& operator<<(std::ostream& out, Language lang) { - switch(lang) { - case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; - case LANG_TPTP: - out << "LANG_TPTP"; - break; - case LANG_CVC: out << "LANG_CVC"; break; - case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; - case LANG_AST: - out << "LANG_AST"; - break; - default: - out << "undefined_output_language"; - } - return out; -} - -} // namespace output - -} // namespace language +}; -typedef language::input::Language InputLanguage; -typedef language::output::Language OutputLanguage; +std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT; namespace language { /** Is the language a variant of the smtlib version 2 language? */ -bool isInputLang_smt2(InputLanguage lang) CVC5_EXPORT; -bool isOutputLang_smt2(OutputLanguage lang) CVC5_EXPORT; - -/** - * Is the language smtlib 2.6 or above? If exact=true, then this method returns - * false if the input language is not exactly SMT-LIB 2.6. - */ -bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC5_EXPORT; -bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC5_EXPORT; +inline bool isLangSmt2(Language lang) +{ + return lang == Language::LANG_SMTLIB_V2_6; +} /** Is the language a variant of the SyGuS input language? */ -bool isInputLangSygus(InputLanguage lang) CVC5_EXPORT; -bool isOutputLangSygus(OutputLanguage lang) CVC5_EXPORT; +inline bool isLangSygus(Language lang) +{ + return lang == Language::LANG_SYGUS_V2; +} -InputLanguage toInputLanguage(OutputLanguage language) CVC5_EXPORT; -OutputLanguage toOutputLanguage(InputLanguage language) CVC5_EXPORT; -InputLanguage toInputLanguage(std::string language) CVC5_EXPORT; -OutputLanguage toOutputLanguage(std::string language) CVC5_EXPORT; +Language toLanguage(const std::string& language) CVC5_EXPORT; } // namespace language } // namespace cvc5 diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 42a63b47c..149aa767b 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -494,41 +494,33 @@ void OptionsHandler::enableOutputTag(const std::string& option, static_cast<size_t>(stringToOutputTag(optarg))); } -OutputLanguage OptionsHandler::stringToOutputLanguage(const std::string& option, - const std::string& flag, - const std::string& optarg) +Language OptionsHandler::stringToLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg) { if(optarg == "help") { d_options->base.languageHelp = true; - return language::output::LANG_AUTO; + return Language::LANG_AUTO; } try { - return language::toOutputLanguage(optarg); + return language::toLanguage(optarg); } catch(OptionException& oe) { - throw OptionException("Error in " + option + ": " + oe.getMessage() + - "\nTry --output-language help"); + throw OptionException("Error in " + option + ": " + oe.getMessage() + + "\nTry --lang help"); } Unreachable(); } -InputLanguage OptionsHandler::stringToInputLanguage(const std::string& option, - const std::string& flag, - const std::string& optarg) +void OptionsHandler::languageIsNotAST(const std::string& option, + const std::string& flag, + Language lang) { - if(optarg == "help") { - d_options->base.languageHelp = true; - return language::input::LANG_AUTO; - } - - try { - return language::toInputLanguage(optarg); - } catch(OptionException& oe) { - throw OptionException("Error in " + option + ": " + oe.getMessage() + "\nTry --lang help"); + if (lang == Language::LANG_AST) + { + throw OptionException("Language LANG_AST is not allowed for " + flag); } - - Unreachable(); } void OptionsHandler::setDumpStream(const std::string& option, diff --git a/src/options/options_handler.h b/src/options/options_handler.h index ba3951c00..3b8eb724f 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -149,12 +149,14 @@ public: int value); void increaseVerbosity(const std::string& option, const std::string& flag); void decreaseVerbosity(const std::string& option, const std::string& flag); - OutputLanguage stringToOutputLanguage(const std::string& option, - const std::string& flag, - const std::string& optarg); - InputLanguage stringToInputLanguage(const std::string& option, - const std::string& flag, - const std::string& optarg); + /** Convert optarg to Language enum */ + Language stringToLanguage(const std::string& option, + const std::string& flag, + const std::string& optarg); + /** Check that lang is not LANG_AST (which is not allowed as input language). */ + void languageIsNotAST(const std::string& option, + const std::string& flag, + Language lang); void enableTraceTag(const std::string& option, const std::string& flag, const std::string& optarg); diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp index 0c351fb71..63351ea04 100644 --- a/src/options/set_language.cpp +++ b/src/options/set_language.cpp @@ -26,9 +26,8 @@ namespace language { const int SetLanguage::s_iosIndex = std::ios_base::xalloc(); -SetLanguage::Scope::Scope(std::ostream& out, OutputLanguage language) - : d_out(out) - , d_oldLanguage(SetLanguage::getLanguage(out)) +SetLanguage::Scope::Scope(std::ostream& out, Language language) + : d_out(out), d_oldLanguage(SetLanguage::getLanguage(out)) { SetLanguage::setLanguage(out, language); } @@ -37,37 +36,37 @@ SetLanguage::Scope::~Scope(){ SetLanguage::setLanguage(d_out, d_oldLanguage); } - -SetLanguage::SetLanguage(OutputLanguage l) - : d_language(l) -{} +SetLanguage::SetLanguage(Language l) : d_language(l) {} void SetLanguage::applyLanguage(std::ostream& out) { // (offset by one to detect whether default has been set yet) out.iword(s_iosIndex) = int(d_language) + 1; } -OutputLanguage SetLanguage::getLanguage(std::ostream& out) { +Language SetLanguage::getLanguage(std::ostream& out) +{ long& l = out.iword(s_iosIndex); if(l == 0) { // set the default language on this ostream // (offset by one to detect whether default has been set yet) if(not Options::isCurrentNull()) { - l = options::outputLanguage() + 1; + l = static_cast<long>(options::outputLanguage()) + 1; } - if(l <= 0 || l > language::output::LANG_MAX) { + if (l <= 0 || l > static_cast<long>(Language::LANG_MAX)) + { // if called from outside the library, we may not have options // available to us at this point (or perhaps the output language // is not set in Options). Default to something reasonable, but // don't set "l" since that would make it "sticky" for this // stream. - return OutputLanguage(s_defaultOutputLanguage); + return s_defaultOutputLanguage; } } - return OutputLanguage(l - 1); + return Language(l - 1); } -void SetLanguage::setLanguage(std::ostream& out, OutputLanguage l) { +void SetLanguage::setLanguage(std::ostream& out, Language l) +{ // (offset by one to detect whether default has been set yet) out.iword(s_iosIndex) = int(l) + 1; } diff --git a/src/options/set_language.h b/src/options/set_language.h index 45add38ac..ae59a18f5 100644 --- a/src/options/set_language.h +++ b/src/options/set_language.h @@ -40,25 +40,25 @@ class CVC5_EXPORT SetLanguage */ class Scope { public: - Scope(std::ostream& out, OutputLanguage language); + Scope(std::ostream& out, Language language); ~Scope(); private: std::ostream& d_out; - OutputLanguage d_oldLanguage; + Language d_oldLanguage; };/* class SetLanguage::Scope */ /** * Construct a ExprSetLanguage with the given setting. */ - SetLanguage(OutputLanguage l); + SetLanguage(Language l); void applyLanguage(std::ostream& out); - static OutputLanguage getLanguage(std::ostream& out); + static Language getLanguage(std::ostream& out); - static void setLanguage(std::ostream& out, OutputLanguage l); + static void setLanguage(std::ostream& out, Language l); -private: + private: /** * The allocated index in ios_base for our depth setting. @@ -70,12 +70,12 @@ private: * setlanguage() applied to them and where the current Options * information isn't available. */ - static const int s_defaultOutputLanguage = language::output::LANG_AUTO; + static const Language s_defaultOutputLanguage = Language::LANG_AUTO; /** * When this manipulator is used, the setting is stored here. */ - OutputLanguage d_language; + Language d_language; }; /* class SetLanguage */ /** diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 73d1b89b5..6d5cbb5cc 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -185,35 +185,32 @@ AntlrInputStream::newStringInputStream(const std::string& input, return new AntlrInputStream(name, inputStream, false, input_duplicate, NULL); } -AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) { - using namespace language::input; - +AntlrInput* AntlrInput::newInput(Language lang, AntlrInputStream& inputStream) +{ AntlrInput* input; switch(lang) { - case LANG_CVC: + case Language::LANG_CVC: { input = new CvcInput(inputStream); break; } - case LANG_SYGUS_V2: input = new SygusInput(inputStream); break; + case Language::LANG_SYGUS_V2: input = new SygusInput(inputStream); break; - case LANG_TPTP: - input = new TptpInput(inputStream); - break; + case Language::LANG_TPTP: input = new TptpInput(inputStream); break; - default: - if (language::isInputLang_smt2(lang)) - { - input = new Smt2Input(inputStream); - } - else - { - std::stringstream ss; - ss << "unable to detect input file format, try --lang "; - throw InputStreamException(ss.str()); - } + default: + if (language::isLangSmt2(lang)) + { + input = new Smt2Input(inputStream); + } + else + { + std::stringstream ss; + ss << "unable to detect input file format, try --lang "; + throw InputStreamException(ss.str()); + } } return input; diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index c74962188..52650f561 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -155,7 +155,7 @@ public: * @param inputStream the input stream * * */ - static AntlrInput* newInput(InputLanguage lang, AntlrInputStream& inputStream); + static AntlrInput* newInput(Language lang, AntlrInputStream& inputStream); /** Retrieve the text associated with a token. */ static std::string tokenText(pANTLR3_COMMON_TOKEN token); diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index f0cb0fc78..a01753b56 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -491,7 +491,7 @@ api::Term createPrecedenceTree(Parser* parser, api::Solver* s, api::Term e = createPrecedenceTree( parser, s, expressions, operators, 0, expressions.size() - 1); if(Debug.isOn("prec") && operators.size() > 1) { - language::SetLanguage::Scope ls(Debug("prec"), language::output::LANG_AST); + language::SetLanguage::Scope ls(Debug("prec"), Language::LANG_AST); Debug("prec") << "=> " << e << std::endl; } return e; @@ -1103,7 +1103,7 @@ declareVariables[std::unique_ptr<cvc5::Command>* cmd, cvc5::api::Sort& t, << "with type " << oldType << std::endl; if(oldType != t) { std::stringstream ss; - ss << language::SetLanguage(language::output::LANG_CVC) + ss << language::SetLanguage(Language::LANG_CVC) << "incompatible type for `" << *i << "':" << std::endl << " old type: " << oldType << std::endl << " new type: " << t << std::endl; @@ -1514,7 +1514,7 @@ letDecl } : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e] { - Debug("parser") << language::SetLanguage(language::output::LANG_CVC) + Debug("parser") << language::SetLanguage(Language::LANG_CVC) << e.getSort() << std::endl; PARSER_STATE->defineVar(name, e); Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: " diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 4c88978de..9d4c65eae 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -51,7 +51,7 @@ InputStream *Input::getInputStream() { return d_inputStream; } -Input* Input::newFileInput(InputLanguage lang, +Input* Input::newFileInput(Language lang, const std::string& filename, bool useMmap) { @@ -60,7 +60,7 @@ Input* Input::newFileInput(InputLanguage lang, return AntlrInput::newInput(lang, *inputStream); } -Input* Input::newStreamInput(InputLanguage lang, +Input* Input::newStreamInput(Language lang, std::istream& input, const std::string& name) { @@ -69,7 +69,7 @@ Input* Input::newStreamInput(InputLanguage lang, return AntlrInput::newInput(lang, *inputStream); } -Input* Input::newStringInput(InputLanguage lang, +Input* Input::newStringInput(Language lang, const std::string& str, const std::string& name) { diff --git a/src/parser/input.h b/src/parser/input.h index 1821bc034..94bbe1d8a 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -100,7 +100,7 @@ class CVC5_EXPORT Input * @param filename the input filename * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ - static Input* newFileInput(InputLanguage lang, + static Input* newFileInput(Language lang, const std::string& filename, bool useMmap = false); @@ -113,7 +113,7 @@ class CVC5_EXPORT Input * (false, the default, means that the entire Input might be read * before being lexed and parsed) */ - static Input* newStreamInput(InputLanguage lang, + static Input* newStreamInput(Language lang, std::istream& input, const std::string& name); @@ -123,7 +123,7 @@ class CVC5_EXPORT Input * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringInput(InputLanguage lang, + static Input* newStringInput(Language lang, const std::string& input, const std::string& name); diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index eab982013..bd0f56b2d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -899,8 +899,7 @@ std::wstring Parser::processAdHocStringEsc(const std::string& s) api::Term Parser::mkStringConstant(const std::string& s) { - if (language::isInputLang_smt2_6( - d_solver->getOptions().base.inputLanguage)) + if (language::isLangSmt2(d_solver->getOptions().base.inputLanguage)) { return d_solver->mkString(s, true); } diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 816803ccc..1ac03fb83 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -50,7 +50,7 @@ ParserBuilder::ParserBuilder(api::Solver* solver, void ParserBuilder::init(api::Solver* solver, SymbolManager* sm) { - d_lang = language::input::LANG_AUTO; + d_lang = Language::LANG_AUTO; d_solver = solver; d_symman = sm; d_checksEnabled = true; @@ -66,14 +66,14 @@ Parser* ParserBuilder::build() Parser* parser = NULL; switch (d_lang) { - case language::input::LANG_SYGUS_V2: + case Language::LANG_SYGUS_V2: parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); break; - case language::input::LANG_TPTP: + case Language::LANG_TPTP: parser = new Tptp(d_solver, d_symman, d_strictMode, d_parseOnly); break; default: - if (language::isInputLang_smt2(d_lang)) + if (language::isLangSmt2(d_lang)) { parser = new Smt2(d_solver, d_symman, d_strictMode, d_parseOnly); } @@ -108,7 +108,8 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { +ParserBuilder& ParserBuilder::withInputLanguage(Language lang) +{ d_lang = lang; return *this; } diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index aed3b06f1..61819a8f9 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -45,7 +45,7 @@ class Parser; class CVC5_EXPORT ParserBuilder { /** The input language */ - InputLanguage d_lang; + Language d_lang; /** The API Solver object. */ api::Solver* d_solver; @@ -93,7 +93,7 @@ class CVC5_EXPORT ParserBuilder * * (Default: LANG_AUTO) */ - ParserBuilder& withInputLanguage(InputLanguage lang); + ParserBuilder& withInputLanguage(Language lang); /** * Are we only parsing, or doing something with the resulting diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 2a39a6208..fe777fe27 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -711,16 +711,9 @@ api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars, return d_allocGrammars.back().get(); } -bool Smt2::sygus() const -{ - InputLanguage ilang = getLanguage(); - return ilang == language::input::LANG_SYGUS_V2; -} +bool Smt2::sygus() const { return language::isLangSygus(getLanguage()); } -bool Smt2::sygus_v2() const -{ - return getLanguage() == language::input::LANG_SYGUS_V2; -} +bool Smt2::sygus_v2() const { return getLanguage() == Language::LANG_SYGUS_V2; } void Smt2::checkThatLogicIsSet() { @@ -848,7 +841,7 @@ api::Term Smt2::mkAbstractValue(const std::string& name) return d_solver->mkAbstractValue(name.substr(1)); } -InputLanguage Smt2::getLanguage() const +Language Smt2::getLanguage() const { return d_solver->getOptions().base.inputLanguage; } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index c70a60e99..50b4a4efc 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -230,7 +230,7 @@ class Smt2 : public Parser */ bool v2_6(bool exact = false) const { - return language::isInputLang_smt2_6(getLanguage(), exact); + return language::isLangSmt2(getLanguage()); } /** Are we using a sygus language? */ bool sygus() const; @@ -415,7 +415,7 @@ class Smt2 : public Parser void addSepOperators(); - InputLanguage getLanguage() const; + Language getLanguage() const; /** * Utility function to create a conjunction of expressions. diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 11959f37b..b42304ecc 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -929,7 +929,7 @@ void CvcPrinter::toStreamNode(std::ostream& out, } toStreamNode(out, n[i], -1, false, lbind); out << ":"; - n[i].getType().toStream(out, language::output::LANG_CVC); + n[i].getType().toStream(out, Language::LANG_CVC); } out << ')'; return; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 69727e1a2..59122cf3d 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -31,32 +31,32 @@ using namespace std; namespace cvc5 { -unique_ptr<Printer> Printer::d_printers[language::output::LANG_MAX]; +unique_ptr<Printer> + Printer::d_printers[static_cast<size_t>(Language::LANG_MAX)]; -unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang) +unique_ptr<Printer> Printer::makePrinter(Language lang) { - using namespace cvc5::language::output; - switch(lang) { - case LANG_SMTLIB_V2_6: - return unique_ptr<Printer>( - new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); + case Language::LANG_SMTLIB_V2_6: + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); - case LANG_TPTP: - return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); + case Language::LANG_TPTP: + return unique_ptr<Printer>(new printer::tptp::TptpPrinter()); - case LANG_CVC: return unique_ptr<Printer>(new printer::cvc::CvcPrinter()); + case Language::LANG_CVC: + return unique_ptr<Printer>(new printer::cvc::CvcPrinter()); - case LANG_SYGUS_V2: - // sygus version 2.0 does not have discrepancies with smt2, hence we use - // a normal smt2 variant here. - return unique_ptr<Printer>( - new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); + case Language::LANG_SYGUS_V2: + // sygus version 2.0 does not have discrepancies with smt2, hence we use + // a normal smt2 variant here. + return unique_ptr<Printer>( + new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant)); - case LANG_AST: - return unique_ptr<Printer>(new printer::ast::AstPrinter()); + case Language::LANG_AST: + return unique_ptr<Printer>(new printer::ast::AstPrinter()); - default: Unhandled() << lang; + default: Unhandled() << lang; } } @@ -83,7 +83,7 @@ void Printer::toStream(std::ostream& out, const smt::Model& m) const }/* Printer::toStream(Model) */ -void Printer::toStreamUsing(OutputLanguage lang, +void Printer::toStreamUsing(Language lang, std::ostream& out, const smt::Model& m) const { @@ -140,9 +140,9 @@ void Printer::toStream(std::ostream& out, const SkolemList& sks) const out << ")" << std::endl; } -Printer* Printer::getPrinter(OutputLanguage lang) +Printer* Printer::getPrinter(Language lang) { - if (lang == language::output::LANG_AUTO) + if (lang == Language::LANG_AUTO) { // Infer the language to use for output. // @@ -154,22 +154,22 @@ Printer* Printer::getPrinter(OutputLanguage lang) { lang = options::outputLanguage(); } - if (lang == language::output::LANG_AUTO + if (lang == Language::LANG_AUTO && Options::current().base.inputLanguageWasSetByUser) { - lang = language::toOutputLanguage(options::inputLanguage()); + lang = options::inputLanguage(); } } - if (lang == language::output::LANG_AUTO) + if (lang == Language::LANG_AUTO) { - lang = language::output::LANG_SMTLIB_V2_6; // default + lang = Language::LANG_SMTLIB_V2_6; // default } } - if (d_printers[lang] == nullptr) + if (d_printers[static_cast<size_t>(lang)] == nullptr) { - d_printers[lang] = makePrinter(lang); + d_printers[static_cast<size_t>(lang)] = makePrinter(lang); } - return d_printers[lang].get(); + return d_printers[static_cast<size_t>(lang)].get(); } void Printer::printUnknownCommand(std::ostream& out, diff --git a/src/printer/printer.h b/src/printer/printer.h index 6c00ebad5..05ac8879b 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -42,8 +42,8 @@ class Printer */ virtual ~Printer() {} - /** Get the Printer for a given OutputLanguage */ - static Printer* getPrinter(OutputLanguage lang); + /** Get the Printer for a given Language */ + static Printer* getPrinter(Language lang); /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, @@ -286,7 +286,7 @@ class Printer Node n) const = 0; /** write model response to command using another language printer */ - void toStreamUsing(OutputLanguage lang, + void toStreamUsing(Language lang, std::ostream& out, const smt::Model& m) const; @@ -301,11 +301,12 @@ class Printer Printer(const Printer&) = delete; Printer& operator=(const Printer&) = delete; - /** Make a Printer for a given OutputLanguage */ - static std::unique_ptr<Printer> makePrinter(OutputLanguage lang); + /** Make a Printer for a given Language */ + static std::unique_ptr<Printer> makePrinter(Language lang); - /** Printers for each OutputLanguage */ - static std::unique_ptr<Printer> d_printers[language::output::LANG_MAX]; + /** Printers for each Language */ + static std::unique_ptr<Printer> + d_printers[static_cast<size_t>(Language::LANG_MAX)]; }; /* class Printer */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ba03a4fe8..b7f32123d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1204,7 +1204,7 @@ std::string Smt2Printer::smtKindString(Kind k, Variant v) void Smt2Printer::toStreamType(std::ostream& out, TypeNode tn) const { // we currently must call TypeNode::toStream here. - tn.toStream(out, language::output::LANG_SMTLIB_V2_6); + tn.toStream(out, Language::LANG_SMTLIB_V2_6); } template <class T> diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index 14bc6f220..bb8df120e 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -38,12 +38,12 @@ void TptpPrinter::toStream(std::ostream& out, int toDepth, size_t dag) const { - n.toStream(out, toDepth, dag, language::output::LANG_SMTLIB_V2_6); + n.toStream(out, toDepth, dag, Language::LANG_SMTLIB_V2_6); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const CommandStatus* s) const { - s->toStream(out, language::output::LANG_SMTLIB_V2_6); + s->toStream(out, Language::LANG_SMTLIB_V2_6); }/* TptpPrinter::toStream() */ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const @@ -52,7 +52,7 @@ void TptpPrinter::toStream(std::ostream& out, const smt::Model& m) const : "CandidateFiniteModel"); out << "% SZS output start " << statusName << " for " << m.getInputName() << endl; - this->Printer::toStreamUsing(language::output::LANG_SMTLIB_V2_6, out, m); + this->Printer::toStreamUsing(Language::LANG_SMTLIB_V2_6, out, m); out << "% SZS output end " << statusName << " for " << m.getInputName() << endl; } diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 6292b5982..b78659d39 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -121,7 +121,7 @@ void Assertions::initializeCheckSat(const std::vector<Node>& assumptions, void Assertions::assertFormula(const Node& n) { ensureBoolean(n); - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); + bool maybeHasFv = language::isLangSygus(options::inputLanguage()); addFormula(n, true, false, false, maybeHasFv); } @@ -185,7 +185,7 @@ void Assertions::addFormula(TNode n, else { se << "Cannot process assertion with free variable."; - if (language::isInputLangSygus(options::inputLanguage())) + if (language::isLangSygus(options::inputLanguage())) { // Common misuse of SyGuS is to use top-level assert instead of // constraint when defining the synthesis conjecture. @@ -207,7 +207,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global) { // Global definitions are asserted at check-sat-time because we have to // make sure that they are always present - Assert(!language::isInputLangSygus(options::inputLanguage())); + Assert(!language::isLangSygus(options::inputLanguage())); d_globalDefineFunLemmas->emplace_back(n); } else @@ -215,7 +215,7 @@ void Assertions::addDefineFunDefinition(Node n, bool global) // We don't permit functions-to-synthesize within recursive function // definitions currently. Thus, we should check for free variables if the // input language is SyGuS. - bool maybeHasFv = language::isInputLangSygus(options::inputLanguage()); + bool maybeHasFv = language::isLangSygus(options::inputLanguage()); addFormula(n, true, false, true, maybeHasFv); } } diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 3dafdd7f0..e6be0a646 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -223,7 +223,7 @@ std::string Command::toString() const return ss.str(); } -void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const +void CommandStatus::toStream(std::ostream& out, Language language) const { Printer::getPrinter(language)->toStream(out, this); } @@ -300,7 +300,7 @@ std::string EmptyCommand::getCommandName() const { return "empty"; } void EmptyCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name); } @@ -347,7 +347,7 @@ std::string EchoCommand::getCommandName() const { return "echo"; } void EchoCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdEcho(out, d_output); } @@ -383,7 +383,7 @@ std::string AssertCommand::getCommandName() const { return "assert"; } void AssertCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdAssert(out, termToNode(d_term)); } @@ -415,7 +415,7 @@ std::string PushCommand::getCommandName() const { return "push"; } void PushCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdPush(out); } @@ -447,7 +447,7 @@ std::string PopCommand::getCommandName() const { return "pop"; } void PopCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdPop(out); } @@ -504,7 +504,7 @@ std::string CheckSatCommand::getCommandName() const { return "check-sat"; } void CheckSatCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdCheckSat(out, termToNode(d_term)); } @@ -578,7 +578,7 @@ std::string CheckSatAssumingCommand::getCommandName() const void CheckSatAssumingCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdCheckSatAssuming( out, termVectorToNodes(d_terms)); @@ -629,7 +629,7 @@ std::string QueryCommand::getCommandName() const { return "query"; } void QueryCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdQuery(out, termToNode(d_term)); } @@ -666,7 +666,7 @@ std::string DeclareSygusVarCommand::getCommandName() const void DeclareSygusVarCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclareVar( out, termToNode(d_var), sortToTypeNode(d_sort)); @@ -723,7 +723,7 @@ std::string SynthFunCommand::getCommandName() const void SynthFunCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { std::vector<Node> nodeVars = termVectorToNodes(d_vars); Printer::getPrinter(language)->toStreamCmdSynthFun( @@ -770,7 +770,7 @@ std::string SygusConstraintCommand::getCommandName() const void SygusConstraintCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdConstraint(out, termToNode(d_term)); } @@ -825,7 +825,7 @@ std::string SygusInvConstraintCommand::getCommandName() const void SygusInvConstraintCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdInvConstraint( out, @@ -866,7 +866,7 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) { std::vector<api::Term> synthFuns = sm->getFunctionsToSynthesize(); d_solution << "(" << std::endl; - Printer* p = Printer::getPrinter(language::output::LANG_SYGUS_V2); + Printer* p = Printer::getPrinter(Language::LANG_SYGUS_V2); for (api::Term& f : synthFuns) { api::Term sol = solver->getSynthSolution(f); @@ -916,7 +916,7 @@ std::string CheckSynthCommand::getCommandName() const { return "check-synth"; } void CheckSynthCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdCheckSynth(out); } @@ -945,7 +945,7 @@ std::string ResetCommand::getCommandName() const { return "reset"; } void ResetCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdReset(out); } @@ -981,7 +981,7 @@ std::string ResetAssertionsCommand::getCommandName() const void ResetAssertionsCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdResetAssertions(out); } @@ -1002,7 +1002,7 @@ std::string QuitCommand::getCommandName() const { return "exit"; } void QuitCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdQuit(out); } @@ -1025,7 +1025,7 @@ std::string CommentCommand::getCommandName() const { return "comment"; } void CommentCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdComment(out, d_comment); } @@ -1123,7 +1123,7 @@ std::string CommandSequence::getCommandName() const { return "sequence"; } void CommandSequence::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdCommandSequence(out, d_commandSequence); @@ -1136,7 +1136,7 @@ void CommandSequence::toStream(std::ostream& out, void DeclarationSequence::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclarationSequence( out, d_commandSequence); @@ -1190,7 +1190,7 @@ std::string DeclareFunctionCommand::getCommandName() const void DeclareFunctionCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclareFunction( out, d_func.toString(), sortToTypeNode(d_sort)); @@ -1241,7 +1241,7 @@ std::string DeclarePoolCommand::getCommandName() const void DeclarePoolCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclarePool( out, @@ -1283,7 +1283,7 @@ std::string DeclareSortCommand::getCommandName() const void DeclareSortCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclareType(out, sortToTypeNode(d_sort)); @@ -1326,7 +1326,7 @@ std::string DefineSortCommand::getCommandName() const { return "define-sort"; } void DefineSortCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDefineType( out, d_symbol, sortVectorToTypeNodes(d_params), sortToTypeNode(d_sort)); @@ -1399,7 +1399,7 @@ std::string DefineFunctionCommand::getCommandName() const void DefineFunctionCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { TypeNode rangeType = termToNode(d_func).getType(); if (rangeType.isFunction()) @@ -1483,7 +1483,7 @@ std::string DefineFunctionRecCommand::getCommandName() const void DefineFunctionRecCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { std::vector<std::vector<Node>> formals; formals.reserve(d_formals.size()); @@ -1524,7 +1524,7 @@ std::string DeclareHeapCommand::getCommandName() const void DeclareHeapCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclareHeap( out, sortToTypeNode(d_locSort), sortToTypeNode(d_dataSort)); @@ -1578,7 +1578,7 @@ std::string SimplifyCommand::getCommandName() const { return "simplify"; } void SimplifyCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdSimplify(out, termToNode(d_term)); } @@ -1658,7 +1658,7 @@ std::string GetValueCommand::getCommandName() const { return "get-value"; } void GetValueCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetValue( out, termVectorToNodes(d_terms)); @@ -1739,7 +1739,7 @@ std::string GetAssignmentCommand::getCommandName() const void GetAssignmentCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetAssignment(out); } @@ -1812,7 +1812,7 @@ std::string GetModelCommand::getCommandName() const { return "get-model"; } void GetModelCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetModel(out); } @@ -1854,7 +1854,7 @@ std::string BlockModelCommand::getCommandName() const { return "block-model"; } void BlockModelCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdBlockModel(out); } @@ -1911,7 +1911,7 @@ std::string BlockModelValuesCommand::getCommandName() const void BlockModelValuesCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdBlockModelValues( out, termVectorToNodes(d_terms)); @@ -1962,7 +1962,7 @@ std::string GetProofCommand::getCommandName() const { return "get-proof"; } void GetProofCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetProof(out); } @@ -2022,7 +2022,7 @@ std::string GetInstantiationsCommand::getCommandName() const void GetInstantiationsCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetInstantiations(out); } @@ -2111,7 +2111,7 @@ std::string GetInterpolCommand::getCommandName() const void GetInterpolCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetInterpol( out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar)); @@ -2196,7 +2196,7 @@ std::string GetAbductCommand::getCommandName() const { return "get-abduct"; } void GetAbductCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetAbduct( out, d_name, termToNode(d_conj), grammarToTypeNode(d_sygus_grammar)); @@ -2272,7 +2272,7 @@ std::string GetQuantifierEliminationCommand::getCommandName() const void GetQuantifierEliminationCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetQuantifierElimination( out, termToNode(d_term)); @@ -2334,7 +2334,7 @@ std::string GetUnsatAssumptionsCommand::getCommandName() const void GetUnsatAssumptionsCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out); } @@ -2411,7 +2411,7 @@ std::string GetUnsatCoreCommand::getCommandName() const void GetUnsatCoreCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out); } @@ -2468,7 +2468,7 @@ std::string GetAssertionsCommand::getCommandName() const void GetAssertionsCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetAssertions(out); } @@ -2515,7 +2515,7 @@ std::string SetBenchmarkStatusCommand::getCommandName() const void SetBenchmarkStatusCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Result::Sat status = Result::SAT_UNKNOWN; switch (d_status) @@ -2564,7 +2564,7 @@ std::string SetBenchmarkLogicCommand::getCommandName() const void SetBenchmarkLogicCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic); } @@ -2609,7 +2609,7 @@ std::string SetInfoCommand::getCommandName() const { return "set-info"; } void SetInfoCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdSetInfo(out, d_flag, d_value); } @@ -2665,7 +2665,7 @@ std::string GetInfoCommand::getCommandName() const { return "get-info"; } void GetInfoCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag); } @@ -2709,7 +2709,7 @@ std::string SetOptionCommand::getCommandName() const { return "set-option"; } void SetOptionCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdSetOption(out, d_flag, d_value); } @@ -2762,7 +2762,7 @@ std::string GetOptionCommand::getCommandName() const { return "get-option"; } void GetOptionCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag); } @@ -2807,7 +2807,7 @@ std::string DatatypeDeclarationCommand::getCommandName() const void DatatypeDeclarationCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration( out, sortVectorToTypeNodes(d_datatypes)); diff --git a/src/smt/command.h b/src/smt/command.h index b83da5825..d3e3679d2 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -130,7 +130,7 @@ class CVC5_EXPORT CommandStatus public: virtual ~CommandStatus() {} void toStream(std::ostream& out, - OutputLanguage language = language::output::LANG_AUTO) const; + Language language = Language::LANG_AUTO) const; virtual CommandStatus& clone() const = 0; }; /* class CommandStatus */ @@ -217,12 +217,11 @@ class CVC5_EXPORT Command SymbolManager* sm, std::ostream& out); - virtual void toStream( - std::ostream& out, - int toDepth = -1, + virtual void toStream(std::ostream& out, + int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const = 0; + size_t dag = 1, + Language language = Language::LANG_AUTO) const = 0; std::string toString() const; @@ -316,11 +315,10 @@ class CVC5_EXPORT EmptyCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: std::string d_name; @@ -340,11 +338,10 @@ class CVC5_EXPORT EchoCommand : public Command Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: std::string d_output; @@ -364,11 +361,10 @@ class CVC5_EXPORT AssertCommand : public Command Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class AssertCommand */ class CVC5_EXPORT PushCommand : public Command @@ -377,11 +373,10 @@ class CVC5_EXPORT PushCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class PushCommand */ class CVC5_EXPORT PopCommand : public Command @@ -390,11 +385,10 @@ class CVC5_EXPORT PopCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class PopCommand */ class CVC5_EXPORT DeclarationDefinitionCommand : public Command @@ -423,11 +417,10 @@ class CVC5_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand @@ -449,11 +442,10 @@ class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class DeclarePoolCommand */ class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand @@ -471,11 +463,10 @@ class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class DeclareSortCommand */ class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand @@ -496,11 +487,10 @@ class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class DefineSortCommand */ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand @@ -523,11 +513,10 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** The function we are defining */ @@ -567,11 +556,10 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** functions we are defining */ @@ -602,11 +590,10 @@ class CVC5_EXPORT DeclareHeapCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** The location sort */ @@ -631,11 +618,10 @@ class CVC5_EXPORT CheckSatCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; private: api::Term d_term; @@ -659,11 +645,10 @@ class CVC5_EXPORT CheckSatAssumingCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; private: std::vector<api::Term> d_terms; @@ -685,11 +670,10 @@ class CVC5_EXPORT QueryCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class QueryCommand */ /* ------------------- sygus commands ------------------ */ @@ -714,11 +698,10 @@ class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** the declared variable */ @@ -763,11 +746,10 @@ class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** the function-to-synthesize */ @@ -800,11 +782,10 @@ class CVC5_EXPORT SygusConstraintCommand : public Command /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** the declared constraint */ @@ -843,11 +824,10 @@ class CVC5_EXPORT SygusInvConstraintCommand : public Command /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** the place holder predicates with which to build the actual constraint @@ -879,11 +859,10 @@ class CVC5_EXPORT CheckSynthCommand : public Command /** returns this command's name */ std::string getCommandName() const override; /** prints this command */ - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** result of the check-synth call */ @@ -910,11 +889,10 @@ class CVC5_EXPORT SimplifyCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class SimplifyCommand */ class CVC5_EXPORT GetValueCommand : public Command @@ -933,11 +911,10 @@ class CVC5_EXPORT GetValueCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class GetValueCommand */ class CVC5_EXPORT GetAssignmentCommand : public Command @@ -953,11 +930,10 @@ class CVC5_EXPORT GetAssignmentCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class GetAssignmentCommand */ class CVC5_EXPORT GetModelCommand : public Command @@ -968,11 +944,10 @@ class CVC5_EXPORT GetModelCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: smt::Model* d_result; @@ -987,11 +962,10 @@ class CVC5_EXPORT BlockModelCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class BlockModelCommand */ /** The command to block model values. */ @@ -1004,11 +978,10 @@ class CVC5_EXPORT BlockModelValuesCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** The terms we are blocking */ @@ -1026,11 +999,10 @@ class CVC5_EXPORT GetProofCommand : public Command Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; private: /** the result of the getProof call */ @@ -1047,11 +1019,10 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: api::Solver* d_solver; @@ -1085,11 +1056,10 @@ class CVC5_EXPORT GetInterpolCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** The name of the interpolation predicate */ @@ -1136,11 +1106,10 @@ class CVC5_EXPORT GetAbductCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** The name of the abduction predicate */ @@ -1174,11 +1143,10 @@ class CVC5_EXPORT GetQuantifierEliminationCommand : public Command Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class GetQuantifierEliminationCommand */ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command @@ -1190,11 +1158,10 @@ class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: std::vector<api::Term> d_result; @@ -1211,11 +1178,10 @@ class CVC5_EXPORT GetUnsatCoreCommand : public Command Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; protected: /** The symbol manager we were invoked with */ @@ -1237,11 +1203,10 @@ class CVC5_EXPORT GetAssertionsCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class GetAssertionsCommand */ class CVC5_EXPORT SetBenchmarkStatusCommand : public Command @@ -1257,11 +1222,10 @@ class CVC5_EXPORT SetBenchmarkStatusCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class SetBenchmarkStatusCommand */ class CVC5_EXPORT SetBenchmarkLogicCommand : public Command @@ -1276,11 +1240,10 @@ class CVC5_EXPORT SetBenchmarkLogicCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class SetBenchmarkLogicCommand */ class CVC5_EXPORT SetInfoCommand : public Command @@ -1298,11 +1261,10 @@ class CVC5_EXPORT SetInfoCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class SetInfoCommand */ class CVC5_EXPORT GetInfoCommand : public Command @@ -1321,11 +1283,10 @@ class CVC5_EXPORT GetInfoCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class GetInfoCommand */ class CVC5_EXPORT SetOptionCommand : public Command @@ -1343,11 +1304,10 @@ class CVC5_EXPORT SetOptionCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class SetOptionCommand */ class CVC5_EXPORT GetOptionCommand : public Command @@ -1366,11 +1326,10 @@ class CVC5_EXPORT GetOptionCommand : public Command void printResult(std::ostream& out, uint32_t verbosity = 2) const override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class GetOptionCommand */ class CVC5_EXPORT DatatypeDeclarationCommand : public Command @@ -1386,11 +1345,10 @@ class CVC5_EXPORT DatatypeDeclarationCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class DatatypeDeclarationCommand */ class CVC5_EXPORT ResetCommand : public Command @@ -1400,11 +1358,10 @@ class CVC5_EXPORT ResetCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class ResetCommand */ class CVC5_EXPORT ResetAssertionsCommand : public Command @@ -1414,11 +1371,10 @@ class CVC5_EXPORT ResetAssertionsCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class ResetAssertionsCommand */ class CVC5_EXPORT QuitCommand : public Command @@ -1428,11 +1384,10 @@ class CVC5_EXPORT QuitCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class QuitCommand */ class CVC5_EXPORT CommentCommand : public Command @@ -1447,11 +1402,10 @@ class CVC5_EXPORT CommentCommand : public Command void invoke(api::Solver* solver, SymbolManager* sm) override; Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class CommentCommand */ class CVC5_EXPORT CommandSequence : public Command @@ -1485,20 +1439,18 @@ class CVC5_EXPORT CommandSequence : public Command Command* clone() const override; std::string getCommandName() const override; - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; /* class CommandSequence */ class CVC5_EXPORT DeclarationSequence : public CommandSequence { - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; }; } // namespace cvc5 diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp index b3e747ecb..000107341 100644 --- a/src/smt/node_command.cpp +++ b/src/smt/node_command.cpp @@ -59,7 +59,7 @@ DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id, void DeclareFunctionNodeCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type); } @@ -85,7 +85,7 @@ DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id, void DeclareTypeNodeCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type); } @@ -112,7 +112,7 @@ DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand( void DeclareDatatypeNodeCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out, d_datatypes); @@ -139,7 +139,7 @@ DefineFunctionNodeCommand::DefineFunctionNodeCommand( void DefineFunctionNodeCommand::toStream(std::ostream& out, int toDepth, size_t dag, - OutputLanguage language) const + Language language) const { TypeNode tn = d_fun.getType(); bool hasRange = diff --git a/src/smt/node_command.h b/src/smt/node_command.h index 0bd60fe9a..3399cb6fb 100644 --- a/src/smt/node_command.h +++ b/src/smt/node_command.h @@ -37,11 +37,10 @@ class NodeCommand virtual ~NodeCommand(); /** Print this NodeCommand to output stream */ - virtual void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const = 0; + virtual void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const = 0; /** Get a string representation of this NodeCommand */ std::string toString() const; @@ -60,11 +59,10 @@ class DeclareFunctionNodeCommand : public NodeCommand { public: DeclareFunctionNodeCommand(const std::string& id, Node fun, TypeNode type); - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; NodeCommand* clone() const override; const Node& getFunction() const; @@ -82,11 +80,10 @@ class DeclareDatatypeNodeCommand : public NodeCommand { public: DeclareDatatypeNodeCommand(const std::vector<TypeNode>& datatypes); - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; NodeCommand* clone() const override; private: @@ -101,11 +98,10 @@ class DeclareTypeNodeCommand : public NodeCommand { public: DeclareTypeNodeCommand(const std::string& id, size_t arity, TypeNode type); - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; NodeCommand* clone() const override; const std::string getSymbol() const; const TypeNode& getType() const; @@ -127,11 +123,10 @@ class DefineFunctionNodeCommand : public NodeCommand Node fun, const std::vector<Node>& formals, Node formula); - void toStream( - std::ostream& out, - int toDepth = -1, - size_t dag = 1, - OutputLanguage language = language::output::LANG_AUTO) const override; + void toStream(std::ostream& out, + int toDepth = -1, + size_t dag = 1, + Language language = Language::LANG_AUTO) const override; NodeCommand* clone() const override; private: diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp index 5730ea062..fecf65275 100644 --- a/src/smt/optimization_solver.cpp +++ b/src/smt/optimization_solver.cpp @@ -33,8 +33,8 @@ namespace smt { std::ostream& operator<<(std::ostream& out, const OptimizationResult& result) { // check the output language first - OutputLanguage lang = language::SetLanguage::getLanguage(out); - if (!language::isOutputLang_smt2(lang)) + Language lang = language::SetLanguage::getLanguage(out); + if (!language::isLangSmt2(lang)) { Unimplemented() << "Only the SMTLib2 language supports optimization right now"; @@ -67,8 +67,8 @@ std::ostream& operator<<(std::ostream& out, const OptimizationObjective& objective) { // check the output language first - OutputLanguage lang = language::SetLanguage::getLanguage(out); - if (!language::isOutputLang_smt2(lang)) + Language lang = language::SetLanguage::getLanguage(out); + if (!language::isLangSmt2(lang)) { Unimplemented() << "Only the SMTLib2 language supports optimization right now"; diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index d158d5010..ec15e67e6 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -1006,7 +1006,7 @@ void SetDefaults::setDefaultsPost(const LogicInfo& logic, Options& opts) const bool SetDefaults::isSygus(const Options& opts) const { - if (language::isInputLangSygus(opts.base.inputLanguage)) + if (language::isLangSygus(opts.base.inputLanguage)) { return true; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f55bfa88b..45056057d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -438,7 +438,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) } else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser) { - language::input::Language ilang = language::input::LANG_SMTLIB_V2_6; + Language ilang = Language::LANG_SMTLIB_V2_6; if (value != "2" && value != "2.6") { @@ -450,7 +450,7 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value) // also update the output language if (!getOptions().base.outputLanguageWasSetByUser) { - language::output::Language olang = language::toOutputLanguage(ilang); + Language olang = ilang; if (d_env->getOptions().base.outputLanguage != olang) { getOptions().base.outputLanguage = olang; @@ -2022,21 +2022,7 @@ std::string SmtEngine::getOption(const std::string& key) const return nm->mkNode(Kind::SEXPR, result).toString(); } - std::string atom = options::get(getOptions(), key); - - if (atom != "true" && atom != "false") - { - try - { - Integer z(atom); - } - catch (std::invalid_argument&) - { - atom = "\"" + atom + "\""; - } - } - - return atom; + return options::get(getOptions(), key); } Options& SmtEngine::getOptions() { return d_env->d_options; } diff --git a/src/theory/quantifiers/sygus/synth_verify.cpp b/src/theory/quantifiers/sygus/synth_verify.cpp index 23ee0e648..9e8171fdc 100644 --- a/src/theory/quantifiers/sygus/synth_verify.cpp +++ b/src/theory/quantifiers/sygus/synth_verify.cpp @@ -43,7 +43,7 @@ SynthVerify::SynthVerify(const Options& opts, TermDbSygus* tds) : d_tds(tds) // Disable sygus on the subsolver. This is particularly important since it // ensures that recursive function definitions have the standard ownership // instead of being claimed by sygus in the subsolver. - d_subOptions.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; + d_subOptions.base.inputLanguage = Language::LANG_SMTLIB_V2_6; d_subOptions.quantifiers.sygus = false; // use tangent planes by default, since we want to put effort into // the verification step for sygus queries with non-linear arithmetic diff --git a/src/util/result.cpp b/src/util/result.cpp index 84e06cdb7..23f38b7ce 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -354,14 +354,13 @@ void Result::toStreamTptp(std::ostream& out) const { out << " for " << getInputName(); } -void Result::toStream(std::ostream& out, OutputLanguage language) const { +void Result::toStream(std::ostream& out, Language language) const +{ switch (language) { - case language::output::LANG_SYGUS_V2: toStreamSmt2(out); break; - case language::output::LANG_TPTP: - toStreamTptp(out); - break; + case Language::LANG_SYGUS_V2: toStreamSmt2(out); break; + case Language::LANG_TPTP: toStreamTptp(out); break; default: - if (language::isOutputLang_smt2(language)) + if (language::isLangSmt2(language)) { toStreamSmt2(out); } diff --git a/src/util/result.h b/src/util/result.h index 716c580e9..251d34548 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -122,7 +122,7 @@ class Result /** * Write a Result out to a stream in this language. */ - void toStream(std::ostream& out, OutputLanguage language) const; + void toStream(std::ostream& out, Language language) const; /** * This is mostly the same the default |