diff --git a/CHANGES b/CHANGES
new file mode 100644
--- /dev/null
+++ b/CHANGES
@@ -0,0 +1,1 @@
+1.0:    First release.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,7 @@
+Copyright (c) 2011 Iavor S. Diatchki, Galois Inc.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/smtLib.cabal b/smtLib.cabal
new file mode 100644
--- /dev/null
+++ b/smtLib.cabal
@@ -0,0 +1,66 @@
+Name:           smtLib
+Version:        1.0
+License:        BSD3
+License-file:   LICENSE
+Author:         Iavor S. Diatchki
+Maintainer:     iavor.diatchki@gmail.com
+Category:       SMT
+Synopsis:       A library for working with the SMTLIB format.
+Description:    A library for working with the SMTLIB format.
+Build-type:     Simple
+Cabal-version: >= 1.8
+Extra-source-files:
+  LICENSE,
+  CHANGES
+
+library
+  hs-source-dirs: src
+
+  exposed-modules:
+    SMTLib1
+    SMTLib1.QF_BV
+    SMTLib1.QF_AUFBV
+    SMTLib2
+    SMTLib2.Compat1
+    SMTLib2.Core
+    SMTLib2.BitVector
+    SMTLib2.Array
+
+  other-modules:
+    SMTLib1.AST
+    SMTLib1.PP
+    SMTLib2.AST
+    SMTLib2.PP
+
+  build-depends:
+    base   < 5,
+    pretty
+
+
+  GHC-options:    -O2 -Wall
+
+source-repository head
+  type:     git
+  location: git://github.com/yav/smtLib.git
+
+executable smtLib-test-1
+
+  hs-source-dirs: test
+
+  main-is: Test1.hs
+
+  build-depends:
+    base    < 5,
+    smtLib,
+    process
+
+executable smtLib-test-2
+
+  hs-source-dirs: test
+
+  main-is: Test2.hs
+
+  build-depends:
+    base    < 5,
+    smtLib,
+    process
diff --git a/src/SMTLib1.hs b/src/SMTLib1.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib1.hs
@@ -0,0 +1,5 @@
+module SMTLib1 (module X) where
+
+import SMTLib1.AST as X
+import SMTLib1.PP as X
+
diff --git a/src/SMTLib1/AST.hs b/src/SMTLib1/AST.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib1/AST.hs
@@ -0,0 +1,154 @@
+-- This file is based on:
+--
+-- "The SMT-LIB Standard, Version 1.2"
+-- by Silvio Ranise and Cesare Tinelli
+-- Release: 5 August 2006
+-- Appendix A
+--
+-- URL:
+-- http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.05.pdf
+
+{-# LANGUAGE OverloadedStrings #-}
+module SMTLib1.AST where
+
+import GHC.Exts(IsString(..))
+
+newtype Name  = N String
+                deriving (Eq,Ord,Show)
+
+data Ident    = I Name [Integer]
+                deriving (Eq,Ord,Show)
+
+data Quant    = Exists | Forall
+                deriving (Eq,Ord,Show)
+
+data Conn     = Not | Implies | And | Or | Xor | Iff | IfThenElse
+                deriving (Eq,Ord,Show)
+
+data Formula  = FTrue
+              | FFalse
+              | FPred Ident [Term]
+              | FVar Name
+              | Conn Conn [Formula]
+              | Quant Quant [Binder] Formula
+              | Let Name Term Formula
+              | FLet Name Formula Formula
+              | FAnnot Formula [Annot]
+                deriving (Eq,Ord,Show)
+
+type Sort     = Ident
+
+data Binder   = Bind { bindVar :: Name, bindSort :: Sort }
+                deriving (Eq,Ord,Show)
+
+data Term     = Var Name
+              | App Ident [Term]
+              | Lit Literal
+              | ITE Formula Term Term
+              | TAnnot Term [Annot]
+                deriving (Eq,Ord,Show)
+
+data Literal  = LitNum Integer
+              | LitFrac Rational
+              | LitStr String
+                deriving (Eq,Ord,Show)
+
+data Annot    = Attr { attrName :: Name, attrVal :: Maybe String }
+                deriving (Eq,Ord,Show)
+
+data FunDecl  = FunDecl { funName   :: Ident
+                        , funArgs   :: [Sort]
+                        , funRes    :: Sort
+                        , funAnnots :: [Annot]
+                        }
+
+data PredDecl = PredDecl { predName   :: Ident
+                         , predArgs   :: [Sort]
+                         , predAnnots :: [Annot]
+                         }
+
+data Status   = Sat | Unsat | Unknown
+
+data Command
+  = CmdLogic Ident
+  | CmdAssumption Formula
+  | CmdFormula Formula
+  | CmdStatus Status
+  | CmdExtraSorts [ Sort ]
+  | CmdExtraFuns  [ FunDecl ]
+  | CmdExtraPreds [ PredDecl ]
+  | CmdNotes String
+  | CmdAnnot Annot
+
+-- aka "benchmark"
+data Script = Script { scrName :: Ident, scrCommands :: [Command] }
+
+
+--------------------------------------------------------------------------------
+-- To make it a bit simpler to write terms in the above AST
+-- we provide some instances.  They are intended to be used only
+-- for writing simple literals, and not any of the computational
+-- operations associated with the classes.
+
+-- Strings
+instance IsString Name      where fromString x = N x
+instance IsString Ident     where fromString x = I (fromString x) []
+instance IsString Term      where fromString x = Lit (LitStr x)
+
+-- Integral operations
+instance Num Term where
+  fromInteger = Lit . LitNum
+  x + y       = App "+" [x,y]
+  x - y       = App "-" [x,y]
+  x * y       = App "*" [x,y]
+  signum x    = App "signum" [x]
+  abs x       = App "abs" [x]
+
+-- Fractional numbers
+instance Fractional Term where
+  fromRational  = Lit . LitFrac . fromRational
+  x / y         = App "/" [x,y]
+
+--------------------------------------------------------------------------------
+-- XXX: move to a separate module?
+
+(===) :: Term -> Term -> Formula
+x === y   = FPred "=" [x,y]
+
+(=/=) :: Term -> Term -> Formula
+x =/= y   = FPred "distinct" [x,y]
+
+-- | For 'Int'
+(.<.) :: Term -> Term -> Formula
+x .<. y   = FPred "<" [x,y]
+
+-- | For 'Int'
+(.>.) :: Term -> Term -> Formula
+x .>. y   = FPred ">" [x,y]
+
+tInt :: Sort
+tInt = "Int"
+
+funDef :: Ident -> [Sort] -> Sort -> Command
+funDef x as b = CmdExtraFuns [ FunDecl { funName = x
+                                       , funArgs = as
+                                       , funRes = b
+                                       , funAnnots = []
+                                       } ]
+
+constDef :: Ident -> Sort -> Command
+constDef x t = funDef x [] t
+
+
+logic :: Ident -> Command
+logic = CmdLogic
+
+assume :: Formula -> Command
+assume = CmdAssumption
+
+goal :: Formula -> Command
+goal = CmdFormula
+
+
+
+
diff --git a/src/SMTLib1/PP.hs b/src/SMTLib1/PP.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib1/PP.hs
@@ -0,0 +1,141 @@
+module SMTLib1.PP where
+
+import SMTLib1.AST
+import Text.PrettyPrint
+
+class PP t where
+  pp :: t -> Doc
+
+instance PP Name where
+  pp (N x) = text x
+
+instance PP Ident where
+  pp (I x is) = pp x <> case is of
+                          [] -> empty
+                          _  -> brackets $ hcat $ punctuate (char ':')
+                                                $ map integer is
+
+instance PP Quant where
+  pp Forall = text "forall"
+  pp Exists = text "exists"
+
+instance PP Conn where
+  pp conn =
+    case conn of
+      Not        -> text "not"
+      Implies    -> text "implies"
+      And        -> text "and"
+      Or         -> text "or"
+      Xor        -> text "xor"
+      Iff        -> text "iff"
+      IfThenElse -> text "if_then_else"
+
+instance PP Binder where
+  pp (Bind x t) = parens (char '?' <> pp x <+> pp t)
+
+instance PP Formula where
+  pp form =
+    case form of
+      FTrue       -> text "true"
+      FFalse      -> text "false"
+      FVar x      -> char '$' <> pp x
+      FPred p []  -> pp p
+      _           -> parens (ppUnwrap form)
+
+    where
+    ppUnwrap form1 =
+      case form1 of
+        Conn c fs     -> pp c <+> fsep (map pp fs)
+        Quant q bs f  ->
+          case bs of
+            [] -> pp f
+            _  -> pp q <+> sep (map pp bs) <+> pp f
+        Let x t f     -> text "let" <+> parens (char '?' <> pp x <+> pp t)
+                      $$ pp f
+        FLet x f1 f2  -> text "flet" <+> parens (char '$' <> pp x <+> pp f1)
+                      $$ pp f2
+        FPred p ts    -> pp p <+> fsep (map pp ts)
+        FAnnot f as   -> ppUnwrap f $$ nest 2 (vcat (map pp as))
+        _             -> pp form1
+
+
+instance PP Annot where
+  pp (Attr x v) = char ':' <> pp x <+> maybe empty ppUserValue v
+    where
+    ppUserValue = braces . text . concatMap esc
+
+    esc '{' = "\\{"
+    esc c   = [c]
+
+instance PP Term where
+  pp term =
+    case term of
+      Var n     -> char '?' <> pp n
+      App f []  -> pp f
+      Lit l     -> pp l
+      _         -> parens (ppUnwrap term)
+
+    where
+    ppUnwrap term1 =
+      case term1 of
+        App f ts    -> pp f <+> fsep (map pp ts)
+        ITE f t1 t2 -> text "ite" <+> pp f $$ nest 2 (pp t1 $$ pp t2)
+        TAnnot t as -> ppUnwrap t $$ nest 2 (vcat (map pp as))
+        _           -> pp term1
+
+
+instance PP Literal where
+  pp lit =
+    case lit of
+      LitNum n  -> integer n
+      LitFrac x -> text (show (fromRational x :: Double)) -- XXX: Good enough?
+      LitStr x  -> text (show x)
+
+instance PP FunDecl where
+  pp d = parens (pp (funName d) <+> fsep (map pp (funArgs d)) <+> pp (funRes d)
+                  $$ nest 2 (vcat (map pp (funAnnots d))))
+
+instance PP PredDecl where
+  pp d = parens (pp (predName d) <+> fsep (map pp (predArgs d))
+                  $$ nest 2 (vcat (map pp (predAnnots d))))
+
+instance PP Status where
+  pp stat =
+    case stat of
+      Sat       -> text "sat"
+      Unsat     -> text "unsat"
+      Unknown   -> text "unknown"
+
+instance PP Command where
+  pp cmd =
+    case cmd of
+      CmdLogic n      -> std "logic" n
+      CmdAssumption f -> std "assumption" f
+      CmdFormula f    -> std "formula" f
+      CmdStatus s     -> std "status" s
+      CmdExtraSorts s -> many "extrasorts" s
+      CmdExtraFuns  f -> many "extrafuns" f
+      CmdExtraPreds p -> many "extrapreds" p
+      CmdNotes s      -> mk "notes" (str s)
+      CmdAnnot a      -> pp a
+
+    where mk x d    = char ':' <> text x <+> d
+
+          std x n   = mk x (pp n)
+
+          many _ [] = empty
+          many x ns = mk x (parens (vcat (map pp ns)))
+
+          esc '"'   = "\\\""
+          esc c     = [c]
+
+          str s     = (char '"' <> text (concatMap esc s) <> char '"')
+
+
+
+
+
+instance PP Script where
+  pp s  = parens (text "benchmark" <+> pp (scrName s)
+                  $$ nest 2 (vcat (map pp (scrCommands s))))
+
diff --git a/src/SMTLib1/QF_AUFBV.hs b/src/SMTLib1/QF_AUFBV.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib1/QF_AUFBV.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE OverloadedStrings #-}
+module SMTLib1.QF_AUFBV (module SMTLib1.QF_AUFBV, module X) where
+
+import SMTLib1.QF_BV as X
+
+-- | 'tArray i n' is an array indexed by bitvectors of widht 'i',
+-- and storing bitvectors of width 'n'.
+tArray :: Integer -> Integer -> Sort
+tArray x y = I "Array" [x,y]
+
+-- | @select array index@
+select :: Term -> Term -> Term
+select a i = App "select" [a,i]
+
+-- | @store array index value@
+store :: Term -> Term -> Term -> Term
+store a i v = App "store" [a,i,v]
+
diff --git a/src/SMTLib1/QF_BV.hs b/src/SMTLib1/QF_BV.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib1/QF_BV.hs
@@ -0,0 +1,132 @@
+{-# LANGUAGE OverloadedStrings #-}
+module SMTLib1.QF_BV (module X, module SMTLib1.QF_BV) where
+
+import SMTLib1 as X
+import GHC.Exts(IsString(..))
+
+
+tBitVec :: Integer -> Sort
+tBitVec n = I "BitVec" [n]
+
+isBitVec :: Sort -> Maybe Integer
+isBitVec (I "BitVec" [n]) = Just n
+isBitVec _                = Nothing
+
+-- | BitVec[1]
+bit0 :: Term
+bit0 = App "bit0" []
+
+-- | BitVec[1]
+bit1 :: Term
+bit1 = App "bit1" []
+
+-- | [m] -> [n] -> [m+n]
+concat :: Term -> Term -> Term
+concat x y = App "concat" [x,y]
+
+extract :: Integer -> Integer -> Term -> Term
+extract i j t = App (I "extract" [i,j]) [t]
+
+bvnot :: Term -> Term
+bvnot t = App "bvnot" [t]
+
+bvand :: Term -> Term -> Term
+bvand s t = App "bvand" [s,t]
+
+bvor :: Term -> Term -> Term
+bvor s t = App "bvor" [s,t]
+
+bvneg :: Term -> Term
+bvneg t  = App "bvneg" [t]
+
+bvadd :: Term -> Term -> Term
+bvadd s t = App "bvadd" [s,t]
+
+bvmul :: Term -> Term -> Term
+bvmul s t = App "bvmul" [s,t]
+
+bvudiv :: Term -> Term -> Term
+bvudiv s t = App "bvudiv" [s,t]
+
+bvurem :: Term -> Term -> Term
+bvurem s t = App "bvurem" [s,t]
+
+bvshl :: Term -> Term -> Term
+bvshl s t = App "bvshl" [s,t]
+
+bvlshr :: Term -> Term -> Term
+bvlshr s t = App "bvlshr" [s,t]
+
+
+bv :: Integer -> Integer -> Term
+bv x m = if x >= 0 then lit x else bvneg (lit (negate x))
+  where lit y = App (I (fromString ("bv" ++ show y)) [m]) []
+
+bvnand :: Term -> Term -> Term
+bvnand s t = App "bvnand" [s,t]
+
+bvnor :: Term -> Term -> Term
+bvnor s t = App "bvnor" [s,t]
+
+bvxor :: Term -> Term -> Term
+bvxor s t = App "bvxor" [s,t]
+
+bvxnor :: Term -> Term -> Term
+bvxnor s t = App "bvxnor" [s,t]
+
+bvcomp :: Term -> Term -> Term
+bvcomp s t = App "bvcomp" [s,t]
+
+bvsub :: Term -> Term -> Term
+bvsub s t = App "bvsub" [s,t]
+
+bvsdiv :: Term -> Term -> Term
+bvsdiv s t = App "bvsdiv" [s,t]
+
+bvsrem :: Term -> Term -> Term
+bvsrem s t = App "bvsrem" [s,t]
+
+bvsmod :: Term -> Term -> Term
+bvsmod s t = App "bvsmod" [s,t]
+
+bvashr :: Term -> Term -> Term
+bvashr s t = App "bvashr" [s,t]
+
+repeat :: Integer -> Term -> Term
+repeat i t = App (I "repeat" [i]) [t]
+
+zero_extend :: Integer -> Term -> Term
+zero_extend i t = App (I "zero_extend" [i]) [t]
+
+sign_extend :: Integer -> Term -> Term
+sign_extend i t = App (I "sign_extend" [i]) [t]
+
+rotate_left :: Integer -> Term -> Term
+rotate_left i t = App (I "rotate_left" [i]) [t]
+
+rotate_right :: Integer -> Term -> Term
+rotate_right i t = App (I "rotate_right" [i]) [t]
+
+bvule :: Term -> Term -> Formula
+bvule s t = FPred "bvule" [s,t]
+
+bvugt :: Term -> Term -> Formula
+bvugt s t = FPred "bvugt" [s,t]
+
+bvuge :: Term -> Term -> Formula
+bvuge s t = FPred "bvuge" [s,t]
+
+bvslt :: Term -> Term -> Formula
+bvslt s t = FPred "bvslt" [s,t]
+
+bvsle :: Term -> Term -> Formula
+bvsle s t = FPred "bvsle" [s,t]
+
+bvsgt :: Term -> Term -> Formula
+bvsgt s t = FPred "bvsgt" [s,t]
+
+bvsge :: Term -> Term -> Formula
+bvsge s t = FPred "bvsge" [s,t]
+
+
+
diff --git a/src/SMTLib2.hs b/src/SMTLib2.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib2.hs
@@ -0,0 +1,5 @@
+module SMTLib2 (module X) where
+
+import SMTLib2.AST as X
+import SMTLib2.PP as X
+
diff --git a/src/SMTLib2/AST.hs b/src/SMTLib2/AST.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib2/AST.hs
@@ -0,0 +1,137 @@
+-- This file is based on:
+--
+-- "The SMT-LIB Standard, Version 2.0"
+-- by Clark Barrett Aaron Stump Cesare Tinelli
+-- Release: December 21, 2010
+-- Appendix C
+--
+-- URL:
+-- http://goedel.cs.uiowa.edu/smtlib/papers/smt-lib-reference-v2.0-r10.12.21.pdf
+
+{-# LANGUAGE OverloadedStrings #-}
+module SMTLib2.AST where
+
+import GHC.Exts(IsString(..))
+
+newtype Name  = N String
+                deriving (Eq,Ord,Show)
+
+data Ident    = I Name [Integer]
+                deriving (Eq,Ord,Show)
+
+data Quant    = Exists | Forall
+                deriving (Eq,Ord,Show)
+
+data Binder   = Bind { bindVar :: Name, bindType :: Type }
+                deriving (Eq,Ord,Show)
+
+data Defn     = Defn { defVar :: Name, defExpr :: Expr }
+                deriving (Eq,Ord,Show)
+
+data Literal  = LitBV Integer Integer   -- ^ value, width (in bits)
+              | LitNum Integer
+              | LitFrac Rational
+              | LitStr String
+                deriving (Eq,Ord,Show)
+
+data Type     = TApp Ident [Type]
+              | TVar Name
+                deriving (Eq,Ord,Show)
+
+data Expr     = Lit Literal
+              | App Ident (Maybe Type) [Expr]
+              | Quant Quant [Binder] Expr
+              | Let [Defn] Expr
+              | Annot Expr [Attr]
+                deriving (Eq,Ord,Show)
+
+data Attr     = Attr { attrName :: Name , attrVal :: Maybe AttrVal }
+                deriving (Eq,Ord,Show)
+
+type AttrVal  = Expr    -- A bit of an approximation....
+
+
+data Option
+  = OptPrintSuccess Bool
+  | OptExpandDefinitions Bool
+  | OptInteractiveMode Bool
+  | OptProduceProofs Bool
+  | OptProduceUnsatCores Bool
+  | OptProduceModels Bool
+  | OptProduceAssignments Bool
+  | OptRegularOutputChannel String
+  | OptDiagnosticOutputChannel String
+  | OptRandomSeed Integer
+  | OptVerbosity Integer
+  | OptAttr Attr
+
+data InfoFlag
+  = InfoAllStatistics
+  | InfoErrorBehavior
+  | InfoName
+  | InfoAuthors
+  | InfoVersion
+  | InfoStatus
+  | InfoReasonUnknown
+  | InfoAttr Attr
+
+data Command
+  = CmdSetLogic Name
+  | CmdSetOption Option
+  | CmdSetInfo Attr
+  | CmdDeclareType Name Integer
+  | CmdDefineType Name [Name] Type
+  | CmdDeclareFun Name [Type] Type
+  | CmdDefineFun Name [Binder] Type Expr
+  | CmdPush Integer
+  | CmdPop Integer
+  | CmdAssert Expr
+  | CmdCheckSat
+  | CmdGetAssertions
+  | CmdGetValue [Expr]
+  | CmdGetProof
+  | CmdGetUnsatCore
+  | CmdGetInfo InfoFlag
+  | CmdGetOption Name
+  | CmdExit
+
+newtype Script = Script [Command]
+
+
+--------------------------------------------------------------------------------
+-- To make it a bit simpler to write terms in the above AST
+-- we provide some instances.  They are intended to be used only
+-- for writing simple literals, and not any of the computational
+-- operations associated with the classes.
+
+-- Strings
+instance IsString Name      where fromString   = N
+instance IsString Ident     where fromString x = I (fromString x) []
+instance IsString Type      where fromString x = TApp (fromString x) []
+instance IsString Expr      where fromString   = Lit . LitStr . fromString
+
+-- Integers
+
+-- NOTE: Some of these might not mean anything, depending on the theory.
+instance Num Expr where
+  fromInteger x = Lit (LitNum x)
+  x + y         = app "+"      [x,y]
+  x - y         = app "-"      [x,y]
+  x * y         = app "*"      [x,y]
+  signum x      = app "signum" [x]
+  abs x         = app "abs"    [x]
+
+
+-- Fractional numbers
+instance Fractional Expr where
+  fromRational x  = Lit (LitFrac x)
+  x / y           = app "/" [x,y]
+
+app :: Ident -> [Expr] -> Expr
+app f es = App f Nothing es
+
+
+
+
+
+
diff --git a/src/SMTLib2/Array.hs b/src/SMTLib2/Array.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib2/Array.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE OverloadedStrings #-}
+module SMTLib2.Array where
+
+import SMTLib2.AST
+
+tArray :: Type -> Type -> Type
+tArray x y = TApp "Array" [x,y]
+
+select :: Expr -> Expr -> Expr
+select x y = app "select" [x,y]
+
+store :: Expr -> Expr -> Expr -> Expr
+store x y z = app "store" [x,y,z]
+
+
diff --git a/src/SMTLib2/BitVector.hs b/src/SMTLib2/BitVector.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib2/BitVector.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE OverloadedStrings #-}
+module SMTLib2.BitVector where
+
+import SMTLib2.AST
+
+tBitVec :: Integer -> Type
+tBitVec n = TApp (I "BitVec" [n]) []
+
+bv :: Integer -> Integer -> Expr
+bv num w = Lit (LitBV num w)
+
+concat :: Expr -> Expr -> Expr
+concat x y = app "concat" [x,y]
+
+extract :: Integer -> Integer -> Expr -> Expr
+extract i j x = app (I "extract" [i,j]) [x]
+
+bvnot :: Expr -> Expr
+bvnot x = app "bvnot" [x]
+
+bvand :: Expr -> Expr -> Expr
+bvand x y = app "bvand" [x,y]
+
+bvor :: Expr -> Expr -> Expr
+bvor x y = app "bvor" [x,y]
+
+bvneg :: Expr -> Expr
+bvneg x = app "bvneg" [x]
+
+bvadd :: Expr -> Expr -> Expr
+bvadd x y = app "bvadd" [x,y]
+
+bvmul :: Expr -> Expr -> Expr
+bvmul x y = app "bvmul" [x,y]
+
+bvudiv :: Expr -> Expr -> Expr
+bvudiv x y = app "bvudiv" [x,y]
+
+bvurem :: Expr -> Expr -> Expr
+bvurem x y = app "bvurem" [x,y]
+
+bvshl :: Expr -> Expr -> Expr
+bvshl x y = app "bvshl" [x,y]
+
+bvlshr :: Expr -> Expr -> Expr
+bvlshr x y = app "bvlshr" [x,y]
+
+bvult :: Expr -> Expr -> Expr
+bvult x y = app "bvult" [x,y]
+
+bvnand :: Expr -> Expr -> Expr
+bvnand x y = app "bvnand" [x,y]
+
+bvnor :: Expr -> Expr -> Expr
+bvnor x y = app "bvnor" [x,y]
+
+bvxor :: Expr -> Expr -> Expr
+bvxor x y = app "bvxor" [x,y]
+
+bvxnor :: Expr -> Expr -> Expr
+bvxnor x y = app "bvxnor" [x,y]
+
+bvcomp :: Expr -> Expr -> Expr
+bvcomp x y = app "bvcomp" [x,y]
+
+bvsub :: Expr -> Expr -> Expr
+bvsub x y = app "bvsub" [x,y]
+
+bvsdiv :: Expr -> Expr -> Expr
+bvsdiv x y = app "bvsdiv" [x,y]
+
+bvsrem :: Expr -> Expr -> Expr
+bvsrem x y = app "bvsrem" [x,y]
+
+bvsmod :: Expr -> Expr -> Expr
+bvsmod x y = app "bvsmod" [x,y]
+
+bvashr :: Expr -> Expr -> Expr
+bvashr x y = app "bvashr" [x,y]
+
+repeat :: Integer -> Expr -> Expr -> Expr
+repeat i x y = app (I "repeat" [i]) [x,y]
+
+zero_extend :: Integer -> Expr -> Expr
+zero_extend i x = app (I "zero_extend" [i]) [x]
+
+sign_extend :: Integer -> Expr -> Expr
+sign_extend i x = app (I "sign_extend" [i]) [x]
+
+rotate_left :: Integer -> Expr -> Expr
+rotate_left i x = app (I "rotate_left" [i]) [x]
+
+rotate_right :: Integer -> Expr -> Expr
+rotate_right i x = app (I "rotate_right" [i]) [x]
+
+bvule :: Expr -> Expr -> Expr
+bvule x y = app "bvule" [x,y]
+
+bvugt :: Expr -> Expr -> Expr
+bvugt x y = app "bvugt" [x,y]
+
+bvuge :: Expr -> Expr -> Expr
+bvuge x y = app "bvuge" [x,y]
+
+bvslt :: Expr -> Expr -> Expr
+bvslt x y = app "bvslt" [x,y]
+
+bvsle :: Expr -> Expr -> Expr
+bvsle x y = app "bvsle" [x,y]
+
+bvsgt :: Expr -> Expr -> Expr
+bvsgt x y = app "bvsgt" [x,y]
+
+bvsge :: Expr -> Expr -> Expr
+bvsge x y = app "bvsge" [x,y]
+
+
+
+
+
+
+
+
+
diff --git a/src/SMTLib2/Compat1.hs b/src/SMTLib2/Compat1.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib2/Compat1.hs
@@ -0,0 +1,182 @@
+module SMTLib2.Compat1 where
+
+import qualified SMTLib1.AST as V1
+import qualified SMTLib1.PP  as V1
+import qualified SMTLib2.AST as V2
+import qualified SMTLib2.Core as V2
+
+import Control.Applicative(Applicative(..), (<$>))
+import Data.Traversable(traverse)
+import Text.PrettyPrint
+
+
+data Trans a = OK a | Fail Doc
+
+toMaybe :: Trans a -> Maybe a
+toMaybe res =
+  case res of
+    OK a   -> Just a
+    Fail _ -> Nothing
+
+toEither :: Trans a -> Either Doc a
+toEither res =
+  case res of
+    OK a     -> Right a
+    Fail msg -> Left msg
+
+instance Functor Trans where
+  fmap f res =
+    case res of
+      OK a     -> OK (f a)
+      Fail msg -> Fail msg
+
+instance Applicative Trans where
+  pure x = OK x
+
+  OK f   <*> OK x   = OK (f x)
+  Fail x <*> OK _   = Fail x
+  OK _   <*> Fail x = Fail x
+  Fail x <*> Fail y = Fail (x $$ y)
+
+err :: Doc -> Trans a
+err msg = Fail msg
+--------------------------------------------------------------------------------
+
+
+name :: V1.Name -> V2.Name
+name (V1.N x) = V2.N x
+
+ident :: V1.Ident -> V2.Ident
+ident (V1.I x ns) = V2.I (name x) ns
+
+quant :: V1.Quant -> V2.Quant
+quant q =
+  case q of
+    V1.Exists -> V2.Exists
+    V1.Forall -> V2.Forall
+
+binder :: V1.Binder -> V2.Binder
+binder b = V2.Bind { V2.bindVar  = name (V1.bindVar b)
+                   , V2.bindType = sort (V1.bindSort b)
+                   }
+
+sort :: V1.Sort -> V2.Type
+sort x = V2.TApp (ident x) []
+
+literal :: V1.Literal -> V2.Literal
+literal lit =
+  case lit of
+    V1.LitNum n   -> V2.LitNum n
+    V1.LitFrac r  -> V2.LitFrac r
+    V1.LitStr s   -> V2.LitStr s
+
+term :: V1.Term -> Trans V2.Expr
+term te =
+  case te of
+    V1.Var x       -> pure (V2.app (V2.I (name x) []) []) -- XXX: or add var?
+    V1.App i ts    -> V2.app (ident i) <$> traverse term ts
+    V1.Lit l       -> pure (V2.Lit (literal l))
+    V1.ITE f t1 t2 -> V2.ite <$> formula f <*> term t1 <*> term t2
+    V1.TAnnot t a  -> V2.Annot <$> term t <*> traverse annot a
+
+
+formula :: V1.Formula -> Trans V2.Expr
+formula form =
+  case form of
+
+    V1.FTrue      -> pure V2.true
+
+    V1.FFalse     -> pure V2.false
+
+    V1.FPred p ts -> V2.app (ident p) <$> traverse term ts
+
+    V1.FVar x     -> pure (V2.app (V2.I (name x) []) []) -- XXX: or add var?
+
+    V1.Conn c es ->
+      case (c,es) of
+        (V1.Not, [e])         -> V2.not <$> formula e
+        (V1.Implies, [e1,e2]) -> (V2.==>) <$> formula e1 <*> formula e2
+        (V1.And, _) ->
+           case es of
+             [] -> pure V2.true
+             _  -> foldr1 V2.and <$> traverse formula es
+        (V1.Or, _) ->
+           case es of
+             [] -> pure V2.false
+             _  -> foldr1 V2.or <$> traverse formula es
+        (V1.Xor, _ : _)             -> foldr1 V2.xor <$> traverse formula es
+        (V1.Iff, [e1,e2])           -> (V2.===) <$> formula e1 <*> formula e2
+        (V1.IfThenElse, [e1,e2,e3]) -> V2.ite <$> formula e1
+                                              <*> formula e2
+                                              <*> formula e3
+        _ -> err (text "Unsupported connective:" <+> V1.pp form)
+
+    V1.Quant q bs f -> V2.Quant (quant q) (map binder bs) <$> formula f
+    V1.Let x t f    -> mkLet <$> term t <*> formula f
+      where mkLet e = V2.Let [ V2.Defn (name x) e ]
+    V1.FLet x f1 f2 ->  mkLet <$> formula f1 <*> formula f2
+      where mkLet e = V2.Let [ V2.Defn (name x) e ]
+    V1.FAnnot t a   -> V2.Annot <$> formula t <*> traverse annot a
+
+annot :: V1.Annot -> Trans V2.Attr
+annot x = case V1.attrVal x of
+            Nothing -> pure V2.Attr { V2.attrName = name (V1.attrName x)
+                                    , V2.attrVal = Nothing
+                                    }
+            _ -> err (text "Unsupported annotation:" <+> V1.pp x)
+
+
+command :: V1.Command -> Trans [V2.Command]
+command com =
+  case com of
+
+    V1.CmdLogic l      -> one . V2.CmdSetLogic <$> simpleIdent l
+
+    V1.CmdAssumption f -> one . V2.CmdAssert <$> formula f
+
+    V1.CmdFormula f    -> one . V2.CmdAssert <$> formula f
+
+    V1.CmdStatus s ->
+      case s of
+        V1.Sat -> pure [ V2.CmdCheckSat ]
+        _      -> err (text "Unsupported command:" <+> V1.pp com)
+
+    V1.CmdExtraSorts xs -> map decl <$> traverse simpleIdent xs
+      where decl x = V2.CmdDeclareType x 0
+
+    V1.CmdExtraFuns fs -> traverse decl fs
+      where decl f = case V1.funAnnots f of
+                       [] -> V2.CmdDeclareFun
+                               <$> simpleIdent (V1.funName f)
+                               <*> pure (map sort (V1.funArgs f))
+                               <*> pure (sort (V1.funRes f))
+                       _ -> err (text "Annotation in function declaration" <+>
+                                  V1.pp com)
+
+    V1.CmdExtraPreds fs -> traverse decl fs
+      where decl f = case V1.predAnnots f of
+                       [] -> V2.CmdDeclareFun
+                               <$> simpleIdent (V1.predName f)
+                               <*> pure (map sort (V1.predArgs f))
+                               <*> pure V2.tBool
+                       _ -> err (text "Annotation in predicate declaration" <+>
+                                  V1.pp com)
+
+    -- XXX: For now, we just ignore comments
+    V1.CmdNotes {}    -> pure []
+
+    V1.CmdAnnot a     -> one . V2.CmdSetInfo <$> annot a
+
+  where one x = [x]
+
+        simpleIdent (V1.I x []) = pure (name x)
+        simpleIdent d =
+          err (text "Unsupported identifier in command:" <+> V1.pp d)
+
+
+script :: V1.Script -> Trans V2.Script
+script s = V2.Script . concat <$> traverse command (V1.scrCommands s)
+
+
+
+
diff --git a/src/SMTLib2/Core.hs b/src/SMTLib2/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib2/Core.hs
@@ -0,0 +1,41 @@
+{-# LANGUAGE OverloadedStrings #-}
+module SMTLib2.Core where
+
+import SMTLib2.AST
+
+tBool :: Type
+tBool = "Bool"
+
+true :: Expr
+true = app "true" []
+
+false :: Expr
+false = app "false" []
+
+not :: Expr -> Expr
+not p = app "not" [p]
+
+(==>) :: Expr -> Expr -> Expr
+p ==> q = app "=>" [p,q]
+
+and :: Expr -> Expr -> Expr
+and p q = app "and" [p,q]
+
+or :: Expr -> Expr -> Expr
+or p q = app "or" [p,q]
+
+xor :: Expr -> Expr -> Expr
+xor p q = app "xor" [p,q]
+
+(===) :: Expr -> Expr -> Expr
+x === y = app "=" [x,y]
+
+(=/=) :: Expr -> Expr -> Expr
+x =/= y = app "distinct" [x,y]
+
+ite :: Expr -> Expr -> Expr -> Expr
+ite b x y = app "ite" [b,x,y]
+
+
+
+
diff --git a/src/SMTLib2/PP.hs b/src/SMTLib2/PP.hs
new file mode 100644
--- /dev/null
+++ b/src/SMTLib2/PP.hs
@@ -0,0 +1,166 @@
+module SMTLib2.PP where
+
+import SMTLib2.AST
+import Text.PrettyPrint
+import Numeric
+import Data.List(genericReplicate)
+
+class PP t where
+  pp :: t -> Doc
+
+instance PP Bool where
+  pp True   = text "true"
+  pp False  = text "false"
+
+instance PP Integer where
+  pp        = integer
+
+ppString :: String -> Doc
+ppString = text . show
+
+instance PP Name where
+  pp (N x) = text x
+
+instance PP Ident where
+  pp (I x []) = pp x
+  pp (I x is) = parens (char '_' <+> pp x <+> fsep (map integer is))
+
+instance PP Attr where
+  pp (Attr x v) = char ':' <> pp x <+> maybe empty pp v
+
+instance PP Quant where
+  pp Forall = text "forall"
+  pp Exists = text "exists"
+
+instance PP Expr where
+  pp expr =
+    case expr of
+
+      Lit l     -> pp l
+
+      App c ty ts  ->
+        case ts of
+          [] -> ppFun
+          _  -> parens (ppFun <+> fsep (map pp ts))
+
+        where ppFun = case ty of
+                        Nothing -> pp c
+                        Just t  -> parens (text "as" <+> pp c <+> pp t)
+
+      Quant q bs e ->
+        case bs of
+          [] -> pp e
+          _  -> parens (pp q <+> parens (fsep (map pp bs)) $$ nest 2 (pp e))
+
+      Let ds e ->
+        case ds of
+          [] -> pp e
+          _  -> parens (text "let" <+> (parens (vcat (map pp ds)) $$ pp e))
+
+      Annot e as ->
+        case as of
+          [] -> pp e
+          _  -> parens (char '!' <+> pp e $$ nest 2 (vcat (map pp as)))
+
+
+instance PP Binder where
+  pp (Bind x t) = parens (pp x <+> pp t)
+
+instance PP Defn where
+  pp (Defn x e)   = parens (pp x <+> pp e)
+
+instance PP Type where
+  pp ty =
+    case ty of
+      TApp c ts ->
+        case ts of
+          [] -> pp c
+          _  -> parens (pp c <+> fsep (map pp ts))
+      TVar x -> pp x
+
+instance PP Literal where
+  pp lit =
+    case lit of
+
+      LitBV n w ->
+        case divMod w 4 of
+          -- For the moment we do not print using HEX literals as
+          -- some solvers do not support them (how hard is that???)
+          -- (x,0) -> text "#x" <> text (pad x (showHex v ""))
+          _ -> text "#b" <> text (pad w (showIntAtBase 2 (head . show) v ""))
+
+        where pad digs xs = genericReplicate
+                                (digs - fromIntegral (length xs)) '0' ++ xs
+
+              v = if n < 0 then 2^w + n else n
+
+      LitNum n -> integer n
+
+      LitFrac x -> text (show (fromRational x :: Double))  -- XXX: Good enough?
+
+      LitStr x -> ppString x
+
+
+
+instance PP Option where
+  pp opt =
+    case opt of
+      OptPrintSuccess b             -> std "print-success" b
+      OptExpandDefinitions b        -> std "expand-definitions" b
+      OptInteractiveMode b          -> std "interactive-mode" b
+      OptProduceProofs b            -> std "produce-proofs" b
+      OptProduceUnsatCores b        -> std "produce-unsat-cores" b
+      OptProduceModels b            -> std "produce-models" b
+      OptProduceAssignments b       -> std "produce-assignments" b
+      OptRegularOutputChannel s     -> str "regular-output-channel" s
+      OptDiagnosticOutputChannel s  -> str "diagnostic-output-channel" s
+      OptRandomSeed n               -> std "random-seed" n
+      OptVerbosity n                -> std "verbosity" n
+      OptAttr a                     -> pp a
+
+    where mk a b  = char ':' <> text a <+> b
+          std a b = mk a (pp b)
+          str a b = mk a (ppString b)
+
+instance PP InfoFlag where
+  pp info =
+    case info of
+      InfoAllStatistics -> mk "all-statistics"
+      InfoErrorBehavior -> mk "error-behavior"
+      InfoName          -> mk "name"
+      InfoAuthors       -> mk "authors"
+      InfoVersion       -> mk "version"
+      InfoStatus        -> mk "status"
+      InfoReasonUnknown -> mk "reason-unknown"
+      InfoAttr a        -> pp a
+    where mk x = char ':' <> text x
+
+instance PP Command where
+  pp cmd =
+    case cmd of
+      CmdSetLogic n     -> std "set-logic" n
+      CmdSetOption o    -> std "set-options" o
+      CmdSetInfo a      -> std "set-info" a
+      CmdDeclareType x n    -> mk "declare-sort" (pp x <+> integer n)
+      CmdDefineType x as t  -> fun "define-sort" x as (pp t)
+      CmdDeclareFun x ts t  -> fun "declare-fun" x ts (pp t)
+      CmdDefineFun x bs t e -> fun "define-fun" x bs (pp t $$ nest 2 (pp e))
+      CmdPush n         -> std "push" n
+      CmdPop n          -> std "pop" n
+      CmdAssert e       -> std "assert" e
+      CmdCheckSat       -> one "check-sat"
+      CmdGetAssertions  -> one "get-assertions"
+      CmdGetValue es    -> mk  "get-value" (parens (fsep (map pp es)))
+      CmdGetProof       -> one "get-proof"
+      CmdGetUnsatCore   -> one "get-unsat-core"
+      CmdGetInfo i      -> std "get-info" i
+      CmdGetOption n    -> std "get-option" n
+      CmdExit           -> one "exit"
+    where mk x d = parens (text x <+> d)
+          one x   = mk x empty
+          std x a = mk x (pp a)
+          fun x y as d = mk x (pp y <+> parens (fsep (map pp as)) <+> d)
+
+instance PP Script where
+  pp (Script cs) = vcat (map pp cs)
+
diff --git a/test/Test1.hs b/test/Test1.hs
new file mode 100644
--- /dev/null
+++ b/test/Test1.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE OverloadedStrings #-}
+import SMTLib1.QF_AUFBV as BV
+import System.Process
+import System.IO
+
+main :: IO ()
+main =
+  do let txt = show (pp script)
+     putStrLn txt
+     putStrLn (replicate 80 '-')
+     -- putStrLn =<< readProcess "yices" ["-smt", "-tc"] txt
+     putStrLn =<< readProcess "yices" ["-f"] txt
+
+
+script :: Script
+script = Script "Test"
+  [ logic "QF_AUFBV"
+  , constDef "a" (tBitVec 8)
+  , goal (BV.concat (bv 1 8) (bv 3 8) === bv 259 16)
+  ]
+
+
+script1 :: Script
+script1 = Script "Test"
+  [ logic "QF_BV"
+  , constDef "x" (tBitVec 8)
+  , assume (c "x" === bv 0 8)
+  , goal (c "x" ===  bv 256 8)
+  ]
+
+c x = App x []
+
diff --git a/test/Test2.hs b/test/Test2.hs
new file mode 100644
--- /dev/null
+++ b/test/Test2.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE OverloadedStrings #-}
+import SMTLib2
+import SMTLib2.Core
+import SMTLib2.BitVector
+import System.Process
+import System.IO
+
+main :: IO ()
+main =
+  do let txt = show (pp script)
+     putStrLn txt
+     putStrLn (replicate 80 '-')
+     putStrLn =<< readProcess "stp" ["--SMTLIB2"] txt
+
+
+script :: Script
+script = Script
+  [ CmdSetLogic "QF_BV"
+  , CmdDeclareFun "x" [] (tBitVec 4)
+  , CmdAssert (c "x" === bv 3 4)
+  , CmdCheckSat
+  , CmdExit
+  ]
+
+c x = app x []