From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 13 Apr 2020 21:27:48 +0000 (-0500)
Subject: Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)
X-Git-Tag: cvc5-1.0.0~3382
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b36892dec58f945b7e724395c53a288f9d2d0ef;p=cvc5.git

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 2405b3402..6cba1ce19 100644
--- 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 72621e5ab..7b675d60e 100644
--- 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
index 000000000..e6c7e4748
--- /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)