diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-31 10:32:34 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-31 10:32:34 +0200 |
| commit | bf7f7d6960f6e03e90880dd3da9ff1bf00943cf3 (patch) | |
| tree | 87630123b624ea6ca98bb85d8cc3e99ca75edc01 /src/parser/smt2/Smt2.g | |
| parent | f2da7296ff76920528c0e9edc35f96a715b85078 (diff) | |
Sygus support for inductive datatypes.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 1564e6f3e..1ce7c4aff 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -606,6 +606,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); $cmd = new DefineFunctionCommand(name, func, terms, expr); } + | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd] + | DECLARE_CODATATYPES_TOK datatypesDefCommand[true, cmd] | /* synth-fun */ ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] @@ -912,7 +914,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] // fail, but we need an operator to continue here.. Debug("parser-sygus") << "Sygus grammar " << fun; Debug("parser-sygus") << " : op (declare=" << PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl; - if( !PARSER_STATE->isDefinedFunction(name) ){ + if( !PARSER_STATE->isDeclared(name) && !PARSER_STATE->isDefinedFunction(name) ){ PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); } sgt.d_name = name; |