From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Sat, 28 Mar 2020 19:31:37 +0000 (-0500)
Subject: Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)
X-Git-Tag: cvc5-1.0.0~3430
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7f4f4fcf4d42f2c5b60bd62d3fd914f31202f64;p=cvc5.git

Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)
---

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 81ddae6d6..04e8be64b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -330,7 +330,7 @@ api::Term Smt2::getExpressionForNameAndType(const std::string& name,
 
 bool Smt2::getTesterName(api::Term cons, std::string& name)
 {
-  if (v2_6() && strictModeEnabled())
+  if ((v2_6() || sygus_v2()) && strictModeEnabled())
   {
     // 2.6 or above uses indexed tester symbols, if we are in strict mode,
     // we do not automatically define is-cons for constructor cons.
@@ -744,11 +744,17 @@ bool Smt2::sygus() const
   return ilang == language::input::LANG_SYGUS
          || ilang == language::input::LANG_SYGUS_V2;
 }
+
 bool Smt2::sygus_v1() const
 {
   return getLanguage() == language::input::LANG_SYGUS;
 }
 
+bool Smt2::sygus_v2() const
+{
+  return getLanguage() == language::input::LANG_SYGUS_V2;
+}
+
 void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
   // TODO: ???
 }
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 0400c680f..35d088601 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -277,6 +277,8 @@ class Smt2 : public Parser
   bool sygus() const;
   /** Are we using the sygus version 1.0 format? */
   bool sygus_v1() const;
+  /** Are we using the sygus version 2.0 format? */
+  bool sygus_v2() const;
 
   /**
    * Returns true if the language that we are parsing (SMT-LIB version >=2.5
diff --git a/test/regress/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy
index 3d078cc25..90fa57827 100644
--- a/test/regress/regress1/sygus/dt-test-ns.sy
+++ b/test/regress/regress1/sygus/dt-test-ns.sy
@@ -1,6 +1,6 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
-(set-logic LIA)
+(set-logic DTLIA)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
 
@@ -8,6 +8,6 @@
 
 (declare-var x Int)
 
-(constraint (is-cons (f x)))
+(constraint ((_ is cons) (f x)))
 (constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x)))))))
 (check-synth)
diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy
index 83ac8290d..ae2bcc00e 100644
--- a/test/regress/regress1/sygus/list-head-x.sy
+++ b/test/regress/regress1/sygus/list-head-x.sy
@@ -8,6 +8,6 @@
 
 (declare-var x Int)
 
-(constraint (is-cons (f x)))
+(constraint ((_ is cons) (f x)))
 (constraint (= (head (f x)) (+ x 7)))
 (check-synth)