Build

Author: msoos

html/index.html

@@ -174,7 +174,7 @@ <h1>Arjun Functional Synthesis in Your Browser</h1>
                         try {
                             console.log('Running with args:', e.data.args);
                             Module.FS.writeFile('/input.cnf', e.data.input);
-                            var args = ['--verb', '3', '--synth'].concat(e.data.extraArgs || []).concat(['/input.cnf']);
+                            var args = ['--verb', '1', '--synth'].concat(e.data.extraArgs || []).concat(['/input.cnf']);
                             Module.callMain(args);
                             postMessage({ type: 'done' });
                         } catch (e) {

scripts/build_emscripten.sh

@@ -2,7 +2,7 @@
 set -e
 
 rm -rf lib* Test* tests* include tests CM* cmake* arjun Makefile rjun-src
-emcmake cmake -DCMAKE_INSTALL_PREFIX=$EMINSTALL -DEXTRA_SYNTH=OFF ..
+emcmake cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=$EMINSTALL -DEXTRA_SYNTH=OFF ..
 emmake make -j26
 emmake make install
 cp arjun.wasm ../html

src/manthan.cpp

@@ -1772,7 +1772,7 @@ void Manthan::inject_formulas_into_solver() {
             vector<Lit> cl2;
             for(const auto& l: cl.lits) {
                 auto v = l.var();
-                if (to_define_full.count(v)) { cl2.push_back(Lit(y_to_y_hat[v], l.sign()));}
+                if (to_define_full.count(v)) { cl2.push_back(Lit(y_to_y_hat.at(v), l.sign()));}
                 else cl2.push_back(l);
             }
             cex_solver.add_clause(cl2);
@@ -1790,7 +1790,7 @@ void Manthan::inject_formulas_into_solver() {
         assert(var_to_formula.count(y));
         for(const auto& cl: var_to_formula[y].clauses) assert(cl.inserted && "All clauses must have been inserted");
         const auto& form_out = var_to_formula[y].out;
-        const auto& y_hat = y_to_y_hat[y];
+        const auto& y_hat = y_to_y_hat.at(y);
 
         y_hat_to_indic[y_hat] = ind;
         indic_to_y_hat[ind] = y_hat;
@@ -1858,6 +1858,13 @@ bool Manthan::get_counterexample(sample& ctx) {
     if (ret == l_True) {
         verb_print(2, COLYEL "[manthan] *** Counterexample found ***");
         ctx = cex_solver.get_model();
+        cout << "ctx: ";
+        for(auto v : ctx) {
+            if (v == l_Undef) cout << "U ";
+            else if (v == l_True) cout << "T ";
+            else cout << "F ";
+        }
+        cout << endl;
         compute_needs_repair(ctx);
         assert(!needs_repair.empty() && "If we found a counterexample, there must be something to repair!");
         return false;

src/synth.cpp

@@ -259,9 +259,7 @@ void SynthRunner::run_manthan_strategies(
             << (mconf.max_repairs ? std::string("unlimited") : std::to_string(mconf.max_repairs)));
         cnf = arjun->standalone_manthan(cnf, mconf);
         if (cnf.synth_done()) {
-            verb_print(1,"Manthan finished with "
-                    << (mconf.max_repairs == std::numeric_limits<uint32_t>::max() ? "unlimited" : std::to_string(mconf.max_repairs))
-                    << " repairs for strategy " << i << "/" << strategies.size()-1
+            verb_print(1,"Manthan finished with strategy " << i << "/" << strategies.size()-1
                     << " -- " << strat.raw);
             break;
         }