meelgroup · msoos · Feb 26, 2026 · Feb 26, 2026 · Feb 26, 2026 · Feb 27, 2026
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -92,7 +92,7 @@ SET(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
 set(CMAKE_EXPORT_COMPILE_COMMANDS 1)
 
 # static compilation
-option(SYNTH "Also build synthesis" ON)
+option(EXTRA_SYNTH "Also build synthesis" ON)
 option(BUILD_SHARED_LIBS "Build the shared library" ON)
 option(STATICCOMPILE "Compile to static executable" OFF)
 if (STATICCOMPILE)
@@ -117,8 +117,8 @@ find_package (sbva REQUIRED)
 find_package(treedecomp CONFIG REQUIRED)
 message(STATUS "Found SBVA includes at: ${SBVA_INCLUDE_DIRS}")
 find_package(GMP REQUIRED)
-if (SYNTH)
-    add_definitions(-DSYNTH)
+if (EXTRA_SYNTH)
+    add_definitions(-DEXTRA_SYNTH)
     find_package(MLPACK REQUIRED)
     find_library(cadical
         PATHS ${CMAKE_CURRENT_SOURCE_DIR}/../cadical/build/

diff --git a/html/index.html b/html/index.html
@@ -0,0 +1,281 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta http-equiv="X-UA-Compatible" content="IE=edge">
+    <meta name="description" content="Arjun in your browser">
+    <meta name="keywords" content="Arjun, Functional Synthesis, WebAssembly, JavaScript, Emscripten">
+    <meta name="author" content="Mate Soos">
+    <meta charset="UTF-8">
+    <meta name="viewport" content="width=device-width, initial-scale=1.0">
+    <title>Arjun in your browser</title>
+    <style>
+        body {
+            font-family: Arial, sans-serif;
+            max-width: 800px;
+            margin: 0 auto;
+            padding: 20px;
+            line-height: 1.6;
+        }
+        .container {
+            display: flex;
+            flex-direction: column;
+            gap: 20px;
+        }
+        textarea {
+            width: 100%;
+            height: 200px;
+            padding: 10px;
+            box-sizing: border-box;
+            font-family: monospace;
+            border: 1px solid #ddd;
+            border-radius: 4px;
+        }
+        button {
+            padding: 10px 15px;
+            background-color: #4CAF50;
+            color: white;
+            border: none;
+            border-radius: 4px;
+            cursor: pointer;
+            font-size: 16px;
+            transition: background-color 0.3s;
+        }
+        button:hover {
+            background-color: #45a049;
+        }
+        button:disabled {
+            background-color: #cccccc;
+            cursor: not-allowed;
+        }
+        #output {
+            border: 1px solid #ddd;
+            padding: 15px;
+            min-height: 100px;
+            white-space: pre-wrap;
+            background-color: #f9f9f9;
+            border-radius: 4px;
+            font-family: monospace;
+            overflow-y: auto;
+            max-height: 400px;
+        }
+        .status {
+            font-style: italic;
+            color: #666;
+            margin-left: 10px;
+        }
+        label {
+            font-weight: bold;
+            display: block;
+            margin-bottom: 5px;
+        }
+        .progress-container {
+            width: 100%;
+            background-color: #f1f1f1;
+            border-radius: 4px;
+            margin-top: 10px;
+        }
+        #progress-bar {
+            height: 10px;
+            background-color: #4CAF50;
+            border-radius: 4px;
+            width: 0%;
+            transition: width 0.3s;
+        }
+    </style>
+</head>
+<body>
+    <div class="container">
+        <h1>Arjun Functional Synthesis in Your Browser</h1>
+        <div>Copy your CNF formula in the input box below and click "Run
+            arjun.js" to run the Functional Synthesis engine in your browser.
+            The output will be displayed below the input box. Format
+            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
+-1 -2 3 0
+1 -3 0
+2 -3 0
+c p show 1 2 0
+</textarea>
+        </div>
+
+        <div>
+            <button id="run-button">Run arjun.js</button>
+            <button id="cancel-button">Cancel</button>
+            <span id="status" class="status">Loading WebAssembly module...</span>
+            <div class="progress-container">
+                <div id="progress-bar"></div>
+            </div>
+        </div>
+
+        <div>
+            <label for="output">Output:</label>
+            <div id="output">Ready - enter your input and click "Run arjun.js"</div>
+        </div>
+    </div>
+
+    <script>
+        // Main thread Module configuration
+        var Module = {
+            noInitialRun: true,
+            stdin: function() { return null; },
+            onRuntimeInitialized: function() {
+                document.getElementById('status').textContent = 'Ready';
+                document.getElementById('run-button').disabled = false;
+            }
+        };
+
+        // Create worker with proper WASM loading
+        function createEmscriptenWorker() {
+            const workerCode = `
+                var Module = {
+                    noInitialRun: true,
+                    stdin: function() { return null; },
+                    print: function(text) {
+                        postMessage({ type: 'output', content: text });
+                    },
+                    printErr: function(text) {
+                        console.error('Error:', text);
+                        //postMessage({ type: 'output', content: 'ERROR: ' + text });
+                    },
+                    onRuntimeInitialized: function() {
+                        postMessage({ type: 'ready' });
+                    },
+                    locateFile: function(path) {
+                        console.log('Locating file:', path);
+                        // Resolve correct path for WASM file
+                        if (path.endsWith('.wasm')) {
+                            return self.workerOptions.wasmPath || 'arjun.wasm';
+                        }
+                        return path;
+                    }
+                };
+
+                // This will be replaced by the Emscripten-generated code
+                var wasmBinary;
+
+                onmessage = function(e) {
+                    if (e.data.type === 'init') {
+                        console.log('Initializing worker with options:', e.data.options);
+                        self.workerOptions = e.data.options;
+                        importScripts(e.data.options.jsPath);
+                    }
+                    else if (e.data.type === 'run') {
+                        try {
+                            console.log('Running with args:', e.data.args);
+                            Module.FS.writeFile('/input.cnf', e.data.input);
+                            var args = ['--verb', '1', '--synth'].concat(e.data.extraArgs || []).concat(['/input.cnf']);
+                            Module.callMain(args);
+                            postMessage({ type: 'done' });
+                        } catch (e) {
+                            postMessage({ type: 'error', content: e.toString() });
+                        }
+                    }
+                };
+            `;
+
+            const blob = new Blob([workerCode], { type: 'application/javascript' });
+            return URL.createObjectURL(blob);
+        }
+
+        // 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';
+                return;
+            }
+
+            outputDiv.textContent = 'Initializing...\n';
+            document.getElementById('run-button').disabled = true;
+            document.getElementById('status').textContent = 'Running...';
+
+            // Get absolute URL for WASM file
+            const wasmPath = new URL('arjun.wasm', window.location.href).href;
+            const jsPath = new URL('arjun.js', window.location.href).href;
+            const workerUrl = createEmscriptenWorker();
+            const worker = new Worker(workerUrl);
+
+            worker.onmessage = function(e) {
+                switch (e.data.type) {
+                    case 'output':
+                        console.log('Output:', e.data.content);
+                        outputDiv.textContent += e.data.content + '\n';
+                        outputDiv.scrollTop = outputDiv.scrollHeight;
+                        break;
+                    case 'ready':
+                        //console.log('ready. Sending input:', inputContent);
+                        worker.postMessage({
+                            type: 'run',
+                            input: inputContent,
+                            extraArgs: extraArgs
+                        });
+                        break;
+                    case 'done':
+                        document.getElementById('status').textContent = 'Completed';
+                        document.getElementById('run-button').disabled = false;
+                        worker.terminate();
+                        URL.revokeObjectURL(workerUrl);
+                        break;
+                    case 'error':
+                        outputDiv.textContent += 'Error: ' + e.data.content + '\n';
+                        document.getElementById('status').textContent = 'Failed';
+                        document.getElementById('run-button').disabled = false;
+                        worker.terminate();
+                        URL.revokeObjectURL(workerUrl);
+                        break;
+                }
+            };
+
+            // Initialize worker with proper paths
+            worker.postMessage({
+                type: 'init',
+                options: {
+                    jsPath: jsPath,
+                    wasmPath: wasmPath
+                }
+            });
+        });
+
+        // Load arjun.js in main thread
+        const script = document.createElement('script');
+        script.src = 'arjun.js';
+        document.body.appendChild(script);
+    </script>
+</body>
+</html>
diff --git a/scripts/build_emscripten.sh b/scripts/build_emscripten.sh
@@ -2,6 +2,8 @@
 set -e
 
 rm -rf lib* Test* tests* include tests CM* cmake* arjun Makefile rjun-src
