Create pretty documentation.

.gitignore

@@ -46,3 +46,6 @@ target/
 /src/main/resources/codegen/build/
 
 .idea/
+
+# Jekyll
+_site/

docs/Gemfile

@@ -0,0 +1,7 @@
+source 'https://rubygems.org'
+
+gem "jekyll", "~> 4.3.4" # installed by `gem jekyll`
+# gem "webrick"        # required when using Ruby >= 3 and Jekyll <= 4.2.2
+
+gem "just-the-docs", "0.10.0" # pinned to the current release
+# gem "just-the-docs"        # always download the latest release

docs/Gemfile.lock

@@ -0,0 +1,91 @@
+GEM
+  remote: https://rubygems.org/
+  specs:
+    addressable (2.8.7)
+      public_suffix (>= 2.0.2, < 7.0)
+    bigdecimal (3.1.8)
+    colorator (1.1.0)
+    concurrent-ruby (1.3.4)
+    em-websocket (0.5.3)
+      eventmachine (>= 0.12.9)
+      http_parser.rb (~> 0)
+    eventmachine (1.2.7)
+    ffi (1.17.0-arm64-darwin)
+    ffi (1.17.0-x86_64-linux-gnu)
+    forwardable-extended (2.6.0)
+    google-protobuf (4.28.1-arm64-darwin)
+      bigdecimal
+      rake (>= 13)
+    google-protobuf (4.28.1-x86_64-linux)
+      bigdecimal
+      rake (>= 13)
+    http_parser.rb (0.8.0)
+    i18n (1.14.6)
+      concurrent-ruby (~> 1.0)
+    jekyll (4.3.4)
+      addressable (~> 2.4)
+      colorator (~> 1.0)
+      em-websocket (~> 0.5)
+      i18n (~> 1.0)
+      jekyll-sass-converter (>= 2.0, < 4.0)
+      jekyll-watch (~> 2.0)
+      kramdown (~> 2.3, >= 2.3.1)
+      kramdown-parser-gfm (~> 1.0)
+      liquid (~> 4.0)
+      mercenary (>= 0.3.6, < 0.5)
+      pathutil (~> 0.9)
+      rouge (>= 3.0, < 5.0)
+      safe_yaml (~> 1.0)
+      terminal-table (>= 1.8, < 4.0)
+      webrick (~> 1.7)
+    jekyll-include-cache (0.2.1)
+      jekyll (>= 3.7, < 5.0)
+    jekyll-sass-converter (3.0.0)
+      sass-embedded (~> 1.54)
+    jekyll-seo-tag (2.8.0)
+      jekyll (>= 3.8, < 5.0)
+    jekyll-watch (2.2.1)
+      listen (~> 3.0)
+    just-the-docs (0.10.0)
+      jekyll (>= 3.8.5)
+      jekyll-include-cache
+      jekyll-seo-tag (>= 2.0)
+      rake (>= 12.3.1)
+    kramdown (2.4.0)
+      rexml
+    kramdown-parser-gfm (1.1.0)
+      kramdown (~> 2.0)
+    liquid (4.0.4)
+    listen (3.9.0)
+      rb-fsevent (~> 0.10, >= 0.10.3)
+      rb-inotify (~> 0.9, >= 0.9.10)
+    mercenary (0.4.0)
+    pathutil (0.16.2)
+      forwardable-extended (~> 2.6)
+    public_suffix (6.0.1)
+    rake (13.2.1)
+    rb-fsevent (0.11.2)
+    rb-inotify (0.11.1)
+      ffi (~> 1.0)
+    rexml (3.3.7)
+    rouge (4.3.0)
+    safe_yaml (1.0.5)
+    sass-embedded (1.78.0-arm64-darwin)
+      google-protobuf (~> 4.27)
+    sass-embedded (1.78.0-x86_64-linux-gnu)
+      google-protobuf (~> 4.27)
+    terminal-table (3.0.2)
+      unicode-display_width (>= 1.1.1, < 3)
+    unicode-display_width (2.6.0)
+    webrick (1.8.1)
+
+PLATFORMS
+  arm64-darwin
+  x86_64-linux-gnu
+
+DEPENDENCIES
+  jekyll (~> 4.3.4)
+  just-the-docs (= 0.10.0)
+
+BUNDLED WITH
+   2.5.9

