Closed scungao closed 8 years ago
Check the following dr file. It's trying to see if this big function nn is close to tan near the origin. x1 is the only argument. dReal returns delta-sat saying nn can be huge. But it shouldn't be.
var: [0,0.000001] x1; [-1000,1000] nn; ctr: nn = (971257242.67759383 * (tanh((-0.83136651156762431 * x1 + -1.3890441137474736) / 2)) + -568873673.47067046 * (tanh((-0.97920630516730212 * x1 + -1.4402130368144705) / 2)) + 64153179.71628686 * (tanh((-1.1564016556640022 * x1 + -1.4695509763173511) / 2)) + -16554003040.338058 * (tanh((-0.53355710931598743 * x1 + -0.57133099279086241) / 2)) + -68921.193356639618 * (tanh((-2.0026357358830604 * x1 + -1.7438878427151638) / 2)) + 165799511.70313755 * (tanh((0.96422942263162748 * x1 + 0.64680155488885971) / 2)) + -21937186428.772785 * (tanh((0.52006010145545756 * x1 + 0.24484238547781062) / 2)) + -380152434664.20251 * (tanh((-0.020027851642538078 * x1 + -0.0054234686583924463) / 2)) + 252269158230.90063 * (tanh((-0.034771086028482959 * x1 + -0.0024616651694859492) / 2)) + -954688015.67861867 * (tanh((-0.79816358456414238 * x1 + 0.10312566694423919) / 2)) + -27899405.568769213 * (tanh((1.0186852821285755 * x1 + -0.33535493671670408) / 2)) + 6361242994.3647032 * (tanh((-0.13321747950773469 * x1 + 0.070499179490618777) / 2)) + -869154092.6946975 * (tanh((-0.71453016378715839 * x1 + 0.52103802004944) / 2)) + -1484435.2311509394 * (tanh((1.3513857684266568 * x1 + -1.2557126199391506) / 2)) + -12166786093.24052 * (tanh((-0.2247710560525841 * x1 + 0.25381230212476813) / 2)) + -2293780192.4803324 * (tanh((-0.58902903072080126 * x1 + 0.78293955125853065) / 2)) + 0); abs(tan(x1)-nn)>0.1;
Check the following dr file. It's trying to see if this big function nn is close to tan near the origin. x1 is the only argument. dReal returns delta-sat saying nn can be huge. But it shouldn't be.