Commit 3911c0af authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix some bugs in certificate generation and rework script for evaluation

parent d3c80dca
......@@ -19,9 +19,9 @@ for file in "${arr[@]}"
do
echo $file
echo "Coq certificate"
time (./daisy $file --certificate=coq >/dev/null)
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=coq >/dev/null
echo "HOL Certificate"
time (./daisy $file --certificate=hol >/dev/null)
/usr/bin/time -o $1 -a -f "%C %E" ./daisy $file --certificate=hol >/dev/null
echo ""
done
#
......@@ -39,7 +39,7 @@ for file in "${arrCoq[@]}"
do
echo $file
echo ""
time (coqc -R ./ Daisy $file)
/usr/bin/time -o $1 -a -f "%C %E" coqc -R ./ Daisy $file
done
cd ../hol
......@@ -54,7 +54,8 @@ for file in "${arrHOL[@]}"
do
echo $file
echo ""
timeout $TIMEOUT time ocaml<$file &>.$file
echo $file >> $1
timeout $TIMEOUT /usr/bin/time -o $1 -a -f "%C %E" ocaml<$file &>.$file
RETVAL=$?
if [ $RETVAL -eq 124 ]
then echo "TIMEOUT "$file
......
......@@ -150,80 +150,83 @@ object CertificatePhase extends DaisyPhase {
reporter.fatalError("Unsupported value")
}
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = e match {
case x @ Variable(id) =>
if (identifierNums.contains(id)){
("",expressionNames(e))
}else{
val varId = nextFreshVariable()
identifierNums += (id -> varId)
val (definition, name) =
if (prv == "coq"){
coqVariable (id,varId,reporter)
private def getValues(e: Expr,reporter:Reporter,prv:String): (String, String) = {
if (expressionNames.contains(e)){
("",expressionNames(e))
}else{
e match {
case x @ Variable(id) =>
if (identifierNums.contains(id)){
("",expressionNames(e))
}else{
holVariable (id,varId,reporter)
val varId = nextFreshVariable()
identifierNums += (id -> varId)
val (definition, name) =
if (prv == "coq"){
coqVariable (id,varId,reporter)
}else{
holVariable (id,varId,reporter)
}
expressionNames += (e -> name)
(definition,name)
}
expressionNames += (e -> name)
(definition,name)
}
case x @ RealLiteral(r) =>
val (definition, name) =
if (prv == "coq")
coqConstant (x,nextConstantId(),reporter)
else
holConstant (x,nextConstantId(),reporter)
expressionNames += (e -> name)
(definition,name)
case x @ Plus(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ Minus(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ Times(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ _ =>
reporter.fatalError(s"Unsupported operation")
case x @ RealLiteral(r) =>
val (definition, name) =
if (prv == "coq")
coqConstant (x,nextConstantId(),reporter)
else
holConstant (x,nextConstantId(),reporter)
expressionNames += (e -> name)
(definition,name)
}
case x @ Plus(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ Minus(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ Times(lhs, rhs) =>
val (lhsText, lhsName) = getValues(lhs,reporter,prv)
val (rhsText, rhsName) = getValues(rhs,reporter,prv)
val (definition, name) =
if (prv == "coq"){
val (binOpDef, binOpName) = coqBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
} else {
val (binOpDef, binOpName) = holBinOp (e, lhsName, rhsName,reporter)
(lhsText + rhsText + binOpDef, binOpName)
}
expressionNames += (e -> name)
(definition,name)
case x @ _ =>
reporter.fatalError(s"Unsupported operation")
}
}
}
private def coqInterval(intv:(Rational,Rational)) :String =
intv match {
......
import daisy.lang._
import Real._
/*
Real2Float
Optimization problems
A Collection of Test Problems for
Constrained Global Optimization Algorithms,
Floudas, Pardalos 1990
*/
object Floudas {
//40 operations
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
//25 operations
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)
(-1) * (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
//3 operations
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
//2 operations
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)
(-1 * x1) - x2
} //1.38e–15
//5 operations
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
//24 operations
// 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))
}
}
import daisy.lang._
import Real._
/*
Real2Float
From a global optimization problem
A Numerical Evaluation of Several Stochastic Algorithms on
Selected Continuous Global Optimization problems,
Ali, Khompatraporn, Zabinsky, 2005
*/
object Himmilbeau {
//15 operations
def himmilbeau(x1: Real, x2: Real) = {
require(-5 <= x1 && x1 <= 5 && -5 <= x2 && x2 <= 5)
(x1*x1 + x2 - 11)*(x1 * x1 + x2 - 11) + (x1 + x2*x2 - 7)*(x1 + x2*x2 - 7)
} //1.43e–12
}
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)
x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * ((-1 * x1) + x2 + x3 - x4 + x5 + x6)
} // 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)
x1 * x4 * ((-1 * x1) + x2 + x3 - x4) + 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)
x1 * x4 * ((-1 * x1) + x2 + x3 - x4 + x5 + x6) + x2 * x5 * (x1 - x2 + x3 + x4 - x5 + x6) +
x3* x6 * (x1 + x2 - x3 + x4 + x5 - x6) - x2 * x3 * x4 -
x1* x3* x5 - x1 * x2 * x6 - x4 * x5 * x6
} //2.08e–12
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment