Fixing up sorting

Author: msoos

src/common.cpp

@@ -218,6 +218,8 @@ void Common::get_incidence()
             incidence[l.var()] = std::max(inc[l.toInt()], inc[(~l).toInt()]);
         } else if (conf.incidence_count == 3) {
             incidence[l.var()] = std::min(inc[l.toInt()],inc[(~l).toInt()]);
+        } else {
+            assert(false && "This is NOT accepted incidence count");
         }
     }
 }

src/common.h

@@ -308,7 +308,7 @@ struct IncidenceSorterCommPartToOtherComm
 template<class T>
 void Common::sort_unknown(T& unknown)
 {
-    if (conf.unknown_sort == 1 || conf.unknown_sort >= 10) {
+    if (conf.unknown_sort == 1) {
         std::sort(unknown.begin(), unknown.end(), IncidenceSorter<uint32_t>(incidence));
     } else if (conf.unknown_sort == 2) {
         std::sort(unknown.begin(), unknown.end(), IncidenceSorter2<uint32_t>(incidence, incidence_probing));

src/config.h

@@ -39,7 +39,7 @@ struct Config {
     int intree = 1;
     int bve_pre_simplify = 1;
     int incidence_count = 3; // this determines what incidence MEANS
-    int unknown_sort = 4; // this determines HOW we sort
+    int unknown_sort = 1; // this determines HOW we sort
     int or_gate_based = 1;
     int xor_gates_based = 1;
     int ite_gate_based = 1;

src/simplify.cpp

@@ -387,10 +387,9 @@ bool Common::remove_definable_by_gates()
     vector<double> var_to_rel_position(orig_num_vars, 1.0);
     for(uint32_t i = 0; i < sampling_set->size(); i++) {
         assert(sampling_set->at(i) < orig_num_vars);
-        var_to_rel_position[sampling_set->at(i)] = (double)i/(double)sampling_set->size();
+        var_to_rel_position[sampling_set->at(i)] = (double)(sampling_set->size()-i)/(double)sampling_set->size();
     }
 
-    std::reverse(sampling_set->begin(), sampling_set->end());
     for(uint32_t v: *sampling_set) {
         assert(seen[v]);
         if (vars_gate_occurs[v].size() == 0) {