This PR combines the two enums InputLanguage and OutputLanguage into a single Language type. It makes sure that AST is not used as input language using a predicate whenever the option is set.
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;
}
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;
}
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;
}
* 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);
* 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) {
}
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) {
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();
}
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
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;
* 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) {
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();
}
* @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);
}
* 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) {
}
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();
#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;
}
catch (ParserException& pe)
{
- if (language::isOutputLang_smt2(d_options.base.outputLanguage))
+ if (language::isLangSmt2(d_options.base.outputLanguage))
{
d_out << "(error \"" << pe << "\")" << endl;
}
#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;
}
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)"
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)"
#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
* directory for licensing information.
* ****************************************************************************
*
- * Definition of input and output languages.
+ * Definition of languages.
*/
#include "cvc5_public.h"
#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
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,
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);
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);
}
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;
}
*/
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.
* 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 */
/**
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;
* @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);
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;
<< "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;
}
: 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() << "]: "
return d_inputStream;
}
-Input* Input::newFileInput(InputLanguage lang,
+Input* Input::newFileInput(Language lang,
const std::string& filename,
bool useMmap)
{
return AntlrInput::newInput(lang, *inputStream);
}
-Input* Input::newStreamInput(InputLanguage lang,
+Input* Input::newStreamInput(Language lang,
std::istream& input,
const std::string& name)
{
return AntlrInput::newInput(lang, *inputStream);
}
-Input* Input::newStringInput(InputLanguage lang,
+Input* Input::newStringInput(Language lang,
const std::string& str,
const std::string& name)
{
* @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);
* (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);
* @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);
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);
}
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;
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);
}
return *this;
}
-ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) {
+ParserBuilder& ParserBuilder::withInputLanguage(Language lang)
+{
d_lang = lang;
return *this;
}
class CVC5_EXPORT ParserBuilder
{
/** The input language */
- InputLanguage d_lang;
+ Language d_lang;
/** The API Solver object. */
api::Solver* d_solver;
*
* (Default: LANG_AUTO)
*/
- ParserBuilder& withInputLanguage(InputLanguage lang);
+ ParserBuilder& withInputLanguage(Language lang);
/**
* Are we only parsing, or doing something with the resulting
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()
{
return d_solver->mkAbstractValue(name.substr(1));
}
-InputLanguage Smt2::getLanguage() const
+Language Smt2::getLanguage() const
{
return d_solver->getOptions().base.inputLanguage;
}
*/
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;
void addSepOperators();
- InputLanguage getLanguage() const;
+ Language getLanguage() const;
/**
* Utility function to create a conjunction of expressions.
}
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;
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;
}
}
}/* Printer::toStream(Model) */
-void Printer::toStreamUsing(OutputLanguage lang,
+void Printer::toStreamUsing(Language lang,
std::ostream& out,
const smt::Model& m) 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.
//
{
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,
*/
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,
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;
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 */
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>
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
: "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;
}
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);
}
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.
{
// 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
// 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);
}
}
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);
}
void EmptyCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdEmpty(out, d_name);
}
void EchoCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdEcho(out, d_output);
}
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));
}
void PushCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdPush(out);
}
void PopCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdPop(out);
}
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));
}
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));
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));
}
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));
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(
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));
}
void SygusInvConstraintCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdInvConstraint(
out,
{
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);
void CheckSynthCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdCheckSynth(out);
}
void ResetCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdReset(out);
}
void ResetAssertionsCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdResetAssertions(out);
}
void QuitCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdQuit(out);
}
void CommentCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdComment(out, d_comment);
}
void CommandSequence::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdCommandSequence(out,
d_commandSequence);
void DeclarationSequence::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdDeclarationSequence(
out, d_commandSequence);
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));
void DeclarePoolCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdDeclarePool(
out,
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));
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));
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())
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());
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));
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));
}
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));
void GetAssignmentCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetAssignment(out);
}
void GetModelCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetModel(out);
}
void BlockModelCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdBlockModel(out);
}
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));
void GetProofCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetProof(out);
}
void GetInstantiationsCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
}
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));
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));
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));
void GetUnsatAssumptionsCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetUnsatAssumptions(out);
}
void GetUnsatCoreCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetUnsatCore(out);
}
void GetAssertionsCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetAssertions(out);
}
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)
void SetBenchmarkLogicCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdSetBenchmarkLogic(out, d_logic);
}
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);
}
void GetInfoCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetInfo(out, d_flag);
}
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);
}
void GetOptionCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdGetOption(out, d_flag);
}
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));
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 */
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;
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;
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;
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
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
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
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
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
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
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
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 */
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 */
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 */
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;
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;
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 ------------------ */
/** 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 */
/** 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 */
/** 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 */
/** 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
/** 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 */
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
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
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
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;
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. */
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 */
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 */
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;
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 */
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 */
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
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;
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 */
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
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
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
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
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
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
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
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
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
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
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
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
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
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);
}
void DeclareTypeNodeCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type);
}
void DeclareDatatypeNodeCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out,
d_datatypes);
void DefineFunctionNodeCommand::toStream(std::ostream& out,
int toDepth,
size_t dag,
- OutputLanguage language) const
+ Language language) const
{
TypeNode tn = d_fun.getType();
bool hasRange =
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;
{
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;
{
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:
{
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;
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:
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";
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";
bool SetDefaults::isSygus(const Options& opts) const
{
- if (language::isInputLangSygus(opts.base.inputLanguage))
+ if (language::isLangSygus(opts.base.inputLanguage))
{
return true;
}
}
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")
{
// 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;
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; }
// 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
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);
}
/**
* 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
}
api::Solver solver;
- InputLanguage ilang =
- input_language == "smt2" ? input::LANG_SMTLIB_V2 : input::LANG_CVC;
+ Language ilang = input_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+ : Language::LANG_CVC;
solver.setOption("input-language", input_language);
solver.setOption("output-language", output_language);
std::cout << "==============================================" << std::endl
<< "translating from "
- << (input_language == "smt2" ? input::LANG_SMTLIB_V2
- : input::LANG_CVC)
+ << (input_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+ : Language::LANG_CVC)
<< " to "
- << (output_language == "smt2" ? output::LANG_SMTLIB_V2
- : output::LANG_CVC)
+ << (output_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+ : Language::LANG_CVC)
<< " this string:" << std::endl
<< instr << std::endl;
std::string outstr = parse(instr, input_language, output_language);
std::cout << "got this:" << std::endl
<< outstr << std::endl
<< "reparsing as "
- << (output_language == "smt2" ? input::LANG_SMTLIB_V2
- : input::LANG_CVC)
+ << (output_language == "smt2" ? Language::LANG_SMTLIB_V2_6
+ : Language::LANG_CVC)
<< std::endl;
std::string poutstr = parse(outstr, output_language, output_language);
assert(outstr == poutstr);
{
std::cout << std::endl
<< "starting with: " << instr << std::endl
- << " in language " << input::LANG_SMTLIB_V2 << std::endl;
+ << " in language " << Language::LANG_SMTLIB_V2_6 << std::endl;
std::string smt2str = translate(instr, instr_language, "smt2");
std::cout << "in SMT2 : " << smt2str << std::endl;
std::string cvcstr = translate(smt2str, "smt2", "cvc");
int main()
{
- cout << language::SetLanguage(language::output::LANG_SMTLIB_V2);
+ cout << language::SetLanguage(Language::LANG_SMTLIB_V2_6);
std::unique_ptr<api::Solver> solver = std::make_unique<api::Solver>();
solver->setOption("input-language", "smtlib2");
std::unique_ptr<Parser> p(
ParserBuilder(solver, symman.get(), solver->getOptions()).build());
- p->setInput(Input::newStringInput(language::input::LANG_SMTLIB_V2,
+ p->setInput(Input::newStringInput(Language::LANG_SMTLIB_V2_6,
string("(get-info ") + s + ")",
"<internal>"));
assert(p != NULL);
; than the language specified in the input file.
;
; COMMAND-LINE: --lang=smt2.6
-; EXPECT: "LANG_SMTLIB_V2_6"
+; EXPECT: LANG_SMTLIB_V2_6
(set-info :smt-lib-version 2.6)
(get-option :input-language)
; EXPECT: true
; EXPECT: false
; EXPECT: 15
-; EXPECT: "SimplificationMode::NONE"
+; EXPECT: SimplificationMode::NONE
(get-option :command-verbosity)
(set-option :command-verbosity (* 1))
TestNode::SetUp();
// setup an SMT engine so that options are in scope
Options opts;
- opts.base.outputLanguage = OutputLanguage::LANG_AST;
+ opts.base.outputLanguage = Language::LANG_AST;
opts.base.outputLanguageWasSetByUser = true;
d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
}
OR, {fffx_eq_x, fffx_eq_y, fx_eq_gx, x_eq_y, fgx_eq_gy});
std::stringstream sstr;
- sstr << Node::setdepth(-1) << Node::setlanguage(language::output::LANG_CVC);
+ sstr << Node::setdepth(-1) << Node::setlanguage(Language::LANG_CVC);
sstr << Node::dag(false) << n; // never dagify
ASSERT_EQ(sstr.str(),
"(f(f(f(x))) = x) OR (f(f(f(x))) = y) OR (f(x) = g(x)) OR (x = "
namespace cvc5 {
using namespace parser;
-using namespace language::input;
namespace test {
class TestParserBlackParser : public TestInternal
{
protected:
- TestParserBlackParser(InputLanguage lang) : d_lang(lang) {}
+ TestParserBlackParser(Language lang) : d_lang(lang) {}
virtual ~TestParserBlackParser() {}
.withInputLanguage(d_lang)
.build());
parser->setInput(Input::newStringInput(d_lang, goodExpr, "test"));
- if (d_lang == LANG_SMTLIB_V2)
+ if (d_lang == Language::LANG_SMTLIB_V2_6)
{
/* Use QF_LIA to make multiplication ("*") available */
std::unique_ptr<Command> cmd(
, ParserException);
}
- InputLanguage d_lang;
+ Language d_lang;
std::unique_ptr<cvc5::api::Solver> d_solver;
std::unique_ptr<SymbolManager> d_symman;
};
class TestParserBlackCvCParser : public TestParserBlackParser
{
protected:
- TestParserBlackCvCParser() : TestParserBlackParser(LANG_CVC) {}
+ TestParserBlackCvCParser() : TestParserBlackParser(Language::LANG_CVC) {}
};
TEST_F(TestParserBlackCvCParser, good_inputs)
class TestParserBlackSmt2Parser : public TestParserBlackParser
{
protected:
- TestParserBlackSmt2Parser() : TestParserBlackParser(LANG_SMTLIB_V2) {}
+ TestParserBlackSmt2Parser()
+ : TestParserBlackParser(Language::LANG_SMTLIB_V2_6)
+ {
+ }
};
TEST_F(TestParserBlackSmt2Parser, good_inputs)
namespace cvc5 {
using namespace parser;
-using namespace language::input;
namespace test {
ASSERT_NE(filename, nullptr);
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
- .withInputLanguage(LANG_CVC)
+ .withInputLanguage(Language::LANG_CVC)
.build());
- parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
+ parser->setInput(Input::newFileInput(Language::LANG_CVC, filename, false));
checkEmptyInput(parser.get());
remove(filename);
fs.close();
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
- .withInputLanguage(LANG_CVC)
+ .withInputLanguage(Language::LANG_CVC)
.build());
- parser->setInput(Input::newFileInput(LANG_CVC, filename, false));
+ parser->setInput(Input::newFileInput(Language::LANG_CVC, filename, false));
checkTrueInput(parser.get());
remove(filename);
TEST_F(TestParseBlackParserBuilder, empty_string_input)
{
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
- .withInputLanguage(LANG_CVC)
+ .withInputLanguage(Language::LANG_CVC)
.build());
- parser->setInput(Input::newStringInput(LANG_CVC, "", "foo"));
+ parser->setInput(Input::newStringInput(Language::LANG_CVC, "", "foo"));
checkEmptyInput(parser.get());
}
TEST_F(TestParseBlackParserBuilder, true_string_input)
{
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
- .withInputLanguage(LANG_CVC)
+ .withInputLanguage(Language::LANG_CVC)
.build());
- parser->setInput(Input::newStringInput(LANG_CVC, "TRUE", "foo"));
+ parser->setInput(Input::newStringInput(Language::LANG_CVC, "TRUE", "foo"));
checkTrueInput(parser.get());
}
{
std::stringstream ss("", std::ios_base::in);
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
- .withInputLanguage(LANG_CVC)
+ .withInputLanguage(Language::LANG_CVC)
.build());
- parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
+ parser->setInput(Input::newStreamInput(Language::LANG_CVC, ss, "foo"));
checkEmptyInput(parser.get());
}
{
std::stringstream ss("TRUE", std::ios_base::in);
std::unique_ptr<Parser> parser(ParserBuilder(&d_solver, d_symman.get())
- .withInputLanguage(LANG_CVC)
+ .withInputLanguage(Language::LANG_CVC)
.build());
- parser->setInput(Input::newStreamInput(LANG_CVC, ss, "foo"));
+ parser->setInput(Input::newStreamInput(Language::LANG_CVC, ss, "foo"));
checkTrueInput(parser.get());
}
void checkToString(TNode n, const std::string& expected)
{
std::stringstream ss;
- ss << Node::setdepth(-1)
- << Node::setlanguage(language::output::LANG_SMTLIB_V2_6) << n;
+ ss << Node::setdepth(-1) << Node::setlanguage(Language::LANG_SMTLIB_V2_6)
+ << n;
ASSERT_EQ(ss.str(), expected);
}
};
Assert(BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD >= 10);
std::cout << expr::ExprSetDepth(-1)
- << language::SetLanguage(language::output::LANG_CVC);
+ << language::SetLanguage(Language::LANG_CVC);
}
// assert equality up to commuting children
projects / cvc5.git / commitdiff