Skip to content
Permalink
Browse files

[PPDP19] Prepare the repository for the final version of the paper.

  • Loading branch information...
ptal committed Jul 24, 2019
1 parent 9a2dced commit 77720c8867018308e80c427caf40aa05b4dcce75
@@ -29,9 +29,9 @@
private boolean human = true;
private int timeLimitSeconds = 1080;

private List<Integer> paramsNQueens = Arrays.asList(7,8,9,10,11);//,11,12,13,14);
private List<Integer> paramsGolombRuler = Arrays.asList(7,8,9,10,11);//,10,11,12,13,14);
private List<Integer> paramsLatinSquare = Arrays.asList(30,35,40,45,50,55);
private List<Integer> paramsNQueens = Arrays.asList(13,14,15);
private List<Integer> paramsGolombRuler = Arrays.asList(10,11,12);
private List<Integer> paramsLatinSquare = Arrays.asList(60,75,90);

public static void main(String[] args) {
new Benchmark().start();
@@ -1,6 +1,10 @@
# Companion guide to the paper submitted to PPDP19
# Companion guide (PPDP19)

This supplementary material gives instructions to compile and run the examples and benchmarks presented in the paper submitted to PPDP19.
* Reference: P. Talbot, “Spacetime Programming: A Synchronous Language for Composable Search Strategies,” in Proceedings of the 21st ACM International Symposium on Principles and Practice of Declarative Programming (PPDP 2019), Porto, Portugal, 2019.
* The paper is available [here](http://hyc.io/papers/ppdp2019.pdf).
* Tagged version of the language used in the paper on [Github](https://github.com/ptal/bonsai/tree/PPDP19).

This supplementary material gives instructions to compile and run the examples and benchmarks presented in the paper.

If you want to replicate any benchmark and running examples, first install the compiler and runtime as follows:

@@ -11,7 +15,7 @@ git checkout PPDP19
python3 setup.py
```

For more explanations, please go to the [Getting Started](getting-started.html) section (but do not forget to switch to the `PPDP19` branch).
In case of problems, please go to the [Getting Started](getting-started.html) section (but do not forget to switch to the `PPDP19` branch).

## Demo of the examples in the paper

@@ -54,4 +58,4 @@ cd runtime
mvn test
```

There are about 200 tests, ranging from the static analysis of the compiler ([compile-fail](https://github.com/ptal/bonsai/tree/master/data/test/compile-fail) and [compile-pass](https://github.com/ptal/bonsai/tree/master/data/test/compile-pass)) as well as the runtime behavior ([run-pass](https://github.com/ptal/bonsai/tree/master/data/test/run-pass)) to the correctness of the lattice library.
There are about 200 tests, ranging from the static analysis of the compiler ([compile-fail](https://github.com/ptal/bonsai/tree/master/data/test/compile-fail) and [compile-pass](https://github.com/ptal/bonsai/tree/master/data/test/compile-pass)), to the runtime behavior ([run-pass](https://github.com/ptal/bonsai/tree/master/data/test/run-pass)), and the correctness of the lattice library.
@@ -29,13 +29,16 @@ Note that this tutorial is a work-in-progress.
| `st T x = e` | Declares the variable `x` of type `T` with the spacetime `st`. |
| `when e then p else q end` | Executes `p` if `e` is equal to `true`, otherwise `q`. |
| `x <- e` | Joins the information of `e` into `x`. |
| `o.m(x1,..,xn)` | Executes the Java method `m` on the object `o`. Variables must be annotated by `read`, `write` or `readwrite` (`read` by default). |
| `pause` | Delays the execution to the next instant. |
| `pause up` | Delays and gives the control back to the upper universe. |
| `stop` | Delays and gives the control back to the host language. |
| `par p`\|\|`q end`| Executes concurrently `p` and `q`. Terminates when both terminate. |
| `par p <> q end`| Same as \|\| but terminates in the next instant if one process terminates before the other (weak preemption). |
| `p ; q` | Executes `p`, when it terminates, executes `q`. |
| `loop p end` | Executes indefinitely `p`. When `p` terminates it is executed from its beginning again. |
| `space p end` | Creates a new branch. All world_line variables are copied and are modified by `p` when the node is popped. |
| `prune` | Indicates that a branch should be pruned. |
| `abort when e in p end`| Executes `p` unless `e` is `true`, in which case the statement terminates in the current instant. |
| `suspend when e in p end`| Executes `p` in every instant in which `e` is `false`. |
| `universe with x in p end`| Executes `p` in a universe with the queue `x`. |
@@ -5,5 +5,6 @@
* [Learn Spacetime](learn-spacetime.md)
* [Universe](universe.md)
* [Application: Musical Composition](application-composition.md)
* [Complementary materials](PPDP19.md)
* [Research](research.md)
* [PPDP19](PPDP19.md)
* [Contributing](contributing.md)
@@ -0,0 +1,7 @@
# Companion guides to research papers

For each paper written about spacetime, I maintain a companion guide in order to:

1. Provide instructions to install the exact same version of the language than the one used in the paper.
2. Help people who wants to execute the examples presented in the paper.
3. Replicate the benchmarks with a single command.
@@ -0,0 +1,71 @@
// Copyright 2019 Pierre Talbot

// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at

// http://www.apache.org/licenses/LICENSE-2.0

// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

package bonsai.examples;

import java.lang.System;
import java.util.*;
import bonsai.runtime.queueing.*;
import bonsai.runtime.core.*;
import bonsai.runtime.lattices.*;

import bonsai.runtime.lattices.choco.*;
import org.chocosolver.solver.variables.*;
import org.chocosolver.solver.Cause;
import org.chocosolver.solver.exception.ContradictionException;

public class MinimizeBAB
{
ref world_line VarStore domains;
ref single_time ES consistent;
ref single_space IntVar x;

public single_space LMin obj = bot;

public MinimizeBAB(VarStore domains, ES consistent, IntVar x) {
this.domains = domains;
this.consistent = consistent;
this.x = x;
}

public proc solve =
par run minimize() <> run yield_objective() end

proc minimize =
loop
when consistent |= true then
when true |= consistent then
single_space LMin pre_obj = new LMin(x.getLB());
pause;
obj <- pre_obj;
else pause end
else pause end
end

flow yield_objective =
consistent <- updateBound(write domains, write x, read obj)
end

private static ES updateBound(VarStore _domains, IntVar x, LMin obj) {
try {
if (!obj.isBottom()) {
x.updateUpperBound(obj.unwrap() - 1, Cause.Null);
}
return new ES(Kleene.UNKNOWN);
}
catch (ContradictionException c) {
return new ES(Kleene.FALSE);
}
}
}
@@ -106,7 +106,7 @@ void section6LDS_IDS() {
}

void beginMessage() {
System.out.println("\n >>>> Welcome to the demo of the code presented in the paper submitted to PPDP19. <<<<\n");
System.out.println("\n >>>> Welcome to the demo of the code presented in the paper accepted to PPDP19. <<<<\n");
System.out.println("Note: The tree are drawn as follows: a '*' represents one node, and the spaces before '*' represent the depth of this node.");
System.out.println("For additional strategies including DDS and ILDS, please see libstd/ in the package `bonsai.strategies.*`.\n");
}
@@ -0,0 +1,100 @@
// Copyright 2019 Pierre Talbot

// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at

// http://www.apache.org/licenses/LICENSE-2.0

// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

package bonsai.examples;

import java.lang.System;
import java.util.*;
import bonsai.runtime.queueing.*;
import bonsai.runtime.core.*;
import bonsai.runtime.lattices.*;
import bonsai.runtime.lattices.choco.*;

import org.chocosolver.solver.*;
import org.chocosolver.solver.variables.*;

// This shows an example of BAB algorithm over the Golomb Ruler problem.
public class SolveBAB
{
world_line VarStore domains = new VarStore();
world_line ConstraintStore constraints = new ConstraintStore();
single_time ES consistent = unknown;

public proc solve =
single_space int m = 10;
init(m, write domains, write constraints);
single_space IntVar x = rulerLengthVar(m, write domains);
module MinimizeBAB bab = new MinimizeBAB(write domains, write consistent, write x);
module Solver solver = new Solver(write domains, write constraints, write consistent);
par
<> run solver.searchInputOrderLB()
<> run bab.solve()
<> flow when consistent |= true then
when true |= consistent then printBound(m,domains); end end
end
end
end

private static void init(int m, VarStore domains, ConstraintStore constraints)
{
IntVar[] ticks = new IntVar[m];
IntVar[] diffs = new IntVar[(m*m -m)/2];
Model model = domains.model();

int ub = (m < 31) ? (1 << (m + 1)) - 1 : 9999;
for(int i=0; i < ticks.length; i++) {
ticks[i] = (IntVar) domains.alloc(new VarStore.IntDomain(0, ub, true));
}
for(int i=0; i < diffs.length; i++) {
diffs[i] = (IntVar) domains.alloc(new VarStore.IntDomain(0, ub, true));
}

constraints.join_in_place(model.arithm(ticks[0], "=", 0));
for (int i = 0; i < m - 1; i++) {
constraints.join_in_place(model.arithm(ticks[i + 1], ">", ticks[i]));
}

IntVar[][] m_diffs = new IntVar[m][m];
for (int k = 0, i = 0; i < m - 1; i++) {
for (int j = i + 1; j < m; j++, k++) {
// d[k] is m[j]-m[i] and must be at least sum of first j-i integers
// <cpru 04/03/12> it is worth adding a constraint instead of a view
constraints.join_in_place(model.scalar(new IntVar[]{ticks[j], ticks[i]}, new int[]{1, -1}, "=", diffs[k]));
constraints.join_in_place(model.arithm(diffs[k], ">=", (j - i) * (j - i + 1) / 2));
constraints.join_in_place(model.arithm(diffs[k], "-", ticks[m - 1], "<=", -((m - 1 - j + i) * (m - j + i)) / 2));
constraints.join_in_place(model.arithm(diffs[k], "<=", ticks[m - 1], "-", ((m - 1 - j + i) * (m - j + i)) / 2));
m_diffs[i][j] = diffs[k];
}
}
constraints.join_in_place(model.allDifferent(diffs, "BC"));

// break symmetries
if (m > 2) {
constraints.join_in_place(model.arithm(diffs[0], "<", diffs[diffs.length - 1]));
}
}

private static IntVar rulerLengthVar(int m, VarStore domains) {
return (IntVar)domains.model().getVars()[m - 1];
}

private static int rulerLength(int m, VarStore domains) {
return rulerLengthVar(m, domains).getLB();
}

private static void printBound(int m, VarStore domains) {
System.out.println("Current bound = " + rulerLength(m, domains));
}
}

@@ -0,0 +1,83 @@
// Copyright 2019 Pierre Talbot

// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at

// http://www.apache.org/licenses/LICENSE-2.0

// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.

package bonsai.examples;

import java.lang.System;
import java.util.*;
import bonsai.runtime.queueing.*;
import bonsai.runtime.core.*;
import bonsai.runtime.lattices.*;
import bonsai.runtime.lattices.choco.*;

import org.chocosolver.solver.variables.*;
import org.chocosolver.solver.constraints.nary.alldifferent.*;
import org.chocosolver.solver.search.strategy.selectors.variables.*;
import org.chocosolver.solver.search.strategy.selectors.values.*;
import org.chocosolver.solver.*;

public class SolveNQueens
{
world_line VarStore domains = new VarStore();
world_line ConstraintStore constraints = new ConstraintStore();
single_time ES consistent = unknown;
single_space ArrayList<IntVar> queens = new ArrayList();

public proc nqueens =
modelNQueens(8, write queens, write domains, write constraints);
run search_one_sol()
end

public proc search_one_sol =
module Solver solver = new Solver(write domains, write constraints,
write consistent);
par
<> run solver.search()
<> loop
when consistent |= true then
when true |= consistent then
printSolution(queens);
stop;
else pause end
else pause end
end
end
end

private void modelNQueens(int n, ArrayList<IntVar> queens, VarStore domains,
ConstraintStore constraints)
{
IntVar[] vars = new IntVar[n];
IntVar[] diag1 = new IntVar[n];
IntVar[] diag2 = new IntVar[n];
for(int i = 0; i < n; i++) {
vars[i] = (IntVar) domains.alloc(new VarStore.IntDomain(1, n, false));
diag1[i] = domains.model().intOffsetView(vars[i], i);
diag2[i] = domains.model().intOffsetView(vars[i], -i);
}
constraints.join_in_place(new AllDifferent(vars, "BC"));
constraints.join_in_place(new AllDifferent(diag1, "BC"));
constraints.join_in_place(new AllDifferent(diag2, "BC"));
for(IntVar v : vars) { queens.add(v); }
}

private void printSolution(ArrayList<IntVar> queens) {
System.out.print("solution: [");
for (IntVar v : queens) {
System.out.print(v.getValue() + ",");
}
System.out.println("]");
}

}

0 comments on commit 77720c8

Please sign in to comment.
You can’t perform that action at this time.