Add support for calling LLM to generate workloads and rulesets

.gitignore

@@ -6,6 +6,7 @@
 /nightly
 /*.terms
 /*.rules
+.env
 
 # Scripts
 scripts/ablation/output/*
@@ -34,3 +35,5 @@ out/
 # Exceptions
 !scripts/oopsla21/ablation/submitted-plots/**/*.pdf
 !scripts/oopsla21/ablation/submitted-plots/**/*.json
+
+stash

Cargo.toml

@@ -5,6 +5,9 @@ authors = ["Max Willsey <me@mwillsey.com>", "Chandrakana Nandi <cnandi@cs.washin
 edition = "2018"
 
 [dependencies]
+dotenv = "0.15"
+openai-api-rs = "6.0.3"
+tokio = { version = "1", features = ["full"] }
 clap = { version = "3.0.7", features = ["derive"] }
 log = "0.4"
 env_logger = { version = "0.7", default-features = false }
@@ -25,8 +28,10 @@ itertools = "0.9.0"
 z3 = {version = "0.10.0", features = ["static-link-z3"]}
 rustc-hash = "1"
 symbolic_expressions = "5"
-rayon = "1"
+rayon = "1.10"
+indicatif = "0.17"
 smallstr = "0.3"
+glob = "0.3"
 [dependencies.egg]
 version = "0.9"
 # git = "https://github.com/egraphs-good/egg"

baseline/enumo_trig.rules

@@ -0,0 +1,29 @@
+(sin (/ PI 4)) <=> (cos (/ PI 4))
+(sin (/ PI 2)) <=> (cos 0)
+(cos 0) <=> (tan (/ PI 4))
+(cos (* PI 2)) <=> (cos 0)
+(cos (/ PI 2)) <=> (tan PI)
+(tan (* PI 2)) <=> (tan PI)
+(sin PI) <=> (sin (* PI 2))
+(sin 0) <=> (sin PI)
+(tan 0) <=> (tan PI)
+0 <=> (tan PI)
+(sin PI) <=> (tan PI)
+(~ (cos ?a)) <=> (cos (- PI ?a))
+(sin (- PI ?a)) <=> (sin ?a)
+(tan ?a) <=> (tan (+ PI ?a))
+(~ (sin ?a)) <=> (sin (~ ?a))
+(tan (~ ?a)) <=> (~ (tan ?a))
+(cos (~ ?a)) <=> (cos ?a)
+(+ (* (sin ?a) (sin ?a)) (* (cos ?a) (cos ?a))) ==> (cos 0)
+(- (* (cos ?b) (cos ?b)) (* (cos ?a) (cos ?a))) <=> (- (* (sin ?a) (sin ?a)) (* (sin ?b) (sin ?b)))
+(- (* (sin ?b) (sin ?b)) (* (cos ?a) (cos ?a))) <=> (- (* (sin ?a) (sin ?a)) (* (cos ?b) (cos ?b)))
+(cos (- (/ PI 2) ?a)) <=> (sin ?a)
+(/ (- 1 (cos (* 2 ?a))) 2) <=> (* (sin ?a) (sin ?a))
+(/ (+ 1 (cos (* 2 ?a))) 2) <=> (* (cos ?a) (cos ?a))
+(- ?a ?a) <=> (~ (- ?a ?a))
+(* (sin ?b) (sin ?a)) <=> (/ (- (cos (- ?b ?a)) (cos (+ ?b ?a))) 2)
+(* (cos ?b) (cos ?a)) <=> (/ (+ (cos (+ ?b ?a)) (cos (- ?b ?a))) 2)
+(+ ?b ?a) ==> (+ ?a ?b)
+(- (* (cos ?b) (cos ?a)) (* (sin ?b) (sin ?a))) <=> (cos (+ ?b ?a))
+(sin (+ ?b ?a)) <=> (+ (* (sin ?b) (cos ?a)) (* (sin ?a) (cos ?b)))

infra/localnightly.sh

@@ -0,0 +1,31 @@
+#!/bin/bash
+# The primary purpose of this script is to run all the tests and upload 
+# the results to the nightly-results server. It also generates some HTML
+# to display the equiderivability tests in a nicely-formatted way.
+
+echo "Beginning Ruler nightly script..."
+
+# exit immediately upon first error
+set -e
+
+# determine physical directory of this script
+src="${BASH_SOURCE[0]}"
+while [ -L "$src" ]; do
+  dir="$(cd -P "$(dirname "$src")" && pwd)"
+  src="$(readlink "$src")"
+  [[ $src != /* ]] && src="$dir/$src"
+done
+MYDIR="$(cd -P "$(dirname "$src")" && pwd)"
+
+RESOURCES_DIR="$MYDIR/nightly-resources"
+NIGHTLY_DIR="$MYDIR/../nightly"
+OUTPUT_DIR="$NIGHTLY_DIR/output"
+
+rm -rf "$OUTPUT_DIR"
+mkdir -p "$OUTPUT_DIR"
+mkdir -p "$OUTPUT_DIR/data"
+
+cp $RESOURCES_DIR/* "$OUTPUT_DIR"
+(echo "var data = "; cat $NIGHTLY_DIR/data/output.json) > $OUTPUT_DIR/data/output.js
+
+cd $OUTPUT_DIR && python3 -m http.server 8002

infra/nightly-resources/data.js

@@ -56,11 +56,11 @@ function getBaseline(name) {
     "Enumo LOC": (row) => row.loc,
     "# Enumo": (row) => row.rules.length,
     "Time (s)": (row) => row.time,
-    "Enumo Derives Baseline (LHS / LHSRHS)": (row) =>
+    "X Derives Baseline (LHS / LHSRHS)": (row) =>
       `${getDerivability(
         row.derivability.enumo_derives_baseline.lhs
       )} / ${getDerivability(row.derivability.enumo_derives_baseline.lhs_rhs)}`,
-    "Enumo derives Baseline Time (s)": (row) => {
+    "X derives Baseline Time (s)": (row) => {
       if (missingDerivability(row.derivability.enumo_derives_baseline)) {
         return "-";
       } else {
@@ -73,11 +73,11 @@ function getBaseline(name) {
         )}`;
       }
     },
-    "Baseline Derives Enumo (LHS / LHSRHS)": (row) =>
+    "Baseline Derives X (LHS / LHSRHS)": (row) =>
       `${getDerivability(
         row.derivability.baseline_derives_enumo.lhs
       )} / ${getDerivability(row.derivability.baseline_derives_enumo.lhs_rhs)}`,
-    "Baseline derives Enumo Time (s)": (row) => {
+    "Baseline derives X Time (s)": (row) => {
       if (missingDerivability(row.derivability.baseline_derives_enumo)) {
         return "-";
       } else {

infra/nightly-resources/index.html

@@ -15,6 +15,9 @@
 
 <body onload="load()">
   <h2>Nightlies</h2>
+  <div>
+    <div class="table" id="enumo_table"></div>
+  </div>
   <div>
     <div class="table" id="baseline_table"></div>
   </div>

infra/nightly-resources/index.js

@@ -2,6 +2,10 @@
 // Populates the oopsla, herbie, and halide tables with data from the
 // global data object
 function load() {
+  document.getElementById("enumo_table").innerHTML = ConvertJsonToTable(
+    getBaseline("enumo")
+  );
+
   document.getElementById("baseline_table").innerHTML = ConvertJsonToTable(
     getBaseline("oopsla")
   );
@@ -66,16 +70,16 @@ function loadDeriveDetail() {
 
     let tableData = [
       {
-        "Enumo->Baseline (derivable)": formatRules(
+        "X->Baseline (derivable)": formatRules(
           derivability.enumo_derives_baseline[deriveType]?.can
         ),
-        "Enumo->Baseline (not derivable)": formatRules(
+        "X->Baseline (not derivable)": formatRules(
           derivability.enumo_derives_baseline[deriveType]?.cannot
         ),
-        "Baseline->Enumo (derivable)": formatRules(
+        "Baseline->X (derivable)": formatRules(
           derivability.baseline_derives_enumo[deriveType]?.can
         ),
-        "Baseline->Enumo (not derivable)": formatRules(
+        "Baseline->X (not derivable)": formatRules(
           derivability.baseline_derives_enumo[deriveType]?.cannot
         ),
       },