From d04b4693b5746cf90d262a50a87734eb12d37664 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Wed, 29 Nov 2017 08:43:38 -0800
Subject: [PATCH] =?utf8?q?Simplifying=20the=20conditions=20in=20checkLetBi?=
 =?utf8?q?nding=20to=20avoid=20using=20iterator=E2=80=A6=20(#1372)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=utf8
Content-Transfer-Encoding: 8bit

---
 src/parser/tptp/tptp.cpp | 38 ++++++++++++++++++--------------------
 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:
-- 
2.30.2