mod package:sbv
Mapping of symbolic values to constants.
Mapping of input variables as reported by the solver. Only collected
if model validation is requested.
Mapping of symbolic values to objective values.
Mapping of uninterpreted functions to association lists in the model.
Note that an uninterpreted constant (function of arity 0) will be
stored in the
modelAssocs field. Left is used when the function
returned is too difficult for SBV to figure out what it means
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.
Proof
>>> runCached modAddLeft
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Lemma: modAddRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Result: Q.E.D.
Lemma: modAddLeft
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
[Proven] modAddLeft :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
Proof
>>> runCached modAddMultiple
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
[Proven] modAddMultiple :: Ɐk ∷ Integer → Ɐn ∷ Integer → Ɐm ∷ Integer → Bool
Proof
>>> runCached modAddRight
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Lemma: modAddRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Result: Q.E.D.
[Proven] modAddRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
Proof
>>> runCached modMulLeft
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Lemma: modAddRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Result: Q.E.D.
Lemma: modAddLeft
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Cached: modAddMultiple Q.E.D.
Cached: modAddRight Q.E.D.
Inductive lemma: modMulRightNonneg
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Step: 4 Q.E.D.
Step: 5 Q.E.D.
Step: 6 Q.E.D.
Result: Q.E.D.
Cached: modAddMultiple Q.E.D.
Cached: modAddRight Q.E.D.
Cached: modAddLeft Q.E.D.
Cached: modAddMultiple Q.E.D.
Lemma: modSubRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Inductive lemma: modMulRightNeg
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Step: 4 Q.E.D.
Step: 5 Q.E.D.
Step: 6 Q.E.D.
Result: Q.E.D.
Lemma: modMulRight
Step: 1 (2 way case split)
Step: 1.1 Q.E.D.
Step: 1.2.1 Q.E.D.
Step: 1.2.2 Q.E.D.
Step: 1.2.3 Q.E.D.
Step: 1.Completeness Q.E.D.
Result: Q.E.D.
Lemma: modMulLeft
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
[Proven. Cached: modAddLeft, modAddMultiple, modAddRight] modMulLeft :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
Proof
>>> runCached modMulRight
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Lemma: modAddRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Result: Q.E.D.
Lemma: modAddLeft
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Cached: modAddMultiple Q.E.D.
Cached: modAddRight Q.E.D.
Inductive lemma: modMulRightNonneg
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Step: 4 Q.E.D.
Step: 5 Q.E.D.
Step: 6 Q.E.D.
Result: Q.E.D.
Cached: modAddMultiple Q.E.D.
Cached: modAddRight Q.E.D.
Cached: modAddLeft Q.E.D.
Cached: modAddMultiple Q.E.D.
Lemma: modSubRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Inductive lemma: modMulRightNeg
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Step: 4 Q.E.D.
Step: 5 Q.E.D.
Step: 6 Q.E.D.
Result: Q.E.D.
Lemma: modMulRight
Step: 1 (2 way case split)
Step: 1.1 Q.E.D.
Step: 1.2.1 Q.E.D.
Step: 1.2.2 Q.E.D.
Step: 1.2.3 Q.E.D.
Step: 1.Completeness Q.E.D.
Result: Q.E.D.
[Proven. Cached: modAddLeft, modAddMultiple, modAddRight] modMulRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
Proof
>>> runCached modMulRightNeg
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Lemma: modAddRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Result: Q.E.D.
Lemma: modAddLeft
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Cached: modAddMultiple Q.E.D.
Lemma: modSubRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Inductive lemma: modMulRightNeg
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Step: 4 Q.E.D.
Step: 5 Q.E.D.
Step: 6 Q.E.D.
Result: Q.E.D.
[Proven. Cached: modAddMultiple] modMulRightNeg :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
Proof
>>> runCached modMulRightNonneg
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Lemma: modAddRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Result: Q.E.D.
Lemma: modAddLeft
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Cached: modAddMultiple Q.E.D.
Cached: modAddRight Q.E.D.
Inductive lemma: modMulRightNonneg
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Step: 4 Q.E.D.
Step: 5 Q.E.D.
Step: 6 Q.E.D.
Result: Q.E.D.
[Proven. Cached: modAddRight] modMulRightNonneg :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
Proof
>>> runCached modSubRight
Inductive lemma: modAddMultiple
Step: Base Q.E.D.
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
Lemma: modSubRight
Step: 1 Q.E.D.
Step: 2 Q.E.D.
Step: 3 Q.E.D.
Result: Q.E.D.
[Proven] modSubRight :: Ɐa ∷ Integer → Ɐb ∷ Integer → Ɐm ∷ Integer → Bool
Various SMT results that we can extract models out of.
Demonstrates use of programmatic model extraction. When programming
with SBV, we typically use
sat/
allSat calls to compute
models automatically. In more advanced uses, however, the user might
want to use programmable extraction features to do fancier
programming. We demonstrate some of these utilities here.
Underlying type for SMTLib arrays, as a list of key-value pairs, with
a default for unmapped elements. Note that this type matches the
typical models returned by SMT-solvers. When we store the array, we do
not bother removing earlier writes, so there might be duplicates. That
is, we store the history of the writes. The earlier a pair is in the
list, the "later" it is done, i.e., it takes precedence over the
latter entries.
Rounding mode to be used for the IEEE floating-point operations. Note
that Haskell's default is
RoundNearestTiesToEven. If you use a
different rounding mode, then the counter-examples you get may not
match what you observe in Haskell.
In a
allSat call, return at most this many models. If nothing,
return all.
Did we reach the user given model count limit?
Given an
allSat call, we typically want to iterate over it and
print the results in sequence. The
displayModels function
automates this task by calling
disp on each result,
consecutively. The first
Int argument to
disp 'is the
current model number. The second argument is a tuple, where the first
element indicates whether the model is alleged (i.e., if the solver is
not sure, returning Unknown). The arrange argument can sort the
results in any way you like, if necessary.
Return all the models from an
allSat call, similar to
extractModel but is suitable for the case of multiple results.