From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 30 Nov 2012 21:43:11 +0000 (+0000)
Subject: internal variables (skolems) aren't printed as part of the model
X-Git-Tag: cvc5-1.0.0~7513
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b59646b043cd6d33b48e012cd47dc920d309a002;p=cvc5.git

internal variables (skolems) aren't printed as part of the model

(this commit was certified error- and warning-free by the test-and-commit script.)
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index a9d439a0f..c375c76c4 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -828,6 +828,10 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
     }
   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
     Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
+    if(n.getKind() == kind::SKOLEM) {
+      // don't print out internal stuff
+      return;
+    }
     TypeNode tn = n.getType();
     out << n << " : ";
     /* Boolean terms functionality needs to be merged in
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ae589eba6..2b2824334 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -563,6 +563,10 @@ void Smt2Printer::toStream(std::ostream& out, Model& m, const Command* c) const
     }
   } else if(dynamic_cast<const DeclareFunctionCommand*>(c) != NULL) {
     Node n = Node::fromExpr( ((const DeclareFunctionCommand*)c)->getFunction() );
+    if(n.getKind() == kind::SKOLEM) {
+      // don't print out internal stuff
+      return;
+    }
     Node val = tm.getValue( n );
     if(val.getKind() == kind::LAMBDA) {
       out << "(define-fun " << n << " " << val[0]