diff --git a/SAT.cabal b/SAT.cabal
index 0eb12ca..94a50d5 100644
--- a/SAT.cabal
+++ b/SAT.cabal
@@ -22,6 +22,9 @@ library
                     , Theory.NonLinearRealArithmatic.Interval
                     , Theory.NonLinearRealArithmatic.Polynomial
                     , Theory.NonLinearRealArithmatic.IntervalConstraintPropagation
+                    , Theory.NonLinearRealArithmatic.Subtropical
+                    , Theory.NonLinearRealArithmatic.VirtualSubstitution
+                    , Theory.NonLinearRealArithmatic.CAD
     other-modules:    Utils
     build-depends:    base ^>=4.14.3.0
                     , megaparsec
diff --git a/src/Theory/NonLinearRealArithmatic/CAD.hs b/src/Theory/NonLinearRealArithmatic/CAD.hs
new file mode 100644
index 0000000..53bdc57
--- /dev/null
+++ b/src/Theory/NonLinearRealArithmatic/CAD.hs
@@ -0,0 +1,5 @@
+-- |  
+-- Cylindrical Algebraic Decomposition
+--
+module Theory.NonLinearRealArithmatic.CAD where
+
diff --git a/src/Theory/NonLinearRealArithmatic/IntervalConstraintPropagation.hs b/src/Theory/NonLinearRealArithmatic/IntervalConstraintPropagation.hs
index 39845cb..12ee504 100644
--- a/src/Theory/NonLinearRealArithmatic/IntervalConstraintPropagation.hs
+++ b/src/Theory/NonLinearRealArithmatic/IntervalConstraintPropagation.hs
@@ -1,4 +1,3 @@
-
 -- |
 -- We are given a list of non-linear real constraints and an 
 -- interval domain for each variable that appears in one of the constraints. 
@@ -106,7 +105,6 @@ eval var_domains expr = Interval.reduce $
       value2 <- eval var_domains expr2
       evalBinaryOp op_symbol value1 value2
 
-
 -- | List of variables paired with their positive integer exponents.
 type Monomial = [(Var, Int)]
 
@@ -227,31 +225,42 @@ solveFor = undefined
 
 -- | 
 preprocess :: forall a. (Ord a, Num a, Bounded a, Floating a) => [Constraint a] -> [Constraint a]
-preprocess constraints = undefined -- TODO
-  where
-    (_, all_expressions) = unzip constraints
+preprocess constraints = do
+  -- Identify largest used variable ID, to generate fresh variables.
+  let max_var = maximum (maximum . varsIn . snd <$> constraints)
 
-    -- Identify largest used variable ID, to generate fresh variables.
-    max_var = maximum (maximum . varsIn <$> all_expressions)
+  (rel, expr) <- constraints
 
-    go :: Var -> Constraint a -> [Constraint a]
-    go max_var (rel, expr) = (rel, new_expr) : []
-      where
-        (linear_terms, non_linear_terms) = L.partition (isLinear . snd) (normalize expr)
+  let terms = normalize expr
+      (linear_terms, non_linear_terms) = L.partition (isLinear . snd) terms
+
+  (new_var, non_linear_term) <- zip [max_var+1 ..] non_linear_terms
+  
+  []
 
-        new_vars = [ max_var+i | i <- [1 .. length non_linear_terms] ]
+  -- where
+  --   (_, all_expressions) = unzip constraints
 
-        f :: Var -> (a, Monomial) -> (a, Monomial)
-        f new_var (coeff, _) = (coeff, [(new_var, 1)])
+  --   max_var = maximum (maximum . varsIn <$> all_expressions)
+
+  --   go :: Var -> Constraint a -> [Constraint a]
+  --   go max_var (rel, expr) = (rel, new_expr) : []
+  --     where
+  --       (linear_terms, non_linear_terms) = L.partition (isLinear . snd) (normalize expr)
+
+  --       new_vars = [ max_var+i | i <- [1 .. length non_linear_terms] ]
+
+  --       f :: Var -> (a, Monomial) -> (a, Monomial)
+  --       f new_var (coeff, _) = (coeff, [(new_var, 1)])
         
-        new_expr = denormalize $ linear_terms <> zipWith f new_vars non_linear_terms
+  --       new_expr = denormalize $ linear_terms <> zipWith f new_vars non_linear_terms
 
-    new_constraint :: VarDomains a -> Var -> Monomial -> Constraint a
-    new_constraint var_domains new_var monomial = (Equals, BinaryOp Sub (Var new_var) monomial_expr)
-      where
-        monomial_expr = denormalize [(1, monomial)]
+  --   new_constraint :: VarDomains a -> Var -> Monomial -> Constraint a
+  --   new_constraint var_domains new_var monomial = (Equals, BinaryOp Sub (Var new_var) monomial_expr)
+  --     where
+  --       monomial_expr = denormalize [(1, monomial)]
 
-        new_var_domain = eval var_domains monomial_expr
+  --       new_var_domain = eval var_domains monomial_expr
 
 contract :: forall a. (Ord a, Bounded a, Floating a) => VarDomains a -> [Constraint a] -> VarDomains a
 contract var_domains0 = foldr go var_domains0 . preprocess
diff --git a/src/Theory/NonLinearRealArithmatic/Subtropical.hs b/src/Theory/NonLinearRealArithmatic/Subtropical.hs
new file mode 100644
index 0000000..8aa0dc3
--- /dev/null
+++ b/src/Theory/NonLinearRealArithmatic/Subtropical.hs
@@ -0,0 +1 @@
+module Theory.NonLinearRealArithmatic.Subtropical where
diff --git a/src/Theory/NonLinearRealArithmatic/VirtualSubstitution.hs b/src/Theory/NonLinearRealArithmatic/VirtualSubstitution.hs
new file mode 100644
index 0000000..842b49f
--- /dev/null
+++ b/src/Theory/NonLinearRealArithmatic/VirtualSubstitution.hs
@@ -0,0 +1 @@
+module Theory.NonLinearRealArithmatic.VirtualSubstitution where