server.py

import torch
from proof_search import generate_tac, BestFirstSearchProver
from flask import Flask, request, jsonify, render_template


app = Flask(__name__)


@app.route('/project/ds-prover/')
def hello():
    return render_template("index.html")


@app.route('/project/ds-prover/prove/', methods=['POST'])
def prove():
    
    if not request.json:
        return jsonify({'error': 'Request must be in JSON format'}), 400
    
    data = request.get_json()
    
    if 'statement' not in data:
        return jsonify({'error': 'Missing parameter: statement'}), 400
    elif type(data['statement']) is not str:
        return jsonify({'error': 'statement must be a string'}), 400

    bfs = BestFirstSearchProver(timeout=300, aug = data["model"] == "augmented", dynamic = data["sampling"] == "dynamic")
    result = bfs.search(data["statement"].strip())
    
    if result['proved']:
        if result['proof'] == []:
            return {'proved': 2, "statement": result['theorem'], "time": round(result['total_time'], 1)}
        else:
            imports = "import all\n"
            return {'proved': 1, "statement": imports + result['theorem'], "proof": result['proof'], "time": round(result['total_time'], 1)}
    else:
        return {'proved': 0, 'error': result['error']}
    
    
@app.route('/project/ds-prover/generate/', methods=['POST'])
def generate():

    if not request.json:
        return jsonify({'error': 'Request must be in JSON format'}), 400
    
    data = request.get_json()
    
    if 'goal' not in data:
        return jsonify({'error': 'Missing parameter: goal'}), 400
    elif type(data['goal']) is not str:
        return jsonify({'error': 'goal must be a string'}), 400
    
    count = 32
    if type(data['num_samples']) == int:
        if data['num_samples'] < 2:
            count = 2
        elif data['num_samples'] > 100:
            count = 100
        else:
            count = data['num_samples']
            
    result = generate_tac(ts = data['goal'],
                          count = count,
                          aug = data["model"] == "augmented")
    
    torch.cuda.empty_cache()
    
    return result


if __name__ == '__main__':
    app.run(debug=True, port=5001, host='0.0.0.0')