diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-11-28 17:37:57 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-11-28 17:37:57 +0000 |
| commit | 83cf3909b50af1d37735a252e79d550aac08cf7a (patch) | |
| tree | c4d09b7aef51e8f38aeb5953e0d091c9fc0fb03c /src/parser/cvc | |
| parent | 629d04c45e1606a4d0ecef2717924e839d5daec3 (diff) | |
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.)
Diffstat (limited to 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 9 |
1 files changed, 6 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); } } } |