diff options
| author | Tim King <taking@google.com> | 2015-12-15 14:35:34 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-12-15 15:28:45 -0800 |
| commit | 3f29ad74a705883181d9c934a0f772d4850b0b0e (patch) | |
| tree | 8644e56a4d03390d72eac9bbb7ed7a35cc3b221a /src/parser/cvc/Cvc.g | |
| parent | c358ccba3bf54a85ed9503b636c1f0bab381bc05 (diff) | |
Breaking the include cycle between Record and Expr.
Diffstat (limited to 'src/parser/cvc/Cvc.g')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 460b1ee03..ff3753a67 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -1559,8 +1559,7 @@ recordStore[CVC4::Expr& f] PARSER_STATE->parseError(ss.str()); } const Record& rec = RecordType(t).getRecord(); - Record::const_iterator fld = rec.find(id); - if(fld == rec.end()) { + if(! rec.contains(id)) { PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } f2 = MK_EXPR(MK_CONST(RecordSelect(id)), f); @@ -1687,8 +1686,7 @@ postfixTerm[CVC4::Expr& f] PARSER_STATE->parseError("record-select applied to non-record"); } const Record& rec = RecordType(t).getRecord(); - Record::const_iterator fld = rec.find(id); - if(fld == rec.end()) { + if(!rec.contains(id)){ PARSER_STATE->parseError(std::string("no such field `") + id + "' in record"); } f = MK_EXPR(MK_CONST(RecordSelect(id)), f); |