docs/_config.yml

@@ -0,0 +1,8 @@
+title: Formulog 
+description: Datalog for SMT-based static analysis 
+theme: just-the-docs
+
+url: https://just-the-docs.github.io
+
+aux_links:
+  GitHub Repository: https://github.com/HarvardPL/formulog

docs/eval_modes/compile.md

@@ -0,0 +1,54 @@
+---
+title: Compilation
+layout: page
+parent: Evaluation Modes
+nav_order: 3
+---
+
+# Compilation
+
+As an alternative to being directly interpreted (the default), Formulog programs can be compiled into a mix of C++ and Souffle code, which can then in turn be compiled into an efficient executable.
+To enable compilation, set the `--codegen` (`-c`) flag; generated code will be placed in the directory `./codegen/` (you can change this using the `--codegen-dir` option).
+Within this directory you can use `cmake` to compile the generated code into a binary named `flg`.
+
+For example, to compile and execute the `greeting.flg` program from above, you can use these steps:
+
+```
+java -jar formulog.jar -c greeting.flg && \
+  cd codegen && \
+  cmake -B build -S . && \
+  cmake --build build -j && \
+  ./build/flg --dump-idb
+```
+
+This should produce output like the following:
+
+```
+Parsing...
+Finished parsing (0.000s)
+Evaluating...
+Finished evaluating (0.029s)
+
+==================== SELECTED IDB RELATIONS ====================
+
+---------- greeting (3) ----------
+greeting("Hello, Bob")
+greeting("Hello, World")
+greeting("Hello, Alice")
+```
+
+Use the command `./build/flg -h` see options available when running the executable.
+
+For more information about the Formulog compiler, see the OOPSLA'24 paper [Making Formulog Fast: An Argument for Unconventional Datalog Evaluation](https://dl.acm.org/doi/10.1145/3689754) by Aaron Bembenek, Michael Greenberg, and Stephen Chong.
+
+## Dependencies
+
+To build the generated code, you must have:
+
+- A C++ compiler that supports the C++17 standard (and OpenMP, if you want to produce a parallelized binary)
+- `cmake` (v3.21+)
+- [`boost`](https://www.boost.org/) (a version compatible with v1.81)
+- [`oneTBB`](https://oneapi-src.github.io/oneTBB/) (v2021.8.0 is known to work)
+- [`souffle`](https://souffle-lang.github.io/) (v2.3 is known to work; you have to use our [custom fork](https://github.com/aaronbembenek/souffle) if you want to combine compilation with [eager evaluation]({{ site.base_url }}{% link eval_modes/eager.md %}).)
+
+The Formulog Docker image already has these dependencies installed.

docs/eval_modes/eager.md

@@ -0,0 +1,26 @@
+---
+title: Eager Evaluation
+layout: page
+parent: Evaluation Modes
+nav_order: 4
+---
+
+# Eager Evaluation
+
+In addition to traditional semi-naive Datalog evaluation, Formulog supports _eager evaluation_, a novel concurrent evaluation algorithm for Datalog that is faster than semi-naive evaluation on some Formulog workloads (often because it induces a more favorable distribution of the SMT workload across SMT solvers).
+Whereas semi-naive evaluation batches derived tuples to process them in explicit rounds, eager evaluation eagerly pursues the consequences of each tuple as it is derived.
+
+Using eager evaluation with the Formulog interpreter is easy: just add the `--eager-eval` flag.
+Eager evaluation can also be used with the Formulog compiler, provided you install [our custom version of Souffle](https://github.com/aaronbembenek/souffle).
+When you configure `cmake` on the generated code, you need to add `-DFLG_EAGER_EVAL=On`.
+For example, to build a version of the greeting program that uses eager evaluation, use these commands:
+
+```
+java -jar formulog.jar -c greeting.flg && \
+  cd codegen && \
+  cmake -B build -S . -DFLG_EAGER_EVAL=On && \
+  cmake --build build -j && \
+  ./build/flg --dump-idb
+```
+
+For more information about eager evaluation, see the OOPSLA'24 paper [Making Formulog Fast: An Argument for Unconventional Datalog Evaluation](https://dl.acm.org/doi/10.1145/3689754) by Aaron Bembenek, Michael Greenberg, and Stephen Chong.

docs/eval_modes/index.md

@@ -0,0 +1,10 @@
+---
+title: Evaluation Modes
+layout: page
+nav_order: 4
+---
+
+# Evaluation Modes
+
+Given a Formulog program, there are many different ways to evaluate it.
+These pages describe the primary options supported by our current implementation of Formulog.

docs/eval_modes/options.md

@@ -0,0 +1,98 @@
+---
+title: Options and System Properties 
+layout: page
+parent: Evaluation Modes
+nav_order: 1
+---
+
+# Options and System Properties 
+
+Formulog evaluation is controlled by options and system properties.
+For example, to interpret the test program with SMT debug information (the `debugSmt` property) and 2
+threads (the `-j 2` option), use
+
+```
+java -DdebugSmt -jar formulog.jar greeting.flg -j 2
+```
+
+## Options
+
+Run Formulog with the `-h` flag to see a list of the command-line options that are currently available.
+As of Formulog v0.8.0, they are:
+
+```
+Usage: formulog [-chV] [--dump-all] [--dump-idb] [--dump-query] [--dump-sizes]
+                [--eager-eval] [--smt-stats] [--codegen-dir=<codegenDir>]
+                [-D=<outDir>] [-j=<parallelism>]
+                [--smt-solver-mode=<smtStrategy>]
+                [--dump=<relationsToPrint>]... [-F=<factDirs>]... <file>
+Runs Formulog.
+      <file>         Formulog program file.
+  -c, --codegen      Compile the Formulog program.
+      --codegen-dir=<codegenDir>
+                     Directory for generated code (default: './codegen').
+  -D, --output-dir=<outDir>
+                     Directory for .tsv output files (default: '.').
+      --dump=<relationsToPrint>
+                     Print selected relations.
+      --dump-all     Print all relations.
+      --dump-idb     Print all IDB relations.
+      --dump-query   Print query result.
+      --dump-sizes   Print relation sizes.
+      --eager-eval   Use eager evaluation (instead of traditional semi-naive
+                       Datalog evaluation)
+  -F, --fact-dir=<factDirs>
+                     Directory to look for fact .tsv files (default: '.').
+  -h, --help         Show this help message and exit.
+  -j, --parallelism=<parallelism>
+                     Number of threads to use.
+      --smt-solver-mode=<smtStrategy>
+                     Strategy to use when interacting with external SMT solvers
+                       ('naive', 'push-pop', or 'check-sat-assuming').
+      --smt-stats    Report basic statistics related to SMT solver usage.
+  -V, --version      Print version information and exit.
+```
+
+**Note:** Formulog does not print any results by default; use one of the
+`--dump*` options to print results to the console, or annotate intensional
+database (IDB) relations with `@disk` to dump them to disk.
+
+## System Properties
+
+In addition to options, there are many system properties that can be set using
+the `-D` flag (as in `-DdebugSmt` or `-DuseDemandTransformation=false`). Some of
+the most useful ones are:
+
+* `debugSmt` - log debugging information related to SMT calls to
+  the `solver_logs/` directory (defaults to false)
+* `debugMst` - print debugging information related to the magic set
+  transformation (defaults to false)
+* `debugRounds` - print statistics for each round of seminaive evaluation
+  (defaults to false)
+* `useDemandTransformation` - apply the demand transformation as a
+  post-processing step after the magic set transformation (defaults to true)
+* `softExceptions` - ignore exceptions during evaluation (i.e., treat them as
+  unification failures, and not as something that should stop evaluation;
+  defaults to false)
+* `sequential` - run interpreter without a thread pool (helpful for debugging
+  runtime; defaults to false)
+* `printRelSizes` - print final relation sizes (defaults to false)
+* `printFinalRules` - print the final, transformed rules (defaults to false)
+* `trackedRelations=REL_1,...,REL_n` - print facts from listed relations as they
+  are derived (defaults to the empty list)
+* `smtLogic=LOGIC` - set the logic used by the external SMT solver (defaults to
+  `ALL`)
+* `smtSolver=SOLVER` - set the external SMT solver to use; current options are
+  `z3` (default), `cvc4`, `yices`, and `boolector`
+* `smtDeclareAdts` - whether to declare Formulog algebraic data types to the SMT
+  solver upon initialization; set this to false for logics that do not support
+  ADTs (defaults to true)
+
+### Alternative SMT Solvers
+
+While we have primarily used Formulog with Z3 as the backend solver, we also
+have some experimental (not recently tested) support for other solvers; not all
+these solvers handle the full range of Formulog features. To use a solver
+besides Z3, you need to set the `smtSolver` system property (see above).  For
+each solver, the relevant binary needs to be on your path: `z3` for Z3,
+`boolector` for Boolector, `cvc4` for CVC4, and `yices-smt2` for Yices.

docs/eval_modes/smt.md

@@ -0,0 +1,34 @@
+---
+title: Solver Modes and Incremental SMT Solving
+layout: page
+parent: Evaluation Modes
+nav_order: 2
+---
+
+# Solver Modes and Incremental SMT Solving
+
+The Formulog runtime associates one external SMT solver process per Formulog
+worker thread. Each SMT query is a list of conjuncts. If the SMT solver is
+invoked via the `is_sat_opt` or `get_model_opt` function, this list is
+explicitly given by the programmer; otherwise, if the solver is invoked via the
+`is_sat` or `is_valid` function, the Formulog runtime breaks the supplied
+proposition into conjuncts.
+
+Formulog supports three strategies for interacting with external SMT solvers;
+they can be set using the `--smt-solver-mode` option.  Consider two SMT queries
+`x` and `y`, where `x` immediately precedes `y` and both are lists of conjuncts.
+
+- `naive`: reset the solver between queries `x` and `y` (do not use incremental
+SMT solving).
+- `push-pop`: try to use incremental SMT solving via the `push` and `pop` SMT
+commands. This can work well when query `y` extends query `x`; e.g., `y = c ::
+x`, where `c` is an additional conjunct; this situation most commonly occurs
+when using [eager evaluation]({{ site.baseurl }}{% link eval_modes/eager.md %}).
+- `check-sat-assuming`: try to use incremental SMT solving via the
+`check-sat-assuming` SMT command. This caches conjuncts in the SMT solver in a
+way such that they can be enabled or disabled per SMT query, and works well if
+there are shared conjuncts between queries `x` and `y`, but query `x` is not
+simply an extension of query `y` (e.g., it omits a conjunct in query `y`).
+
+For more info, see the ICLP'20 extended abstract [Datalog-Based Systems Can Use Incremental SMT Solving](https://aaronbembenek.github.io/papers/datalog-incr-smt-iclp2020.pdf)
+by Aaron Bembenek, Michael Ballantyne, Michael Greenberg, and Nada Amin.

docs/index.md

@@ -0,0 +1,13 @@
+---
+title: Home
+layout: home
+nav_order: 1
+---
+
+# Welcome to Formulog!
+
+Formulog is a programming language that extends the logic programming language Datalog with SMT solving and first-order functional programming.
+Formulog was designed to be a domain-specific language for implementing SMT-based program analyses, like refinement type checking and symbolic execution.
+But who knows---maybe it will also have other uses!
+
+Questions? Feedback? Please [raise a GitHub issue](https://github.com/HarvardPL/formulog/issues/new)!