Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 82 additions & 0 deletions .github/workflows/solver-web.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,82 @@
name: Browser solver package

on:
push:
tags: ['solver-web-v*']
pull_request:
paths:
- 'packages/solver-web/**'
- 'tools/build_solver_web.py'
- 'tests/test_solver_web.mjs'
- 'tests/test_web_dynamic.c'
- 'tests/web_yang_zhang.json'
- 'include/wang/**'
- 'src/**'
- '.github/workflows/solver-web.yml'
workflow_dispatch:

permissions:
contents: read

jobs:
build:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
persist-credentials: false
- uses: actions/setup-node@v4
with:
node-version: '24'
- name: Install the pinned Emscripten SDK outside the checkout
run: |
git clone --depth 1 --branch 4.0.23 https://github.com/emscripten-core/emsdk.git "$RUNNER_TEMP/emsdk"
"$RUNNER_TEMP/emsdk/emsdk" install 4.0.23
"$RUNNER_TEMP/emsdk/emsdk" activate 4.0.23
- name: Build versioned package and check tag
env:
REF_TYPE: ${{ github.ref_type }}
REF_NAME: ${{ github.ref_name }}
run: |
if [ "$REF_TYPE" = tag ]; then
python3 -c 'import json, os; assert os.environ["REF_NAME"] == "solver-web-v" + json.load(open("packages/solver-web/package.json"))["version"]'
python3 tools/build_solver_web.py --release --emcc "$RUNNER_TEMP/emsdk/upstream/emscripten/emcc"
else
python3 tools/build_solver_web.py --emcc "$RUNNER_TEMP/emsdk/upstream/emscripten/emcc"
fi
- name: Check both compiled engines against exhaustive enumeration
run: |
for package in build/solver-web/*/; do
node tests/test_solver_web.mjs "$package"
done
- name: Check browser engine memory safety and allocation failures
run: |
cc -Iinclude -std=c17 -Wall -Wextra -Werror -O1 -g -fsanitize=address,undefined tests/test_web_dynamic.c -o build/test_web_dynamic
build/test_web_dynamic
- name: Retain release archive briefly
uses: actions/upload-artifact@v4
with:
name: solver-web
path: |
build/solver-web/*.tar.gz
build/solver-web/*.sha256
retention-days: 1

release:
if: startsWith(github.ref, 'refs/tags/solver-web-v')
needs: build
runs-on: ubuntu-latest
permissions:
contents: write
steps:
- uses: actions/download-artifact@v4
with:
name: solver-web
path: package
- name: Publish package assets
env:
GH_TOKEN: ${{ github.token }}
GH_REPO: ${{ github.repository }}
TAG: ${{ github.ref_name }}
run: |
gh release create "$TAG" package/* --verify-tag --title "Browser solver ${TAG#solver-web-v}" --generate-notes
4 changes: 4 additions & 0 deletions Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,10 @@ serial: $(SERIAL_LIBRARY)

shared: $(SHARED_LIBRARY)

.PHONY: solver-web
solver-web:
$(PYTHON) tools/build_solver_web.py

openmp: $(OPENMP_LIBRARY)

$(SERIAL_LIBRARY): $(SERIAL_OBJECTS) | $(LIB_DIR)
Expand Down
15 changes: 15 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,12 @@ it, and checking that the different views of the instance agree.
[Evidence](https://xtraid.github.io/tiling-foundry/evidence/) ·
[Run dossiers](https://xtraid.github.io/tiling-foundry/run-dossiers/)

**[Open Wang Studio in your browser →](https://xtraid.github.io/wang-studio/)**

Build your own regions and tilesets in the independent research editor.
Both C solvers run in your browser; no download or installation is required.
Square solving is available now.

## Why this repository exists

Yang and Zhang proved in 2024 that tiling finite simply connected regions is
Expand Down Expand Up @@ -192,6 +198,15 @@ the data flow and component boundaries. The
[worked example](https://xtraid.github.io/tiling-foundry/worked-example/)
follows a SAT instance from its source formula to the checked tiling.

## Interactive research companion

[Wang Studio](https://xtraid.github.io/wang-studio/) is an independent editor
for subsequent tiling research, with its own repository and website. It consumes
the [versioned browser solver package](packages/solver-web/README.md) built here
from the reference and optimized C engines. See the
[integration notes](docs/plans/wang_studio.md). Studio is distinct from the
artifact renderer and requires no Python solver at runtime.

## Small standalone harness

[`harness_wangz3/`](harness_wangz3/) contains a small reimplementation of the
Expand Down
2 changes: 2 additions & 0 deletions docs/_includes/footer.html
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,8 @@
<p>
<a href="{{ site.repository_url }}">Source on GitHub</a>
<span aria-hidden="true">·</span>
<a href="https://xtraid.github.io/wang-studio/">Wang Studio · independent research editor</a>
<span aria-hidden="true">·</span>
<span>{{ site.time | date: "%Y" }}</span>
</p>
</div>
Expand Down
23 changes: 23 additions & 0 deletions docs/assets/css/site.css
Original file line number Diff line number Diff line change
Expand Up @@ -1307,3 +1307,26 @@ img {
color: #161819 !important;
}
}

/* Keep the browser app visible near the top of the project home. */
.studio-entry {
margin-block: 2rem;
padding: 1.25rem;
border: 1px solid var(--rule-strong);
background: var(--black-raised);
}

