diff options
-rw-r--r-- | src/parser/cvc/Cvc.g | 9 | ||||
-rw-r--r-- | src/parser/parser.cpp | 10 | ||||
-rw-r--r-- | src/parser/parser.h | 5 |
3 files changed, 21 insertions, 3 deletions
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); |