Removing non-working components

meelgroup · Apr 12, 2024 · 2c4a797 · 2c4a797
1 parent 4dc5fc7
commit 2c4a797
Show file tree

Hide file tree

Showing 13 changed files with 0 additions and 795 deletions.
diff --git a/scripts/synth.sh b/scripts/synth.sh
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -59,7 +59,6 @@ target_link_libraries(arjun
 )
 
 add_executable(arjun-bin main.cpp)
-# add_executable(unate-bin main-unate.cpp)
 add_executable(arjun-example example.cpp)
 
 IF (ZLIB_FOUND)
@@ -77,13 +76,7 @@ set_target_properties(arjun-bin PROPERTIES
     RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
     INSTALL_RPATH_USE_LINK_PATH TRUE)
 
-# set_target_properties(unate-bin PROPERTIES
-#     OUTPUT_NAME unate
-#     RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
-#     INSTALL_RPATH_USE_LINK_PATH TRUE)
-
 target_link_libraries(arjun-bin ${arjun_bin_exec_link_libs} arjun)
-# target_link_libraries(unate-bin ${arjun_bin_exec_link_libs} arjun)
 set_target_properties(arjun-example PROPERTIES
     OUTPUT_NAME example
     RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}

diff --git a/src/arjun.cpp b/src/arjun.cpp
@@ -192,20 +192,6 @@ DLL_PUBLIC vector<uint32_t> Arjun::run_backwards() {
     return arjdata->common.sampling_set;
 }
 
