early: optimize subsumption checking

src/complement_alg_mh.cpp

@@ -44,9 +44,12 @@ class mstate_mh : public abstract_complement_alg::mstate
       auto rhs_mh = dynamic_cast<const mstate_mh*>(&rhs);
 
       auto S_subs = std::includes(states_.begin(), states_.end(), rhs_mh->states_.begin(), rhs_mh->states_.end());
-      auto B_subs = std::includes(breakpoint_.begin(), breakpoint_.end(), rhs_mh->breakpoint_.begin(), rhs_mh->breakpoint_.end());
+      if(!S_subs) {
+        return false;
+      }
 
-      return (S_subs && B_subs);
+      auto B_subs = std::includes(breakpoint_.begin(), breakpoint_.end(), rhs_mh->breakpoint_.begin(), rhs_mh->breakpoint_.end());
+      return B_subs;
   };
 
   virtual bool subsum_less_early_plus(const mstate& rhs) override {

src/complement_alg_ncsb.cpp

@@ -45,13 +45,17 @@ class mstate_ncsb : public abstract_complement_alg::mstate
   virtual bool subsum_less_early(const mstate& rhs) override {
     auto rhs_ncsb = dynamic_cast<const mstate_ncsb*>(&rhs);
 
+    auto S_subs = std::includes(this->safe_.begin(), this->safe_.end(), rhs_ncsb->safe_.begin(), rhs_ncsb->safe_.end());
+    if(!S_subs) {
+      return false;
+    }
+
     std::set<unsigned> S_and_B;
     set_union(safe_.begin(), safe_.end(), breakpoint_.begin() , breakpoint_.end(), std::inserter(S_and_B, S_and_B.begin()));
 
     auto B_subs = std::includes(S_and_B.begin(), S_and_B.end(), rhs_ncsb->breakpoint_.begin(), rhs_ncsb->breakpoint_.end());
-    auto S_subs = std::includes(this->safe_.begin(), this->safe_.end(), rhs_ncsb->safe_.begin(), rhs_ncsb->safe_.end());
-
-    return (B_subs && S_subs);
+
+    return B_subs;
   };
 
   friend class kofola::complement_ncsb;

src/complement_sync.hpp

@@ -238,8 +238,11 @@ namespace cola
 
             bool subsum_less_early(const uberstate& b)
             {
+                if(!std::includes(this->reached_states_.begin(), this->reached_states_.end(), b.reached_states_.begin(), b.reached_states_.end())) {
+                    return false;
+                }
                 for(unsigned i = 0; i < part_macrostates_.size(); i++) {
-                    if(!(std::includes(this->reached_states_.begin(), this->reached_states_.end(), b.reached_states_.begin(), b.reached_states_.end()) && this->part_macrostates_[i]->subsum_less_early(*(b.part_macrostates_[i])))) {
+                    if(!this->part_macrostates_[i]->subsum_less_early(*(b.part_macrostates_[i]))) {
                         return false;
                     }
                 }

src/emptiness_check.cpp

@@ -218,8 +218,9 @@ namespace kofola {
                 auto dst_mstate = succs.back();
                 succs.pop_back();
 
-                if(empty_lang(dst_mstate))
+                if(empty_lang(dst_mstate)) {
                     continue;
+                }
 
                 // init structure
                 if(dfs_num_.count(dst_mstate) == 0)

src/inclusion_check.cpp

@@ -249,20 +249,14 @@ namespace kofola {
         std::cout << std::endl << "==================" << std::endl; 
     }
 
-    bool inclusion_check::subsum_less_early(const std::shared_ptr<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b) {
-        auto casted_a = a;
-        auto casted_b = b;
-
+    bool inclusion_check::subsum_less_early(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& b) {
         // between states of A only identity
-        return (casted_a->state_.first == casted_b->state_.first && aut_B_compl_.subsum_less_early(casted_a->state_.second, casted_b->state_.second));
+        return (a->state_.first == b->state_.first && aut_B_compl_.subsum_less_early(a->state_.second, b->state_.second));
     }
 
-    bool inclusion_check::subsum_less_early_plus(const std::shared_ptr<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b) {
-        auto casted_a = a;
-        auto casted_b = b;
-
+    bool inclusion_check::subsum_less_early_plus(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& b) {
         // between states of A only identity
-        return (casted_a->state_.first == casted_b->state_.first && aut_B_compl_.subsum_less_early_plus(casted_a->state_.second, casted_b->state_.second));
+        return (a->state_.first == b->state_.first && aut_B_compl_.subsum_less_early_plus(a->state_.second, b->state_.second));
     }
 
     cola::tnba_complement::vec_state_taggedcol inclusion_check::get_successors_compl(unsigned compl_state, const bdd& letter) {

src/inclusion_check.hpp

@@ -128,10 +128,10 @@ namespace kofola {
         std::vector<std::shared_ptr<inclusion_mstate>> get_succs(const std::shared_ptr<inclusion_mstate> &src);
 
         /// returns true if a is early simul. less than b
-        bool subsum_less_early(const std::shared_ptr<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b);
+        bool subsum_less_early(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& b);
 
         /// returns true if a is early+1 simul. less than b
-        bool subsum_less_early_plus(const std::shared_ptr<inclusion_mstate> a, const std::shared_ptr<inclusion_mstate> b);
+        bool subsum_less_early_plus(const std::shared_ptr<inclusion_mstate>& a, const std::shared_ptr<inclusion_mstate>& b);
 
         /// returns true when the provided mark_t satisfies acc_cond_, for the need of emptiness check
         bool is_accepting(spot::acc_cond::mark_t inf_cond);