diff --git a/src/arjun.cpp b/src/arjun.cpp index 8156d77..e98eda4 100644 --- a/src/arjun.cpp +++ b/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& 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& aigs_orig, const uint32_t max_num_vars, - std::optional>> back_map) { + std::optional>> 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 visited; @@ -504,7 +510,16 @@ DLL_PUBLIC void SimplifiedCNF::map_aigs_to_orig(const vector& 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; diff --git a/src/arjun.h b/src/arjun.h index 2567ca5..ed3c320 100644 --- a/src/arjun.h +++ b/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 extend_sample(const std::vector& sample, const bool relaxed = false) const; void map_aigs_to_orig(const std::vector& aigs, const uint32_t max_num_vars, - std::optional>> back_map = std::nullopt); + std::optional>> back_map = std::nullopt, bool overwrite_existing = false); SimplifiedCNF get_cnf( std::unique_ptr& 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> 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 = ""; diff --git a/src/backward.cpp b/src/backward.cpp index 817a71b..b629f7e 100644 --- a/src/backward.cpp +++ b/src/backward.cpp @@ -415,12 +415,23 @@ void Minimize::backward_round_synth(SimplifiedCNF& cnf, const Arjun::ManthanConf vector unknown_set(orig_num_vars, 0); vector 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> dep_cache; + map> backward_depends_on_orig; set 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,6 +499,7 @@ 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); @@ -496,7 +507,16 @@ void Minimize::backward_round_synth(SimplifiedCNF& cnf, const Arjun::ManthanConf //Assumption filling assert(test_var != var_Undef); - fill_assumptions_backward(assumptions, unknown, unknown_set, pretend_input, input); + set 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(); diff --git a/src/main.cpp b/src/main.cpp index 3277087..63562e3 100644 --- a/src/main.cpp +++ b/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; @@ -90,6 +91,7 @@ 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 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::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::max(); + if (effective_strategy == 1) tries = std::numeric_limits::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::max(); + if (effective_strategy == 2) tries = std::numeric_limits::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::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::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"); diff --git a/src/manthan.cpp b/src/manthan.cpp index 46e96e6..0ac3ea5 100644 --- a/src/manthan.cpp +++ b/src/manthan.cpp @@ -264,6 +264,35 @@ void Manthan::fill_dependency_mat_with_backward() { assert(check_map_dependency_cycles()); } +void Manthan::fill_dependency_mat_from_all_defined() { + dependency_mat.clear(); + dependency_mat.resize(cnf.nVars()); + for(auto& m: dependency_mat) m.resize(cnf.nVars(), 0); + + map> cache; + const auto new_to_orig = cnf.get_new_to_orig_var(); + const auto& orig_to_new = cnf.get_orig_to_new_var(); + const auto& orig_inputs = cnf.get_orig_sampl_vars(); + + for (const auto& y_new : to_define_full) { + assert(input.count(y_new) == 0); + const uint32_t y_orig = new_to_orig.at(y_new).var(); + const auto deps_orig = cnf.get_dependent_vars_recursive(y_orig, cache); + for (const auto& d_orig : deps_orig) { + if (orig_inputs.count(d_orig)) continue; + const auto it = orig_to_new.find(d_orig); + if (it == orig_to_new.end()) continue; + const uint32_t d_new = it->second.var(); + if (d_new == y_new) continue; + if (input.count(d_new)) continue; + set_depends_on(y_new, d_new); + } + } + + assert(check_transitive_closure_correctness()); + assert(check_map_dependency_cycles()); +} + bool Manthan::check_transitive_closure_correctness() const { // Then, compute transitive closure to ensure transitivity // If A depends on B and B depends on C, then A depends on C @@ -288,10 +317,11 @@ bool Manthan::check_transitive_closure_correctness() const { return true; } -void Manthan::fill_var_to_formula_with(set& vars) { +void Manthan::fill_var_to_formula_with_backward(const bool include_to_define) { const auto new_to_orig = cnf.get_new_to_orig_var(); - for(const auto& v: vars) { + for(const auto& v: to_define_full) { + if (!include_to_define && to_define.count(v)) continue; FHolder::Formula f; // Get the original variable number @@ -339,7 +369,75 @@ void Manthan::fill_var_to_formula_with(set& vars) { map cache; const Lit out_lit = AIG::transform(aig, aig_to_cnf_visitor, cache); f.out = out_lit ^ orig.sign(); - f.aig = nullptr; // we won't need it. + + if (include_to_define) { + // Candidate mode needs AIGs for final map-back of to_define vars. + map aig_cache; + auto aig_to_cnf_aig_visitor = + [&](AIGT type, const uint32_t var_orig, const bool neg, const aig_ptr* left, const aig_ptr* right) -> aig_ptr { + if (type == AIGT::t_const) { + return neg ? aig_mng.new_const(false) : aig_mng.new_const(true); + } + if (type == AIGT::t_lit) { + const Lit lit_new = cnf.orig_to_new_lit(Lit(var_orig, neg)); + return AIG::new_lit(lit_new); + } + if (type == AIGT::t_and) { + assert(left != nullptr && right != nullptr); + return AIG::new_and(*left, *right, neg); + } + assert(false && "Unhandled AIG type in AIG visitor"); + exit(EXIT_FAILURE); + }; + f.aig = AIG::transform(aig, aig_to_cnf_aig_visitor, aig_cache); + } else { + // Normal mode keeps previous behavior for backward-defined vars. + f.aig = nullptr; + } + assert(var_to_formula.count(v) == 0); + var_to_formula[v] = f; + } + SLOW_DEBUG_DO(assert(check_functions_for_y_vars())); +} + +void Manthan::fill_var_to_formula_with(set& vars) { + const auto new_to_orig = cnf.get_new_to_orig_var(); + for (const auto& v: vars) { + FHolder::Formula f; + + const auto orig = new_to_orig.at(v); + const uint32_t v_orig = orig.var(); + const auto& aig = cnf.get_def(v_orig); + assert(aig != nullptr); + + std::function aig_to_cnf_visitor = + [&](AIGT type, const uint32_t var_orig, const bool neg, const Lit* left, const Lit* right) -> Lit { + if (type == AIGT::t_const) { + return neg ? ~fh->get_true_lit() : fh->get_true_lit(); + } + if (type == AIGT::t_lit) { + const Lit lit_new = cnf.orig_to_new_lit(Lit(var_orig, neg)); + return map_y_to_y_hat(lit_new); + } + if (type == AIGT::t_and) { + const Lit l_lit = *left; + const Lit r_lit = *right; + cex_solver.new_var(); + const Lit and_out = Lit(cex_solver.nVars() - 1, false); + helpers.insert(and_out.var()); + f.clauses.push_back(CL({~and_out, l_lit})); + f.clauses.push_back(CL({~and_out, r_lit})); + f.clauses.push_back(CL({~l_lit, ~r_lit, and_out})); + return neg ? ~and_out : and_out; + } + assert(false && "Unhandled AIG type in visitor"); + exit(EXIT_FAILURE); + }; + + map cache; + const Lit out_lit = AIG::transform(aig, aig_to_cnf_visitor, cache); + f.out = out_lit ^ orig.sign(); + f.aig = nullptr; assert(var_to_formula.count(v) == 0); var_to_formula[v] = f; } @@ -821,22 +919,50 @@ SimplifiedCNF Manthan::do_manthan(const uint32_t max_repairs) { // defined non-input vars -- vars defined via backward_round_synth // to_define vars -- vars that are not defined yet, and not input std::tie(input, to_define, backward_defined) = cnf.get_var_types(conf.verb | verbose_debug_enabled, "start do_manthan"); - if (to_define.empty()) { + const bool candidate_mode = (mconf.start_from_candidate_cex != 0); + if (!candidate_mode && to_define.empty()) { verb_print(1, "[manthan] No variables to define, returning original CNF"); return cnf; } - for(const auto& v: helper_functions) { - if (!input.count(v)) { - cout << "ERROR: helper function var " << v+1 << " is not detected as an input var" << endl; - release_assert(false); + if (!candidate_mode) { + for(const auto& v: helper_functions) { + if (!input.count(v)) { + cout << "ERROR: helper function var " << v+1 << " is not detected as an input var" << endl; + release_assert(false); + } } } - - // Extend to_define_full to to_define + backward_defined to_define_full.clear(); - to_define_full.insert(to_define.begin(), to_define.end()); - to_define_full.insert(backward_defined.begin(), backward_defined.end()); - fill_dependency_mat_with_backward(); + if (candidate_mode) { + input.clear(); + to_define.clear(); + backward_defined.clear(); + + const auto& orig_inputs = cnf.get_orig_sampl_vars(); + for (const auto& [orig_v, new_l] : cnf.get_orig_to_new_var()) { + if (orig_inputs.count(orig_v)) { + input.insert(new_l.var()); + continue; + } + if (!cnf.defined(orig_v)) continue; + to_define.insert(new_l.var()); + } + + to_define_full = to_define; + if (to_define_full.empty()) { + verb_print(1, "[manthan] Candidate mode requested but no candidate-defined vars found"); + return cnf; + } + fill_dependency_mat_from_all_defined(); + } else { + if (to_define.empty()) { + verb_print(1, "[manthan] No variables to define, returning original CNF"); + return cnf; + } + to_define_full.insert(to_define.begin(), to_define.end()); + to_define_full.insert(backward_defined.begin(), backward_defined.end()); + fill_dependency_mat_with_backward(); + } get_incidence(); inject_cnf(repair_solver); @@ -852,13 +978,19 @@ SimplifiedCNF Manthan::do_manthan(const uint32_t max_repairs) { verb_print(2, "[manthan] After fh creation: solver_train.nVars() = " << cex_solver.nVars() << " cnf.nVars() = " << cnf.nVars()); // Order & train - pre_order_vars(); - fill_var_to_formula_with(backward_defined); - fill_var_to_formula_with(helper_functions); - - if (mconf.manthan_bve) bve_and_substitute(); - else full_train(); - post_order_vars(); + if (candidate_mode) { + fill_var_to_formula_with_backward(true); + verb_print(1, "[manthan] Candidate mode: skipping training/BVE substitution, starting with counterexample checks"); + pre_order_vars(); + post_order_vars(); + } else { + pre_order_vars(); + fill_var_to_formula_with_backward(false); + fill_var_to_formula_with(helper_functions); + if (mconf.manthan_bve) bve_and_substitute(); + else full_train(); + post_order_vars(); + } // Counterexample-guided repair repair_start_time = cpuTime(); @@ -936,7 +1068,7 @@ SimplifiedCNF Manthan::do_manthan(const uint32_t max_repairs) { aigs[y] = var_to_formula[y].aig; } SimplifiedCNF fcnf = cnf; - fcnf.map_aigs_to_orig(aigs, cnf.nVars(), y_hat_to_y); + fcnf.map_aigs_to_orig(aigs, cnf.nVars(), y_hat_to_y, candidate_mode); assert(verify_final_cnf(fcnf)); auto [input2, to_define2, backward_defined2] = fcnf.get_var_types(0 | verbose_debug_enabled, "end do_manthan"); verb_print(1, COLRED "[manthan] Done. " @@ -1989,9 +2121,11 @@ vector Manthan::filter_samples(const uint32_t v, const vector& samples) { if (samples.size() <= 1) return; + set unique_key_vars = input; + unique_key_vars.insert(backward_defined.begin(), backward_defined.end()); std::sort(samples.begin(), samples.end(), - [this](const sample& a, const sample& b) { - for(const auto& v: input) { + [&unique_key_vars](const sample& a, const sample& b) { + for(const auto& v: unique_key_vars) { if (a[v] != b[v]) return a[v] == l_False; } return false; // equal @@ -2001,7 +2135,7 @@ void Manthan::sort_all_samples(vector& samples) { vector samples2; samples2.push_back(samples[0]); for(size_t i = 1; i < samples.size(); i++) { - for(const auto& v: input) { + for(const auto& v: unique_key_vars) { if (samples[i][v] != samples2.back()[v]) { samples2.push_back(samples[i]); break; @@ -2009,7 +2143,7 @@ void Manthan::sort_all_samples(vector& samples) { } } verb_print(1, "[sort_all_samples] Reduced samples from " << samples.size() - << " to " << samples2.size() << " by removing duplicates on input vars."); + << " to " << samples2.size() << " by removing duplicates on input+predefined vars."); samples = samples2; } } diff --git a/src/manthan.h b/src/manthan.h index c889193..c3aa1c1 100644 --- a/src/manthan.h +++ b/src/manthan.h @@ -88,8 +88,8 @@ class Manthan { set input; set to_define; set backward_defined; - set to_define_full; // to_define + backward_defined - set helper_functions; // these are in BW, but we definitely want them + set to_define_full; // vars represented by y/y_hat in Manthan + set helper_functions; // helper vars treated as fixed inputs (e.g. BVA XOR vars) // To help us account for every variable in the formulas' clauses set helpers; // used for ITE @@ -125,6 +125,8 @@ class Manthan { void perform_repair(const uint32_t y_rep, const sample& ctx, const vector& conflict); void add_not_f_x_yhat(); void fill_dependency_mat_with_backward(); + void fill_dependency_mat_from_all_defined(); + void fill_var_to_formula_with_backward(bool include_to_define); void fill_var_to_formula_with(set& vars); void print_y_order_occur() const; void compute_needs_repair(const sample& ctx);