Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372)

diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index af675dec13abff7191a67df54381c19a8355737c..70430bcaecdafb090fbf76626a613eee4b9ca832 100644 (file)
--- 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 c955d152e190f26186ef02984daec05ccf12b29a..4e03bc57624de529a09835fb8d77849acb0afb69 100644 (file)
--- 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: