    -----------------------------------------------------------------------------
    -- |
    -- 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.
    -----------------------------------------------------------------------------

    {-# LANGUAGE OverloadedStrings #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    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 :: Predicate
    problem = do SBV Integer
    x <- String -> Symbolic (SBV Integer)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "x"
                 SBV Integer
    y <- String -> Symbolic (SBV Integer)
    forall a. SymVal a => String -> Symbolic (SBV a)
    free String
    "y"
                 SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV Integer
    x SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .>= SBV Integer
    0
                 SBool -> SymbolicT IO ()
    forall a. QuantifiedBool a => a -> SymbolicT IO ()
    forall (m :: * -> *) a.
    (SolverContext m, QuantifiedBool a) =>
    a -> m ()
    constrain (SBool -> SymbolicT IO ()) -> SBool -> SymbolicT IO ()
    forall a b. (a -> b) -> a -> b
    $ SBV Integer
    x SBV Integer -> SBV Integer -> SBool
    forall a. OrdSymbolic a => a -> a -> SBool
    .<= SBV Integer
    1
                 SBool -> Predicate
    forall a. a -> SymbolicT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SBool -> Predicate) -> SBool -> Predicate
    forall a b. (a -> b) -> a -> b
    $ SBV Integer
    x SBV Integer -> SBV Integer -> SBV Integer
    forall a. Num a => a -> a -> a
    - SBV Integer -> SBV Integer
    forall a. Num a => a -> a
    abs SBV Integer
    y SBV Integer -> SBV Integer -> SBool
    forall a. EqSymbolic a => a -> a -> SBool
    .== (SBV Integer
    0 :: SInteger)

    -- | Generate all satisfying assignments for our problem. We have:
    --
    -- >>> allModels
    -- Solution #1:
    --   x =  1 :: Integer
    --   y = -1 :: Integer
    -- Solution #2:
    --   x = 1 :: Integer
    --   y = 1 :: Integer
    -- Solution #3:
    --   x = 0 :: Integer
    --   y = 0 :: 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 :: IO AllSatResult
    allModels = Predicate -> IO AllSatResult
    forall a. Satisfiable a => a -> IO AllSatResult
    allSat Predicate
    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 = 1 :: Integer
    -- Solution #2:
    --   x = 0 :: 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 :: IO AllSatResult
    modelsWithYAux = SMTConfig -> Predicate -> IO AllSatResult
    forall a. Satisfiable a => SMTConfig -> a -> IO AllSatResult
    allSatWith SMTConfig
    z3{isNonModelVar :: String -> Bool
    isNonModelVar = (String -> [String] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String
    "y"])} Predicate
    problem