The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
I see. Thanks!On Saturday, July 16, 2016 at 11:58:44 PM UTC-4, gmhwxi wrote:
In this case, the constraints do not involve transcendental functions
(sin, cos, exp, etc.).
Once you have transcendental functions (and beyond), there is very little
that z3 can do.
The hope is that dReal can be used to solve such constraints effectively
in practice.
On Saturday, July 16, 2016 at 11:53:42 PM UTC-4, Steinway Wu wrote:
I’m a little confused. This is solved using z3, not using dReal, right?
So what’s the relation with dReal/dReach here?
On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
Keen. Why M1 and M2? Eyeballing it, they seem like they should instead be
testing the sign of v? Also because I think it would be good to be
testing/constraining the sign of v. As in what if / how to disallow X<=0 &&
v>0?
M1 and M2 come from the corresponding dReach model…
What the ATS code does is to make sure the model is “correctly” implemented.On Saturday, May 7, 2016 at 5:41:06 PM UTC-4, Raoul Duke wrote:
Keen. Why M1 and M2? Eyeballing it, they seem like they should instead be
testing the sign of v? Also because I think it would be good to be
testing/constraining the sign of v. As in what if / how to disallow X<=0 &&
v>0?
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
In this case, the constraints do not involve transcendental functions (sin,
cos, exp, etc.).
Once you have transcendental functions (and beyond), there is very little
that z3 can do.
The hope is that dReal can be used to solve such constraints effectively in
practice.On Saturday, July 16, 2016 at 11:53:42 PM UTC-4, Steinway Wu wrote:
I’m a little confused. This is solved using z3, not using dReal, right? So
what’s the relation with dReal/dReach here?
On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
I’m a little confused. This is solved using z3, not using dReal, right? So
what’s the relation with dReal/dReach here?On Monday, June 13, 2016 at 6:08:13 PM UTC-4, gmhwxi wrote:
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.
The graphics is uninteresting. What is interesting here is that the
differential equations governing the movement of the ball are
captured in the ATS types.