.studio-entry h2 { margin-top: 0; }
.studio-entry__link {
display: inline-block;
padding: 0.75rem 1rem;
border: 1px solid currentColor;
color: var(--ink-strong);
font-weight: 700;
}
.studio-entry__link:hover,
.studio-entry__link:focus-visible {
text-decoration-thickness: 0.15em;
outline: 2px solid currentColor;
outline-offset: 3px;
}
8 changes: 8 additions & 0 deletions docs/index.md
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,14 @@ description: From a CM1-in-3 formula to a region over 23 Wang tiles, checked sol
checkers validate SAT witnesses, and a PDF dossier records the run.
</p>

<aside class="studio-entry" aria-label="Online research editor">
<h2>Try Wang Studio</h2>
<p>Build your own regions and tilesets in the independent research editor.
Both C solvers run in your browser. Square solving is available now;
no download or installation is required.</p>
<a class="studio-entry__link" href="https://xtraid.github.io/wang-studio/">Open the editor in your browser →</a>
</aside>

<div class="story-actions">
<a class="text-link" href="{{ '/run-dossiers/' | relative_url }}">Run the demo</a>
<a class="text-link" href="{{ '/presentazione/' | relative_url }}">Follow the technical tour</a>
Expand Down
54 changes: 54 additions & 0 deletions docs/plans/wang_studio.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
# Wang Studio: independent research editor

Wang Studio is an independent project for the research following Tiling Foundry,
with its own repository and website. It consumes Foundry's versioned solver
package for authoring tilesets, constructing finite regions and exploring search.

The browser package is maintained under `packages/solver-web/` in Foundry and
contains the C reference and optimized engines compiled to WebAssembly. Its
documentation is the current package contract. Python/Z3 is not distributed
to the editor. The local Python connector described below remains an optional
development comparison path. Foundry's Pages link to Studio; Studio is not
hosted in the Foundry source repository.

It is distinct from `renderer/`, which produces figures from verified
Foundry artifacts. Studio owns interaction and experiments; Foundry continues
to own native propagation, search, verification and scientific pipelines.

The first local connector consumes `libwang.so` through
`wang_solve_optimized_tileset`: the **same optimized core** accepts a runtime
square tileset of 1–32 tiles with colors 0–15. It supports initial domains and
metrics. Canonical trace formats are not accepted for custom tilesets.
The existing 23-tile APIs and the Yang–Zhang pipeline remain available.

The runtime verifier is `wang_verify_tiling_with_tileset`. Both interfaces
borrow their input arrays. The result lifecycle is unchanged:
`wang_solve_result_destroy` releases returned domains.

Studio runs solves in worker processes for cancellation/deadlines, checks
solutions independently, and treats timeout as distinct from UNSAT. It does
not copy the solver implementation or use Z3 as a runtime fallback.

Current local companion checkout: `~/Projects/wang-studio`. Its README
contains startup instructions and the connector's resource limits. Native
adjacency for hexagons and triangles is future work; Studio's support for
editing those geometries does not imply that this square-grid API solves them.

## Incremental enumeration

`wang_enumerate_optimized_tileset` shares the optimized search core. Each
verified solution is passed to a borrowed-domain visitor. Returning true
continues via trail rollback; false stops. A visitor may block, retaining the
DFS stack, to implement interactive next-solution requests. Return codes are
`0` for exhaustive completion, `1` for visitor-requested stop, and `-1` for error.

