rerun backward synthesis after unate_def with dependency-aware predefined vars

Author: kuldeepmeel

src/arjun.h

@@ -1248,7 +1248,6 @@ class SimplifiedCNF {
         }
     }
     void set_after_backward_round_synth() {
-        assert(!after_backward_round_synth && "Should only be set once");
         after_backward_round_synth = true;
     }
     const auto& get_orig_to_new_var() const {

src/backward.cpp

@@ -415,12 +415,23 @@ void Minimize::backward_round_synth(SimplifiedCNF& cnf, const Arjun::ManthanConf
     vector<char> unknown_set(orig_num_vars, 0);
     vector<uint32_t> unknown;
     auto [input, to_define, backward_defined] = cnf.get_var_types(conf.verb | verbose_debug_enabled, "start backward_round_synth");
+    const auto new_to_orig_var = cnf.get_new_to_orig_var();
+    map<uint32_t, set<uint32_t>> dep_cache;
+    map<uint32_t, set<uint32_t>> backward_depends_on_orig;
     set<uint32_t> pretend_input;
     if (to_define.empty()) {
         verb_print(1, "[backw-synth] No variables to define, returning original CNF");
         return;
     }
-    assert(backward_defined.empty());
+    if (!backward_defined.empty()) {
+        verb_print(1, "[backw-synth] Rerun mode: respecting pre-defined backward vars: "
+            << backward_defined.size());
+        for (const auto& b_new : backward_defined) {
+            assert(new_to_orig_var.count(b_new));
+            const uint32_t b_orig = new_to_orig_var.at(b_new).var();
+            backward_depends_on_orig[b_new] = cnf.get_dependent_vars_recursive(b_orig, dep_cache);
+        }
+    }
 
     add_all_indics_except(input);
     for(const auto& v: input) {
@@ -439,9 +450,8 @@ void Minimize::backward_round_synth(SimplifiedCNF& cnf, const Arjun::ManthanConf
     interp.fill_picolsat(orig_num_vars);
     interp.fill_var_to_indic(var_to_indic);
 
-    for(uint32_t x = 0; x < orig_num_vars; x++) {
-        pretend_input.insert(x); // we pretend that all vars are input vars
-        if (input.count(x)) continue;
+    for(uint32_t x = 0; x < orig_num_vars; x++) pretend_input.insert(x); // we pretend that all vars are input vars
+    for(const auto& x: to_define) {
         unknown.push_back(x);
         unknown_set[x] = 1;
     }
@@ -489,14 +499,24 @@ void Minimize::backward_round_synth(SimplifiedCNF& cnf, const Arjun::ManthanConf
         }
         assert(test_var < orig_num_vars);
         assert(!input.count(test_var));
+        assert(!backward_defined.count(test_var));
         assert(unknown_set[test_var]);
         unknown_set[test_var] = 0;
         pretend_input.erase(test_var);
         verb_print(3, "Testing: " << test_var+1);
 
         //Assumption filling
         assert(test_var != var_Undef);
-        fill_assumptions_backward(assumptions, unknown, unknown_set, pretend_input, input);
+        set<uint32_t> ignore_assumps = input;
+        if (!backward_defined.empty()) {
+            assert(new_to_orig_var.count(test_var));
+            const uint32_t test_orig = new_to_orig_var.at(test_var).var();
+            for (const auto& b_new : backward_defined) {
+                const auto& deps = backward_depends_on_orig.at(b_new);
+                if (deps.count(test_orig)) ignore_assumps.insert(b_new);
+            }
+        }
+        fill_assumptions_backward(assumptions, unknown, unknown_set, pretend_input, ignore_assumps);
         assumptions.push_back(Lit(test_var, false));
         assumptions.push_back(Lit(test_var + orig_num_vars, true));
         solver->set_no_confl_needed();
@@ -556,6 +576,7 @@ void Minimize::backward_round_synth(SimplifiedCNF& cnf, const Arjun::ManthanConf
         const auto& aig = interp.get_defs()[v];
         if (aig == nullptr) continue;
         assert(input.count(v) == 0);
+        assert(backward_defined.count(v) == 0);
     }
     cnf.map_aigs_to_orig(interp.get_defs(), orig_num_vars);
     cnf.set_after_backward_round_synth();

src/main.cpp

@@ -83,6 +83,7 @@ int do_synth_bve = true;
 int do_pre_backbone = 0;
 int manthan_rep_mult = 4;
 int manthan_strategy = 0;
+constexpr uint32_t unate_def_backward_rerun_threshold = 8;
 
 int synthesis = false;
 int do_unate = false;
@@ -386,8 +387,28 @@ void do_synthesis() {
     }
 
     if (!candidate_all_specified && do_unate_def && !cnf.synth_done()) {
+        uint32_t unate_def_newly_defined = 0;
+        auto [input_before_unate_def, to_define_before_unate_def, backward_before_unate_def] =
+            cnf.get_var_types(0 | verbose_debug_enabled, "pre_unate_def_count");
         arjun->standalone_unate_def(cnf);
         if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-unsat_unate_def.aig");
+        auto [input_after_unate_def, to_define_after_unate_def, backward_after_unate_def] =
+            cnf.get_var_types(0 | verbose_debug_enabled, "post_unate_def_count");
+        (void)input_after_unate_def;
+        (void)backward_after_unate_def;
+        if (to_define_before_unate_def.size() >= to_define_after_unate_def.size()) {
+            unate_def_newly_defined += to_define_before_unate_def.size() - to_define_after_unate_def.size();
+        }
+
+        if (do_minim_indep && !cnf.synth_done()
+            && unate_def_newly_defined >= unate_def_backward_rerun_threshold) {
+            cout << "c o [synth] unate_def defined " << unate_def_newly_defined
+                << " vars (threshold " << unate_def_backward_rerun_threshold
+                << "), rerunning backward synthesis" << endl;
+            arjun->standalone_backward_round_synth(cnf, mconf);
+            if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-minim_idep_synt-post_unate_def.aig");
+            cnf.simplify_aigs(conf.verb);
+        }
     }
 
     auto mconf_orig = mconf;