add rules file

Author: doyougnu

EMSE2021/README.md

@@ -12,10 +12,10 @@
     - the `*.nix` files in the `nix` directory, pin the development environment
       used in the benchmarks and analysis to specific commits of `nixpkgs` which
       are dated for the time of publication. This allows researchers to create a
-      development environment identical to the one used in this paper for both
-      the `vsat` tool and for the statistics scripts, in a `nix-shell`; Use `>
-      nix-shell R.nix` for the `R` environment. To reproduce the haskell
-      environment we rely on the `stack` built tool
+      development environment identical to the one used in this paper for the
+      statistics scripts, in a `nix-shell`; Use `> nix-shell R.nix` for the `R`
+      environment. To reproduce the haskell environment we rely on the `stack`
+      build tool.
     - We provide the source code R scripts used in our evaluation in the
       `statisticsScripts` directory. The scripts are heavily commented.
     - The vsat tool can be built using either `cabal`, `stack`. Both allow a
@@ -24,11 +24,20 @@
       recommend `stack` for most cases because it pins the package set to a
       specific package set, whereas `cabal` uses the package set present on the
       user's computer.
+    - We also provide a small haskell implementation of the inference rules in
+      the `rules/VSAT.hs` file. If you are looking to build your own variational
+      solver, and want to learn the inference rules, this would be the simplest
+      place to start because it is just a pure, functional model, i.e., it
+      doesn't actually solve anything it just uses haskell's type system to show
+      the rules are sound. Once you are comfortable, you can view the rest of
+      the architecture in the `vsat` repo linked above.
 
 
 ### The Vsat tool
 You can find the version of Vsat for this paper
-[here](https://github.com/doyougnu/VSat). To run the tool:
+[here](https://github.com/doyougnu/VSat) and archived here:
+[![DOI](https://zenodo.org/badge/105307042.svg)](https://zenodo.org/badge/latestdoi/105307042)
+. To run the tool:
 1. Clone the repository, i.e., `git clone https://github.com/doyougnu/VSat`
 2. If you are using `nix` un-comment the following in `stack.yaml`:
    ```

EMSE2021/rules/VSAT.hs

@@ -0,0 +1,107 @@
+module VSAT where
+
+import Prelude hiding (and,or)
+
+
+type Dim = String
+type Var = String
+
+data Op = And | Or
+  deriving (Eq,Show)
+
+data Exp
+   = Sym
+   | Unit
+   | Ref Var
+   | Not Exp
+   | Bin Op Exp Exp
+   | Chc Dim Exp Exp
+  deriving Eq
+
+instance Show Exp where
+  show Sym     = "s"
+  show Unit    = "o"
+  show (Ref x) = x
+  show (Chc d l r)   = concat [d, "<", show l, ",", show r, ">"]
+  show (Bin Or l r)  = show l ++ " | " ++ show r
+  show (Bin And l r) = help l ++ " & " ++ help r
+    where
+      help e@(Bin Or _ _) = "(" ++ show e ++ ")"
+      help e              = show e
+
+and  = Bin And
+or   = Bin Or
+a    = Ref "a"
+b    = Ref "b"
+c    = Ref "c"
+chc  = Chc "D"
+chc' = Chc "D'"
+
+
+-- | Structure of accumulation.
+acc :: Exp -> Exp
+acc (Ref _)     = Sym
+acc (Not e)     = case acc e of
+    Sym -> Sym
+    e'  -> Not e'
+acc (Bin o l r) = case (acc l, acc r) of
+    (Sym, Sym) -> Sym
+    (l', r')   -> Bin o l' r'
+acc e = e
+
+-- | Structure of evaluation.
+eval :: Exp -> Exp
+eval Sym           = Unit
+eval (Bin And l r) = case (eval l, eval r) of
+    (Unit, r') -> r'
+    (l', Unit) -> l'
+    (l', r')   -> Bin And l' r'
+eval e = let e' = acc e
+         in if e == e' then e' else eval e'
+
+
+data Ctx = InL Op Exp Ctx
+         | InR Op Ctx -- there's a Sym in here!
+         | InN Ctx    -- there's a Sym in here!
+         | Top
+
+type Cfg = [(Dim,Bool)]
+
+-- | Structure of choice removal.
+cr :: Cfg -> Ctx -> Exp -> (Exp,Int)
+
+cr c Top Sym = (eval Sym,1)
+
+cr c (InL o r z) Sym = cr c (InR o z) r
+cr c (InR o z)   Sym = let s = acc (Bin o Sym Sym)
+                       in cr c z s
+
+cr c (InN z)     Sym = let s = acc (Not Sym)
+                       in cr c z s
+
+-- recursive cases
+cr c z (Not e)       = cr c (InN z) e
+
+cr c z (Bin And l r) = cr c (InL And r z) l
+cr c z (Bin Or  l r) = cr c (InL Or  r z) l
+
+cr c z (Chc d l r)   = case lookup d c of
+    Just True  -> cr c z l
+    Just False -> cr c z r
+    Nothing    -> let (Unit,i) = cr ((d,True):c) z l
+                      (Unit,j) = cr ((d,False):c) z r
+                  in (Unit,i+j)
+
+cr c z e = let e' = acc e
+           in if e == e' then error "boom" else cr c z e'
+
+
+-- Examples from accumulation section.
+ex1 = or a (and a b)
+ex2 = or ex1 (and (chc a (and a b)) ex1)
+
+
+-- Example from evaluation section.
+ex3 = and (or a b) (chc a c)
+
+ex4 = and (chc' a c) (or a b)