Support for trigonometric functions

[LeventErkok]

Z3 has limited support for trig functions, see here: https://github.com/Z3Prover/z3/issues/680

Would be interesting to see if we can target these; shouldn't be too hard.

Also, the dReal solver has support for δ-satisfiability and handles trigonometry much better with that caveat. This would require adding a dsat function perhaps, but would be nice to have support for it too: http://dreal.github.io/

[LeventErkok]

Due to types, we can only do this reasonably with SReal; but currently we don't have a Floating AlgReal instance. Adding one would skip so many elements of that it's a half-hearted effort anyhow. Better leave this if someone really has a use-case.

[georgefst]

Better leave this if someone really has a use-case.

Well, hello there.

Any thoughts on this? Obviously Floating AlgReal doesn't really make any sense, given some of the functions defined in that class. Although, aren't there already similar cases where SBV has to cede to Haskell's less-than-perfect numeric typeclass hierarchy?

Incidentally, is it actually currently possible to use dReal with SBV?

[LeventErkok]

It's certainly possible to add functions sin, cos, tan :: SReal -> SReal and put it in a separate module and import qualified to avoid clashes. We already do that for sequences, for instance. The main issue is there is no official SMTLib semantics for these functions, so it's hard to generalize. I'm not sure what the current state of the implementation is in z3, nor I'm aware of any other solver that supports these. If you want to add and experiment, I'd be more than happy to help. Please submit a pull request!

Regarding dReal: I never wrote bindings for it in SBV, but assuming it plays by the rules of SMTLib, it should not be hook it up, so far as the SMTLib subset is concerned. For instance, this is all the code needed to hook up MathSAT to SBV: https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Provers/MathSAT.hs and I'd expect the dReal integration would be about the same size; assuming it's SMTLib compliant.

The more interesting would be to actually implement dSat command in SBV, and that would take more work, but would be a fun project indeed. I'm happy to advise if you start doing that and need any help. (You'd start by defining a DSatResult type, just like we have SatResult, ThmResult, etc.)

[LeventErkok]

I've started looking into this, in the branch dReal: https://github.com/LeventErkok/sbv/tree/dReal

Unfortunately, looks like dReal folks aren't quite SMTLib compliant quite yet, so filed two issues:

https://github.com/dreal/dreal4/issues/207 https://github.com/dreal/dreal4/issues/206

Once they address these issues, SBV should be able to start communicating with it and we can think about how to support a dSat command.

[georgefst]

