-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.Misc.Auxiliary
-- Author    : 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