search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

Cleaner output of dReach variables with --verbose #6

Open markerazo opened 10 years ago

markerazo commented 10 years ago

dReal currently prints calculated intervals of each variable at every time step during computation. For example,

[0.734523,0.734525] {[2999.98,3000],[-1.50824e-14,1.50824e-14],[-3000,-2999.98],
[-0.00110029,-0.00109605],[-0.00467694,-0.00467153],[6.91665,6.91667],[0.642616,0.642622],
[442.218,442.225],[-2.04482e-14,2.04482e-14],[0.734523,0.734525],[-442.225,-442.218],
[-0.000634133,-0.000634096],[-0.00211078,-0.00211075],[2.60351,2.60353]}

Despite printing out this information, the intervals are not labeled and occasionally change order when being printed, making the majority of variables unidentifiable for the majority of the computation history. Although the end of the computation prints the intervals next to their respective variables:

(The interval on d_phi_0_t: [648.058,648.08]);

added labels during computation (or more orderly printed intervals) would allow us to make more use of these printouts.

soonhokong commented 10 years ago

Thanks @markerazo, I'll work on it later. BTW, I've updated your comment by syntax-highlighting the output of dReal. I think it's a useful thing to know.