Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
AVA
FloVer
Commits
22942c41
Commit
22942c41
authored
Feb 25, 2019
by
Joachim Bard
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'exprMerge' of gitlab.mpi-sws.org:jbard/FloVer into exprMerge
parents
e01c7e3f
14600d6d
Changes
27
Hide whitespace changes
Inline
Side-by-side
Showing
27 changed files
with
1047 additions
and
0 deletions
+1047
-0
testcases/smalltest/BallBeam.scala
testcases/smalltest/BallBeam.scala
+15
-0
testcases/smalltest/Bicycle.scala
testcases/smalltest/Bicycle.scala
+24
-0
testcases/smalltest/Bsplines.scala
testcases/smalltest/Bsplines.scala
+36
-0
testcases/smalltest/Floudas.scala
testcases/smalltest/Floudas.scala
+88
-0
testcases/smalltest/InvertedPendulum.scala
testcases/smalltest/InvertedPendulum.scala
+16
-0
testcases/smalltest/Kepler.scala
testcases/smalltest/Kepler.scala
+47
-0
testcases/smalltest/Science.scala
testcases/smalltest/Science.scala
+33
-0
testcases/smalltest/Traincar1.scala
testcases/smalltest/Traincar1.scala
+35
-0
testcases/testsmt/BallBeam.scala
testcases/testsmt/BallBeam.scala
+15
-0
testcases/testsmt/BatchProcessor.scala
testcases/testsmt/BatchProcessor.scala
+43
-0
testcases/testsmt/BatchReactor.scala
testcases/testsmt/BatchReactor.scala
+44
-0
testcases/testsmt/Bicycle.scala
testcases/testsmt/Bicycle.scala
+24
-0
testcases/testsmt/Bsplines.scala
testcases/testsmt/Bsplines.scala
+36
-0
testcases/testsmt/DCMotor.scala
testcases/testsmt/DCMotor.scala
+28
-0
testcases/testsmt/Doppler.scala
testcases/testsmt/Doppler.scala
+18
-0
testcases/testsmt/DopplerFMA.scala
testcases/testsmt/DopplerFMA.scala
+18
-0
testcases/testsmt/Floudas.scala
testcases/testsmt/Floudas.scala
+88
-0
testcases/testsmt/Himmilbeau.scala
testcases/testsmt/Himmilbeau.scala
+25
-0
testcases/testsmt/InvertedPendulum.scala
testcases/testsmt/InvertedPendulum.scala
+16
-0
testcases/testsmt/Kepler.scala
testcases/testsmt/Kepler.scala
+47
-0
testcases/testsmt/RigidBody.scala
testcases/testsmt/RigidBody.scala
+23
-0
testcases/testsmt/Science.scala
testcases/testsmt/Science.scala
+33
-0
testcases/testsmt/Traincar1.scala
testcases/testsmt/Traincar1.scala
+35
-0
testcases/testsmt/Traincar2.scala
testcases/testsmt/Traincar2.scala
+53
-0
testcases/testsmt/Traincar3.scala
testcases/testsmt/Traincar3.scala
+76
-0
testcases/testsmt/Traincar4.scala
testcases/testsmt/Traincar4.scala
+98
-0
testcases/testsmt/Turbine.scala
testcases/testsmt/Turbine.scala
+33
-0
No files found.
testcases/smalltest/BallBeam.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
BallBeam
{
// s1 <1, 16, 14>, s2, s3, s4: <1, 16, 15>
def
ballbeam
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
)
=
{
require
(
0
<=
s1
&&
s1
<=
1
&&
-
0.5
<=
s2
&&
s2
<=
0.5
&&
0
<=
s3
&&
s3
<=
0.5
&&
0
<=
s4
&&
s4
<=
0.5
)
(-
1828.6
)
*
s1
+
(-
1028.6
)
*
s2
+
(-
2008.0
)
*
s3
+
(-
104.0
)
*
s4
}
}
testcases/smalltest/Bicycle.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
Bicycle
{
// s1, s2, s3, y1: <1, 16, 14>, [-1, 1]
def
out1
(
s1
:
Real
,
s2
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
)
(-
3.025300
)
*
s1
+
(-
12.608900
)
*
s2
}
def
state1
(
s1
:
Real
,
s2
:
Real
,
y1
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
)
(
0.961270
)
*
s1
+
(-
0.095962
)
*
s2
+
(
0.013200
)
*
y1
}
def
state2
(
s1
:
Real
,
s2
:
Real
,
y1
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
)
(-
0.058217
)
*
s1
+
(
0.727430
)
*
s2
+
(
0.102100
)
*
y1
}
}
\ No newline at end of file
testcases/smalltest/Bsplines.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
/**
Equation and initial ranges from:
L. Zhang, Y. Zhang, and W. Zhou. Tradeoff between Approximation Accuracy and
Complexity for Range Analysis using Affine Arithmetic.
*/
object
Bsplines
{
def
bspline0
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
(
1
-
u
)
*
(
1
-
u
)
*
(
1
-
u
)
/
6.0
}
ensuring
(
res
=>
0
<=
res
&&
res
<=
0.17
&&
res
+/-
1
e
-
15
)
// proven in paper: [-0.05, 0.17]
def
bspline1
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
(
3
*
u
*
u
*
u
-
6
*
u
*
u
+
4
)
/
6.0
}
ensuring
(
res
=>
0.16
<=
res
&&
res
<=
0.7
&&
res
+/-
1
e
-
15
)
// in paper [-0.05, 0.98]
def
bspline2
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
(-
3
*
u
*
u
*
u
+
3
*
u
*
u
+
3
*
u
+
1
)
/
6.0
}
ensuring
(
res
=>
0.16
<=
res
&&
res
<=
0.7
&&
res
+/-
1
e
-
15
)
// in paper [-0.02, 0.89]
def
bspline3
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
-
u
*
u
*
u
/
6.0
}
ensuring
(
res
=>
-
0.17
<=
res
&&
res
<=
0.0
&&
res
+/-
1
e
-
15
)
// in paper [-0.17, 0.05]
}
testcases/smalltest/Floudas.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
/*
Real2Float
Optimization problems
A Collection of Test Problems for
Constrained Global Optimization Algorithms,
Floudas, Pardalos 1990
*/
object
Floudas
{
def
floudas26
(
x1
:
Real
,
x2
:
Real
,
x3
:
Real
,
x4
:
Real
,
x5
:
Real
,
x6
:
Real
,
x7
:
Real
,
x8
:
Real
,
x9
:
Real
,
x10
:
Real
)
:
Real
=
{
require
(
0
<=
x1
&&
x1
<=
1
&&
0
<=
x2
&&
x2
<=
1
&&
0
<=
x3
&&
x3
<=
1
&&
0
<=
x4
&&
x4
<=
1
&&
0
<=
x5
&&
x5
<=
1
&&
0
<=
x6
&&
x6
<=
1
&&
0
<=
x7
&&
x7
<=
1
&&
0
<=
x8
&&
x8
<=
1
&&
0
<=
x9
&&
x9
<=
1
&&
0
<=
x10
&&
x10
<=
1
&&
2
*
x1
+
6
*
x2
+
1
*
x3
+
0
*
x4
+
3
*
x5
+
3
*
x6
+
2
*
x7
+
6
*
x8
+
2
*
x9
+
2
*
x10
-
4
>=
0
&&
22
-(
6
*
x1
-
5
*
x2
+
8
*
x3
-
3
*
x4
+
0
*
x5
+
1
*
x6
+
3
*
x7
+
8
*
x8
+
9
*
x9
-
3
*
x10
)>=
0
&&
-(
5
*
x1
+
6
*
x2
+
5
*
x3
+
3
*
x4
+
8
*
x5
-
8
*
x6
+
9
*
x7
+
2
*
x8
+
0
*
x9
-
9
*
x10
)
-
6
>=
0
&&
-(
9
*
x1
+
5
*
x2
+
0
*
x3
-
9
*
x4
+
1
*
x5
-
8
*
x6
+
3
*
x7
-
9
*
x8
-
9
*
x9
-
3
*
x10
)
-
23
>=
0
&&
-(-(
8
*
x1
)
+
7
*
x2
-
4
*
x3
-
5
*
x4
-
9
*
x5
+
1
*
x6
-
7
*
x7
-
1
*
x8
+
3
*
x9
-
2
*
x10
)
-
12
>=
0
)
48
*
x1
+
42
*
x2
+
48
*
x3
+
45
*
x4
+
44
*
x5
+
41
*
x6
+
47
*
x7
+
42
*
x8
+
45
*
x9
+
46
*
x10
-
50
*(
x1
*
x1
+
x2
*
x2
+
x3
*
x3
+
x4
*
x4
+
x5
*
x5
+
x6
*
x6
+
x7
*
x7
+
x8
*
x8
+
x9
*
x9
+
x10
*
x10
)
}
// 5.15e-13
def
floudas33
(
x1
:
Real
,
x2
:
Real
,
x3
:
Real
,
x4
:
Real
,
x5
:
Real
,
x6
:
Real
)
:
Real
=
{
require
(
0
<=
x1
&&
x1
<=
6
&&
0
<=
x2
&&
x2
<=
6
&&
1
<=
x3
&&
x3
<=
5
&&
0
<=
x4
&&
x4
<=
6
&&
1
<=
x5
&&
x5
<=
5
&&
0
<=
x6
&&
x6
<=
10
&&
(
x3
-
3
)*(
x3
-
3
)
+
x4
-
4
>=
0
&&
(
x5
-
3
)*(
x5
-
3
)
+
x6
-
4
>=
0
&&
2
-
x1
+
3
*
x2
>=
0
&&
2
+
x1
-
x2
>=
0
&&
6
-
x1
-
x2
>=
0
&&
x1
+
x2
-
2
>=
0
)
-
(
25
*
(
x1
-
2
)*(
x1
-
2
))
-
(
x2
-
2
)*
(
x2
-
2
)
-
(
x3
-
1
)*(
x3
-
1
)
-
(
x4
-
4
)*(
x4
-
4
)
-
(
x5
-
1
)*(
x5
-
1
)
-
(
x6
-
4
)*
(
x6
-
4
)
}
//5.81e–13
def
floudas34
(
x1
:
Real
,
x2
:
Real
,
x3
:
Real
)
:
Real
=
{
require
(
0
<=
x1
&&
x1
<=
2
&&
0
<=
x2
&&
x2
<=
2
&&
0
<=
x3
&&
x3
<=
3
&&
4
-
x1
-
x2
-
x3
>=
0
&&
6
-
3
*
x2
-
x3
>=
0
&&
2
*
x1
-
0.75
-
2
*
x3
+
4
*
x1
*
x1
-
4
*
x1
*
x2
+
4
*
x1
*
x3
+
2
*
x2
*
x2
-
2
*
x2
*
x3
+
2
*
x3
*
x3
>=
0
)
-
2
*
x1
+
x2
-
x3
}
//2.67e - 15
def
floudas46
(
x1
:
Real
,
x2
:
Real
)
:
Real
=
{
require
(
0
<=
x1
&&
x1
<=
3
&&
0
<=
x2
&&
x2
<=
4
&&
2
*
x1
*
x1
*
x1
*
x1
-
8
*
x1
*
x1
*
x1
+
8
*
x1
*
x1
-
x2
>=
0
&&
4
*
x1
*
x1
*
x1
*
x1
-
32
*
x1
*
x1
*
x1
+
88
*
x1
*
x1
-
96
*
x1
+
36
-
x2
>=
0
)
-
x1
-
x2
}
//1.38e–15
def
floudas47
(
x1
:
Real
,
x2
:
Real
)
:
Real
=
{
require
(
0
<=
x1
&&
x1
<=
2
&&
0
<=
x2
&&
x2
<=
3
&&
-
2
*
x1
*
x1
*
x1
*
x1
+
2
-
x2
>=
0
)
-
12
*
x1
-
7
*
x2
+
x2
*
x2
}
//1.01e–14
// from FPTaylor github
def
floudas1
(
x1
:
Real
,
x2
:
Real
,
x3
:
Real
,
x4
:
Real
,
x5
:
Real
,
x6
:
Real
)
:
Real
=
{
require
(
0
<=
x1
&&
x1
<=
6
&&
0
<=
x2
&&
x2
<=
6
&&
1
<=
x3
&&
x3
<=
5
&&
0
<=
x4
&&
x4
<=
6
&&
1
<=
x5
&&
x5
<=
5
&&
0
<=
x6
&&
x6
<=
10
&&
(
x3
-
3
)
*
(
x3
-
3
)
+
x4
-
4
>=
0
&&
(
x5
-
3
)
*
(
x5
-
3
)
+
x6
-
4
>=
0
&&
2
-
x1
+
3
*
x2
>=
0
&&
2
+
x1
-
x2
>=
0
&&
6
-
x1
-
x2
>=
0
&&
x1
+
x2
-
2
>=
0
)
-
25
*
((
x1
-
2
)
*
(
x1
-
2
))
-
((
x2
-
2
)
*
(
x2
-
2
))
-
((
x3
-
1
)
*
(
x3
-
1
))
-
((
x4
-
4
)
*
(
x4
-
4
))
-
((
x5
-
1
)
*
(
x5
-
1
))
-
((
x6
-
4
)
*
(
x6
-
4
))
}
}
testcases/smalltest/InvertedPendulum.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
InvertedPendulum
{
// s1: <1, 16, 9> s2: <1, 16, 11> s3,s4: <1, 16, 15>
def
out
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
)
=
{
require
(-
50
<=
s1
&&
s1
<=
50
&&
-
10
<=
s2
&&
s2
<=
10
&&
-
0.785
<=
s3
&&
s3
<=
0.785
&&
-
0.785
<=
s4
&&
s4
<=
0.785
)
1.0000
*
s1
+
1.6567
*
s2
+
(-
18.6854
)
*
s3
+
(-
3.4594
)
*
s4
}
}
testcases/smalltest/Kepler.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
/*
These benchmarks were used by the Real2Float tool,
and come from the proof of the Kepler conjecture
Introduction to the flyspec project, T.C. Hales, Dagstuhl 2006
*/
object
Kepler
{
//15 operations
def
kepler0
(
x1
:
Real
,
x2
:
Real
,
x3
:
Real
,
x4
:
Real
,
x5
:
Real
,
x6
:
Real
)
:
Real
=
{
require
(
4
<=
x1
&&
x1
<=
6.36
&&
4
<=
x2
&&
x2
<=
6.36
&&
4
<=
x3
&&
x3
<=
6.36
&&
4
<=
x4
&&
x4
<=
6.36
&&
4
<=
x5
&&
x5
<=
6.36
&&
4
<=
x6
&&
x6
<=
6.36
)
val
t
=
((-
1
*
x1
)
+
x2
+
x3
-
x4
+
x5
+
x6
)
x2
*
x5
+
x3
*
x6
-
x2
*
x3
-
x5
*
x6
+
x1
*
t
}
// 1.15e-15
//24 operations
def
kepler1
(
x1
:
Real
,
x2
:
Real
,
x3
:
Real
,
x4
:
Real
)
:
Real
=
{
require
(
4
<=
x1
&&
x1
<=
6.36
&&
4
<=
x2
&&
x2
<=
6.36
&&
4
<=
x3
&&
x3
<=
6.36
&&
4
<=
x4
&&
x4
<=
6.36
)
val
t
=
((-
1
*
x1
)
+
x2
+
x3
-
x4
)
x1
*
x4
*
t
+
x2
*
(
x1
-
x2
+
x3
+
x4
)
+
x3
*
(
x1
+
x2
-
x3
+
x4
)
-
x2
*
x3
*
x4
-
x1
*
x3
-
x1
*
x2
-
x4
}
// 4.50e–13
//36 operations
def
kepler2
(
x1
:
Real
,
x2
:
Real
,
x3
:
Real
,
x4
:
Real
,
x5
:
Real
,
x6
:
Real
)
:
Real
=
{
require
(
4
<=
x1
&&
x1
<=
6.36
&&
4
<=
x2
&&
x2
<=
6.36
&&
4
<=
x3
&&
x3
<=
6.36
&&
4
<=
x4
&&
x4
<=
6.36
&&
4
<=
x5
&&
x5
<=
6.36
&&
4
<=
x6
&&
x6
<=
6.36
)
val
t
=
((-
1
*
x1
)
+
x2
+
x3
-
x4
+
x5
+
x6
)
val
t2
=
(
x1
-
x2
+
x3
+
x4
-
x5
+
x6
)
x1
*
x4
*
t
+
x2
*
x5
*
t2
+
x3
*
x6
*
(
x1
+
x2
-
x3
+
x4
+
x5
-
x6
)
-
x2
*
x3
*
x4
-
x1
*
x3
*
x5
-
x1
*
x2
*
x6
-
x4
*
x5
*
x6
}
//2.08e–12
}
testcases/smalltest/Science.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
Science
{
def
verhulst
(
r
:
Real
,
K
:
Real
,
x
:
Real
)
:
Real
=
{
require
(
r
>=
4.0
&&
r
<=
4.0
&&
K
>=
1.11
&&
K
<=
1.11
&&
0.1
<=
x
&&
x
<=
0.3
)
(
r
*
x
)
/
(
1
+
(
x
/
K
))
}
def
predatorPrey
(
r
:
Real
,
K
:
Real
,
x
:
Real
)
:
Real
=
{
require
(
r
>=
4.0
&&
r
<=
4.0
&&
K
>=
1.11
&&
K
<=
1.11
&&
0.1
<=
x
&&
x
<=
0.3
)
(
r
*
x
*
x
)
/
(
1
+
(
x
/
K
)*(
x
/
K
))
}
def
carbonGas
(
T
:
Real
,
a
:
Real
,
b
:
Real
,
N
:
Real
,
p
:
Real
,
V
:
Real
)
:
Real
=
{
require
(
T
>=
300
&&
T
<=
300
&&
a
>=
0.401
&&
a
<=
0.401
&&
b
>=
42.7e-6
&&
b
<=
42.7e-6
&&
N
>=
1000
&&
N
<=
1000
&&
p
>=
3.5e7
&&
p
<=
3.5e7
&&
0.1
<
V
&&
V
<
0.5
)
val
k
:
Real
=
1.3806503e-23
(
p
+
a
*
(
N
/
V
)
*
(
N
/
V
))
*
(
V
-
N
*
b
)
-
k
*
N
*
T
}
}
\ No newline at end of file
testcases/smalltest/Traincar1.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
Traincar1
{
// y1, y2: <1, 30, 16> s1, s2, s3: <1, 30, 25>
def
out1
(
s0
:
Real
,
s1
:
Real
,
s2
:
Real
)
=
{
require
(
0
<=
s0
&&
s0
<=
4.6
&&
0
<=
s1
&&
s1
<=
10
&&
0
<=
s2
&&
s2
<=
10
)
(-
3.795323e2
)
*
s0
+
(-
5.443608e2
)
*
s1
+
92.729
*
s2
+
4.5165916241610748e3
}
def
state1
(
s0
:
Real
,
s1
:
Real
,
s2
:
Real
,
y0
:
Real
,
y1
:
Real
)
=
{
require
(
0
<=
s0
&&
s0
<=
4.6
&&
0
<=
s1
&&
s1
<=
10
&&
0
<=
s2
&&
s2
<=
10
&&
0
<=
y0
&&
y0
<=
10
&&
0
<=
y1
&&
y1
<=
10
)
(
9.9992292212695999e-01
)*
s0
+
(
6.7987387059578006e-02
)*
s1
+
(-
5.7849982690687002e-02
)*
s2
+
(-
6.7093068270769995e-02
)*
y0
+
(
5.6868444245656999e-02
)*
y1
+
(
1.93109421e-07
)*
4.5165916241610748e+03
}
def
state2
(
s0
:
Real
,
s1
:
Real
,
s2
:
Real
,
y0
:
Real
,
y1
:
Real
)
=
{
require
(
0
<=
s0
&&
s0
<=
4.6
&&
0
<=
s1
&&
s1
<=
10
&&
0
<=
s2
&&
s2
<=
10
&&
0
<=
y0
&&
y0
<=
10
&&
0
<=
y1
&&
y1
<=
10
)
(-
2.1755689728790001e-03
)*
s0
+
(
9.8343791204296505e-01
)*
s1
+
(
2.6908497812900001e-03
)*
s2
+
(
1.3497550507479000e-02
)*
y0
+
(-
2.1628302791680000e-03
)*
y1
+
(
5.615999103e-06
)*
4.5165916241610748e+03
}
def
state3
(
s0
:
Real
,
s1
:
Real
,
s2
:
Real
,
y0
:
Real
,
y1
:
Real
)
=
{
require
(
0
<=
s0
&&
s0
<=
4.6
&&
0
<=
s1
&&
s1
<=
10
&&
0
<=
s2
&&
s2
<=
10
&&
0
<=
y0
&&
y0
<=
10
&&
0
<=
y1
&&
y1
<=
10
)
(
7.5141305955000001e-05
)*
s0
+
(
2.4840831806619999e-03
)*
s1
+
(
9.9188004018882503e-01
)*
s2
+
(-
2.4770170720600001e-03
)*
y0
+
(
8.1097048460159991e-03
)*
y1
+
(
7.060315e-09
)*
4.5165916241610748e+03
}
}
\ No newline at end of file
testcases/testsmt/BallBeam.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
BallBeam
{
// s1 <1, 16, 14>, s2, s3, s4: <1, 16, 15>
def
ballbeam
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
)
=
{
require
(
0
<=
s1
&&
s1
<=
1
&&
-
0.5
<=
s2
&&
s2
<=
0.5
&&
0
<=
s3
&&
s3
<=
0.5
&&
0
<=
s4
&&
s4
<=
0.5
)
(-
1828.6
)
*
s1
+
(-
1028.6
)
*
s2
+
(-
2008.0
)
*
s3
+
(-
104.0
)
*
s4
}
}
testcases/testsmt/BatchProcessor.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
BatchProcessor
{
// s1, s2, s3, s4, y1, y2: <1, 16, 11>
def
out1
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
)
=
{
require
(-
10
<=
s1
&&
s1
<=
10
&&
-
10
<=
s2
&&
s2
<=
10
&&
-
10
<=
s3
&&
s3
<=
10
&&
-
10
<=
s4
&&
s4
<=
10
)
(-
0.0429
)
*
s1
+
(-
0.9170
)
*
s2
+
(-
0.3299
)
*
s3
+
(-
0.8206
)
*
s4
}
def
out2
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
)
=
{
require
(-
10
<=
s1
&&
s1
<=
10
&&
-
10
<=
s2
&&
s2
<=
10
&&
-
10
<=
s3
&&
s3
<=
10
&&
-
10
<=
s4
&&
s4
<=
10
)
2.4908
*
s1
+
0.0751
*
s2
+
1.7481
*
s3
+
(-
1.1433
)
*
s4
}
def
state1
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
)
=
{
require
(-
10
<=
s1
&&
s1
<=
10
&&
-
10
<=
s2
&&
s2
<=
10
&&
-
10
<=
s3
&&
s3
<=
10
&&
-
10
<=
s4
&&
s4
<=
10
&&
-
10
<=
y1
&&
y1
<=
10
)
0.9670
*
s1
+
(-
0.0019
)
*
s2
+
0.0187
*
s3
+
(-
0.0088
)
*
s4
+
0.0447
*
y1
}
def
state2
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
,
y2
:
Real
)
=
{
require
(-
10
<=
s1
&&
s1
<=
10
&&
-
10
<=
s2
&&
s2
<=
10
&&
-
10
<=
s3
&&
s3
<=
10
&&
-
10
<=
s4
&&
s4
<=
10
&&
-
10
<=
y1
&&
y1
<=
10
&&
-
10
<=
y2
&&
y2
<=
10
)
(-
0.0078
)
*
s1
+
0.9052
*
s2
+
(-
0.0181
)
*
s3
+
(-
0.0392
)
*
s4
+
(-
0.0003
)
*
y1
+
0.0020
*
y2
//((0.9052 * s2) + (((s3 * -0.0181) + (-0.0078 * s1)) + (((-0.0392 * s4) + (-0.0003 * y1)) + (0.002 * y2))))
}
def
state3
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
,
y2
:
Real
)
=
{
require
(-
10
<=
s1
&&
s1
<=
10
&&
-
10
<=
s2
&&
s2
<=
10
&&
-
10
<=
s3
&&
s3
<=
10
&&
-
10
<=
s4
&&
s4
<=
10
&&
-
10
<=
y1
&&
y1
<=
10
&&
-
10
<=
y2
&&
y2
<=
10
)
(-
0.0830
)
*
s1
+
0.0222
*
s2
+
0.8620
*
s3
+
0.0978
*
s4
+
0.0170
*
y1
+
0.0058
*
y2
}
def
state4
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
,
y2
:
Real
)
=
{
require
(-
10
<=
s1
&&
s1
<=
10
&&
-
10
<=
s2
&&
s2
<=
10
&&
-
10
<=
s3
&&
s3
<=
10
&&
-
10
<=
s4
&&
s4
<=
10
&&
-
10
<=
y1
&&
y1
<=
10
&&
-
10
<=
y2
&&
y2
<=
10
)
(-
0.0133
)
*
s1
+
0.0243
*
s2
+
(-
0.0043
)
*
s3
+
0.9824
*
s4
+
0.0127
*
y1
+
0.0059
*
y2
}
}
\ No newline at end of file
testcases/testsmt/BatchReactor.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
BatchReactor
{
// s1, s2, s3, s4, y1, y2: <1, 16, 14>
def
out1
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
s4
&&
s4
<=
1
)
(-
0.058300
)
*
s1
+
(-
0.908300
)
*
s2
+
(-
0.325800
)
*
s3
+
(-
0.872100
)
*
s4
}
def
out2
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
s4
&&
s4
<=
1
)
(
2.463800
)
*
s1
+
(
0.050400
)
*
s2
+
(
1.709900
)
*
s3
+
(-
1.165300
)
*
s4
}
def
state1
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
,
y2
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
s4
&&
s4
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
&&
-
1
<=
y2
&&
y2
<=
1
)
(
0.934292
)
*
s1
+
(
0.008415
)
*
s2
+
(-
0.014106
)
*
s3
+
(
0.023954
)
*
s4
+
(
0.077400
)
*
y1
+
(-
0.010300
)
*
y2
}
def
state2
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
,
y2
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
s4
&&
s4
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
&&
-
1
<=
y2
&&
y2
<=
1
)
(-
0.006769
)
*
s1
+
(
0.884924
)
*
s2
+
(-
0.016066
)
*
s3
+
(-
0.044019
)
*
s4
+
(-
0.002200
)
*
y1
+
(
0.022700
)
*
y2
}
def
state3
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
,
y2
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
s4
&&
s4
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
&&
-
1
<=
y2
&&
y2
<=
1
)
(-
0.092148
)
*
s1
+
(-
0.011039
)
*
s2
+
(
0.853511
)
*
s3
+
(
0.107537
)
*
s4
+
(
0.026700
)
*
y1
+
(
0.039800
)
*
y2
}
def
state4
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
s4
:
Real
,
y1
:
Real
,
y2
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
s4
&&
s4
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
&&
-
1
<=
y2
&&
y2
<=
1
)
(-
0.036410
)
*
s1
+
(
0.030194
)
*
s2
+
(-
0.027155
)
*
s3
+
(
1.004619
)
*
s4
+
(
0.035600
)
*
y1
+
(
0.000100
)
*
y2
}
}
\ No newline at end of file
testcases/testsmt/Bicycle.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
Bicycle
{
// s1, s2, s3, y1: <1, 16, 14>, [-1, 1]
def
out1
(
s1
:
Real
,
s2
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
)
(-
3.025300
)
*
s1
+
(-
12.608900
)
*
s2
}
def
state1
(
s1
:
Real
,
s2
:
Real
,
y1
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
)
(
0.961270
)
*
s1
+
(-
0.095962
)
*
s2
+
(
0.013200
)
*
y1
}
def
state2
(
s1
:
Real
,
s2
:
Real
,
y1
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
)
(-
0.058217
)
*
s1
+
(
0.727430
)
*
s2
+
(
0.102100
)
*
y1
}
}
\ No newline at end of file
testcases/testsmt/Bsplines.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
/**
Equation and initial ranges from:
L. Zhang, Y. Zhang, and W. Zhou. Tradeoff between Approximation Accuracy and
Complexity for Range Analysis using Affine Arithmetic.
*/
object
Bsplines
{
def
bspline0
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
(
1
-
u
)
*
(
1
-
u
)
*
(
1
-
u
)
/
6.0
}
ensuring
(
res
=>
0
<=
res
&&
res
<=
0.17
&&
res
+/-
1
e
-
15
)
// proven in paper: [-0.05, 0.17]
def
bspline1
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
(
3
*
u
*
u
*
u
-
6
*
u
*
u
+
4
)
/
6.0
}
ensuring
(
res
=>
0.16
<=
res
&&
res
<=
0.7
&&
res
+/-
1
e
-
15
)
// in paper [-0.05, 0.98]
def
bspline2
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
(-
3
*
u
*
u
*
u
+
3
*
u
*
u
+
3
*
u
+
1
)
/
6.0
}
ensuring
(
res
=>
0.16
<=
res
&&
res
<=
0.7
&&
res
+/-
1
e
-
15
)
// in paper [-0.02, 0.89]
def
bspline3
(
u
:
Real
)
:
Real
=
{
require
(
0
<=
u
&&
u
<=
1
)
-
u
*
u
*
u
/
6.0
}
ensuring
(
res
=>
-
0.17
<=
res
&&
res
<=
0.0
&&
res
+/-
1
e
-
15
)
// in paper [-0.17, 0.05]
}
testcases/testsmt/DCMotor.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
DCMotor
{
// s1, s2, s3, y1: <1, 16, 14>, [-1, 1]
def
out1
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
)
(-
0.112900
)
*
s1
+
(-
0.021100
)
*
s2
+
(-
0.009300
)
*
s3
}
def
state1
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
y1
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
)
(
0.960883
)
*
s1
+
(
0.000949
)
*
s2
+
(-
0.000004
)
*
s3
+
(
0.039000
)
*
y1
}
def
state2
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
y1
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
)
(-
0.602449
)
*
s1
+
(
0.899089
)
*
s2
+
(-
0.013648
)
*
s3
+
(
0.370000
)
*
y1
}
def
state3
(
s1
:
Real
,
s2
:
Real
,
s3
:
Real
,
y1
:
Real
)
=
{
require
(-
1
<=
s1
&&
s1
<=
1
&&
-
1
<=
s2
&&
s2
<=
1
&&
-
1
<=
s3
&&
s3
<=
1
&&
-
1
<=
y1
&&
y1
<=
1
)
(-
0.009134
)
*
s1
+
(-
0.011434
)
*
s2
+
(-
0.002232
)
*
s3
+
(-
0.017500
)
*
y1
}
}
\ No newline at end of file
testcases/testsmt/Doppler.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
Doppler
{
def
doppler
(
u
:
Real
,
v
:
Real
,
T
:
Real
)
:
Real
=
{
require
(-
100.0
<=
u
&&
u
<=
100
&&
20
<=
v
&&
v
<=
20000
&&
-
30
<=
T
&&
T
<=
50
&&
u
+
T
<=
100
)
val
t1
=
331.4
+
0.6
*
T
(-
(
t1
)
*
v
)
/
((
t1
+
u
)*(
t1
+
u
))
}
}
testcases/testsmt/DopplerFMA.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
object
DopplerFMA
{
def
doppler
(
u
:
Real
,
v
:
Real
,
T
:
Real
)
:
Real
=
{
require
(-
100.0
<=
u
&&
u
<=
100
&&
20
<=
v
&&
v
<=
20000
&&
-
30
<=
T
&&
T
<=
50
)
val
t1
=
fma
(
0.6
,
T
,
331.4
)
(-
(
t1
)
*
v
)
/
((
t1
+
u
)*(
t1
+
u
))
}
}
testcases/testsmt/Floudas.scala
0 → 100644
View file @
22942c41
import
daisy.lang._
import
Real._
/*
Real2Float
Optimization problems
A Collection of Test Problems for
Constrained Global Optimization Algorithms,
Floudas, Pardalos 1990
*/