-DLL_PUBLIC vector<uint32_t> Arjun::synthesis_define()
-{
-    assert(!arjdata->common.already_duplicated);
-    arjdata->common.conf.simp = false;
-    std::set<uint32_t> input;
-    for(const auto& v: arjdata->common.sampling_set) input.insert(v);
-    arjdata->common.init();
-    if (!arjdata->common.preproc_and_duplicate()) goto end;
-    arjdata->common.synthesis_define(input);
-
-    end:
-    return arjdata->common.sampling_set;
-}
-
 DLL_PUBLIC vector<uint32_t> Arjun::extend_sampl_set()
 {
     assert(!arjdata->common.already_duplicated);
@@ -280,7 +266,6 @@ set_get_macro(double, no_gates_below)
 set_get_macro(std::string, specified_order_fname)
 set_get_macro(bool, bce)
 set_get_macro(bool, bve_during_elimtofile)
-set_get_macro(bool, do_unate)
 set_get_macro(bool, weighted)
 
 DLL_PUBLIC void Arjun::set_pred_forever_cutoff(int pred_forever_cutoff) {

diff --git a/src/arjun.h b/src/arjun.h
@@ -154,7 +154,6 @@ namespace ArjunNS {
         const std::vector<uint32_t>& get_current_indep_set() const;
         std::vector<uint32_t> run_backwards();
         std::vector<uint32_t> extend_sampl_set();
-        std::vector<uint32_t> synthesis_define();
         uint32_t get_orig_num_vars() const;
         const std::vector<uint32_t>& get_orig_sampl_vars() const;
         const std::vector<uint32_t>& get_empty_sampl_vars() const;
@@ -196,7 +195,6 @@ namespace ArjunNS {
         void set_gauss_jordan(bool gauss_jordan);
         void set_find_xors(bool find_xors);
         void set_ite_gate_based(bool ite_gate_based);
-        void set_do_unate(bool do_unate);
         void set_irreg_gate_based(const bool irreg_gate_based);
         void set_gate_sort_special(bool gate_sort_special);
         //void set_polar_mode(CMSat::PolarityMode mode);
@@ -210,7 +208,6 @@ namespace ArjunNS {
         mpz_class get_multiplier_weight() const;
 
         //Get config
-        bool get_do_unate() const;
         std::string get_specified_order_fname() const;
         double get_no_gates_below() const;
         bool get_simp() const;

diff --git a/src/common.h b/src/common.h
@@ -164,9 +164,6 @@ struct Common
         vector<Lit>& assumptions,
         const T& indep);
     void extend_round();
-    void synthesis_define(const std::set<uint32_t>& input);
-    void generate_picosat(const vector<Lit>& assumptions , uint32_t test_var
-        , const set<uint32_t>& indep);
 
     //Sorting
     template<class T> void sort_unknown(T& unknown);

diff --git a/src/config.h b/src/config.h
@@ -48,7 +48,6 @@ struct Config {
     int backward = 1;
     int gauss_jordan = 0;
     int bce = 0;
-    int do_unate = 0;
     double no_gates_below = 0.01;
     std::string specified_order_fname;
     uint32_t backw_max_confl = 5000*10;

diff --git a/src/extend.cpp b/src/extend.cpp
@@ -26,9 +26,6 @@
 #include <algorithm>
 #include <set>
 #include <map>
-extern "C" {
-#include "mpicosat/mpicosat.h"
-}
 
 using namespace ArjunInt;
 
@@ -81,199 +78,6 @@ void Common::add_all_indics()
     }
 }
 
-// lit to picolit
-int lit_to_pl(const Lit l) {
-    int picolit = (l.var()+1) * (l.sign() ? -1 : 1);
-    return picolit;
-}
-
-void Common::generate_picosat(const vector<Lit>& assumptions , uint32_t test_var
-        , const set<uint32_t>& inputs) {
-
-    // FIRST, we get an UNSAT core
-    PicoSAT* ps = picosat_init();
-    int pret = picosat_enable_trace_generation(ps);
-    release_assert(pret != 0 && "Traces cannot be generated in PicoSAT");
-    map<uint32_t, vector<Lit>> cl_map;
-    uint32_t cl_num = 0;
-
-    solver->start_getting_constraints(false);
-    bool ret = true;
-    vector<Lit> cl;
-    bool is_xor, rhs;
-    for(uint32_t i = 0; i < solver->nVars(); i++) picosat_inc_max_var(ps);
-    while(ret) {
-        ret = solver->get_next_constraint(cl, is_xor, rhs);
-        if (!ret) break;
-        assert(!is_xor); assert(rhs);
-        cl_map[cl_num++] = cl;
-        for (const auto& l: cl) picosat_add(ps, lit_to_pl(l));
-        picosat_add(ps, 0);
-    }
-    solver->end_getting_constraints();
-    for(const auto& l: assumptions) {
-        cl_map[cl_num++] = vector<Lit>{l};
-        picosat_add(ps, lit_to_pl(l));
-        picosat_add(ps, 0);
-    }
-    pret = picosat_sat(ps, 10000);
-    release_assert(pret == PICOSAT_UNSATISFIABLE);
-
-    // NEXT we extract information we'll need to make simplified UNSAT core
-    // in particular, we'll make sure that variables that are equivalent are
-    // not represented as two different variables
-    map<uint32_t, uint32_t> indic_map;
-    for(const auto& m: cl_map) {
-        if (picosat_coreclause(ps, m.first)) {
-            if (m.second.size() != 1) continue;
-            Lit l = m.second[0];
-            if (l.var() < indic_to_var.size() && l.var() >= orig_num_vars*2) {
-                /* cout << "c indic-to-var: " << l << " -- " << indic_to_var[l.var()]+1 << endl; */
-                indic_map[indic_to_var[l.var()]+orig_num_vars] = indic_to_var[l.var()];
-            }
-        }
-    }
-
-    // NEXT we generate the small CNF that is UNSAT and is simplified
-    // TODO: simplify away the SET values of x && \neg x
-    vector<vector<Lit>> mini_cls;
-    if (seen.size() < solver->nVars()*2) seen.resize(solver->nVars()*2, 0);
-    for(const auto& m: cl_map) {
-        if (picosat_coreclause(ps, m.first)) {
-            bool indic = false;
-            bool taut = false;
-            cl = m.second;
-            cl.clear();
-            for(auto l: m.second) {
-                if (l.var() < indic_to_var.size() && l.var() >= orig_num_vars*2)
-                    indic = true;
-                if (indic_map.count(l.var())) l = Lit(indic_map[l.var()], l.sign());
-                if (seen[(~l).toInt()]) {taut = true; break;}
-                seen[l.toInt()] = true;
-                cl.push_back(l);
-            }
-            if (taut) goto end;
-            if (indic && cl.size() == 1) {
-                // only indic, skip
-                assert(cl[0].sign() == false);
-                goto end;
-            }
-            mini_cls.push_back(cl);
-            end:
-            for(const auto& l: cl) seen[l.toInt()] = false;
-        }
-    }
-
-    // Write the CORE file
-    std::stringstream name;
-    name << "core-" << test_var+1 << ".cnf";
-    auto f = std::ofstream(name.str());
-    f << "p cnf " << orig_num_vars*2 << " " << mini_cls.size() << endl;
-    f << "c orig_num_vars: " << orig_num_vars << endl;
-    f << "c output: " << test_var +1 << endl;
-    f << "c output2: " << orig_num_vars+test_var +1 << endl;
-    f << "c num inputs: " << inputs.size() << endl;
-    f << "c inputs: "; for(const auto& l: inputs) f << (l+1) << " "; f << endl;
-    for(const auto& c: mini_cls) f << c << " 0" << endl;
-    f.close();
-    picosat_reset(ps);
-
-    // picosat on the core only, on a simplified CNF
-    ps = picosat_init();
-    pret = picosat_enable_trace_generation(ps);
-    release_assert(pret != 0 && "Traces cannot be generated in PicoSAT");
-    for(uint32_t i = 0; i < orig_num_vars*2; i++) picosat_inc_max_var(ps);
-    for(const auto& c: mini_cls) {
-        for(const auto& l: c) picosat_add(ps, lit_to_pl(l));
-        picosat_add(ps, 0);
-    }
-    pret = picosat_sat(ps, 10000);
-    release_assert(pret == PICOSAT_UNSATISFIABLE);
-    name.str("");
-    name.clear();
-    name << "proof-" << test_var+1 << ".trace";
-    FILE* trace = fopen(name.str().c_str(), "w");
-    picosat_write_extended_trace (ps, trace);
-    picosat_reset(ps);
-    fclose(trace);
-}
-
-void Common::synthesis_define(const set<uint32_t>& input) {
-    assert(already_duplicated);
-    solver->set_verbosity(0);
-    add_all_indics();
-
-    for(const auto& x: seen) assert(x == 0);
-    double start_round_time = cpuTimeTotal();
-    set<uint32_t> indep;
-
-    //Initially, all of samping_set is unknown
-    vector<uint32_t> unknown;
-    for(uint32_t i = 0; i < orig_num_vars; i++) {
-        if (solver->removed_var(i)) continue;
-        indep.insert(i);
-        if (input.count(i)) continue;
-        unknown.push_back(i);
-    }
-
-    sort_unknown(unknown);
-    verb_print(1,"[arjun] Start unknown size: " << unknown.size());
-
-    vector<Lit> assumptions;
-    uint32_t tot_ret_false = 0;
-    while(!unknown.empty()) {
-        uint32_t test_var = unknown.back();
-        unknown.pop_back();
-
-        assert(test_var < orig_num_vars);
-        verb_print(5, "Testing: " << test_var);
-
-        //Assumption filling
-        assert(test_var != var_Undef);
-        indep.erase(test_var);
-        fill_assumptions_extend(assumptions, indep);
-        assumptions.push_back(Lit(test_var, false));
-        assumptions.push_back(Lit(test_var + orig_num_vars, true));
-
-        //TODO: Actually, we should get conflict, that will make things easier
-        solver->set_no_confl_needed();
-
-        lbool ret = l_Undef;
-        // TODO we probably shouldn't use this, removing.
-        /* solver->set_max_confl(conf.backw_max_confl); */
-        ret = solver->solve(&assumptions);
-        if (ret == l_False) {
-            tot_ret_false++;
-            verb_print(5, "[arjun] extend solve(): False");
-        } else if (ret == l_True) {
-            verb_print(5, "[arjun] extend solve(): True");
-        } else if (ret == l_Undef) {
-            verb_print(5, "[arjun] extend solve(): Undef");
-        }
-
-        if (ret == l_Undef) {
-            // Timed out, we'll treat is as unknown
-            assert(test_var < orig_num_vars);
-            indep.insert(test_var);
-        } else if (ret == l_True) {
-            // Not fully dependent
-            indep.insert(test_var);
-        } else if (ret == l_False) {
-            // Dependent fully on `indep`
-            // TODO: run get_conflict and then we know which were
-            // actually needed, so we can do an easier generation/check
-            generate_picosat(assumptions, test_var, indep);
-        }
-    }
-    sampling_set.clear();
-    for(const auto& i: indep) sampling_set.push_back(i);
-
-    verb_print(1, "[arjun] UNSAT-based define finished "
-            << " final extension: " << tot_ret_false
-            << " T: " << std::setprecision(2) << std::fixed << (cpuTime() - start_round_time));
-    if (conf.verb >= 2) solver->print_stats();
-}
-
 void Common::extend_round()
 {
     assert(already_duplicated);