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,
-        const map<uint32_t, uint32_t>* back_map) {
+        const map<uint32_t, uint32_t>* 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;
@@ -502,7 +508,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;
@@ -591,6 +606,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());
@@ -1204,7 +1205,8 @@ 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, const std::map<uint32_t, uint32_t>* back_map = nullptr);
+    void map_aigs_to_orig(const std::vector<aig_ptr>& aigs, const uint32_t max_num_vars,
+        const std::map<uint32_t, uint32_t>* back_map = nullptr, bool overwrite_existing = false);
 
     SimplifiedCNF get_cnf(
             std::unique_ptr<CMSat::SATSolver>& solver,
@@ -1246,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 {
@@ -1274,8 +1275,11 @@ 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; }
 
 private:
+    bool preserve_existing_defs = false;
     bool after_backward_round_synth = false;
     bool need_aig = false;
     std::vector<std::vector<CMSat::Lit>> clauses;
@@ -1374,6 +1378,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/interpolant.cpp

@@ -48,7 +48,19 @@ void MyTracer::add_derived_clause(uint64_t id, bool /*red*/, const std::vector<i
 
   const uint64_t id1 = rantec[0];
   auto aig = fs_clid[id1];
+  release_assert(aig != nullptr);
   set<Lit> resolvent(cls[id1].begin(),cls[id1].end());
+  std::vector<aig_ptr> same_op_terms;
+  bool same_op_is_and = false;
+  bool same_op_started = false;
+
+  auto flush_terms = [&]() {
+      if (!same_op_started) return;
+      aig = combine_balanced(std::move(same_op_terms), same_op_is_and);
+      same_op_terms.clear();
+      same_op_started = false;
+  };
+
   for(uint32_t i = 1; i < rantec.size(); i++) {
       if (conf.verb >= 4) {
           cout << "resolvent: "; for(const auto& l: resolvent) cout << l << " "; cout << endl;
@@ -70,9 +82,24 @@ void MyTracer::add_derived_clause(uint64_t id, bool /*red*/, const std::vector<i
       }
       assert(res_lit != lit_Undef);
       bool input_or_copy = input.count(res_lit.var()) || res_lit.var() >= (uint32_t)orig_num_vars;
-      if (input_or_copy) aig = AIG::new_and(aig, fs_clid[id2]);
-      else aig = AIG::new_or(aig, fs_clid[id2]);
+      auto rhs = fs_clid[id2];
+      release_assert(rhs != nullptr);
+      if (!same_op_started) {
+          same_op_started = true;
+          same_op_is_and = input_or_copy;
+          same_op_terms.push_back(aig);
+          same_op_terms.push_back(rhs);
+      } else if (same_op_is_and == input_or_copy) {
+          same_op_terms.push_back(rhs);
+      } else {
+          flush_terms();
+          same_op_started = true;
+          same_op_is_and = input_or_copy;
+          same_op_terms.push_back(aig);
+          same_op_terms.push_back(rhs);
+      }
   }
+  flush_terms();
   fs_clid[id] = aig;
   verb_print(5, "intermediate formula: " << fs_clid[id]);
   if (clause.empty()) {
@@ -179,8 +206,8 @@ void Interpolant::generate_interpolant(
     }
 
     // CaDiCaL on the core only
-    auto cdcl = std::make_unique<Solver>();
     MyTracer t(orig_num_vars, input_vars, conf, lit_to_aig, cnf.get_aig_mng());
+    auto cdcl = std::make_unique<Solver>();
 
     cdcl->connect_proof_tracer(&t, true);
     /* std::stringstream name; */
@@ -204,6 +231,7 @@ void Interpolant::generate_interpolant(
     }
     release_assert(pret == Status::UNSATISFIABLE);
     cdcl->disconnect_proof_tracer(&t);
+    cdcl.reset();
 
     defs[test_var] = t.out;
     verb_print(5, "definition of var: " << test_var+1 << " is: " << t.out);

src/interpolant.h

@@ -34,6 +34,7 @@ extern "C" {
 #include "formula.h"
 #include <vector>
 #include <map>
+#include <utility>
 #include <cstdint>
 #include <cadical.hpp>
 #include <tracer.hpp>
@@ -63,6 +64,21 @@ struct MyTracer : public CaDiCaL::Tracer {
     // AIG cache
     map<Lit, aig_ptr>& lit_to_aig;
 
+    static aig_ptr combine_balanced(std::vector<aig_ptr> terms, bool use_and) {
+      release_assert(!terms.empty());
+      while (terms.size() > 1) {
+          std::vector<aig_ptr> next;
+          next.reserve((terms.size()+1)/2);
+          for(uint32_t i = 0; i < terms.size(); i += 2) {
+              if (i+1 >= terms.size()) next.push_back(terms[i]);
+              else if (use_and) next.push_back(AIG::new_and(terms[i], terms[i+1]));
+              else next.push_back(AIG::new_or(terms[i], terms[i+1]));
+          }
+          terms = std::move(next);
+      }
+      return terms[0];
+    }
+
     aig_ptr get_aig(const Lit l) {
       if (lit_to_aig.count(l)) return lit_to_aig.at(l);
       aig_ptr aig = AIG::new_lit(l);
@@ -73,13 +89,12 @@ struct MyTracer : public CaDiCaL::Tracer {
     aig_ptr get_aig(const vector<Lit>& unsorted_cl) {
       vector<Lit> cl = unsorted_cl;
       std::sort(cl.begin(), cl.end());
-      aig_ptr aig = nullptr;
-      for(const auto& l: cl) {
-          if (aig == nullptr) aig = get_aig(l);
-          else aig = AIG::new_or(aig, get_aig(l));
-      }
-      if (aig == nullptr) aig = aig_mng.new_const(false);
-      return aig;
+      if (cl.empty()) return aig_mng.new_const(false);
+
+      std::vector<aig_ptr> leaves;
+      leaves.reserve(cl.size());
+      for(const auto& l: cl) leaves.push_back(get_aig(l));
+      return combine_balanced(std::move(leaves), false);
     };
 
     void add_derived_clause (uint64_t id, bool red, const std::vector<int> & clause,
@@ -124,4 +139,3 @@ class Interpolant {
     vector<uint32_t> var_to_indic; //maps an ORIG VAR to an INDICATOR VAR
     vector<aig_ptr> defs; //definition of variables in terms of AIG. ORIGINAL number space
 };
-