Some minor fixed and improvements

Author: msoos

src/arjun.cpp

@@ -322,7 +322,7 @@ DLL_PUBLIC void SimplifiedCNF::get_bve_mapping(SimplifiedCNF& scnf, unique_ptr<C
         }
         bool sign = neg > pos;
 
-        auto overall = scnf.aig_mng.new_const(false);
+        aig_ptr overall = nullptr;
         for(const auto& cl: orig_def) {
             auto current = scnf.aig_mng.new_const(true);
 
@@ -341,9 +341,12 @@ DLL_PUBLIC void SimplifiedCNF::get_bve_mapping(SimplifiedCNF& scnf, unique_ptr<C
                 auto aig = AIG::new_lit(~l);
                 current = AIG::new_and(current, aig);
             }
-            overall = AIG::new_or(overall, current);
+            if (overall == nullptr) overall = current;
+            else overall = AIG::new_or(overall, current);
         }
-        if (sign ^ orig_target.sign()) overall = AIG::new_not(overall);
+        if (overall == nullptr) overall = scnf.aig_mng.new_const(false);
+        if (sign ^ orig_target.sign()) overall->flip();
+
         scnf.defs[orig_target.var()] = overall;
         if (verb >= 5)
             cout << "c o [bve-aig] set aig for var: " << orig_target << " from bve elim: " << overall << endl;

src/arjun.h

@@ -62,6 +62,8 @@ class AIG {
     AIG(const AIG&) = delete;
     AIG& operator=(const AIG&) = delete;
 
+    void flip() { neg = !neg; }
+
     bool invariants() const {
         if (type == AIGT::t_lit) {
             if (l != nullptr || r != nullptr) std::cout << "ERROR: AIG literal has children!" << std::endl;

src/manthan.cpp

@@ -84,6 +84,7 @@ vector<int> lits_to_ints(const vector<Lit>& lits) {
 // LOTS of repairs, fast, but does not terminate: benchmarks-qdimacs/query01_query42_1344n.qdimacs.cnf
 // many repairs, does finish: benchmarks-qdimacs/stmt32_329_378.qdimacs.cnf
 // many-many repairs, does finish: benchmarks-qdimacs/sdlx-fixpoint-10.qdimacs.cnf
+// no repair, learning/mbve does it: rankfunc57_unsigned_64.qdimacs.cnf
 
 template<typename S>
 void Manthan::inject_cnf(S& s, bool also_vars) const {
@@ -396,7 +397,7 @@ void Manthan::print_y_order_occur() const {
     for(const auto& y: y_order) {
         const uint32_t pos = occur_lit[Lit(y, false).toInt()];
         const uint32_t neg = occur_lit[Lit(y, true).toInt()];
-        verb_print(2, "[y-order] var " << setw(4) << y+1
+        verb_print(2, "[manthan] y-order var " << setw(4) << y+1
             << " BW: " << backward_defined.count(y)
             << "   pos occur " << setw(6) << pos
             << "   --  neg occur " << setw(6) << neg);
@@ -578,22 +579,26 @@ void Manthan::bve_and_substitute() {
 
         FHolder::Formula f;
         map<uint32_t, aig_ptr> transformed;
-        auto overall = aig_mng.new_const(false);
 
         // For optimizing which side of the BVE to take
-        /* uint32_t num_pos = 0; */
-        /* uint32_t num_neg = 0; */
-        /* for(const auto& cl: cnf.get_clauses()) { */
-        /*     for(const auto& l: cl) { */
-        /*         if (l.var() == v) { */
-        /*             if (l.sign()) num_neg++; */
-        /*             else num_pos++; */
-        /*             break; */
-        /*         } */
-        /*     } */
-        /* } */
-        /* bool sign = (num_pos >= num_neg); */
-        bool sign = false;
+        uint32_t num_pos = 0;
+        uint32_t num_neg = 0;
+        for(const auto& cl: cnf.get_clauses()) {
+            for(const auto& l: cl) {
+                if (l.var() == v) {
+                    if (l.sign()) num_neg++;
+                    else num_pos++;
+                    break;
+                }
+            }
+        }
+        verb_print(2, "[manthan] bve var " << setw(5) << v+1
+            << " pos occur: " << setw(6) << num_pos
+            << " neg occur: " << setw(6) << num_neg);
+
+        const bool sign = (num_pos >= num_neg);
+        /* const bool sign = false; */
+        aig_ptr overall = nullptr;
         for(const auto& cl: cnf.get_clauses()) {
             bool todo = false;
             for(const auto& l: cl) {
@@ -622,9 +627,11 @@ void Manthan::bve_and_substitute() {
                     }
                 }
             }
-            overall = AIG::new_or(overall, current);
-            if (sign) overall = AIG::new_not(overall);
+            if (overall == nullptr) overall = current;
+            else overall = AIG::new_or(overall, current);
         }
+        if (overall == nullptr) overall = aig_mng.new_const(true);
+        if (sign) overall->flip();
 
         f.aig = AIG::simplify(overall);
         var_to_formula[v] = f;

src/puura.cpp

@@ -144,7 +144,7 @@ void Puura::synthesis_unate(SimplifiedCNF& cnf) {
     var_to_indic.clear();
     var_to_indic.resize(cnf.nVars(), var_Undef);
     for(uint32_t i = 0; i < orig_num_vars; i++) {
-        if (input.count(i)) continue;
+        if (sampl_set.count(i)) continue;
         s->new_var();
         const Lit ind_l = Lit(s->nVars()-1, false);