From ceaf5e69f76661935dfe3c6f09aaae9957e59385 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa Date: Mon, 29 May 2023 01:13:59 -0400 Subject: [PATCH 1/7] Add artifact README, Szalinski script --- OOPSLA23.md | 57 +++++++++++++++++++++++++++++++++++++ scripts/oopsla23/sz-eval.sh | 26 +++++++++++++++++ 2 files changed, 83 insertions(+) create mode 100644 OOPSLA23.md create mode 100755 scripts/oopsla23/sz-eval.sh diff --git a/OOPSLA23.md b/OOPSLA23.md new file mode 100644 index 00000000..41ee2394 --- /dev/null +++ b/OOPSLA23.md @@ -0,0 +1,57 @@ +# Equality Saturation Theory Exploration à la Carte + +This is the artifact for our paper +"Equality Saturation Theory Exploration à la Carte". + + + +## Dependencies + +* Install Rust + +* Install make by typing: `sudo apt-get install make` + +* Install g++ by typing: `sudo apt-get install g++` + +* Install jq by typing: `sudo apt-get install jq` + +* Install [CGAL](https://www.cgal.org/download/linux.html) by typing + `sudo apt-get install libcgal-dev` + +* Install [OpenSCAD](https://www.openscad.org/) from `https://launchpad.net/~openscad/+archive/ubuntu/releases` + +* Install git by typing `sudo apt install git` + +* Install pip by typing `sudo apt install python3-pip` and then +install the following: +``` +pip3 install pandas +pip3 install "jinja2>=3" +``` + +## Step-by-step + +Our paper has TODO quantitative evaluations: + +1. Synthesizing Szalinski's CAD identities (`Section 6.2.2`): We show that Ruler can infer CAD identities for Szalinski that closely match the pre-existing hand-written rules. + +2. TODO: add other evals. + +## 1. Synthesizing Szalinski's CAD identities (Table 4). + +First, clone our evaluation branch of Szalinski within the top-level directory of this repository. + +``` +git clone --branch eval https://github.com/rtjoa/szalinski +``` + +To show the results of a preexisting run, run the following from the `szalinski` repository. Table 4 should be printed to output. +``` +./to_latex.py +``` + +To regenerate Table 4 from scratch, run the following from the `ruler` repository. It should finish within 30 minutes. +``` +scripts/oopsla23/sz-eval.sh +``` + diff --git a/scripts/oopsla23/sz-eval.sh b/scripts/oopsla23/sz-eval.sh new file mode 100755 index 00000000..a759a268 --- /dev/null +++ b/scripts/oopsla23/sz-eval.sh @@ -0,0 +1,26 @@ +#!/usr/bin/env bash + +# Synthesize rules +cargo test --package ruler --test szalinski -- --ignored --nocapture > szalinski/rules.txt + +# Check rule synthesis +if ! test -f szalinski/rules.txt; then + echo "szalinski/rules.txt not found. Did rule inference not run?" + exit 1 +fi + +if ! grep -q "RULER RULES START" szalinski/rules.txt; then + echo "Rule inference had malformed output!" + exit 1 +fi + +cd szalinski + +# Copy synthesized rules +python3 copy-rules.py + +# Run Szalinski eval +make -B out/aec-table2/table2.csv + +# Print results +python3 to_latex.py From 078ebf8f138dacb3740762a299df86884ba621dc Mon Sep 17 00:00:00 2001 From: Ryan Tjoa <51928404+rtjoa@users.noreply.github.com> Date: Mon, 29 May 2023 01:21:36 -0400 Subject: [PATCH 2/7] Update OOPSLA23.md --- OOPSLA23.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/OOPSLA23.md b/OOPSLA23.md index 41ee2394..dcfae00d 100644 --- a/OOPSLA23.md +++ b/OOPSLA23.md @@ -18,7 +18,7 @@ This is the artifact for our paper * Install [CGAL](https://www.cgal.org/download/linux.html) by typing `sudo apt-get install libcgal-dev` -* Install [OpenSCAD](https://www.openscad.org/) from `https://launchpad.net/~openscad/+archive/ubuntu/releases` +* Install [OpenSCAD](https://www.openscad.org/) from [https://launchpad.net/~openscad/+archive/ubuntu/releases](https://launchpad.net/~openscad/+archive/ubuntu/releases) * Install git by typing `sudo apt install git` @@ -52,6 +52,6 @@ To show the results of a preexisting run, run the following from the `szalinski` To regenerate Table 4 from scratch, run the following from the `ruler` repository. It should finish within 30 minutes. ``` -scripts/oopsla23/sz-eval.sh +./scripts/oopsla23/sz-eval.sh ``` From e3ccecca60278a384e71c669429c5e834cd5ae89 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa <51928404+rtjoa@users.noreply.github.com> Date: Mon, 29 May 2023 01:22:16 -0400 Subject: [PATCH 3/7] Update OOPSLA23.md --- OOPSLA23.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/OOPSLA23.md b/OOPSLA23.md index dcfae00d..577e0167 100644 --- a/OOPSLA23.md +++ b/OOPSLA23.md @@ -20,8 +20,6 @@ This is the artifact for our paper * Install [OpenSCAD](https://www.openscad.org/) from [https://launchpad.net/~openscad/+archive/ubuntu/releases](https://launchpad.net/~openscad/+archive/ubuntu/releases) -* Install git by typing `sudo apt install git` - * Install pip by typing `sudo apt install python3-pip` and then install the following: ``` From 52bf4fc2c019290dab8efba3242da1c1c1501f12 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa <51928404+rtjoa@users.noreply.github.com> Date: Mon, 29 May 2023 01:23:45 -0400 Subject: [PATCH 4/7] Update OOPSLA23.md --- OOPSLA23.md | 30 ++++++++++++++---------------- 1 file changed, 14 insertions(+), 16 deletions(-) diff --git a/OOPSLA23.md b/OOPSLA23.md index 577e0167..4bedbaa9 100644 --- a/OOPSLA23.md +++ b/OOPSLA23.md @@ -13,20 +13,6 @@ This is the artifact for our paper * Install g++ by typing: `sudo apt-get install g++` -* Install jq by typing: `sudo apt-get install jq` - -* Install [CGAL](https://www.cgal.org/download/linux.html) by typing - `sudo apt-get install libcgal-dev` - -* Install [OpenSCAD](https://www.openscad.org/) from [https://launchpad.net/~openscad/+archive/ubuntu/releases](https://launchpad.net/~openscad/+archive/ubuntu/releases) - -* Install pip by typing `sudo apt install python3-pip` and then -install the following: -``` -pip3 install pandas -pip3 install "jinja2>=3" -``` - ## Step-by-step Our paper has TODO quantitative evaluations: @@ -48,8 +34,20 @@ To show the results of a preexisting run, run the following from the `szalinski` ./to_latex.py ``` -To regenerate Table 4 from scratch, run the following from the `ruler` repository. It should finish within 30 minutes. +To regenerate Table 4 from scratch, the Szalinski tool will have to be run end-to-end, which involves the following extra dependencies: + +* Install jq by typing: `sudo apt-get install jq` + +* Install [CGAL](https://www.cgal.org/download/linux.html) by typing + `sudo apt-get install libcgal-dev` + +* Install [OpenSCAD](https://www.openscad.org/) from [https://launchpad.net/~openscad/+archive/ubuntu/releases](https://launchpad.net/~openscad/+archive/ubuntu/releases) + +* Install pip by typing `sudo apt install python3-pip` and then +install the following: +`pip3 install pandas && pip3 install "jinja2>=3"` + +Now, run the following from the `ruler` repository. It should finish within 30 minutes. ``` ./scripts/oopsla23/sz-eval.sh ``` - From af861ffee3100084b25f1e14be7e0f5541d7ba94 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa <51928404+rtjoa@users.noreply.github.com> Date: Mon, 29 May 2023 01:24:15 -0400 Subject: [PATCH 5/7] Update OOPSLA23.md --- OOPSLA23.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/OOPSLA23.md b/OOPSLA23.md index 4bedbaa9..6c969818 100644 --- a/OOPSLA23.md +++ b/OOPSLA23.md @@ -13,6 +13,10 @@ This is the artifact for our paper * Install g++ by typing: `sudo apt-get install g++` +* Install pip by typing `sudo apt install python3-pip` and then +install the following: +`pip3 install pandas && pip3 install "jinja2>=3"` + ## Step-by-step Our paper has TODO quantitative evaluations: @@ -43,10 +47,6 @@ To regenerate Table 4 from scratch, the Szalinski tool will have to be run end-t * Install [OpenSCAD](https://www.openscad.org/) from [https://launchpad.net/~openscad/+archive/ubuntu/releases](https://launchpad.net/~openscad/+archive/ubuntu/releases) -* Install pip by typing `sudo apt install python3-pip` and then -install the following: -`pip3 install pandas && pip3 install "jinja2>=3"` - Now, run the following from the `ruler` repository. It should finish within 30 minutes. ``` ./scripts/oopsla23/sz-eval.sh From efbbddc4de7e51d30186210d99460028d7790846 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa <51928404+rtjoa@users.noreply.github.com> Date: Mon, 29 May 2023 01:24:43 -0400 Subject: [PATCH 6/7] Update OOPSLA23.md --- OOPSLA23.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/OOPSLA23.md b/OOPSLA23.md index 6c969818..ffb956f4 100644 --- a/OOPSLA23.md +++ b/OOPSLA23.md @@ -47,7 +47,7 @@ To regenerate Table 4 from scratch, the Szalinski tool will have to be run end-t * Install [OpenSCAD](https://www.openscad.org/) from [https://launchpad.net/~openscad/+archive/ubuntu/releases](https://launchpad.net/~openscad/+archive/ubuntu/releases) -Now, run the following from the `ruler` repository. It should finish within 30 minutes. +Now, run the following from the `ruler` repository. It should finish within 30 minutes and print Table 4. ``` ./scripts/oopsla23/sz-eval.sh ``` From 01d4831352dfc2b7c7bf905ea952595d4e191c62 Mon Sep 17 00:00:00 2001 From: Ryan Tjoa <51928404+rtjoa@users.noreply.github.com> Date: Mon, 29 May 2023 01:26:30 -0400 Subject: [PATCH 7/7] Update OOPSLA23.md --- OOPSLA23.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/OOPSLA23.md b/OOPSLA23.md index ffb956f4..8ccc7b37 100644 --- a/OOPSLA23.md +++ b/OOPSLA23.md @@ -38,7 +38,7 @@ To show the results of a preexisting run, run the following from the `szalinski` ./to_latex.py ``` -To regenerate Table 4 from scratch, the Szalinski tool will have to be run end-to-end, which involves the following extra dependencies: +To regenerate Table 4 from scratch, Szalinski will have to be run end-to-end, which involves the following extra dependencies: * Install jq by typing: `sudo apt-get install jq`