Wow, thanks for taking a look at this. At this point, this is just somewhere on the horizon for my project (it came up in a conversation earlier this week that we will at some point need to be able to analyse trig functions, and that if so we'd want to use dReal), but it would be great if it were possible within SBV.

I'd be happy to help where I can, although it would probably be at least a few weeks before it becomes enough of a priority for me to devote much time to it.

[LeventErkok]

@georgefst At this point the most helpful thing you can do is actually help dReal folks to resolve the two tickets I filed. (See above.) Once they do that, the SBV side should be fairly easy to handle.

[LeventErkok]

Made some progress on this, but currently stuck due to https://github.com/dreal/dreal4/issues/217

[LeventErkok]

Update: Continuing work on this; we now have:

Prelude Data.SBV> proveWith dReal $ \x -> x .== (x::SReal)
Q.E.D.

But we can't quite parse models yet:

Prelude Data.SBV> satWith dReal $ \x -> x .== (x::SReal)
*** Exception:

[LeventErkok]

TODO list:

• Which logics does dreal support? Essentially fill out the "capabilities" matrix
• Check if they support bitvectors; if not, we'll have to add a capability for that and reject accordingly
• Implement a dSat function that calls dRealwith the specified precision
• Handle models

[soonho-tri]

I guess I can answer some:

Which logics does dreal support? Essentially fill out the "capabilities" matrix

Based on QF_NRA, we extend it to allow integer variables and a set of nonlinear functions.

Check if they support bitvectors; if not, we'll have to add a capability for that and reject accordingly

We don't support it. We don't have a plan to work on it either.

[LeventErkok]

@soonho-tri Thanks! That's really helpful. Much appreciated.

[soonho-tri]

Happy to help.

BTW, if you have difficulties in handling and parsing models and want to change the output format from dReal, please let me know. I was not sure it's acceptable to use [] to represent intervals in LISP..

[LeventErkok]

Indeed, that'll be the next one thing to tackle. In general, everything has to be an s-expression. I suggest something like:

(interval low high)

If you have open/close bounds, which I suppose you do, you can do:

(interval (open low) (closed high))

etc. Something like:

(interval (open 0.0) (closed 1.0))

to represent the interval (0 1].

Also, if dreal determines that a value is fixed (i.e., low = high), then it'd be nice if it printed:

(exact value)

[soonho-tri]

FYI, in dReal, every interval is a closed interval. I'll make the following change:

• [lb, ub] => (interval lb ub).
• [c, c] => (exact c)

[soonho-tri]

Implemented in https://github.com/dreal/dreal4/commit/16bbd5d64bd25e1cd5c83df3f9ca5b1074da1b40

[LeventErkok]

@soonho-tri

Great! Thanks..

A question: Does dreal support uninterpreted functions?

[soonho-tri]

Does dreal support uninterpreted functions?

No.

[LeventErkok]

Thanks!

[LeventErkok]

Update: Basic infrastructure in place, now need to handle models.

[LeventErkok]

Update: We can now handle "exact" solutions coming out of dReal. For interval values, I need to think about how to represent them as legitimate SBV objects. Will require some design work. But so far so good!

[LeventErkok]

@soonho-tri

Hi Soonho,

I see that dReal prints values in scientific notation, like this:

(s0 (exact 1.7976931348623157e+308))

This is hard to process by upstream solvers, is it a regular double value? Almost implies there's some sort of inherent limitation on the bound of values for reals, which I don't believe is true.

For this cases, it's much better to use the usual rational representation if you can. Something like:

(s0 (exact (/ numerator denominator)))

where numerator and denominator are arbitrary integers that represent the real value as a fraction. (Assuming dreal only handles proper fractions, which is presumably the case.)

Can you print values in this format instead? Again, it'd be perfectly fine if you want to tie this to a command-line switch.

[soonho-tri]

• Internally, dReal uses a double interval to approximate a real value.
• To be "exact" and lossless, I think it's best to output a FP constant in the hexadecimal FP format (using %a format-specifier). What do you think?

[LeventErkok]

That's interesting. So, how do you handle cases where the real value is larger than what an IEEE754 double-precision float can represent? I can easily ask: Give me a real that's larger than 10^400, what happens then?

I'm assuming dreal doesn't deal with transcendentals. (No way to really compute pi, e, etc.) And it also cannot deal with algebraic reals (i.e., roots of polynomials, such as sqrt(2)). So, all the reals it can compute with actually are rationals. In that case, you can always represent the value as the division of two unbounded integers. And the standard way SMTLib represents such values is by a simple fraction of them. (See here: http://smtlib.cs.uiowa.edu/theories-Reals.shtml) So, I suggest sticking to that notation for consistency.

[LeventErkok]

Also related, for integer values, you should print them without any 0's: I see:

  (s0 (exact 805306369.0))

for the benchmark:

(set-option :smtlib2_compliant true)
(set-option :produce-models true)
(set-logic ALL) ; has unbounded values, using catch-all.
(declare-fun s1 () Int) (assert (= s1 2))
(declare-fun s0 () Int)
(declare-fun s2 () Bool) (assert (= s2 (> s0 s1)))
(assert s2)
(check-sat)

would be great to have this value printed without the suffix .0.

While we're at it: I assume dReal will always produce an exact value for a boolean or an unbounded integer, correct? Or, are integers not unbounded?

[soonho-tri]

That's interesting. So, how do you handle cases where the real value is larger than what an IEEE754 double-precision float can represent? I can easily ask: Give me a real that's larger than 10^400, what happens then?

The theory behind dReal assumes that every variable is bounded. In dReal, we assume that every unbounded variable and intermediate values have the range of IEEE754 double-precision FP. Extending dReal to use a multi-precision FP library such as MPFR is on our TODO list, but we haven't had time to work on it yet.

I'm assuming dreal doesn't deal with transcendentals. (No way to really compute pi, e, etc.) And it also cannot deal with algebraic reals (i.e., roots of polynomials, such as sqrt(2)). So, all the reals it can compute with actually are rationals.

FYI, it supports sin and sqrt, and one can write:

(set-logic QF_NRA)
(declare-fun x () Real)
(assert (< 3 x))
(assert (< x 4))
(assert (= (sin x) 0))
(declare-fun y () Real)
(assert (= (sqrt 2) y))
(check-sat)
(get-value (x y))
(exit)

which approximate the values of pi and sqrt(2) as follows:

(
    (x (interval 3.141592653589793 3.1415926535897936))
    (y (interval 1.414213562373095 1.4142135623730954))
)

So, all the reals it can compute with actually are rationals. In that case, you can always represent the value as the division of two unbounded integers. And the standard way SMTLib represents such values is by a simple fraction of them. (See here: http://smtlib.cs.uiowa.edu/theories-Reals.shtml) So, I suggest sticking to that notation for consistency.

I guess there is a way to use a function in GMP to convert a double to a GMP rational. I'll check things.

Also related, for integer values, you should print them without any 0's: I see: (s0 (exact 805306369.0))

Thanks for the report. I'll fix that. I'll also check the Boolean case and a test case.

By the way, I think (var (exact c)) is redundant and we can reduce it to (var c). We only need (interval lb ub) when c is an interval.

[LeventErkok]

Does this mean the unbounded-integer's (i.e., SMTLib's Int type) are limited to the range of an IEEE-754 double as well?

Agreed on the redundancy of exact; it wouldn't hurt to keep it there, but you can remove it. To reiterate, you'll never print an interval for a boolean or an integer value, correct? (i.e., the only time I'll see an interval is if the variable is of type Real.)

[soonho-tri]

Does this mean the unbounded-integer's (i.e., SMTLib's Int type) are limited to the range of an IEEE-754 double as well?

Yes, that's the case. To be safe, it's bounded by the range of int32 as there are integers in (MAX_INT, MAX_DOUBLE] range that can't be represented as a double.

To reiterate, you'll never print an interval for a boolean or an integer value, correct?

Correct. I'll ping you here when the implementation is updated.

[LeventErkok]

Thanks that's very helpful. Looking forward to the update.

[soonho-tri]

https://github.com/dreal/dreal4/commit/080c794067a4ed73c5712f9f8152f634bf7d71c5 addresses the issue.

Input:

(set-logic QF_NRA)
(set-option :smtlib2_compliant true)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(declare-fun i () Int)
(declare-fun b1 () Bool)
(declare-fun b2 () Bool)

(assert (< 3 x))
(assert (< x 4))
(assert (= (sin x) 0))
(assert (= (sqrt 2) y))
(assert (= z (/ (* 3 4) 2)))
(assert (= i (/ (* 3 4) 4)))
(assert (= b1 (and (> x y)
           (> y z))))
(assert (= b2 (or (> x y)
          (> y z))))

(check-sat)
(get-value (x y z i b1 b2))

(exit)

Output:

delta-sat
(
    (x (interval (884279719003555 / 281474976710656) (7074237752028441 / 2251799813685248)))
    (y (interval (1592262918131443 / 1125899906842624) (3184525836262887 / 2251799813685248)))
    (z 6)
    (i 3)
    (b1 false)
    (b2 true)
)

[LeventErkok]

Great! One issue: An sExpr is essentially a prefix form. That is (2 / 3) should really be (/ 2 3). Can you change that?

[LeventErkok]

Another request: I understand that all dReal intervals are closed on both ends. But it'd be nice to make this explicit in the output: I can imagine other solvers also returning intervals with open/close boundaries. I'm open to other ideas for expressing this as well; if there's some other well-established syntax. A simple option is:

(interval (open low) (closed high))

etc.; with dreal always outputting (interval (closed low) (closed high)). What do you think?

[soonho-tri]

I agree. How does the following output look?

delta-sat
(
    (x (interval (closed (/ 884279719003555 281474976710656)) (closed (/ 7074237752028441 2251799813685248))))
    (y (interval (closed (/ 1592262918131443 1125899906842624)) (closed (/ 3184525836262887 2251799813685248))))
    (z 6)
    (i 3)
    (b1 false)
    (b2 true)
)

[LeventErkok]

@soonho-tri Yes, I think that'd work nicely. Is this committed yet?

[soonho-tri]

Great!

Is this committed yet?

Yes. PTAL https://github.com/dreal/dreal4/commit/cf3472bde4f21deab759f9ec29f48c1be10ee8df and https://github.com/dreal/dreal4/commit/b42bb1a3c63c50425260f678ca1a6dea1c5448f3.

[LeventErkok]

Great! This works just fine now:

Data.SBV> dsat $ \x -> x .> (2::SReal) .&& x .< (3::SReal)
Delta satisfiable, precision: 0.001. Model:
  s0 = [2.374499999999999833022457096376456320285797119140625, 2.375500000000000166977542903623543679714202880859375] :: Real

[soonho-tri]

Great!

I can release a new version of dReal and update the homebrew formula. I just want to make sure that you don't have further feature-requests or bug reports.

[LeventErkok]

@soonho-tri

Ah, I spoke too soon! When you print negative values in SMTLib, you have to explicitly parenthesize them. Currently, you are printing:

     (
        (s0 (interval (closed (/ -8162775450508931 2251799813685248)) (closed (/ -8162773198709117 2251799813685248))))
       )

The literal in there should be:

(/ (- 8162775450508931) 2251799813685248)

Note the parenthesized negation.

[LeventErkok]

@soonho-tri

If you fix the negated literals, I think it'd be a release candidate for sure. I still need to hook up trigonometric functions and see if there are other things to sort out, but we at least have a proper communication channel now.

[LeventErkok]

@soonho-tri

Note that negation is also required for integer literals, not just the rationals.

In general, if you're putting out a negative literal, you put it out as (- x) where x has no plus/minus sign in front.

[soonho-tri]

Added https://github.com/dreal/dreal4/commit/ba5ff2a6f5220ea368ae63b9e8a92f9ce98412cc.

[LeventErkok]

Looks great! Please go ahead with the homebrew update if you like; I'll be playing with the trigonometric function support later this week. Cheers, and thanks for all the help.

[soonho-tri]

FYI, dreal-4.20.08.1 is out. I've also updated its homebrew formula.

[LeventErkok]

@soonho-tri Great! thanks.

[LeventErkok]

SBV now supports trigonometric functions via dReal/dSat. Closing this ticket.