Support RandomSymbol and assumptions in SMT-Lib Printer.

[kunalsheth]

References to other Issues or PRs

Brief description of what is fixed or changed

• Added support for the old assumption system.
• Added support for random variables.
• Improved error messages.

Other comments

Certain assumptions, like e.g. prime, cannot easily be automatically asserted in the SMT-Lib code. If a user passes e.g. Symbol('x', prime=True) into smtlib_code(..), should this be a log_warn or an error?

Is there any precedent set by sympy's built-in solvers for unsupported/ignored assumptions?

Release Notes

• printing
  • SMT-Lib printer now supports random variables and assumptions.

[sympy-bot]

✅

Hi, I am the SymPy bot (v169). I'm here to help you write a release notes entry. Please read the guide on how to write release notes.

Your release notes are in good order.

Here is what the release notes will look like:

• printing
  • SMT-Lib printer now supports random variables and assumptions. (#24406 by @kunalsheth)

This will be added to https://github.com/sympy/sympy/wiki/Release-Notes-for-1.12.

Click here to see the pull request description that was parsed.

<!-- Your title above should be a short description of what
was changed. Do not include the issue number in the title. -->

#### References to other Issues or PRs
<!-- If this pull request fixes an issue, write "Fixes #NNNN" in that exact
format, e.g. "Fixes #1234" (see
https://tinyurl.com/auto-closing for more information). Also, please
write a comment on that issue linking back to this pull request once it is
open. -->


#### Brief description of what is fixed or changed
- Added support for the old assumption system.
- Added support for random variables.
- Improved error messages.

#### Other comments
Certain assumptions, like e.g. `prime`, cannot easily be automatically asserted in the SMT-Lib code. If a user passes e.g. `Symbol('x', prime=True)` into `smtlib_code(..)`, should this be a `log_warn` or an error?

Is there any precedent set by sympy's built-in solvers for unsupported/ignored assumptions?

#### Release Notes

<!-- Write the release notes for this release below between the BEGIN and END
statements. The basic format is a bulleted list with the name of the subpackage
and the release note for this PR. For example:

* solvers
  * Added a new solver for logarithmic equations.

* functions
  * Fixed a bug with log of integers.

or if no release note(s) should be included use:

NO ENTRY

See https://github.com/sympy/sympy/wiki/Writing-Release-Notes for more
information on how to write release notes. The bot will check your release
notes automatically to see if they are formatted correctly. -->

<!-- BEGIN RELEASE NOTES -->

* printing
  * SMT-Lib printer now supports random variables and assumptions.

<!-- END RELEASE NOTES -->

[github-actions]

Benchmark results from GitHub Actions

Lower numbers are good, higher numbers are bad. A ratio less than 1
means a speed up and greater than 1 means a slowdown. Green lines
beginning with + are slowdowns (the PR is slower then master or
master is slower than the previous release). Red lines beginning
with - are speedups.

Significantly changed benchmark results (PR vs master)

Significantly changed benchmark results (master vs previous release)

       before           after         ratio
     [41d90958]       [c87cd361]
     <sympy-1.11.1^0>                 
-         975±4μs          635±2μs     0.65  solve.TimeSparseSystem.time_linear_eq_to_matrix(10)
-        2.78±0ms         1.17±0ms     0.42  solve.TimeSparseSystem.time_linear_eq_to_matrix(20)
-     5.55±0.02ms         1.72±0ms     0.31  solve.TimeSparseSystem.time_linear_eq_to_matrix(30)

Full benchmark results can be found as artifacts in GitHub Actions
(click on checks at the top of the PR).

[oscarbenjamin]

Is there any precedent set by sympy's built-in solvers for unsupported/ignored assumptions?

Most solvers ignore assumptions and infer the meaning based on context or docs e.g. solveset(f(x), x, Reals) assumes that you want to solve for real values of x and deliberately ignores any assumptions set on the symbol x. Only solve checks assumptions and it only does a cursory check. Personally I think it's a mistake that solve does that and it would be better to just have separate functions like solve_real and solve_complex or another explicit mechanism for distinguishing.

[oscarbenjamin]

Btw it's better to make a dedicated branch for a pull request rather than using master.

[sylee957]

How would RandomSymbol be handled in the context of smtlib?
I'm not sure if it is just some exploit to use symbols with the interval values.

[kunalsheth]

Hi! RandomSymbol is reduced to a constant within a domain, though this domain doesn't necessarily have to be an interval.

This is not an exploit because "RandomSymbol" and "Symbol with a domain" have distinct meanings:

• Symbols + Manual assertion of the domains: Does a solution exist to this system?
• Symbols + RandomSymbols: Does some set of undesirable states intersect the set of all possible outcomes?

Example:

Suppose I were reasoning about some robotic system that has noise in its sensor readings. I could write out the SMT query using Symbol and then manually assert the domains of each. But this makes our system impossible to simulate. We cannot simulate/sample() Symbols with manually encoded domains. In order to simulate, we need a combination of Symbols and RandomSymbols as these have distinct purposes. It defeats the point of automated verification to have the user simulate one system (with RandomSymbols) but then go and verify a different system (with manual domain assertions), so it is best we support RandomSymbol directly in our printer.

Also, the same argument could be made against for-loops with respect to while-loops. Sure it is possible to only use while-loops. But idiomatically, for-loops mean something different in the same way RandomSymbol means something different than just asserting a domain on a Symbol.

[sylee957]

I think that sympy old assumptions are only used correctly in the expand, rewrite, simplify interface where it needs context-free judgement.
It is deliberately ignored in the solver because the explicit context given to equation/inequality often makes assumptions redundant or makes it trivial, (let's say, x.is_positive compared to solving (x > 0) & (x < 2))

I'm not sure if it is necessarily needed, if same thing about RandomSymbol can already be done with giving a mix of equations/inequality that gives.
It can give some maintenance weight.
It can be useful for some cases where you want to manually translate the stuff like random symbols to equations, or back, or such
But I'm not sure if smt-lib distingushes semantics about the cases you describe

[sylee957]

And I'm also not sure about why things like smtlib_code(Uniform('h', 31, 41)) raise error though.

[kunalsheth]

smtlib_code(Uniform('h', 31, 41))

raises a type error for the same reason that

h = Symbol('h', real=True)
smtlib_code([
    Eq(h, 3.14),
    h
])

raises a type error.

That is, saying a value has a uniform distribution forces it to be a float, and asserting a float is a mistake.

[kunalsheth]

I think that sympy old assumptions are only used correctly in the expand, rewrite, simplify interface where it needs context-free judgement.
It is deliberately ignored in the solver because the explicit context given to equation/inequality often makes assumptions redundant or makes it trivial, (let's say, x.is_positive compared to solving (x > 0) & (x < 2))

I see. I do not want to ignore any information or constraints sent to the SMT interface, however. Would a better way to proceed be to throw an exception if any of the symbols contain assumptions?

For RVs, I think it may be possible to implement a totally separate function (maybe in the sympy.stats package) which does the domain-to-query translation independently from the SMTlib printer. Does this sound better to you? @sylee957

[sylee957]

For RVs, I think it may be possible to implement a totally separate function (maybe in the sympy.stats package) which does the domain-to-query translation independently from the SMTlib printer. Does this sound better to you? @sylee957

I'm not sure you mean by 'domain-to-query' translation though,
But I agree that the functions should be separated, such that does one function do procedure each, like type inference, dealing with random variables, which can be some pre-printing steps. Because I don't think that we should do too many things implicitly.