diff options
Diffstat (limited to 'src/options')
-rw-r--r-- | src/options/CMakeLists.txt | 6 | ||||
-rw-r--r-- | src/options/datatypes_options.toml | 2 | ||||
-rw-r--r-- | src/options/language.h | 30 | ||||
-rw-r--r-- | src/options/mkoptions.py | 8 | ||||
-rw-r--r-- | src/options/open_ostream.cpp | 7 | ||||
-rw-r--r-- | src/options/open_ostream.h | 2 | ||||
-rw-r--r-- | src/options/option_exception.h | 4 | ||||
-rw-r--r-- | src/options/options.h | 4 | ||||
-rw-r--r-- | src/options/options_handler.cpp | 5 | ||||
-rw-r--r-- | src/options/options_template.cpp | 4 | ||||
-rw-r--r-- | src/options/set_language.h | 6 |
11 files changed, 39 insertions, 39 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 77c4d5a09..424f5e0df 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -16,7 +16,7 @@ # Check if the toml Python module is installed. check_python_module("toml") -libcvc4_add_sources( +libcvc5_add_sources( base_handlers.h decision_weight.h didyoumean.cpp @@ -66,7 +66,7 @@ set(options_toml_files string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files}) string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files}) -libcvc4_add_sources(GENERATED options.cpp ${options_gen_cpp_files}) +libcvc5_add_sources(GENERATED options.cpp ${options_gen_cpp_files}) list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files) @@ -88,7 +88,7 @@ add_custom_command( module_template.cpp options_holder_template.h options_template.cpp - ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc4.1_template + ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc5.1_template ${CMAKE_CURRENT_BINARY_DIR}/../../doc/SmtEngine.3cvc_template ${CMAKE_CURRENT_BINARY_DIR}/../../doc/options.3cvc_template ) diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index a43641c73..164dd736b 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -4,7 +4,7 @@ header = "options/datatypes_options.h" # How to handle selectors applied to incorrect constructors. If this option is set, # then we do not rewrite such a selector term to an arbitrary ground term. -# For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then +# For example, by default cvc5 considers cdr( nil ) = nil. If this option is set, then # cdr( nil ) has no set value. [[option]] name = "dtRewriteErrorSel" diff --git a/src/options/language.h b/src/options/language.h index 54e0e9dfa..04182cdd9 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -21,14 +21,14 @@ #include <ostream> #include <string> -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { namespace language { namespace input { -enum CVC4_EXPORT Language +enum CVC5_EXPORT Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 @@ -60,7 +60,7 @@ enum CVC4_EXPORT Language LANG_MAX }; /* enum Language */ -inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT; +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: @@ -84,7 +84,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { namespace output { -enum CVC4_EXPORT Language +enum CVC5_EXPORT Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 @@ -119,7 +119,7 @@ enum CVC4_EXPORT Language LANG_MAX }; /* enum Language */ -inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT; +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; @@ -147,24 +147,24 @@ typedef language::output::Language OutputLanguage; namespace language { /** Is the language a variant of the smtlib version 2 language? */ -bool isInputLang_smt2(InputLanguage lang) CVC4_EXPORT; -bool isOutputLang_smt2(OutputLanguage lang) CVC4_EXPORT; +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) CVC4_EXPORT; -bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_EXPORT; +bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC5_EXPORT; +bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC5_EXPORT; /** Is the language a variant of the SyGuS input language? */ -bool isInputLangSygus(InputLanguage lang) CVC4_EXPORT; -bool isOutputLangSygus(OutputLanguage lang) CVC4_EXPORT; +bool isInputLangSygus(InputLanguage lang) CVC5_EXPORT; +bool isOutputLangSygus(OutputLanguage lang) CVC5_EXPORT; -InputLanguage toInputLanguage(OutputLanguage language) CVC4_EXPORT; -OutputLanguage toOutputLanguage(InputLanguage language) CVC4_EXPORT; -InputLanguage toInputLanguage(std::string language) CVC4_EXPORT; -OutputLanguage toOutputLanguage(std::string language) CVC4_EXPORT; +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; } // namespace language } // namespace cvc5 diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 4fe93c129..c28a6f0cf 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -33,7 +33,7 @@ - module_template.h Directory <tpl-doc> must contain: - - cvc4.1_template + - cvc5.1_template - options.3cvc_template - SmtEngine.3cvc_template These files get generated during autogen.sh from the corresponding *.in @@ -49,7 +49,7 @@ - <dst>/MODULE_options.cpp - <dst>/options_holder.h - <dst>/options.cpp - - <tpl-doc>/cvc4.1 + - <tpl-doc>/cvc5.1 - <tpl-doc>/options.3 - <tpl-doc>/SmtEngine.3 """ @@ -1133,7 +1133,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, getoption_handlers='\n'.join(getoption_handlers) )) - write_file(doc_dir, 'cvc4.1', tpl_man_cvc.format( + write_file(doc_dir, 'cvc5.1', tpl_man_cvc.format( man_common='\n'.join(man_common), man_others='\n'.join(man_others) )) @@ -1330,7 +1330,7 @@ def mkoptions_main(): tpl_options_holder = read_tpl(src_dir, 'options_holder_template.h') # Read documentation template files from documentation directory. - tpl_man_cvc = read_tpl(doc_dir, 'cvc4.1_template') + tpl_man_cvc = read_tpl(doc_dir, 'cvc5.1_template') tpl_man_smt = read_tpl(doc_dir, 'SmtEngine.3cvc_template') tpl_man_int = read_tpl(doc_dir, 'options.3cvc_template') diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp index fa36738d9..3b13c42e2 100644 --- a/src/options/open_ostream.cpp +++ b/src/options/open_ostream.cpp @@ -60,15 +60,16 @@ std::pair< bool, std::ostream* > OstreamOpener::open(const std::string& optarg) std::ofstream::out | std::ofstream::trunc); if(outStream == NULL || !*outStream) { std::stringstream ss; - ss << "Cannot open " << d_channelName << " file: `" - << optarg << "': " << cvc4_errno_failreason(); + ss << "Cannot open " << d_channelName << " file: `" << optarg + << "': " << cvc5_errno_failreason(); throw OptionException(ss.str()); } return make_pair(true, outStream); } } -std::string cvc4_errno_failreason() { +std::string cvc5_errno_failreason() +{ #if HAVE_STRERROR_R #if STRERROR_R_CHAR_P if(errno != 0) { diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h index b135ef7ce..162bf3f11 100644 --- a/src/options/open_ostream.h +++ b/src/options/open_ostream.h @@ -54,7 +54,7 @@ class OstreamOpener { }; /* class OstreamOpener */ -std::string cvc4_errno_failreason(); +std::string cvc5_errno_failreason(); } // namespace cvc5 diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 4cfe55a31..f5590709e 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -19,7 +19,7 @@ #define CVC5__OPTION_EXCEPTION_H #include "base/exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { @@ -29,7 +29,7 @@ namespace cvc5 { * name is itself unrecognized, a UnrecognizedOptionException (a derived * class, below) should be used instead. */ -class CVC4_EXPORT OptionException : public cvc5::Exception +class CVC5_EXPORT OptionException : public cvc5::Exception { public: OptionException(const std::string& s) : cvc5::Exception(s_errPrefix + s) {} diff --git a/src/options/options.h b/src/options/options.h index 79b00de30..67707c990 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -25,7 +25,7 @@ #include "base/listener.h" #include "base/modal_exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/language.h" #include "options/option_exception.h" #include "options/printer_modes.h" @@ -42,7 +42,7 @@ namespace options { class OptionsListener; -class CVC4_EXPORT Options +class CVC5_EXPORT Options { friend api::Solver; /** The struct that holds all option values. */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 3c5616c73..0e2315aa0 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -15,15 +15,14 @@ #include "options/options_handler.h" +#include <cerrno> #include <ostream> #include <string> -#include <cerrno> - -#include "cvc4autoconfig.h" #include "base/check.h" #include "base/configuration.h" #include "base/configuration_private.h" +#include "base/cvc5config.h" #include "base/exception.h" #include "base/modal_exception.h" #include "base/output.h" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 91d06dec2..f24f83b2b 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -15,7 +15,7 @@ #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) // force use of optreset; mingw32 croaks on argv-switching otherwise -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #define _BSD_SOURCE #undef HAVE_DECL_OPTRESET #define HAVE_DECL_OPTRESET 1 @@ -58,7 +58,7 @@ extern int optreset; ${headers_module}$ #include "options/options_holder.h" -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #include "options/base_handlers.h" ${headers_handler}$ diff --git a/src/options/set_language.h b/src/options/set_language.h index 5ff7cdb7b..45add38ac 100644 --- a/src/options/set_language.h +++ b/src/options/set_language.h @@ -20,7 +20,7 @@ #include <iostream> -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/language.h" namespace cvc5 { @@ -29,7 +29,7 @@ namespace language { /** * IOStream manipulator to set the output language for Exprs. */ -class CVC4_EXPORT SetLanguage +class CVC5_EXPORT SetLanguage { public: /** @@ -87,7 +87,7 @@ private: * * The setting stays permanently (until set again) with the stream. */ -std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC5_EXPORT; } // namespace language } // namespace cvc5 |