From 3255e4335f25f35318a41f174ec15a28b0f0520d Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 8 Dec 2020 14:10:10 -0600
Subject: [PATCH] Fix a bug with synth-fun printer (#5512)

This PR fixes #5448. SynthFunCommand::toStream used to call d_grammar->resolve even when d_grammar is a nullptr. This PR fixes the issue and modifies the signature of Printer::toStreamCmdSynthFun to make it clear that grammar is an optional argument.
---
 src/printer/printer.h                        |  2 +-
 src/printer/smt2/smt2_printer.cpp            |  2 +-
 src/printer/smt2/smt2_printer.h              | 13 +++++++------
 src/smt/command.cpp                          |  3 ++-
 test/regress/CMakeLists.txt                  |  1 +
 test/regress/regress0/sygus/issue5512-vvv.sy | 17 +++++++++++++++++
 6 files changed, 29 insertions(+), 9 deletions(-)
 create mode 100644 test/regress/regress0/sygus/issue5512-vvv.sy

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 068c79330..bfc1dc64a 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -135,7 +135,7 @@ class Printer
                                    const std::vector<Node>& vars,
                                    TypeNode range,
                                    bool isInv,
-                                   TypeNode sygusType) const;
+                                   TypeNode sygusType = TypeNode::null()) const;
 
   /** Print constraint command */
   virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 376913ebd..81445d281 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -2043,7 +2043,7 @@ void Smt2Printer::toStreamCmdSynthFun(std::ostream& out,
   }
   out << '\n';
   // print grammar, if any
-  if (sygusType != TypeNode::null())
+  if (!sygusType.isNull())
   {
     toStreamSygusGrammar(out, sygusType);
   }
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 287a81286..1e6be22d3 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -117,12 +117,13 @@ class Smt2Printer : public CVC4::Printer
                              TypeNode type) const override;
 
   /** Print synth-fun command */
-  void toStreamCmdSynthFun(std::ostream& out,
-                           const std::string& sym,
-                           const std::vector<Node>& vars,
-                           TypeNode range,
-                           bool isInv,
-                           TypeNode sygusType) const override;
+  void toStreamCmdSynthFun(
+      std::ostream& out,
+      const std::string& sym,
+      const std::vector<Node>& vars,
+      TypeNode range,
+      bool isInv,
+      TypeNode sygusType = TypeNode::null()) const override;
 
   /** Print constraint command */
   void toStreamCmdConstraint(std::ostream& out, Node n) const override;
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cfd25fa3b..2a316409e 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -689,7 +689,8 @@ void SynthFunCommand::toStream(std::ostream& out,
       nodeVars,
       d_sort.getTypeNode(),
       d_isInv,
-      d_grammar->resolve().getTypeNode());
+      d_grammar == nullptr ? TypeNode::null()
+                           : d_grammar->resolve().getTypeNode());
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 56780278b..ef00b11b0 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1091,6 +1091,7 @@ set(regress_0_tests
   regress0/sygus/issue3645-grammar-sets.smt2
   regress0/sygus/issue4383-cache-fv-id.sy
   regress0/sygus/issue4790-dtd.sy
+  regress0/sygus/issue5512-vvv.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
   regress0/sygus/no-logic.sy
diff --git a/test/regress/regress0/sygus/issue5512-vvv.sy b/test/regress/regress0/sygus/issue5512-vvv.sy
new file mode 100644
index 000000000..9d37032ac
--- /dev/null
+++ b/test/regress/regress0/sygus/issue5512-vvv.sy
@@ -0,0 +1,17 @@
+; COMMAND-LINE: -vvv --sygus-out=status --check-synth-sol --check-abducts
+; SCRUBBER: sed -e 's/.*//g'
+; EXIT: 0
+
+; This regression ensures that printing Sygus commands with option -vvv does not
+; crash CVC4
+
+(set-logic UF)
+(declare-var x Bool)
+(synth-fun f ((x Bool)) Bool ((Start Bool)) ((Start Bool (true))))
+(synth-inv inv-f ((x Bool)))
+(define-fun pre-f ((x Bool)) Bool true)
+(define-fun trans-f ((x Bool) (x! Bool)) Bool true)
+(define-fun post-f ((x Bool)) Bool true)
+(inv-constraint inv-f pre-f trans-f post-f)
+(constraint true)
+(check-synth)
-- 
2.30.2