Remove support for unused `declare-*` commands (#8623)

This commit removes support for
declare-sorts/declare-funs/declare-preds. These commands seem to
be a leftover of an earlier SMT-LIB draft [0]. We only had a test for
declare-funs and Z3 doesn't support declare-funs either.

[0] http://homepage.cs.uiowa.edu/~astump/papers/smt-cmd-lang.pdf

diff --git a/NEWS.md b/NEWS.md
index 950e2303a2f2b9a05b91df92d88e13813ffd1947..98fc47dcb111ee629806101e6bdc1cf8be756143 100644 (file)
--- a/NEWS.md
+++ b/NEWS.md
@@ -1,5 +1,14 @@
 This file contains a summary of important user-visible changes.
 
+cvc5 1.0.1
+==========
+
+**Changes**
+
+- Removed support for non-standard `declare-funs`, `declare-consts`, and
+  `declare-sorts` commands.
+
+
 cvc5 1.0
 =========
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 29262da320d50192041f2ecbb7adc8246e295da0..224da51f44aa6b82d9559cdf16ec739c336ba06e 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -914,67 +914,6 @@ extendedCommand[std::unique_ptr<cvc5::Command>* cmd]
 
     /* Support some of Z3's extended SMT-LIB commands */
 
-  | DECLARE_SORTS_TOK
-    {
-      PARSER_STATE->checkThatLogicIsSet();
-      PARSER_STATE->checkLogicAllowsFreeSorts();
-      seq.reset(new cvc5::CommandSequence());
-    }
-    LPAREN_TOK
-    ( symbol[name,CHECK_UNDECLARED,SYM_SORT]
-      { PARSER_STATE->checkUserSymbol(name);
-        cvc5::Sort type = PARSER_STATE->mkSort(name);
-        seq->addCommand(new DeclareSortCommand(name, 0, type));
-      }
-    )+
-    RPAREN_TOK
-    { cmd->reset(seq.release()); }
-
-  | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { seq.reset(new cvc5::CommandSequence()); }
-    LPAREN_TOK
-    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
-      { PARSER_STATE->checkUserSymbol(name); }
-      nonemptySortList[sorts] RPAREN_TOK
-      { cvc5::Sort tt;
-        if(sorts.size() > 1) {
-          PARSER_STATE->checkLogicAllowsFunctions();
-          // must flatten
-          cvc5::Sort range = sorts.back();
-          sorts.pop_back();
-          tt = PARSER_STATE->mkFlatFunctionType(sorts, range);
-        } else {
-          tt = sorts[0];
-        }
-        // allow overloading
-        cvc5::Term func =
-            PARSER_STATE->bindVar(name, tt, true);
-        seq->addCommand(new DeclareFunctionCommand(name, func, tt));
-        sorts.clear();
-      }
-    )+
-    RPAREN_TOK
-    { cmd->reset(seq.release()); }
-  | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { seq.reset(new cvc5::CommandSequence()); }
-    LPAREN_TOK
-    ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
-      { PARSER_STATE->checkUserSymbol(name); }
-      sortList[sorts] RPAREN_TOK
-      { t = SOLVER->getBooleanSort();
-        if(sorts.size() > 0) {
-          PARSER_STATE->checkLogicAllowsFunctions();
-          t = SOLVER->mkFunctionSort(sorts, t);
-        }
-        // allow overloading
-        cvc5::Term func =
-            PARSER_STATE->bindVar(name, t, true);
-        seq->addCommand(new DeclareFunctionCommand(name, func, t));
-        sorts.clear();
-      }
-    )+
-    RPAREN_TOK
-    { cmd->reset(seq.release()); }
   | // (define-const x U t)
     DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -2215,9 +2154,6 @@ GET_MODEL_TOK : 'get-model';
 BLOCK_MODEL_TOK : 'block-model';
 BLOCK_MODEL_VALUES_TOK : 'block-model-values';
 ECHO_TOK : 'echo';
-DECLARE_SORTS_TOK : 'declare-sorts';
-DECLARE_FUNS_TOK : 'declare-funs';
-DECLARE_PREDS_TOK : 'declare-preds';
 DECLARE_CONST_TOK : 'declare-const';
 DEFINE_CONST_TOK : 'define-const';
 SIMPLIFY_TOK : 'simplify';

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index dbdd97c83f7bcd1c9458213e02a867e0b30aa4f0..871fe3b66781acb552a7f6264361a4e94d995d02 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -591,7 +591,6 @@ set(regress_0_tests
   regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smtv1.smt2
   regress0/decision/wchains010ue.delta02.smtv1.smt2
   regress0/declare-fun-is-match.smt2
-  regress0/declare-funs.smt2
   regress0/define-fun-model.smt2
   regress0/difficulty-simple.smt2
   regress0/difficulty-model-ex.smt2

diff --git a/test/regress/cli/regress0/declare-funs.smt2 b/test/regress/cli/regress0/declare-funs.smt2
deleted file mode 100644 (file)
index 9cbbd8f..0000000
--- a/test/regress/cli/regress0/declare-funs.smt2
+++ /dev/null
@@ -1,5 +0,0 @@
-(set-logic QF_LIA)
-(set-info :status sat)
-(declare-funs ((f Int) (g Int)))
-(assert (= f g))
-(check-sat)
\ No newline at end of file