added option to pass candidate functions

src/arjun.cpp

@@ -447,7 +447,10 @@ DLL_PUBLIC void SimplifiedCNF::get_fixed_values(
         if (l.var() >= nVars()) continue;
         Lit orig_lit = new_to_orig_var.at(l.var());
         orig_lit ^= l.sign();
-        assert(scnf.defs[orig_lit.var()] == nullptr && "Variable must not already have a definition");
+        if (scnf.defs[orig_lit.var()] != nullptr) {
+            if (scnf.preserve_existing_defs) continue;
+            assert(false && "Variable must not already have a definition");
+        }
         scnf.defs[orig_lit.var()] = scnf.aig_mng.new_const(!orig_lit.sign());
     }
 }
@@ -458,13 +461,16 @@ DLL_PUBLIC void SimplifiedCNF::add_fixed_values(const vector<Lit>& fixed) {
         if (l.var() >= nVars()) continue;
         Lit orig_lit = new_to_orig_var.at(l.var());
         orig_lit ^= l.sign();
-        assert(defs[orig_lit.var()] == nullptr && "Variable must not already have a definition");
+        if (defs[orig_lit.var()] != nullptr) {
+            if (preserve_existing_defs) continue;
+            assert(false && "Variable must not already have a definition");
+        }
         defs[orig_lit.var()] = aig_mng.new_const(!orig_lit.sign());
     }
 }
 
 DLL_PUBLIC void SimplifiedCNF::map_aigs_to_orig(const vector<aig_ptr>& aigs_orig, const uint32_t max_num_vars,
-            std::optional<std::reference_wrapper<const std::map<uint32_t, CMSat::Lit>>> back_map) {
+            std::optional<std::reference_wrapper<const std::map<uint32_t, CMSat::Lit>>> back_map, const bool overwrite_existing) {
     const auto new_to_orig_var = get_new_to_orig_var();
     auto aigs = AIG::deep_clone_vec(aigs_orig);
     set<aig_ptr> visited;
@@ -504,7 +510,16 @@ DLL_PUBLIC void SimplifiedCNF::map_aigs_to_orig(const vector<aig_ptr>& aigs_orig
         if (aig == nullptr) continue;
 
         auto l = new_to_orig_var.at(v);
-        assert(defs[l.var()] == nullptr && "Variable must not already have a definition");
+        if (defs[l.var()] != nullptr) {
+            if (overwrite_existing) {
+                // Explicitly requested by caller (candidate verification path).
+            } else if (preserve_existing_defs) {
+                // Candidate-provided defs are authoritative.
+                continue;
+            } else {
+                assert(false && "Variable must not already have a definition");
+            }
+        }
         assert(orig_sampl_vars.count(l.var()) == 0 && "Original sampling var cannot have definition via extend_synth or backward_round_synth");
         if (l.sign()) defs[l.var()] = AIG::new_not(aig);
         else defs[l.var()] = aig;
@@ -633,6 +648,7 @@ DLL_PUBLIC SimplifiedCNF SimplifiedCNF::get_cnf(
     scnf.new_vars(solver->simplified_nvars());
     scnf.aig_mng = aig_mng;
     scnf.need_aig = need_aig;
+    scnf.preserve_existing_defs = preserve_existing_defs;
     if (need_aig) {
         scnf.defs = defs;
         scnf.aig_mng = aig_mng;

src/arjun.h

@@ -892,6 +892,7 @@ class SimplifiedCNF {
         backbone_done = other.backbone_done;
         weights = other.weights;
         orig_to_new_var = other.orig_to_new_var;
+        preserve_existing_defs = other.preserve_existing_defs;
         if (!need_aig) {
             assert(defs.empty());
             assert(other.defs.empty());
@@ -1205,7 +1206,7 @@ class SimplifiedCNF {
     std::vector<CMSat::lbool> extend_sample(const std::vector<CMSat::lbool>& sample, const bool relaxed = false) const;
 
     void map_aigs_to_orig(const std::vector<aig_ptr>& aigs, const uint32_t max_num_vars,
-            std::optional<std::reference_wrapper<const std::map<uint32_t, CMSat::Lit>>> back_map = std::nullopt);
+            std::optional<std::reference_wrapper<const std::map<uint32_t, CMSat::Lit>>> back_map = std::nullopt, bool overwrite_existing = false);
 
     SimplifiedCNF get_cnf(
             std::unique_ptr<CMSat::SATSolver>& solver,
@@ -1247,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 {
@@ -1275,9 +1275,12 @@ class SimplifiedCNF {
         AIG::simplify_aigs(verb, defs);
     }
     const auto& get_aig_mng() const { return aig_mng; }
+    void set_preserve_existing_defs(bool b) { preserve_existing_defs = b; }
+    bool get_preserve_existing_defs() const { return preserve_existing_defs; }
     void import_candidate_functions(const std::string& fname, int verb = 0);
 
 private:
+    bool preserve_existing_defs = false;
     bool after_backward_round_synth = false;
     bool need_aig = false;
     std::vector<std::vector<CMSat::Lit>> clauses;
@@ -1376,6 +1379,7 @@ class Arjun
         int manthan_order = 0;
         int manthan_on_the_fly_order = 0;
         int one_repair_per_loop = 0;
+        int start_from_candidate_cex = 0;
         int do_td_contract = 1; // contract over the input variables
         int td_max_edges = 70000;
         std::string td_visualize_dot_file = "";

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,13 +83,15 @@ 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;
 int do_unate_def = false;
 int do_revbce = false;
 int do_minim_indep = true;
 string debug_minim;
+string candidate_defs_file;
 double cms_glob_mult = -1.0;
 int mode = 0;
 unique_ptr<FieldGen> fg = nullptr;
@@ -165,6 +167,7 @@ void add_arjun_options() {
     // synth -- debug
     myopt("--manthancnf", mconf.write_manthan_cnf, string, "Write Manthan CNF to this file");
     myopt("--debugsynth", conf.debug_synth, string,"Debug synthesis, prefix with this fname");
+    myopt("--candidatefuns", candidate_defs_file, string, "Load candidate functions from AIG-defs file");
 
 
     // Simplification options for minim
@@ -298,73 +301,140 @@ void do_synthesis() {
     check_cnf_sat(cnf);
     cout << "c o ignoring --backbone option, doing backbone for synth no matter what" << endl;
     cnf.get_var_types(conf.verb | verbose_debug_enabled, "start do_synthesis");
-    if (do_synth_bve && !cnf.synth_done()) {
+    if (!candidate_defs_file.empty()) {
+        cnf.set_preserve_existing_defs(true);
+        cnf.import_candidate_functions(candidate_defs_file, conf.verb);
+        cnf.simplify_aigs(conf.verb);
+        cnf.get_var_types(conf.verb | verbose_debug_enabled, "after importing candidate functions");
+    }
+    const bool has_candidate_funs = !candidate_defs_file.empty();
+    const bool candidate_all_specified = (has_candidate_funs && cnf.synth_done());
+    if (candidate_all_specified) {
+        cout << "c o [synth] all non-input functions provided by candidate file;"
+             << " skipping synth preprocessing and starting from counterexample checks" << endl;
+    }
+    if (has_candidate_funs && do_synth_bve) {
+        cout << "c o [synth] candidate functions supplied; skipping --synthbve preprocessing" << endl;
+    }
+
+    if (!has_candidate_funs && !candidate_all_specified && do_synth_bve && !cnf.synth_done()) {
         /* simp_conf.bve_too_large_resolvent = -1; */
         cnf = arjun->standalone_get_simplified_cnf(cnf, simp_conf);
         if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-simplified_cnf.aig");
     }
 
-    if (etof_conf.do_autarky && !cnf.synth_done()) {
+    if (!candidate_all_specified && etof_conf.do_autarky && !cnf.synth_done()) {
         arjun->standalone_autarky(cnf);
         if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-autarky.aig");
     }
 
-    if (etof_conf.do_extend_indep && !cnf.synth_done()) {
+    if (!candidate_all_specified && etof_conf.do_extend_indep && !cnf.synth_done()) {
         arjun->standalone_unsat_define(cnf);
         if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-extend_synth.aig");
         cnf.simplify_aigs(conf.verb);
     }
 
-     if (do_minim_indep && !cnf.synth_done()) {
+     if (!candidate_all_specified && do_minim_indep && !cnf.synth_done()) {
         arjun->standalone_backward_round_synth(cnf, mconf);
         if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-minim_idep_synt.aig");
         cnf.simplify_aigs(conf.verb);
     }
 
-    if (do_unate && !cnf.synth_done()) {
+    if (!candidate_all_specified && do_unate && !cnf.synth_done()) {
         arjun->standalone_unate(cnf);
         if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-unsat_unate.aig");
     }
 
-    if (do_unate_def && !cnf.synth_done()) {
+    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;
+    int effective_strategy = manthan_strategy;
+    if (has_candidate_funs && effective_strategy == 4) {
+        cout << "c o [synth] candidate functions supplied; ignoring --mstrategy 4 (BVE-only), using strategy 2" << endl;
+        effective_strategy = 2;
+    }
     uint32_t tries;
     if (manthan_strategy > 4) {
         cout << "ERROR: unknown strategy " << manthan_strategy << endl;
         exit(EXIT_FAILURE);
     }
-    if (!cnf.synth_done() && (manthan_strategy == 0 || manthan_strategy == 1)) {
+    const bool all_defined_before_manthan = cnf.synth_done();
+    if (all_defined_before_manthan) {
+        mconf = mconf_orig;
+        if (!candidate_all_specified) {
+            cout << "c o [synth] all non-input functions are already defined;"
+                 << " running final counterexample check before returning" << endl;
+        }
+        mconf.start_from_candidate_cex = 1;
+        mconf.manthan_bve = 0;
+        if (mconf.manthan_order == 2) mconf.manthan_order = 0;
+        tries = std::numeric_limits<uint32_t>::max();
+        cnf = arjun->standalone_manthan(cnf, mconf, tries);
+    } else if (!cnf.synth_done() && (effective_strategy == 0 || effective_strategy == 1)) {
         mconf = mconf_orig;
         // Learning with no samples
         mconf.manthan_bve = 0;
+        if (has_candidate_funs && mconf.manthan_order == 2) mconf.manthan_order = 0;
         mconf.num_samples = 1;
         mconf.num_samples_ccnr = 0;
         mconf.manthan_bve = 0;
         tries = 20*manthan_rep_mult;
-        if (manthan_strategy == 1) tries = std::numeric_limits<uint32_t>::max();
+        if (effective_strategy == 1) tries = std::numeric_limits<uint32_t>::max();
         cnf = arjun->standalone_manthan(cnf, mconf, tries);
         if (cnf.synth_done()) verb_print(1, "Manthan finished with strategy 1");
     }
-    if (!cnf.synth_done() && (manthan_strategy == 0 || manthan_strategy == 2)) {
+    if (!candidate_all_specified && !cnf.synth_done() && (effective_strategy == 0 || effective_strategy == 2)) {
         // Learning with (larger) samples size
         mconf = mconf_orig;
         mconf.manthan_bve = 0;
+        if (has_candidate_funs && mconf.manthan_order == 2) mconf.manthan_order = 0;
         tries = 100*manthan_rep_mult;
-        if (manthan_strategy == 2) tries = std::numeric_limits<uint32_t>::max();
+        if (effective_strategy == 2) tries = std::numeric_limits<uint32_t>::max();
         cnf = arjun->standalone_manthan(cnf, mconf, tries);
         if (cnf.synth_done()) verb_print(1, "Manthan finished with strategy 2");
     }
-    if (!cnf.synth_done() && (manthan_strategy == 0 || manthan_strategy == 3)) {
+    if (!cnf.synth_done() && (effective_strategy == 0 || effective_strategy == 3)) {
+        // Learning, no BW, only input var learning, no silent update
+        mconf = mconf_orig;
+        mconf.manthan_bve = 0;
+        mconf.force_bw_equal = 1;
+        mconf.silent_var_update = 0;
+        mconf.do_use_all_variables_as_features = 0;
+        tries = 100*manthan_rep_mult;
+        if (effective_strategy == 3) tries = std::numeric_limits<uint32_t>::max();
+        cnf = arjun->standalone_manthan(cnf, mconf, tries);
+        if (cnf.synth_done()) verb_print(1, "Manthan finished with strategy 3");
+    }
+    if (!has_candidate_funs && !cnf.synth_done() && (effective_strategy == 0 || effective_strategy == 4)) {
         // BVE strategy
         mconf = mconf_orig;
         mconf.manthan_bve = 1;
         tries = std::numeric_limits<uint32_t>::max();
         cnf = arjun->standalone_manthan(cnf, mconf, tries);
-        if (cnf.synth_done()) verb_print(1, "Manthan finished with strategy 3");
+        if (cnf.synth_done()) verb_print(1, "Manthan finished with strategy 4");
     }
     release_assert(cnf.synth_done() && "Synthesis should be done by now, but it is not!");
     if (!conf.debug_synth.empty()) cnf.write_aig_defs_to_file(conf.debug_synth + "-5-manthan.aig");