Explicit end marker for models printed in the CVC language (#3934)

Fixes https://github.com/CVC4/cvc4-wishues/issues/9.

When communicating with CVC4 using pipes and the CVC language, it was not possible to determine when all the lines of a model have been printed.

This change adds begin and end markers as the example below:
```
MODEL BEGIN
x : INT = -3;
y : INT = 0;
z : INT = 0;
MODEL END;
```

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 86dd31da2f4e0d238d7508cb96f032793d022dc2..79a8904cdf65f0e3ef7ca518f0cf087b8917b66c 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1174,6 +1174,23 @@ void DeclareFunctionCommandToStream(std::ostream& out,
 
 }  // namespace
 
+void CvcPrinter::toStream(std::ostream& out, const Model& m) const
+{
+  // print the model comments
+  std::stringstream c;
+  m.getComments(c);
+  std::string ln;
+  while (std::getline(c, ln))
+  {
+    out << "; " << ln << std::endl;
+  }
+
+  // print the model
+  out << "MODEL BEGIN" << std::endl;
+  this->Printer::toStream(out, m);
+  out << "MODEL END;" << std::endl;
+}
+
 void CvcPrinter::toStream(std::ostream& out,
                           const Model& model,
                           const Command* command) const

diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index d379af7e340dc40b2ece53da3647d742cd93d190..1694ea1ec449badba920167a663764281c70cfb9 100644 (file)
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -42,6 +42,7 @@ class CvcPrinter : public CVC4::Printer {
                 bool types,
                 size_t dag) const override;
   void toStream(std::ostream& out, const CommandStatus* s) const override;
+  void toStream(std::ostream& out, const Model& m) const override;
 
  private:
   void toStream(

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5eaaf3e6705355c6a764199c6bc9aa6851e362d1..3bcbfa859159e21fe915748194fdd44c3ac51110 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -645,6 +645,7 @@ set(regress_0_tests
   regress0/preprocess/preprocess_14.cvc
   regress0/preprocess/preprocess_15.cvc
   regress0/print_lambda.cvc
+  regress0/print_model.cvc
   regress0/printer/bv_consts_bin.smt2
   regress0/printer/bv_consts_dec.smt2
   regress0/printer/empty_sort.smt2

diff --git a/test/regress/regress0/print_lambda.cvc b/test/regress/regress0/print_lambda.cvc
index 548623954749a2d2dded5ef99bc8ef2a443902c7..99e5ff174055bcaaaf4a5c5ee110b30948bfbbac 100644 (file)
--- a/test/regress/regress0/print_lambda.cvc
+++ b/test/regress/regress0/print_lambda.cvc
@@ -1,7 +1,9 @@
 % SCRUBBER: sed -e 's/f : (INT) -> INT = (LAMBDA(.*:INT): 0);$/f : (INT) -> INT = (LAMBDA(VAR:INT): 0);/'
 % COMMAND-LINE: --produce-models
 % EXPECT: sat
+% EXPECT: MODEL BEGIN
 % EXPECT: f : (INT) -> INT = (LAMBDA(VAR:INT): 0);
+% EXPECT: MODEL END;
 
 f : INT -> INT;
 ASSERT f(1) = 0;

diff --git a/test/regress/regress0/print_model.cvc b/test/regress/regress0/print_model.cvc
new file mode 100644 (file)
index 0000000..0ad9ddf
--- /dev/null
+++ b/test/regress/regress0/print_model.cvc
@@ -0,0 +1,12 @@
+% COMMAND-LINE: --produce-models
+% EXPECT: sat
+% EXPECT: MODEL BEGIN
+% EXPECT: s1 : INT = 2;
+% EXPECT: s2 : INT = 1;
+% EXPECT: MODEL END;
+
+OPTION "produce-models";
+s1, s2 : INT;
+ASSERT s1 = 2;
+CHECKSAT s2 > 0 AND s2 < s1;
+COUNTERMODEL;