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.
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
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
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);
}
}
- for (NodeManagerListener* nml : d_listeners)
- {
- nml->nmNotifyNewDatatypes(dtts, flags);
- }
-
return dtts;
}
NodeBuilder nb(this, kind::SORT_TYPE);
Node sortTag = NodeBuilder(this, kind::SORT_TAG);
nb << sortTag;
- TypeNode tn = nb.constructTypeNode();
- for(std::vector<NodeManagerListener*>::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) {
nb << sortTag;
TypeNode tn = nb.constructTypeNode();
setAttribute(tn, expr::VarNameAttr(), name);
- for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewSort(tn, flags);
- }
return tn;
}
nb.append(children);
TypeNode type = nb.constructTypeNode();
setAttribute(type, expr::VarNameAttr(), name);
- for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyInstantiateSortConstructor(constructor, type, flags);
- }
return type;
}
TypeNode type = nb.constructTypeNode();
setAttribute(type, expr::VarNameAttr(), name);
setAttribute(type, expr::SortArityAttr(), arity);
- for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewSortConstructor(type, flags);
- }
return type;
}
setAttribute(n, TypeAttr(), type);
setAttribute(n, TypeCheckedAttr(), true);
setAttribute(n, expr::VarNameAttr(), name);
- for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewVar(n);
- }
return n;
}
Node n = NodeBuilder(this, kind::VARIABLE);
setAttribute(n, TypeAttr(), type);
setAttribute(n, TypeCheckedAttr(), true);
- for(std::vector<NodeManagerListener*>::iterator i = d_listeners.begin(); i != d_listeners.end(); ++i) {
- (*i)->nmNotifyNewVar(n);
- }
return n;
}
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<TypeNode>& 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;
/** unique vars per (Kind,Type) */
std::map< Kind, std::map< TypeNode, Node > > d_unique_vars;
- /**
- * A list of subscribers for NodeManager events.
- */
- std::vector<NodeManagerListener*> d_listeners;
-
/** A list of datatypes owned by this node manager */
std::vector<std::unique_ptr<DType> > d_dtypes;
/** 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<NodeManagerListener*>::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
#include "options/smt_options.h"
#include "options/theory_options.h"
#include "smt/command.h"
-#include "smt/dump.h"
#include "util/didyoumean.h"
namespace cvc5 {
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)
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
/** 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;
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 = ["<iostream>", "options/managed_streams.h"]
-
[[option]]
name = "ackermann"
category = "regular"
#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"
<< endl;
assertionsToPreprocess->push_back(nar);
}
- // indicate correspondence between the functions
- smt::DumpManager* dm = d_env.getDumpManager();
- for (const std::pair<const Node, Node>& 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
#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"
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()),
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.
#include "options/language.h" // for LANG_AST
#include "printer/let_binding.h"
#include "smt/command.h"
-#include "smt/node_command.h"
using namespace std;
#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;
#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"
#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;
#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"
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);
}
// 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());
#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"
#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"
void QuitCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
- Dump("benchmark") << *this;
d_commandStatus = CommandSuccess::instance();
}
+++ /dev/null
-/******************************************************************************
- * 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<char*>(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
+++ /dev/null
-/******************************************************************************
- * 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<std::string> 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 */
+++ /dev/null
-/******************************************************************************
- * 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<NodeCommand>(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
+++ /dev/null
-/******************************************************************************
- * 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 <memory>
-#include <vector>
-
-#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<std::unique_ptr<NodeCommand>> d_dumpCommands;
-};
-
-} // namespace smt
-} // namespace cvc5
-
-#endif
#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"
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<StatisticsRegistry>(*this)),
d_options(),
void Env::shutdown()
{
d_rewriter.reset(nullptr);
- d_dumpManager.reset(nullptr);
// d_resourceManager must be destroyed before d_statisticsRegistry
d_resourceManager.reset(nullptr);
}
return *d_topLevelSubs.get();
}
-DumpManager* Env::getDumpManager() { return d_dumpManager.get(); }
-
const LogicInfo& Env::getLogicInfo() const { return d_logic; }
StatisticsRegistry& Env::getStatisticsRegistry()
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<size_t>(tag)];
} // namespace context
namespace smt {
-class DumpManager;
class PfManager;
}
/** 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;
*/
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).
std::unique_ptr<theory::Evaluator> d_eval;
/** The top level substitutions */
std::unique_ptr<theory::TrustSubstitutionMap> d_topLevelSubs;
- /** The dump manager */
- std::unique_ptr<smt::DumpManager> 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
#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"
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<TypeNode>& 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
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<TypeNode>& 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
+++ /dev/null
-/******************************************************************************
- * 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 <sstream>
-
-#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<TypeNode>& 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<Node>& 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
+++ /dev/null
-/******************************************************************************
- * 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 <string>
-
-#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 <id> ( <type.getArgTypes()> ) <type.getRangeType()> )
- */
-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 ( <datatype decls>{n+1} ) ( <datatypes>{n+1} ) )
- */
-class DeclareDatatypeNodeCommand : public NodeCommand
-{
- public:
- DeclareDatatypeNodeCommand(const std::vector<TypeNode>& 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<TypeNode> d_datatypes;
-};
-
-/**
- * Declare uninterpreted sort.
- * SMT-LIB: ( declare-sort <id> <arity> )
- */
-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 <id> ( <formals> ) <fun.getType()> <formula> )
- */
-class DefineFunctionNodeCommand : public NodeCommand
-{
- public:
- DefineFunctionNodeCommand(const std::string& id,
- Node fun,
- const std::vector<Node>& 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<Node> d_formals;
- Node d_formula;
-};
-
-} // namespace cvc5
-
-#endif /* CVC5__SMT__NODE_COMMAND_H */
+++ /dev/null
-/******************************************************************************
- * 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
+++ /dev/null
-/******************************************************************************
- * 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 <ostream>
-
-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
#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"
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;
/**
* 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);
/**
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);
#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"
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;
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
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;
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)
}
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")
<< "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
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;
}
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;
// 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
{
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;
// 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;
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<Node> 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<Node>& asld = as.getAssertionListDefinitions();
+ std::vector<Node> 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
#include "context/cdlist.h"
#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
#include "smt/env_obj.h"
#include "util/resource_manager.h"
namespace preprocessing {
class AssertionPipeline;
-class PreprocessingPass;
-class PreprocessingPassContext;
}
namespace smt {
* 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
#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"
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),
d_quantElimSolver(nullptr),
d_isInternalSubsolver(false),
d_stats(nullptr),
- d_outMgr(this),
d_scope(nullptr)
{
// !!!!!!!!!!!!!!!!!!!!!! temporary hack: this makes the current SolverEngine
// 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
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)
{
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);
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;
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);
Result SolverEngine::checkSat(const Node& assumption)
{
- if (Dump.isOn("benchmark"))
- {
- getPrinter().toStreamCmdCheckSatAssuming(d_env->getDumpOut(), {assumption});
- }
std::vector<Node> assump;
if (!assumption.isNull())
{
Result SolverEngine::checkSat(const std::vector<Node>& 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<Node>() : std::vector<Node>{node},
true)
"UNSAT/ENTAILED.");
}
finishInit();
- if (Dump.isOn("benchmark"))
- {
- getPrinter().toStreamCmdGetUnsatAssumptions(d_env->getDumpOut());
- }
UnsatCore core = getUnsatCoreInternal();
std::vector<Node> res;
std::vector<Node>& assumps = d_asserts->getAssumptions();
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
finishInit();
- if (Dump.isOn("benchmark"))
- {
- getPrinter().toStreamCmdBlockModel(d_env->getDumpOut());
- }
-
TheoryModel* m = getAvailableModel("block model");
if (d_env->getOptions().smt.blockModelsMode == options::BlockModelsMode::NONE)
finishInit();
- if (Dump.isOn("benchmark"))
- {
- getPrinter().toStreamCmdBlockModelValues(d_env->getDumpOut(), exprs);
- }
-
TheoryModel* m = getAvailableModel("block model values");
// get expanded assertions
Trace("smt") << "SMT getUnsatCore()" << std::endl;
SolverEngineScope smts(this);
finishInit();
- if (Dump.isOn("benchmark"))
- {
- getPrinter().toStreamCmdGetUnsatCore(d_env->getDumpOut());
- }
return getUnsatCoreInternal();
}
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.");
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)
{
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(
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();
}
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
// (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();
{
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(" ");
return "2";
}
- if (Dump.isOn("benchmark"))
- {
- getPrinter().toStreamCmdGetOption(d_env->getDumpOut(), key);
- }
-
if (key == "command-verbosity")
{
vector<Node> result;
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
#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 <map>
#include <memory>
#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"
class SolverEngineState;
class AbstractValues;
class Assertions;
-class DumpManager;
class ResourceOutListener;
class SmtNodeManagerListener;
class OptionsManager;
/** 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();
/**
std::unique_ptr<smt::Assertions> d_asserts;
/** Resource out listener */
std::unique_ptr<smt::ResourceOutListener> d_routListener;
- /** Node manager listener */
- std::unique_ptr<smt::SmtNodeManagerListener> d_snmListener;
/** The SMT solver */
std::unique_ptr<smt::SmtSolver> d_smtSolver;
/** The statistics class */
std::unique_ptr<smt::SolverEngineStatistics> 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
#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"
#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"
}
}
-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<TNode>::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<Assertion>::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
} 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)
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);
// 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
void ensureLemmaAtoms(const std::vector<TNode>& atoms,
theory::TheoryId atomsTo);
- /** Dump the assertions to the dump */
- void dumpAssertions(const char* tag);
-
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
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
+++ /dev/null
-; REQUIRES: dumping
-; COMMAND-LINE: --dump invalidDumpTag
-; ERROR-SCRUBBER: grep -o "unknown option for --dump"
-; EXPECT-ERROR: unknown option for --dump
-; EXIT: 1
-; 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)
projects / cvc5.git / commitdiff