diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-26 15:00:26 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-26 15:00:26 +0000 |
commit | c005a1109982f13427b15e12501f6150fe2f7330 (patch) | |
tree | af2fb375e7018ec25bd1906f8eae8b296a498bf2 /src/smt | |
parent | d4de9caf21439e5b34b0b254e6de7a97c67817b5 (diff) |
don't include internal variables in model output
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 8 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b9025a2ce..7c913578b 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -381,7 +381,7 @@ public: if(Dump.isOn("skolems") && comment != "") { Dump("skolems") << CommentCommand(id + " is " + comment); } - d_smt.addToModelCommandAndDump(c, "skolems"); + d_smt.addToModelCommandAndDump(c, false, "skolems"); } Node applySubstitutions(TNode node) const { @@ -2629,8 +2629,8 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { return SExpr(sexprs); } -void SmtEngine::addToModelCommandAndDump(const Command& c, const char* dumpTag) { - Trace("smt") << "SMT addToModelCommand(" << c << ")" << endl; +void SmtEngine::addToModelCommandAndDump(const Command& c, 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 @@ -2640,7 +2640,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, const char* dumpTag) // 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( !d_fullyInited || options::produceModels() ) { + if(userVisible && (!d_fullyInited || options::produceModels())) { doPendingPops(); d_modelCommands->push_back(c.clone()); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 3a7fbe389..2590bc8e2 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -304,7 +304,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommandAndDump(const Command& c, const char* dumpTag = "declarations"); + void addToModelCommandAndDump(const Command& c, bool userVisible = true, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT |