Merge pull request #60 from GaloisInc/combine-repos

Combine repos

README.md

@@ -1,10 +1,22 @@
-This repository contains the code for SAWCore, an intermediate
-language for representing the semantics of software (and potentially
-hardware). It provides support for constructing models in a
-dependently-typed lambda-calculus, transforming those models using a
-rewriting engine, concretely or symbolically interpreting those
-models, and emitting them as input to various external theorem
-provers.
-
-Currently, the library supports generating AIG, CNF, and SMT-Lib
-output.
+SAWCore is a purely functional dependently-typed intermediate language
+for representing the semantics of software (and potentially hardware).
+It includes primitive types and operations sufficient to represent
+values from a multitude of languages, such as C, LLVM, Java, and
+Cryptol.
+
+This repository contains multiple Haskell packages:
+
+  * **`saw-core`** defines the term language, the surface syntax with
+      parser and type checker, a term rewriting engine, and various
+      operations for constructing, analyzing, and evaluating terms.
+
+  * **`saw-core-aig`** provides a backend for generating And-Inverter
+      Graphs (AIGs) from SAWCore terms.
+
+  * **`saw-core-sbv`** provides a backend for translating SAWCore
+      terms into symbolic values in the Haskell SBV library, which can
+      be sent to external SMT solvers.
+
+  * **`saw-core-what4`** provides a backend for translating SAWCore
+      terms into symbolic values in the Haskell What4 library, which
+      can be send to external SMT solvers.

saw-core-aig/.gitignore

@@ -0,0 +1 @@
+.stack-work

saw-core-aig/README.md

@@ -0,0 +1,2 @@
+This repository contains a backend for the `saw-core` library that uses
+the `aig` library for construction of And-Inverter Graphs (AIGs).

saw-core-aig/saw-core-aig.cabal

@@ -0,0 +1,29 @@
+Name:               saw-core-aig
+Version:            0.1
+License:            BSD3
+License-file:       LICENSE
+Author:             Galois, Inc.
+Maintainer:         [email protected]
+Copyright:          (c) 2012-2016 Galois Inc.
+Category:           Formal Methods
+Build-type:         Simple
+cabal-version:      >= 1.8
+Synopsis:           SAWCore backend for AIGs
+Description:
+  A backend for symbolically evaluating terms in the SAWCore
+  intermediate language using the aig library to generate And-Inverter
+  Graphs (AIGs).
+
+library
+  build-depends:
+    aig,
+    base == 4.*,
+    containers,
+    saw-core,
+    vector
+  hs-source-dirs: src
+  exposed-modules:
+     Verifier.SAW.Simulator.BitBlast
+  GHC-options: -Wall -Werror
+  if impl(ghc == 8.0.1)
+    ghc-options: -Wno-redundant-constraints