summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r--src/smt/smt_engine.cpp100
1 files changed, 11 insertions, 89 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5d34e6fa2..f114dba7c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -83,8 +83,8 @@
#include "smt/abduction_solver.h"
#include "smt/abstract_values.h"
#include "smt/command.h"
-#include "smt/command_list.h"
#include "smt/defined_function.h"
+#include "smt/dump_manager.h"
#include "smt/listeners.h"
#include "smt/logic_request.h"
#include "smt/model_blocker.h"
@@ -137,16 +137,6 @@ extern const char* const plf_signatures;
namespace smt {
-struct DeleteCommandFunction : public std::unary_function<const Command*, void>
-{
- void operator()(const Command* command) { delete command; }
-};
-
-void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
- std::for_each(commands.begin(), commands.end(), DeleteCommandFunction());
- commands.clear();
-}
-
/**
* This is an inelegant solution, but for the present, it will work.
* The point of this is to separate the public and private portions of
@@ -338,8 +328,9 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
d_exprManager(em),
d_nodeManager(d_exprManager->getNodeManager()),
d_absValues(new AbstractValues(d_nodeManager)),
+ d_dumpm(new DumpManager(d_userContext.get())),
d_routListener(new ResourceOutListener(*this)),
- d_snmListener(new SmtNodeManagerListener(*this)),
+ d_snmListener(new SmtNodeManagerListener(*d_dumpm.get())),
d_theoryEngine(nullptr),
d_propEngine(nullptr),
d_proofManager(nullptr),
@@ -348,9 +339,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
d_abductSolver(nullptr),
d_assertionList(nullptr),
d_assignments(nullptr),
- d_modelGlobalCommands(),
- d_modelCommands(nullptr),
- d_dumpCommands(),
d_defineCommands(),
d_logic(),
d_originalOptions(),
@@ -413,7 +401,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
#endif
d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
- d_modelCommands = new (true) smt::CommandList(getUserContext());
}
void SmtEngine::finishInit()
@@ -495,13 +482,8 @@ void SmtEngine::finishInit()
everything.getLogicString());
}
- Trace("smt-debug") << "Dump declaration commands..." << std::endl;
- // dump out any pending declaration commands
- for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
- Dump("declarations") << *d_dumpCommands[i];
- delete d_dumpCommands[i];
- }
- d_dumpCommands.clear();
+ // initialize the dump manager
+ d_dumpm->finishInit();
// subsolvers
if (options::produceAbducts())
@@ -579,18 +561,6 @@ SmtEngine::~SmtEngine()
d_assertionList->deleteSelf();
}
- for(unsigned i = 0; i < d_dumpCommands.size(); ++i) {
- delete d_dumpCommands[i];
- d_dumpCommands[i] = NULL;
- }
- d_dumpCommands.clear();
-
- DeleteAndClearCommandVector(d_modelGlobalCommands);
-
- if(d_modelCommands != NULL) {
- d_modelCommands->deleteSelf();
- }
-
d_definedFunctions->deleteSelf();
//destroy all passes before destroying things that they refer to
@@ -608,6 +578,7 @@ SmtEngine::~SmtEngine()
#endif
d_absValues.reset(nullptr);
+ d_dumpm.reset(nullptr);
d_theoryEngine.reset(nullptr);
d_propEngine.reset(nullptr);
@@ -950,7 +921,7 @@ void SmtEngine::defineFunction(Expr func,
language::SetLanguage::getLanguage(Dump.getStream()))
<< func;
DefineFunctionCommand c(ss.str(), func, formals, formula, global);
- addToModelCommandAndDump(
+ d_dumpm->addToModelCommandAndDump(
c, ExprManager::VAR_FLAG_DEFINED, true, "declarations");
PROOF(if (options::checkUnsatCores()) {
@@ -2050,35 +2021,6 @@ vector<pair<Expr, Expr>> SmtEngine::getAssignment()
return res;
}
-void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool userVisible, const char* dumpTag) {
- Trace("smt") << "SMT addToModelCommandAndDump(" << c << ")" << endl;
- SmtScope smts(this);
- // If we aren't yet fully inited, the user might still turn on
- // produce-models. So let's keep any commands around just in
- // case. This is useful in two cases: (1) SMT-LIBv1 auto-declares
- // sort "U" in QF_UF before setLogic() is run and we still want to
- // support finding card(U) with --finite-model-find, and (2) to
- // decouple SmtEngine and ExprManager if the user does a few
- // ExprManager::mkSort() before SmtEngine::setOption("produce-models")
- // and expects to find their cardinalities in the model.
- if(/* userVisible && */
- (!d_fullyInited || options::produceModels()) &&
- (flags & ExprManager::VAR_FLAG_DEFINED) == 0) {
- if(flags & ExprManager::VAR_FLAG_GLOBAL) {
- d_modelGlobalCommands.push_back(c.clone());
- } else {
- d_modelCommands->push_back(c.clone());
- }
- }
- if(Dump.isOn(dumpTag)) {
- if(d_fullyInited) {
- Dump(dumpTag) << c;
- } else {
- d_dumpCommands.push_back(c.clone());
- }
- }
-}
-
// TODO(#1108): Simplify the error reporting of this method.
Model* SmtEngine::getModel() {
Trace("smt") << "SMT getModel()" << endl;
@@ -3078,7 +3020,7 @@ void SmtEngine::resetAssertions()
// (see solver execution modes in the SMT-LIB standard)
Assert(d_context->getLevel() == 0);
Assert(d_userContext->getLevel() == 0);
- DeleteAndClearCommandVector(d_modelGlobalCommands);
+ d_dumpm->resetAssertions();
return;
}
@@ -3100,7 +3042,7 @@ void SmtEngine::resetAssertions()
Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
d_context->popto(0);
d_userContext->popto(0);
- DeleteAndClearCommandVector(d_modelGlobalCommands);
+ d_dumpm->resetAssertions();
d_userContext->push();
d_context->push();
@@ -3177,28 +3119,6 @@ void SmtEngine::setUserAttribute(const std::string& attr,
d_theoryEngine->setUserAttribute(attr, expr.getNode(), node_values, str_value);
}
-void SmtEngine::setPrintFuncInModel(Expr f, bool p) {
- Trace("setp-model") << "Set printInModel " << f << " to " << p << std::endl;
- for( unsigned i=0; i<d_modelGlobalCommands.size(); i++ ){
- Command * c = d_modelGlobalCommands[i];
- DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
- if(dfc != NULL) {
- if( dfc->getFunction()==f ){
- dfc->setPrintInModel( p );
- }
- }
- }
- for( unsigned i=0; i<d_modelCommands->size(); i++ ){
- Command * c = (*d_modelCommands)[i];
- DeclareFunctionCommand* dfc = dynamic_cast<DeclareFunctionCommand*>(c);
- if(dfc != NULL) {
- if( dfc->getFunction()==f ){
- dfc->setPrintInModel( p );
- }
- }
- }
-}
-
void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
{
// Always check whether the SmtEngine has been initialized (which is done
@@ -3317,6 +3237,8 @@ ResourceManager* SmtEngine::getResourceManager()
return d_resourceManager.get();
}
+DumpManager* SmtEngine::getDumpManager() { return d_dumpm.get(); }
+
void SmtEngine::setSygusConjectureStale()
{
if (d_private->d_sygusConjectureStale)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback