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