Fix sygus parser for non-tokenized operators, reenable regression. Fix for --fmf...

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index acdecf0c467c29754056f2065cd4fb0e1169616a..d2e83702fcf8f7ccfd600bbbcfa04168f3f7a5e5 100644 (file)
--- 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 f47cb8f1e24870f77667f3aae52d950759a5a554..cb379ec9272cfd3947da9be4a228ec8115473764 100644 (file)
--- 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 53ebf0a78d4e8ef1c2db0d8077eba59579c3bc19..efa656e7bb86c2c0ff84365434fc4b804a7296aa 100644 (file)
--- 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