From 8aac04e31310be4fb80fb60df0c88751ee457f6c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 18 Apr 2022 06:30:30 -0700 Subject: [PATCH] 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 --- NEWS.md | 9 +++ src/parser/smt2/Smt2.g | 64 --------------------- test/regress/cli/CMakeLists.txt | 1 - test/regress/cli/regress0/declare-funs.smt2 | 5 -- 4 files changed, 9 insertions(+), 70 deletions(-) delete mode 100644 test/regress/cli/regress0/declare-funs.smt2 diff --git a/NEWS.md b/NEWS.md index 950e2303a..98fc47dcb 100644 --- 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 29262da32..224da51f4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -914,67 +914,6 @@ extendedCommand[std::unique_ptr* 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 dbdd97c83..871fe3b66 100644 --- 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 index 9cbbd8f73..000000000 --- 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 -- 2.30.2