diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,4 @@
+0.8:   Support for declare; loading of strings/files; more sugar for SMT commands
 0.6.0: Allow finer-grained logging
 0.5.5: Add support for unsupported results
 0.5.3: Add 'zeroExtend' and 'signExtend'
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -5,13 +5,12 @@
 module SimpleSMT
   (
     -- * Basic Solver Interface
-    Solver
+    Solver(..)
   , newSolver
-  , command
-  , stop
   , ackCommand
   , simpleCommand
   , simpleCommandMaybe
+  , loadFile
 
     -- ** S-Expressions
   , SExpr(..)
@@ -29,8 +28,10 @@
   , setOption, setOptionMaybe
   , push, pushMany
   , pop, popMany
+  , inNewScope
   , declare
   , declareFun
+  , declareDatatype
   , define
   , defineFun
   , assert
@@ -40,7 +41,7 @@
   , getConsts, getConst
   , Value(..)
 
-    -- * Convenienct Functoins for SmtLib-2 Epxressions
+    -- * Convenience Functions for SmtLib-2 Epxressions
   , fam
   , fun
   , const
@@ -63,7 +64,9 @@
     -- ** Connectives
   , not
   , and
+  , andMany
   , or
+  , orMany
   , xor
   , implies
 
@@ -72,6 +75,7 @@
 
     -- ** Relational Predicates
   , eq
+  , distinct
   , gt
   , lt
   , geq
@@ -83,6 +87,7 @@
 
     -- ** Arithmetic
   , add
+  , addMany
   , sub
   , neg
   , mul
@@ -196,7 +201,7 @@
 
 -- | Start a new solver process.
 newSolver :: String       {- ^ Executable -}            ->
-             [String]     {- ^ Argumetns -}             ->
+             [String]     {- ^ Arguments -}             ->
              Maybe Logger {- ^ Optional logging here -} ->
              IO Solver
 newSolver exe opts mbLog =
@@ -248,7 +253,31 @@
      return solver
 
 
+-- | Load the contents of a file.
+loadFile :: Solver -> FilePath -> IO ()
+loadFile s file = loadString s =<< readFile file
 
+-- | Load a raw SMT string.
+loadString :: Solver -> String -> IO ()
+loadString s str = go (dropComments str)
+  where
+  go txt
+    | all isSpace txt = return ()
+    | otherwise =
+      case readSExpr txt of
+        Just (e,rest) -> command s e >> go rest
+        Nothing       -> fail $ unlines [ "Failed to parse SMT file."
+                                        , txt
+                                        ]
+
+  dropComments = unlines . map dropComment . lines
+  dropComment xs = case break (== ';') xs of
+                     (as,_:_) -> as
+                     _ -> xs
+
+
+
+
 -- | A command with no interesting result.
 ackCommand :: Solver -> SExpr -> IO ()
 ackCommand proc c =
@@ -302,7 +331,7 @@
 push :: Solver -> IO ()
 push proc = pushMany proc 1
 
--- | Restore to last check-point.  A sepcial case of 'popMany'.
+-- | Restore to last check-point.  A special case of 'popMany'.
 pop :: Solver -> IO ()
 pop proc = popMany proc 1
 
@@ -314,8 +343,14 @@
 popMany :: Solver -> Integer -> IO ()
 popMany proc n = simpleCommand proc [ "pop", show n ]
 
+-- | Execute the IO action in a new solver scope (push before, pop after)
+inNewScope :: Solver -> IO a -> IO a
+inNewScope s m =
+  do push s
+     m `X.finally` pop s
 
 
+
 -- | Declare a constant.  A common abbreviation for 'declareFun'.
 -- For convenience, returns an the declared name as a constant expression.
 declare :: Solver -> String -> SExpr -> IO SExpr
@@ -328,6 +363,30 @@
   do ackCommand proc $ fun "declare-fun" [ Atom f, List as, r ]
      return (const f)
 
+-- | Declare an ADT using the format introduced in SmtLib 2.6.
+declareDatatype ::
+  Solver ->
+  String {- ^ datatype name -} ->
+  [String] {- ^ sort parameters -} ->
+  [(String, [(String, SExpr)])] {- ^ constructors -} ->
+  IO ()
+declareDatatype proc t [] cs =
+  ackCommand proc $
+    fun "declare-datatype" $
+      [ Atom t
+      , List [ List (Atom c : [ List [Atom s, argTy] | (s, argTy) <- args]) | (c, args) <- cs ]
+      ]
+declareDatatype proc t ps cs =
+  ackCommand proc $
+    fun "declare-datatype" $
+      [ Atom t
+      , fun "par" $
+          [ List (map Atom ps)
+          , List [ List (Atom c : [ List [Atom s, argTy] | (s, argTy) <- args]) | (c, args) <- cs ]
+          ]
+      ]
+
+
 -- | Declare a constant.  A common abbreviation for 'declareFun'.
 -- For convenience, returns the defined name as a constant expression.
 define :: Solver ->
@@ -495,7 +554,7 @@
 int x | x < 0     = neg (int (negate x))
          | otherwise = Atom (show x)
 
--- | Real (well, reational) literals.
+-- | Real (well, rational) literals.
 real :: Rational -> SExpr
 real x = realDiv (int (denominator x)) (int (numerator x))
 
@@ -542,14 +601,20 @@
 not :: SExpr -> SExpr
 not p = fun "not" [p]
 
--- | Conjucntion.
+-- | Conjunction.
 and :: SExpr -> SExpr -> SExpr
 and p q = fun "and" [p,q]
 
+andMany :: [SExpr] -> SExpr
+andMany xs = if null xs then bool True else fun "and" xs
+
 -- | Disjunction.
 or :: SExpr -> SExpr -> SExpr
 or p q = fun "or" [p,q]
 
+orMany :: [SExpr] -> SExpr
+orMany xs = if null xs then bool False else fun "or" xs
+
 -- | Exclusive-or.
 xor :: SExpr -> SExpr -> SExpr
 xor p q = fun "xor" [p,q]
@@ -574,7 +639,10 @@
 eq :: SExpr -> SExpr -> SExpr
 eq x y = fun "=" [x,y]
 
--- | Greather-then
+distinct :: [SExpr] -> SExpr
+distinct xs = if null xs then bool True else fun "distinct" xs
+
+-- | Greater-then
 gt :: SExpr -> SExpr -> SExpr
 gt x y = fun ">" [x,y]
 
@@ -614,6 +682,9 @@
 add :: SExpr -> SExpr -> SExpr
 add x y = fun "+" [x,y]
 
+addMany :: [SExpr] -> SExpr
+addMany xs = if null xs then int 0 else fun "+" xs
+
 -- | Subtraction.
 sub :: SExpr -> SExpr -> SExpr
 sub x y = fun "-" [x,y]
@@ -639,7 +710,7 @@
 mod :: SExpr -> SExpr -> SExpr
 mod x y = fun "mod" [x,y]
 
--- | Is the number divisible by the given constante.
+-- | Is the number divisible by the given constant.
 divisible :: SExpr -> Integer -> SExpr
 divisible x n = List [ fam "divisible" [n], x ]
 
@@ -672,11 +743,11 @@
 bvAnd :: SExpr -> SExpr -> SExpr
 bvAnd x y = fun "bvand" [x,y]
 
--- | Bitwsie disjucntion.
+-- | Bitwise disjunction.
 bvOr :: SExpr -> SExpr -> SExpr
 bvOr x y = fun "bvor" [x,y]
 
--- | Bitwsie exclusive or.
+-- | Bitwise exclusive or.
 bvXOr :: SExpr -> SExpr -> SExpr
 bvXOr x y = fun "bvxor" [x,y]
 
diff --git a/simple-smt.cabal b/simple-smt.cabal
--- a/simple-smt.cabal
+++ b/simple-smt.cabal
@@ -1,5 +1,5 @@
 name:                simple-smt
-version:             0.7.1
+version:             0.8
 synopsis:            A simple way to interact with an SMT solver process.
 description:         A simple way to interact with an SMT solver process.
 license:             BSD3