diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014, Dillon Huff
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Dillon Huff nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Smooth.cabal b/Smooth.cabal
new file mode 100644
--- /dev/null
+++ b/Smooth.cabal
@@ -0,0 +1,22 @@
+-- Initial Smooth.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                Smooth
+version:             0.1.0.1
+synopsis:            A tiny, lazy SMT solver
+description:         A tiny, lazy SMT solver. This solver is based on algorithms
+		     described in 'Decision Procedures: An Algorithmic Point of View'
+license:             BSD3
+license-file:        LICENSE
+author:              Dillon Huff
+maintainer:          dillonhuff@gmail.com
+-- copyright:           
+category:            Math
+build-type:          Simple
+cabal-version:       >=1.8
+
+library
+  exposed-modules:     Smooth.LazyBasicSMT
+  -- other-modules:
+  build-depends:       base ==4.6.*, containers ==0.5.*, FirstOrderTheory ==0.1.*, Proper ==0.5.*, DifferenceLogic ==0.1.*, HUnit ==1.2.*
+  hs-source-dirs:      src
diff --git a/src/Smooth/LazyBasicSMT.hs b/src/Smooth/LazyBasicSMT.hs
new file mode 100644
--- /dev/null
+++ b/src/Smooth/LazyBasicSMT.hs
@@ -0,0 +1,47 @@
+module Smooth.LazyBasicSMT(
+  lazyBasicSMT) where
+
+import Data.List as L
+import Data.Map as M
+import Data.Set as S
+
+import FirstOrderTheory.Syntax as Fol
+import FirstOrderTheory.Theory
+import Proper.Clause as Prop
+import Proper.CNF
+
+-- |A simple, lazy SMT solver based on Algorithm 11.2.1
+-- on page 245 of 'Decision Procedures: An Algorithmic Point of View'
+lazyBasicSMT :: (FirstOrderTheory t) =>
+                t ->
+                NNFFormula ->
+                Bool
+lazyBasicSMT theory formula = trySAT theory cnfFormula
+  where
+    cnfFormula = toPropositionalCNF formula
+
+trySAT :: (FirstOrderTheory t) => t -> CNF Literal -> Bool
+trySAT theory cnfForm = case formIsSat of
+  True -> case assignmentIsSatInTheory of
+    True -> True
+    False -> trySAT theory (addClause propLemma cnfForm)
+  False -> False
+  where
+    (formIsSat, satisfyingAsg) = case naiveSAT cnfForm of
+      Just asg -> (True, asg)
+      _ -> (False, M.empty)
+    literals = buildClauseFromSatAsg satisfyingAsg
+    (assignmentIsSatInTheory, lemma) = decideSat theory literals
+    propLemma = clause $ L.map propNegates $ S.toList lemma
+
+propNegates :: Literal -> Prop.Atom Literal
+propNegates l = case isNeg l of
+  True -> negation $ Prop.lit $ Fol.lit $ Fol.getAtom l
+  False -> Prop.lit l
+
+buildClauseFromSatAsg :: Map Literal Bool -> Set Literal
+buildClauseFromSatAsg lits = S.fromList $ L.map negateFalseLit $ M.toList lits
+
+negateFalseLit :: (Literal, Bool) -> Literal
+negateFalseLit (l, True) = l
+negateFalseLit (l, False) = Fol.negateLit l