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 c82a984d27404b91a618278f91fb0cd00e5a3190..d0fe9036bb86b5d52ca4de0a15e98e90e447f2bd 100644 (file)
--- 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 57589ec9cf613c702a2533e7577a659ce2dddbb7..721dedc70a3806d1863a416925662d54fad71007 100644 (file)
--- 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 eed8531a59fcc30111197ab07aac0bef381a86a6..fc956b463228513c22e52c6e4a35321c8e453764 100644 (file)
--- 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);