Skip to content
Permalink
Browse files

Merge branch 'master' of github.com:ptal/bonsai

  • Loading branch information...
ptal committed Apr 15, 2019
2 parents 68a4f4c + 6a43d7a commit 26a22bff137175308b92e894715245f1941de098
@@ -22,7 +22,7 @@
<dependency>
<groupId>org.choco-solver</groupId>
<artifactId>choco-solver</artifactId>
<version>4.0.0</version>
<version>4.10.0</version>
</dependency>
<dependency>
<groupId>bonsai</groupId>
@@ -30,8 +30,8 @@
private int trials = 10;
private int timeLimitSeconds = 1080;

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

public static void main(String[] args) {
@@ -41,8 +41,8 @@ public static void main(String[] args) {
private void start() {
Config.timeout = timeLimitSeconds;
System.out.println(Config.headerCSV());
benchNQueens();
benchLatinSquare();
// benchNQueens();
// benchLatinSquare();
benchGolombRuler();
}

@@ -59,18 +59,18 @@ private void benchGolombRuler() {
for (Integer n : paramsGolombRuler) {
runBonsaiGolombRulerIOLB(n);
}
// for (Integer n : paramsGolombRuler) {
// runBonsaiGolombRulerFFM(n);
// }
// for (Integer n : paramsGolombRuler) {
// runBonsaiGolombRulerMDLB(n);
// }
for (Integer n : paramsGolombRuler) {
runBonsaiGolombRulerFFM(n);
}
for (Integer n : paramsGolombRuler) {
runBonsaiGolombRulerMDLB(n);
}
for (Integer n : paramsGolombRuler) {
runChocoGolombRulerIOLB(n);
}
// for (Integer n : paramsGolombRuler) {
// runChocoGolombRulerFFM(n);
// }
for (Integer n : paramsGolombRuler) {
runChocoGolombRulerFFM(n);
}
}

private void benchLatinSquare() {
@@ -38,11 +38,9 @@
public proc solve() =
modelChoco(write domains, write constraints);
module Solver solver = new Solver(write domains, write constraints, write consistent);
module SolutionNode solutions = new SolutionNode(write consistent);
par
<> run solver.propagation()
<> run solver.minDomLB()
<> flow when solutions.value |= 1 then stop end end
end
end

@@ -124,7 +124,7 @@ public void configureSearch(boolean isFFM) {
if (isFFM) {
model.getSolver().setSearch(Search.intVarSearch(new FirstFail(model),
new IntDomainMiddle(true),
DecisionOperator.int_split,
DecisionOperatorFactory.makeIntSplit(),
model.retrieveIntVars(true)));
}
else {
@@ -87,5 +87,6 @@ public void buildModel() {
public void configureSearch() {
model.getSolver().setSearch(minDomLBSearch(vars));
model.getSolver().limitTime(Config.timeout + "s");
// model.getSolver().showDecisions();
}
}
@@ -18,6 +18,8 @@ Finally, we go through a full application of this language by designing a intera

The code is available on [github](https://github.com/ptal/bonsai).

Note that this tutorial is a work-in-progress.

### Syntax cheat sheet

`p` and `q` are statements, `e` is an expression, `x` a variable identifier and `st` is a spacetime attribute (either `single_space`, `single_time` and `world_line`).
@@ -2,9 +2,8 @@

* [Introduction](README.md)
* [Getting Started](getting-started.md)
* [Synchronous Programming](synchronous-programming.md)
* [Learn Spacetime](learn-spacetime.md)
* [Universe](universe.md)
* [Application: Musical Composition](application-composition.md)
* [Benchmarks](benchmarks.md)
* [Contributing](contributing.md)
* [Submission to ESOP2019](complement-esop2019.md)
@@ -1,4 +1,4 @@
# Supplementary material to the submission to ESOP 2019
# Benchmark of the language

This supplementary page completes the evaluation of spacetime presented in the paper.
It also gives instructions to compile the examples presented in the paper.
@@ -1 +1,30 @@
# Learn Spacetime

Please [install spacetime](getting-started.md) first to run the program of this section.

## Running a first program

In this section, we compile a first spacetime program in a Java project.
Go to the toy project available at [examples/bonsai/HelloWorld](https://github.com/ptal/bonsai/tree/master/examples/bonsai/HelloWorld) and launch the following script:

```sh
./run.sh
```

It compiles and runs the code.
It prints the message `HelloWorld` 5 times:

```
Hello world!
1
Hello world!
2
Hello world!
3
Hello world!
4
5
```

You can start from this code to modify it.
The standard library of spacetime is usable and you can find different modules in the directory [libstd](https://github.com/ptal/bonsai/tree/master/libstd/src/main/java/bonsai).
@@ -27,7 +27,7 @@
<dependency>
<groupId>org.choco-solver</groupId>
<artifactId>choco-solver</artifactId>
<version>4.0.0</version>
<version>4.10.0</version>
</dependency>
<dependency>
<groupId>bonsai</groupId>
@@ -22,7 +22,7 @@
<dependency>
<groupId>org.choco-solver</groupId>
<artifactId>choco-solver</artifactId>
<version>4.0.0</version>
<version>4.10.0</version>
</dependency>
<dependency>
<groupId>bonsai</groupId>
@@ -48,16 +48,16 @@ public flow assign() =
when unknown |= consistent then
single_time IntVar x = readwrite var.getVariable(domains.vars());
single_time Integer v = readwrite val.selectValue(x);
space constraints <- x.eq(v) end;
space constraints <- x.ne(v) end
space readwrite domains.join_eq(x, v) end;
space readwrite domains.join_neq(x, v) end
end

public flow split() =
when unknown |= consistent then
single_time IntVar x = readwrite var.getVariable(domains.vars());
single_time Integer v = readwrite val.selectValue(x);
space constraints <- x.le(v) end;
space constraints <- x.gt(v) end
space readwrite domains.join_le(x, v) end;
space readwrite domains.join_gt(x, v) end
end

public static VariableSelector<IntVar> inputOrder(VarStore domains) {
@@ -22,6 +22,8 @@

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

public class MaximizeBAB
{
@@ -46,22 +48,23 @@ proc maximize() =
loop
when consistent |= true then
when true |= consistent then
single_space LMax pre_obj = new LMax(x.getUB());
single_space LMax pre_obj = new LMin(x.getUB());
pause;
obj <- pre_obj;
readwrite objV.inc();
else pause end
else pause end
end

flow yield_objective() =
when objV |= conV then
when conV |= objV then nothing
else
constraints <- x.gt(obj.unwrap());
single_time LMax objV2 = new LMax(objV.unwrap());
space conV <- objV2; end;
end
end
end
consistent <- updateBound(write x, read obj)

public static ES updateBound(IntVar x, LMax obj) {
try {
x.updateLowerBound(obj.unwrap() + 1, Cause.Null);
return new ES(Kleene.UNKNOWN);
}
catch (ContradictionException c) {
return new ES(Kleene.FALSE);
}
}
}
@@ -22,6 +22,8 @@

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

public class MinimizeBAB
{
@@ -30,8 +32,6 @@
ref single_space IntVar x;

public single_space LMin obj = bot;
single_space LMax objV = new LMax(0);
world_line LMax conV = new LMax(1);

public MinimizeBAB(ConstraintStore constraints, ES consistent, IntVar x) {
this.constraints = constraints;
@@ -49,19 +49,20 @@ proc minimize() =
single_space LMin pre_obj = new LMin(x.getLB());
pause;
obj <- pre_obj;
readwrite objV.inc();
else pause end
else pause end
end

flow yield_objective() =
when objV |= conV then
when conV |= objV then nothing
else
constraints <- x.lt(obj.unwrap());
single_time LMax objV2 = new LMax(objV.unwrap());
space conV <- objV2; end;
end
end
end
consistent <- updateBound(write x, read obj)

public static ES updateBound(IntVar x, LMin obj) {
try {
x.updateUpperBound(obj.unwrap() - 1, Cause.Null);
return new ES(Kleene.UNKNOWN);
}
catch (ContradictionException c) {
return new ES(Kleene.FALSE);
}
}
}
@@ -27,8 +27,8 @@ public BoundedDepth(LMax limit) {
public proc bound() =
module Depth depth = new Depth();
par
|| run depth.count();
|| flow
<> run depth.count();
<> flow
when depth.value |= limit then
prune
end
@@ -17,6 +17,9 @@
import bonsai.runtime.lattices.*;
import bonsai.statistics.Discrepancy;

// This strategy explores the search tree until it reaches a limit for the number of discrepancies taken, it is described in the following paper:
// W. D. Harvey and M. L. Ginsberg, “Limited discrepancy search,” in IJCAI (1), 1995, pp. 607–615.
// Note that this class only perform one iteration (given by limit).
public class BoundedDiscrepancy
{
ref single_space LMax limit;
@@ -27,8 +30,8 @@ public BoundedDiscrepancy(LMax limit) {
public proc bound() =
module Discrepancy dis = new Discrepancy();
par
|| run dis.count();
|| flow
<> run dis.count();
<> flow
space nothing end;
when dis.value |= limit then
prune
@@ -0,0 +1,63 @@
// 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.strategies;

import bonsai.runtime.lattices.*;
import bonsai.statistics.Depth;
import bonsai.statistics.Discrepancy;

import java.lang.System;

// Depth-bounded discrepancy search (DDS) improves ILDS by not requiring an upper bound on the depth of the search tree.
// It is available here:
// T. Walsh, “Depth-bounded discrepancy search,” in IJCAI, 1997, vol. 97, pp. 1388–1393.
public class DDS
{
// This variable represents the depth until which we can take discrepancies.
ref single_space LMax max_dis_at_depth;

public DDS(LMax max_dis_at_depth) {
this.max_dis_at_depth = max_dis_at_depth;
}

public proc bound() =
module Depth depth = new Depth();
single_space LMin zero = new LMin(0);
single_space LMin one = new LMin(1);
par
<> run depth.count();
<> flow
single_time LMin remaining_depth = minus(max_dis_at_depth, depth.value);
par
when remaining_depth |= zero then
space nothing end;
prune
else
when remaining_depth |= one then
prune;
space nothing end;
else
space nothing end;
end
end
end
end
end
end

public static LMin minus(LMax a, LMax b) {
return new LMin(a.unwrap() - b.unwrap());
}
}

0 comments on commit 26a22bf

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