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 f56fc3c90159ad19e58c17a958cb7e57dcfa1cd9..577aeb0a9bc7f6f61c8df885e43ca5b7a3e5b406 100644 (file)
--- 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 6f71e09936f242d3845766cd6577c3bf6f6f7c6b..1f2e17a7c18cab801e86eb2487cae0daabac20f7 100644 (file)
--- 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 (file)
index 0000000..443355a
--- /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)