diff --git a/Dockerfile b/Dockerfile new file mode 100644 index 0000000..324daa9 --- /dev/null +++ b/Dockerfile @@ -0,0 +1,6 @@ +FROM maven:3.6.3-jdk-11 +ADD ./target/server-jar-with-dependencies.jar ./ +RUN mkdir -p ./snark-20120808r02 +COPY ./snark-20120808r02/ ./snark-20120808r02 +EXPOSE 25333 25334 +CMD java -jar server-jar-with-dependencies.jar \ No newline at end of file diff --git a/Example.ipynb b/Example.ipynb new file mode 100644 index 0000000..91a9def --- /dev/null +++ b/Example.ipynb @@ -0,0 +1,103 @@ +{ + "cells": [ + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [], + "source": [ + "from interface import *" + ] + }, + { + "cell_type": "code", + "execution_count": 9, + "metadata": {}, + "outputs": [], + "source": [ + "goal = \"(Believes! a (and P Q))\"" + ] + }, + { + "cell_type": "code", + "execution_count": 11, + "metadata": {}, + "outputs": [ + { + "data": { + "text/plain": [ + "'[a1 ]'" + ] + }, + "execution_count": 11, + "metadata": {}, + "output_type": "execute_result" + } + ], + "source": [ + "plan_from_description(\"\"\"\n", + " {:name \"test 1\"\n", + " :background [p]\n", + " :start [q]\n", + " :goal [r]\n", + " :actions [(define-action a1 ()\n", + " {:preconditions [(or q r)]\n", + " :additions [r]\n", + " :deletions [q]})]\n", + "\n", + " :expected-plans ([a1])}\n", + "\"\"\")" + ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] + } + ], + "metadata": { + "kernelspec": { + "display_name": "Python 3", + "language": "python", + "name": "python3" + }, + "language_info": { + "codemirror_mode": { + "name": "ipython", + "version": 3 + }, + "file_extension": ".py", + "mimetype": "text/x-python", + "name": "python", + "nbconvert_exporter": "python", + "pygments_lexer": "ipython3", + "version": "3.6.8" + }, + "pycharm": { + "stem_cell": { + "cell_type": "raw", + "metadata": { + "collapsed": false + }, + "source": [] + } + }, + "toc": { + "base_numbering": 1, + "nav_menu": {}, + "number_sections": false, + "sideBar": false, + "skip_h1_title": false, + "title_cell": "Table of Contents", + "title_sidebar": "Contents", + "toc_cell": false, + "toc_position": {}, + "toc_section_display": false, + "toc_window_display": false + } + }, + "nbformat": 4, + "nbformat_minor": 2 +} diff --git a/docker-compose.yml b/docker-compose.yml new file mode 100644 index 0000000..47e9911 --- /dev/null +++ b/docker-compose.yml @@ -0,0 +1,13 @@ +version: "3.0" +services: + py-shadowprover: + image: naveensundarg/py-interface-spectra:0.1.3 + ports: + - "25334:25334" + - "25333:25333" + interface: + image: naveensundarg/py-interface-spectra:0.1.3 + ports: + - "8888:8888" + volumes: + - ./files:/base \ No newline at end of file diff --git a/interface.py b/interface.py new file mode 100644 index 0000000..7e264fc --- /dev/null +++ b/interface.py @@ -0,0 +1,30 @@ +from py4j.java_gateway import JavaGateway + +gateway = None + +def start(): + global gateway + if not (gateway): + gateway = JavaGateway() + +def stop(): + global gateway + gateway = None + +def plan_from_description(description): + global gateway + if not gateway: + start() + return gateway.proveFromDescription(description) + +def prove(assumptions, goal): + + global gateway + if not gateway: + start() + + lst = gateway.newEmptyList() + for assumption in assumptions: + lst.append(assumption) + + return gateway.prove(lst, goal) \ No newline at end of file diff --git a/pom.xml b/pom.xml index c3d0f84..3ac2cdd 100644 --- a/pom.xml +++ b/pom.xml @@ -8,6 +8,55 @@ planner 0.50 + + + + org.apache.maven.plugins + maven-assembly-plugin + 2.4 + + + sandbox + + + + com.naveensundarg.planner.Py4JServer + + + + jar-with-dependencies + + sandbox + + package + + single + + + + server + + + + true + com.naveensundarg.planner.Py4JServer + + + + jar-with-dependencies + + server + + package + + single + + + + + + + @@ -41,6 +90,14 @@ [24.1.1,) + + + net.sf.py4j + py4j + 0.8.1 + + + diff --git a/src/main/java/com/naveensundarg/planner/Py4JServer.java b/src/main/java/com/naveensundarg/planner/Py4JServer.java new file mode 100644 index 0000000..e365f72 --- /dev/null +++ b/src/main/java/com/naveensundarg/planner/Py4JServer.java @@ -0,0 +1,86 @@ +package com.naveensundarg.planner; + +import com.naveensundarg.planner.utils.PlanningProblem; +import com.naveensundarg.shadow.prover.core.ccprovers.CognitiveCalculusProver; +import com.naveensundarg.shadow.prover.core.proof.Justification; +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.utils.Problem; +import com.naveensundarg.shadow.prover.utils.ProblemReader; +import com.naveensundarg.shadow.prover.utils.Reader; +import py4j.GatewayServer; + +import java.io.ByteArrayInputStream; +import java.net.Inet4Address; +import java.net.InetAddress; +import java.net.UnknownHostException; +import java.util.*; +import java.util.stream.Collectors; + + +public final class Py4JServer { + + + private DepthFirstPlanner depthFirstPlanner; + + + public Py4JServer(){ + + depthFirstPlanner = new DepthFirstPlanner(); + + } + + + public Planner getPlanner(){ + return depthFirstPlanner; + } + + public static void main(String[] args) throws UnknownHostException { + + System.out.println("--------------- Starting GatewayServer --------------- "); + System.out.println("--------------- Started Py4J Gateway --------------- "); + + InetAddress addr; + System.setProperty("java.net.preferIPv4Stack", "true"); + addr = Inet4Address.getByName("0.0.0.0"); + GatewayServer server = new GatewayServer(new Py4JServer(),25333, 25334, addr,addr, 0, 0, null); + System.out.println("--------------- Started Py4J Gateway --------------- "); + + server.start(); + + } + + public ArrayList newEmptyList(){ + + return new ArrayList(); + } + + public String proveFromDescription(String fileString){ + try { + + List planningProblemList = (PlanningProblem.readFromFile(new ByteArrayInputStream(fileString.getBytes()))); + + Planner depthFirstPlanner = new DepthFirstPlanner(); + + PlanningProblem planningProblem = planningProblemList.get(0); + + + Optional> optionalPlans = depthFirstPlanner.plan( + planningProblem.getBackground(), + planningProblem.getActions(), + planningProblem.getStart(), + planningProblem.getGoal()); + + if(optionalPlans.isPresent()) { + return optionalPlans.get().toString(); + } + else { + return "FAILED"; + } + + } catch (Reader.ParsingException e) { + e.printStackTrace(); + return null; + } + } + +} \ No newline at end of file