diff options
| -rw-r--r-- | src/parser/smt2/Smt2.g | 27 | ||||
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 8 |
3 files changed, 23 insertions, 14 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index acdecf0c4..d2e83702f 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -724,15 +724,26 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri name = kind::kindToString(k); } | symbol[name,CHECK_NONE,SYM_VARIABLE] - { // 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; - Debug("parser-sygus") << " : op (declare=" << PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl; - if( !PARSER_STATE->isDefinedFunction(name) ){ - PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); + { + bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); + if(isBuiltinOperator) { + Kind k = PARSER_STATE->getOperatorKind(name); + if( k==CVC4::kind::BITVECTOR_UDIV ){ + k = CVC4::kind::BITVECTOR_UDIV_TOTAL; + } + ops.push_back(EXPR_MANAGER->operatorOf(k)); + name = kind::kindToString(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; + Debug("parser-sygus") << " : op (declare=" << PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl; + if( !PARSER_STATE->isDefinedFunction(name) ){ + PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); + } + ops.push_back( PARSER_STATE->getVariable(name) ); } - ops.push_back( PARSER_STATE->getVariable(name) ); } ) { cnames.push_back( name ); diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index f47cb8f1e..cb379ec92 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -136,7 +136,7 @@ Node FunDefFmf::simplify( Node n, bool pol, bool hasPol, std::vector< Node >& co childChanged = c!=n[i] || childChanged; } if( childChanged ){ - nn = n; + nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); } }else{ //simplify term diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 53ebf0a78..efa656e7b 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -26,17 +26,15 @@ TESTS = commutative.sy \ array_sum_2_5.sy \ parity-AIG-d0.sy \ twolets1.sy \ - array_search_2.sy + array_search_2.sy \ + hd-01-d1-prog.sy \ + icfp_28_10.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ max.smt2 \ sygus-uf.sl -# Failing dues to parser changes. Need to be fixed. -EXTRA_DIST += \ - hd-01-d1-prog.sy \ - icfp_28_10.sy #if CVC4_BUILD_PROFILE_COMPETITION #else |