From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Aug 2021 02:34:45 +0000 (-0500)
Subject: Support sygus standard command syntax set-feature (#7040)
X-Git-Tag: cvc5-1.0.0~1359
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=45dd1c4f1695663ce0350ce71d72ec4b1850f043;p=cvc5.git

Support sygus standard command syntax set-feature (#7040)

This currently has no effect other than giving an unsupported warning.

In the future, set-feature will be implemented via the appropriate call to Solver::setOption if necessary.

Fixes #6182.
---

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index f56fc3c90..577aeb0a9 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -585,10 +585,24 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
     }
   | /* check-synth */
     CHECK_SYNTH_TOK
-    { PARSER_STATE->checkThatLogicIsSet(); }
     {
+      PARSER_STATE->checkThatLogicIsSet();
       cmd.reset(new CheckSynthCommand());
     }
+  | /* set-feature */
+    SET_FEATURE_TOK keyword[name] symbolicExpr[expr]
+    {
+      PARSER_STATE->checkThatLogicIsSet();
+      // ":grammars" is defined in the SyGuS version 2.1 standard and is by
+      // default supported, all other features are not.
+      if (name != ":grammars")
+      {
+        std::stringstream ss;
+        ss << "SyGuS feature " << name << " not currently supported";
+        PARSER_STATE->warning(ss.str());
+      }
+      cmd.reset(new EmptyCommand());
+    }
   | command[&cmd]
   ;
 
@@ -2270,7 +2284,7 @@ CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
 INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
-SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options';
+SET_FEATURE_TOK : { PARSER_STATE->sygus() }? 'set-feature';
 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
 SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable';
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6f71e0993..1f2e17a7c 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1262,6 +1262,7 @@ set(regress_0_tests
   regress0/sygus/print-debug.sy
   regress0/sygus/print-define-fun.sy
   regress0/sygus/real-si-all.sy
+  regress0/sygus/setFeature.sy
   regress0/sygus/strings-unconstrained.sy
   regress0/sygus/sygus-no-wf.sy
   regress0/sygus/sygus-uf.sy
diff --git a/test/regress/regress0/sygus/setFeature.sy b/test/regress/regress0/sygus/setFeature.sy
new file mode 100644
index 000000000..443355af3
--- /dev/null
+++ b/test/regress/regress0/sygus/setFeature.sy
@@ -0,0 +1,5 @@
+; REQUIRES: no-competition
+; EXPECT-ERROR: setFeature.sy:5.29: SyGuS feature :recursion not currently supported
+(set-logic ALL)
+(set-feature :grammars true)
+(set-feature :recursion false)