diff options
52 files changed, 13 insertions, 1439 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 945f71d36..c535890e1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -121,7 +121,6 @@ cvc4_option(ENABLE_DEBUG_SYMBOLS "Enable debug symbols") cvc4_option(ENABLE_DUMPING "Enable dumping") cvc4_option(ENABLE_MUZZLE "Suppress ALL non-result output") cvc4_option(ENABLE_PROOFS "Enable proof support") -cvc4_option(ENABLE_REPLAY "Enable the replay feature") cvc4_option(ENABLE_STATISTICS "Enable statistics") cvc4_option(ENABLE_TRACING "Enable tracing") cvc4_option(ENABLE_UNIT_TESTING "Enable unit testing") @@ -429,10 +428,6 @@ if(ENABLE_PROOFS) add_definitions(-DCVC4_PROOF) endif() -if(ENABLE_REPLAY) - add_definitions(-DCVC4_REPLAY) -endif() - if(ENABLE_TRACING) add_definitions(-DCVC4_TRACING) endif() @@ -608,7 +603,6 @@ message("") print_config("Dumping :" ENABLE_DUMPING) print_config("Muzzle :" ENABLE_MUZZLE) print_config("Proofs :" ENABLE_PROOFS) -print_config("Replay :" ENABLE_REPLAY) print_config("Statistics :" ENABLE_STATISTICS) print_config("Tracing :" ENABLE_TRACING) message("") diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake index 6bd846d0c..e18d2b2f1 100644 --- a/cmake/ConfigCompetition.cmake +++ b/cmake/ConfigCompetition.cmake @@ -8,8 +8,6 @@ set(OPTIMIZATION_LEVEL 9) cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF) # enable_statistics=no cvc4_set_option(ENABLE_STATISTICS OFF) -# enable_replay=no -cvc4_set_option(ENABLE_REPLAY OFF) # enable_assertions=no cvc4_set_option(ENABLE_ASSERTIONS OFF) # enable_proof=no diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index 31b142ffc..1ee78a602 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -7,8 +7,6 @@ add_c_cxx_flag("-Og") cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON) # enable_statistics=yes cvc4_set_option(ENABLE_STATISTICS ON) -# enable_replay=yes -cvc4_set_option(ENABLE_REPLAY ON) # enable_assertions=yes cvc4_set_option(ENABLE_ASSERTIONS ON) # enable_proof=yes diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index 49e338abf..503f5d58f 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -4,8 +4,6 @@ set(OPTIMIZATION_LEVEL 3) cvc4_set_option(ENABLE_DEBUG_SYMBOLS OFF) # enable_statistics=yes cvc4_set_option(ENABLE_STATISTICS ON) -# enable_replay=no -cvc4_set_option(ENABLE_REPLAY OFF) # enable_assertions=no cvc4_set_option(ENABLE_ASSERTIONS OFF) # enable_proof=yes diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 40366495d..cdc9e3af8 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -4,8 +4,6 @@ set(OPTIMIZATION_LEVEL 2) cvc4_set_option(ENABLE_DEBUG_SYMBOLS ON) # enable_statistics=yes cvc4_set_option(ENABLE_STATISTICS ON) -# enable_replay=yes -cvc4_set_option(ENABLE_REPLAY ON) # enable_assertions=yes cvc4_set_option(ENABLE_ASSERTIONS ON) # enable_proof=yes diff --git a/configure.sh b/configure.sh index ae9b275aa..bd95e38ed 100755 --- a/configure.sh +++ b/configure.sh @@ -34,7 +34,6 @@ The following flags enable optional features (disable with --no-<option name>). --valgrind Valgrind instrumentation --debug-context-mm use the debug context memory manager --statistics include statistics - --replay turn on the replay feature --assertions turn on assertions --tracing include tracing code --dumping include dumping code @@ -130,7 +129,6 @@ lfsc=default muzzle=default optimized=default proofs=default -replay=default shared=default static_binary=default statistics=default @@ -248,9 +246,6 @@ do --proofs) proofs=ON;; --no-proofs) proofs=OFF;; - --replay) replay=ON;; - --no-replay) replay=OFF;; - --static) shared=OFF; static_binary=ON;; --no-static) shared=ON;; @@ -387,8 +382,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized" [ $proofs != default ] \ && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs" -[ $replay != default ] \ - && cmake_opts="$cmake_opts -DENABLE_REPLAY=$replay" [ $shared != default ] \ && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared" [ $static_binary != default ] \ diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 912df8b82..c1c8c15e0 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -427,14 +427,6 @@ libcvc4_add_sources( theory/fp/theory_fp_rewriter.h theory/fp/theory_fp_type_rules.h theory/fp/type_enumerator.h - theory/idl/idl_assertion.cpp - theory/idl/idl_assertion.h - theory/idl/idl_assertion_db.cpp - theory/idl/idl_assertion_db.h - theory/idl/idl_model.cpp - theory/idl/idl_model.h - theory/idl/theory_idl.cpp - theory/idl/theory_idl.h theory/interrupted.h theory/logic_info.cpp theory/logic_info.h @@ -769,8 +761,7 @@ set(KINDS_FILES ${PROJECT_SOURCE_DIR}/src/theory/sep/kinds ${PROJECT_SOURCE_DIR}/src/theory/sets/kinds ${PROJECT_SOURCE_DIR}/src/theory/strings/kinds - ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds - ${PROJECT_SOURCE_DIR}/src/theory/idl/kinds) + ${PROJECT_SOURCE_DIR}/src/theory/quantifiers/kinds) #-----------------------------------------------------------------------------# # Add subdirectories @@ -905,7 +896,6 @@ install(FILES expr/datatype.h expr/emptyset.h expr/expr_iomanip.h - expr/expr_stream.h expr/record.h expr/symbol_table.h expr/type.h diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index f907f212f..aed835f3f 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -50,10 +50,6 @@ bool Configuration::isStatisticsBuild() { return IS_STATISTICS_BUILD; } -bool Configuration::isReplayBuild() { - return IS_REPLAY_BUILD; -} - bool Configuration::isTracingBuild() { return IS_TRACING_BUILD; } diff --git a/src/base/configuration.h b/src/base/configuration.h index 60cdd5a9c..72ccb2301 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -47,8 +47,6 @@ public: static bool isStatisticsBuild(); - static bool isReplayBuild(); - static bool isTracingBuild(); static bool isDumpingBuild(); diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h index f3e76d53b..77db0b51c 100644 --- a/src/base/configuration_private.h +++ b/src/base/configuration_private.h @@ -36,12 +36,6 @@ namespace CVC4 { # define IS_STATISTICS_BUILD false #endif /* CVC4_STATISTICS_ON */ -#ifdef CVC4_REPLAY -# define IS_REPLAY_BUILD true -#else /* CVC4_REPLAY */ -# define IS_REPLAY_BUILD false -#endif /* CVC4_REPLAY */ - #ifdef CVC4_TRACING # define IS_TRACING_BUILD true #else /* CVC4_TRACING */ diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index c6034d0aa..c5abf9b27 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -65,7 +65,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java ${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java ${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java - ${CMAKE_CURRENT_BINARY_DIR}/ExprStream.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java diff --git a/src/cvc4.i b/src/cvc4.i index 42713ce40..01fd088a8 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -301,7 +301,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; // The remainder of the includes: %include "expr/expr.i" %include "expr/expr_manager.i" -%include "expr/expr_stream.i" %include "expr/variable_type_map.i" %include "options/option_exception.i" %include "options/options.i" diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 00bd121cb..a308e536c 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -12,7 +12,6 @@ libcvc4_add_sources( expr_iomanip.cpp expr_iomanip.h expr_manager_scope.h - expr_stream.h kind_map.h match_trie.cpp match_trie.h diff --git a/src/expr/expr_stream.h b/src/expr/expr_stream.h deleted file mode 100644 index d31e8e4fc..000000000 --- a/src/expr/expr_stream.h +++ /dev/null @@ -1,45 +0,0 @@ -/********************* */ -/*! \file expr_stream.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief A stream interface for expressions - ** - ** A stream interface for expressions. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__EXPR_STREAM_H -#define CVC4__EXPR_STREAM_H - -#include "expr/expr.h" - -namespace CVC4 { - -/** - * A pure-virtual stream interface for expressions. Can be used to - * communicate streams of expressions between different parts of CVC4. - */ -class CVC4_PUBLIC ExprStream { -public: - /** Virtual destructor; this implementation does nothing. */ - virtual ~ExprStream() {} - - /** - * Get the next expression in the stream (advancing the stream - * pointer as a side effect.) - */ - virtual Expr nextExpr() = 0; -};/* class ExprStream */ - -}/* CVC4 namespace */ - -#endif /* CVC4__EXPR_STREAM_H */ - diff --git a/src/expr/expr_stream.i b/src/expr/expr_stream.i deleted file mode 100644 index f1144623b..000000000 --- a/src/expr/expr_stream.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "expr/expr_stream.h" -%} - -%include "expr/expr_stream.h" diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index c4d35b7dc..fb1626adb 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -203,20 +203,6 @@ Kind operatorToKind(::CVC4::expr::NodeValue* nv); #line 205 "${template}" -namespace theory { - -static inline bool useTheoryValidate(std::string theory) { -${use_theory_validations} - return false; -} - -static const char *const useTheoryHelp = "\ -The following options are valid alternate implementations for use with\n\ -the --use-theory option:\n\ -\n\ -${theory_alternate_doc}"; - -}/* CVC4::theory namespace */ }/* CVC4 namespace */ #endif /* CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index fe8a152df..e2a733ec8 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -50,9 +50,6 @@ metakind_ubchildren= metakind_lbchildren= metakind_operatorKinds= -use_theory_validations= -theory_alternate_doc= - seen_theory=false seen_theory_builtin=false @@ -108,13 +105,6 @@ function alternate { theory_header="$4" theory_includes="${theory_includes}#include \"$theory_header\" " - - use_theory_validations="${use_theory_validations} - if(theory == \"$name\") { - return true; - }" - theory_alternate_doc="$theory_alternate_doc$name - alternate implementation for $theory_id\\n\\ -" } function properties { @@ -410,10 +400,6 @@ check_builtin_theory_seen nl -ba -s' ' "$template" | grep '^ *[0-9][0-9]* # *line' | awk '{OFS="";if($1+1!=$3) print "'"$template"':",$1,": warning: incorrect annotation \"#line ",$3,"\" (it should be \"#line ",($1+1),"\")"}' >&2 -if [ -z "$theory_alternate_doc" ]; then - theory_alternate_doc="[none defined]" -fi - text=$(cat "$template") for var in \ metakind_includes \ @@ -428,8 +414,6 @@ for var in \ metakind_ubchildren \ metakind_lbchildren \ metakind_operatorKinds \ - use_theory_validations \ - theory_alternate_doc \ template \ ; do eval text="\${text//\\\$\\{$var\\}/\${$var}}" diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp index 9db704621..323f24492 100644 --- a/src/main/command_executor.cpp +++ b/src/main/command_executor.cpp @@ -53,8 +53,7 @@ CommandExecutor::CommandExecutor(Options& options) d_smtEngine(d_solver->getSmtEngine()), d_options(options), d_stats("driver"), - d_result(), - d_replayStream(nullptr) + d_result() { } @@ -72,12 +71,6 @@ void CommandExecutor::safeFlushStatistics(int fd) const d_stats.safeFlushInformation(fd); } -void CommandExecutor::setReplayStream(ExprStream* replayStream) { - assert(d_replayStream == NULL); - d_replayStream = replayStream; - d_smtEngine->setReplayStream(d_replayStream); -} - bool CommandExecutor::doCommand(Command* cmd) { if( d_options.getParseOnly() ) { diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 3fc971f5b..a9b6d9077 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -44,17 +44,12 @@ class CommandExecutor Options& d_options; StatisticsRegistry d_stats; Result d_result; - ExprStream* d_replayStream; public: CommandExecutor(Options& options); virtual ~CommandExecutor() { - if (d_replayStream != NULL) - { - delete d_replayStream; - } } /** @@ -92,8 +87,6 @@ class CommandExecutor void flushOutputStreams(); - void setReplayStream(ExprStream* replayStream); - protected: /** Executes treating cmd as a singleton */ virtual bool doCommandSingleton(CVC4::Command* cmd); diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index be2d0a0f8..92368148b 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -184,23 +184,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { // Create the command executor to execute the parsed commands pExecutor = new CommandExecutor(opts); - std::unique_ptr<Parser> replayParser; - if (opts.getReplayInputFilename() != "") - { - std::string replayFilename = opts.getReplayInputFilename(); - ParserBuilder replayParserBuilder( - pExecutor->getSolver(), replayFilename, opts); - - if( replayFilename == "-") { - if( inputFromStdin ) { - throw OptionException("Replay file and input file can't both be stdin."); - } - replayParserBuilder.withStreamInput(cin); - } - replayParser.reset(replayParserBuilder.build()); - pExecutor->setReplayStream(new Parser::ExprStream(replayParser.get())); - } - int returnValue = 0; { // Timer statistic @@ -241,10 +224,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { << endl << endl; Message() << Configuration::copyright() << endl; } - if(replayParser) { - // have the replay parser use the declarations input interactively - replayParser->useDeclarationsFrom(shell.getParser()); - } while(true) { try { @@ -294,10 +273,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { vector< vector<Command*> > allCommands; allCommands.push_back(vector<Command*>()); std::unique_ptr<Parser> parser(parserBuilder.build()); - if(replayParser) { - // have the replay parser use the file's declarations - replayParser->useDeclarationsFrom(parser.get()); - } int needReset = 0; // true if one of the commands was interrupted bool interrupted = false; @@ -453,10 +428,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { } std::unique_ptr<Parser> parser(parserBuilder.build()); - if(replayParser) { - // have the replay parser use the file's declarations - replayParser->useDeclarationsFrom(parser.get()); - } bool interrupted = false; while (status) { diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 4fb331e50..4909d7d43 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -47,7 +47,6 @@ set(options_toml_files decision_options.toml expr_options.toml fp_options.toml - idl_options.toml main_options.toml parser_options.toml printer_options.toml diff --git a/src/options/idl_options.toml b/src/options/idl_options.toml deleted file mode 100644 index d3bee7018..000000000 --- a/src/options/idl_options.toml +++ /dev/null @@ -1,11 +0,0 @@ -id = "IDL" -name = "Idl" -header = "options/idl_options.h" - -[[option]] - name = "idlRewriteEq" - category = "regular" - long = "idl-rewrite-equalities" - type = "bool" - default = "false" - help = "enable rewriting equalities into two inequalities in IDL solver (default is disabled)" diff --git a/src/options/options.h b/src/options/options.h index ad2729205..3d1e67aba 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -67,9 +67,6 @@ class CVC4_PUBLIC Options { /** Listeners for options::tlimit-per. */ ListenerCollection d_rlimitPerListeners; - /** Listeners for options::useTheoryList. */ - ListenerCollection d_useTheoryListListeners; - /** Listeners for options::defaultExprDepth. */ ListenerCollection d_setDefaultExprDepthListeners; @@ -94,10 +91,6 @@ class CVC4_PUBLIC Options { /** Listeners for options::diagnosticChannelName. */ ListenerCollection d_setDiagnosticChannelListeners; - /** Listeners for options::replayFilename. */ - ListenerCollection d_setReplayFilenameListeners; - - static ListenerCollection::Registration* registerAndNotify( ListenerCollection& collection, Listener* listener, bool notify); @@ -231,7 +224,6 @@ public: std::ostream* getOut(); std::ostream* getOutConst() const; // TODO: Remove this. std::string getBinaryName() const; - std::string getReplayInputFilename() const; unsigned getParseStep() const; // TODO: Document these. @@ -382,19 +374,6 @@ public: Listener* listener, bool notifyIfSet); /** - * Registers a listener for options::useTheoryList being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerUseTheoryListListener( - Listener* listener, bool notifyIfSet); - - - /** * Registers a listener for options::defaultExprDepth being set. * * If notifyIfSet is true, this calls notify on the listener @@ -490,18 +469,6 @@ public: ListenerCollection::Registration* registerSetDiagnosticOutputChannelListener( Listener* listener, bool notifyIfSet); - /** - * Registers a listener for options::replayLogFilename being set. - * - * If notifyIfSet is true, this calls notify on the listener - * if the option was set by the user. - * - * The memory for the Registration is controlled by the user and must - * be destroyed before the Options object is. - */ - ListenerCollection::Registration* registerSetReplayLogFilename( - Listener* listener, bool notifyIfSet); - /** Sends a std::flush to getErr(). */ void flushErr(); diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 3e6c4da3c..7fcc8f2ae 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -244,20 +244,6 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg) } } -// theory/options_handlers.h -std::string OptionsHandler::handleUseTheoryList(std::string option, std::string optarg) { - std::string currentList = options::useTheoryList(); - if(currentList.empty()){ - return optarg; - } else { - return currentList +','+ optarg; - } -} - -void OptionsHandler::notifyUseTheoryList(std::string option) { - d_options->d_useTheoryListListeners.notify(); -} - // printer/options_handlers.h const std::string OptionsHandler::s_instFormatHelp = "\ Inst format modes currently supported by the --inst-format option:\n\ @@ -340,23 +326,6 @@ void OptionsHandler::notifySetDiagnosticOutputChannel(std::string option) { d_options->d_setDiagnosticChannelListeners.notify(); } - -std::string OptionsHandler::checkReplayFilename(std::string option, std::string optarg) { -#ifdef CVC4_REPLAY - if(optarg == "") { - throw OptionException (std::string("Bad file name for --replay")); - } else { - return optarg; - } -#else /* CVC4_REPLAY */ - throw OptionException("The replay feature was disabled in this build of CVC4."); -#endif /* CVC4_REPLAY */ -} - -void OptionsHandler::notifySetReplayLogFilename(std::string option) { - d_options->d_setReplayFilenameListeners.notify(); -} - void OptionsHandler::statsEnabledBuild(std::string option, bool value) { #ifndef CVC4_STATISTICS_ON @@ -453,7 +422,6 @@ void OptionsHandler::showConfiguration(std::string option) { print_config_cond("debug code", Configuration::isDebugBuild()); print_config_cond("statistics", Configuration::isStatisticsBuild()); - print_config_cond("replay", Configuration::isReplayBuild()); print_config_cond("tracing", Configuration::isTracingBuild()); print_config_cond("dumping", Configuration::isDumpingBuild()); print_config_cond("muzzled", Configuration::isMuzzledBuild()); diff --git a/src/options/options_handler.h b/src/options/options_handler.h index a395bb453..396b2c8ea 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -74,10 +74,6 @@ public: void setBitblastAig(std::string option, bool arg); - // theory/options_handlers.h - void notifyUseTheoryList(std::string option); - std::string handleUseTheoryList(std::string option, std::string optarg); - // printer/options_handlers.h InstFormatMode stringToInstFormatMode(std::string option, std::string optarg); @@ -96,8 +92,6 @@ public: void notifyDumpToFile(std::string option); void notifySetRegularOutputChannel(std::string option); void notifySetDiagnosticOutputChannel(std::string option); - std::string checkReplayFilename(std::string option, std::string optarg); - void notifySetReplayLogFilename(std::string option); void statsEnabledBuild(std::string option, bool value); diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index d1022c51c..bae60a374 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -187,10 +187,6 @@ std::string Options::getBinaryName() const{ return (*this)[options::binary_name]; } -std::string Options::getReplayInputFilename() const{ - return (*this)[options::replayInputFilename]; -} - unsigned Options::getParseStep() const{ return (*this)[options::parseStep]; } diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index dad4f13a1..48b6a66dd 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -317,13 +317,6 @@ ListenerCollection::Registration* Options::registerRlimitPerListener( return registerAndNotify(d_rlimitPerListeners, listener, notify); } -ListenerCollection::Registration* Options::registerUseTheoryListListener( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::useTheoryList); - return registerAndNotify(d_useTheoryListListeners, listener, notify); -} - ListenerCollection::Registration* Options::registerSetDefaultExprDepthListener( Listener* listener, bool notifyIfSet) { @@ -382,14 +375,6 @@ Options::registerSetDiagnosticOutputChannelListener( return registerAndNotify(d_setDiagnosticChannelListeners, listener, notify); } -ListenerCollection::Registration* -Options::registerSetReplayLogFilename( - Listener* listener, bool notifyIfSet) -{ - bool notify = notifyIfSet && wasSetByUser(options::replayLogFilename); - return registerAndNotify(d_setReplayFilenameListeners, listener, notify); -} - ${custom_handlers}$ diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 67829ede8..c813e1900 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -626,27 +626,6 @@ header = "options/smt_options.h" read_only = true help = "amount of resources spent for each sat conflict (bitvectors)" -# --replay is currently broken; don't document it for 1.0 -[[option]] - name = "replayInputFilename" - category = "undocumented" - long = "replay=FILE" - type = "std::string" - handler = "checkReplayFilename" - read_only = true - help = "replay decisions from file" - -# --replay is currently broken; don't document it for 1.0 -[[option]] - name = "replayLogFilename" - category = "undocumented" - long = "replay-log=FILE" - type = "std::string" - handler = "checkReplayFilename" - notifies = ["notifySetReplayLogFilename", "notifyBeforeSearch"] - read_only = true - help = "replay decisions from file" - [[option]] name = "forceNoLimitCpuWhileDump" category = "regular" diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 13c3d5cfb..84c994c3f 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -19,17 +19,6 @@ header = "options/theory_options.h" help = "Type variables as uninterpreted, type constants by theory, equalities by the parametric theory." [[option]] - name = "useTheoryList" - smt_name = "use-theory" - category = "regular" - long = "use-theory=NAME" - type = "std::string" - handler = "handleUseTheoryList" - notifies = ["notifyUseTheoryList"] - read_only = true - help = "use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list." - -[[option]] name = "assignFunctionValues" category = "regular" long = "assign-function-values" diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 7b3e1c4de..32604d03f 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1324,8 +1324,6 @@ restrictedTypePossiblyFunctionLHS[CVC4::api::Sort& t, * declared in the outer context. What follows isn't quite right, * though, since type aliases and function definitions should be * retained in the set of current declarations. */ - { /*symtab = PARSER_STATE->getSymbolTable(); - PARSER_STATE->useDeclarationsFrom(new SymbolTable());*/ } formula[f] ( COMMA formula[f2] )? RPAREN { PARSER_STATE->unimplementedFeature("predicate subtyping not supported in this release"); diff --git a/src/parser/parser.h b/src/parser/parser.h index 72e175a58..cd4105cd0 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -26,7 +26,6 @@ #include "api/cvc4cpp.h" #include "expr/expr.h" -#include "expr/expr_stream.h" #include "expr/kind.h" #include "expr/symbol_table.h" #include "parser/input.h" @@ -806,63 +805,9 @@ public: d_globalDeclarations = flag; } - /** - * Set the current symbol table used by this parser. - * From now on, this parser will perform its definitions and - * lookups in the declaration scope of the "parser" argument - * (but doesn't re-delegate if the other parser's declaration scope - * changes later). A NULL argument restores this parser's - * "primordial" declaration scope assigned at its creation. Calling - * p->useDeclarationsFrom(p) is a no-op. - * - * This feature is useful when e.g. reading out-of-band expression data: - * 1. Parsing --replay log files produced with --replay-log. - * 2. Perhaps a multi-query benchmark file is being single-stepped - * with intervening queries on stdin that must reference the same - * declaration scope(s). - * - * However, the feature must be used carefully. Pushes and pops - * should be performed with the correct current declaration scope. - * Care must be taken to match up declaration scopes, of course; - * If variables in the deferred-to parser go out of scope, the - * secondary parser will give errors that they are undeclared. - * Also, an outer-scope variable shadowed by an inner-scope one of - * the same name may be temporarily inaccessible. - * - * In short, caveat emptor. - */ - inline void useDeclarationsFrom(Parser* parser) { - if(parser == NULL) { - d_symtab = &d_symtabAllocated; - } else { - d_symtab = parser->d_symtab; - } - } - - inline void useDeclarationsFrom(SymbolTable* symtab) { - d_symtab = symtab; - } - inline SymbolTable* getSymbolTable() const { return d_symtab; } - - /** - * An expression stream interface for a parser. This stream simply - * pulls expressions from the given Parser object. - * - * Here, the ExprStream base class allows a Parser (from the parser - * library) and core components of CVC4 (in the core library) to - * communicate without polluting the public interface or having them - * reach into private (undocumented) interfaces. - */ - class ExprStream : public CVC4::ExprStream { - Parser* d_parser; - public: - ExprStream(Parser* parser) : d_parser(parser) {} - ~ExprStream() { delete d_parser; } - Expr nextExpr() override { return d_parser->nextExpression().getExpr(); } - };/* class Parser::ExprStream */ //------------------------ operator overloading /** is this function overloaded? */ diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 80cce599f..f56f6a447 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -662,15 +662,6 @@ Lit Solver::pickBranchLit() { Lit nextLit; -#ifdef CVC4_REPLAY - - nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextReplayDecision()); - - if (nextLit != lit_Undef) { - return nextLit; - } -#endif /* CVC4_REPLAY */ - // Theory requests nextLit = MinisatSatSolver::toMinisatLit(d_proxy->getNextTheoryDecisionRequest()); @@ -1547,10 +1538,6 @@ lbool Solver::search(int nof_conflicts) check_type = CHECK_FINAL; continue; } - -#ifdef CVC4_REPLAY - d_proxy->logDecision(MinisatSatSolver::toSatLiteral(next)); -#endif /* CVC4_REPLAY */ } // Increase decision level and enqueue 'next' diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2436aed04..89b919109 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -44,13 +44,6 @@ using namespace std; using namespace CVC4::context; - -#ifdef CVC4_REPLAY -# define CVC4_USE_REPLAY true -#else /* CVC4_REPLAY */ -# define CVC4_USE_REPLAY false -#endif /* CVC4_REPLAY */ - namespace CVC4 { namespace prop { @@ -76,9 +69,7 @@ public: PropEngine::PropEngine(TheoryEngine* te, Context* satContext, - UserContext* userContext, - std::ostream* replayLog, - ExprStream* replayStream) + UserContext* userContext) : d_inCheckSat(false), d_theoryEngine(te), d_context(satContext), @@ -101,13 +92,8 @@ PropEngine::PropEngine(TheoryEngine* te, d_cnfStream = new CVC4::prop::TseitinCnfStream( d_satSolver, d_registrar, userContext, true); - d_theoryProxy = new TheoryProxy(this, - d_theoryEngine, - d_decisionEngine.get(), - d_context, - d_cnfStream, - replayLog, - replayStream); + d_theoryProxy = new TheoryProxy( + this, d_theoryEngine, d_decisionEngine.get(), d_context, d_cnfStream); d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 707244ff5..f1d73fc92 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -24,7 +24,6 @@ #include <sys/time.h> #include "base/modal_exception.h" -#include "expr/expr_stream.h" #include "expr/node.h" #include "options/options.h" #include "preprocessing/assertion_pipeline.h" @@ -62,9 +61,7 @@ class PropEngine */ PropEngine(TheoryEngine*, context::Context* satContext, - context::UserContext* userContext, - std::ostream* replayLog, - ExprStream* replayStream); + context::UserContext* userContext); /** * Destructor. diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 557dcc413..38c99f551 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -18,7 +18,6 @@ #include "context/context.h" #include "decision/decision_engine.h" -#include "expr/expr_stream.h" #include "options/decision_options.h" #include "prop/cnf_stream.h" #include "prop/prop_engine.h" @@ -37,24 +36,17 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream, - std::ostream* replayLog, - ExprStream* replayStream) + CnfStream* cnfStream) : d_propEngine(propEngine), d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_replayLog(replayLog), - d_replayStream(replayStream), - d_queue(context), - d_replayedDecisions("prop::theoryproxy::replayedDecisions", 0) + d_queue(context) { - smtStatisticsRegistry()->registerStat(&d_replayedDecisions); } TheoryProxy::~TheoryProxy() { /* nothing to do for now */ - smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions); } void TheoryProxy::variableNotify(SatVariable var) { @@ -150,29 +142,6 @@ void TheoryProxy::notifyRestart() { d_theoryEngine->notifyRestart(); } -SatLiteral TheoryProxy::getNextReplayDecision() { -#ifdef CVC4_REPLAY - if(d_replayStream != NULL) { - Expr e = d_replayStream->nextExpr(); - if(!e.isNull()) { // we get null node when out of decisions to replay - // convert & return - ++d_replayedDecisions; - return d_cnfStream->getLiteral(e); - } - } -#endif /* CVC4_REPLAY */ - return undefSatLiteral; -} - -void TheoryProxy::logDecision(SatLiteral lit) { -#ifdef CVC4_REPLAY - if(d_replayLog != NULL) { - Assert(lit != undefSatLiteral) << "logging an `undef' decision ?!"; - (*d_replayLog) << d_cnfStream->getNode(lit) << std::endl; - } -#endif /* CVC4_REPLAY */ -} - void TheoryProxy::spendResource(ResourceManager::Resource r) { d_theoryEngine->spendResource(r); diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 0d76b473f..089d2082d 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -27,7 +27,6 @@ #include <unordered_set> #include "context/cdqueue.h" -#include "expr/expr_stream.h" #include "expr/node.h" #include "prop/sat_solver.h" #include "theory/theory.h" @@ -54,9 +53,7 @@ class TheoryProxy TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, - CnfStream* cnfStream, - std::ostream* replayLog, - ExprStream* replayStream); + CnfStream* cnfStream); ~TheoryProxy(); @@ -83,10 +80,6 @@ class TheoryProxy void notifyRestart(); - SatLiteral getNextReplayDecision(); - - void logDecision(SatLiteral lit); - void spendResource(ResourceManager::Resource r); bool isDecisionEngineDone(); @@ -111,12 +104,6 @@ class TheoryProxy /** The theory engine we are using. */ TheoryEngine* d_theoryEngine; - /** Stream on which to log replay events. */ - std::ostream* d_replayLog; - - /** Stream for replaying decisions. */ - ExprStream* d_replayStream; - /** Queue of asserted facts */ context::CDQueue<TNode> d_queue; @@ -126,11 +113,6 @@ class TheoryProxy */ std::unordered_set<Node, NodeHashFunction> d_shared; - /** - * Statistic: the number of replayed decisions (via --replay). - */ - IntStat d_replayedDecisions; - }; /* class SatSolver */ }/* CVC4::prop namespace */ diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp index a73ec44f4..7615325b7 100644 --- a/src/smt/managed_ostreams.cpp +++ b/src/smt/managed_ostreams.cpp @@ -163,31 +163,4 @@ void ManagedDiagnosticOutputChannel::addSpecialCases(OstreamOpener* opener) opener->addSpecialCase("stderr", &std::cerr); } - -ManagedReplayLogOstream::ManagedReplayLogOstream() : d_replayLog(NULL) {} -ManagedReplayLogOstream::~ManagedReplayLogOstream(){ - if(d_replayLog != NULL) { - (*d_replayLog) << std::flush; - } -} - -std::string ManagedReplayLogOstream::defaultSource() const { - return options::replayLogFilename(); -} - -void ManagedReplayLogOstream::initialize(std::ostream* outStream) { - if(outStream != NULL){ - *outStream << language::SetLanguage(options::outputLanguage()) - << expr::ExprSetDepth(-1); - } - /* Do this regardless of managing the memory. */ - d_replayLog = outStream; -} - -/** Adds special cases to an ostreamopener. */ -void ManagedReplayLogOstream::addSpecialCases(OstreamOpener* opener) const { - opener->addSpecialCase("-", &std::cout); -} - - }/* CVC4 namespace */ diff --git a/src/smt/managed_ostreams.h b/src/smt/managed_ostreams.h index f495f8e72..bc12bbe39 100644 --- a/src/smt/managed_ostreams.h +++ b/src/smt/managed_ostreams.h @@ -156,27 +156,6 @@ class ManagedDiagnosticOutputChannel : public ManagedOstream { void addSpecialCases(OstreamOpener* opener) const override; };/* class ManagedRegularOutputChannel */ -/** This controls the memory associated with replay-log. */ -class ManagedReplayLogOstream : public ManagedOstream { - public: - ManagedReplayLogOstream(); - ~ManagedReplayLogOstream(); - - std::ostream* getReplayLog() const { return d_replayLog; } - const char* getName() const override { return "replay-log"; } - std::string defaultSource() const override; - - protected: - /** Initializes an output stream. Not necessarily managed. */ - void initialize(std::ostream* outStream) override; - - /** Adds special cases to an ostreamopener. */ - void addSpecialCases(OstreamOpener* opener) const override; - - private: - std::ostream* d_replayLog; -};/* class ManagedRegularOutputChannel */ - }/* CVC4 namespace */ #endif /* CVC4__MANAGED_OSTREAMS_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 30c1cd0f5..10fc76bf7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -294,40 +294,6 @@ class BeforeSearchListener : public Listener { SmtEngine* d_smt; }; /* class BeforeSearchListener */ -class UseTheoryListListener : public Listener { - public: - UseTheoryListListener(TheoryEngine* theoryEngine) - : d_theoryEngine(theoryEngine) - {} - - void notify() override - { - std::stringstream commaList(options::useTheoryList()); - std::string token; - - Debug("UseTheoryListListener") << "UseTheoryListListener::notify() " - << options::useTheoryList() << std::endl; - - while(std::getline(commaList, token, ',')){ - if(token == "help") { - puts(theory::useTheoryHelp); - exit(1); - } - if(theory::useTheoryValidate(token)) { - d_theoryEngine->enableTheoryAlternative(token); - } else { - throw OptionException( - std::string("unknown option for --use-theory : `") + token + - "'. Try --use-theory=help."); - } - } - } - - private: - TheoryEngine* d_theoryEngine; -}; /* class UseTheoryListListener */ - - class SetDefaultExprDepthListener : public Listener { public: void notify() override @@ -433,15 +399,11 @@ class SmtEnginePrivate : public NodeManagerListener { /** Manager for the memory of --dump-to. */ ManagedDumpOStream d_managedDumpChannel; - /** Manager for --replay-log. */ - ManagedReplayLogOstream d_managedReplayLog; - /** * This list contains: * softResourceOut * hardResourceOut * beforeSearchListener - * UseTheoryListListener * * This needs to be deleted before both NodeManager's Options, * SmtEngine, d_resourceManager, and TheoryEngine. @@ -554,7 +516,6 @@ class SmtEnginePrivate : public NodeManagerListener { d_managedRegularChannel(), d_managedDiagnosticChannel(), d_managedDumpChannel(), - d_managedReplayLog(), d_listenerRegistrations(new ListenerRegistrationList()), d_propagator(true, true), d_assertions(), @@ -618,9 +579,6 @@ class SmtEnginePrivate : public NodeManagerListener { d_listenerRegistrations->add( nodeManagerOptions.registerDumpToFileNameListener( new SetToDefaultSourceListener(&d_managedDumpChannel), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetReplayLogFilename( - new SetToDefaultSourceListener(&d_managedReplayLog), true)); } catch (OptionException& e) { @@ -814,17 +772,6 @@ class SmtEnginePrivate : public NodeManagerListener { return retval; } - void addUseTheoryListListener(TheoryEngine* theoryEngine){ - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - d_listenerRegistrations->add( - nodeManagerOptions.registerUseTheoryListListener( - new UseTheoryListListener(theoryEngine), true)); - } - - std::ostream* getReplayLog() const { - return d_managedReplayLog.getReplayLog(); - } - //------------------------------- expression names // implements setExpressionName, as described in smt_engine.h void setExpressionName(Expr e, std::string name) { @@ -874,7 +821,6 @@ SmtEngine::SmtEngine(ExprManager* em) d_status(), d_expectedStatus(), d_smtMode(SMT_MODE_START), - d_replayStream(nullptr), d_private(nullptr), d_statisticsRegistry(nullptr), d_stats(nullptr) @@ -923,8 +869,6 @@ void SmtEngine::finishInit() #endif } - d_private->addUseTheoryListListener(getTheoryEngine()); - // set the random seed Random::getRandom().setSeed(options::seed()); @@ -938,11 +882,8 @@ void SmtEngine::finishInit() * are unregistered by the obsolete PropEngine object before registered * again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(getTheoryEngine(), - getContext(), - getUserContext(), - d_private->getReplayLog(), - d_replayStream)); + d_propEngine.reset( + new PropEngine(getTheoryEngine(), getContext(), getUserContext())); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(getPropEngine()); @@ -4337,11 +4278,8 @@ void SmtEngine::resetAssertions() * statistics are unregistered by the obsolete PropEngine object before * registered again by the new PropEngine object */ d_propEngine.reset(nullptr); - d_propEngine.reset(new PropEngine(getTheoryEngine(), - getContext(), - getUserContext(), - d_private->getReplayLog(), - d_replayStream)); + d_propEngine.reset( + new PropEngine(getTheoryEngine(), getContext(), getUserContext())); d_theoryEngine->setPropEngine(getPropEngine()); } @@ -4534,12 +4472,6 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const return SExpr::parseAtom(nodeManagerOptions.getOption(key)); } -void SmtEngine::setReplayStream(ExprStream* replayStream) { - AlwaysAssert(!d_fullyInited) - << "Cannot set replay stream once fully initialized"; - d_replayStream = replayStream; -} - bool SmtEngine::getExpressionName(Expr e, std::string& name) const { return d_private->getExpressionName(e, name); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index f5abda1b0..2cb227fc9 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -28,7 +28,6 @@ #include "context/cdlist_forward.h" #include "expr/expr.h" #include "expr/expr_manager.h" -#include "expr/expr_stream.h" #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" @@ -800,13 +799,6 @@ class CVC4_PUBLIC SmtEngine void beforeSearch(); /** - * Expermintal feature: Sets the sequence of decisions. - * This currently requires very fine grained knowledge about literal - * translation. - */ - void setReplayStream(ExprStream* exprStream); - - /** * Get expression name. * * Return true if given expressoion has a name in the current context. @@ -1243,9 +1235,6 @@ class CVC4_PUBLIC SmtEngine */ std::map<std::string, Integer> d_commandVerbosity; - /** ReplayStream for the solver. */ - ExprStream* d_replayStream; - /** * A private utility class to SmtEngine. */ diff --git a/src/theory/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp deleted file mode 100644 index 1e3905537..000000000 --- a/src/theory/idl/idl_assertion.cpp +++ /dev/null @@ -1,213 +0,0 @@ -/********************* */ -/*! \file idl_assertion.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/idl/idl_assertion.h" - -using namespace CVC4; -using namespace theory; -using namespace idl; - -IDLAssertion::IDLAssertion() -: d_op(kind::LAST_KIND) -{} - -IDLAssertion::IDLAssertion(TNode node) { - bool ok = parse(node, 1, false); - if (!ok) { - d_x = d_y = TNode::null(); - } else { - if (d_op == kind::GT) { - // Turn GT into LT x - y > c is the same as y - x < -c - std::swap(d_x, d_y); - d_c = -d_c; - d_op = kind::LT; - } - if (d_op == kind::GEQ) { - // Turn GT into LT x - y >= c is the same as y - x <= -c - std::swap(d_x, d_y); - d_c = -d_c; - d_op = kind::LEQ; - } - if (d_op == kind::LT) { - // Turn strict into non-strict x - y < c is the same as x - y <= c-1 - d_c = d_c - 1; - d_op = kind::LEQ; - } - } - d_original = node; -} - -IDLAssertion::IDLAssertion(const IDLAssertion& other) -: d_x(other.d_x) -, d_y(other.d_y) -, d_op(other.d_op) -, d_c(other.d_c) -, d_original(other.d_original) -{} - -bool IDLAssertion::propagate(IDLModel& model) const { - Debug("theory::idl::model") << model << std::endl; - Assert(ok()); - // Should be d_x - d_y <= d_c, or d_x - d_c <= d_y - Integer x_value = model.getValue(d_x); - Integer y_value = model.getValue(d_y); - if (x_value - y_value > d_c) { - model.setValue(d_y, x_value - d_c, IDLReason(d_x, d_original)); - Debug("theory::idl::model") << model << std::endl; - return true; - } else { - return false; - } -} - -void IDLAssertion::toStream(std::ostream& out) const { - out << "IDL[" << d_x << " - " << d_y << " " << d_op << " " << d_c << "]"; -} - -/** Negates the given arithmetic kind */ -static Kind negateOp(Kind op) { - switch (op) { - case kind::LT: - // not (a < b) = (a >= b) - return kind::GEQ; - case kind::LEQ: - // not (a <= b) = (a > b) - return kind::GT; - case kind::GT: - // not (a > b) = (a <= b) - return kind::LEQ; - case kind::GEQ: - // not (a >= b) = (a < b) - return kind::LT; - case kind::EQUAL: - // not (a = b) = (a != b) - return kind::DISTINCT; - case kind::DISTINCT: - // not (a != b) = (a = b) - return kind::EQUAL; - default: - Unreachable(); - break; - } - return kind::LAST_KIND; -} - -bool IDLAssertion::parse(TNode node, int c, bool negated) { - - // Only unit coefficients allowed - if (c != 1 && c != -1) { - return false; - } - - // Assume we're ok - bool ok = true; - - // The kind of the node - switch(node.getKind()) { - - case kind::NOT: - // We parse the negation - ok = parse(node[0], c, true); - // Setup the kind - if (ok) { - d_op = negateOp(d_op); - } - break; - - case kind::EQUAL: - case kind::LT: - case kind::LEQ: - case kind::GT: - case kind::GEQ: { - // All relation operators are parsed on both sides - d_op = node.getKind(); - ok = parse(node[0], c, negated); - if (ok) { - ok = parse(node[1],-c, negated); - } - break; - } - - case kind::CONST_RATIONAL: { - // Constants - Rational m = node.getConst<Rational>(); - if (m.isIntegral()) { - d_c += m.getNumerator() * (-c); - } else { - ok = false; - } - break; - } - case kind::MULT: { - // Only unit multiplication of variables - if (node.getNumChildren() == 2 && node[0].isConst()) { - Rational a = node[0].getConst<Rational>(); - if (a == 1 || a == -1) { - ok = parse(node[1], c * a.sgn(), negated); - } else { - ok = false; - } - } else { - ok = false; - } - break; - } - - case kind::PLUS: { - for(unsigned i = 0; i < node.getNumChildren(); ++i) { - ok = parse(node[i], c, negated); - if(!ok) { - break; - } - } - break; - } - - case kind::MINUS: { - ok = parse(node[0], c, negated); - if (ok) { - ok = parse(node[1], -c, negated); - } - break; - } - - case kind::UMINUS: { - ok = parse(node[0], -c, negated); - break; - } - - default: { - if (c > 0) { - if (d_x.isNull()) { - d_x = node; - } else { - ok = false; - } - } else { - if (d_y.isNull()) { - d_y = node; - } else { - ok = false; - } - } - break; - } - } // End case - - // Difference logic OK - return ok; -} diff --git a/src/theory/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h deleted file mode 100644 index e24fbfc67..000000000 --- a/src/theory/idl/idl_assertion.h +++ /dev/null @@ -1,91 +0,0 @@ -/********************* */ -/*! \file idl_assertion.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#pragma once - -#include "theory/idl/idl_model.h" - -namespace CVC4 { -namespace theory { -namespace idl { - -/** - * An internal representation of the IDL assertions. Each IDL assertions is - * of the form (x - y op c) where op is one of (<=, =, !=). IDL assertion - * can be constructed from an expression. - */ -class IDLAssertion { - - /** The positive variable */ - TNode d_x; - /** The negative variable */ - TNode d_y; - /** The relation */ - Kind d_op; - /** The RHS constant */ - Integer d_c; - - /** Original assertion we got this one from */ - TNode d_original; - - /** Parses the given node into an assertion, and return true if OK. */ - bool parse(TNode node, int c = 1, bool negated = false); - -public: - - /** Null assertion */ - IDLAssertion(); - /** Create the assertion from given node */ - IDLAssertion(TNode node); - /** Copy constructor */ - IDLAssertion(const IDLAssertion& other); - - TNode getX() const { return d_x; } - TNode getY() const { return d_y; } - Kind getOp() const { return d_op;} - Integer getC() const { return d_c; } - - /** - * Propagate the constraint using the model. For example, if the constraint - * is of the form x - y <= -1, and the value of x in the model is 0, then - * - * (x - y <= -1) and (x = 0) implies y >= x + 1 = 1 - * - * If the value of y is less then 1, is is set to 1 and true is returned. If - * the value of y is 1 or more, than false is return. - * - * @return true if value of y was updated - */ - bool propagate(IDLModel& model) const; - - /** Is this constraint proper */ - bool ok() const { - return !d_x.isNull() || !d_y.isNull(); - } - - /** Output to the stream */ - void toStream(std::ostream& out) const; -}; - -inline std::ostream& operator << (std::ostream& out, const IDLAssertion& assertion) { - assertion.toStream(out); - return out; -} - -} -} -} diff --git a/src/theory/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp deleted file mode 100644 index 865d8b4f5..000000000 --- a/src/theory/idl/idl_assertion_db.cpp +++ /dev/null @@ -1,59 +0,0 @@ -/********************* */ -/*! \file idl_assertion_db.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/idl/idl_assertion_db.h" - -using namespace CVC4; -using namespace theory; -using namespace idl; - -IDLAssertionDB::IDLAssertionDB(context::Context* c) -: d_assertions(c) -, d_variableLists(c) -{} - -void IDLAssertionDB::add(const IDLAssertion& assertion, TNode var) { - // Is there a list for the variable already? - unsigned previous = -1; - var_to_unsigned_map::iterator find = d_variableLists.find(var); - if (find != d_variableLists.end()) { - previous = (*find).second; - } - // Add to the DB - d_variableLists[var] = d_assertions.size(); - d_assertions.push_back(IDLAssertionListElement(assertion, previous)); -} - -IDLAssertionDB::iterator::iterator(IDLAssertionDB& db, TNode var) -: d_db(db) -, d_current(-1) -{ - var_to_unsigned_map::const_iterator find = d_db.d_variableLists.find(var); - if (find != d_db.d_variableLists.end()) { - d_current = (*find).second; - } -} - -void IDLAssertionDB::iterator::next() { - if (d_current != (unsigned)(-1)) { - d_current = d_db.d_assertions[d_current].d_previous; - } -} - -IDLAssertion IDLAssertionDB::iterator::get() const { - return d_db.d_assertions[d_current].d_assertion; -} diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h deleted file mode 100644 index ac87282d9..000000000 --- a/src/theory/idl/idl_assertion_db.h +++ /dev/null @@ -1,86 +0,0 @@ -/********************* */ -/*! \file idl_assertion_db.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#pragma once - -#include "theory/idl/idl_assertion.h" -#include "context/cdlist.h" - -namespace CVC4 { -namespace theory { -namespace idl { - -/** - * Context-dependent database assertions, organized by variable. Each variable - * can be associated a list of IDL assertions. The list of assertions can - * be iterated over using the provided iterator class. - */ -class IDLAssertionDB { - - /** Elements of the assertion lists */ - struct IDLAssertionListElement { - /** The assertion itself */ - IDLAssertion d_assertion; - /** The index of the previous element (-1 for null) */ - unsigned d_previous; - - IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous) - : d_assertion(assertion), d_previous(previous) - {} - }; - - /** All assertions in a context dependent stack */ - context::CDList<IDLAssertionListElement> d_assertions; - - typedef context::CDHashMap<TNode, unsigned, TNodeHashFunction> var_to_unsigned_map; - - /** Map from variables to the first element of their list */ - var_to_unsigned_map d_variableLists; - -public: - - /** Create a new assertion database */ - IDLAssertionDB(context::Context* c); - - /** Add a new assertion, attach to the list of the given variable */ - void add(const IDLAssertion& assertion, TNode var); - - /** Iteration over the constraints of a variable */ - class iterator { - /** The database */ - const IDLAssertionDB& d_db; - /** Index of the current constraint */ - unsigned d_current; - public: - /** Construct the iterator for the variable */ - iterator(IDLAssertionDB& db, TNode var); - /** Is this iterator done */ - bool done() const { return d_current == (unsigned)(-1); } - /** Next element */ - void next(); - /** Get the assertion */ - IDLAssertion get() const; - }; -}; - -} -} -} - - - - diff --git a/src/theory/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp deleted file mode 100644 index 4a3426222..000000000 --- a/src/theory/idl/idl_model.cpp +++ /dev/null @@ -1,74 +0,0 @@ -/********************* */ -/*! \file idl_model.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/idl/idl_model.h" - -using namespace CVC4; -using namespace theory; -using namespace idl; - -IDLModel::IDLModel(context::Context* context) - : d_model(context), d_reason(context) -{ -} - -Integer IDLModel::getValue(TNode var) const -{ - model_value_map::const_iterator find = d_model.find(var); - if (find != d_model.end()) - { - return (*find).second; - } - else - { - return 0; - } -} - -void IDLModel::setValue(TNode var, Integer value, IDLReason reason) -{ - Assert(!reason.d_constraint.isNull()); - d_model[var] = value; - d_reason[var] = reason; -} - -void IDLModel::getReasonCycle(TNode var, std::vector<TNode>& reasons) -{ - TNode current = var; - do - { - Debug("theory::idl::model") << "processing: " << var << std::endl; - Assert(d_reason.find(current) != d_reason.end()); - IDLReason reason = d_reason[current]; - Debug("theory::idl::model") - << "adding reason: " << reason.d_constraint << std::endl; - reasons.push_back(reason.d_constraint); - current = reason.d_x; - } while (current != var); -} - -void IDLModel::toStream(std::ostream& out) const -{ - model_value_map::const_iterator it = d_model.begin(); - model_value_map::const_iterator it_end = d_model.end(); - out << "Model[" << std::endl; - for (; it != it_end; ++it) - { - out << (*it).first << " -> " << (*it).second << std::endl; - } - out << "]"; -} diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h deleted file mode 100644 index 610b90695..000000000 --- a/src/theory/idl/idl_model.h +++ /dev/null @@ -1,84 +0,0 @@ -/********************* */ -/*! \file idl_model.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#pragma once - -#include "context/cdhashmap.h" -#include "expr/node.h" - -namespace CVC4 { -namespace theory { -namespace idl { - -/** - * A reason for a value of a variable in the model is a constraint that implies - * this value by means of the value of another variable. For example, if the - * value of x is 0, then the variable x and the constraint (y > 0) are a reason - * for the y taking the value 1. - */ -struct IDLReason -{ - /** The variable of the reason */ - TNode d_x; - /** The constraint of the reason */ - TNode d_constraint; - - IDLReason(TNode x, TNode constraint) : d_x(x), d_constraint(constraint) {} - IDLReason() {} -}; - -/** - * A model maps variables to integer values and backs them up with reasons. - * Default values (if not set with setValue) for all variables are 0. - */ -class IDLModel -{ - typedef context::CDHashMap<TNode, Integer, TNodeHashFunction> model_value_map; - typedef context::CDHashMap<TNode, IDLReason, TNodeHashFunction> - model_reason_map; - - /** Values assigned to individual variables */ - model_value_map d_model; - - /** Reasons constraining the individual variables */ - model_reason_map d_reason; - - public: - IDLModel(context::Context* context); - - /** Get the model value of the variable */ - Integer getValue(TNode var) const; - - /** Set the value of the variable */ - void setValue(TNode var, Integer value, IDLReason reason); - - /** Get the cycle of reasons behind the variable var */ - void getReasonCycle(TNode var, std::vector<TNode>& reasons); - - /** Output to the given stream */ - void toStream(std::ostream& out) const; -}; - -inline std::ostream& operator<<(std::ostream& out, const IDLModel& model) -{ - model.toStream(out); - return out; -} - -} // namespace idl -} // namespace theory -} // namespace CVC4 diff --git a/src/theory/idl/kinds b/src/theory/idl/kinds deleted file mode 100644 index 6bf0218b0..000000000 --- a/src/theory/idl/kinds +++ /dev/null @@ -1,8 +0,0 @@ -# kinds -*- sh -*- -# -# For documentation on this file format, please refer to -# src/theory/builtin/kinds. -# - -alternate THEORY_ARITH "idl" ::CVC4::theory::idl::TheoryIdl "theory/idl/theory_idl.h" - diff --git a/src/theory/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp deleted file mode 100644 index f92738bcb..000000000 --- a/src/theory/idl/theory_idl.cpp +++ /dev/null @@ -1,156 +0,0 @@ -/********************* */ -/*! \file theory_idl.cpp - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Tim King, Morgan Deters - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "theory/idl/theory_idl.h" - -#include <set> -#include <queue> - -#include "options/idl_options.h" -#include "theory/rewriter.h" - - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace idl { - -TheoryIdl::TheoryIdl(context::Context* c, context::UserContext* u, - OutputChannel& out, Valuation valuation, - const LogicInfo& logicInfo) - : Theory(THEORY_ARITH, c, u, out, valuation, logicInfo) - , d_model(c) - , d_assertionsDB(c) -{} - -Node TheoryIdl::ppRewrite(TNode atom) { - if (atom.getKind() == kind::EQUAL && options::idlRewriteEq()) { - // If the option is turned on, each equality into two inequalities. This in - // effect removes equalities, and theorefore dis-equalities too. - Node leq = NodeBuilder<2>(kind::LEQ) << atom[0] << atom[1]; - Node geq = NodeBuilder<2>(kind::GEQ) << atom[0] << atom[1]; - Node rewritten = Rewriter::rewrite(leq.andNode(geq)); - return rewritten; - } else { - return atom; - } -} - -void TheoryIdl::check(Effort level) { - if (done() && !fullEffort(level)) { - return; - } - - TimerStat::CodeTimer checkTimer(d_checkTime); - - while(!done()) { - - // Get the next assertion - Assertion assertion = get(); - Debug("theory::idl") << "TheoryIdl::check(): processing " - << assertion.d_assertion << std::endl; - - // Convert the assertion into the internal representation - IDLAssertion idlAssertion(assertion.d_assertion); - Debug("theory::idl") << "TheoryIdl::check(): got " << idlAssertion << std::endl; - - if (idlAssertion.ok()) { - if (idlAssertion.getOp() == kind::DISTINCT) { - // We don't handle dis-equalities - d_out->setIncomplete(); - } else { - // Process the convex assertions immediately - bool ok = processAssertion(idlAssertion); - if (!ok) { - // In conflict, we're done - return; - } - } - } else { - // Not an IDL assertion, set incomplete - d_out->setIncomplete(); - } - } - -} - -bool TheoryIdl::processAssertion(const IDLAssertion& assertion) { - - Debug("theory::idl") << "TheoryIdl::processAssertion(" << assertion << ")" << std::endl; - - // Add the constraint (x - y op c) to the list assertions of x - d_assertionsDB.add(assertion, assertion.getX()); - - // Update the model, if forced by the assertion - bool y_updated = assertion.propagate(d_model); - - // If the value of y was updated, we might need to update further - if (y_updated) { - - std::queue<TNode> queue; // Queue of variables to consider - std::set<TNode> inQueue; // Current elements of the queue - - // Add the first updated variable to the queue - queue.push(assertion.getY()); - inQueue.insert(assertion.getY()); - - while (!queue.empty()) { - // Pop a new variable x off the queue - TNode x = queue.front(); - queue.pop(); - inQueue.erase(x); - - // Go through the constraint (x - y op c), and update values of y - IDLAssertionDB::iterator it(d_assertionsDB, x); - while (!it.done()) { - // Get the assertion and update y - IDLAssertion x_y_assertion = it.get(); - y_updated = x_y_assertion.propagate(d_model); - // If updated add to the queue - if (y_updated) { - // If the variable that we updated is the same as the first - // variable that we updated, it's a cycle of updates => conflict - if (x_y_assertion.getY() == assertion.getX()) { - std::vector<TNode> reasons; - d_model.getReasonCycle(x_y_assertion.getY(), reasons); - // Construct the reason of the conflict - Node conflict = NodeManager::currentNM()->mkNode(kind::AND, reasons); - d_out->conflict(conflict); - return false; - } else { - // No cycle, just a model update, so we add to the queue - TNode y = x_y_assertion.getY(); - if (inQueue.count(y) == 0) { - queue.push(y); - inQueue.insert(x_y_assertion.getY()); - } - } - } - // Go to the next constraint - it.next(); - } - } - } - - // Everything fine, no conflict - return true; -} - -} /* namepsace CVC4::theory::idl */ -} /* namepsace CVC4::theory */ -} /* namepsace CVC4 */ diff --git a/src/theory/idl/theory_idl.h b/src/theory/idl/theory_idl.h deleted file mode 100644 index 1d48d0785..000000000 --- a/src/theory/idl/theory_idl.h +++ /dev/null @@ -1,63 +0,0 @@ -/********************* */ -/*! \file theory_idl.h - ** \verbatim - ** Top contributors (to current version): - ** Dejan Jovanovic, Mathias Preiner, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#pragma once - -#include "cvc4_private.h" - -#include "theory/theory.h" -#include "theory/idl/idl_model.h" -#include "theory/idl/idl_assertion_db.h" - -namespace CVC4 { -namespace theory { -namespace idl { - -/** - * Handles integer difference logic (IDL) constraints. - */ -class TheoryIdl : public Theory { - - /** The current model */ - IDLModel d_model; - - /** The asserted constraints, organized by variable */ - IDLAssertionDB d_assertionsDB; - - /** Process a new assertion, returns false if in conflict */ - bool processAssertion(const IDLAssertion& assertion); - -public: - - /** Theory constructor. */ - TheoryIdl(context::Context* c, context::UserContext* u, OutputChannel& out, - Valuation valuation, const LogicInfo& logicInfo); - - /** Pre-processing of input atoms */ - Node ppRewrite(TNode atom) override; - - /** Check the assertions for satisfiability */ - void check(Effort effort) override; - - /** Identity string */ - std::string identify() const override { return "THEORY_IDL"; } - -};/* class TheoryIdl */ - -}/* CVC4::theory::idl namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 8a900e1e7..a87203015 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -121,12 +121,6 @@ function alternate { theory_header="$4" theory_includes="${theory_includes}#include \"$theory_header\" " - - eval "alternate_for_$1=\"\${alternate_for_$1} - if(engine->useTheoryAlternative(\\\"$2\\\")) { - engine->addTheory< $3 >($1); - return; - }\"" } function rewriter { diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 32a80a418..e665f6115 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -350,7 +350,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_theoryAlternatives(), d_attr_handle(), d_arithSubstitutionsAdded("theory::arith::zzz::arith::substitutions", 0) { @@ -2374,18 +2373,6 @@ void TheoryEngine::spendResource(ResourceManager::Resource r) d_resourceManager->spendResource(r); } -void TheoryEngine::enableTheoryAlternative(const std::string& name){ - Debug("TheoryEngine::enableTheoryAlternative") - << "TheoryEngine::enableTheoryAlternative(" << name << ")" << std::endl; - - d_theoryAlternatives.insert(name); -} - -bool TheoryEngine::useTheoryAlternative(const std::string& name) { - return d_theoryAlternatives.find(name) != d_theoryAlternatives.end(); -} - - TheoryEngine::Statistics::Statistics(theory::TheoryId theory): conflicts(getStatsPrefix(theory) + "::conflicts", 0), propagations(getStatsPrefix(theory) + "::propagations", 0), diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c1e1e4cac..840d42417 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -895,14 +895,7 @@ public: /** Prints the assertions to the debug stream */ void printAssertions(const char* tag); - /** Theory alternative is in use. */ - bool useTheoryAlternative(const std::string& name); - - /** Enables using a theory alternative by name. */ - void enableTheoryAlternative(const std::string& name); - private: - std::set< std::string > d_theoryAlternatives; std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; |