From b09cdf3e0f407c69c8df8023b70c776d1b0a4589 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 24 Apr 2015 10:29:36 +0200
Subject: [PATCH] Fix sygus parser for non-tokenized operators, reenable
 regression. Fix for --fmf-fun.

---
 src/parser/smt2/Smt2.g                     | 27 +++++++++++++++-------
 src/theory/quantifiers/fun_def_process.cpp |  2 +-
 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
-- 
2.30.2