From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 26 Nov 2012 15:00:26 +0000 (+0000)
Subject: don't include internal variables in model output
X-Git-Tag: cvc5-1.0.0~7562
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c005a1109982f13427b15e12501f6150fe2f7330;p=cvc5.git

don't include internal variables in model output
---

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