New CNF dumping setup, fixing empty etc

Author: msoos

src/arjun.cpp

@@ -312,19 +312,18 @@ DLL_PUBLIC const vector<Lit> Arjun::get_internal_cnf(uint32_t& num_cls) const
     return cnf;
 }
 
-static std::pair<vector<vector<Lit>>, uint32_t> get_simplified_cnf(
-        SATSolver* solver, vector<uint32_t>& sampl_vars, const bool renumber)
+static void get_simplified_cnf(
+        SATSolver* solver, vector<uint32_t>& sampl_vars, const bool renumber,
+        vector<vector<Lit>>& cnf, uint32_t& nvars)
 {
-    vector<vector<Lit>> cnf;
+    assert(cnf.empty());
     solver->start_getting_small_clauses(
         std::numeric_limits<uint32_t>::max(),
         std::numeric_limits<uint32_t>::max(),
         false, //red
         false, //bva vars
         renumber); //simplified
-
     if (renumber) sampl_vars = solver->translate_sampl_set(sampl_vars);
-    std::sort(sampl_vars.begin(), sampl_vars.end());
 
     bool ret = true;
     vector<Lit> clause;
@@ -335,8 +334,7 @@ static std::pair<vector<vector<Lit>>, uint32_t> get_simplified_cnf(
         }
     }
     solver->end_getting_small_clauses();
-    return std::make_pair(cnf,
-            renumber ? solver->simplified_nvars() :  solver->nVars());
+    nvars = renumber ? solver->simplified_nvars() :  solver->nVars();
 }
 
 static void fill_solver(
@@ -387,8 +385,7 @@ static void fill_solver(
     }
 }
 
-DLL_PUBLIC std::tuple<std::pair<std::vector<std::vector<CMSat::Lit>>, uint32_t>, std::vector<uint32_t>>
-Arjun::get_fully_simplified_renumbered_cnf(
+DLL_PUBLIC SimplifiedCNF Arjun::get_fully_simplified_renumbered_cnf(
     const vector<uint32_t>& sampl_vars, //contains empty_vars!
     const uint32_t orig_num_vars,
     const bool sparsify,
@@ -438,10 +435,17 @@ Arjun::get_fully_simplified_renumbered_cnf(
     str += string(", must-scc-vrepl, must-renumber");
     solver.simplify(&dont_elim, &str);
 
-    vector<uint32_t> new_sampl_set;
-    for(const auto& l: dont_elim) new_sampl_set.push_back(l.var());
-    auto cnf = get_simplified_cnf(&solver, new_sampl_set, renumber);
-    return std::make_tuple(cnf, new_sampl_set);
+    vector<uint32_t> new_sampl_vars (sampl_vars);
+    SimplifiedCNF cnf;
+    get_simplified_cnf(&solver, new_sampl_vars, renumber, cnf.cnf, cnf.nvars);
+
+    vector<uint32_t> empty_occs;
+    if (arjdata->common.conf.empty_occs_based)
+        solver.find_equiv_subformula(new_sampl_vars, empty_occs);
+    std::sort(new_sampl_vars.begin(), new_sampl_vars.end());
+    cnf.sampling_vars = new_sampl_vars;
+    cnf.empty_occs = empty_occs.size();
+    return cnf;
 }
 
 DLL_PUBLIC void Arjun::set_pred_forever_cutoff(int pred_forever_cutoff)

src/arjun.h

@@ -35,6 +35,13 @@ THE SOFTWARE.
 #endif
 
 namespace ArjunNS {
+    struct SimplifiedCNF {
+        std::vector<std::vector<CMSat::Lit>> cnf;
+        std::vector<uint32_t> sampling_vars;
+        uint32_t nvars;
+        uint32_t empty_occs;
+    };
+
     struct ArjPrivateData;
     #ifdef _WIN32
     class __declspec(dllexport) Arjun
@@ -73,8 +80,7 @@ namespace ArjunNS {
         bool get_next_small_clause(std::vector<CMSat::Lit>& ret); //returns FALSE if no more
         void end_getting_small_clauses();
         const std::vector<CMSat::Lit> get_internal_cnf(uint32_t& num_cls) const;
-        std::tuple<std::pair<std::vector<std::vector<CMSat::Lit>>, uint32_t>, std::vector<uint32_t>>
-        get_fully_simplified_renumbered_cnf(
+        SimplifiedCNF get_fully_simplified_renumbered_cnf(
             const std::vector<uint32_t>& sampl_vars,
             const uint32_t orig_num_vars,
             const bool sparsify = true,

src/main.cpp

@@ -313,28 +313,23 @@ void readInAFile(const string& filename)
     #endif
 }
 
-void dump_cnf(const std::pair<vector<vector<Lit>>,
-        uint32_t>& cnf, const vector<uint32_t>& sampl_set,
-        const uint32_t multiply = 0)
+void dump_cnf(const ArjunNS::SimplifiedCNF& simpcnf)
 {
-    uint32_t num_cls = cnf.first.size();
-    uint32_t max_var = cnf.second;
+    uint32_t num_cls = simpcnf.cnf.size();
     std::ofstream outf;
     outf.open(elimtofile.c_str(), std::ios::out);
-    outf << "p cnf " << max_var << " " << num_cls << endl;
+    outf << "p cnf " << simpcnf.nvars << " " << num_cls << endl;
 
     //Add projection
     outf << "c ind ";
-    for(const auto& v: sampl_set) {
-        assert(v < max_var);
+    for(const auto& v: simpcnf.sampling_vars) {
+        assert(v < simpcnf.nvars);
         outf << v+1  << " ";
     }
     outf << "0\n";
 
-    for(const auto& cl: cnf.first) {
-        outf << cl << " 0\n";
-    }
-    outf << "c MUST MUTIPLY BY 2**" << multiply << endl;
+    for(const auto& cl: simpcnf.cnf) outf << cl << " 0\n";
+    outf << "c MUST MUTIPLY BY 2**" << simpcnf.empty_occs << endl;
 }
 
 void elim_to_file(
@@ -346,7 +341,7 @@ void elim_to_file(
     auto ret = arjun->get_fully_simplified_renumbered_cnf(
         sampl_vars, orig_num_vars, sparsify, renumber);
 
-    dump_cnf(std::get<0>(ret), std::get<1>(ret), 0);
+    dump_cnf(ret);
     cout << "c [arjun] Done dumping. T: "
         << std::setprecision(2) << (cpuTime() - dump_start_time) << endl;
 }