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 81ddae6d6c64f50fe13ad6e769a4593a3164dc5d..04e8be64b14858a24a92678794497d88c015dcc1 100644 (file)
--- 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 0400c680f52c10c4d812fe3fcd81626048c845a4..35d0886018b4c7d9ebe0d7fc88b602619acaf275 100644 (file)
--- 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 3d078cc2519abb47d86e31c498cecb448484ce5f..90fa57827f55164a6ac1fc687fb34e405af27b28 100644 (file)
--- 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 83ac8290d5fbddbcea626c860e30f22f49a8d6b7..ae2bcc00e8fc042f8e5d67b34bbb5c6e225b68d0 100644 (file)
--- 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)