From 5f207ba01302c3245e169bfbe2ed91ad0cd659cd Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 18 Dec 2015 17:19:07 -0800 Subject: [PATCH] Modifying emptyset.h and sexpr. Adding SetLanguage. - Modifies expr/emptyset.h to use SetType only as an incomplete type within expr/emptyset.h. This breaks the include cycle between expr/emptyset.h, expr/expr.h and expr/type.h. - Refactors SExpr to avoid a potentially infinite cycle. This is likely overkill, but it works. - Moving Expr::setlanguage and related utilities out of the Expr class and into their own file. This allows files in util/ to know the output language set on an ostream. --- doc/libcvc4.3_template.in | 2 +- examples/api/sets.cpp | 5 +- examples/api/strings.cpp | 5 +- examples/hashsmt/sha1_collision.cpp | 14 +- examples/hashsmt/sha1_inversion.cpp | 16 +- examples/nra-translate/normalize.cpp | 16 +- examples/sets-translate/sets_translate.cpp | 19 +- examples/translator.cpp | 3 +- src/compat/cvc3_compat.cpp | 3 +- src/expr/datatype.cpp | 9 +- src/expr/emptyset.cpp | 60 +++++- src/expr/emptyset.h | 63 +++--- src/expr/expr_template.cpp | 1 - src/expr/expr_template.h | 104 ---------- src/expr/node.h | 3 +- src/expr/sexpr.cpp | 188 +++++++++++++++++- src/expr/sexpr.h | 169 +++++----------- src/main/command_executor_portfolio.cpp | 3 +- src/main/driver_unified.cpp | 5 +- src/options/Makefile.am | 2 + src/options/language.h | 2 +- src/options/set_language.cpp | 81 ++++++++ src/options/set_language.h | 99 +++++++++ src/parser/cvc/Cvc.g | 7 +- src/parser/smt2/Smt2.g | 3 +- src/printer/smt2/smt2_printer.cpp | 2 +- src/smt/smt_engine.cpp | 7 +- src/smt/smt_options_handler.cpp | 5 +- src/theory/quantifiers/term_database.cpp | 2 +- test/system/ouroborous.cpp | 3 +- test/system/smt2_compliance.cpp | 3 +- test/unit/util/boolean_simplification_black.h | 3 +- 32 files changed, 572 insertions(+), 335 deletions(-) create mode 100644 src/options/set_language.cpp create mode 100644 src/options/set_language.h diff --git a/doc/libcvc4.3_template.in b/doc/libcvc4.3_template.in index 2ff96eb5a..f85a909dd 100644 --- a/doc/libcvc4.3_template.in +++ b/doc/libcvc4.3_template.in @@ -22,7 +22,7 @@ int main() { Expr onePlusTwo = em.mkExpr(kind::PLUS, em.mkConst(Rational(1)), em.mkConst(Rational(2))); - std::cout << Expr::setlanguage(language::output::LANG_CVC4) + std::cout << language::SetLanguage(language::output::LANG_CVC4) << smt.getInfo("name") << " says that 1 + 2 = " << smt.simplify(onePlusTwo) diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 7390eefe0..68de230fe 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -18,6 +18,7 @@ //#include // use this after CVC4 is properly installed #include "smt/smt_engine.h" +#include "options/set_language.h" using namespace std; using namespace CVC4; @@ -34,8 +35,8 @@ int main() { smt.setOption("produce-models", true); // Set output language to SMTLIB2 - cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); - + cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); + Type integer = em.integerType(); Type set = em.mkSetType(integer); diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 14ab0e64d..2e5d467d3 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -18,6 +18,7 @@ //#include // use this after CVC4 is properly installed #include "smt/smt_engine.h" +#include "options/set_language.h" using namespace CVC4; @@ -35,8 +36,8 @@ int main() { smt.setOption("strings-exp", true); // Set output language to SMTLIB2 - std::cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); - + std::cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); + // String type Type string = em.stringType(); diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp index e23be29bf..9ed4424ba 100644 --- a/examples/hashsmt/sha1_collision.cpp +++ b/examples/hashsmt/sha1_collision.cpp @@ -22,16 +22,17 @@ * Author: dejan */ -#include +#include #include #include #include +#include -#include "word.h" +#include "options/language.h" +#include "options/set_language.h" #include "sha1.hpp" #include "smt_util/command.h" - -#include +#include "word.h" using namespace std; using namespace CVC4; @@ -69,7 +70,7 @@ int main(int argc, char* argv[]) { // The output ofstream output(argv[3]); - output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); + output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2); output << SetBenchmarkLogicCommand("QF_BV") << endl; output << SetBenchmarkStatusCommand(SMT_UNSATISFIABLE) << endl; @@ -103,6 +104,3 @@ int main(int argc, char* argv[]) { cerr << e << endl; } } - - - diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp index fadc6ecb9..15c7d8728 100644 --- a/examples/hashsmt/sha1_inversion.cpp +++ b/examples/hashsmt/sha1_inversion.cpp @@ -22,16 +22,17 @@ * Author: dejan */ -#include +#include #include #include #include +#include -#include "word.h" +#include "options/language.h" +#include "options/set_language.h" #include "sha1.hpp" #include "smt_util/command.h" - -#include +#include "word.h" using namespace std; using namespace CVC4; @@ -50,7 +51,7 @@ int main(int argc, char* argv[]) { string msg = argv[1]; unsigned msgSize = msg.size(); ofstream output(argv[2]); - output << expr::ExprSetDepth(-1) << expr::ExprSetLanguage(language::output::LANG_SMTLIB_V2); + output << expr::ExprSetDepth(-1) << language::SetLanguage(language::output::LANG_SMTLIB_V2); output << SetBenchmarkLogicCommand("QF_BV") << endl; output << SetBenchmarkStatusCommand(SMT_SATISFIABLE) << endl; @@ -58,7 +59,7 @@ int main(int argc, char* argv[]) { hashsmt::cvc4_uchar8 *cvc4input = new hashsmt::cvc4_uchar8[msgSize]; for (unsigned i = 0; i < msgSize; ++ i) { stringstream ss; - ss << "x" << i; + ss << "x" << i; cvc4input[i] = hashsmt::cvc4_uchar8(ss.str()); output << DeclareFunctionCommand(ss.str(), cvc4input[i].getExpr(), cvc4input[i].getExpr().getType()) << endl; @@ -102,6 +103,3 @@ int main(int argc, char* argv[]) { cerr << e << endl; } } - - - diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index d4aecbba9..db76390a7 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -23,7 +23,9 @@ #include #include "expr/expr.h" +#include "options/language.h" #include "options/options.h" +#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" @@ -35,18 +37,19 @@ using namespace CVC4::parser; using namespace CVC4::options; using namespace CVC4::theory; -int main(int argc, char* argv[]) +int main(int argc, char* argv[]) { - // Get the filename + // Get the filename string input(argv[1]); // Create the expression manager Options options; options.set(inputLanguage, language::input::LANG_SMTLIB_V2); ExprManager exprManager(options); - - cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << Expr::setdepth(-1); + + cout << language::SetLanguage(language::output::LANG_SMTLIB_V2) + << Expr::setdepth(-1); // Create the parser ParserBuilder parserBuilder(&exprManager, input, options); @@ -76,12 +79,11 @@ int main(int argc, char* argv[]) } cout << *cmd << endl; - delete cmd; + delete cmd; } cout << "(check-sat)" << endl; - + // Get rid of the parser delete parser; } - diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index c33ccb367..7e17e68f4 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -23,7 +23,9 @@ #include #include "expr/expr.h" +#include "options/language.h" #include "options/options.h" +#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt_util/command.h" @@ -34,7 +36,7 @@ using namespace CVC4; using namespace CVC4::parser; using namespace CVC4::options; -bool nonsense(char c) { return !isalnum(c); } +bool nonsense(char c) { return !isalnum(c); } #ifdef ENABLE_AXIOMS const bool enableAxioms = true; @@ -94,7 +96,7 @@ class Mapper { Type elementType = t.getElementType(); ostringstream oss_type; - oss_type << Expr::setlanguage(language::output::LANG_SMTLIB_V2) + oss_type << language::SetLanguage(language::output::LANG_SMTLIB_V2) << elementType; string elementTypeAsString = oss_type.str(); elementTypeAsString.erase( @@ -103,7 +105,7 @@ class Mapper { // define-sort ostringstream oss_name; - oss_name << Expr::setlanguage(language::output::LANG_SMTLIB_V2) + oss_name << language::SetLanguage(language::output::LANG_SMTLIB_V2) << "(Set " << elementType << ")"; string name = oss_name.str(); Type newt = em->mkArrayType(t.getElementType(), em->booleanType()); @@ -184,7 +186,8 @@ class Mapper { int N = sizeof(setaxioms) / sizeof(setaxioms[0]); for(int i = 0; i < N; ++i) { string s = setaxioms[i]; - ostringstream oss; oss << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << elementType; + ostringstream oss; + oss << language::SetLanguage(language::output::LANG_SMTLIB_V2) << elementType; boost::replace_all(s, "HOLDA", elementTypeAsString); boost::replace_all(s, "HOLDB", oss.str()); if( s == "" ) continue; @@ -207,7 +210,7 @@ class Mapper { public: Mapper(ExprManager* e) : em(e),depth(0) { - sout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + sout << language::SetLanguage(language::output::LANG_SMTLIB_V2); } void defineSetSort() { @@ -259,17 +262,17 @@ int main(int argc, char* argv[]) // Create the expression manager Options options; options.set(inputLanguage, language::input::LANG_SMTLIB_V2); - cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); // cout << Expr::dag(0); ExprManager exprManager(options); Mapper m(&exprManager); - + // Create the parser ParserBuilder parserBuilder(&exprManager, input, options); if(input == "") parserBuilder.withStreamInput(cin); Parser* parser = parserBuilder.build(); - + // Variables and assertions vector variables; vector info_tags; diff --git a/examples/translator.cpp b/examples/translator.cpp index 522d88573..7d5e912e7 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -24,6 +24,7 @@ #include "expr/expr.h" #include "options/language.h" +#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt/smt_engine.h" @@ -97,7 +98,7 @@ static void readFile(const char* filename, InputLanguage fromLang, OutputLanguag toLang = toOutputLanguage(fromLang); } - *out << Expr::setlanguage(toLang); + *out << language::SetLanguage(toLang); Options opts; opts.set(options::inputLanguage, fromLang); diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 35211a49a..d44bae7ee 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -29,6 +29,7 @@ #include "expr/sexpr.h" #include "options/expr_options.h" #include "options/parser_options.h" +#include "options/set_language.h" #include "options/smt_options.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -1521,7 +1522,7 @@ void ValidityChecker::printExpr(const Expr& e) { void ValidityChecker::printExpr(const Expr& e, std::ostream& os) { Expr::setdepth::Scope sd(os, -1); Expr::printtypes::Scope pt(os, false); - Expr::setlanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]); + CVC4::language::SetLanguage::Scope sl(os, d_em->getOptions()[CVC4::options::outputLanguage]); os << e; } diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index c758fe297..09fe2cdc3 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -27,6 +27,7 @@ #include "expr/node.h" #include "expr/node_manager.h" #include "expr/type.h" +#include "options/set_language.h" using namespace std; @@ -934,7 +935,7 @@ std::string DatatypeConstructorArg::getTypeName() const { // Unfortunately, in the case of complex selector types, we can // enter nontrivial recursion here. Make sure that doesn't happen. stringstream ss; - ss << Expr::setlanguage(language::output::LANG_CVC4); + ss << language::SetLanguage(language::output::LANG_CVC4); ss.iword(s_printDatatypeNamesOnly) = 1; t.toStream(ss); return ss.str(); @@ -961,7 +962,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { Debug("datatypes-output") << "printNameOnly is now " << printNameOnly << std::endl; // can only output datatypes in the CVC4 native language - Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); os << "DATATYPE " << dt.getName(); if(dt.isParametric()) { @@ -992,7 +993,7 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) { // can only output datatypes in the CVC4 native language - Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); os << ctor.getName(); @@ -1013,7 +1014,7 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructor& ctor) { std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) { // can only output datatypes in the CVC4 native language - Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); + language::SetLanguage::Scope ls(os, language::output::LANG_CVC4); os << arg.getName() << ": " << arg.getTypeName(); diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp index 69e34b848..a6e2c1ece 100644 --- a/src/expr/emptyset.cpp +++ b/src/expr/emptyset.cpp @@ -17,7 +17,10 @@ #include "expr/emptyset.h" -#include +#include + +#include "expr/expr.h" +#include "expr/type.h" namespace CVC4 { @@ -25,4 +28,59 @@ std::ostream& operator<<(std::ostream& out, const EmptySet& asa) { return out << "emptyset(" << asa.getType() << ')'; } +size_t EmptySetHashFunction::operator()(const EmptySet& es) const { + return TypeHashFunction()(es.getType()); +} + +/** + * Constructs an emptyset of the specified type. Note that the argument + * is the type of the set itself, NOT the type of the elements. + */ +EmptySet::EmptySet(const SetType& setType) + : d_type(new SetType(setType)) +{ } + +EmptySet::EmptySet(const EmptySet& es) + : d_type(new SetType(es.getType())) +{ } + +EmptySet& EmptySet::operator=(const EmptySet& es) { + (*d_type) = es.getType(); + return *this; +} + + +EmptySet::~EmptySet() throw() { + delete d_type; +} + +const SetType& EmptySet::getType() const { + return *d_type; +} + +bool EmptySet::operator==(const EmptySet& es) const throw() { + return getType() == es.getType(); +} + +bool EmptySet::operator!=(const EmptySet& es) const throw() { + return !(*this == es); +} + +bool EmptySet::operator<(const EmptySet& es) const throw() { + return getType() < es.getType(); +} + +bool EmptySet::operator<=(const EmptySet& es) const throw() { + return getType() <= es.getType(); +} + +bool EmptySet::operator>(const EmptySet& es) const throw() { + return !(*this <= es); +} + +bool EmptySet::operator>=(const EmptySet& es) const throw() { + return !(*this < es); +} + + }/* CVC4 namespace */ diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h index 4b3bb204f..e5eada731 100644 --- a/src/expr/emptyset.h +++ b/src/expr/emptyset.h @@ -19,65 +19,50 @@ #pragma once +#include + namespace CVC4 { // messy; Expr needs EmptySet (because it's the payload of a - // CONSTANT-kinded expression), and EmptySet needs Expr. - class CVC4_PUBLIC EmptySet; + // CONSTANT-kinded expression), EmptySet needs SetType, and + // SetType needs Expr. Using a forward declaration here in + // order to break the build cycle. + // Uses of SetType need to be as an incomplete type throughout + // this header. + class CVC4_PUBLIC SetType; }/* CVC4 namespace */ -#include "expr/expr.h" -#include "expr/type.h" -#include - namespace CVC4 { - class CVC4_PUBLIC EmptySet { - - const SetType d_type; - - EmptySet() { } public: - /** * Constructs an emptyset of the specified type. Note that the argument * is the type of the set itself, NOT the type of the elements. */ - EmptySet(SetType setType):d_type(setType) { } - - - ~EmptySet() throw() { - } + EmptySet(const SetType& setType); + ~EmptySet() throw(); + EmptySet(const EmptySet& other); + EmptySet& operator=(const EmptySet& other); - SetType getType() const { return d_type; } + const SetType& getType() const; + bool operator==(const EmptySet& es) const throw(); + bool operator!=(const EmptySet& es) const throw(); + bool operator<(const EmptySet& es) const throw(); + bool operator<=(const EmptySet& es) const throw(); + bool operator>(const EmptySet& es) const throw() ; + bool operator>=(const EmptySet& es) const throw(); - bool operator==(const EmptySet& es) const throw() { - return d_type == es.d_type; - } - bool operator!=(const EmptySet& es) const throw() { - return !(*this == es); - } +private: + /** Pointer to the SetType node. This is never NULL. */ + SetType* d_type; - bool operator<(const EmptySet& es) const throw() { - return d_type < es.d_type; - } - bool operator<=(const EmptySet& es) const throw() { - return d_type <= es.d_type; - } - bool operator>(const EmptySet& es) const throw() { - return !(*this <= es); - } - bool operator>=(const EmptySet& es) const throw() { - return !(*this < es); - } + EmptySet(); };/* class EmptySet */ std::ostream& operator<<(std::ostream& out, const EmptySet& es) CVC4_PUBLIC; struct CVC4_PUBLIC EmptySetHashFunction { - inline size_t operator()(const EmptySet& es) const { - return TypeHashFunction()(es.getType()); - } + size_t operator()(const EmptySet& es) const; };/* struct EmptySetHashFunction */ }/* CVC4 namespace */ diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 0739e3355..dbd7c049b 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -45,7 +45,6 @@ namespace expr { const int ExprSetDepth::s_iosIndex = std::ios_base::xalloc(); const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc(); const int ExprDag::s_iosIndex = std::ios_base::xalloc(); -const int ExprSetLanguage::s_iosIndex = std::ios_base::xalloc(); }/* CVC4::expr namespace */ diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index f609d8990..2e2f17742 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -80,7 +80,6 @@ namespace expr { class CVC4_PUBLIC ExprSetDepth; class CVC4_PUBLIC ExprPrintTypes; class CVC4_PUBLIC ExprDag; - class CVC4_PUBLIC ExprSetLanguage; class ExportPrivate; }/* CVC4::expr namespace */ @@ -549,11 +548,6 @@ public: */ typedef expr::ExprDag dag; - /** - * IOStream manipulator to set the output language for Exprs. - */ - typedef expr::ExprSetLanguage setlanguage; - /** * Very basic pretty printer for Expr. * This is equivalent to calling e.getNode().printAst(...) @@ -847,90 +841,6 @@ public: };/* class ExprDag::Scope */ };/* class ExprDag */ - -/** - * IOStream manipulator to set the output language for Exprs. - */ -class CVC4_PUBLIC ExprSetLanguage { - /** - * The allocated index in ios_base for our depth setting. - */ - static const int s_iosIndex; - - /** - * The default language to use, for ostreams that haven't yet had a - * setlanguage() applied to them and where the current Options - * information isn't available. - */ - static const int s_defaultOutputLanguage = language::output::LANG_AUTO; - - /** - * When this manipulator is used, the setting is stored here. - */ - OutputLanguage d_language; - -public: - /** - * Construct a ExprSetLanguage with the given setting. - */ - ExprSetLanguage(OutputLanguage l) : d_language(l) {} - - inline void applyLanguage(std::ostream& out) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = int(d_language) + 1; - } - - static inline OutputLanguage 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; - } - if(l <= 0 || l > language::output::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 OutputLanguage(l - 1); - } - - static inline void setLanguage(std::ostream& out, OutputLanguage l) { - // (offset by one to detect whether default has been set yet) - out.iword(s_iosIndex) = int(l) + 1; - } - - /** - * Set a language on the output stream for the current stack scope. - * This makes sure the old language is reset on the stream after - * normal OR exceptional exit from the scope, using the RAII C++ - * idiom. - */ - class Scope { - std::ostream& d_out; - OutputLanguage d_oldLanguage; - - public: - - inline Scope(std::ostream& out, OutputLanguage language) : - d_out(out), - d_oldLanguage(ExprSetLanguage::getLanguage(out)) { - ExprSetLanguage::setLanguage(out, language); - } - - inline ~Scope() { - ExprSetLanguage::setLanguage(d_out, d_oldLanguage); - } - - };/* class ExprSetLanguage::Scope */ - -};/* class ExprSetLanguage */ - }/* CVC4::expr namespace */ ${getConst_instantiations} @@ -981,20 +891,6 @@ inline std::ostream& operator<<(std::ostream& out, ExprDag d) { return out; } -/** - * Sets the output language when pretty-printing a Expr to an ostream. - * Use like this: - * - * // let out be an ostream, e an Expr - * out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl; - * - * The setting stays permanently (until set again) with the stream. - */ -inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) { - l.applyLanguage(out); - return out; -} - }/* CVC4::expr namespace */ inline size_t ExprHashFunction::operator()(CVC4::Expr e) const { diff --git a/src/expr/node.h b/src/expr/node.h index 384dbcc03..f345ba552 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -38,6 +38,7 @@ #include "expr/metakind.h" #include "expr/expr.h" #include "options/language.h" +#include "options/set_language.h" #include "util/configuration.h" #include "util/utility.h" #include "util/hash.h" @@ -864,7 +865,7 @@ public: /** * IOStream manipulator to set the output language for Exprs. */ - typedef expr::ExprSetLanguage setlanguage; + typedef language::SetLanguage setlanguage; /** * Very basic pretty printer for Node. diff --git a/src/expr/sexpr.cpp b/src/expr/sexpr.cpp index b8ffca5e5..0c0828616 100644 --- a/src/expr/sexpr.cpp +++ b/src/expr/sexpr.cpp @@ -30,6 +30,7 @@ #include "base/cvc4_assert.h" #include "expr/expr.h" +#include "options/set_language.h" #include "util/smt2_quote_string.h" @@ -42,13 +43,151 @@ std::ostream& operator<<(std::ostream& out, PrettySExprs ps) { return out; } + +SExpr::~SExpr() { + if(d_children != NULL){ + delete d_children; + d_children = NULL; + } + Assert(d_children == NULL); +} + +SExpr& SExpr::operator=(const SExpr& other) { + d_sexprType = other.d_sexprType; + d_integerValue = other.d_integerValue; + d_rationalValue = other.d_rationalValue; + d_stringValue = other.d_stringValue; + + if(d_children == NULL && other.d_children == NULL){ + // Do nothing. + } else if(d_children == NULL){ + d_children = new SExprVector(*other.d_children); + } else if(other.d_children == NULL){ + delete d_children; + d_children = NULL; + } else { + (*d_children) = other.getChildren(); + } + Assert( isAtom() == other.isAtom() ); + Assert( (d_children == NULL) == isAtom() ); + return *this; +} + +SExpr::SExpr() : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + + +SExpr::SExpr(const SExpr& other) : + d_sexprType(other.d_sexprType), + d_integerValue(other.d_integerValue), + d_rationalValue(other.d_rationalValue), + d_stringValue(other.d_stringValue), + d_children(NULL) +{ + d_children = (other.d_children == NULL) ? NULL : new SExprVector(*other.d_children); + // d_children being NULL is equivalent to the node being an atom. + Assert( (d_children == NULL) == isAtom() ); +} + + +SExpr::SExpr(const CVC4::Integer& value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { + } + +SExpr::SExpr(int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(unsigned int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(unsigned long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(const CVC4::Rational& value) : + d_sexprType(SEXPR_RATIONAL), + d_integerValue(0), + d_rationalValue(value), + d_stringValue(""), + d_children(NULL) { +} + +SExpr::SExpr(const std::string& value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) { +} + + /** + * This constructs a string expression from a const char* value. + * This cannot be removed in order to support SExpr("foo"). + * Given the other constructors this SExpr("foo") converts to bool. + * instead of SExpr(string("foo")). + */ +SExpr::SExpr(const char* value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children(NULL) { +} + #warning "TODO: Discuss this change with Clark." SExpr::SExpr(bool value) : d_sexprType(SEXPR_KEYWORD), d_integerValue(0), d_rationalValue(0), d_stringValue(value ? "true" : "false"), - d_children() { + d_children(NULL) { +} + +SExpr::SExpr(const Keyword& value) : + d_sexprType(SEXPR_KEYWORD), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value.getString()), + d_children(NULL) { +} + +SExpr::SExpr(const std::vector& children) : + d_sexprType(SEXPR_NOT_ATOM), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(""), + d_children(new SExprVector(children)) { } std::string SExpr::toString() const { @@ -57,13 +196,39 @@ std::string SExpr::toString() const { return ss.str(); } +/** Is this S-expression an atom? */ +bool SExpr::isAtom() const { + return d_sexprType != SEXPR_NOT_ATOM; +} + +/** Is this S-expression an integer? */ +bool SExpr::isInteger() const { + return d_sexprType == SEXPR_INTEGER; +} + +/** Is this S-expression a rational? */ +bool SExpr::isRational() const { + return d_sexprType == SEXPR_RATIONAL; +} + +/** Is this S-expression a string? */ +bool SExpr::isString() const { + return d_sexprType == SEXPR_STRING; +} + +/** Is this S-expression a keyword? */ +bool SExpr::isKeyword() const { + return d_sexprType == SEXPR_KEYWORD; +} + + std::ostream& operator<<(std::ostream& out, const SExpr& sexpr) { SExpr::toStream(out, sexpr); return out; } void SExpr::toStream(std::ostream& out, const SExpr& sexpr) throw() { - toStream(out, sexpr, Expr::setlanguage::getLanguage(out)); + toStream(out, sexpr, language::SetLanguage::getLanguage(out)); } void SExpr::toStream(std::ostream& out, const SExpr& sexpr, OutputLanguage language) throw() { @@ -181,15 +346,22 @@ const CVC4::Rational& SExpr::getRationalValue() const { const std::vector& SExpr::getChildren() const { CheckArgument( !isAtom(), this ); - return d_children; + Assert( d_children != NULL ); + return *d_children; } bool SExpr::operator==(const SExpr& s) const { - return d_sexprType == s.d_sexprType && - d_integerValue == s.d_integerValue && - d_rationalValue == s.d_rationalValue && - d_stringValue == s.d_stringValue && - d_children == s.d_children; + if (d_sexprType == s.d_sexprType && + d_integerValue == s.d_integerValue && + d_rationalValue == s.d_rationalValue && + d_stringValue == s.d_stringValue) { + if(d_children == NULL && s.d_children == NULL){ + return true; + } else if(d_children != NULL && s.d_children != NULL){ + return getChildren() == s.getChildren(); + } + } + return false; } bool SExpr::operator!=(const SExpr& s) const { diff --git a/src/expr/sexpr.h b/src/expr/sexpr.h index 158be0efb..40fd9dd56 100644 --- a/src/expr/sexpr.h +++ b/src/expr/sexpr.h @@ -27,7 +27,7 @@ #define __CVC4__SEXPR_H #include -#include +#include #include #include @@ -50,94 +50,25 @@ public: * string value, or a list of other S-expressions. */ class CVC4_PUBLIC SExpr { - - enum SExprTypes { - SEXPR_STRING, - SEXPR_KEYWORD, - SEXPR_INTEGER, - SEXPR_RATIONAL, - SEXPR_NOT_ATOM - } d_sexprType; - - /** The value of an atomic integer-valued S-expression. */ - CVC4::Integer d_integerValue; - - /** The value of an atomic rational-valued S-expression. */ - CVC4::Rational d_rationalValue; - - /** The value of an atomic S-expression. */ - std::string d_stringValue; - - /** The children of a list S-expression. */ - std::vector d_children; - public: typedef SExprKeyword Keyword; - SExpr() : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(); + SExpr(const SExpr&); + SExpr& operator=(const SExpr& other); + ~SExpr(); - SExpr(const CVC4::Integer& value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(const CVC4::Integer& value); - SExpr(int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(int value); + SExpr(long int value); + SExpr(unsigned int value); + SExpr(unsigned long int value); - SExpr(long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } + SExpr(const CVC4::Rational& value); - SExpr(unsigned int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } - - SExpr(unsigned long int value) : - d_sexprType(SEXPR_INTEGER), - d_integerValue(value), - d_rationalValue(0), - d_stringValue(""), - d_children() { - } - - SExpr(const CVC4::Rational& value) : - d_sexprType(SEXPR_RATIONAL), - d_integerValue(0), - d_rationalValue(value), - d_stringValue(""), - d_children() { - } - - SExpr(const std::string& value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children() { - } + SExpr(const std::string& value); /** * This constructs a string expression from a const char* value. @@ -145,60 +76,30 @@ public: * Given the other constructors this SExpr("foo") converts to bool. * instead of SExpr(string("foo")). */ - SExpr(const char* value) : - d_sexprType(SEXPR_STRING), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value), - d_children() { - } + SExpr(const char* value); /** * This adds a convenience wrapper to SExpr to cast from bools. * This is internally handled as the strings "true" and "false" */ SExpr(bool value); - - SExpr(const Keyword& value) : - d_sexprType(SEXPR_KEYWORD), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(value.getString()), - d_children() { - } - - SExpr(const std::vector& children) : - d_sexprType(SEXPR_NOT_ATOM), - d_integerValue(0), - d_rationalValue(0), - d_stringValue(""), - d_children(children) { - } + SExpr(const Keyword& value); + SExpr(const std::vector& children); /** Is this S-expression an atom? */ - bool isAtom() const { - return d_sexprType != SEXPR_NOT_ATOM; - } + bool isAtom() const; /** Is this S-expression an integer? */ - bool isInteger() const { - return d_sexprType == SEXPR_INTEGER; - } + bool isInteger() const; /** Is this S-expression a rational? */ - bool isRational() const { - return d_sexprType == SEXPR_RATIONAL; - } + bool isRational() const; /** Is this S-expression a string? */ - bool isString() const { - return d_sexprType == SEXPR_STRING; - } + bool isString() const; /** Is this S-expression a keyword? */ - bool isKeyword() const { - return d_sexprType == SEXPR_KEYWORD; - } + bool isKeyword() const; /** * This wraps the toStream() printer. @@ -261,7 +162,7 @@ public: /** * Outputs the SExpr onto the ostream out. This version reads defaults to the - * OutputLanguage, Expr::setlanguage::getLanguage(out). The indent level is + * OutputLanguage, language::SetLanguage::getLanguage(out). The indent level is * set to 2 if PrettySExprs::getPrettySExprs() is on and is 0 otherwise. */ static void toStream(std::ostream& out, const SExpr& sexpr) throw(); @@ -297,6 +198,34 @@ private: /** Returns true if this language quotes Keywords when printing. */ static bool languageQuotesKeywords(OutputLanguage language); + enum SExprTypes { + SEXPR_STRING, + SEXPR_KEYWORD, + SEXPR_INTEGER, + SEXPR_RATIONAL, + SEXPR_NOT_ATOM + } d_sexprType; + + /** The value of an atomic integer-valued S-expression. */ + CVC4::Integer d_integerValue; + + /** The value of an atomic rational-valued S-expression. */ + CVC4::Rational d_rationalValue; + + /** The value of an atomic S-expression. */ + std::string d_stringValue; + + typedef std::vector SExprVector; + + /** + * The children of a list S-expression. + * Whenever the SExpr isAtom() holds, this points at NULL. + * + * This should be a pointer in case the implementation of vector ever + * directly contained or allocated an SExpr. If this happened this would trigger, + * either the size being infinite or SExpr() being an infinite loop. + */ + SExprVector* d_children; };/* class SExpr */ /** Prints an SExpr. */ diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index bb6487bf0..a1f737d1d 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -34,6 +34,7 @@ #include "options/main_options.h" #include "options/options.h" #include "options/printer_options.h" +#include "options/set_language.h" #include "options/smt_options.h" #include "smt_util/command.h" @@ -143,7 +144,7 @@ void CommandExecutorPortfolio::lemmaSharingInit() // important even for muzzled builds (to get result output right) *d_threadOptions[i][options::out] - << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]); + << language::SetLanguage(d_threadOptions[i][options::outputLanguage]); } } }/* CommandExecutorPortfolio::lemmaSharingInit() */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index df78df0f3..7e82e1bd1 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -38,6 +38,7 @@ #include "options/main_options.h" #include "options/options.h" #include "options/quantifiers_options.h" +#include "options/set_language.h" #include "options/smt_options.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -231,7 +232,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { } // important even for muzzled builds (to get result output right) - *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]); + *opts[options::out] << language::SetLanguage(opts[options::outputLanguage]); // Create the expression manager using appropriate options ExprManager* exprMgr; @@ -283,7 +284,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { opts.set(options::replayStream, new Parser::ExprStream(replayParser)); } if( opts[options::replayLog] != NULL ) { - *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1); + *opts[options::replayLog] << language::SetLanguage(opts[options::outputLanguage]) << Expr::setdepth(-1); } int returnValue = 0; diff --git a/src/options/Makefile.am b/src/options/Makefile.am index d871bfb0a..cf38708e1 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -227,6 +227,8 @@ liboptions_la_SOURCES = \ printer_modes.h \ quantifiers_modes.cpp \ quantifiers_modes.h \ + set_language.cpp \ + set_language.h \ simplification_mode.cpp \ simplification_mode.h \ theoryof_mode.cpp \ diff --git a/src/options/language.h b/src/options/language.h index d400b4afb..9191a1d59 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -59,7 +59,7 @@ enum CVC4_PUBLIC Language { LANG_Z3STR, /** The SyGuS input language */ LANG_SYGUS, - + // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10 // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp new file mode 100644 index 000000000..db0275e04 --- /dev/null +++ b/src/options/set_language.cpp @@ -0,0 +1,81 @@ +/********************* */ +/*! \file language.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definition of input and output languages + ** + ** Definition of input and output languages. + **/ +#include "options/set_language.h" + +#include +#include + +#include "options/language.h" +#include "options/options.h" + +namespace CVC4 { +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::setLanguage(out, language); +} + +SetLanguage::Scope::~Scope(){ + SetLanguage::setLanguage(d_out, d_oldLanguage); +} + + +SetLanguage::SetLanguage(OutputLanguage 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) { + 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; + } + if(l <= 0 || l > language::output::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 OutputLanguage(l - 1); +} + +void SetLanguage::setLanguage(std::ostream& out, OutputLanguage l) { + // (offset by one to detect whether default has been set yet) + out.iword(s_iosIndex) = int(l) + 1; +} + +std::ostream& operator<<(std::ostream& out, SetLanguage l) { + l.applyLanguage(out); + return out; +} + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ diff --git a/src/options/set_language.h b/src/options/set_language.h new file mode 100644 index 000000000..53b0a6a63 --- /dev/null +++ b/src/options/set_language.h @@ -0,0 +1,99 @@ +/********************* */ +/*! \file language.h + ** \verbatim + ** Original author: Morgan Deters + ** Major contributors: none + ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Definition of input and output languages + ** + ** Definition of input and output languages. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__OPTIONS__SET_LANGUAGE_H +#define __CVC4__OPTIONS__SET_LANGUAGE_H + +#include +#include "options/language.h" + +namespace CVC4 { +namespace language { + +/** + * IOStream manipulator to set the output language for Exprs. + */ +class CVC4_PUBLIC SetLanguage { +public: + /** + * Set a language on the output stream for the current stack scope. + * This makes sure the old language is reset on the stream after + * normal OR exceptional exit from the scope, using the RAII C++ + * idiom. + */ + class Scope { + public: + Scope(std::ostream& out, OutputLanguage language); + ~Scope(); + private: + std::ostream& d_out; + OutputLanguage d_oldLanguage; + };/* class SetLanguage::Scope */ + + /** + * Construct a ExprSetLanguage with the given setting. + */ + SetLanguage(OutputLanguage l); + + void applyLanguage(std::ostream& out); + + static OutputLanguage getLanguage(std::ostream& out); + + static void setLanguage(std::ostream& out, OutputLanguage l); + +private: + + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default language to use, for ostreams that haven't yet had a + * setlanguage() applied to them and where the current Options + * information isn't available. + */ + static const int s_defaultOutputLanguage = language::output::LANG_AUTO; + + /** + * When this manipulator is used, the setting is stored here. + */ + OutputLanguage d_language; +};/* class SetLanguage */ + + +/** + * Sets the output language when pretty-printing a Expr to an ostream. + * This is used liek this: + * + * // let out be an ostream, e an Expr + * out << language::SetLanguage(LANG_SMTLIB_V2_5) << e << endl; + * + * This used to be used like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setlanguage(LANG_SMTLIB_V2_5) << e << endl; + * + * The setting stays permanently (until set again) with the stream. + */ +std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_PUBLIC; + +}/* CVC4::language namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__OPTIONS__SET_LANGUAGE_H */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index ff3753a67..efa51963a 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -434,7 +434,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, Expr e = createPrecedenceTree(parser, em, expressions, operators, 0, expressions.size() - 1); if(Debug.isOn("prec") && operators.size() > 1) { - Expr::setlanguage::Scope ls(Debug("prec"), language::output::LANG_AST); + language::SetLanguage::Scope ls(Debug("prec"), language::output::LANG_AST); Debug("prec") << "=> " << e << std::endl; } return e; @@ -487,6 +487,7 @@ Expr addNots(ExprManager* em, size_t n, Expr e) { #include #include +#include "options/set_language.h" #include "parser/antlr_tracing.h" #include "parser/parser.h" #include "smt_util/command.h" @@ -995,7 +996,7 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vectordefineVar(name, e); Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: " << name << std::endl diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 8ac1fa34c..7f639762a 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -111,6 +111,7 @@ namespace CVC4 { #include "expr/expr.h" #include "expr/kind.h" #include "expr/type.h" +#include "options/set_language.h" #include "parser/antlr_input.h" #include "parser/parser.h" #include "parser/smt2/smt2.h" @@ -1466,7 +1467,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } | builtinOp[k] { std::stringstream ss; - ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k); + ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k); sexpr = SExpr(ss.str()); } ; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index f93857796..ece4e9177 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -977,7 +977,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, static std::string quoteSymbol(TNode n) { #warning "check the old implementation. It seems off." std::stringstream ss; - ss << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5); + ss << language::SetLanguage(language::output::LANG_SMTLIB_V2_5); return CVC4::quoteSymbol(ss.str()); } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index f3724b432..1bd2b059b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -56,6 +56,7 @@ #include "options/printer_options.h" #include "options/prop_options.h" #include "options/quantifiers_options.h" +#include "options/set_language.h" #include "options/smt_options.h" #include "options/strings_options.h" #include "options/theory_options.h" @@ -1658,7 +1659,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) if(!options::outputLanguage.wasSetByUser() && options::outputLanguage() == language::output::LANG_SMTLIB_V2_5) { options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0); - *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_0); + *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0); } return; } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) || @@ -1667,7 +1668,7 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value) if(!options::outputLanguage.wasSetByUser() && options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) { options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5); - *options::out() << Expr::setlanguage(language::output::LANG_SMTLIB_V2_5); + *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5); } return; } @@ -1774,7 +1775,7 @@ void SmtEngine::defineFunction(Expr func, } stringstream ss; - ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream())) + ss << language::SetLanguage(language::SetLanguage::getLanguage(Dump.getStream())) << func; DefineFunctionCommand c(ss.str(), func, formals, formula); addToModelCommandAndDump(c, ExprManager::VAR_FLAG_DEFINED, true, "declarations"); diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp index 3dc5720ab..371cdcddd 100644 --- a/src/smt/smt_options_handler.cpp +++ b/src/smt/smt_options_handler.cpp @@ -45,6 +45,7 @@ #include "options/parser_options.h" #include "options/printer_modes.h" #include "options/quantifiers_modes.h" +#include "options/set_language.h" #include "options/simplification_mode.h" #include "options/smt_options.h" #include "options/theory_options.h" @@ -1216,12 +1217,12 @@ void SmtOptionsHandler::proofEnabledBuild(std::string option, bool value) throw( int dagSetting = expr::ExprDag::getDag(__channel_get); \ size_t exprDepthSetting = expr::ExprSetDepth::getDepth(__channel_get); \ bool printtypesSetting = expr::ExprPrintTypes::getPrintTypes(__channel_get); \ - OutputLanguage languageSetting = expr::ExprSetLanguage::getLanguage(__channel_get); \ + OutputLanguage languageSetting = language::SetLanguage::getLanguage(__channel_get); \ __channel_set; \ __channel_get << Expr::dag(dagSetting); \ __channel_get << Expr::setdepth(exprDepthSetting); \ __channel_get << Expr::printtypes(printtypesSetting); \ - __channel_get << Expr::setlanguage(languageSetting); \ + __channel_get << language::SetLanguage(languageSetting); \ } void SmtOptionsHandler::dumpToFile(std::string option, std::string optarg) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index f3bbc65cc..e6478440d 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -579,7 +579,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){ }else{ if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){ std::stringstream ss; - ss << Expr::setlanguage(options::outputLanguage()); + ss << language::SetLanguage(options::outputLanguage()); ss << "e_" << tn; mbt = NodeManager::currentNM()->mkSkolem( ss.str(), tn, "is a model basis term" ); Trace("mkVar") << "ModelBasis:: Make variable " << mbt << " : " << tn << std::endl; diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp index fd06517a9..dd6cbccb8 100644 --- a/test/system/ouroborous.cpp +++ b/test/system/ouroborous.cpp @@ -29,6 +29,7 @@ #include #include "expr/expr.h" +#include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" #include "smt_util/command.h" @@ -69,7 +70,7 @@ string translate(string in, InputLanguage inlang, OutputLanguage outlang) { psr->setInput(Input::newStringInput(inlang, in, "internal-buffer")); Expr e = psr->nextExpression(); stringstream ss; - ss << Expr::setlanguage(outlang) << Expr::setdepth(-1) << e; + ss << language::SetLanguage(outlang) << Expr::setdepth(-1) << e; assert(psr->nextExpression().isNull());// next expr should be null assert(psr->done());// parser should be done string s = ss.str(); diff --git a/test/system/smt2_compliance.cpp b/test/system/smt2_compliance.cpp index 108e30b5c..99b4c625c 100644 --- a/test/system/smt2_compliance.cpp +++ b/test/system/smt2_compliance.cpp @@ -19,6 +19,7 @@ #include #include "expr/expr_manager.h" +#include "options/set_language.h" #include "options/smt_options.h" #include "parser/parser.h" #include "parser/parser_builder.h" @@ -36,7 +37,7 @@ int main() { opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2); opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2); - cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2); + cout << language::SetLanguage(language::output::LANG_SMTLIB_V2); ExprManager em(opts); SmtEngine smt(&em); diff --git a/test/unit/util/boolean_simplification_black.h b/test/unit/util/boolean_simplification_black.h index ac343ede8..355d4ff37 100644 --- a/test/unit/util/boolean_simplification_black.h +++ b/test/unit/util/boolean_simplification_black.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "expr/node_manager.h" #include "options/language.h" +#include "options/set_language.h" #include "smt_util/boolean_simplification.h" using namespace CVC4; @@ -102,7 +103,7 @@ public: BooleanSimplification::DUPLICATE_REMOVAL_THRESHOLD); cout << Expr::setdepth(-1) - << Expr::setlanguage(language::output::LANG_CVC4); + << language::SetLanguage(language::output::LANG_CVC4); } void tearDown() { -- 2.30.2