test(nra_ode): add kquine_04

related issue: #114

src/tests/nra_ode/kquine_04.smt2

@@ -0,0 +1,102 @@
+(set-logic QF_NRA_ODE)
+(declare-fun xRDR () Real)
+(declare-fun xAIL () Real)
+(declare-fun tau () Real)
+(declare-fun rRDR () Real)
+(declare-fun rAIL () Real)
+(declare-fun r () Real)
+(declare-fun psi () Real)
+(declare-fun phi () Real)
+(declare-fun p () Real)
+(declare-fun gRDR () Real)
+(declare-fun gDir () Real)
+(declare-fun gAIL () Real)
+(declare-fun beta () Real)
+(declare-fun xRDR_0_0 () Real)
+(declare-fun xRDR_0_t () Real)
+(declare-fun xAIL_0_0 () Real)
+(declare-fun xAIL_0_t () Real)
+(declare-fun tau_0_0 () Real)
+(declare-fun tau_0_t () Real)
+(declare-fun rRDR_0_0 () Real)
+(declare-fun rRDR_0_t () Real)
+(declare-fun rAIL_0_0 () Real)
+(declare-fun rAIL_0_t () Real)
+(declare-fun r_0_0 () Real)
+(declare-fun r_0_t () Real)
+(declare-fun psi_0_0 () Real)
+(declare-fun psi_0_t () Real)
+(declare-fun phi_0_0 () Real)
+(declare-fun phi_0_t () Real)
+(declare-fun p_0_0 () Real)
+(declare-fun p_0_t () Real)
+(declare-fun gRDR_0_0 () Real)
+(declare-fun gRDR_0_t () Real)
+(declare-fun gDir_0_0 () Real)
+(declare-fun gDir_0_t () Real)
+(declare-fun gAIL_0_0 () Real)
+(declare-fun gAIL_0_t () Real)
+(declare-fun beta_0_0 () Real)
+(declare-fun beta_0_t () Real)
+(declare-fun time_0 () Real)
+(declare-fun mode_0 () Real)
+(define-ode flow_1 ((= d/dt[beta] (+ (- (/ (* (* 13.97 300) (+ (+ (* (/ (* -0.02 180) 3.14159) beta) (/ (* 0.021 xAIL) 20)) (/ (* 0.086 xRDR) 30))) (* 20500 111.64)) r) (* (* (/ 111.64 9.80555) (cos beta)) (sin phi)))) (= d/dt[gAIL] 0) (= d/dt[gDir] 0) (= d/dt[gRDR] 0) (= d/dt[p] (+ (+ (* (* (+ (* -0.77 r) (* 0.02755 p)) r) (tan phi)) (* 0.0001055 (* (* (* 13.97 30) 300) (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))))) (* 1.642e-06 (* (* (* 13.97 30) 300) (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30)))))) (= d/dt[phi] p) (= d/dt[psi] (* (/ 9.80555 111.64) (tan phi))) (= d/dt[r] (+ (+ (* (* (- (* -0.7336 p) (* 0.02755 r)) r) (tan phi)) (* 1.642e-06 (* (* (* 13.97 30) 300) (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))))) (* 1.587e-05 (* (* (* 13.97 30) 300) (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30)))))) (= d/dt[rAIL] 0) (= d/dt[rRDR] 0) (= d/dt[tau] 1) (= d/dt[xAIL] rAIL) (= d/dt[xRDR] rRDR)))
+(assert (<= -60 xRDR_0_0))
+(assert (<= xRDR_0_0 60))
+(assert (<= -60 xRDR_0_t))
+(assert (<= xRDR_0_t 60))
+(assert (<= -60 xAIL_0_0))
+(assert (<= xAIL_0_0 60))
+(assert (<= -60 xAIL_0_t))
+(assert (<= xAIL_0_t 60))
+(assert (<= 0 tau_0_0))
+(assert (<= tau_0_0 0.5))
+(assert (<= 0 tau_0_t))
+(assert (<= tau_0_t 0.5))
+(assert (<= -60 rRDR_0_0))
+(assert (<= rRDR_0_0 60))
+(assert (<= -60 rRDR_0_t))
+(assert (<= rRDR_0_t 60))
+(assert (<= -60 rAIL_0_0))
+(assert (<= rAIL_0_0 60))
+(assert (<= -60 rAIL_0_t))
+(assert (<= rAIL_0_t 60))
+(assert (<= -1.5 r_0_0))
+(assert (<= r_0_0 1.5))
+(assert (<= -1.5 r_0_t))
+(assert (<= r_0_t 1.5))
+(assert (<= -1.5 psi_0_0))
+(assert (<= psi_0_0 1.5))
+(assert (<= -1.5 psi_0_t))
+(assert (<= psi_0_t 1.5))
+(assert (<= -1.5 phi_0_0))
+(assert (<= phi_0_0 1.5))
+(assert (<= -1.5 phi_0_t))
+(assert (<= phi_0_t 1.5))
+(assert (<= -1.5 p_0_0))
+(assert (<= p_0_0 1.5))
+(assert (<= -1.5 p_0_t))
+(assert (<= p_0_t 1.5))
+(assert (<= -60 gRDR_0_0))
+(assert (<= gRDR_0_0 60))
+(assert (<= -60 gRDR_0_t))
+(assert (<= gRDR_0_t 60))
+(assert (<= -60 gDir_0_0))
+(assert (<= gDir_0_0 60))
+(assert (<= -60 gDir_0_t))
+(assert (<= gDir_0_t 60))
+(assert (<= -60 gAIL_0_0))
+(assert (<= gAIL_0_0 60))
+(assert (<= -60 gAIL_0_t))
+(assert (<= gAIL_0_t 60))
+(assert (<= -1.5 beta_0_0))
+(assert (<= beta_0_0 1.5))
+(assert (<= -1.5 beta_0_t))
+(assert (<= beta_0_t 1.5))
+(assert (<= 0 time_0 [0.000000]))
+(assert (<= time_0 0.5 [0.000000]))
+(assert (<= 1 mode_0))
+(assert (<= mode_0 1))
+(assert (and (= mode_0 1) (and (= tau_0_0 0) (= gRDR_0_0 0) (= gAIL_0_0 0) (= rRDR_0_0 0) (= rAIL_0_0 0) (= xRDR_0_0 0) (= xAIL_0_0 0) (= r_0_0 0) (= p_0_0 0) (= psi_0_0 0) (= beta_0_0 0)) (= mode_0 1) (= [beta_0_t gAIL_0_t gDir_0_t gRDR_0_t p_0_t phi_0_t psi_0_t r_0_t rAIL_0_t rRDR_0_t tau_0_t xAIL_0_t xRDR_0_t] (integral 0. time_0 [beta_0_0 gAIL_0_0 gDir_0_0 gRDR_0_0 p_0_0 phi_0_0 psi_0_0 r_0_0 rAIL_0_0 rRDR_0_0 tau_0_0 xAIL_0_0 xRDR_0_0] flow_1)) (= mode_0 1) (forall_t 1 [0 time_0] (>= tau_0_t 0)) (>= tau_0_t 0) (>= tau_0_0 0) (forall_t 1 [0 time_0] (<= tau_0_t 0.5)) (<= tau_0_t 0.5) (<= tau_0_0 0.5)))
+(check-sat)
+(exit)

src/tests/nra_ode/kquine_04.smt2.expected

@@ -0,0 +1 @@
+delta-sat with delta = 0.00100000000000000