Add z3 on backend

backend/Dockerfile

@@ -5,6 +5,9 @@ WORKDIR /backend
 
 COPY . /backend 
 
+RUN apt-get update && apt-get install -y
+RUN apt-get install z3 -y
+
 RUN pip install --no-cache-dir --upgrade pip setuptools
 RUN pip install --no-cache-dir -r requirements.txt
 

backend/routes.py

@@ -3,32 +3,40 @@
 from datetime import datetime, timedelta
 from flask import Blueprint, request, jsonify, session, make_response, abort
 from utils.db import db, Data
-from utils import xmv 
+from utils import xmv, z3
 from utils.permalink_generator import generate_passphrase
 from utils.db_query import *
 import pytz
 aware_datetime = datetime.now(pytz.utc)
 
 routes = Blueprint('routes', __name__)
 
-TIME_WINDOW = 1 # time window within which multiple requests are not allowed
+TIME_WINDOW = 1 
 
-# Check if the code is too large
 def is_valid_size(code: str) -> bool:
+  """Check if the code is less than 1MB
+  
+  Parameters:
+    code (str): The code to be checked
+    
+  Returns:
+    bool: True if the code is less than 1MB, False otherwise
+  """
   size_in_bytes = sys.getsizeof(code)
   size_in_mb = size_in_bytes / (1024*1024)
   return size_in_mb <= 1
 
 
 @routes.route('/api/')
 def index():
-    current_time = datetime.now(pytz.utc)
-    last_request_time = session.get('last_request_time')
-    if last_request_time is not None and current_time - last_request_time < timedelta(seconds=TIME_WINDOW):
-        return abort(429)  # HTTP status code for "Too Many Requests"
+  """Index page"""
+  current_time = datetime.now(pytz.utc)
+  last_request_time = session.get('last_request_time')
+  if last_request_time is not None and current_time - last_request_time < timedelta(seconds=TIME_WINDOW):
+    return abort(429) # Too Many Requests
 
-    session['last_request_time'] = current_time
-    return "Request accepted"
+  session['last_request_time'] = current_time
+  return "Request accepted"
 
 
 
@@ -116,7 +124,29 @@ def run_nuxmv():
     res = xmv.process_commands(code)
     response = make_response(jsonify({'result': res}), 200)
   except:
-    response = make_response(jsonify({'result': "Error running nuXmv. Server is busy. Please try again after"}), 503)
+    response = make_response(jsonify({'result': "Error running nuXmv. Server is busy. Please try again"}), 503)
 
   return response
-
+
+@routes.route('/api/run_z3', methods=['POST'])
+def run_z3():
+  data = request.get_json()
+  code = data['code']
+  current_time = datetime.now(pytz.utc)
+
+  # Check if the code is too large
+  if not is_valid_size(code):
+    return {'error': "The code is too large."}, 413
+
+  last_request_time = session.get('last_request_time')
+
+  if last_request_time is not None and current_time - last_request_time < timedelta(seconds=TIME_WINDOW):
+    response = make_response(jsonify({'error': "You've already made a request recently."}), 429)
+    return response
+  try:
+    res = z3.process_commands(code)
+    response = make_response(jsonify({'result': res}), 200)
+  except:
+    response = make_response(jsonify({'result': "Error running Z3. Server is busy. Please try again"}), 503)
+
+  return response

backend/utils/z3.py

