Documentation.SBV.Examples.Misc.Auxiliary

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.

Documentation

problem :: Predicate

A simple predicate, based on two variables x and y, true when 0 <= x <= 1 and x - abs y is 0.

allModels :: IO AllSatResult

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.

modelsWithYAux :: IO AllSatResult

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.