Skip to content

Commit 500a36c

Browse files
msoosmsoos
committed
Refactor to allow building for emscripten
Make emscripten build work Should be fixed Making progress This actually compiles now Build Fixing
1 parent dea44a5 commit 500a36c

21 files changed

+715
-289
lines changed

‎CMakeLists.txt‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -92,7 +92,7 @@ SET(CMAKE_MODULE_PATH ${PROJECT_SOURCE_DIR}/cmake)
9292
set(CMAKE_EXPORT_COMPILE_COMMANDS 1)
9393

9494
# static compilation
95-
option(SYNTH "Also build synthesis" ON)
95+
option(EXTRA_SYNTH "Also build synthesis" ON)
9696
option(BUILD_SHARED_LIBS "Build the shared library" ON)
9797
option(STATICCOMPILE "Compile to static executable" OFF)
9898
if (STATICCOMPILE)
@@ -117,8 +117,8 @@ find_package (sbva REQUIRED)
117117
find_package(treedecomp CONFIG REQUIRED)
118118
message(STATUS "Found SBVA includes at: ${SBVA_INCLUDE_DIRS}")
119119
find_package(GMP REQUIRED)
120-
if (SYNTH)
121-
add_definitions(-DSYNTH)
120+
if (EXTRA_SYNTH)
121+
add_definitions(-DEXTRA_SYNTH)
122122
find_package(MLPACK REQUIRED)
123123
find_library(cadical
124124
PATHS ${CMAKE_CURRENT_SOURCE_DIR}/../cadical/build/

‎html/index.html‎

Lines changed: 281 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,281 @@
1+
<!DOCTYPE html>
2+
<html lang="en">
3+
<head>
4+
<meta http-equiv="X-UA-Compatible" content="IE=edge">
5+
<meta name="description" content="Arjun in your browser">
6+
<meta name="keywords" content="Arjun, Functional Synthesis, WebAssembly, JavaScript, Emscripten">
7+
<meta name="author" content="Mate Soos">
8+
<meta charset="UTF-8">
9+
<meta name="viewport" content="width=device-width, initial-scale=1.0">
10+
<title>Arjun in your browser</title>
11+
<style>
12+
body {
13+
font-family: Arial, sans-serif;
14+
max-width: 800px;
15+
margin: 0 auto;
16+
padding: 20px;
17+
line-height: 1.6;
18+
}
19+
.container {
20+
display: flex;
21+
flex-direction: column;
22+
gap: 20px;
23+
}
24+
textarea {
25+
width: 100%;
26+
height: 200px;
27+
padding: 10px;
28+
box-sizing: border-box;
29+
font-family: monospace;
30+
border: 1px solid #ddd;
31+
border-radius: 4px;
32+
}
33+
button {
34+
padding: 10px 15px;
35+
background-color: #4CAF50;
36+
color: white;
37+
border: none;
38+
border-radius: 4px;
39+
cursor: pointer;
40+
font-size: 16px;
41+
transition: background-color 0.3s;
42+
}
43+
button:hover {
44+
background-color: #45a049;
45+
}
46+
button:disabled {
47+
background-color: #cccccc;
48+
cursor: not-allowed;
49+
}
50+
#output {
51+
border: 1px solid #ddd;
52+
padding: 15px;
53+
min-height: 100px;
54+
white-space: pre-wrap;
55+
background-color: #f9f9f9;
56+
border-radius: 4px;
57+
font-family: monospace;
58+
overflow-y: auto;
59+
max-height: 400px;
60+
}
61+
.status {
62+
font-style: italic;
63+
color: #666;
64+
margin-left: 10px;
65+
}
66+
label {
67+
font-weight: bold;
68+
display: block;
69+
margin-bottom: 5px;
70+
}
71+
.progress-container {
72+
width: 100%;
73+
background-color: #f1f1f1;
74+
border-radius: 4px;
75+
margin-top: 10px;
76+
}
77+
#progress-bar {
78+
height: 10px;
79+
background-color: #4CAF50;
80+
border-radius: 4px;
81+
width: 0%;
82+
transition: width 0.3s;
83+
}
84+
</style>
85+
</head>
86+
<body>
87+
<div class="container">
88+
<h1>Arjun Functional Synthesis in Your Browser</h1>
89+
<div>Copy your CNF formula in the input box below and click "Run
90+
arjun.js" to run the Functional Synthesis engine in your browser.
91+
The output will be displayed below the input box. Format
92+
description is available <a
93+
href="https://jix.github.io/varisat/manual/0.2.0/formats/dimacs.html">here</a></div>
94+
You need to have "c p show ... 0" for all the variables that are inputs
95+
<div>
96+
<label for="extra-args">Extra command line arguments:</label>
97+
<input type="text" id="extra-args"
98+
value='--mstrategy "const(max_repairs=400),const(max_repairs=400,inv_learnt=1),bve"'
99+
style="width:100%;padding:8px;box-sizing:border-box;font-family:monospace;border:1px solid #ddd;border-radius:4px;">
100+
</div>
101+
102+
<div>
103+
<label for="input-content">CNF:</label>
104+
<textarea id="input-content">p cnf 3 3
105+
-1 -2 3 0
106+
1 -3 0
107+
2 -3 0
108+
c p show 1 2 0
109+
</textarea>
110+
</div>
111+
112+
<div>
113+
<button id="run-button">Run arjun.js</button>
114+
<button id="cancel-button">Cancel</button>
115+
<span id="status" class="status">Loading WebAssembly module...</span>
116+
<div class="progress-container">
117+
<div id="progress-bar"></div>
118+
</div>
119+
</div>
120+
121+
<div>
122+
<label for="output">Output:</label>
123+
<div id="output">Ready - enter your input and click "Run arjun.js"</div>
124+
</div>
125+
</div>
126+
127+
<script>
128+
// Main thread Module configuration
129+
var Module = {
130+
noInitialRun: true,
131+
stdin: function() { return null; },
132+
onRuntimeInitialized: function() {
133+
document.getElementById('status').textContent = 'Ready';
134+
document.getElementById('run-button').disabled = false;
135+
}
136+
};
137+
138+
// Create worker with proper WASM loading
139+
function createEmscriptenWorker() {
140+
const workerCode = `
141+
var Module = {
142+
noInitialRun: true,
143+
stdin: function() { return null; },
144+
print: function(text) {
145+
postMessage({ type: 'output', content: text });
146+
},
147+
printErr: function(text) {
148+
console.error('Error:', text);
149+
//postMessage({ type: 'output', content: 'ERROR: ' + text });
150+
},
151+
onRuntimeInitialized: function() {
152+
postMessage({ type: 'ready' });
153+
},
154+
locateFile: function(path) {
155+
console.log('Locating file:', path);
156+
// Resolve correct path for WASM file
157+
if (path.endsWith('.wasm')) {
158+
return self.workerOptions.wasmPath || 'arjun.wasm';
159+
}
160+
return path;
161+
}
162+
};
163+
164+
// This will be replaced by the Emscripten-generated code
165+
var wasmBinary;
166+
167+
onmessage = function(e) {
168+
if (e.data.type === 'init') {
169+
console.log('Initializing worker with options:', e.data.options);
170+
self.workerOptions = e.data.options;
171+
importScripts(e.data.options.jsPath);
172+
}
173+
else if (e.data.type === 'run') {
174+
try {
175+
console.log('Running with args:', e.data.args);
176+
Module.FS.writeFile('/input.cnf', e.data.input);
177+
var args = ['--verb', '1', '--synth'].concat(e.data.extraArgs || []).concat(['/input.cnf']);
178+
Module.callMain(args);
179+
postMessage({ type: 'done' });
180+
} catch (e) {
181+
postMessage({ type: 'error', content: e.toString() });
182+
}
183+
}
184+
};
185+
`;
186+
187+
const blob = new Blob([workerCode], { type: 'application/javascript' });
188+
return URL.createObjectURL(blob);
189+
}
190+
191+
// Main execution logic
192+
function parseExtraArgs(str) {
193+
// Shell-like tokenizer: handles "quoted strings" and unquoted tokens
194+
const args = [];
195+
let i = 0;
196+
while (i < str.length) {
197+
while (i < str.length && str[i] === ' ') i++;
198+
if (i >= str.length) break;
199+
if (str[i] === '"') {
200+
i++;
201+
let start = i;
202+
while (i < str.length && str[i] !== '"') i++;
203+
args.push(str.slice(start, i));
204+
if (i < str.length) i++; // skip closing quote
205+
} else {
206+
let start = i;
207+
while (i < str.length && str[i] !== ' ') i++;
208+
args.push(str.slice(start, i));
209+
}
210+
}
211+
return args;
212+
}
213+
214+
document.getElementById('run-button').addEventListener('click', async function() {
215+
const inputContent = document.getElementById('input-content').value;
216+
const outputDiv = document.getElementById('output');
217+
const extraArgs = parseExtraArgs(document.getElementById('extra-args').value);
218+
219+
if (!inputContent.trim()) {
220+
outputDiv.textContent = 'Error: Please enter input content';
221+
return;
222+
}
223+
224+
outputDiv.textContent = 'Initializing...\n';
225+
document.getElementById('run-button').disabled = true;
226+
document.getElementById('status').textContent = 'Running...';
227+
228+
// Get absolute URL for WASM file
229+
const wasmPath = new URL('arjun.wasm', window.location.href).href;
230+
const jsPath = new URL('arjun.js', window.location.href).href;
231+
const workerUrl = createEmscriptenWorker();
232+
const worker = new Worker(workerUrl);
233+
234+
worker.onmessage = function(e) {
235+
switch (e.data.type) {
236+
case 'output':
237+
console.log('Output:', e.data.content);
238+
outputDiv.textContent += e.data.content + '\n';
239+
outputDiv.scrollTop = outputDiv.scrollHeight;
240+
break;
241+
case 'ready':
242+
//console.log('ready. Sending input:', inputContent);
243+
worker.postMessage({
244+
type: 'run',
245+
input: inputContent,
246+
extraArgs: extraArgs
247+
});
248+
break;
249+
case 'done':
250+
document.getElementById('status').textContent = 'Completed';
251+
document.getElementById('run-button').disabled = false;
252+
worker.terminate();
253+
URL.revokeObjectURL(workerUrl);
254+
break;
255+
case 'error':
256+
outputDiv.textContent += 'Error: ' + e.data.content + '\n';
257+
document.getElementById('status').textContent = 'Failed';
258+
document.getElementById('run-button').disabled = false;
259+
worker.terminate();
260+
URL.revokeObjectURL(workerUrl);
261+
break;
262+
}
263+
};
264+
265+
// Initialize worker with proper paths
266+
worker.postMessage({
267+
type: 'init',
268+
options: {
269+
jsPath: jsPath,
270+
wasmPath: wasmPath
271+
}
272+
});
273+
});
274+
275+
// Load arjun.js in main thread
276+
const script = document.createElement('script');
277+
script.src = 'arjun.js';
278+
document.body.appendChild(script);
279+
</script>
280+
</body>
281+
</html>

