From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 20 Nov 2020 19:51:07 +0000 (-0600)
Subject: Fix use of declaration sequence command in cvc parser (#5479)
X-Git-Tag: cvc5-1.0.0~2573
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=020879ca5fe52e272d7e7f8df1cbcc9a0e74899c;p=cvc5.git

Fix use of declaration sequence command in cvc parser (#5479)

This is required to make the cvc parser work properly with the new version of getting models based on the symbol manager.
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index fe14ce5fc..91c7d0ded 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1141,6 +1141,13 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
           PARSER_STATE->parseError("cannot construct a definition here; maybe you want a LET");
         }
         assert(!idList.empty());
+        api::Term fterm = f;
+        std::vector<api::Term> formals;
+        if (f.getKind()==api::LAMBDA)
+        {
+          formals.insert(formals.end(), f[0].begin(), f[0].end());
+          f = f[1];
+        }
         for(std::vector<std::string>::const_iterator i = idList.begin(),
               i_end = idList.end();
             i != i_end;
@@ -1151,13 +1158,13 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t,
               *i,
               t,
               ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED);
-          PARSER_STATE->defineVar(*i, f);
-          Command* decl = new DefineFunctionCommand(*i, func, f, true);
+          PARSER_STATE->defineVar(*i, fterm);
+          Command* decl = new DefineFunctionCommand(*i, func, formals, f, true);
           seq->addCommand(decl);
         }
       }
       if(topLevel) {
-        cmd->reset(new DeclarationSequence());
+        cmd->reset(seq.release());
       }
     }
   ;
@@ -2169,13 +2176,10 @@ simpleTerm[CVC4::api::Term& f]
     }
 
     /* array literals */
-  | ARRAY_TOK /* { PARSER_STATE->pushScope(); } */ LPAREN
+  | ARRAY_TOK LPAREN
     restrictedType[t, CHECK_DECLARED] OF_TOK restrictedType[t2, CHECK_DECLARED]
     RPAREN COLON simpleTerm[f]
-    { /* Eventually if we support a bound var (like a lambda) for array
-       * literals, we can use the push/pop scope. */
-      /* PARSER_STATE->popScope(); */
-      t = SOLVER->mkArraySort(t, t2);
+    { t = SOLVER->mkArraySort(t, t2);
       if(!t2.isComparableTo(f.getSort())) {
         std::stringstream ss;
         ss << "type mismatch inside array constant term:" << std::endl