Fixing up literal signs

meelgroup · Jun 24, 2023 · 6c41154 · 6c41154
1 parent 99c4ed4
commit 6c41154
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 21 deletions.
diff --git a/src/backward.cpp b/src/backward.cpp
@@ -44,7 +44,7 @@ void Common::fill_assumptions_backward(
 
         uint32_t indic = var_to_indic[var];
         assert(indic != var_Undef);
-        assumptions.push_back(Lit(indic, true));
+        assumptions.push_back(Lit(indic, false));
         if (conf.verb > 5) {
             cout << "Filled assump with indep: " << var << endl;
         }
@@ -66,7 +66,7 @@ void Common::fill_assumptions_backward(
         assert(var < orig_num_vars);
         uint32_t indic = var_to_indic[var];
         assert(indic != var_Undef);
-        assumptions.push_back(Lit(indic, true));
+        assumptions.push_back(Lit(indic, false));
     }
     unknown.resize(j);
     if (conf.verb > 5) {

diff --git a/src/common.cpp b/src/common.cpp
@@ -104,12 +104,8 @@ void Common::add_fixed_clauses()
     indic_to_var.resize(solver->nVars(), var_Undef);
 
     //Indicator variable is TRUE when they are NOT equal
+    vector<Lit> tmp;
     for(uint32_t var: *sampling_set) {
-        //(a=b) = !f
-        //a  V -b V  f
-        //-a V  b V  f
-        //a  V  b V -f
-        //-a V -b V -f
         solver->new_var();
         uint32_t this_indic = solver->nVars()-1;
         //torem_orig.push_back(Lit(this_indic, false));
@@ -121,24 +117,12 @@ void Common::add_fixed_clauses()
         tmp.clear();
         tmp.push_back(Lit(var,               false));
         tmp.push_back(Lit(var+orig_num_vars, true));
-        tmp.push_back(Lit(this_indic,      false));
-        solver->add_clause(tmp);
-
-        tmp.clear();
-        tmp.push_back(Lit(var,               true));
-        tmp.push_back(Lit(var+orig_num_vars, false));
-        tmp.push_back(Lit(this_indic,      false));
-        solver->add_clause(tmp);
-
-        tmp.clear();
-        tmp.push_back(Lit(var,               false));
-        tmp.push_back(Lit(var+orig_num_vars, false));
         tmp.push_back(Lit(this_indic,      true));
         solver->add_clause(tmp);
 
         tmp.clear();
         tmp.push_back(Lit(var,               true));
-        tmp.push_back(Lit(var+orig_num_vars, true));
+        tmp.push_back(Lit(var+orig_num_vars, false));
         tmp.push_back(Lit(this_indic,      true));
         solver->add_clause(tmp);
     }

diff --git a/src/common.h b/src/common.h
@@ -78,7 +78,6 @@ struct Common
     vector<uint32_t>* sampling_set = NULL;
     vector<uint32_t> empty_occs;
 
-    vector<Lit> tmp;
     vector<char> seen;
     uint32_t orig_num_vars = std::numeric_limits<uint32_t>::max();
     uint32_t total_eq_removed = 0;