sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Misc.Auxiliary

Description

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.

Synopsis

- problem :: Predicate
- allModels :: IO AllSatResult
- modelsWithYAux :: IO AllSatResult

# Documentation

problem :: Predicate Source #

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

allModels :: IO AllSatResult Source #

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

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.