Skip to content
Snippets Groups Projects
Commit adde75c8 authored by dgelessus's avatar dgelessus
Browse files

Add :solve command to solve a predicate with a different solver

parent 731b8867
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
.gitignore
+ 9
− 3
View file @ adde75c8
...@@ -10,6 +10,12 @@ ...@@ -10,6 +10,12 @@
# Jupyter notebook checkpoints # Jupyter notebook checkpoints
.ipynb_checkpoints/ .ipynb_checkpoints/
/notebooks/*/*.aux
/notebooks/*/*.log # LaTeX
/notebooks/*/*.out /notebooks/**/*.aux
/notebooks/**/*.log
/notebooks/**/*.out
# Kodkod log files
probkodkod.log
probkodkod.log.lck
notebooks/tests/solver.ipynb 0 → 100644
+ 192
− 0
View file @ adde75c8
%% Cell type:code id: tags:
``` prob
:help :solve
```
%% Output
:solve SOLVER PREDICATE
Solve a predicate with the specified solver
%% Cell type:code id: tags:
``` prob
:solve prob xx > 2 & yy < 5 & xx < yy
```
%% Output
TRUE
Solution:
xx = 3
yy = 4
%% Cell type:code id: tags:
``` prob
:solve kodkod xx > 2 & yy < 5 & xx < yy
```
%% Output
[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
[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).
[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]
TRUE
Solution:
xx = 3
yy = 4
%% Cell type:code id: tags:
``` prob
:solve smt_supported_interpreter xx > 2 & yy < 5 & xx < yy
```
%% Output
[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
[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
[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
[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))
[2018-05-24 14:05:12,949, T+20390] "ProB Output Logger for instance 44fff386" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! An error occurred !
[2018-05-24 14:05:12,950, T+20391] "ProB Output Logger for instance 44fff386" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! source(internal_error(smt_solvers_interface))
[2018-05-24 14:05:12,952, T+20393] "ProB Output Logger for instance 44fff386" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] ! Call for event start_solving failed. init_interface(z3)
[2018-05-24 14:05:12,987, T+20428] "ProB Output Logger for instance 44fff386" de.prob.cli.ProBInstance.readAndLog(ConsoleListener.java:48): [INFO] exception(make_call/3, error(existence_error(procedure,z3interface:pop_frame/0),existence_error($@(z3interface:pop_frame,4570400316),0,procedure,z3interface:pop_frame/0,0))).
[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
[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
[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
[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))
---------------------------------------------------------------------------
de.prob.exception.ProBError: (error(existence_error(procedure,:(z3interface,/(pop_frame,0))),existence_error($@(:(z3interface,pop_frame),4570400316),0,procedure,:(z3interface,/(pop_frame,0)),0)))
at de.prob.animator.CommandProcessor.extractResult(CommandProcessor.java:70)
at de.prob.animator.CommandProcessor.sendCommand(CommandProcessor.java:51)
at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:68)
at de.prob.statespace.StateSpace.execute(StateSpace.java:549)
at de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:70)
at de.prob2.jupyter.ProBKernel.executeLineCommand(ProBKernel.java:118)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:142)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)
%% Cell type:code id: tags:
``` prob
:solve z3 xx > 2 & yy < 5 & xx < yy
```
%% Output
[2018-05-24 14:05:13,149, T+20590] "Shell-0" de.prob.animator.AnimatorImpl.getErrorItems(AnimatorImpl.java:105): [ERROR] ProB raised exception(s):
[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)
[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
---------------------------------------------------------------------------
de.prob.exception.ProBError: ProB reported Errors
ProB returned error messages:
Internal error: Call for event start_solving failed. init_interface(z3)
at de.prob.animator.command.AbstractCommand.processErrorResult(AbstractCommand.java:137)
at de.prob.animator.AnimatorImpl.execute(AnimatorImpl.java:81)
at de.prob.statespace.StateSpace.execute(StateSpace.java:549)
at de.prob2.jupyter.commands.SolveCommand.run(SolveCommand.java:70)
at de.prob2.jupyter.ProBKernel.executeLineCommand(ProBKernel.java:118)
at de.prob2.jupyter.ProBKernel.eval(ProBKernel.java:142)
at io.github.spencerpark.jupyter.kernel.BaseKernel.handleExecuteRequest(BaseKernel.java:282)
at io.github.spencerpark.jupyter.channels.ShellChannel.lambda$bind$0(ShellChannel.java:50)
at java.lang.Thread.run(Thread.java:748)
at io.github.spencerpark.jupyter.channels.Loop.run(Loop.java:39)
[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
src/main/java/de/prob2/jupyter/ProBKernel.java
+ 2
− 0
View file @ adde75c8
...@@ -28,6 +28,7 @@ import de.prob2.jupyter.commands.LoadCellCommand; ...@@ -28,6 +28,7 @@ import de.prob2.jupyter.commands.LoadCellCommand;
import de.prob2.jupyter.commands.LoadFileCommand; import de.prob2.jupyter.commands.LoadFileCommand;
import de.prob2.jupyter.commands.NoSuchCommandException; import de.prob2.jupyter.commands.NoSuchCommandException;
import de.prob2.jupyter.commands.PrefCommand; import de.prob2.jupyter.commands.PrefCommand;
import de.prob2.jupyter.commands.SolveCommand;
import de.prob2.jupyter.commands.VersionCommand; import de.prob2.jupyter.commands.VersionCommand;
import io.github.spencerpark.jupyter.kernel.BaseKernel; import io.github.spencerpark.jupyter.kernel.BaseKernel;
...@@ -62,6 +63,7 @@ public final class ProBKernel extends BaseKernel { ...@@ -62,6 +63,7 @@ public final class ProBKernel extends BaseKernel {
this.lineCommands.put(":help", help); this.lineCommands.put(":help", help);
this.lineCommands.put(":version", injector.getInstance(VersionCommand.class)); this.lineCommands.put(":version", injector.getInstance(VersionCommand.class));
this.lineCommands.put(":eval", injector.getInstance(EvalCommand.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(":load", injector.getInstance(LoadFileCommand.class));
this.lineCommands.put(":pref", injector.getInstance(PrefCommand.class)); this.lineCommands.put(":pref", injector.getInstance(PrefCommand.class));
this.lineCommands.put(":browse", injector.getInstance(BrowseCommand.class)); this.lineCommands.put(":browse", injector.getInstance(BrowseCommand.class));
......
src/main/java/de/prob2/jupyter/commands/SolveCommand.java 0 → 100644
+ 73
− 0
View file @ adde75c8
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());
}
}
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment