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.

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 068c793305e3c381c7b8404445ae9900784d39bb..bfc1dc64a3d691afcdfa9083c3df9a87aa84dca1 100644 (file)
--- 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 376913ebd22bd42bde1bbca76e30a7a00f5df7f4..81445d281f25263dfe6d5d123c2ef4f12d24f2f5 100644 (file)
--- 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 287a8128632a221918082993ac67fdee36f1356b..1e6be22d3908bbeb19c8a2492ea57767f3a59c5e 100644 (file)
--- 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 cfd25fa3b01dc6bdd3d957a8f3ce368ef00fd2a6..2a316409e0ecbb1d1f779735a6f1ceab1b4a1052 100644 (file)
--- 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 56780278b24064148231ae4896918d7d876e6063..ef00b11b09e259087d286faf6a79016dd01654c5 100644 (file)
--- 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 (file)
index 0000000..9d37032
--- /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)