From adde75c8b0a6297863619dc623d2a5ed88815143 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Thu, 24 May 2018 14:06:41 +0200
Subject: [PATCH] Add :solve command to solve a predicate with a different
solver
---
.gitignore | 12 +-
notebooks/tests/solver.ipynb | 192 ++++++++++++++++++
.../java/de/prob2/jupyter/ProBKernel.java | 2 +
.../prob2/jupyter/commands/SolveCommand.java | 73 +++++++
4 files changed, 276 insertions(+), 3 deletions(-)
create mode 100644 notebooks/tests/solver.ipynb
create mode 100644 src/main/java/de/prob2/jupyter/commands/SolveCommand.java
diff --git a/.gitignore b/.gitignore
index d0801b1..288dc53 100644
--- a/.gitignore
+++ b/.gitignore
@@ -10,6 +10,12 @@
# Jupyter notebook checkpoints
.ipynb_checkpoints/
-/notebooks/*/*.aux
-/notebooks/*/*.log
-/notebooks/*/*.out
+
+# LaTeX
+/notebooks/**/*.aux
+/notebooks/**/*.log
+/notebooks/**/*.out
+
+# Kodkod log files
+probkodkod.log
+probkodkod.log.lck
diff --git a/notebooks/tests/solver.ipynb b/notebooks/tests/solver.ipynb
new file mode 100644
index 0000000..6f4bb90
--- /dev/null
+++ b/notebooks/tests/solver.ipynb
@@ -0,0 +1,192 @@
+{
+ "cells": [
+ {
+ "cell_type": "code",
+ "execution_count": 1,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ ":solve SOLVER PREDICATE\n",
+ "\n",
+ "Solve a predicate with the specified solver"
+ ]
+ },
+ "execution_count": 1,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":help :solve"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 2,
+ "metadata": {},
+ "outputs": [
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\txx = 3\n",
+ "\tyy = 4"
+ ]
+ },
+ "execution_count": 2,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve prob xx > 2 & yy < 5 & xx < yy"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 3,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[2018-05-24 14:05:12,836, T+20277] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] kodkod ok: xx > 2 & yy < 5 & xx < yy ints: irange(2,5), intatoms: none\u001b[0m\n",
+ "[2018-05-24 14:05:12,839, T+20280] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Kodkod module started up successfully (SAT solver SAT4J with timeout of 1500 ms).\u001b[0m\n",
+ "[2018-05-24 14:05:12,840, T+20281] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Times for computing solutions: [3]\u001b[0m\n"
+ ]
+ },
+ {
+ "data": {
+ "text/plain": [
+ "TRUE\n",
+ "\n",
+ "Solution:\n",
+ "\txx = 3\n",
+ "\tyy = 4"
+ ]
+ },
+ "execution_count": 3,
+ "metadata": {},
+ "output_type": "execute_result"
+ }
+ ],
+ "source": [
+ ":solve kodkod xx > 2 & yy < 5 & xx < yy"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 4,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[2018-05-24 14:05:12,934, T+20375] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** LOADING Z3 library failed\u001b[0m\n",
+ "[2018-05-24 14:05:12,936, T+20377] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** error(system_error,system_error(dlopen(\"/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\") failed in load_foreign_resource/1: dlopen(/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle, 2): Library not loaded: libz3.dylib\u001b[0m\n",
+ "[2018-05-24 14:05:12,937, T+20378] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Referenced from: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\u001b[0m\n",
+ "[2018-05-24 14:05:12,939, T+20380] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Reason: image not found))\u001b[0m\n",
+ "[2018-05-24 14:05:12,949, T+20390] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[31m\u001b[1m! An error occurred !\u001b[0m\n",
+ "[2018-05-24 14:05:12,950, T+20391] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! source(internal_error(smt_solvers_interface))\u001b[0m\n",
+ "[2018-05-24 14:05:12,952, T+20393] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0m\u001b[31m\u001b[1m! Call for event start_solving failed. init_interface(z3)\u001b[0m\n",
+ "[2018-05-24 14:05:12,987, T+20428] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] \u001b[0mexception(make_call/3, error(existence_error(procedure,z3interface:pop_frame/0),existence_error($@(z3interface:pop_frame,4570400316),0,procedure,z3interface:pop_frame/0,0))).\u001b[0m\n",
+ "[2018-05-24 14:05:12,992, T+20433] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** LOADING Z3 library failed\u001b[0m\n",
+ "[2018-05-24 14:05:12,993, T+20434] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** error(system_error,system_error(dlopen(\"/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\") failed in load_foreign_resource/1: dlopen(/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle, 2): Library not loaded: libz3.dylib\u001b[0m\n",
+ "[2018-05-24 14:05:12,994, T+20435] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Referenced from: /Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\u001b[0m\n",
+ "[2018-05-24 14:05:12,995, T+20436] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] Reason: image not found))\u001b[0m\n"
+ ]
+ },
+ {
+ "ename": "ProBError",
+ "evalue": "(error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4570400316),0,procedure,:(z3interface,/(pop_frame,0)),0)))",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[1m\u001b[31mde.prob.exception.ProBError: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4570400316),0,procedure,:(z3interface,/(pop_frame,0)),0)))\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.animator.CommandProcessor.extractResult(CommandProcessor.java:70)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:51)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:68)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.execute(StateSpace.java:549)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:70)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeLineCommand(ProBKernel.java:118)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:142)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\u001b[0m"
+ ]
+ }
+ ],
+ "source": [
+ ":solve smt_supported_interpreter xx > 2 & yy < 5 & xx < yy"
+ ]
+ },
+ {
+ "cell_type": "code",
+ "execution_count": 5,
+ "metadata": {},
+ "outputs": [
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[2018-05-24 14:05:13,149, T+20590] \"Shell-0\" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:105): [ERROR] ProB raised exception(s):\n",
+ "[2018-05-24 14:05:13,150, T+20591] \"Shell-0\" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:107): [ERROR] Internal error: Call for event start_solving failed. init_interface(z3)\n",
+ "[2018-05-24 14:05:13,152, T+20593] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** LOADING Z3 library failed\u001b[0m\n"
+ ]
+ },
+ {
+ "ename": "ProBError",
+ "evalue": "ProB reported Errors\nProB returned error messages:\nInternal error: Call for event start_solving failed. init_interface(z3)",
+ "output_type": "error",
+ "traceback": [
+ "\u001b[1m\u001b[31m---------------------------------------------------------------------------\u001b[0m",
+ "\u001b[1m\u001b[31mde.prob.exception.ProBError: ProB reported Errors\u001b[0m",
+ "\u001b[1m\u001b[31mProB returned error messages:\u001b[0m",
+ "\u001b[1m\u001b[31mInternal error: Call for event start_solving failed. init_interface(z3)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.animator.command.AbstractCommand.processErrorResult(AbstractCommand.java:137)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:81)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob.statespace.StateSpace.execute(StateSpace.java:549)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:70)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.executeLineCommand(ProBKernel.java:118)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:142)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat java.lang.Thread.run(Thread.java:748)\u001b[0m",
+ "\u001b[1m\u001b[31m\tat io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)\u001b[0m"
+ ]
+ },
+ {
+ "name": "stdout",
+ "output_type": "stream",
+ "text": [
+ "[2018-05-24 14:05:13,154, T+20595] \"ProB Output Logger for instance 44fff386\" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] *** error(system_error,system_error(dlopen(\"/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle\") failed in load_foreign_resource/1: dlopen(/Users/david/.prob/prob2-3.2.10-SNAPSHOT/lib/z3interface.bundle, 2): Library not loaded: libz3.dylib\u001b[0m\n"
+ ]
+ }
+ ],
+ "source": [
+ ":solve z3 xx > 2 & yy < 5 & xx < yy"
+ ]
+ }
+ ],
+ "metadata": {
+ "kernelspec": {
+ "display_name": "ProB 2",
+ "language": "prob",
+ "name": "prob2"
+ },
+ "language_info": {
+ "file_extension": ".prob",
+ "mimetype": "text/x-prob",
+ "name": "prob"
+ }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 2
+}
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index 774c15f..10d4df6 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -28,6 +28,7 @@ import de.prob2.jupyter.commands.LoadCellCommand;
import de.prob2.jupyter.commands.LoadFileCommand;
import de.prob2.jupyter.commands.NoSuchCommandException;
import de.prob2.jupyter.commands.PrefCommand;
+import de.prob2.jupyter.commands.SolveCommand;
import de.prob2.jupyter.commands.VersionCommand;
import io.github.spencerpark.jupyter.kernel.BaseKernel;
@@ -62,6 +63,7 @@ public final class ProBKernel extends BaseKernel {
this.lineCommands.put(":help", help);
this.lineCommands.put(":version", injector.getInstance(VersionCommand.class));
this.lineCommands.put(":eval", injector.getInstance(EvalCommand.class));
+ this.lineCommands.put(":solve", injector.getInstance(SolveCommand.class));
this.lineCommands.put(":load", injector.getInstance(LoadFileCommand.class));
this.lineCommands.put(":pref", injector.getInstance(PrefCommand.class));
this.lineCommands.put(":browse", injector.getInstance(BrowseCommand.class));
diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
new file mode 100644
index 0000000..c3bafd4
--- /dev/null
+++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java
@@ -0,0 +1,73 @@
+package de.prob2.jupyter.commands;
+
+import com.google.inject.Inject;
+
+import de.prob.animator.command.CbcSolveCommand;
+import de.prob.animator.domainobjects.FormulaExpand;
+import de.prob.animator.domainobjects.IEvalElement;
+import de.prob.statespace.AnimationSelector;
+import de.prob.statespace.Trace;
+
+import de.prob2.jupyter.ProBKernel;
+import de.prob2.jupyter.UserErrorException;
+
+import io.github.spencerpark.jupyter.messages.DisplayData;
+
+import org.jetbrains.annotations.NotNull;
+
+public final class SolveCommand implements LineCommand {
+ private final @NotNull AnimationSelector animationSelector;
+
+ @Inject
+ private SolveCommand(final @NotNull AnimationSelector animationSelector) {
+ super();
+
+ this.animationSelector = animationSelector;
+ }
+
+ @Override
+ public @NotNull String getSyntax() {
+ return ":solve SOLVER PREDICATE";
+ }
+
+ @Override
+ public @NotNull String getShortHelp() {
+ return "Solve a predicate with the specified solver";
+ }
+
+ @Override
+ public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+ final String[] split = argString.split("\\h+", 2);
+ if (split.length != 2) {
+ throw new UserErrorException("Expected 2 arguments, got 1");
+ }
+
+ final Trace trace = this.animationSelector.getCurrentTrace();
+ final CbcSolveCommand.Solvers solver;
+ switch (split[0]) {
+ case "prob":
+ solver = CbcSolveCommand.Solvers.PROB;
+ break;
+
+ case "kodkod":
+ solver = CbcSolveCommand.Solvers.KODKOD;
+ break;
+
+ case "smt_supported_interpreter":
+ solver = CbcSolveCommand.Solvers.SMT_SUPPORTED_INTERPRETER;
+ break;
+
+ case "z3":
+ solver = CbcSolveCommand.Solvers.Z3;
+ break;
+
+ default:
+ throw new UserErrorException("Unknown solver: " + split[0]);
+ }
+ final IEvalElement predicate = trace.getModel().parseFormula(split[1], FormulaExpand.EXPAND);
+
+ final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver);
+ trace.getStateSpace().execute(cmd);
+ return CommandUtils.displayDataForEvalResult(cmd.getValue());
+ }
+}
--
GitLab