Compiler and runtime of the Smten language for functional programming and orchestration of SMT queries
Haskell C++ C TeX Tcl
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
doc
smten-base
smten-lib
smten-minisat
smten-stp
smten-yices1
smten
tclmk
tutorials
.gitignore
LICENSE
README
makefile

README

Smten (Developer) README
========================
Richard Uhler <ruhler@csail.mit.edu>
June 2014

Non-Developer Smten Installation
--------------------------------
If you do not wish to modify the smten implementation, it is easier to build
and install smten using distributed cabal packages.
See tutorials/T1-GettingStarted.txt for how to do this.

This document describes how to build the distributed cabal packages, which is
only needed if you desire to modify the smten implementation.

Configuring Smten for Development Build
---------------------------------------
Before building smten using the makefile, you must configure the build for your
system. This is done by creating the file "tclmk/local.tcl" containing
information about your system.

The following variables should be set in tclmk/local.tcl:
::env(PATH) - The PATH to use for executables
::env(LD_LIBRARY_PATH) - the ld library path
::GHC - the path the the ghc executable to use

For example, tclmk/local.tcl might look like:

=========================================
set ::env(PATH) "/bin:/usr/bin:/home/ruhler/local/bin"
set ::env(LD_LIBRARY_PATH) "/home/ruhler/local/lib"
set ::GHC "/home/ruhler/local/bin/ghc"
=========================================

Yices1, Yices2, STP and Z3
--------------------------
The tests for Smten currently require yices1, yices2, STP, and Z3 to be
installed. See the documentation in tutorial/T3-SMTBackends.txt
for information on how to install them.

Building Smten
--------------
Once smten is configured for build and the required SMT solvers are installed,
it can be built by running `make`. The following targets are supported:

all::
  Build all the smten packages locally and run the test suites for them.
  For the location of the generated cabal distribution packages, run:
  +
    find build -name "smten*.tar.gz"
 
userinstall::
  Build all the smten packages locally, run the test suites, and
  then install the packages into the current users account.

userinstall2::
  Install the packages into the current users account without first building
  them locally. This requires you have already built the packages locally.

clean::
  Clean up the locally generated cabal packages.

fullclean::
  Remove the entire local 'home' directory, including any packages already
  installed locally which smten depends on.

Documentation
-------------
The 'doc' directory contains mostly out-of-date documents. The most relevant
documents now are:

doc/todo.txt:: contains a brief list of known issues and planned work to do.
doc/history.txt:: contains the release history of smten.

For user documentation, consult the generated haddock documentation after
building the packages locally at build/home/.cabal/share/doc/index.html or 
build/smten-*/dist/doc/html/smten-*/index.html for the individual packages.
There are also some tutorials on using Smten in the 'tutorials' directory.