-emcmake cmake -DCMAKE_INSTALL_PREFIX=$EMINSTALL -DSYNTH=OFF ..
+emcmake cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=$EMINSTALL -DEXTRA_SYNTH=OFF ..
 emmake make -j26
 emmake make install
+cp arjun.wasm ../html
+cp $EMINSTALL/bin/arjun.js ../html
diff --git a/scripts/build_no_extra_synth.sh b/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
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
@@ -23,7 +23,7 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR})
 include_directories(${CRYPTOMINISAT5_INCLUDE_DIRS})
 include_directories(${SBVA_INCLUDE_DIRS})
 include_directories( ${GMP_INCLUDE_DIR} )
-if (SYNTH)
+if (EXTRA_SYNTH)
     include_directories(${EVALMAXSAT_INCLUDE_DIRS})
     include_directories( ${MLPACK_INCLUDE_DIR} )
 endif()
@@ -58,12 +58,12 @@ set(libfiles
     autarky.cpp
     ccnr/ccnr.cpp
     ${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp
+    manthan.cpp
+    interpolant.cpp
 )
 
-if (SYNTH)
-    set(libfiles ${libfiles}
-    manthan.cpp
-    interpolant.cpp)
+if (EXTRA_SYNTH)
+    list(APPEND libfiles manthan_learn.cpp)
 endif()
 
 add_library(arjun ${libfiles})
@@ -78,7 +78,7 @@ target_link_libraries(arjun
     LINK_PUBLIC ${TREEDECOMP_LIBRARIES}
 )
 
-add_executable(arjun-bin main.cpp)
+add_executable(arjun-bin main.cpp synth.cpp)
 add_executable(arjun-example example.cpp)
 add_executable(test-synth test-synth.cpp)
 
@@ -91,10 +91,20 @@ set_target_properties(arjun PROPERTIES
     VERSION ${PROJECT_VERSION_MAJOR}.${PROJECT_VERSION_MINOR}
     SOVERSION ${PROJECT_VERSION_MAJOR}.${PROJECT_VERSION_MINOR}
 )
-set_target_properties(arjun-bin PROPERTIES
-    OUTPUT_NAME arjun
-    RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
-    INSTALL_RPATH_USE_LINK_PATH TRUE)
+
+if(CMAKE_SYSTEM_NAME STREQUAL "Emscripten")
+    set_target_properties(arjun-bin PROPERTIES
+      OUTPUT_NAME arjun
+      RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
+      INSTALL_RPATH_USE_LINK_PATH TRUE
+      LINK_FLAGS "-s WASM=1 -s ALLOW_MEMORY_GROWTH=1 -s EXPORTED_RUNTIME_METHODS='[\"callMain\", \"ccall\", \"cwrap\", \"FS\", \"print\"]' -s FORCE_FILESYSTEM=1"
+    )
+else()
+    set_target_properties(arjun-bin PROPERTIES
+        OUTPUT_NAME arjun
+        RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
+        INSTALL_RPATH_USE_LINK_PATH TRUE)
+    endif()
 target_link_libraries(arjun-bin ${arjun_bin_exec_link_libs} arjun)
 
 set_target_properties(arjun-example PROPERTIES