‎scripts/build_emscripten.sh‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@
22
set -e
33

44
rm -rf lib* Test* tests* include tests CM* cmake* arjun Makefile rjun-src
5-
emcmake cmake -DCMAKE_INSTALL_PREFIX=$EMINSTALL -DSYNTH=OFF ..
5+
emcmake cmake -DCMAKE_BUILD_TYPE=Debug -DCMAKE_INSTALL_PREFIX=$EMINSTALL -DEXTRA_SYNTH=OFF ..
66
emmake make -j26
77
emmake make install
8+
cp arjun.wasm ../html
9+
cp $EMINSTALL/bin/arjun.js ../html

‎scripts/build_no_extra_synth.sh‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
#!/bin/bash
2+
3+
set -e
4+
5+
rm -rf lib* Test* tests* include tests CM* cmake* arjun Makefile rjun-src
6+
cmake -DEXTRA_SYNTH=OFF -DENABLE_TESTING=OFF ..
7+
make -j26

‎src/CMakeLists.txt‎

Lines changed: 20 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR})
2323
include_directories(${CRYPTOMINISAT5_INCLUDE_DIRS})
2424
include_directories(${SBVA_INCLUDE_DIRS})
2525
include_directories( ${GMP_INCLUDE_DIR} )
26-
if (SYNTH)
26+
if (EXTRA_SYNTH)
2727
include_directories(${EVALMAXSAT_INCLUDE_DIRS})
2828
include_directories( ${MLPACK_INCLUDE_DIR} )
2929
endif()
@@ -58,12 +58,12 @@ set(libfiles
5858
autarky.cpp
5959
ccnr/ccnr.cpp
6060
${CMAKE_CURRENT_BINARY_DIR}/GitSHA1.cpp
61+
manthan.cpp
62+
interpolant.cpp
6163
)
6264

