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 .
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)
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) {
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));
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));
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")
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")
{
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,
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";
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,
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";
%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;
%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"
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\
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\
";
break;
}
- case LANG_SYGUS_V1:
case LANG_SYGUS_V2: input = new SygusInput(inputStream); break;
case LANG_TPTP:
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;
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");
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(); }
| 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<CVC4::api::Term>& sygus_vars,
- const std::string& fun]
-@declarations
-{
- CVC4::api::Sort t;
- std::string name;
- unsigned startIndex = 0;
- std::vector<std::vector<CVC4::SygusGTerm>> sgts;
- std::vector<api::DatatypeDecl> datatypes;
- std::vector<api::Sort> sorts;
- std::vector<std::vector<ParseOp>> ops;
- std::vector<std::vector<std::string>> cnames;
- std::vector<std::vector<std::vector<CVC4::api::Sort>>> cargs;
- std::vector<bool> allow_const;
- std::vector<std::vector<std::string>> unresolved_gterm_sym;
- std::map<CVC4::api::Sort, CVC4::api::Sort> sygus_to_builtin;
- std::map<CVC4::api::Sort, CVC4::api::Term> 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<CVC4::SygusGTerm>());
- 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<CVC4::Datatype> dtypes;
- dtypes.reserve(ndatatypes);
-
- for (api::DatatypeDecl i : datatypes)
- {
- dtypes.push_back(i.getDatatype());
- }
-
- std::set<Type> tset =
- api::sortSetToTypes(PARSER_STATE->getUnresolvedSorts());
-
- std::vector<DatatypeType> 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
*
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]
} 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<std::string, api::Term>& binder : binders)
{
| 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
<< " ...)";
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 : ')';
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';
}
}
- 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;
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
return d_solver->mkAbstractValue(name.substr(1));
}
-void Smt2::mkSygusConstantsForType(const api::Sort& type,
- std::vector<api::Term>& 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<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- const std::vector<api::Term>& sygus_vars,
- std::map<api::Sort, api::Sort>& sygus_to_builtin,
- std::map<api::Sort, api::Term>& 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<api::Sort>());
- for( unsigned i=0; i<sgt.d_children.size(); i++ ){
- std::stringstream ss;
- ss << datatypes[index].getName() << "_" << ops[index].size() << "_arg_" << i;
- std::string sub_dname = ss.str();
- //add datatype for child
- api::Sort null_type;
- pushSygusDatatypeDef( null_type, sub_dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym );
- int sub_dt_index = datatypes.size()-1;
- //process child
- api::Sort sub_ret;
- processSygusGTerm( sgt.d_children[i], sub_dt_index, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym,
- sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret, true );
- //process the nested gterm (either pop the last datatype, or flatten the argument)
- api::Sort tt = processSygusNestedGTerm(sub_dt_index,
- sub_dname,
- datatypes,
- sorts,
- ops,
- cnames,
- cargs,
- allow_const,
- unresolved_gterm_sym,
- sygus_to_builtin,
- sygus_to_builtin_expr,
- sub_ret);
- cargs[index].back().push_back(tt);
- }
- }
- else if (sgt.d_gterm_type == SygusGTerm::gterm_constant)
- {
- if( sgt.getNumChildren()!=0 ){
- parseError("Bad syntax for Sygus Constant.");
- }
- std::vector<api::Term> consts;
- mkSygusConstantsForType( sgt.d_type, consts );
- Debug("parser-sygus") << "...made " << consts.size() << " constants." << std::endl;
- for( unsigned i=0; i<consts.size(); i++ ){
- std::stringstream ss;
- ss << consts[i];
- Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
- ParseOp constOp;
- constOp.d_expr = consts[i];
- ops[index].push_back(constOp);
- cnames[index].push_back( ss.str() );
- cargs[index].push_back(std::vector<api::Sort>());
- }
- 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<sygus_vars.size(); i++ ){
- if (sygus_vars[i].getSort() == sgt.d_type)
- {
- std::stringstream ss;
- ss << sygus_vars[i];
- Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
- ParseOp varOp;
- varOp.d_expr = sygus_vars[i];
- ops[index].push_back(varOp);
- cnames[index].push_back( ss.str() );
- cargs[index].push_back(std::vector<api::Sort>());
- }
- }
- }
- 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<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym)
-{
- sorts.push_back(t);
- datatypes.push_back(d_solver->mkDatatypeDecl(dname));
- ops.push_back(std::vector<ParseOp>());
- cnames.push_back(std::vector<std::string>());
- cargs.push_back(std::vector<std::vector<api::Sort>>());
- allow_const.push_back(false);
- unresolved_gterm_sym.push_back(std::vector< std::string >());
- return true;
-}
-
-bool Smt2::popSygusDatatypeDef(
- std::vector<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& 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<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- std::map<api::Sort, api::Sort>& sygus_to_builtin,
- std::map<api::Sort, CVC4::api::Term>& 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<api::Term> children;
- for( unsigned i=0; i<cargs[sub_dt_index][0].size(); i++ ){
- std::map<api::Sort, CVC4::api::Term>::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<api::Sort, api::Sort>::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<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops)
-{
- if( startIndex>0 ){
- api::DatatypeDecl tmp_dt = datatypes[0];
- api::Sort tmp_sort = sorts[0];
- std::vector<ParseOp> 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<ParseOp>& ops,
- std::vector<std::string>& cnames,
- std::vector<std::vector<api::Sort>>& cargs,
- std::vector<std::string>& unresolved_gterm_sym,
- std::map<api::Sort, api::Sort>& 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<cargs[i].size(); k++ ){
- if( cargs[i][k]!=cargs[j][k] ){
- is_dup = false;
- break;
- }
- }
- }
- if( is_dup ){
- break;
- }
- }
- }
- Debug("parser-sygus") << "SYGUS CONS " << i << " : ";
- if( is_dup ){
- Debug("parser-sygus") << "--> 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<SygusPrintCallback> spc;
- if (is_dup_op)
- {
- Debug("parser-sygus") << "--> Duplicate gterm operator : " << ops[i]
- << std::endl;
- // make into define-fun
- std::vector<api::Sort> ltypes;
- for (unsigned j = 0, size = cargs[i].size(); j < size; j++)
- {
- ltypes.push_back(sygus_to_builtin[cargs[i][j]]);
- }
- std::vector<api::Term> largs;
- api::Term lbvl = makeSygusBoundVarList(dt, i, ltypes, largs);
-
- // make the let_body
- std::vector<api::Term> 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<printer::SygusExprPrintCallback>(
- 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<printer::SygusNamedPrintCallback>(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<api::Sort> ftypes =
- sop.getSort().getFunctionDomainSorts();
- std::vector<api::Term> 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<printer::SygusNamedPrintCallback>(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<api::Sort> types;
- Debug("parser-sygus") << "...resolve " << unresolved_gterm_sym.size() << " symbols..." << std::endl;
- for( unsigned i=0; i<unresolved_gterm_sym.size(); i++ ){
- Debug("parser-sygus") << " resolve : " << unresolved_gterm_sym[i] << std::endl;
- if( isUnresolvedType(unresolved_gterm_sym[i]) ){
- Debug("parser-sygus") << " it is an unresolved type." << std::endl;
- api::Sort t = getSort(unresolved_gterm_sym[i]);
- if( std::find( types.begin(), types.end(), t )==types.end() ){
- types.push_back( t );
- //identity element
- api::Sort bt = api::Sort(d_solver, dt.getDatatype().getSygusType());
- Debug("parser-sygus") << ": make identity function for " << bt << ", argument type " << t << std::endl;
-
- std::stringstream ss;
- ss << t << "_x";
- api::Term var = bindBoundVar(ss.str(), bt);
- std::vector<api::Term> 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<SygusPrintCallback> sepc =
- std::make_shared<printer::SygusEmptyPrintCallback>();
-
- //make the sygus argument list
- std::vector<api::Sort> 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<api::Sort>& ltypes,
- std::vector<api::Term>& 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,
}
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
{
*/
std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
std::pair<api::Term, std::string> d_lastNamedTerm;
- // for sygus
- std::vector<api::Term> d_sygusVars, d_sygusVarPrimed, d_sygusConstraints,
- d_sygusFunSymbols;
protected:
Smt2(api::Solver* solver,
}
/** 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;
*/
api::Term mkAbstractValue(const std::string& name);
- void mkSygusConstantsForType(const api::Sort& type,
- std::vector<api::Term>& ops);
-
- void processSygusGTerm(
- CVC4::SygusGTerm& sgt,
- int index,
- std::vector<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- const std::vector<api::Term>& sygus_vars,
- std::map<api::Sort, api::Sort>& sygus_to_builtin,
- std::map<api::Sort, api::Term>& sygus_to_builtin_expr,
- api::Sort& ret,
- bool isNested = false);
-
- bool pushSygusDatatypeDef(
- api::Sort t,
- std::string& dname,
- std::vector<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym);
-
- bool popSygusDatatypeDef(
- std::vector<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym);
-
- void setSygusStartIndex(const std::string& fun,
- int startIndex,
- std::vector<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops);
-
- void mkSygusDatatype(api::DatatypeDecl& dt,
- std::vector<ParseOp>& ops,
- std::vector<std::string>& cnames,
- std::vector<std::vector<api::Sort>>& cargs,
- std::vector<std::string>& unresolved_gterm_sym,
- std::map<api::Sort, api::Sort>& sygus_to_builtin);
-
/**
* Adds a constructor to sygus datatype dt whose sygus operator is term.
*
void addSygusConstructorVariables(api::DatatypeDecl& dt,
const std::vector<api::Term>& sygusVars,
api::Sort type) const;
-
/**
* Smt2 parser provides its own checkDeclaration, which does the
* same as the base, but with some more helpful errors.
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";
api::Term applyParseOp(ParseOp& p, std::vector<api::Term>& args);
//------------------------- end processing parse operators
private:
- std::map<api::Term, api::Sort> d_sygus_bound_var_type;
-
- api::Sort processSygusNestedGTerm(
- int sub_dt_index,
- std::string& sub_dname,
- std::vector<api::DatatypeDecl>& datatypes,
- std::vector<api::Sort>& sorts,
- std::vector<std::vector<ParseOp>>& ops,
- std::vector<std::vector<std::string>>& cnames,
- std::vector<std::vector<std::vector<api::Sort>>>& cargs,
- std::vector<bool>& allow_const,
- std::vector<std::vector<std::string>>& unresolved_gterm_sym,
- std::map<api::Sort, api::Sort>& sygus_to_builtin,
- std::map<api::Sort, api::Term>& 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<api::Sort>& ltypes,
- std::vector<api::Term>& lvars);
/** Purify sygus grammar term
*
case LANG_CVC4:
return unique_ptr<Printer>(new printer::cvc::CvcPrinter());
- case LANG_Z3STR:
- return unique_ptr<Printer>(
- new printer::smt2::Smt2Printer(printer::smt2::z3str_variant));
-
- case LANG_SYGUS_V1:
- return unique_ptr<Printer>(
- 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.
// 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;
}
//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" ;
|| tryToStream<EmptyCommand>(out, c)
|| tryToStream<EchoCommand>(out, c, d_variant)
|| tryToStream<SynthFunCommand>(out, c)
- || tryToStream<DeclareSygusPrimedVarCommand>(out, c)
|| tryToStream<DeclareSygusFunctionCommand>(out, c)
|| tryToStream<DeclareSygusVarCommand>(out, c)
|| tryToStream<SygusConstraintCommand>(out, c)
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)
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 << "\")";
// 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 << "\")";
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()
// 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;
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;
}
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 {
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 */
/* -------------------------------------------------------------------------- */
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
// 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)
*/
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.
*
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);
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:
projects / cvc5.git / commitdiff