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 directory is renamed as follows: >>> >>> >>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/CPS/DREACH/SCRATCH/bouncing_ball >>> >>> Also, the constraints can now be solved if they are passed to >>> patsolve_z3. >>> >>> On Wednesday, May 11, 2016 at 11:39:09 PM UTC-4, gmhwxi wrote: >>>> >>>> I skipped the constraint-solving part, which needs to be exported to Z3. >>>> >>>> On Wednesday, May 11, 2016 at 11:36:34 PM UTC-4, Artyom Shalkhakov >>>> wrote: >>>>> >>>>> On Thursday, May 12, 2016 at 5:56:56 AM UTC+6, gmhwxi wrote: >>>>>> >>>>>> Adding a 2d-oscillator example: >>>>>> >>>>>> >>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/ >>>>>> >>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/oscillator/oscillator_2d_anim.html >>>>>> >>>>>> >>>>> What's this for? >>>>> >>>>> prval () = >>>>> $UN.prop_assert{false}() >>>>> >>>>> >>>>> >>>>> Is it asserting falsity? >>>>> >>>>> On Wednesday, May 11, 2016 at 7:54:58 PM UTC-4, gmhwxi wrote: >>>>>>> >>>>>>> Renaming Github to GitHub: >>>>>>> >>>>>>> >>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/ >>>>>>> >>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html >>>>>>> >>>>>>> http://www.cs.bu.edu/~hwxi/GitHub/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html >>>>>>> >>>>>>> >>>>>>> On Saturday, May 7, 2016 at 3:50:21 PM UTC-4, gmhwxi wrote: >>>>>>>> >>>>>>>> >>>>>>>> I'd like to report an interesting example of using types in ATS. >>>>>>>> >>>>>>>> Here are two animations of bouncing balls: >>>>>>>> >>>>>>>> >>>>>>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/ >>>>>>>> >>>>>>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_anim.html >>>>>>>> >>>>>>>> http://www.cs.bu.edu/~hwxi/Github/ATS-Postiats-contrib/projects/LARGE/DREACH/SCRATCH/bouncing_ball/bouncing_ball_with_drag_anim.html >>>>>>>> >>>>>>>> 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. >>>>>>>> >>>>>>>> Cheers! >>>>>>>> >>>>>>>>
-- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/8a958078-8a5e-48a5-88ea-720cf0ce9fd4%40googlegroups.com.
