diff options
author | Tim King <taking@cs.nyu.edu> | 2017-11-29 08:43:38 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-29 08:43:38 -0800 |
commit | d04b4693b5746cf90d262a50a87734eb12d37664 (patch) | |
tree | 3663332cd532b817f98a66b1467e75b5efaac0e9 /src/parser | |
parent | 41917106e89bd35e99ac313f0a5ca13f72f86d93 (diff) |
Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372)
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/tptp/tptp.cpp | 38 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 2 |
2 files changed, 19 insertions, 21 deletions
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index af675dec1..70430bcae 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -17,11 +17,12 @@ // Do not #include "parser/antlr_input.h" directly. Rely on the header. #include "parser/tptp/tptp.h" +#include <algorithm> +#include <set> + #include "expr/type.h" #include "parser/parser.h" -#include <algorithm> - // ANTLR defines these, which is really bad! #undef true #undef false @@ -183,36 +184,33 @@ void Tptp::includeFile(std::string fileName) { } } -void Tptp::checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula) { - if(lhs.getKind() != CVC4::kind::APPLY_UF) { +void Tptp::checkLetBinding(const std::vector<Expr>& bvlist, Expr lhs, Expr rhs, + bool formula) { + if (lhs.getKind() != CVC4::kind::APPLY_UF) { parseError("malformed let: LHS must be a flat function application"); } - std::vector<CVC4::Expr> v = lhs.getChildren(); + const std::multiset<CVC4::Expr> vars{lhs.begin(), lhs.end()}; if(formula && !lhs.getType().isBoolean()) { parseError("malformed let: LHS must be formula"); } - for(size_t i = 0; i < v.size(); ++i) { - if(v[i].hasOperator()) { - parseError("malformed let: LHS must be flat, illegal child: " + v[i].toString()); + for (const CVC4::Expr& var : vars) { + if (var.hasOperator()) { + parseError("malformed let: LHS must be flat, illegal child: " + + var.toString()); } } - std::sort(v.begin(), v.end()); - std::sort(bvlist.begin(), bvlist.end()); + // ensure all let-bound variables appear on the LHS, and appear only once - for (size_t i = 0; i < bvlist.size(); ++i) { - std::vector<CVC4::Expr>::const_iterator found = - std::lower_bound(v.begin(), v.end(), bvlist[i]); - if (found == v.end() || *found != bvlist[i]) { + for (const Expr& bound_var : bvlist) { + const size_t count = vars.count(bound_var); + if (count == 0) { parseError( "malformed let: LHS must make use of all quantified variables, " "missing `" + - bvlist[i].toString() + "'"); - } - assert(found != v.end()); - std::vector<CVC4::Expr>::const_iterator found2 = found + 1; - if (found2 != v.end() && *found2 == *found) { + bound_var.toString() + "'"); + } else if (count >= 2) { parseError("malformed let: LHS cannot use same bound variable twice: " + - (*found).toString()); + bound_var.toString()); } } } diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index c955d152e..4e03bc576 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -115,7 +115,7 @@ class Tptp : public Parser { void includeFile(std::string fileName); /** Check a TPTP let binding for well-formedness. */ - void checkLetBinding(std::vector<Expr>& bvlist, Expr lhs, Expr rhs, + void checkLetBinding(const std::vector<Expr>& bvlist, Expr lhs, Expr rhs, bool formula); private: |