query package:sbv
A query is a user-guided mechanism to directly communicate and extract
results from the solver.
If
verbose is
True, print the message, useful for
debugging messages in custom queries. Note that
redirectVerbose
will be respected: If a file redirection is given, the output will go
to the file.
NB. For a version which generalizes over the underlying monad, see
queryDebug
In our first query we'll define a constraint that will not be known to
the shared or second query and then solve for an answer that will
differ from the first query. Note that we need to pass an MVar in so
that we can operate on the shared variables. In general, the variables
you want to operate on should be defined in the shared part of the
query and then passed to the children queries via channels, MVars, or
TVars. In this query we constrain x to be less than y and then return
the sum of the values. We add a threadDelay just for demonstration
purposes
In the second query we constrain for an answer where y is smaller than
x, and then return the product of the found values.
Triggered from inside SBV
The state we keep track of as we interact with the solver
A query is a user-guided mechanism to directly communicate and extract
results from the solver. A generalization of
Query.
A query is a user-guided mechanism to directly communicate and extract
results from the solver. A generalization of
Query.