@@ -0,0 +1,48 @@
+import os
+import subprocess
+import tempfile
+import re
+import queue
+import concurrent.futures
+
+MAX_CONCURRENT_REQUESTS = 10 # Maximum number of concurrent subprocesses
+
+executor = concurrent.futures.ThreadPoolExecutor(max_workers=MAX_CONCURRENT_REQUESTS) #thread pool with a maximum of max_concurrent threads
+
+code_queue = queue.Queue() # to hold incoming commands
+
+
+def run_z3(code: str):
+  tmp_file = tempfile.NamedTemporaryFile(mode='w', delete=False, suffix='.smt2')
+  tmp_file.write(code.strip())  
+  tmp_file.close()
+  print(tmp_file.name)
+  command = ["z3", "-smt2", tmp_file.name] 
+  try:
+    result = subprocess.run(command, capture_output=True, text=True, timeout=5)
+    os.remove(tmp_file.name)
+    return result.stdout
+  except subprocess.TimeoutExpired:
+    os.remove(tmp_file.name)
+    return "Process timed out after {} seconds".format(5)
+
+
+def prettify_output(stdout: str):
+  res = [line for line in stdout.split('\n') if '***' not in line.lower() and line.strip()]
+  return '\n'.join(res)
+
+def prettify_error(stderr: str):
+  pattern = r'^.*?:(?=\sline)'
+  res = [re.sub(pattern, 'error:', line) for line in stderr.split('\n') ]
+  res_clean = [item for item in res if item != '']
+  return '\n'.join(res_clean[:-3])
+
+
+def process_commands(code: str):
+  code_queue.put(code)
+  while True:
+    code_command = code_queue.get()
+    if code_queue is None:
+      break
+    ex = executor.submit(run_z3, code_command)
+    return ex.result()

frontend/main.js

@@ -456,7 +456,7 @@ function run_limboole(wrapper) {
   info.innerText = "";
 
   let non_ascii = findNonASCII(window.input_textarea);
-  if(findNonASCII){
+  if(non_ascii != null){
     info.innerText += `<stdin>:${non_ascii.position}:parse error at '${non_ascii.character}' expected ASCII character\n`;
     run_button_enable();
     return;
@@ -514,25 +514,67 @@ Module.print = (text) => {
   info.innerText += text + "\n";
 };
 
+
+/* ---------------Start z3 --------------- */
 function run_z3(code) {
   const info = document.getElementById("info");
   editor.getModel().setValue(code);
-  if (z3_loaded) {
+  fetch(apiUrl+'run_z3', {
+    method: 'POST',
+    headers: {
+      'Content-Type': 'application/json',
+    },
+    body: JSON.stringify({code: code}),
+  })
+  .then(response => {
+    if (response.status === 200) {
+        return response.json();
+    } else if(response.status === 413){
+      alert("Code size is too large!");
+      throw new Error('Request failed with status ' + response.status);
+    } else if(response.status === 429){
+      alert("Slow Down! You've already made a request recently.");
+      throw new Error('Request failed with status ' + response.status);
+    }else {
+      throw new Error('Request failed with status ' + response.status);
+    }
+  })
+  .then(data => {
     try {
       info.innerText = "";
+      info.innerText += data.result;
       save_to_db(code);
-      let res = Z3.solve(code);
-      info.innerText += res;
     } catch (error) {
       console.error(error);
-      // info.innerText += error;
+      //info.innerText += error;
     }
-  } else {
-    info.innerText = "Wait for Z3 to load and try again."
-  }
-  run_button_enable()
+  })
+  .catch((error) => {
+    console.error('Error:', error);
+  });
+  run_button_enable();
+
 }
 
+// function run_z3(code) {
+//   const info = document.getElementById("info");
+//   editor.getModel().setValue(code);
+//   if (z3_loaded) {
+//     try {
+//       info.innerText = "";
+//       save_to_db(code);
+//       let res = Z3.solve(code);
+//       info.innerText += res;
+//     } catch (error) {
+//       console.error(error);
+//       // info.innerText += error;
+//     }
+//   } else {
+//     info.innerText = "Wait for Z3 to load and try again."
+//   }
+//   run_button_enable()
+// }
+
 
 /* ---------------Start nuXmv --------------- */
 function run_nuxmv(code) {
@@ -829,7 +871,7 @@ function findNonASCII(input) {
       character: match[0],
       position: match.index
     };
+  }else{
+    return null;
   }
-
-  return null;
 }