fix: remove extra space

agurfinkel · Dec 2, 2021 · 79c0870 · 79c0870
1 parent e060231
commit 79c0870
Showing 2 changed files with 4 additions and 31 deletions.
diff --git a/include/Target/Btor/BtorToBtorIRTranslation.h b/include/Target/Btor/BtorToBtorIRTranslation.h
@@ -85,26 +85,6 @@ class Deserialize {
 
   void parseModelLine(Btor2Line *l);
 
-  void filterInits(){
-    size_t i = 0;
-    for (size_t j = 0, sz = inits.size(); j < sz; ++j) {
-        if (inits.at(j)) {
-            inits[i++] = inits.at(j);
-        }
-    }
-    inits.resize(i);
-  }
-
-  void filterNexts() {
-    size_t i = 0;
-    for (size_t j = 0, sz = nexts.size(); j < sz; ++j) {
-      if (nexts.at(j)) {
-        nexts[i++] = nexts.at(j);
-      }
-    }
-    nexts.resize(i);
-  }
-
 ///===----------------------------------------------------------------------===//
 /// Create MLIR module
 ///===----------------------------------------------------------------------===//

diff --git a/lib/Target/Btor/BtorToBtorIRTranslation.cpp b/lib/Target/Btor/BtorToBtorIRTranslation.cpp
@@ -29,15 +29,15 @@ void Deserialize::parseModelLine(Btor2Line *l) {
     break;
 
   case BTOR2_TAG_init:
-    inits[l->args[0]] = l;
+    inits.push_back(l);
     break;
 
   case BTOR2_TAG_input:
     inputs.push_back(l);
     break;
 
   case BTOR2_TAG_next:
-    nexts[l->args[0]] = l;
+    nexts.push_back(l);
     break;
 
   case BTOR2_TAG_state:
@@ -58,25 +58,18 @@ bool Deserialize::parseModelIsSuccessful() {
     return false;
   }
   // register each line that has been parsed
-  auto numLines = btor2parser_max_id(model);
-  inits.resize(numLines, nullptr);
-  nexts.resize(numLines, nullptr);
   Btor2LineIterator it = btor2parser_iter_init(model);
   Btor2Line *line;
   while ((line = btor2parser_iter_next(&it))) {
     parseModelLine(line);
   }
   // ensure each state has a next function
-  for (size_t i = 0; i < states.size(); i++) {
-    Btor2Line *state = states.at(i);
-    if (!nexts[state->id]) {
+  for (auto state : states) {
+    if (reachedLines.find(state->next) == reachedLines.end()) {
       std::cerr << "state " << state->id << " without next function\n";
       return false;
     }
   }
-  // extract relevant inits and nexts
-  filterInits();
-  filterNexts();
 
   return true;
 }