63-
if (SYNTH)
64-
set(libfiles ${libfiles}
65-
manthan.cpp
66-
interpolant.cpp)
65+
if (EXTRA_SYNTH)
66+
list(APPEND libfiles manthan_learn.cpp)
6767
endif()
6868

6969
add_library(arjun ${libfiles})
@@ -78,11 +78,7 @@ target_link_libraries(arjun
7878
LINK_PUBLIC ${TREEDECOMP_LIBRARIES}
7979
)
8080

81-
if (SYNTH)
82-
add_executable(arjun-bin main.cpp synth.cpp)
83-
else()
84-
add_executable(arjun-bin main.cpp)
85-
endif()
81+
add_executable(arjun-bin main.cpp synth.cpp)
8682
add_executable(arjun-example example.cpp)
8783
add_executable(test-synth test-synth.cpp)
8884

@@ -95,10 +91,20 @@ set_target_properties(arjun PROPERTIES
9591
VERSION ${PROJECT_VERSION_MAJOR}.${PROJECT_VERSION_MINOR}
9692
SOVERSION ${PROJECT_VERSION_MAJOR}.${PROJECT_VERSION_MINOR}
9793
)
98-
set_target_properties(arjun-bin PROPERTIES
99-
OUTPUT_NAME arjun
100-
RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
101-
INSTALL_RPATH_USE_LINK_PATH TRUE)
94+
95+
if(CMAKE_SYSTEM_NAME STREQUAL "Emscripten")
96+
set_target_properties(arjun-bin PROPERTIES
97+
OUTPUT_NAME arjun
98+
RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
99+
INSTALL_RPATH_USE_LINK_PATH TRUE
100+
LINK_FLAGS "-s WASM=1 -s ALLOW_MEMORY_GROWTH=1 -s EXPORTED_RUNTIME_METHODS='[\"callMain\", \"ccall\", \"cwrap\", \"FS\", \"print\"]' -s FORCE_FILESYSTEM=1"
101+
)
102+
else()
103+
set_target_properties(arjun-bin PROPERTIES
104+
OUTPUT_NAME arjun
105+
RUNTIME_OUTPUT_DIRECTORY ${PROJECT_BINARY_DIR}
106+
INSTALL_RPATH_USE_LINK_PATH TRUE)
107+
endif()
102108
target_link_libraries(arjun-bin ${arjun_bin_exec_link_libs} arjun)
103109

104110
set_target_properties(arjun-example PROPERTIES

0 commit comments

Comments
 (0)