LASolver: Use map instead of sparse vector to remember atom-to-bounds…

… mapping
usi-verification-and-security · May 25, 2022 · b0f3a3b · b0f3a3b
1 parent 7b8f262
commit b0f3a3b
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 17 deletions.
diff --git a/src/tsolvers/lasolver/LASolver.cc b/src/tsolvers/lasolver/LASolver.cc
@@ -49,12 +49,8 @@ LABoundStore::BoundInfo LASolver::addBound(PTRef leq_tr) {
     }
     int br_pos_idx = boundStore[br_pos].getId();
     int br_neg_idx = boundStore[br_neg].getId();
-
-    int tid = Idx(logic.getPterm(leq_tr).getId());
-    if (LeqToLABoundRefPair.size() <= tid) {
-        LeqToLABoundRefPair.growTo(tid + 1);
-    }
-    LeqToLABoundRefPair[tid] = LABoundRefPair{br_pos, br_neg};
+    assert(LeqToLABoundRefPair.find(leq_tr) == LeqToLABoundRefPair.end());
+    LeqToLABoundRefPair.insert({leq_tr, LABoundRefPair{br_pos, br_neg}});
 
     if (LABoundRefToLeqAsgn.size() <= std::max(br_pos_idx, br_neg_idx)) {
         LABoundRefToLeqAsgn.growTo(std::max(br_pos_idx, br_neg_idx) + 1);
@@ -67,12 +63,7 @@ LABoundStore::BoundInfo LASolver::addBound(PTRef leq_tr) {
 void LASolver::updateBound(PTRef tr)
 {
     // If the bound already exists, do nothing.
-    int id = Idx(logic.getPterm(tr).getId());
-
-    if ((LeqToLABoundRefPair.size() > id) &&
-        !(LeqToLABoundRefPair[id] == LABoundRefPair{LABoundRef_Undef, LABoundRef_Undef})) {
-        return;
-    }
+    if (LeqToLABoundRefPair.find(tr) != LeqToLABoundRefPair.end()) { return; }
 
     LABoundStore::BoundInfo bi = addBound(tr);
     boundStore.updateBound(bi);

diff --git a/src/tsolvers/lasolver/LASolver.h b/src/tsolvers/lasolver/LASolver.h
@@ -69,11 +69,10 @@ class LASolver: public TSolver
 
     vec<PtAsgn>          LABoundRefToLeqAsgn;
     PtAsgn getAsgnByBound(LABoundRef br) const;
-    vec<LABoundRefPair>  LeqToLABoundRefPair;
-    LABoundRefPair getBoundRefPair(const PTRef leq) const {
-        auto index = Idx(logic.getPterm(leq).getId());
-        assert(index < LeqToLABoundRefPair.size_());
-        return LeqToLABoundRefPair[index];
+    std::unordered_map<PTRef, LABoundRefPair, PTRefHash>  LeqToLABoundRefPair;
+    LABoundRefPair getBoundRefPair(PTRef leq) const {
+        assert(LeqToLABoundRefPair.find(leq) != LeqToLABoundRefPair.end());
+        return LeqToLABoundRefPair.at(leq);
     }
 
     // Possible internal states of the solver