Enumeration deduplicates identical edge tuples within each initial cell domain.
It disables the single-solution shortcut that arbitrarily picks one tile for an
isolated cell. The canonical decision solver and its trace formats retain their
previous behavior. The caller owns the count, so no fixed-width counter can
silently overflow inside the core.

Studio's worker counts with Python integers, publishes throttled progress
atomically, and waits for next/count commands inside the native visitor. Stop
and deadlines retain only a lower bound; exhaustive completion publishes the
exact total. Displayed solutions do not replace the original fixed constraints.
59 changes: 59 additions & 0 deletions include/wang/solver.h
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,65 @@ WangSolveStatus wang_solve_optimized(
WangSolveResult *out_result
);

/* Runtime square-grid tilesets use the same optimized search mechanisms.
* Initial integration limit: 1..32 tiles, colors 0..COLOR_COUNT-1.
* Tile position is its ID; generalized metadata is ignored. No rotations.
* Domain bit i refers to tileset[i], including bit 31 for a 32-tile set.
* Supports initial_domains and COLLECT_METRICS; canonical trace formats are
* intentionally not accepted for non-canonical tilesets. Borrowed inputs.
*/
#define WANG_RUNTIME_MAX_TILES 32u
WangSolveStatus wang_solve_optimized_tileset(
const Region *region,
const WangTile *tileset,
size_t tileset_count,
const WangSolverOptions *options,
WangSolveResult *out_result
);

/* Enumerate distinct edge-color configurations using the optimized DFS.
* The visitor receives borrowed singleton domains and returns true to continue
* or false to stop. It may block to pause without losing the search stack.
* Duplicate edge tuples are collapsed per cell, respecting initial domains.
* Return: -1 error, 0 exhaustive completion, 1 visitor-requested stop.
* The caller owns any counter (so counting is not limited to uint64_t).
* No rotations. Inputs must remain immutable until this call returns.
*/
typedef bool (*WangSolutionVisitor)(
const uint32_t *domains, size_t cell_count,
const WangSolverMetrics *metrics, void *userdata
);
int wang_enumerate_optimized_tileset(
const Region *region, const WangTile *tileset, size_t tileset_count,
const WangSolverOptions *options, WangSolutionVisitor visitor,
void *userdata, WangSolverMetrics *metrics
);

/* Same runtime enumeration contract using the reference mechanisms. */
int wang_enumerate_serial_tileset(
const Region *region, const WangTile *tileset, size_t tileset_count,
const WangSolverOptions *options, WangSolutionVisitor visitor,
void *userdata, WangSolverMetrics *metrics
);

/* Explicit reciprocal cell/side adjacency. -1 is an exterior side; otherwise
* neighbors[i * side_count + d] is the neighboring cell, and neighbor_sides
* gives its incident side. Dense edges are tile-major; boundary uses COLOR_NONE.
* Borrowed inputs, 1..6 sides, 1..4096 cells, 1..32 tiles. No rotations.
* Shares propagation, MRV, trail and DFS with square enumeration. */
#define WANG_GRAPH_MAX_SIDES 6u
typedef struct {
size_t cell_count;
size_t side_count;
const int32_t *neighbors;
const uint8_t *neighbor_sides;
const uint8_t *boundary;
const uint8_t *edges;
} WangGraph;
int wang_enumerate_graph(const WangGraph *graph, size_t tile_count,
const WangSolverOptions *options, bool reference, WangSolutionVisitor visitor,
void *userdata, WangSolverMetrics *metrics);

/* Release the owned snapshot and reset every field. Accepts NULL. */
void wang_solve_result_destroy(WangSolveResult *result);

Expand Down
6 changes: 6 additions & 0 deletions include/wang/verify.h
Original file line number Diff line number Diff line change
Expand Up @@ -28,4 +28,10 @@ WangVerifyStatus wang_verify_tiling(
size_t tile_count
);

/* Independent verification against an explicitly supplied square tileset. */
WangVerifyStatus wang_verify_tiling_with_tileset(
const Region *region, const TileId *tiles, size_t tile_count,
const WangTile *tileset, size_t tileset_count
);

#endif /* WANG_VERIFY_H */
Loading
Loading