Using symbolica with automated theorem provers

[nkrusch]

Hello, thanks a lot for this *very nice* library! I am using Symbolica for a research implementation, and I am finding it absolutely necessary for what I want to accomplish, as I am working in Rust.

My use case involves generating symbolic logical expressions on variables. For example, let's assume I have (somehow) generated the following two expressions: $x = 0$ and $x ≤ 0$. Up to this point everything works very nicely with Symbolica. As a next step, I want to do some reasoning over the expressions. For example, because I know $x = 0$, I can eliminate the weaker redundant expression $x ≤ 0$, based on a proof that is easy to discover with an SMT solver.

To run a solver and obtain the proof, I must translate the expressions out of Atom type to a different language. My intuition is to use the pattern matching over AtomView to implement the conversion (ref: "Walking the expression tree" example). Even more naively, I can output an Atom as a string, and then just parse from there to a different language. I am just wondering if there is some more obvious/efficient/recommended way to convert out of Atom type?

The grammar of the expressions I am considering is simple. In fact, I am only concerned with handling what appears on the left-hand-side of the expressions. There I have free variables, standard operators ($+$, $-$, $\times$, $\div$, ^), and "custom" functions min, max. Therefore, the conversion is doable, and fairly simple, just wondering about the best practices.