From: Andrew Reynolds Date: Thu, 4 Nov 2021 19:55:13 +0000 (-0500) Subject: Replace the old dump infrastructure (#7572) X-Git-Tag: cvc5-1.0.0~889 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e680a299ac1da58b8fee27e3733d5e5eea255d94;p=cvc5.git Replace the old dump infrastructure (#7572) This deletes the old dumping infrastructure, which due to changes in our usage of SolverEngine does not print valid benchmarks. This eliminates the concept of a "NodeManagerListener" which has been problematic to maintain. This PR reimplements the --dump=assertions:pre-X and --dump=assertions:post-X as -t assertions::pre-X and -t assertions::post-X. This is done in a self contained utility method in ProcessAssertions using smt::PrintBenchmark and does not require keeping the rest of the code in sync. The other dumping tags are deleted for now, and will be reimplemented as needed. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 268668dfd..1adf40695 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -281,10 +281,6 @@ libcvc5_add_sources( smt/command.h smt/difficulty_post_processor.cpp smt/difficulty_post_processor.h - smt/dump.cpp - smt/dump.h - smt/dump_manager.cpp - smt/dump_manager.h smt/env.cpp smt/env.h smt/env_obj.cpp @@ -302,18 +298,16 @@ libcvc5_add_sources( smt/model_core_builder.h smt/model_blocker.cpp smt/model_blocker.h - smt/node_command.cpp - smt/node_command.h smt/optimization_solver.cpp smt/optimization_solver.h - smt/output_manager.cpp - smt/output_manager.h smt/quant_elim_solver.cpp smt/quant_elim_solver.h smt/preprocessor.cpp smt/preprocessor.h smt/preprocess_proof_generator.cpp smt/preprocess_proof_generator.h + smt/print_benchmark.cpp + smt/print_benchmark.h smt/process_assertions.cpp smt/process_assertions.h smt/proof_manager.cpp diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 3734e5860..b8e22c6f7 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -365,10 +365,6 @@ void NodeManager::reclaimZombies() { TNode n; n.d_nv = nv; nv->d_rc = 1; // so that TNode doesn't assert-fail - for (NodeManagerListener* listener : d_listeners) - { - listener->nmNotifyDeleteNode(n); - } // this would mean that one of the listeners stowed away // a reference to this node! Assert(nv->d_rc == 1); @@ -662,11 +658,6 @@ std::vector NodeManager::mkMutualDatatypeTypes( } } - for (NodeManagerListener* nml : d_listeners) - { - nml->nmNotifyNewDatatypes(dtts, flags); - } - return dtts; } @@ -830,11 +821,7 @@ TypeNode NodeManager::mkSort(uint32_t flags) { NodeBuilder nb(this, kind::SORT_TYPE); Node sortTag = NodeBuilder(this, kind::SORT_TAG); nb << sortTag; - TypeNode tn = nb.constructTypeNode(); - for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSort(tn, flags); - } - return tn; + return nb.constructTypeNode(); } TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { @@ -843,9 +830,6 @@ TypeNode NodeManager::mkSort(const std::string& name, uint32_t flags) { nb << sortTag; TypeNode tn = nb.constructTypeNode(); setAttribute(tn, expr::VarNameAttr(), name); - for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSort(tn, flags); - } return tn; } @@ -869,9 +853,6 @@ TypeNode NodeManager::mkSort(TypeNode constructor, nb.append(children); TypeNode type = nb.constructTypeNode(); setAttribute(type, expr::VarNameAttr(), name); - for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags); - } return type; } @@ -886,9 +867,6 @@ TypeNode NodeManager::mkSortConstructor(const std::string& name, TypeNode type = nb.constructTypeNode(); setAttribute(type, expr::VarNameAttr(), name); setAttribute(type, expr::SortArityAttr(), arity); - for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewSortConstructor(type, flags); - } return type; } @@ -898,9 +876,6 @@ Node NodeManager::mkVar(const std::string& name, const TypeNode& type) setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); setAttribute(n, expr::VarNameAttr(), name); - for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n); - } return n; } @@ -1021,9 +996,6 @@ Node NodeManager::mkVar(const TypeNode& type) Node n = NodeBuilder(this, kind::VARIABLE); setAttribute(n, TypeAttr(), type); setAttribute(n, TypeCheckedAttr(), true); - for(std::vector::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) { - (*i)->nmNotifyNewVar(n); - } return n; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5b5f07e6f..d0c607a4b 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -56,30 +56,6 @@ namespace expr { class TypeChecker; } // namespace expr -/** - * An interface that an interested party can implement and then subscribe - * to NodeManager events via NodeManager::subscribeEvents(this). - */ -class NodeManagerListener { - public: - virtual ~NodeManagerListener() {} - virtual void nmNotifyNewSort(TypeNode tn, uint32_t flags) {} - virtual void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) {} - virtual void nmNotifyInstantiateSortConstructor(TypeNode ctor, TypeNode sort, - uint32_t flags) {} - virtual void nmNotifyNewDatatypes(const std::vector& datatypes, - uint32_t flags) - { - } - virtual void nmNotifyNewVar(TNode n) {} - /** - * Notify a listener of a Node that's being GCed. If this function stores a - * reference - * to the Node somewhere, very bad things will happen. - */ - virtual void nmNotifyDeleteNode(TNode n) {} -}; /* class NodeManagerListener */ - class NodeManager { friend class api::Solver; @@ -175,11 +151,6 @@ class NodeManager /** unique vars per (Kind,Type) */ std::map< Kind, std::map< TypeNode, Node > > d_unique_vars; - /** - * A list of subscribers for NodeManager events. - */ - std::vector d_listeners; - /** A list of datatypes owned by this node manager */ std::vector > d_dtypes; @@ -370,21 +341,6 @@ class NodeManager /** Get this node manager's bound variable manager */ BoundVarManager* getBoundVarManager() { return d_bvManager.get(); } - /** Subscribe to NodeManager events */ - void subscribeEvents(NodeManagerListener* listener) { - Assert(std::find(d_listeners.begin(), d_listeners.end(), listener) - == d_listeners.end()) - << "listener already subscribed"; - d_listeners.push_back(listener); - } - - /** Unsubscribe from NodeManager events */ - void unsubscribeEvents(NodeManagerListener* listener) { - std::vector::iterator elt = std::find(d_listeners.begin(), d_listeners.end(), listener); - Assert(elt != d_listeners.end()) << "listener not subscribed"; - d_listeners.erase(elt); - } - /** * Return the datatype at the given index owned by this class. Type nodes are * associated with datatypes through the DatatypeIndexConstant class. The diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index b58063dbb..d5d61977c 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -38,7 +38,6 @@ #include "options/smt_options.h" #include "options/theory_options.h" #include "smt/command.h" -#include "smt/dump.h" #include "util/didyoumean.h" namespace cvc5 { @@ -375,7 +374,6 @@ void OptionsHandler::setDefaultDagThresh(const std::string& flag, int dag) Chat.getStream() << expr::ExprDag(dag); CVC5Message.getStream() << expr::ExprDag(dag); Warning.getStream() << expr::ExprDag(dag); - Dump.getStream() << expr::ExprDag(dag); } static void print_config(const char* str, std::string config) @@ -475,27 +473,5 @@ void OptionsHandler::showTraceTags(const std::string& flag) std::exit(0); } -void OptionsHandler::setDumpMode(const std::string& flag, - const std::string& optarg) -{ -#ifdef CVC5_DUMPING - Dump.setDumpFromString(optarg); -#else /* CVC5_DUMPING */ - throw OptionException( - "The dumping feature was disabled in this build of cvc5."); -#endif /* CVC5_DUMPING */ -} - -void OptionsHandler::setDumpStream(const std::string& flag, - const ManagedOut& mo) -{ -#ifdef CVC5_DUMPING - Dump.setStream(mo); -#else /* CVC5_DUMPING */ - throw OptionException( - "The dumping feature was disabled in this build of cvc5."); -#endif /* CVC5_DUMPING */ -} - } // namespace options } // namespace cvc5 diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 077e2119d..884298930 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -130,12 +130,6 @@ class OptionsHandler /** Show all trace tags and exit */ void showTraceTags(const std::string& flag); - /******************************* smt options *******************************/ - /** Set a mode on the dumping output stream. */ - void setDumpMode(const std::string& flag, const std::string& optarg); - /** Set the dumping output stream. */ - void setDumpStream(const std::string& flag, const ManagedOut& mo); - private: /** Pointer to the containing Options object.*/ Options* d_options; diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 420496190..2e2742e73 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -1,23 +1,6 @@ id = "SMT" name = "SMT Layer" -[[option]] - name = "dumpModeString" - category = "common" - long = "dump=MODE" - type = "std::string" - help = "dump preprocessed assertions, etc., see --dump=help" - predicates = ["setDumpMode"] - -[[option]] - name = "dumpToFileName" - category = "common" - long = "dump-to=FILE" - type = "ManagedOut" - help = "all dumping goes to FILE (instead of stdout)" - predicates = ["setDumpStream"] - includes = ["", "options/managed_streams.h"] - [[option]] name = "ackermann" category = "regular" diff --git a/src/preprocessing/passes/sort_infer.cpp b/src/preprocessing/passes/sort_infer.cpp index 68fb89e1f..107e789bb 100644 --- a/src/preprocessing/passes/sort_infer.cpp +++ b/src/preprocessing/passes/sort_infer.cpp @@ -19,7 +19,6 @@ #include "options/uf_options.h" #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" -#include "smt/dump_manager.h" #include "theory/rewriter.h" #include "theory/sort_inference.h" #include "theory/theory_engine.h" @@ -70,13 +69,9 @@ PreprocessingPassResult SortInferencePass::applyInternal( << endl; assertionsToPreprocess->push_back(nar); } - // indicate correspondence between the functions - smt::DumpManager* dm = d_env.getDumpManager(); - for (const std::pair& mrf : model_replace_f) - { - dm->setPrintFuncInModel(mrf.first, false); - dm->setPrintFuncInModel(mrf.second, true); - } + // could indicate correspondence between the functions + // for (f1, f2) in model_replace_f, f1's model should be based on f2. + // See cvc4-wishues/issues/75. } // only need to compute monotonicity on the resulting formula if we are // using this option diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 244e551f7..f7e300a2d 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -18,9 +18,7 @@ #include "preprocessing/assertion_pipeline.h" #include "preprocessing/preprocessing_pass_context.h" #include "printer/printer.h" -#include "smt/dump.h" #include "smt/env.h" -#include "smt/output_manager.h" #include "smt/smt_statistics_registry.h" #include "smt/solver_engine_scope.h" #include "util/statistics_stats.h" @@ -33,29 +31,11 @@ PreprocessingPassResult PreprocessingPass::apply( TimerStat::CodeTimer codeTimer(d_timer); Trace("preprocessing") << "PRE " << d_name << std::endl; Chat() << d_name << "..." << std::endl; - dumpAssertions(("pre-" + d_name).c_str(), *assertionsToPreprocess); PreprocessingPassResult result = applyInternal(assertionsToPreprocess); - dumpAssertions(("post-" + d_name).c_str(), *assertionsToPreprocess); Trace("preprocessing") << "POST " << d_name << std::endl; return result; } -void PreprocessingPass::dumpAssertions(const char* key, - const AssertionPipeline& assertionList) { - if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key)) - { - // Push the simplified assertions to the dump output stream - Env& env = d_preprocContext->getEnv(); - const Printer& printer = env.getPrinter(); - std::ostream& out = env.getDumpOut(); - - for (const auto& n : assertionList) - { - printer.toStreamCmdAssert(out, n); - } - } -} - PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext, const std::string& name) : EnvObj(preprocContext->getEnv()), diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index cc438e5c6..bd141261f 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -60,11 +60,6 @@ class PreprocessingPass : protected EnvObj virtual ~PreprocessingPass(); protected: - /* - * Method for dumping assertions within a pass. Also called before and after - * applying the pass. - */ - void dumpAssertions(const char* key, const AssertionPipeline& assertionList); /* * Abstract method that each pass implements to do the actual preprocessing. diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index e8bdab039..c35d55d05 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -24,7 +24,6 @@ #include "options/language.h" // for LANG_AST #include "printer/let_binding.h" #include "smt/command.h" -#include "smt/node_command.h" using namespace std; diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index cc9df91f4..b66ae5728 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -23,7 +23,6 @@ #include "printer/tptp/tptp_printer.h" #include "proof/unsat_core.h" #include "smt/command.h" -#include "smt/node_command.h" #include "theory/quantifiers/instantiation_list.h" using namespace std; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index da8e56448..51458d66e 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -41,8 +41,6 @@ #include "printer/let_binding.h" #include "proof/unsat_core.h" #include "smt/command.h" -#include "smt/node_command.h" -#include "smt/solver_engine.h" #include "smt_util/boolean_simplification.h" #include "theory/arrays/theory_arrays_rewriter.h" #include "theory/datatypes/sygus_datatype_utils.h" diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp index e5f2ea55d..fe44becb6 100644 --- a/src/printer/tptp/tptp_printer.cpp +++ b/src/printer/tptp/tptp_printer.cpp @@ -24,7 +24,6 @@ #include "options/smt_options.h" // for unsat cores #include "proof/unsat_core.h" #include "smt/command.h" -#include "smt/node_command.h" #include "smt/solver_engine.h" using namespace std; diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 1bac953fd..4026760f7 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -26,7 +26,6 @@ #include "prop/minisat/minisat.h" #include "prop/prop_engine.h" #include "prop/theory_proxy.h" -#include "smt/dump.h" #include "smt/env.h" #include "smt/smt_statistics_registry.h" #include "smt/solver_engine_scope.h" @@ -61,26 +60,6 @@ CnfStream::CnfStream(SatSolver* satSolver, bool CnfStream::assertClause(TNode node, SatClause& c) { Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n"; - if (Dump.isOn("clauses") && d_env != nullptr) - { - const Printer& printer = d_env->getPrinter(); - std::ostream& out = d_env->getDumpOut(); - if (c.size() == 1) - { - printer.toStreamCmdAssert(out, getNode(c[0])); - } - else - { - Assert(c.size() > 1); - NodeBuilder b(kind::OR); - for (unsigned i = 0; i < c.size(); ++i) - { - b << getNode(c[i]); - } - Node n = b; - printer.toStreamCmdAssert(out, n); - } - } ClauseId clauseId = d_satSolver->addClause(c, d_removable); @@ -207,8 +186,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister } // If it's a theory literal, need to store it for back queries - if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK - || (Dump.isOn("clauses"))) + if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK) { d_literalToNodeMap.insert_safe(lit, node); d_literalToNodeMap.insert_safe(~lit, node.notNode()); diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp index 13e504835..d7f654fc6 100644 --- a/src/smt/check_models.cpp +++ b/src/smt/check_models.cpp @@ -18,7 +18,6 @@ #include "base/modal_exception.h" #include "options/smt_options.h" #include "smt/env.h" -#include "smt/node_command.h" #include "smt/preprocessor.h" #include "smt/smt_solver.h" #include "theory/rewriter.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 1794765b4..a15e20998 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -36,7 +36,6 @@ #include "options/smt_options.h" #include "printer/printer.h" #include "proof/unsat_core.h" -#include "smt/dump.h" #include "smt/model.h" #include "util/smt2_quote_string.h" #include "util/unsafe_interrupt_exception.h" @@ -991,7 +990,6 @@ void ResetAssertionsCommand::toStream(std::ostream& out, void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm) { - Dump("benchmark") << *this; d_commandStatus = CommandSuccess::instance(); } diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp deleted file mode 100644 index ab6144e02..000000000 --- a/src/smt/dump.cpp +++ /dev/null @@ -1,231 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andres Noetzli, Morgan Deters, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Dump utility classes and functions. - */ - -#include "smt/dump.h" - -#include "base/configuration.h" -#include "base/output.h" -#include "lib/strtok_r.h" -#include "options/option_exception.h" -#include "preprocessing/preprocessing_pass_registry.h" -#include "smt/command.h" -#include "smt/node_command.h" - -namespace cvc5 { - -#if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE) - -CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c) -{ - if (d_os != nullptr) - { - (*d_os) << c; - } - return *this; -} - -CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc) -{ - if (d_os != nullptr) - { - (*d_os) << nc; - } - return *this; -} - -#else - -CVC5dumpstream& CVC5dumpstream::operator<<(const Command& c) { return *this; } -CVC5dumpstream& CVC5dumpstream::operator<<(const NodeCommand& nc) -{ - return *this; -} - -#endif /* CVC5_DUMPING && !CVC5_MUZZLE */ - -DumpC DumpChannel; - -std::ostream& DumpC::setStream(std::ostream* os) -{ - ::cvc5::DumpOutChannel.setStream(os); - return *os; -} -std::ostream& DumpC::getStream() { return ::cvc5::DumpOutChannel.getStream(); } -std::ostream* DumpC::getStreamPointer() -{ - return ::cvc5::DumpOutChannel.getStreamPointer(); -} - -void DumpC::setDumpFromString(const std::string& optarg) -{ - if (Configuration::isDumpingBuild()) - { - // Make a copy of optarg for strtok_r to use. - std::string optargCopy = optarg; - char* optargPtr = const_cast(optargCopy.c_str()); - char* tokstr = optargPtr; - char* toksave; - while ((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) - { - tokstr = NULL; - if (!strcmp(optargPtr, "benchmark")) - { - } - else if (!strcmp(optargPtr, "declarations")) - { - } - else if (!strcmp(optargPtr, "assertions")) - { - Dump.on("assertions:post-everything"); - } - else if (!strncmp(optargPtr, "assertions:", 11)) - { - const char* p = optargPtr + 11; - if (!strncmp(p, "pre-", 4)) - { - p += 4; - } - else if (!strncmp(p, "post-", 5)) - { - p += 5; - } - else - { - throw OptionException(std::string("don't know how to dump `") - + optargPtr - + "'. Please consult --dump help."); - } - // hard-coded cases - if (!strcmp(p, "everything") || !strcmp(p, "definition-expansion") - || !strcmp(p, "simplify") || !strcmp(p, "repeat-simplify")) - { - } - else if (preprocessing::PreprocessingPassRegistry::getInstance() - .hasPass(p)) - { - } - else - { - throw OptionException(std::string("don't know how to dump `") - + optargPtr - + "'. Please consult --dump help."); - } - Dump.on("assertions"); - } - else if (!strcmp(optargPtr, "skolems")) - { - } - else if (!strcmp(optargPtr, "clauses")) - { - } - else if (!strcmp(optargPtr, "t-conflicts") - || !strcmp(optargPtr, "t-lemmas") - || !strcmp(optargPtr, "t-explanations") - || !strcmp(optargPtr, "theory::fullcheck")) - { - } - else if (!strcmp(optargPtr, "help")) - { - puts(s_dumpHelp.c_str()); - - std::stringstream ss; - ss << "Available preprocessing passes:\n"; - for (const std::string& pass : - preprocessing::PreprocessingPassRegistry::getInstance() - .getAvailablePasses()) - { - ss << "- " << pass << "\n"; - } - puts(ss.str().c_str()); - exit(1); - } - else - { - throw OptionException(std::string("unknown option for --dump: `") - + optargPtr + "'. Try --dump help."); - } - - Dump.on(optargPtr); - Dump.on("benchmark"); - if (strcmp(optargPtr, "benchmark")) - { - Dump.on("declarations"); - } - } - } - else - { - throw OptionException( - "The dumping feature was disabled in this build of cvc5."); - } -} - -const std::string DumpC::s_dumpHelp = - "\ -Dump modes currently supported by the --dump option:\n\ -\n\ -benchmark\n\ -+ Dump the benchmark structure (set-logic, push/pop, queries, etc.), but\n\ - does not include any declarations or assertions. Implied by all following\n\ - modes.\n\ -\n\ -declarations\n\ -+ Dump user declarations. Implied by all following modes.\n\ -\n\ -skolems\n\ -+ Dump internally-created skolem variable declarations. These can\n\ - arise from preprocessing simplifications, existential elimination,\n\ - and a number of other things. Implied by all following modes.\n\ -\n\ -assertions\n\ -+ Output the assertions after preprocessing and before clausification.\n\ - Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\ - where PASS is one of the preprocessing passes: definition-expansion\n\ - boolean-terms constrain-subtypes substitution bv-to-bool bool-to-bv\n\ - strings-pp skolem-quant simplify static-learning ite-removal\n\ - repeat-simplify rewrite-apply-to-const theory-preprocessing.\n\ - PASS can also be the special value \"everything\", in which case the\n\ - assertions are printed before any preprocessing (with\n\ - \"assertions:pre-everything\") or after all preprocessing completes\n\ - (with \"assertions:post-everything\").\n\ -\n\ -clauses\n\ -+ Do all the preprocessing outlined above, and dump the CNF-converted\n\ - output\n\ -\n\ -t-conflicts\n\ -+ Output correctness queries for all theory conflicts\n\ -\n\ -t-lemmas\n\ -+ Output correctness queries for all theory lemmas\n\ -\n\ -t-explanations\n\ -+ Output correctness queries for all theory explanations\n\ -\n\ -theory::fullcheck\n\ -+ Output completeness queries for all full-check effort-level theory checks\n\ -\n\ -Dump modes can be combined by concatenating the above values with \",\" in\n\ -between them. Generally you want one from the assertions category (either\n\ -assertions or clauses), and perhaps one or more other modes for checking\n\ -correctness and completeness of decision procedure implementations.\n\ -\n\ -The --output-language option controls the language used for dumping, and\n\ -this allows you to connect cvc5 to another solver implementation via a UNIX\n\ -pipe to perform on-line checking. The --dump-to option can be used to dump\n\ -to a file.\n\ -"; - -} // namespace cvc5 diff --git a/src/smt/dump.h b/src/smt/dump.h deleted file mode 100644 index 3038d8996..000000000 --- a/src/smt/dump.h +++ /dev/null @@ -1,118 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Andres Noetzli, Abdalrhman Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Dump utility classes and functions. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__DUMP_H -#define CVC5__DUMP_H - -#include "base/output.h" - -namespace cvc5 { - -class Command; -class NodeCommand; - -#if defined(CVC5_DUMPING) && !defined(CVC5_MUZZLE) - -class CVC5dumpstream -{ - public: - CVC5dumpstream() : d_os(nullptr) {} - CVC5dumpstream(std::ostream& os) : d_os(&os) {} - - CVC5dumpstream& operator<<(const Command& c); - - /** A convenience function for dumping internal commands. - * - * Since Commands are now part of the public API, internal code should use - * NodeCommands and this function (instead of the one above) to dump them. - */ - CVC5dumpstream& operator<<(const NodeCommand& nc); - - private: - std::ostream* d_os; -}; /* class CVC5dumpstream */ - -#else - -/** - * Dummy implementation of the dump stream when dumping is disabled or the - * build is muzzled. - */ -class CVC5dumpstream -{ - public: - CVC5dumpstream() {} - CVC5dumpstream(std::ostream& os) {} - CVC5dumpstream& operator<<(const Command& c); - CVC5dumpstream& operator<<(const NodeCommand& nc); -}; /* class CVC5dumpstream */ - -#endif /* CVC5_DUMPING && !CVC5_MUZZLE */ - -/** The dump class */ -class DumpC -{ - public: - CVC5dumpstream operator()(const char* tag) - { - if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { - return CVC5dumpstream(getStream()); - } else { - return CVC5dumpstream(); - } - } - - CVC5dumpstream operator()(std::string tag) - { - if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC5dumpstream(getStream()); - } else { - return CVC5dumpstream(); - } - } - - bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } - bool on (std::string tag) { d_tags.insert(tag); return true; } - bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } - bool off(std::string tag) { d_tags.erase (tag); return false; } - bool off() { d_tags.clear(); return false; } - - bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } - bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } - - std::ostream& setStream(std::ostream* os); - std::ostream& getStream(); - std::ostream* getStreamPointer(); - - void setDumpFromString(const std::string& optarg); - - private: - /** Set of dumping tags that are currently active. */ - std::set d_tags; - - /** The message printed on `--dump help`. */ - static const std::string s_dumpHelp; -};/* class DumpC */ - -/** The dump singleton */ -extern DumpC DumpChannel; - -#define Dump ::cvc5::DumpChannel - -} // namespace cvc5 - -#endif /* CVC5__DUMP_H */ diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp deleted file mode 100644 index 83ff8e6b9..000000000 --- a/src/smt/dump_manager.cpp +++ /dev/null @@ -1,76 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Gereon Kremer, Morgan Deters - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of the dump manager. - */ - -#include "smt/dump_manager.h" - -#include "options/smt_options.h" -#include "smt/dump.h" -#include "smt/node_command.h" - -namespace cvc5 { -namespace smt { - -DumpManager::DumpManager(context::UserContext* u) - : d_fullyInited(false), - d_dumpCommands() -{ -} - -DumpManager::~DumpManager() -{ - d_dumpCommands.clear(); -} - -void DumpManager::finishInit() -{ - Trace("smt-debug") << "Dump declaration commands..." << std::endl; - // dump out any pending declaration commands - for (size_t i = 0, ncoms = d_dumpCommands.size(); i < ncoms; ++i) - { - Dump("declarations") << *d_dumpCommands[i]; - } - d_dumpCommands.clear(); - - d_fullyInited = true; -} -void DumpManager::resetAssertions() -{ - // currently, do nothing -} - -void DumpManager::addToDump(const NodeCommand& c, const char* dumpTag) -{ - Trace("smt") << "SMT addToDump(" << c << ")" << std::endl; - if (Dump.isOn(dumpTag)) - { - if (d_fullyInited) - { - Dump(dumpTag) << c; - } - else - { - d_dumpCommands.push_back(std::unique_ptr(c.clone())); - } - } -} - -void DumpManager::setPrintFuncInModel(Node f, bool p) -{ - Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl; - // TODO (cvc4-wishues/issues/75): implement -} - -} // namespace smt -} // namespace cvc5 diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h deleted file mode 100644 index b6e0ccfa2..000000000 --- a/src/smt/dump_manager.h +++ /dev/null @@ -1,81 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Morgan Deters, Gereon Kremer - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The dump manager of the SolverEngine. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__SMT__DUMP_MANAGER_H -#define CVC5__SMT__DUMP_MANAGER_H - -#include -#include - -#include "expr/node.h" - -namespace cvc5 { - -class NodeCommand; - -namespace context { -class UserContext; -} - -namespace smt { - -/** - * This utility is responsible for: - * implementing some dumping traces e.g. --dump=declarations. - */ -class DumpManager -{ - - public: - DumpManager(context::UserContext* u); - ~DumpManager(); - /** - * Finish init, called during SolverEngine::finishInit, which is triggered - * when initialization of options is finished. - */ - void finishInit(); - /** - * Reset assertions, called on SolverEngine::resetAssertions. - */ - void resetAssertions(); - /** - * Add to dump command. This is used for recording a command - * that should be reported via the dumpTag trace. - */ - void addToDump(const NodeCommand& c, const char* dumpTag = "declarations"); - - /** - * Set that function f should print in the model if and only if p is true. - */ - void setPrintFuncInModel(Node f, bool p); - - private: - /** Fully inited */ - bool d_fullyInited; - /** - * A vector of declaration commands waiting to be dumped out. - * Once the SolverEngine is fully initialized, we'll dump them. - * This ensures the declarations come after the set-logic and - * any necessary set-option commands are dumped. - */ - std::vector> d_dumpCommands; -}; - -} // namespace smt -} // namespace cvc5 - -#endif diff --git a/src/smt/env.cpp b/src/smt/env.cpp index dc9efdf91..641360456 100644 --- a/src/smt/env.cpp +++ b/src/smt/env.cpp @@ -24,7 +24,6 @@ #include "options/strings_options.h" #include "printer/printer.h" #include "proof/conv_proof_generator.h" -#include "smt/dump_manager.h" #include "smt/solver_engine_stats.h" #include "theory/evaluator.h" #include "theory/rewriter.h" @@ -45,7 +44,6 @@ Env::Env(NodeManager* nm, const Options* opts) d_evalRew(nullptr), d_eval(nullptr), d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())), - d_dumpManager(new DumpManager(d_userContext.get())), d_logic(), d_statisticsRegistry(std::make_unique(*this)), d_options(), @@ -80,7 +78,6 @@ void Env::setProofNodeManager(ProofNodeManager* pnm) void Env::shutdown() { d_rewriter.reset(nullptr); - d_dumpManager.reset(nullptr); // d_resourceManager must be destroyed before d_statisticsRegistry d_resourceManager.reset(nullptr); } @@ -123,8 +120,6 @@ theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions() return *d_topLevelSubs.get(); } -DumpManager* Env::getDumpManager() { return d_dumpManager.get(); } - const LogicInfo& Env::getLogicInfo() const { return d_logic; } StatisticsRegistry& Env::getStatisticsRegistry() @@ -146,8 +141,6 @@ const Printer& Env::getPrinter() return *Printer::getPrinter(d_options.base.outputLanguage); } -std::ostream& Env::getDumpOut() { return *d_options.base.out; } - bool Env::isOutputOn(OutputTag tag) const { return d_options.base.outputTagHolder[static_cast(tag)]; diff --git a/src/smt/env.h b/src/smt/env.h index 25f8d0b71..f94d8efea 100644 --- a/src/smt/env.h +++ b/src/smt/env.h @@ -44,7 +44,6 @@ class UserContext; } // namespace context namespace smt { -class DumpManager; class PfManager; } @@ -119,9 +118,6 @@ class Env /** Get a reference to the top-level substitution map */ theory::TrustSubstitutionMap& getTopLevelSubstitutions(); - /** Get a pointer to the underlying dump manager. */ - smt::DumpManager* getDumpManager(); - /** Get the options object (const version only) owned by this Env. */ const Options& getOptions() const; @@ -145,12 +141,6 @@ class Env */ const Printer& getPrinter(); - /** - * Get the output stream that --dump=X should print to - * @return the output stream - */ - std::ostream& getDumpOut(); - /** * Check whether the output for the given output tag is enabled. Output tags * are enabled via the `output` option (or `-o` on the command line). @@ -284,8 +274,6 @@ class Env std::unique_ptr d_eval; /** The top level substitutions */ std::unique_ptr d_topLevelSubs; - /** The dump manager */ - std::unique_ptr d_dumpManager; /** * The logic we're in. This logic may be an extension of the logic set by the * user, which may be different from the user-provided logic due to the diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp index 7a1951d95..628457a31 100644 --- a/src/smt/listeners.cpp +++ b/src/smt/listeners.cpp @@ -15,14 +15,6 @@ #include "smt/listeners.h" -#include "base/configuration.h" -#include "expr/attribute.h" -#include "expr/node_manager_attributes.h" -#include "options/smt_options.h" -#include "printer/printer.h" -#include "smt/dump.h" -#include "smt/dump_manager.h" -#include "smt/node_command.h" #include "smt/solver_engine.h" #include "smt/solver_engine_scope.h" @@ -38,56 +30,5 @@ void ResourceOutListener::notify() d_slv.interrupt(); } -SmtNodeManagerListener::SmtNodeManagerListener(DumpManager& dm, - OutputManager& outMgr) - : d_dm(dm), d_outMgr(outMgr) -{ -} - -void SmtNodeManagerListener::nmNotifyNewSort(TypeNode tn, uint32_t flags) -{ - DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn); - if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0) - { - d_dm.addToDump(c); - } -} - -void SmtNodeManagerListener::nmNotifyNewSortConstructor(TypeNode tn, - uint32_t flags) -{ - DeclareTypeNodeCommand c(tn.getAttribute(expr::VarNameAttr()), - tn.getAttribute(expr::SortArityAttr()), - tn); - if ((flags & NodeManager::SORT_FLAG_PLACEHOLDER) == 0) - { - d_dm.addToDump(c); - } -} - -void SmtNodeManagerListener::nmNotifyNewDatatypes( - const std::vector& dtts, uint32_t flags) -{ - if ((flags & NodeManager::DATATYPE_FLAG_PLACEHOLDER) == 0) - { - if (Configuration::isAssertionBuild()) - { - for (CVC5_UNUSED const TypeNode& dt : dtts) - { - Assert(dt.isDatatype()); - } - } - DeclareDatatypeNodeCommand c(dtts); - d_dm.addToDump(c); - } -} - -void SmtNodeManagerListener::nmNotifyNewVar(TNode n) -{ - DeclareFunctionNodeCommand c( - n.getAttribute(expr::VarNameAttr()), n, n.getType()); - d_dm.addToDump(c); -} - } // namespace smt } // namespace cvc5 diff --git a/src/smt/listeners.h b/src/smt/listeners.h index df99f8008..a20051bd7 100644 --- a/src/smt/listeners.h +++ b/src/smt/listeners.h @@ -43,34 +43,6 @@ class ResourceOutListener : public Listener SolverEngine& d_slv; }; -class DumpManager; - -/** - * A listener for node manager calls, which impacts certain dumping traces. - */ -class SmtNodeManagerListener : public NodeManagerListener -{ - public: - SmtNodeManagerListener(DumpManager& dm, OutputManager& outMgr); - /** Notify when new sort is created */ - void nmNotifyNewSort(TypeNode tn, uint32_t flags) override; - /** Notify when new sort constructor is created */ - void nmNotifyNewSortConstructor(TypeNode tn, uint32_t flags) override; - /** Notify when list of datatypes is created */ - void nmNotifyNewDatatypes(const std::vector& dtts, - uint32_t flags) override; - /** Notify when new variable is created */ - void nmNotifyNewVar(TNode n) override; - /** Notify when a term is deleted */ - void nmNotifyDeleteNode(TNode n) override {} - - private: - /** Reference to the dump manager of smt engine */ - DumpManager& d_dm; - /** Reference to the output manager of the smt engine */ - OutputManager& d_outMgr; -}; - } // namespace smt } // namespace cvc5 diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp deleted file mode 100644 index 000107341..000000000 --- a/src/smt/node_command.cpp +++ /dev/null @@ -1,160 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed, Yoni Zohar, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of NodeCommand functions. - */ - -#include "smt/node_command.h" - -#include - -#include "printer/printer.h" - -namespace cvc5 { - -/* -------------------------------------------------------------------------- */ -/* class NodeCommand */ -/* -------------------------------------------------------------------------- */ - -NodeCommand::~NodeCommand() {} - -std::string NodeCommand::toString() const -{ - std::stringstream ss; - toStream(ss); - return ss.str(); -} - -std::ostream& operator<<(std::ostream& out, const NodeCommand& nc) -{ - nc.toStream(out, - Node::setdepth::getDepth(out), - Node::dag::getDag(out), - Node::setlanguage::getLanguage(out)); - return out; -} - -/* -------------------------------------------------------------------------- */ -/* class DeclareFunctionNodeCommand */ -/* -------------------------------------------------------------------------- */ - -DeclareFunctionNodeCommand::DeclareFunctionNodeCommand(const std::string& id, - Node expr, - TypeNode type) - : d_id(id), - d_fun(expr), - d_type(type) -{ -} - -void DeclareFunctionNodeCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const -{ - Printer::getPrinter(language)->toStreamCmdDeclareFunction(out, d_id, d_type); -} - -NodeCommand* DeclareFunctionNodeCommand::clone() const -{ - return new DeclareFunctionNodeCommand(d_id, d_fun, d_type); -} - -const Node& DeclareFunctionNodeCommand::getFunction() const { return d_fun; } - -/* -------------------------------------------------------------------------- */ -/* class DeclareTypeNodeCommand */ -/* -------------------------------------------------------------------------- */ - -DeclareTypeNodeCommand::DeclareTypeNodeCommand(const std::string& id, - size_t arity, - TypeNode type) - : d_id(id), d_arity(arity), d_type(type) -{ -} - -void DeclareTypeNodeCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const -{ - Printer::getPrinter(language)->toStreamCmdDeclareType(out, d_type); -} - -NodeCommand* DeclareTypeNodeCommand::clone() const -{ - return new DeclareTypeNodeCommand(d_id, d_arity, d_type); -} - -const std::string DeclareTypeNodeCommand::getSymbol() const { return d_id; } - -const TypeNode& DeclareTypeNodeCommand::getType() const { return d_type; } - -/* -------------------------------------------------------------------------- */ -/* class DeclareDatatypeNodeCommand */ -/* -------------------------------------------------------------------------- */ - -DeclareDatatypeNodeCommand::DeclareDatatypeNodeCommand( - const std::vector& datatypes) - : d_datatypes(datatypes) -{ -} - -void DeclareDatatypeNodeCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const -{ - Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(out, - d_datatypes); -} - -NodeCommand* DeclareDatatypeNodeCommand::clone() const -{ - return new DeclareDatatypeNodeCommand(d_datatypes); -} - -/* -------------------------------------------------------------------------- */ -/* class DefineFunctionNodeCommand */ -/* -------------------------------------------------------------------------- */ - -DefineFunctionNodeCommand::DefineFunctionNodeCommand( - const std::string& id, - Node fun, - const std::vector& formals, - Node formula) - : d_id(id), d_fun(fun), d_formals(formals), d_formula(formula) -{ -} - -void DefineFunctionNodeCommand::toStream(std::ostream& out, - int toDepth, - size_t dag, - Language language) const -{ - TypeNode tn = d_fun.getType(); - bool hasRange = - (tn.isFunction() || tn.isConstructor() || tn.isSelector()); - Printer::getPrinter(language)->toStreamCmdDefineFunction( - out, - d_fun.toString(), - d_formals, - (hasRange ? d_fun.getType().getRangeType() : tn), - d_formula); -} - -NodeCommand* DefineFunctionNodeCommand::clone() const -{ - return new DefineFunctionNodeCommand(d_id, d_fun, d_formals, d_formula); -} - -} // namespace cvc5 diff --git a/src/smt/node_command.h b/src/smt/node_command.h deleted file mode 100644 index 3399cb6fb..000000000 --- a/src/smt/node_command.h +++ /dev/null @@ -1,141 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Datastructures used for printing commands internally. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__SMT__NODE_COMMAND_H -#define CVC5__SMT__NODE_COMMAND_H - -#include - -#include "expr/node.h" -#include "expr/type_node.h" -#include "options/language.h" - -namespace cvc5 { - -/** - * A node version of Command. DO NOT use this version unless there is a need - * to buffer commands for later use (e.g., printing models). - */ -class NodeCommand -{ - public: - /** Destructor */ - virtual ~NodeCommand(); - - /** Print this NodeCommand to output stream */ - virtual void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - Language language = Language::LANG_AUTO) const = 0; - - /** Get a string representation of this NodeCommand */ - std::string toString() const; - - /** Clone this NodeCommand (make a shallow copy). */ - virtual NodeCommand* clone() const = 0; -}; - -std::ostream& operator<<(std::ostream& out, const NodeCommand& nc); - -/** - * Declare n-ary function symbol. - * SMT-LIB: ( declare-fun ( ) ) - */ -class DeclareFunctionNodeCommand : public NodeCommand -{ - public: - DeclareFunctionNodeCommand(const std::string& id, Node fun, TypeNode type); - void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - Language language = Language::LANG_AUTO) const override; - NodeCommand* clone() const override; - const Node& getFunction() const; - - private: - std::string d_id; - Node d_fun; - TypeNode d_type; -}; - -/** - * Create datatype sort. - * SMT-LIB: ( declare-datatypes ( {n+1} ) ( {n+1} ) ) - */ -class DeclareDatatypeNodeCommand : public NodeCommand -{ - public: - DeclareDatatypeNodeCommand(const std::vector& datatypes); - void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - Language language = Language::LANG_AUTO) const override; - NodeCommand* clone() const override; - - private: - std::vector d_datatypes; -}; - -/** - * Declare uninterpreted sort. - * SMT-LIB: ( declare-sort ) - */ -class DeclareTypeNodeCommand : public NodeCommand -{ - public: - DeclareTypeNodeCommand(const std::string& id, size_t arity, TypeNode type); - void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - Language language = Language::LANG_AUTO) const override; - NodeCommand* clone() const override; - const std::string getSymbol() const; - const TypeNode& getType() const; - - private: - std::string d_id; - size_t d_arity; - TypeNode d_type; -}; - -/** - * Define n-ary function. - * SMT-LIB: ( define-fun ( ) ) - */ -class DefineFunctionNodeCommand : public NodeCommand -{ - public: - DefineFunctionNodeCommand(const std::string& id, - Node fun, - const std::vector& formals, - Node formula); - void toStream(std::ostream& out, - int toDepth = -1, - size_t dag = 1, - Language language = Language::LANG_AUTO) const override; - NodeCommand* clone() const override; - - private: - std::string d_id; - Node d_fun; - std::vector d_formals; - Node d_formula; -}; - -} // namespace cvc5 - -#endif /* CVC5__SMT__NODE_COMMAND_H */ diff --git a/src/smt/output_manager.cpp b/src/smt/output_manager.cpp deleted file mode 100644 index 0a363c08a..000000000 --- a/src/smt/output_manager.cpp +++ /dev/null @@ -1,32 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Implementation of OutputManager functions. - */ - -#include "smt/output_manager.h" - -#include "options/base_options.h" -#include "smt/solver_engine.h" - -namespace cvc5 { - -OutputManager::OutputManager(SolverEngine* slv) : d_slv(slv) {} - -const Printer& OutputManager::getPrinter() const { return d_slv->getPrinter(); } - -std::ostream& OutputManager::getDumpOut() const -{ - return *d_slv->getOptions().base.out; -} - -} // namespace cvc5 diff --git a/src/smt/output_manager.h b/src/smt/output_manager.h deleted file mode 100644 index 34dcc41b4..000000000 --- a/src/smt/output_manager.h +++ /dev/null @@ -1,58 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Abdalrhman Mohamed - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * The output manager for the SolverEngine. - * - * The output manager provides helper functions for printing commands - * internally. - */ - -#ifndef CVC5__SMT__OUTPUT_MANAGER_H -#define CVC5__SMT__OUTPUT_MANAGER_H - -#include - -namespace cvc5 { - -class Printer; -class SolverEngine; - -/** This utility class provides helper functions for printing commands - * internally */ -class OutputManager -{ - public: - /** Constructor - * - * @param smt SMT engine to manage output for - */ - explicit OutputManager(SolverEngine* smt); - - /** Get the current printer based on the current options - * - * @return the current printer - */ - const Printer& getPrinter() const; - - /** Get the output stream that --dump=X should print to - * - * @return the output stream - */ - std::ostream& getDumpOut() const; - - private: - SolverEngine* d_slv; -}; - -} // namespace cvc5 - -#endif // CVC5__SMT__OUTPUT_MANAGER_H diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp index 3aed58b30..1835e61db 100644 --- a/src/smt/preprocessor.cpp +++ b/src/smt/preprocessor.cpp @@ -22,7 +22,6 @@ #include "printer/printer.h" #include "smt/abstract_values.h" #include "smt/assertions.h" -#include "smt/dump.h" #include "smt/env.h" #include "smt/preprocess_proof_generator.h" #include "smt/solver_engine.h" @@ -145,10 +144,6 @@ void Preprocessor::expandDefinitions(std::vector& ns) Node Preprocessor::simplify(const Node& node) { Trace("smt") << "SMT simplify(" << node << ")" << endl; - if (Dump.isOn("benchmark")) - { - d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node); - } Node ret = expandDefinitions(node); ret = rewrite(ret); return ret; diff --git a/src/smt/preprocessor.h b/src/smt/preprocessor.h index 40a84981a..957b5e36e 100644 --- a/src/smt/preprocessor.h +++ b/src/smt/preprocessor.h @@ -62,6 +62,8 @@ class Preprocessor : protected EnvObj /** * Process the assertions that have been asserted in argument as. Returns * true if no conflict was discovered while preprocessing them. + * + * @param as The assertions. */ bool process(Assertions& as); /** diff --git a/src/smt/print_benchmark.cpp b/src/smt/print_benchmark.cpp index c1913e209..598cb9afc 100644 --- a/src/smt/print_benchmark.cpp +++ b/src/smt/print_benchmark.cpp @@ -159,6 +159,11 @@ void PrintBenchmark::printDeclaredFuns(std::ostream& out, for (const Node& f : funs) { Assert(f.isVar()); + // do not print selectors, constructors + if (!f.getType().isFirstClass()) + { + continue; + } if (alreadyPrinted.find(f) == alreadyPrinted.end()) { d_printer->toStreamCmdDeclareFunction(out, f); diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp index 47deddac3..468b754cc 100644 --- a/src/smt/process_assertions.cpp +++ b/src/smt/process_assertions.cpp @@ -27,11 +27,9 @@ #include "options/strings_options.h" #include "options/uf_options.h" #include "preprocessing/assertion_pipeline.h" -#include "preprocessing/preprocessing_pass.h" #include "preprocessing/preprocessing_pass_registry.h" #include "printer/printer.h" #include "smt/assertions.h" -#include "smt/dump.h" #include "smt/expand_definitions.h" #include "smt/print_benchmark.h" #include "smt/solver_engine_stats.h" @@ -98,7 +96,8 @@ bool ProcessAssertions::apply(Assertions& as) AssertionPipeline& assertions = as.getAssertionPipeline(); Assert(d_preprocessingPassContext != nullptr); // Dump the assertions - dumpAssertions("pre-everything", as); + dumpAssertions("assertions::pre-everything", as); + Trace("assertions::pre-everything") << std::endl; Trace("smt-proc") << "ProcessAssertions::processAssertions() begin" << endl; Trace("smt") << "ProcessAssertions::processAssertions()" << endl; @@ -114,7 +113,7 @@ bool ProcessAssertions::apply(Assertions& as) if (options().bv.bvGaussElim) { - d_passes["bv-gauss"]->apply(&assertions); + applyPass("bv-gauss", as); } // Add dummy assertion in last position - to be used as a @@ -129,44 +128,42 @@ bool ProcessAssertions::apply(Assertions& as) Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-definition-expansion" << endl; - dumpAssertions("pre-definition-expansion", as); // Apply substitutions first. If we are non-incremental, this has only the // effect of replacing defined functions with their definitions. // We do not call theory-specific expand definitions here, since we want // to give the opportunity to rewrite/preprocess terms before expansion. - d_passes["apply-substs"]->apply(&assertions); + applyPass("apply-substs", as); Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-definition-expansion" << endl; - dumpAssertions("post-definition-expansion", as); Debug("smt") << " assertions : " << assertions.size() << endl; if (options().quantifiers.globalNegate) { // global negation of the formula - d_passes["global-negate"]->apply(&assertions); + applyPass("global-negate", as); as.flipGlobalNegated(); } if (options().arith.nlExtPurify) { - d_passes["nl-ext-purify"]->apply(&assertions); + applyPass("nl-ext-purify", as); } if (options().smt.solveRealAsInt) { - d_passes["real-to-int"]->apply(&assertions); + applyPass("real-to-int", as); } if (options().smt.solveIntAsBV > 0) { - d_passes["int-to-bv"]->apply(&assertions); + applyPass("int-to-bv", as); } if (options().smt.ackermann) { - d_passes["ackermann"]->apply(&assertions); + applyPass("ackermann", as); } Debug("smt") << " assertions : " << assertions.size() << endl; @@ -175,92 +172,93 @@ bool ProcessAssertions::apply(Assertions& as) if (options().smt.extRewPrep) { - d_passes["ext-rew-pre"]->apply(&assertions); + applyPass("ext-rew-pre", as); } // Unconstrained simplification if (options().smt.unconstrainedSimp) { - d_passes["rewrite"]->apply(&assertions); - d_passes["unconstrained-simplifier"]->apply(&assertions); + applyPass("rewrite", as); + applyPass("unconstrained-simplifier", as); } if (options().bv.bvIntroducePow2) { - d_passes["bv-intro-pow2"]->apply(&assertions); + applyPass("bv-intro-pow2", as); } // Lift bit-vectors of size 1 to bool if (options().bv.bitvectorToBool) { - d_passes["bv-to-bool"]->apply(&assertions); + applyPass("bv-to-bool", as); } if (options().smt.solveBVAsInt != options::SolveBVAsIntMode::OFF) { - d_passes["bv-to-int"]->apply(&assertions); + applyPass("bv-to-int", as); } if (options().smt.foreignTheoryRewrite) { - d_passes["foreign-theory-rewrite"]->apply(&assertions); + applyPass("foreign-theory-rewrite", as); } // Since this pass is not robust for the information tracking necessary for // unsat cores, it's only applied if we are not doing unsat core computation - d_passes["apply-substs"]->apply(&assertions); + applyPass("apply-substs", as); // Assertions MUST BE guaranteed to be rewritten by this point - d_passes["rewrite"]->apply(&assertions); + applyPass("rewrite", as); // Convert non-top-level Booleans to bit-vectors of size 1 if (options().bv.boolToBitvector != options::BoolToBVMode::OFF) { - d_passes["bool-to-bv"]->apply(&assertions); + applyPass("bool-to-bv", as); } if (options().sep.sepPreSkolemEmp) { - d_passes["sep-skolem-emp"]->apply(&assertions); + applyPass("sep-skolem-emp", as); } if (logicInfo().isQuantified()) { // remove rewrite rules, apply pre-skolemization to existential quantifiers - d_passes["quantifiers-preprocess"]->apply(&assertions); + applyPass("quantifiers-preprocess", as); // fmf-fun : assume admissible functions, applying preprocessing reduction // to FMF if (options().quantifiers.fmfFunWellDefined) { - d_passes["fun-def-fmf"]->apply(&assertions); + applyPass("fun-def-fmf", as); } } if (!options().strings.stringLazyPreproc) { - d_passes["strings-eager-pp"]->apply(&assertions); + applyPass("strings-eager-pp", as); } if (options().smt.sortInference || options().uf.ufssFairnessMonotone) { - d_passes["sort-inference"]->apply(&assertions); + applyPass("sort-inference", as); } if (options().arith.pbRewrites) { - d_passes["pseudo-boolean-processor"]->apply(&assertions); + applyPass("pseudo-boolean-processor", as); } // rephrasing normal inputs as sygus problems if (options().quantifiers.sygusInference) { - d_passes["sygus-infer"]->apply(&assertions); + applyPass("sygus-infer", as); } else if (options().quantifiers.sygusRewSynthInput) { // do candidate rewrite rule synthesis - d_passes["synth-rr"]->apply(&assertions); + applyPass("synth-rr", as); } Trace("smt-proc") << "ProcessAssertions::processAssertions() : pre-simplify" << endl; - dumpAssertions("pre-simplify", as); + dumpAssertions("assertions::pre-simplify", as); + Trace("assertions::pre-simplify") << std::endl; Chat() << "simplifying assertions..." << endl; noConflict = simplifyAssertions(as); if (!noConflict) @@ -269,31 +267,33 @@ bool ProcessAssertions::apply(Assertions& as) } Trace("smt-proc") << "ProcessAssertions::processAssertions() : post-simplify" << endl; - dumpAssertions("post-simplify", as); + dumpAssertions("assertions::post-simplify", as); + Trace("assertions::post-simplify") << std::endl; if (options().smt.doStaticLearning) { - d_passes["static-learning"]->apply(&assertions); + applyPass("static-learning", as); } Debug("smt") << " assertions : " << assertions.size() << endl; if (options().smt.learnedRewrite) { - d_passes["learned-rewrite"]->apply(&assertions); + applyPass("learned-rewrite", as); } if (options().smt.earlyIteRemoval) { d_slvStats.d_numAssertionsPre += assertions.size(); - d_passes["ite-removal"]->apply(&assertions); + applyPass("ite-removal", as); // This is needed because when solving incrementally, removeITEs may // introduce skolems that were solved for earlier and thus appear in the // substitution map. - d_passes["apply-substs"]->apply(&assertions); + applyPass("apply-substs", as); d_slvStats.d_numAssertionsPost += assertions.size(); } - dumpAssertions("pre-repeat-simplify", as); + dumpAssertions("assertions::pre-repeat-simplify", as); + Trace("assertions::pre-repeat-simplify") << std::endl; if (options().smt.repeatSimp) { Trace("smt-proc") @@ -306,11 +306,12 @@ bool ProcessAssertions::apply(Assertions& as) << "ProcessAssertions::processAssertions() : post-repeat-simplify" << endl; } - dumpAssertions("post-repeat-simplify", as); + dumpAssertions("assertions::post-repeat-simplify", as); + Trace("assertions::post-repeat-simplify") << std::endl; if (logicInfo().isHigherOrder()) { - d_passes["ho-elim"]->apply(&assertions); + applyPass("ho-elim", as); } // begin: INVARIANT to maintain: no reordering of assertions or @@ -323,21 +324,22 @@ bool ProcessAssertions::apply(Assertions& as) Debug("smt") << " assertions : " << assertions.size() << endl; // ensure rewritten - d_passes["rewrite"]->apply(&assertions); + applyPass("rewrite", as); // rewrite equalities based on theory-specific rewriting - d_passes["theory-rewrite-eq"]->apply(&assertions); + applyPass("theory-rewrite-eq", as); // apply theory preprocess, which includes ITE removal - d_passes["theory-preprocess"]->apply(&assertions); + applyPass("theory-preprocess", as); // notice that we do not apply substitutions as a last step here, since // the range of substitutions is not theory-preprocessed. if (options().bv.bitblastMode == options::BitblastMode::EAGER) { - d_passes["bv-eager-atoms"]->apply(&assertions); + applyPass("bv-eager-atoms", as); } Trace("smt-proc") << "ProcessAssertions::apply() end" << endl; - dumpAssertions("post-everything", as); + dumpAssertions("assertions::post-everything", as); + Trace("assertions::post-everything") << std::endl; return noConflict; } @@ -356,8 +358,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as) if (options().smt.simplificationMode != options::SimplificationMode::NONE) { // Perform non-clausal simplification - PreprocessingPassResult res = - d_passes["non-clausal-simp"]->apply(&assertions); + PreprocessingPassResult res = applyPass("non-clausal-simp", as); if (res == PreprocessingPassResult::CONFLICT) { return false; @@ -374,7 +375,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as) // re-simplification, which we don't expect to be useful anyway) assertions.getRealAssertionsEnd() == assertions.size()) { - d_passes["miplib-trick"]->apply(&assertions); + applyPass("miplib-trick", as); } else { @@ -389,7 +390,7 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as) if (options().smt.doITESimp && (d_simplifyAssertionsDepth <= 1 || options().smt.doITESimpOnRepeat)) { - PreprocessingPassResult res = d_passes["ite-simp"]->apply(&assertions); + PreprocessingPassResult res = applyPass("ite-simp", as); if (res == PreprocessingPassResult::CONFLICT) { Chat() << "...ITE simplification found unsat..." << endl; @@ -402,15 +403,14 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as) // Unconstrained simplification if (options().smt.unconstrainedSimp) { - d_passes["unconstrained-simplifier"]->apply(&assertions); + applyPass("unconstrained-simplifier", as); } if (options().smt.repeatSimp && options().smt.simplificationMode != options::SimplificationMode::NONE) { - PreprocessingPassResult res = - d_passes["non-clausal-simp"]->apply(&assertions); + PreprocessingPassResult res = applyPass("non-clausal-simp", as); if (res == PreprocessingPassResult::CONFLICT) { return false; @@ -435,18 +435,65 @@ bool ProcessAssertions::simplifyAssertions(Assertions& as) return true; } -void ProcessAssertions::dumpAssertions(const char* key, Assertions& as) +void ProcessAssertions::dumpAssertions(const std::string& key, Assertions& as) { - if (Dump.isOn("assertions") && Dump.isOn(string("assertions:") + key)) - { - const AssertionPipeline& assertionList = as.getAssertionPipeline(); - // Push the simplified assertions to the dump output stream - for (unsigned i = 0; i < assertionList.size(); ++i) + bool isTraceOn = Trace.isOn(key); + if (!isTraceOn) + { + return; + } + // Cannot print unless produce assertions is enabled. Otherwise, the printing + // is misleading, since it does not capture what symbols were provided + // as definitions. + if (!options().smt.produceAssertions) + { + Warning() + << "Assertions not available for dumping (use --produce-assertions)." + << std::endl; + return; + } + PrintBenchmark pb(&d_env.getPrinter()); + std::vector assertions; + // Notice that the following list covers define-fun and define-fun-rec + // from input. The former does not impact the assertions since define-fun are + // added as top-level substitutions. The latter do get added to the list + // of assertions. Since we are interested in printing the result of + // preprocessed quantified formulas corresponding to recursive function + // definitions and not the original definitions, we discard the latter + // in the loop below. + // + // In summary, this means that define-fun-rec are expanded to + // (declare-fun ...) + (assert (forall ...)) in the printing below, whereas + // define-fun are preserved. + const context::CDList& asld = as.getAssertionListDefinitions(); + std::vector defs; + for (const Node& d : asld) + { + if (d.getKind() != FORALL) { - TNode n = assertionList[i]; - d_env.getPrinter().toStreamCmdAssert(d_env.getDumpOut(), n); + defs.push_back(d); } } + AssertionPipeline& ap = as.getAssertionPipeline(); + for (size_t i = 0, size = ap.size(); i < size; i++) + { + assertions.push_back(ap[i]); + } + std::stringstream ss; + pb.printBenchmark(ss, logicInfo().getLogicString(), defs, assertions); + Trace(key) << ";;; " << key << " start" << std::endl; + Trace(key) << ss.str(); + Trace(key) << ";;; " << key << " end " << std::endl; +} + +PreprocessingPassResult ProcessAssertions::applyPass(const std::string& pname, + Assertions& as) +{ + dumpAssertions("assertions::pre-" + pname, as); + AssertionPipeline& assertions = as.getAssertionPipeline(); + PreprocessingPassResult res = d_passes[pname]->apply(&assertions); + dumpAssertions("assertions::post-" + pname, as); + return res; } } // namespace smt diff --git a/src/smt/process_assertions.h b/src/smt/process_assertions.h index 84c5d1d43..81ea9f475 100644 --- a/src/smt/process_assertions.h +++ b/src/smt/process_assertions.h @@ -22,6 +22,7 @@ #include "context/cdlist.h" #include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" #include "smt/env_obj.h" #include "util/resource_manager.h" @@ -29,8 +30,6 @@ namespace cvc5 { namespace preprocessing { class AssertionPipeline; -class PreprocessingPass; -class PreprocessingPassContext; } namespace smt { @@ -111,7 +110,10 @@ class ProcessAssertions : protected EnvObj * Dump assertions. Print the current assertion list to the dump * assertions:`key` if it is enabled. */ - void dumpAssertions(const char* key, Assertions& as); + void dumpAssertions(const std::string& key, Assertions& as); + /** apply pass */ + preprocessing::PreprocessingPassResult applyPass(const std::string& pass, + Assertions& as); }; } // namespace smt diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp index fddea7649..264e1ec0b 100644 --- a/src/smt/solver_engine.cpp +++ b/src/smt/solver_engine.cpp @@ -40,15 +40,12 @@ #include "smt/abstract_values.h" #include "smt/assertions.h" #include "smt/check_models.h" -#include "smt/dump.h" -#include "smt/dump_manager.h" #include "smt/env.h" #include "smt/interpolation_solver.h" #include "smt/listeners.h" #include "smt/logic_exception.h" #include "smt/model_blocker.h" #include "smt/model_core_builder.h" -#include "smt/node_command.h" #include "smt/preprocessor.h" #include "smt/proof_manager.h" #include "smt/quant_elim_solver.h" @@ -90,7 +87,6 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) d_absValues(new AbstractValues(getNodeManager())), d_asserts(new Assertions(*d_env.get(), *d_absValues.get())), d_routListener(new ResourceOutListener(*this)), - d_snmListener(new SmtNodeManagerListener(*getDumpManager(), d_outMgr)), d_smtSolver(nullptr), d_checkModels(nullptr), d_pfManager(nullptr), @@ -101,7 +97,6 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) d_quantElimSolver(nullptr), d_isInternalSubsolver(false), d_stats(nullptr), - d_outMgr(this), d_scope(nullptr) { // !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SolverEngine @@ -116,8 +111,6 @@ SolverEngine::SolverEngine(NodeManager* nm, const Options* optr) // hand, this hack breaks use cases where multiple SolverEngine objects are // created by the user. d_scope.reset(new SolverEngineScope(this)); - // listen to node manager events - getNodeManager()->subscribeEvents(d_snmListener.get()); // listen to resource out getResourceManager()->registerListener(d_routListener.get()); // make statistics @@ -224,25 +217,6 @@ void SolverEngine::finishInit() Trace("smt-debug") << "Set up assertions..." << std::endl; d_asserts->finishInit(); - // dump out a set-logic command only when raw-benchmark is disabled to avoid - // dumping the command twice. - if (Dump.isOn("benchmark")) - { - LogicInfo everything; - everything.lock(); - getPrinter().toStreamCmdSetInfo( - d_env->getDumpOut(), - "notes", - "cvc5 always dumps the most general, all-supported logic (below), as " - "some internals might require the use of a logic more general than " - "the input."); - getPrinter().toStreamCmdSetBenchmarkLogic(d_env->getDumpOut(), - everything.getLogicString()); - } - - // initialize the dump manager - getDumpManager()->finishInit(); - // subsolvers if (d_env->getOptions().smt.produceAbducts) { @@ -302,8 +276,6 @@ SolverEngine::~SolverEngine() d_smtSolver.reset(nullptr); d_stats.reset(nullptr); - getNodeManager()->unsubscribeEvents(d_snmListener.get()); - d_snmListener.reset(nullptr); d_routListener.reset(nullptr); // destroy the state d_state.reset(nullptr); @@ -374,11 +346,6 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value) Trace("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdSetInfo(d_env->getDumpOut(), key, value); - } - if (key == "filename") { d_env->d_options.driver.filename = value; @@ -572,14 +539,6 @@ void SolverEngine::defineFunction(Node func, Trace("smt") << "SMT defineFunction(" << func << ")" << endl; debugCheckFormals(formals, func); - stringstream ss; - ss << language::SetLanguage( - language::SetLanguage::getLanguage(Dump.getStream())) - << func; - - DefineFunctionNodeCommand nc(ss.str(), func, formals, formula); - getDumpManager()->addToDump(nc, "declarations"); - // type check body debugCheckFunctionBody(formula, formals, func); @@ -786,10 +745,6 @@ Result SolverEngine::checkSat() Result SolverEngine::checkSat(const Node& assumption) { - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), {assumption}); - } std::vector assump; if (!assumption.isNull()) { @@ -800,27 +755,11 @@ Result SolverEngine::checkSat(const Node& assumption) Result SolverEngine::checkSat(const std::vector& assumptions) { - if (Dump.isOn("benchmark")) - { - if (assumptions.empty()) - { - getPrinter().toStreamCmdCheckSat(d_env->getDumpOut()); - } - else - { - getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), - assumptions); - } - } return checkSatInternal(assumptions, false); } Result SolverEngine::checkEntailed(const Node& node) { - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdQuery(d_env->getDumpOut(), node); - } return checkSatInternal( node.isNull() ? std::vector() : std::vector{node}, true) @@ -929,10 +868,6 @@ std::vector SolverEngine::getUnsatAssumptions(void) "UNSAT/ENTAILED."); } finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetUnsatAssumptions(d_env->getDumpOut()); - } UnsatCore core = getUnsatCoreInternal(); std::vector res; std::vector& assumps = d_asserts->getAssumptions(); @@ -1056,10 +991,6 @@ Node SolverEngine::getValue(const Node& ex) const SolverEngineScope smts(this); Trace("smt") << "SMT getValue(" << ex << ")" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetValue(d_env->getDumpOut(), {ex}); - } TypeNode expectedType = ex.getType(); // Substitute out any abstract values in ex and expand @@ -1202,11 +1133,6 @@ Result SolverEngine::blockModel() finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdBlockModel(d_env->getDumpOut()); - } - TheoryModel* m = getAvailableModel("block model"); if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE) @@ -1232,11 +1158,6 @@ Result SolverEngine::blockModelValues(const std::vector& exprs) finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs); - } - TheoryModel* m = getAvailableModel("block model values"); // get expanded assertions @@ -1538,10 +1459,6 @@ UnsatCore SolverEngine::getUnsatCore() Trace("smt") << "SMT getUnsatCore()" << std::endl; SolverEngineScope smts(this); finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetUnsatCore(d_env->getDumpOut()); - } return getUnsatCoreInternal(); } @@ -1563,10 +1480,6 @@ std::string SolverEngine::getProof() Trace("smt") << "SMT getProof()\n"; SolverEngineScope smts(this); finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetProof(d_env->getDumpOut()); - } if (!d_env->getOptions().smt.produceProofs) { throw ModalException("Cannot get a proof when proof option is off."); @@ -1775,10 +1688,6 @@ std::vector SolverEngine::getAssertions() SolverEngineScope smts(this); finishInit(); d_state->doPendingPops(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetAssertions(d_env->getDumpOut()); - } Trace("smt") << "SMT getAssertions()" << endl; if (!d_env->getOptions().smt.produceAssertions) { @@ -1795,10 +1704,6 @@ void SolverEngine::getDifficultyMap(std::map& dmap) Trace("smt") << "SMT getDifficultyMap()\n"; SolverEngineScope smts(this); finishInit(); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetDifficulty(d_env->getDumpOut()); - } if (!d_env->getOptions().smt.produceDifficulty) { throw ModalException( @@ -1820,10 +1725,6 @@ void SolverEngine::push() d_state->doPendingPops(); Trace("smt") << "SMT push()" << endl; d_smtSolver->processAssertions(*d_asserts); - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdPush(d_env->getDumpOut()); - } d_state->userPush(); } @@ -1832,10 +1733,6 @@ void SolverEngine::pop() SolverEngineScope smts(this); finishInit(); Trace("smt") << "SMT pop()" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdPop(d_env->getDumpOut()); - } d_state->userPop(); // Clear out assertion queues etc., in case anything is still in there @@ -1859,19 +1756,13 @@ void SolverEngine::resetAssertions() // (see solver execution modes in the SMT-LIB standard) Assert(getContext()->getLevel() == 0); Assert(getUserContext()->getLevel() == 0); - getDumpManager()->resetAssertions(); return; } Trace("smt") << "SMT resetAssertions()" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdResetAssertions(d_env->getDumpOut()); - } d_asserts->clearCurrent(); d_state->notifyResetAssertions(); - getDumpManager()->resetAssertions(); // push the state to maintain global context around everything d_state->setup(); @@ -1939,11 +1830,6 @@ void SolverEngine::setOption(const std::string& key, const std::string& value) { Trace("smt") << "SMT setOption(" << key << ", " << value << ")" << endl; - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdSetOption(d_env->getDumpOut(), key, value); - } - if (key == "command-verbosity") { size_t fstIndex = value.find(" "); @@ -1999,11 +1885,6 @@ std::string SolverEngine::getOption(const std::string& key) const return "2"; } - if (Dump.isOn("benchmark")) - { - getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key); - } - if (key == "command-verbosity") { vector result; @@ -2047,12 +1928,8 @@ ResourceManager* SolverEngine::getResourceManager() const return d_env->getResourceManager(); } -DumpManager* SolverEngine::getDumpManager() { return d_env->getDumpManager(); } - const Printer& SolverEngine::getPrinter() const { return d_env->getPrinter(); } -OutputManager& SolverEngine::getOutputManager() { return d_outMgr; } - theory::Rewriter* SolverEngine::getRewriter() { return d_env->getRewriter(); } } // namespace cvc5 diff --git a/src/smt/solver_engine.h b/src/smt/solver_engine.h index 75e653656..7096aec92 100644 --- a/src/smt/solver_engine.h +++ b/src/smt/solver_engine.h @@ -15,8 +15,8 @@ #include "cvc5_public.h" -#ifndef CVC5__SOLVER_ENGINE_H -#define CVC5__SOLVER_ENGINE_H +#ifndef CVC5__SMT__SOLVER_ENGINE_H +#define CVC5__SMT__SOLVER_ENGINE_H #include #include @@ -26,7 +26,6 @@ #include "context/cdhashmap_forward.h" #include "cvc5_export.h" #include "options/options.h" -#include "smt/output_manager.h" #include "smt/smt_mode.h" #include "theory/logic_info.h" #include "util/result.h" @@ -80,7 +79,6 @@ namespace smt { class SolverEngineState; class AbstractValues; class Assertions; -class DumpManager; class ResourceOutListener; class SmtNodeManagerListener; class OptionsManager; @@ -847,15 +845,9 @@ class CVC5_EXPORT SolverEngine /** Get the resource manager of this SMT engine */ ResourceManager* getResourceManager() const; - /** Permit access to the underlying dump manager. */ - smt::DumpManager* getDumpManager(); - /** Get the printer used by this SMT engine */ const Printer& getPrinter() const; - /** Get the output manager for this SMT engine */ - OutputManager& getOutputManager(); - /** Get a pointer to the Rewriter owned by this SolverEngine. */ theory::Rewriter* getRewriter(); /** @@ -1055,8 +1047,6 @@ class CVC5_EXPORT SolverEngine std::unique_ptr d_asserts; /** Resource out listener */ std::unique_ptr d_routListener; - /** Node manager listener */ - std::unique_ptr d_snmListener; /** The SMT solver */ std::unique_ptr d_smtSolver; @@ -1104,8 +1094,6 @@ class CVC5_EXPORT SolverEngine /** The statistics class */ std::unique_ptr d_stats; - /** the output manager for commands */ - mutable OutputManager d_outMgr; /** * The global scope object. Upon creation of this SolverEngine, it becomes the * SolverEngine in scope. It says the SolverEngine in scope until it is diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index 613942d19..208f0ebd3 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -24,7 +24,6 @@ #include "context/context.h" #include "printer/printer.h" -#include "smt/dump.h" #include "smt/solver_engine.h" #include "smt/solver_engine_scope.h" #include "theory/bv/theory_bv_utils.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 5aafae367..53365e1b6 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -30,10 +30,8 @@ #include "proof/proof_checker.h" #include "proof/proof_ensure_closed.h" #include "prop/prop_engine.h" -#include "smt/dump.h" #include "smt/env.h" #include "smt/logic_exception.h" -#include "smt/output_manager.h" #include "theory/combination_care_graph.h" #include "theory/decision_manager.h" #include "theory/quantifiers/first_order_model.h" @@ -349,54 +347,6 @@ void TheoryEngine::printAssertions(const char* tag) { } } -void TheoryEngine::dumpAssertions(const char* tag) { - if (Dump.isOn(tag)) { - const Printer& printer = d_env.getPrinter(); - std::ostream& out = d_env.getDumpOut(); - printer.toStreamCmdSetInfo(out, "notes", "Starting completeness check"); - for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { - Theory* theory = d_theoryTable[theoryId]; - if (theory && d_logicInfo.isTheoryEnabled(theoryId)) { - printer.toStreamCmdSetInfo(out, "notes", "Completeness check"); - printer.toStreamCmdPush(out); - - // Dump the shared terms - if (d_logicInfo.isSharingEnabled()) { - printer.toStreamCmdSetInfo(out, "notes", "Shared terms"); - context::CDList::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end(); - for (unsigned i = 0; it != it_end; ++ it, ++i) { - stringstream ss; - ss << (*it); - printer.toStreamCmdSetInfo(out, "notes", ss.str()); - } - } - - // Dump the assertions - printer.toStreamCmdSetInfo(out, "notes", "Assertions"); - context::CDList::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); - for (; it != it_end; ++ it) { - // Get the assertion - Node assertionNode = (*it).d_assertion; - // Purify all the terms - - if ((*it).d_isPreregistered) - { - printer.toStreamCmdSetInfo(out, "notes", "Preregistered"); - } - else - { - printer.toStreamCmdSetInfo(out, "notes", "Shared assertion"); - } - printer.toStreamCmdAssert(out, assertionNode); - } - printer.toStreamCmdCheckSat(out); - - printer.toStreamCmdPop(out); - } - } - } -} - /** * Check all (currently-active) theories for conflicts. * @param effort the effort level to use @@ -544,12 +494,6 @@ void TheoryEngine::check(Theory::Effort effort) { } catch(const theory::Interrupted&) { Trace("theory") << "TheoryEngine::check() => interrupted" << endl; } - // If fulleffort, check all theories - if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) { - if (!d_inConflict && !needCheck()) { - dumpAssertions("theory::fullcheck"); - } - } } void TheoryEngine::propagate(Theory::Effort effort) @@ -1351,15 +1295,6 @@ void TheoryEngine::lemma(TrustNode tlemma, tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial"); } - if(Dump.isOn("t-lemmas")) { - // we dump the negation of the lemma, to show validity of the lemma - Node n = lemma.negate(); - const Printer& printer = d_env.getPrinter(); - std::ostream& out = d_env.getDumpOut(); - printer.toStreamCmdSetInfo(out, "notes", "theory lemma: expect valid"); - printer.toStreamCmdCheckSatAssuming(out, {n}); - } - // assert the lemma d_propEngine->assertLemma(tlemma, p); @@ -1412,13 +1347,6 @@ void TheoryEngine::conflict(TrustNode tconflict, TheoryId theoryId) // Mark that we are in conflict markInConflict(); - if(Dump.isOn("t-conflicts")) { - const Printer& printer = d_env.getPrinter(); - std::ostream& out = d_env.getDumpOut(); - printer.toStreamCmdSetInfo(out, "notes", "theory conflict: expect unsat"); - printer.toStreamCmdCheckSatAssuming(out, {conflict}); - } - // In the multiple-theories case, we need to reconstruct the conflict if (d_logicInfo.isSharingEnabled()) { // Create the workplace for explanations diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0a9b67979..efde513a9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -499,9 +499,6 @@ class TheoryEngine : protected EnvObj void ensureLemmaAtoms(const std::vector& atoms, theory::TheoryId atomsTo); - /** Dump the assertions to the dump */ - void dumpAssertions(const char* tag); - /** Associated PropEngine engine */ prop::PropEngine* d_propEngine; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f97575808..99c65e973 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -775,7 +775,6 @@ set(regress_0_tests regress0/opt-abd-no-use.smt2 regress0/options/ast-and-sexpr.smt2 regress0/options/interactive-mode.smt2 - regress0/options/invalid_dump.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 diff --git a/test/regress/regress0/options/invalid_dump.smt2 b/test/regress/regress0/options/invalid_dump.smt2 deleted file mode 100644 index ab6f6db31..000000000 --- a/test/regress/regress0/options/invalid_dump.smt2 +++ /dev/null @@ -1,5 +0,0 @@ -; REQUIRES: dumping -; COMMAND-LINE: --dump invalidDumpTag -; ERROR-SCRUBBER: grep -o "unknown option for --dump" -; EXPECT-ERROR: unknown option for --dump -; EXIT: 1 diff --git a/test/regress/regress0/print_define_fun_internal.smt2 b/test/regress/regress0/print_define_fun_internal.smt2 index 47b08da23..997096561 100644 --- a/test/regress/regress0/print_define_fun_internal.smt2 +++ b/test/regress/regress0/print_define_fun_internal.smt2 @@ -1,5 +1,5 @@ -; REQUIRES: dumping -; COMMAND-LINE: --solve-real-as-int --dump=assertions:post-real-to-int +; REQUIRES: tracing +; COMMAND-LINE: --solve-real-as-int -t assertions::post-real-to-int --produce-assertions ; EXIT: 0 ; SCRUBBER: grep -v -E '.*' (set-logic QF_NRA)