sygusComp2018: update semantics for declare-fun in sygus. (#2102)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 4b8c5284137b14d895f74a76695147774b33275a..b52be77bba1dc389564901a9553415d5e346d69a 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -353,8 +353,17 @@ command [std::unique_ptr<CVC4::Command>* cmd]
                                       "be declared in logic ");
       }
       // we allow overloading for function declarations
-      Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
-      cmd->reset(new DeclareFunctionCommand(name, func, t));
+      if (PARSER_STATE->sygus())
+      {
+        // it is a higher-order universal variable
+        PARSER_STATE->mkSygusVar(name, t);
+        cmd->reset(new EmptyCommand());
+      }
+      else
+      {
+        Expr func = PARSER_STATE->mkVar(name, t, ExprManager::VAR_FLAG_NONE, true);
+        cmd->reset(new DeclareFunctionCommand(name, func, t));
+      }
     }
   | /* function definition */
     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 33ac69c636ba6ea6114a57a8ac7545b38a5c57d3..257ee1171bf0fa10700a7e2a7ba2c03e3e7987d9 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -625,10 +625,12 @@ Expr Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed)
   d_sygusVars.push_back(e);
   d_sygusVarPrimed[e] = false;
   if( isPrimed ){
+    d_sygusInvVars.push_back(e);
     std::stringstream ss;
     ss << name << "'";
     Expr ep = mkBoundVar(ss.str(), type);
     d_sygusVars.push_back(ep);
+    d_sygusInvVars.push_back(ep);
     d_sygusVarPrimed[ep] = true;
   }
   return e;
@@ -1228,15 +1230,14 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt,
 }
 
 const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
-  for( unsigned i=0; i<d_sygusVars.size(); i++ ){
-    Expr v = d_sygusVars[i];
+  for (unsigned i = 0, size = d_sygusInvVars.size(); i < size; i++)
+  {
+    Expr v = d_sygusInvVars[i];
     std::map< Expr, bool >::iterator it = d_sygusVarPrimed.find( v );
     if( it!=d_sygusVarPrimed.end() ){
       if( it->second==isPrimed ){
         vars.push_back( v );
       }
-    }else{
-      //should never happen
     }
   }
 }

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 85d9b112eefd941eda2eb782bacb2becc327d87e..c9b224d390db0d65c41b1512e62442de5f9d1f9f 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -64,7 +64,8 @@ private:
   std::unordered_map<std::string, Kind> operatorKindMap;
   std::pair<Expr, std::string> d_lastNamedTerm;
   // for sygus
-  std::vector<Expr> d_sygusVars, d_sygusConstraints, d_sygusFunSymbols;
+  std::vector<Expr> d_sygusVars, d_sygusInvVars, d_sygusConstraints,
+      d_sygusFunSymbols;
   std::map< Expr, bool > d_sygusVarPrimed;
 
 protected: