    -----------------------------------------------------------------------------
    -- |
    -- Module      :  Documentation.SBV.Examples.Misc.Auxiliary
    -- Copyright   :  (c) Levent Erkok
    -- License     :  BSD3
    -- Maintainer  :  erkokl@gmail.com
    -- Stability   :  experimental
    --
    -- Demonstrates model construction with auxiliary variables. Sometimes we
    -- need to introduce a variable in our problem as an existential variable,
    -- but it's "internal" to the problem and we do not consider it as part of
    -- the solution. Also, in an `allSat` scenario, we may not care for models
    -- that only differ in these auxiliaries. SBV allows designating such variables
    -- as `isNonModelVar` so we can still use them like any other variable, but without
    -- considering them explicitly in model construction.
    -----------------------------------------------------------------------------

    module Documentation.SBV.Examples.Misc.Auxiliary where

    import Data.SBV

    -- | A simple predicate, based on two variables @x@ and @y@, true when
    -- @0 <= x <= 1@ and @x - abs y@ is @0@.
    problem :: Predicate
    problem = do x <- free "x"
                 y <- free "y"
                 constrain $ x .>= 0
                 constrain $ x .<= 1
                 return $ x - abs y .== (0 :: SInteger)

    -- | Generate all satisfying assignments for our problem. We have:
    --
    -- >>> allModels
    -- Solution #1:
    --   x = 0 :: Integer
    --   y = 0 :: Integer
    -- Solution #2:
    --   x = 1 :: Integer
    --   y = 1 :: Integer
    -- Solution #3:
    --   x =  1 :: Integer
    --   y = -1 :: Integer
    -- Found 3 different solutions.
    --
    -- Note that solutions @2@ and @3@ share the value @x = 1@, since there are
    -- multiple values of @y@ that make this particular choice of @x@ satisfy our constraint.
    allModels :: IO AllSatResult
    allModels = allSat problem

    -- | Generate all satisfying assignments, but we first tell SBV that @y@ should not be considered
    -- as a model problem, i.e., it's auxiliary. We have:
    --
    -- >>> modelsWithYAux
    -- Solution #1:
    --   x = 0 :: Integer
    -- Solution #2:
    --   x = 1 :: Integer
    -- Found 2 different solutions.
    --
    -- Note that we now have only two solutions, one for each unique value of @x@ that satisfy our
    -- constraint.
    modelsWithYAux :: IO AllSatResult
    modelsWithYAux = allSatWith z3{isNonModelVar = (`elem` ["y"])} problem