From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 28 Nov 2012 17:37:57 +0000 (+0000)
Subject: Bug fix:
X-Git-Tag: cvc5-1.0.0~7542
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=83cf3909b50af1d37735a252e79d550aac08cf7a;p=cvc5.git

Bug fix:
* Fix creation of bound variables in CVC native language parser
* This corrects a problem with misleading model output

(this commit was certified error- and warning-free by the test-and-commit script.)
---

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index c82a984d2..d0fe9036b 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -866,7 +866,7 @@ boundVarDeclReturn[std::vector<CVC4::Expr>& terms,
   // NOTE: do not clear the vectors here!
 }
   : identifierList[ids,CHECK_NONE,SYM_VARIABLE] COLON type[t,CHECK_DECLARED]
-    { const std::vector<Expr>& vars = PARSER_STATE->mkVars(ids, t, false);
+    { const std::vector<Expr>& vars = PARSER_STATE->mkBoundVars(ids, t);
       terms.insert(terms.end(), vars.begin(), vars.end());
       for(unsigned i = 0; i < vars.size(); ++i) {
         types.push_back(t);
@@ -920,7 +920,8 @@ declareTypes[CVC4::Command*& cmd, const std::vector<std::string>& idList]
  * re-declared if topLevel is true (CVC allows re-declaration if the
  * types are compatible---if they aren't compatible, an error is
  * thrown).  Also if topLevel is true, variable definitions are
- * permitted and "cmd" is output.
+ * permitted and "cmd" is output.  If topLevel is false, bound vars
+ * are created
  */
 declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::string>& idList, bool topLevel]
 @init {
@@ -957,10 +958,12 @@ declareVariables[CVC4::Command*& cmd, CVC4::Type& t, const std::vector<std::stri
             }
           } else {
             Debug("parser") << "  " << *i << " not declared" << std::endl;
-            Expr func = PARSER_STATE->mkVar(*i, t, true);
             if(topLevel) {
+              Expr func = PARSER_STATE->mkVar(*i, t, true);
               Command* decl = new DeclareFunctionCommand(*i, func, t);
               seq->addCommand(decl);
+            } else {
+              PARSER_STATE->mkBoundVar(*i, t);
             }
           }
         }
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 57589ec9c..721dedc70 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -179,6 +179,16 @@ Parser::mkVars(const std::vector<std::string> names,
   return vars;
 }
 
+std::vector<Expr>
+Parser::mkBoundVars(const std::vector<std::string> names,
+                    const Type& type) {
+  std::vector<Expr> vars;
+  for(unsigned i = 0; i < names.size(); ++i) {
+    vars.push_back(mkBoundVar(names[i], type));
+  }
+  return vars;
+}
+
 void
 Parser::defineVar(const std::string& name, const Expr& val,
                   bool levelZero) {
diff --git a/src/parser/parser.h b/src/parser/parser.h
index eed8531a5..fc956b463 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -335,6 +335,11 @@ public:
   /** Create a new CVC4 bound variable expression of the given type. */
   Expr mkBoundVar(const std::string& name, const Type& type);
 
+  /**
+   * Create a set of new CVC4 bound variable expressions of the given type.
+   */
+  std::vector<Expr> mkBoundVars(const std::vector<std::string> names, const Type& type);
+
   /** Create a new CVC4 function expression of the given type. */
   Expr mkFunction(const std::string& name, const Type& type,
                   bool levelZero = false);