Allow inversion of the learnt function

Author: msoos

src/arjun.h

@@ -1386,6 +1386,7 @@ class Arjun
         int force_bw_equal = 1;
         int bva_xor_vars = 0;
         int silent_var_update = 1;
+        int inv_learnt = 0;
         uint32_t max_repairs = std::numeric_limits<uint32_t>::max();
     };
 

src/main.cpp

@@ -166,6 +166,7 @@ void add_arjun_options() {
     myopt("--mbve", mconf.manthan_bve, fc_int,"Use BVE with constants instead of training");
     myopt("--monflyorder", mconf.manthan_on_the_fly_order, fc_int,"Use on-the-fly training order and post-training topological order");
     myopt("--moneperloop", mconf.one_repair_per_loop, fc_int,"One repair per CEX loop");
+    myopt("--minvertlearn", mconf.inv_learnt, fc_int,"Invert learnt functions");
 
     // repairing on vars
     myopt("--bwequal", mconf.force_bw_equal, fc_int,"Force BW vars' indicators to be TRUE -- prevents repairing with them, but faster to repair");

src/manthan.cpp

@@ -2066,7 +2066,7 @@ double Manthan::train(const vector<sample>& orig_samples, const uint32_t v) {
             << setw(6) << (samples.size() - num_ones) << " zeros");
     double train_error;
     if (samples.empty()) {
-        var_to_formula[v] = fh->constant_formula(true);
+        var_to_formula[v] = fh->constant_formula(!mconf.inv_learnt);
         train_error = 0.0;
     } else {
         // Create the RandomForest object and train it on the training data.
@@ -2115,6 +2115,8 @@ double Manthan::train(const vector<sample>& orig_samples, const uint32_t v) {
         assert(var_to_formula.count(v) == 0);
         uint32_t max_depth = 0;
         var_to_formula[v] = recur(&r, v, used_vars, 0, max_depth);
+        if (mconf.inv_learnt)
+            var_to_formula[v] = fh->neg(var_to_formula[v]);
         verb_print(1, "Training error: " << setprecision(2) << setw(6) << train_error << "%."
                 << " depth: " << setw(6) << max_depth
                 << " ones: " << setprecision(0) << fixed << setw(5) << (double)num_ones/samples.size()*100.0 << "%"

src/synth.cpp

@@ -76,6 +76,7 @@ const std::map<string, ParamDef> param_table = {
     {"force_bw_equal",           {PT::Int,    [](MC& c, const string& v) { c.force_bw_equal           = parse_val<int>(v); }}},
     {"bva_xor_vars",             {PT::Int,    [](MC& c, const string& v) { c.bva_xor_vars             = parse_val<int>(v); }}},
     {"silent_var_update",        {PT::Int,    [](MC& c, const string& v) { c.silent_var_update        = parse_val<int>(v); }}},
+    {"inv_learnt",               {PT::Int,    [](MC& c, const string& v) { c.inv_learnt               = parse_val<int>(v); }}},
 };
 } // namespace