Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)

A recent change made it so that defined functions would print as the anonymous lambda corresponding to their definition if the SyGuS v1 parser was used. This was caused by comparison with the wrong kind in the new API.

Notice that the v2 parser does not have this issue.

This also adds a regression to ensure this behavior is maintained by the SyGuS v2 parser.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2405b3402c11087e37195930c333dfff221c6a43..6cba1ce1903f6e021c7ffa020098d95ce8b15221 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1293,7 +1293,7 @@ void Smt2::mkSygusDatatype(api::DatatypeDecl& dt,
           // the given name.
           spc = std::make_shared<printer::SygusNamedPrintCallback>(cnames[i]);
         }
-        else if (!sop.isNull() && sop.getKind() == api::VARIABLE)
+        else if (!sop.isNull() && sop.getKind() == api::CONSTANT)
         {
           Debug("parser-sygus") << "--> Defined function " << ops[i]
                                 << std::endl;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 72621e5abc1b9b8de475bb511c89c1b8bf34902e..7b675d60ec33a3d0ead77c4a1980db5fde44c14f 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1007,6 +1007,7 @@ set(regress_0_tests
   regress0/sygus/parse-bv-let.sy
   regress0/sygus/pbe-pred-contra.sy
   regress0/sygus/pLTL-sygus-syntax-err.sy
+  regress0/sygus/print-define-fun.sy
   regress0/sygus/real-si-all.sy
   regress0/sygus/sygus-no-wf.sy
   regress0/sygus/sygus-uf.sy

diff --git a/test/regress/regress0/sygus/print-define-fun.sy b/test/regress/regress0/sygus/print-define-fun.sy
new file mode 100644 (file)
index 0000000..e6c7e47
--- /dev/null
+++ b/test/regress/regress0/sygus/print-define-fun.sy
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --lang=sygus2
+; EXPECT: unsat
+; EXPECT: (define-fun g ((x Int)) Int (f 0))
+(set-logic LIA)
+(define-fun f ((x Int)) Int (+ x 1))
+(synth-fun g ((x Int)) Int ((Start Int)) ((Start Int ((f 0)))))
+(check-synth)