Should be fixed

Author: msoos

html/index.html

@@ -92,6 +92,13 @@ <h1>Arjun Functional Synthesis in Your Browser</h1>
             description is available <a
                 href="https://jix.github.io/varisat/manual/0.2.0/formats/dimacs.html">here</a></div>
             You need to have "c p show ... 0" for all the variables that are inputs
+        <div>
+            <label for="extra-args">Extra command line arguments:</label>
+            <input type="text" id="extra-args"
+                value='--mstrategy "const(max_repairs=400),const(max_repairs=400,inv_learnt=1),bve"'
+                style="width:100%;padding:8px;box-sizing:border-box;font-family:monospace;border:1px solid #ddd;border-radius:4px;">
+        </div>
+
         <div>
             <label for="input-content">CNF:</label>
             <textarea id="input-content">p cnf 3 3
@@ -167,7 +174,8 @@ <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);
-                            Module.callMain(['--verb', '1', '--synth', '/input.cnf']);
+                            var args = ['--verb', '3', '--synth'].concat(e.data.extraArgs || []).concat(['/input.cnf']);
+                            Module.callMain(args);
                             postMessage({ type: 'done' });
                         } catch (e) {
                             postMessage({ type: 'error', content: e.toString() });
@@ -181,9 +189,32 @@ <h1>Arjun Functional Synthesis in Your Browser</h1>
         }
 
         // Main execution logic
+        function parseExtraArgs(str) {
+            // Shell-like tokenizer: handles "quoted strings" and unquoted tokens
+            const args = [];
+            let i = 0;
+            while (i < str.length) {
+                while (i < str.length && str[i] === ' ') i++;
+                if (i >= str.length) break;
+                if (str[i] === '"') {
+                    i++;
+                    let start = i;
+                    while (i < str.length && str[i] !== '"') i++;
+                    args.push(str.slice(start, i));
+                    if (i < str.length) i++; // skip closing quote
+                } else {
+                    let start = i;
+                    while (i < str.length && str[i] !== ' ') i++;
+                    args.push(str.slice(start, i));
+                }
+            }
+            return args;
+        }
+
         document.getElementById('run-button').addEventListener('click', async function() {
             const inputContent = document.getElementById('input-content').value;
             const outputDiv = document.getElementById('output');
+            const extraArgs = parseExtraArgs(document.getElementById('extra-args').value);
 
             if (!inputContent.trim()) {
                 outputDiv.textContent = 'Error: Please enter input content';
@@ -211,7 +242,8 @@ <h1>Arjun Functional Synthesis in Your Browser</h1>
                         //console.log('ready. Sending input:', inputContent);
                         worker.postMessage({
                             type: 'run',
-                            input: inputContent
+                            input: inputContent,
+                            extraArgs: extraArgs
                         });
                         break;
                     case 'done':

scripts/build_no_extra_synth.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+
+set -e
+
+rm -rf lib* Test* tests* include tests CM* cmake* arjun Makefile rjun-src
+cmake -DEXTRA_SYNTH=OFF -DENABLE_TESTING=OFF ..
+make -j26

src/main.cpp

@@ -162,7 +162,6 @@ void add_arjun_options() {
     myopt("--unate", do_unate, fc_int,"Perform unate analysis");
     myopt("--unatedef", do_unate_def, fc_int,"Perform definition-aware unate analysis");
     myopt("--autarky", etof_conf.do_autarky, fc_int,"Perform unate analysis");
-    myopt("--mbve", mconf.manthan_base, 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");

src/manthan.cpp

@@ -48,6 +48,7 @@
 #ifdef EXTRA_SYNTH
 #include <mlpack/methods/decision_tree/decision_tree.hpp>
 #include "EvalMaxSAT.h"
+#include "manthan_learn.h"
 #endif
 
 using std::min;
@@ -823,7 +824,8 @@ SimplifiedCNF Manthan::do_manthan() {
 
     if (mconf.manthan_base == 0) {
 #ifdef EXTRA_SYNTH
-        full_train();
+        ManthanLearn learn(*this, conf, mconf);
+        learn.full_train();
 #else
         cout << "ERROR: manthan_base is set to 2 but we are not in EXTRA_SYNTH mode!" << endl;
         exit(EXIT_FAILURE);
@@ -1865,6 +1867,7 @@ bool Manthan::get_counterexample(sample& ctx) {
         verb_print(2, COLYEL "[manthan] *** Counterexample found ***");
         ctx = cex_solver.get_model();
         compute_needs_repair(ctx);
+        assert(!needs_repair.empty() && "If we found a counterexample, there must be something to repair!");
         return false;
     } else {
         assert(ret == l_False);

src/manthan.h

@@ -22,6 +22,8 @@
  THE SOFTWARE.
  */
 
+#pragma once
+
 #include "arjun.h"
 #include "config.h"
 #include "metasolver.h"

src/manthan_learn.h

@@ -41,7 +41,7 @@ using sample = vector<lbool>;
 
 class ManthanLearn {
 public:
-    ManthanLearn(Manthan& _manthan, const Config& _conf, const Arjun::ManthanConf& _mconf) :
+    ManthanLearn(Manthan& _manthan, const Config& _conf, const ArjunNS::Arjun::ManthanConf& _mconf) :
         m(_manthan), conf(_conf), mconf(_mconf) {
             point_0.zeros(m.cnf.nVars());
             point_1.zeros(m.cnf.nVars());
@@ -56,5 +56,5 @@ class ManthanLearn {
 
     Manthan& m;
     const Config& conf;
-    const Arjun::ManthanConf& mconf;
+    const ArjunNS::Arjun::ManthanConf& mconf;
 };