From: Andrew Reynolds Date: Thu, 25 Jun 2020 18:36:09 +0000 (-0500) Subject: Remove sygus1 parser (#4651) X-Git-Tag: cvc5-1.0.0~3174 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8374a8dd4bf740bf26748c1dbe1616ad798cf624;p=cvc5.git Remove sygus1 parser (#4651) We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard). As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script. This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR. FYI @abdoo8080 . --- diff --git a/src/options/language.cpp b/src/options/language.cpp index c03ae1cbb..b00d5c102 100644 --- a/src/options/language.cpp +++ b/src/options/language.cpp @@ -29,15 +29,12 @@ Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6; bool isInputLang_smt2(InputLanguage lang) { - return (lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END) - || lang == input::LANG_Z3STR; + return lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END; } bool isOutputLang_smt2(OutputLanguage lang) { - return (lang >= output::LANG_SMTLIB_V2_0 - && lang <= output::LANG_SMTLIB_V2_END) - || lang == output::LANG_Z3STR; + return lang >= output::LANG_SMTLIB_V2_0 && lang <= output::LANG_SMTLIB_V2_END; } bool isInputLang_smt2_5(InputLanguage lang, bool exact) @@ -70,12 +67,12 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact) bool isInputLangSygus(InputLanguage lang) { - return lang == input::LANG_SYGUS_V1 || lang == input::LANG_SYGUS_V2; + return lang == input::LANG_SYGUS_V2; } bool isOutputLangSygus(OutputLanguage lang) { - return lang == output::LANG_SYGUS_V1 || lang == output::LANG_SYGUS_V2; + return lang == output::LANG_SYGUS_V2; } InputLanguage toInputLanguage(OutputLanguage language) { @@ -85,8 +82,6 @@ InputLanguage toInputLanguage(OutputLanguage language) { case output::LANG_SMTLIB_V2_6: case output::LANG_TPTP: case output::LANG_CVC4: - case output::LANG_Z3STR: - case output::LANG_SYGUS_V1: case output::LANG_SYGUS_V2: // these entries directly correspond (by design) return InputLanguage(int(language)); @@ -107,8 +102,6 @@ OutputLanguage toOutputLanguage(InputLanguage language) { case input::LANG_SMTLIB_V2_6: case input::LANG_TPTP: case input::LANG_CVC4: - case input::LANG_Z3STR: - case input::LANG_SYGUS_V1: case input::LANG_SYGUS_V2: // these entries directly correspond (by design) return OutputLanguage(int(language)); @@ -152,13 +145,6 @@ OutputLanguage toOutputLanguage(std::string language) { return output::LANG_SMTLIB_V2_6; } else if(language == "tptp" || language == "LANG_TPTP") { return output::LANG_TPTP; - } else if(language == "z3str" || language == "z3-str" || - language == "LANG_Z3STR") { - return output::LANG_Z3STR; - } - else if (language == "sygus1" || language == "LANG_SYGUS_V1") - { - return output::LANG_SYGUS_V1; } else if (language == "sygus" || language == "LANG_SYGUS" || language == "sygus2" || language == "LANG_SYGUS_V2") @@ -195,13 +181,6 @@ InputLanguage toInputLanguage(std::string language) { return input::LANG_SMTLIB_V2_6; } else if(language == "tptp" || language == "LANG_TPTP") { return input::LANG_TPTP; - } else if(language == "z3str" || language == "z3-str" || - language == "LANG_Z3STR") { - return input::LANG_Z3STR; - } - else if (language == "sygus1" || language == "LANG_SYGUS_V1") - { - return input::LANG_SYGUS_V1; } else if (language == "sygus2" || language == "LANG_SYGUS_V2") { diff --git a/src/options/language.h b/src/options/language.h index 7dc1cf987..0a0f63ca6 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -56,10 +56,6 @@ enum CVC4_PUBLIC Language LANG_TPTP, /** The CVC4 input language */ LANG_CVC4, - /** The Z3-str input language */ - LANG_Z3STR, - /** The SyGuS input language version 1.0 */ - LANG_SYGUS_V1, /** The SyGuS input language version 2.0 */ LANG_SYGUS_V2, @@ -91,10 +87,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_CVC4: out << "LANG_CVC4"; break; - case LANG_Z3STR: - out << "LANG_Z3STR"; - break; - case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break; case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; default: out << "undefined_input_language"; @@ -132,10 +124,6 @@ enum CVC4_PUBLIC Language LANG_TPTP = input::LANG_TPTP, /** The CVC4 output language */ LANG_CVC4 = input::LANG_CVC4, - /** The Z3-str output language */ - LANG_Z3STR = input::LANG_Z3STR, - /** The sygus output language version 1.0 */ - LANG_SYGUS_V1 = input::LANG_SYGUS_V1, /** The sygus output language version 2.0 */ LANG_SYGUS_V2 = input::LANG_SYGUS_V2, @@ -167,10 +155,6 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_CVC4: out << "LANG_CVC4"; break; - case LANG_Z3STR: - out << "LANG_Z3STR"; - break; - case LANG_SYGUS_V1: out << "LANG_SYGUS_V1"; break; case LANG_SYGUS_V2: out << "LANG_SYGUS_V2"; break; case LANG_AST: out << "LANG_AST"; diff --git a/src/options/language.i b/src/options/language.i index 639cb0bda..7f81ea7c6 100644 --- a/src/options/language.i +++ b/src/options/language.i @@ -26,8 +26,6 @@ namespace CVC4 { %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP; %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; -%rename(INPUT_LANG_Z3STR) CVC4::language::input::LANG_Z3STR; -%rename(INPUT_LANG_SYGUS_V1) CVC4::language::input::LANG_SYGUS_V1; %rename(INPUT_LANG_SYGUS_V2) CVC4::language::input::LANG_SYGUS_V2; %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO; @@ -39,8 +37,6 @@ namespace CVC4 { %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4; %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; %rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX; -%rename(OUTPUT_LANG_Z3STR) CVC4::language::output::LANG_Z3STR; -%rename(OUTPUT_LANG_SYGUS_V1) CVC4::language::output::LANG_SYGUS_V1; %rename(OUTPUT_LANG_SYGUS_V2) CVC4::language::output::LANG_SYGUS_V2; %include "options/language.h" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index a49ede98e..234ddd5b4 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -418,7 +418,6 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ tptp TPTP format (cnf, fof and tff)\n\ - sygus1 SyGuS version 1.0 \n\ sygus | sygus2 SyGuS version 2.0\n\ \n\ Languages currently supported as arguments to the --output-lang option:\n\ @@ -430,7 +429,6 @@ Languages currently supported as arguments to the --output-lang option:\n\ smt2.5 | smtlib2.5 SMT-LIB format 2.5\n\ smt2.6 | smtlib2.6 SMT-LIB format 2.6 with support for the strings standard\n\ tptp TPTP format\n\ - z3str SMT-LIB 2.0 with Z3-str string constraints\n\ ast internal format (simple syntax trees)\n\ "; diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 273b9fd93..1d5190e3f 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -247,7 +247,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre break; } - case LANG_SYGUS_V1: case LANG_SYGUS_V2: input = new SygusInput(inputStream); break; case LANG_TPTP: diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index 729d3b9a3..f65618267 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -89,7 +89,6 @@ Parser* ParserBuilder::build() Parser* parser = NULL; switch (d_lang) { - case language::input::LANG_SYGUS_V1: case language::input::LANG_SYGUS_V2: parser = new Smt2(d_solver, input, d_strictMode, d_parseOnly); break; diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index a11b9670b..3e8234a86 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -305,14 +305,7 @@ command [std::unique_ptr* cmd] PARSER_STATE->checkLogicAllowsFunctions(); } // we allow overloading for function declarations - if (PARSER_STATE->sygus_v1()) - { - // it is a higher-order universal variable - api::Term func = PARSER_STATE->bindBoundVar(name, t); - cmd->reset( - new DeclareSygusFunctionCommand(name, func.getExpr(), t.getType())); - } - else if( PARSER_STATE->sygus() ) + if( PARSER_STATE->sygus() ) { PARSER_STATE->parseErrorLogic("declare-fun are not allowed in sygus " "version 2.0"); @@ -567,39 +560,7 @@ sygusCommand returns [std::unique_ptr cmd] api::Term var = PARSER_STATE->bindBoundVar(name, t); cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType())); } - | /* declare-primed-var */ - DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } - symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(name); } - sortSymbol[t,CHECK_DECLARED] - { - // spurious command, we do not need to create a variable. We only keep - // track of the command for sanity checking / dumping - cmd.reset(new DeclareSygusPrimedVarCommand(name, t.getType())); - } - | /* synth-fun */ - ( SYNTH_FUN_V1_TOK { isInv = false; } - | SYNTH_INV_V1_TOK { isInv = true; range = SOLVER->getBooleanSort(); } - ) - { PARSER_STATE->checkThatLogicIsSet(); } - symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - ( sortSymbol[range,CHECK_DECLARED] )? - { - synthFunFactory.reset(new Smt2::SynthFunFactory( - PARSER_STATE, fun, isInv, range, sortedVarNames)); - } - ( - // optionally, read the sygus grammar - // - // `grammar` specifies the required grammar for the function to - // synthesize, expressed as a type - sygusGrammarV1[grammar, synthFunFactory->getSygusVars(), fun] - )? - { - cmd = synthFunFactory->mkCommand(grammar); - } | /* synth-fun */ ( SYNTH_FUN_TOK { isInv = false; } | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); } @@ -647,292 +608,6 @@ sygusCommand returns [std::unique_ptr cmd] | command[&cmd] ; -/** Reads a sygus grammar - * - * The resulting sygus datatype encoding the grammar is stored in ret. - * The argument sygus_vars indicates the sygus bound variable list, which is - * the argument list of the function-to-synthesize (or null if the grammar - * has bound variables). - * The argument fun is a unique identifier to avoid naming clashes for the - * datatypes constructed by this call. - */ -sygusGrammarV1[CVC4::api::Sort & ret, - const std::vector& sygus_vars, - const std::string& fun] -@declarations -{ - CVC4::api::Sort t; - std::string name; - unsigned startIndex = 0; - std::vector> sgts; - std::vector datatypes; - std::vector sorts; - std::vector> ops; - std::vector> cnames; - std::vector>> cargs; - std::vector allow_const; - std::vector> unresolved_gterm_sym; - std::map sygus_to_builtin; - std::map sygus_to_builtin_expr; -} - : LPAREN_TOK { PARSER_STATE->pushScope(); } - (LPAREN_TOK - symbol[name, CHECK_NONE, SYM_VARIABLE] sortSymbol[t, CHECK_DECLARED] { - if (name == "Start") - { - startIndex = datatypes.size(); - } - sgts.push_back(std::vector()); - sgts.back().push_back(CVC4::SygusGTerm()); - PARSER_STATE->pushSygusDatatypeDef(t, - name, - datatypes, - sorts, - ops, - cnames, - cargs, - allow_const, - unresolved_gterm_sym); - api::Sort unres_t; - if (!PARSER_STATE->isUnresolvedType(name)) - { - // if not unresolved, must be undeclared - Debug("parser-sygus") << "Make unresolved type : " << name - << std::endl; - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT); - unres_t = PARSER_STATE->mkUnresolvedType(name); - } - else - { - Debug("parser-sygus") << "Get sort : " << name << std::endl; - unres_t = PARSER_STATE->getSort(name); - } - sygus_to_builtin[unres_t] = t; - Debug("parser-sygus") << "--- Read sygus grammar " << name - << " under function " << fun << "..." - << std::endl - << " type to resolve " << unres_t << std::endl - << " builtin type " << t << std::endl; - } - // Note the official spec for NTDef is missing the ( parens ) - // but they are necessary to parse SyGuS examples - LPAREN_TOK(sygusGTerm[sgts.back().back(), fun] { - sgts.back().push_back(CVC4::SygusGTerm()); - }) - + RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK) - + RPAREN_TOK - { - unsigned numSTerms = sgts.size(); - Debug("parser-sygus") << "--- Process " << numSTerms << " sygus gterms..." - << std::endl; - for (unsigned i = 0; i < numSTerms; i++) - { - for (unsigned j = 0, size = sgts[i].size(); j < size; j++) - { - api::Sort sub_ret; - PARSER_STATE->processSygusGTerm(sgts[i][j], - i, - datatypes, - sorts, - ops, - cnames, - cargs, - allow_const, - unresolved_gterm_sym, - sygus_vars, - sygus_to_builtin, - sygus_to_builtin_expr, - sub_ret); - } - } - // swap index if necessary - Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl; - unsigned ndatatypes = datatypes.size(); - for (unsigned i = 0; i < ndatatypes; i++) - { - Debug("parser-sygus") << "..." << datatypes[i].getName() - << " has builtin sort " << sorts[i] << std::endl; - } - api::Term bvl; - if (!sygus_vars.empty()) - { - bvl = MK_TERM(api::BOUND_VAR_LIST, sygus_vars); - } - for (unsigned i = 0; i < ndatatypes; i++) - { - Debug("parser-sygus") << "...make " << datatypes[i].getName() - << " with builtin sort " << sorts[i] << std::endl; - if (sorts[i].isNull()) - { - PARSER_STATE->parseError( - "Internal error : could not infer " - "builtin sort for nested gterm."); - } - datatypes[i].getDatatype().setSygus( - sorts[i].getType(), bvl.getExpr(), allow_const[i], false); - PARSER_STATE->mkSygusDatatype(datatypes[i], - ops[i], - cnames[i], - cargs[i], - unresolved_gterm_sym[i], - sygus_to_builtin); - } - PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, ops); - PARSER_STATE->popScope(); - Debug("parser-sygus") << "--- Make " << ndatatypes - << " mutual datatypes..." << std::endl; - for (unsigned i = 0; i < ndatatypes; i++) - { - Debug("parser-sygus") << " " << i << " : " << datatypes[i].getName() - << std::endl; - } - - std::vector dtypes; - dtypes.reserve(ndatatypes); - - for (api::DatatypeDecl i : datatypes) - { - dtypes.push_back(i.getDatatype()); - } - - std::set tset = - api::sortSetToTypes(PARSER_STATE->getUnresolvedSorts()); - - std::vector datatypeTypes = - SOLVER->getExprManager()->mkMutualDatatypeTypes( - dtypes, tset, ExprManager::DATATYPE_FLAG_PLACEHOLDER); - - PARSER_STATE->getUnresolvedSorts().clear(); - - ret = api::Sort(SOLVER, datatypeTypes[0]); - }; - -// SyGuS grammar term. -// -// fun is the name of the synth-fun this grammar term is for. -// This method adds N operators to ops[index], N names to cnames[index] and N -// type argument vectors to cargs[index] (where typically N=1) -// This method may also add new elements pairwise into -// datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. -sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] -@declarations { - std::string name, name2; - CVC4::api::Kind k; - CVC4::api::Sort t; - std::string sname; - std::vector< CVC4::api::Term > let_vars; - std::string s; - CVC4::api::Term atomTerm; -} - : LPAREN_TOK - //read operator - ( SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_constant; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar constant." << std::endl; - } - | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_variable; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar variable." << std::endl; - } - | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_local_variable; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar local variable...ignore." - << std::endl; - } - | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_input_variable; - sgt.d_type = t; - Debug("parser-sygus") << "Sygus grammar (input) variable." - << std::endl; - } - | symbol[name,CHECK_NONE,SYM_VARIABLE] { - bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); - if(isBuiltinOperator) { - Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " - << name << std::endl; - k = PARSER_STATE->getOperatorKind(name); - sgt.d_name = api::kindToString(k); - sgt.d_gterm_type = SygusGTerm::gterm_op; - sgt.d_op.d_kind = k; - }else{ - // what is this sygus term trying to accomplish here, if the - // symbol isn't yet declared?! probably the following line will - // fail, but we need an operator to continue here.. - Debug("parser-sygus") - << "Sygus grammar " << fun << " : op (declare=" - << PARSER_STATE->isDeclared(name) << ") : " << name - << std::endl; - if (!PARSER_STATE->isDeclared(name)) - { - PARSER_STATE->parseError("Functions in sygus grammars must be " - "defined."); - } - sgt.d_name = name; - sgt.d_gterm_type = SygusGTerm::gterm_op; - sgt.d_op.d_expr = PARSER_STATE->getVariable(name) ; - } - } - ) - //read arguments - { Debug("parser-sygus") << "Read arguments under " << sgt.d_name - << std::endl; - sgt.addChild(); - } - ( sygusGTerm[sgt.d_children.back(), fun] - { Debug("parser-sygus") << "Finished read argument #" - << sgt.d_children.size() << "..." << std::endl; - sgt.addChild(); - } - )* - RPAREN_TOK { - //pop last child index - sgt.d_children.pop_back(); - } - | termAtomic[atomTerm] - { - Debug("parser-sygus") << "Sygus grammar " << fun << " : atomic " - << "expression " << atomTerm << std::endl; - std::stringstream ss; - ss << atomTerm; - sgt.d_op.d_expr = atomTerm; - sgt.d_name = ss.str(); - sgt.d_gterm_type = SygusGTerm::gterm_op; - } - | symbol[name,CHECK_NONE,SYM_VARIABLE] - { - if( name[0] == '-' ){ //hack for unary minus - Debug("parser-sygus") << "Sygus grammar " << fun - << " : unary minus integer literal " << name - << std::endl; - sgt.d_op.d_expr = SOLVER->mkReal(name); - sgt.d_name = name; - sgt.d_gterm_type = SygusGTerm::gterm_op; - }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ - Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " - << name << std::endl; - sgt.d_op.d_expr = PARSER_STATE->getExpressionForName(name); - sgt.d_name = name; - sgt.d_gterm_type = SygusGTerm::gterm_op; - }else{ - if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ - Debug("parser-sygus") << "Sygus grammar " << fun - << " : nested sort " << name << std::endl; - sgt.d_type = PARSER_STATE->getSort(name); - sgt.d_gterm_type = SygusGTerm::gterm_nested_sort; - }else{ - Debug("parser-sygus") << "Sygus grammar " << fun - << " : unresolved symbol " << name - << std::endl; - sgt.d_gterm_type = SygusGTerm::gterm_unresolved; - sgt.d_name = name; - } - } - } - ; - /** Reads a sygus grammar in the sygus version 2 format * @@ -1780,7 +1455,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] expr = PARSER_STATE->applyParseOp(p, args); } | /* a let or sygus let binding */ - LPAREN_TOK ( + LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(true); } ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] @@ -1796,24 +1471,7 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] } else { names.insert(name); } - binders.push_back(std::make_pair(name, expr)); } )+ | - SYGUS_LET_TOK LPAREN_TOK - { PARSER_STATE->pushScope(true); } - ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] - sortSymbol[type,CHECK_DECLARED] - term[expr, f2] - RPAREN_TOK - // this is a parallel let, so we have to save up all the contributions - // of the let and define them only later on - { if(names.count(name) == 1) { - std::stringstream ss; - ss << "warning: symbol `" << name << "' bound multiple times by let;" - << " the last binding will be used, shadowing earlier ones"; - PARSER_STATE->warning(ss.str()); - } else { - names.insert(name); - } - binders.push_back(std::make_pair(name, expr)); } )+ ) + binders.push_back(std::make_pair(name, expr)); } )+ { // now implement these bindings for (const std::pair& binder : binders) { @@ -2398,8 +2056,9 @@ sortSymbol[CVC4::api::Sort& t, CVC4::parser::DeclarationCheck check] | LPAREN_TOK (INDEX_TOK {indexed = true;} | {indexed = false;}) symbol[name,CHECK_NONE,SYM_SORT] ( nonemptyNumeralList[numerals] - { // allow sygus inputs to elide the `_' - if( !indexed && !PARSER_STATE->sygus_v1() ) { + { + if (!indexed) + { std::stringstream ss; ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name << " ...)"; @@ -2615,8 +2274,7 @@ GET_UNSAT_CORE_TOK : 'get-unsat-core'; EXIT_TOK : 'exit'; RESET_TOK : { PARSER_STATE->v2_5() }? 'reset'; RESET_ASSERTIONS_TOK : 'reset-assertions'; -LET_TOK : { !PARSER_STATE->sygus_v1() }? 'let'; -SYGUS_LET_TOK : { PARSER_STATE->sygus_v1() }? 'let'; +LET_TOK : 'let'; ATTRIBUTE_TOK : '!'; LPAREN_TOK : '('; RPAREN_TOK : ')'; @@ -2660,20 +2318,15 @@ GET_ABDUCT_TOK : 'get-abduct'; DECLARE_HEAP : 'declare-heap'; // SyGuS commands -SYNTH_FUN_V1_TOK : { PARSER_STATE->sygus_v1() }?'synth-fun'; -SYNTH_FUN_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1() }?'synth-fun'; -SYNTH_INV_V1_TOK : { PARSER_STATE->sygus_v1()}?'synth-inv'; -SYNTH_INV_TOK : { PARSER_STATE->sygus() && !PARSER_STATE->sygus_v1()}?'synth-inv'; +SYNTH_FUN_TOK : { PARSER_STATE->sygus() }?'synth-fun'; +SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv'; CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth'; DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var'; -DECLARE_PRIMED_VAR_TOK : { PARSER_STATE->sygus_v1() }?'declare-primed-var'; CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint'; INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint'; SET_OPTIONS_TOK : { PARSER_STATE->sygus() }? 'set-options'; SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant'; SYGUS_VARIABLE_TOK : { PARSER_STATE->sygus() }? 'Variable'; -SYGUS_INPUT_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'InputVariable'; -SYGUS_LOCAL_VARIABLE_TOK : { PARSER_STATE->sygus_v1() }? 'LocalVariable'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a7eb218af..68b1945fc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -568,16 +568,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) } } - if (sygus_v1()) - { - // non-smt2-standard sygus logic names go here (http://sygus.seas.upenn.edu/files/sygus.pdf Section 3.2) - if(name == "Arrays") { - name = "A"; - }else if(name == "Reals") { - name = "LRA"; - } - } - d_logicSet = true; d_logic = name; @@ -752,13 +742,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) bool Smt2::sygus() const { InputLanguage ilang = getLanguage(); - return ilang == language::input::LANG_SYGUS_V1 - || ilang == language::input::LANG_SYGUS_V2; -} - -bool Smt2::sygus_v1() const -{ - return getLanguage() == language::input::LANG_SYGUS_V1; + return ilang == language::input::LANG_SYGUS_V2; } bool Smt2::sygus_v2() const @@ -899,538 +883,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name) return d_solver->mkAbstractValue(name.substr(1)); } -void Smt2::mkSygusConstantsForType(const api::Sort& type, - std::vector& ops) -{ - if( type.isInteger() ){ - ops.push_back(d_solver->mkReal(0)); - ops.push_back(d_solver->mkReal(1)); - }else if( type.isBitVector() ){ - uint32_t sz = type.getBVSize(); - ops.push_back(d_solver->mkBitVector(sz, 0)); - ops.push_back(d_solver->mkBitVector(sz, 1)); - }else if( type.isBoolean() ){ - ops.push_back(d_solver->mkTrue()); - ops.push_back(d_solver->mkFalse()); - } - //TODO : others? -} - -// This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) -// This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. -void Smt2::processSygusGTerm( - CVC4::SygusGTerm& sgt, - int index, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym, - const std::vector& sygus_vars, - std::map& sygus_to_builtin, - std::map& sygus_to_builtin_expr, - api::Sort& ret, - bool isNested) -{ - if (sgt.d_gterm_type == SygusGTerm::gterm_op) - { - Debug("parser-sygus") << "Add " << sgt.d_op << " to datatype " - << index << std::endl; - api::Kind oldKind; - api::Kind newKind = api::UNDEFINED_KIND; - //convert to UMINUS if one child of MINUS - if (sgt.d_children.size() == 1 && sgt.d_op.d_kind == api::MINUS) - { - oldKind = api::MINUS; - newKind = api::UMINUS; - } - if (newKind != api::UNDEFINED_KIND) - { - Debug("parser-sygus") - << "Replace " << sgt.d_op.d_kind << " with " << newKind << std::endl; - sgt.d_op.d_kind = newKind; - std::string oldName = api::kindToString(oldKind); - std::string newName = api::kindToString(newKind); - size_t pos = 0; - if((pos = sgt.d_name.find(oldName, pos)) != std::string::npos){ - sgt.d_name.replace(pos, oldName.length(), newName); - } - } - ops[index].push_back(sgt.d_op); - cnames[index].push_back( sgt.d_name ); - cargs[index].push_back(std::vector()); - for( unsigned i=0; i consts; - mkSygusConstantsForType( sgt.d_type, consts ); - Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl; - for( unsigned i=0; i()); - } - allow_const[index] = true; - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_variable - || sgt.d_gterm_type == SygusGTerm::gterm_input_variable) - { - if( sgt.getNumChildren()!=0 ){ - parseError("Bad syntax for Sygus Variable."); - } - Debug("parser-sygus") << "...process " << sygus_vars.size() << " variables." << std::endl; - for( unsigned i=0; i()); - } - } - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_nested_sort) - { - ret = sgt.d_type; - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_unresolved) - { - if( isNested ){ - if( isUnresolvedType(sgt.d_name) ){ - ret = getSort(sgt.d_name); - }else{ - //nested, unresolved symbol...fail - std::stringstream ss; - ss << "Cannot handle nested unresolved symbol " << sgt.d_name << std::endl; - parseError(ss.str()); - } - }else{ - //will resolve when adding constructors - unresolved_gterm_sym[index].push_back(sgt.d_name); - } - } - else if (sgt.d_gterm_type == SygusGTerm::gterm_ignore) - { - // do nothing - } -} - -bool Smt2::pushSygusDatatypeDef( - api::Sort t, - std::string& dname, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym) -{ - sorts.push_back(t); - datatypes.push_back(d_solver->mkDatatypeDecl(dname)); - ops.push_back(std::vector()); - cnames.push_back(std::vector()); - cargs.push_back(std::vector>()); - allow_const.push_back(false); - unresolved_gterm_sym.push_back(std::vector< std::string >()); - return true; -} - -bool Smt2::popSygusDatatypeDef( - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym) -{ - sorts.pop_back(); - datatypes.pop_back(); - ops.pop_back(); - cnames.pop_back(); - cargs.pop_back(); - allow_const.pop_back(); - unresolved_gterm_sym.pop_back(); - return true; -} - -api::Sort Smt2::processSygusNestedGTerm( - int sub_dt_index, - std::string& sub_dname, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym, - std::map& sygus_to_builtin, - std::map& sygus_to_builtin_expr, - api::Sort sub_ret) -{ - api::Sort t = sub_ret; - Debug("parser-sygus") << "Argument is "; - if( t.isNull() ){ - //then, it is the datatype we constructed, which should have a single constructor - t = mkUnresolvedType(sub_dname); - Debug("parser-sygus") << "inline flattening of (auxiliary, local) datatype " << t << std::endl; - Debug("parser-sygus") << ": to compute type, construct ground term witnessing the grammar, #cons=" << cargs[sub_dt_index].size() << std::endl; - if( cargs[sub_dt_index].empty() ){ - parseError(std::string("Internal error : datatype for nested gterm does not have a constructor.")); - } - ParseOp op = ops[sub_dt_index][0]; - api::Sort curr_t; - if (!op.d_expr.isNull() - && (op.d_expr.isConst() || cargs[sub_dt_index][0].empty())) - { - api::Term sop = op.d_expr; - curr_t = sop.getSort(); - Debug("parser-sygus") - << ": it is constant/0-arg cons " << sop << " with type " - << sop.getSort() << ", debug=" << sop.isConst() << " " - << cargs[sub_dt_index][0].size() << std::endl; - // only cache if it is a singleton datatype (has unique expr) - if (ops[sub_dt_index].size() == 1) - { - sygus_to_builtin_expr[t] = sop; - // store that term sop has dedicated sygus type t - if (d_sygus_bound_var_type.find(sop) == d_sygus_bound_var_type.end()) - { - d_sygus_bound_var_type[sop] = t; - } - } - } - else - { - std::vector children; - for( unsigned i=0; i::iterator it = - sygus_to_builtin_expr.find(cargs[sub_dt_index][0][i]); - if( it==sygus_to_builtin_expr.end() ){ - if( sygus_to_builtin.find( cargs[sub_dt_index][0][i] )==sygus_to_builtin.end() ){ - std::stringstream ss; - ss << "Missing builtin type for type " << cargs[sub_dt_index][0][i] << "!" << std::endl; - ss << "Builtin types are currently : " << std::endl; - for (std::map::iterator itb = - sygus_to_builtin.begin(); - itb != sygus_to_builtin.end(); - ++itb) - { - ss << " " << itb->first << " -> " << itb->second << std::endl; - } - parseError(ss.str()); - } - api::Sort bt = sygus_to_builtin[cargs[sub_dt_index][0][i]]; - Debug("parser-sygus") << ": child " << i << " introduce type elem for " << cargs[sub_dt_index][0][i] << " " << bt << std::endl; - std::stringstream ss; - ss << t << "_x_" << i; - api::Term bv = bindBoundVar(ss.str(), bt); - children.push_back( bv ); - d_sygus_bound_var_type[bv] = cargs[sub_dt_index][0][i]; - }else{ - Debug("parser-sygus") << ": child " << i << " existing sygus to builtin expr : " << it->second << std::endl; - children.push_back( it->second ); - } - } - api::Term e = applyParseOp(op, children); - Debug("parser-sygus") << ": constructed " << e << ", which has type " - << e.getSort() << std::endl; - curr_t = e.getSort(); - sygus_to_builtin_expr[t] = e; - } - sorts[sub_dt_index] = curr_t; - sygus_to_builtin[t] = curr_t; - }else{ - Debug("parser-sygus") << "simple argument " << t << std::endl; - Debug("parser-sygus") << "...removing " << datatypes.back().getName() << std::endl; - //otherwise, datatype was unecessary - //pop argument datatype definition - popSygusDatatypeDef( datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym ); - } - return t; -} - -void Smt2::setSygusStartIndex(const std::string& fun, - int startIndex, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops) -{ - if( startIndex>0 ){ - api::DatatypeDecl tmp_dt = datatypes[0]; - api::Sort tmp_sort = sorts[0]; - std::vector tmp_ops; - tmp_ops.insert( tmp_ops.end(), ops[0].begin(), ops[0].end() ); - datatypes[0] = datatypes[startIndex]; - sorts[0] = sorts[startIndex]; - ops[0].clear(); - ops[0].insert( ops[0].end(), ops[startIndex].begin(), ops[startIndex].end() ); - datatypes[startIndex] = tmp_dt; - sorts[startIndex] = tmp_sort; - ops[startIndex].clear(); - ops[startIndex].insert( ops[startIndex].begin(), tmp_ops.begin(), tmp_ops.end() ); - }else if( startIndex<0 ){ - std::stringstream ss; - ss << "warning: no symbol named Start for synth-fun " << fun << std::endl; - warning(ss.str()); - } -} - -void Smt2::mkSygusDatatype(api::DatatypeDecl& dt, - std::vector& ops, - std::vector& cnames, - std::vector>& cargs, - std::vector& unresolved_gterm_sym, - std::map& sygus_to_builtin) -{ - Debug("parser-sygus") << "Making sygus datatype " << dt.getName() << std::endl; - Debug("parser-sygus") << " add constructors..." << std::endl; - - Debug("parser-sygus") << "SMT2 sygus parser : Making constructors for sygus datatype " << dt.getName() << std::endl; - Debug("parser-sygus") << " add constructors..." << std::endl; - // size of cnames changes, this loop must check size - for (unsigned i = 0; i < cnames.size(); i++) - { - bool is_dup = false; - bool is_dup_op = false; - for (unsigned j = 0; j < i; j++) - { - if( ops[i]==ops[j] ){ - is_dup_op = true; - if( cargs[i].size()==cargs[j].size() ){ - is_dup = true; - for( unsigned k=0; k Duplicate gterm : " << ops[i] << std::endl; - ops.erase( ops.begin() + i, ops.begin() + i + 1 ); - cnames.erase( cnames.begin() + i, cnames.begin() + i + 1 ); - cargs.erase( cargs.begin() + i, cargs.begin() + i + 1 ); - i--; - } - else - { - std::shared_ptr spc; - if (is_dup_op) - { - Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i] - << std::endl; - // make into define-fun - std::vector ltypes; - for (unsigned j = 0, size = cargs[i].size(); j < size; j++) - { - ltypes.push_back(sygus_to_builtin[cargs[i][j]]); - } - std::vector largs; - api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs); - - // make the let_body - std::vector largsApply = largs; - api::Term body = applyParseOp(ops[i], largsApply); - // replace by lambda - ParseOp pLam; - pLam.d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); - ops[i] = pLam; - Debug("parser-sygus") << " ...replace op : " << ops[i] << std::endl; - // callback prints as the expression - spc = std::make_shared( - body.getExpr(), api::termVectorToExprs(largs)); - } - else - { - api::Term sop = ops[i].d_expr; - if (!sop.isNull() && sop.getSort().isBitVector() && sop.isConst()) - { - Debug("parser-sygus") << "--> Bit-vector constant " << sop << " (" - << cnames[i] << ")" << std::endl; - // Since there are multiple output formats for bit-vectors and - // we are required by sygus standards to print in the exact input - // format given by the user, we use a print callback to custom print - // the given name. - spc = std::make_shared(cnames[i]); - } - else if (!sop.isNull() && sop.getKind() == api::CONSTANT) - { - Debug("parser-sygus") << "--> Defined function " << ops[i] - << std::endl; - // turn f into (lammbda (x) (f x)) - // in a degenerate case, ops[i] may be a defined constant, - // in which case we do not replace by a lambda. - if (sop.getSort().isFunction()) - { - std::vector ftypes = - sop.getSort().getFunctionDomainSorts(); - std::vector largs; - api::Term lbvl = makeSygusBoundVarList(dt, i, ftypes, largs); - largs.insert(largs.begin(), sop); - api::Term body = d_solver->mkTerm(api::APPLY_UF, largs); - ops[i].d_expr = d_solver->mkTerm(api::LAMBDA, lbvl, body); - Debug("parser-sygus") << " ...replace op : " << ops[i] - << std::endl; - } - else - { - Debug("parser-sygus") << " ...replace op : " << ops[i] - << std::endl; - } - // keep a callback to say it should be printed with the defined name - spc = std::make_shared(cnames[i]); - } - else - { - Debug("parser-sygus") << "--> Default case " << ops[i] << std::endl; - } - } - // must rename to avoid duplication - std::stringstream ss; - ss << dt.getName() << "_" << i << "_" << cnames[i]; - cnames[i] = ss.str(); - Debug("parser-sygus") << " construct the datatype " << cnames[i] << "..." - << std::endl; - - // Add the sygus constructor, either using the expression operator of - // ops[i], or the kind. - if (!ops[i].d_expr.isNull()) - { - dt.getDatatype().addSygusConstructor(ops[i].d_expr.getExpr(), - cnames[i], - api::sortVectorToTypes(cargs[i]), - spc); - } - else if (ops[i].d_kind != api::NULL_EXPR) - { - dt.getDatatype().addSygusConstructor(extToIntKind(ops[i].d_kind), - cnames[i], - api::sortVectorToTypes(cargs[i]), - spc); - } - else - { - std::stringstream ess; - ess << "unexpected parse operator for sygus constructor" << ops[i]; - parseError(ess.str()); - } - Debug("parser-sygus") << " finished constructing the datatype" - << std::endl; - } - } - - Debug("parser-sygus") << " add constructors for unresolved symbols..." << std::endl; - if( !unresolved_gterm_sym.empty() ){ - std::vector types; - Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl; - for( unsigned i=0; i lchildren; - lchildren.push_back(d_solver->mkTerm(api::BOUND_VAR_LIST, var)); - lchildren.push_back(var); - api::Term id_op = d_solver->mkTerm(api::LAMBDA, lchildren); - - // empty sygus callback (should not be printed) - std::shared_ptr sepc = - std::make_shared(); - - //make the sygus argument list - std::vector id_carg; - id_carg.push_back( t ); - dt.getDatatype().addSygusConstructor(id_op.getExpr(), - unresolved_gterm_sym[i], - api::sortVectorToTypes(id_carg), - sepc); - - //add to operators - ParseOp idOp; - idOp.d_expr = id_op; - ops.push_back(idOp); - } - }else{ - std::stringstream ss; - ss << "Unhandled sygus constructor " << unresolved_gterm_sym[i]; - throw ParserException(ss.str()); - } - } - } -} - -api::Term Smt2::makeSygusBoundVarList(api::DatatypeDecl& dt, - unsigned i, - const std::vector& ltypes, - std::vector& lvars) -{ - for (unsigned j = 0, size = ltypes.size(); j < size; j++) - { - std::stringstream ss; - ss << dt.getName() << "_x_" << i << "_" << j; - api::Term v = bindBoundVar(ss.str(), ltypes[j]); - lvars.push_back(v); - } - return d_solver->mkTerm(api::BOUND_VAR_LIST, lvars); -} void Smt2::addSygusConstructorTerm( api::DatatypeDecl& dt, @@ -1592,18 +1044,9 @@ api::Term Smt2::parseOpToExpr(ParseOp& p) } else if (!isDeclared(p.d_name, SYM_VARIABLE)) { - if (sygus_v1() && p.d_name[0] == '-' - && p.d_name.find_first_not_of("0123456789", 1) == std::string::npos) - { - // allow unary minus in sygus version 1 - expr = d_solver->mkReal(p.d_name); - } - else - { - std::stringstream ss; - ss << "Symbol " << p.d_name << " is not declared."; - parseError(ss.str()); - } + std::stringstream ss; + ss << "Symbol " << p.d_name << " is not declared."; + parseError(ss.str()); } else { diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 868177d27..579fa90ce 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -60,9 +60,6 @@ class Smt2 : public Parser */ std::unordered_map d_indexedOpKindMap; std::pair d_lastNamedTerm; - // for sygus - std::vector d_sygusVars, d_sygusVarPrimed, d_sygusConstraints, - d_sygusFunSymbols; protected: Smt2(api::Solver* solver, @@ -282,8 +279,6 @@ class Smt2 : public Parser } /** Are we using a sygus language? */ 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; @@ -350,58 +345,6 @@ class Smt2 : public Parser */ api::Term mkAbstractValue(const std::string& name); - void mkSygusConstantsForType(const api::Sort& type, - std::vector& ops); - - void processSygusGTerm( - CVC4::SygusGTerm& sgt, - int index, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym, - const std::vector& sygus_vars, - std::map& sygus_to_builtin, - std::map& sygus_to_builtin_expr, - api::Sort& ret, - bool isNested = false); - - bool pushSygusDatatypeDef( - api::Sort t, - std::string& dname, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym); - - bool popSygusDatatypeDef( - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym); - - void setSygusStartIndex(const std::string& fun, - int startIndex, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops); - - void mkSygusDatatype(api::DatatypeDecl& dt, - std::vector& ops, - std::vector& cnames, - std::vector>& cargs, - std::vector& unresolved_gterm_sym, - std::map& sygus_to_builtin); - /** * Adds a constructor to sygus datatype dt whose sygus operator is term. * @@ -427,7 +370,6 @@ class Smt2 : public Parser void addSygusConstructorVariables(api::DatatypeDecl& dt, const std::vector& sygusVars, api::Sort type) const; - /** * Smt2 parser provides its own checkDeclaration, which does the * same as the base, but with some more helpful errors. @@ -442,11 +384,6 @@ class Smt2 : public Parser if (name.length() > 1 && name[0] == '-' && name.find_first_not_of("0123456789", 1) == std::string::npos) { - if (sygus_v1()) - { - // "-1" is allowed in SyGuS version 1.0 - return; - } std::stringstream ss; ss << notes << "You may have intended to apply unary minus: `(- " << name.substr(1) << ")'\n"; @@ -537,34 +474,6 @@ class Smt2 : public Parser api::Term applyParseOp(ParseOp& p, std::vector& args); //------------------------- end processing parse operators private: - std::map d_sygus_bound_var_type; - - api::Sort processSygusNestedGTerm( - int sub_dt_index, - std::string& sub_dname, - std::vector& datatypes, - std::vector& sorts, - std::vector>& ops, - std::vector>& cnames, - std::vector>>& cargs, - std::vector& allow_const, - std::vector>& unresolved_gterm_sym, - std::map& sygus_to_builtin, - std::map& sygus_to_builtin_expr, - api::Sort sub_ret); - - /** make sygus bound var list - * - * This is used for converting non-builtin sygus operators to lambda - * expressions. It takes as input a datatype and constructor index (for - * naming) and a vector of type ltypes. - * It appends a bound variable to lvars for each type in ltypes, and returns - * a bound variable list whose children are lvars. - */ - api::Term makeSygusBoundVarList(api::DatatypeDecl& dt, - unsigned i, - const std::vector& ltypes, - std::vector& lvars); /** Purify sygus grammar term * diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index c17684b15..5d54759b9 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -52,14 +52,6 @@ unique_ptr Printer::makePrinter(OutputLanguage lang) case LANG_CVC4: return unique_ptr(new printer::cvc::CvcPrinter()); - case LANG_Z3STR: - return unique_ptr( - new printer::smt2::Smt2Printer(printer::smt2::z3str_variant)); - - case LANG_SYGUS_V1: - return unique_ptr( - new printer::smt2::Smt2Printer(printer::smt2::sygus_variant)); - case LANG_SYGUS_V2: // sygus version 2.0 does not have discrepancies with smt2, hence we use // a normal smt2 variant here. diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 31aa67ff9..784e321a0 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -593,35 +593,10 @@ void Smt2Printer::toStream(std::ostream& out, // string theory case kind::STRING_CONCAT: - if(d_variant == z3str_variant) { - out << "Concat "; - for(unsigned i = 0; i < n.getNumChildren(); ++i) { - toStream(out, n[i], -1, types, TypeNode::null()); - if(i + 1 < n.getNumChildren()) { - out << ' '; - } - if(i + 2 < n.getNumChildren()) { - out << "(Concat "; - } - } - for(unsigned i = 0; i < n.getNumChildren() - 1; ++i) { - out << ")"; - } - return; - } out << "str.++ "; break; case kind::STRING_IN_REGEXP: { stringstream ss; - if(d_variant == z3str_variant && stringifyRegexp(n[1], ss)) { - out << "= "; - toStream(out, n[0], -1, types, TypeNode::null()); - out << " "; - Node str = NodeManager::currentNM()->mkConst(String(ss.str())); - toStream(out, str, -1, types, TypeNode::null()); - out << ")"; - return; - } out << smtKindString(k, d_variant) << " "; break; } @@ -1188,7 +1163,7 @@ static string smtKindString(Kind k, Variant v) //string theory case kind::STRING_CONCAT: return "str.++"; - case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len"; + case kind::STRING_LENGTH: return "str.len"; case kind::STRING_SUBSTR: return "str.substr" ; case kind::STRING_STRCTN: return "str.contains" ; case kind::STRING_CHARAT: return "str.at" ; @@ -1285,7 +1260,6 @@ void Smt2Printer::toStream(std::ostream& out, || tryToStream(out, c) || tryToStream(out, c, d_variant) || tryToStream(out, c) - || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) @@ -1852,12 +1826,7 @@ static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, Variant v) { - // Z3-str doesn't have string-specific logic strings(?), so comment it - if(v == z3str_variant) { - out << "; (set-logic " << c->getLogic() << ")"; - } else { - out << "(set-logic " << c->getLogic() << ")"; - } + out << "(set-logic " << c->getLogic() << ")"; } static void toStream(std::ostream& out, const SetInfoCommand* c, Variant v) @@ -2021,7 +1990,7 @@ static void toStream(std::ostream& out, const CommentCommand* c, Variant v) string s = c->getComment(); size_t pos = 0; while((pos = s.find_first_of('"', pos)) != string::npos) { - s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); + s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\""); pos += 2; } out << "(set-info :notes \"" << s << "\")"; @@ -2035,7 +2004,7 @@ static void toStream(std::ostream& out, const EchoCommand* c, Variant v) // escape all double-quotes size_t pos = 0; while((pos = s.find('"', pos)) != string::npos) { - s.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); + s.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\""); pos += 2; } out << "(echo \"" << s << "\")"; @@ -2155,12 +2124,6 @@ static void toStream(std::ostream& out, const DeclareSygusFunctionCommand* c) out << " (" << argTypes << ") " << ft.getRangeType() << ')'; } -static void toStream(std::ostream& out, const DeclareSygusPrimedVarCommand* c) -{ - out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol()) - << ' ' << c->getType() << ')'; -} - static void toStream(std::ostream& out, const DeclareSygusVarCommand* c) { out << '(' << c->getCommandName() << ' ' << c->getVar() << ' ' << c->getType() @@ -2240,7 +2203,7 @@ static void errorToStream(std::ostream& out, std::string message, Variant v) { // escape all double-quotes size_t pos = 0; while((pos = message.find('"', pos)) != string::npos) { - message.replace(pos, 1, (v == z3str_variant || v == smt2_0_variant) ? "\\\"" : "\"\""); + message.replace(pos, 1, v == smt2_0_variant ? "\\\"" : "\"\""); pos += 2; } out << "(error \"" << message << "\")" << endl; @@ -2270,9 +2233,6 @@ static OutputLanguage variantToLanguage(Variant variant) switch(variant) { case smt2_0_variant: return language::output::LANG_SMTLIB_V2_0; - case z3str_variant: - return language::output::LANG_Z3STR; - case sygus_variant: return language::output::LANG_SYGUS_V1; case no_variant: default: return language::output::LANG_SMTLIB_V2_6; } diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 1330bf79f..398e510cb 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -33,7 +33,6 @@ enum Variant smt2_0_variant, // old-style 2.0 syntax, when it makes a difference smt2_6_variant, // new-style 2.6 syntax, when it makes a difference, with // support for the string standard - z3str_variant, // old-style 2.0 and also z3str syntax sygus_variant // variant for sygus }; /* enum Variant */ class Smt2Printer : public CVC4::Printer { diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 962882309..cbb2076dd 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -605,48 +605,6 @@ std::string DeclareSygusVarCommand::getCommandName() const return "declare-var"; } -/* -------------------------------------------------------------------------- */ -/* class DeclareSygusPrimedVarCommand */ -/* -------------------------------------------------------------------------- */ - -DeclareSygusPrimedVarCommand::DeclareSygusPrimedVarCommand( - const std::string& id, Type t) - : DeclarationDefinitionCommand(id), d_type(t) -{ -} - -Type DeclareSygusPrimedVarCommand::getType() const { return d_type; } - -void DeclareSygusPrimedVarCommand::invoke(SmtEngine* smtEngine) -{ - try - { - smtEngine->declareSygusPrimedVar(d_symbol, d_type); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* DeclareSygusPrimedVarCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - return new DeclareSygusPrimedVarCommand( - d_symbol, d_type.exportTo(exprManager, variableMap)); -} - -Command* DeclareSygusPrimedVarCommand::clone() const -{ - return new DeclareSygusPrimedVarCommand(d_symbol, d_type); -} - -std::string DeclareSygusPrimedVarCommand::getCommandName() const -{ - return "declare-primed-var"; -} - /* -------------------------------------------------------------------------- */ /* class DeclareSygusFunctionCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index f7c780dee..efb4f2f4a 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -675,38 +675,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand Type d_type; }; -/** Declares a sygus primed variable, for invariant problems - * - * We do not actually build expressions for the declared variables because they - * are unnecessary for building SyGuS problems. - */ -class CVC4_PUBLIC DeclareSygusPrimedVarCommand - : public DeclarationDefinitionCommand -{ - public: - DeclareSygusPrimedVarCommand(const std::string& id, Type type); - /** returns the declared primed variable's type */ - Type getType() const; - - /** invokes this command - * - * The type of the primed variable is communicated to the SMT engine for - * debugging purposes when a synthesis conjecture is built later on. - */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; - /** creates a copy of this command */ - Command* clone() const override; - /** returns this command's name */ - std::string getCommandName() const override; - - protected: - /** the type of the declared primed variable */ - Type d_type; -}; - /** Declares a sygus universal function variable */ class CVC4_PUBLIC DeclareSygusFunctionCommand : public DeclarationDefinitionCommand diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b826ef23d..a6d89aaf5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1873,15 +1873,6 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) // don't need to set that the conjecture is stale } -void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) -{ - SmtScope smts(this); - finalOptionsAreSet(); - // do nothing (the command is spurious) - Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; - // don't need to set that the conjecture is stale -} - void SmtEngine::declareSygusFunctionVar(const std::string& id, Expr var, Type type) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b1e3313d8..8a9a60251 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -403,16 +403,6 @@ class CVC4_PUBLIC SmtEngine */ void declareSygusVar(const std::string& id, Expr var, Type type); - /** - * Store information for debugging sygus invariants setup. - * - * Since in SyGuS the commands "declare-primed-var" are not necessary for - * building invariant constraints, we only use them to check that the number - * of variables declared corresponds to the number of arguments of the - * invariant-to-synthesize. - */ - void declareSygusPrimedVar(const std::string& id, Type type); - /** * Add a function variable declaration. * diff --git a/src/util/result.cpp b/src/util/result.cpp index 8b527d322..0ed063ebc 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -374,7 +374,6 @@ void Result::toStreamTptp(std::ostream& out) const { void Result::toStream(std::ostream& out, OutputLanguage language) const { switch (language) { - case language::output::LANG_SYGUS_V1: case language::output::LANG_SYGUS_V2: toStreamSmt2(out); break; case language::output::LANG_TPTP: toStreamTptp(out); diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 9b8ad81b8..6f2da480e 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -272,7 +272,6 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr, bool SExpr::languageQuotesKeywords(OutputLanguage language) { switch (language) { - case language::output::LANG_SYGUS_V1: case language::output::LANG_TPTP: return true; case language::output::LANG_AST: