Commit c6dc52d4 authored by Heiko Becker's avatar Heiko Becker

Merge latest changes from master branch

parents 665b39ac f5e323af
......@@ -9,7 +9,7 @@ Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealR
Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments.
Require Export Coq.QArith.QArith.
Require Export Daisy.Infra.ExpressionAbbrevs.
Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
(** Certificate checking function **)
Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) :=
......@@ -104,4 +104,4 @@ Proof.
- intros v v_in_empty.
rewrite NatSet.mem_spec in v_in_empty.
inversion v_in_empty.
Qed.
\ No newline at end of file
Qed.
......@@ -23,7 +23,11 @@ Fixpoint validErrorbound (e:exp Q) (absenv:analysisResult) (dVars:NatSet.t):=
else (Qleb (maxAbs intv * RationalSimps.machineEpsilon) err)
|Const n =>
Qleb (maxAbs intv * RationalSimps.machineEpsilon) err
|Unop _ _ => false
|Unop Neg e =>
if (validErrorbound e absenv dVars)
then Qeq_bool err (snd (absenv e))
else false
|Unop Inv e => false
|Binop b e1 e2 =>
if ((validErrorbound e1 absenv dVars) && (validErrorbound e2 absenv dVars))
then
......@@ -80,7 +84,9 @@ Proof.
andb_to_prop validErrorbound_e.
- apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
- apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
- inversion R.
- destruct u; simpl in *; try congruence.
andb_to_prop R.
apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
- apply Qle_bool_iff in L; apply Qle_Rle in L; rewrite Q2R0_is_0 in L; auto.
Qed.
......@@ -1961,7 +1967,26 @@ Proof.
- unfold validErrorbound in valid_error.
rewrite absenv_eq in valid_error.
andb_to_prop valid_error.
inversion R.
destruct u; try congruence.
env_assert absenv e absenv_e.
destruct absenv_e as [iv [err_e absenv_e]].
rename R into valid_error.
andb_to_prop valid_error.
apply Qeq_bool_iff in R.
apply Qeq_eqR in R.
rewrite R.
destruct iv as [e_lo e_hi].
inversion eval_real; subst.
inversion eval_float; subst.
unfold evalUnop.
apply bound_flip_sub.
eapply IHe; eauto.
simpl in valid_intv.
rewrite absenv_eq in valid_intv; andb_to_prop valid_intv.
auto.
instantiate (1 := e_hi).
instantiate (1 := e_lo).
rewrite absenv_e; auto.
- pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p.
simpl in valid_error.
env_assert absenv e1 absenv_e1.
......
......@@ -24,7 +24,13 @@ val validErrorbound_def = Define `
case e of
| Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * machineEpsilon <= err)
| Const n => (maxAbs intv * machineEpsilon <= err)
| Unop op f => F
| Unop Neg f =>
if (validErrorbound f absenv dVars)
then
err = (SND (absenv f))
else
F
| Unop Inv f => F
| Binop op f1 f2 =>
(if (validErrorbound f1 absenv dVars /\ validErrorbound f2 absenv dVars)
then
......@@ -74,7 +80,7 @@ val err_always_positive = store_thm ("err_always_positive",
val validErrorboundCorrectVariable_ind = prove (
``!(E1 E2:env) absenv fVars dVars.
approxEnv E1 absenv fVars dVars E2 ==>
! (v:num) (nR nF err nlo nhi:real) (P:precond).
!(v:num) (nR nF err nlo nhi:real) (P:precond).
eval_exp 0 E1 (Var v) nR /\
eval_exp machineEpsilon E2 (Var v) nF /\
validIntervalbounds (Var v) absenv P dVars /\
......@@ -149,8 +155,8 @@ val validErrorboundCorrectVariable_ind = prove (
>- (match_mp_tac Var_load \\ fs [])
>- (match_mp_tac Var_load \\ fs [])
>- (rpt strip_tac
\\ rpt( first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domin dVars ==> _` `v' IN domain dVars`
\\ rpt(first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domain dVars ==> _` `v' IN domain dVars`
\\ fs []
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
......@@ -178,7 +184,7 @@ val validErrorboundCorrectVariable_ind = prove (
>- (fs [validIntervalbounds_def, lookup_insert])
>- (fs [validErrorbound_def, lookup_insert])
>- (rpt strip_tac
\\ specialize `!v. v = _ \/ v IN domain _ ==> _` `v'`
\\ specialize `!v'. (v' = _) \/ v' IN domain _ ==> _` `v'`
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
\\ Cases_on `lookup v' fVars`
......@@ -188,7 +194,7 @@ val validErrorboundCorrectVariable_ind = prove (
\\ fs [domain_insert]))
>- (rpt strip_tac
\\ rpt (first_x_assum (qspec_then `v'` ASSUME_TAC))
\\ specialize `v' IN domin fVars ==> _` `v' IN domain fVars`
\\ specialize `v' IN domain fVars ==> _` `v' IN domain fVars`
\\ fs []
\\ Cases_on `v' = x`
>- (rveq \\ fs [lookup_union]
......@@ -2130,8 +2136,25 @@ val validErrorbound_sound = store_thm ("validErrorbound_sound",
\\ qpat_x_assum `absenv _ = _` (fn thm => fs[thm])
\\ first_x_assum match_mp_tac
\\ fs [usedVars_def, SUBSET_DEF])
>- (qpat_x_assum `validErrorbound _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm)) \\
qpat_x_assum `absenv _ = _` (fn thm => fs[thm]))
>- (qpat_x_assum `validErrorbound _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [validErrorbound_def] thm))
\\ qpat_x_assum `absenv _ = _` (fn thm => fs[thm])
\\ Cases_on `u` \\ fs []
\\ rveq
\\ Cases_on `absenv e`
\\ fs[]
\\ inversion `eval_exp 0 _ _ _` eval_exp_cases
\\ inversion `eval_exp machineEpsilon _ _ _` eval_exp_cases
\\ fs [evalUnop_def]
\\ once_rewrite_tac [real_sub] \\ once_rewrite_tac [GSYM REAL_NEG_ADD]
\\ once_rewrite_tac [ABS_NEG]
\\ once_rewrite_tac [GSYM real_sub]
\\ first_x_assum match_mp_tac
\\ qexistsl_tac [`E1`, `E2`, `absenv`, `P`, `FST q`, `SND q`, `fVars`, `dVars`]
\\ fs [Once usedVars_def]
\\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
\\ fs []
\\ Cases_on `absenv e` \\ Cases_on `absenv (Unop Neg e)`
\\ fs [])
>- (rename1 `Binop op e1 e2`
\\ inversion `eval_exp 0 _ _ _` eval_exp_cases
\\ rename1 `eval_exp 0 _ e1 nR1`
......
......@@ -80,7 +80,8 @@ val (eval_exp_rules, eval_exp_ind, eval_exp_cases) = Hol_reln `
(!eps E b f1 f2 v1 v2 delta.
abs delta <= eps /\
eval_exp eps E f1 v1 /\
eval_exp eps E f2 v2 ==>
eval_exp eps E f2 v2 /\
((b = Div) ==> (~ v2 = 0)) ==>
eval_exp eps E (Binop b f1 f2) (perturb (evalBinop b v1 v2) delta))`;
(**
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......@@ -19,7 +19,6 @@ BARE_THYS = BasicProvers Defn HolKernel Parse Tactic monadsyntax \
quantHeuristicsLib relationTheory res_quanTheory rich_listTheory \
sortingTheory sptreeTheory stringTheory sumTheory wordsTheory \
simpLib realTheory realLib RealArith \
cakeml/translator/ml_translatorLib
DEPS = $(patsubst %,%.uo,$(BARE_THYS1)) $(PARENTHEAP)
......
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../
INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../ ../Infra
OPTIONS = QUIT_ON_FAILURE
ifdef POLY
......
......@@ -17,6 +17,7 @@ val validVars_add = store_thm("validVars_add",
domain (usedVars e) domain (insert n () Vs)``,
fs [domain_insert, SUBSET_DEF]);
(*
val validVars_non_stuck = store_thm ("validVars_non_stuck",
``!(e:real exp) inVars E.
domain (usedVars e) ⊆ inVars /\
......@@ -52,6 +53,7 @@ val validVars_non_stuck = store_thm ("validVars_non_stuck",
\\ Cases_on `b` \\ fs[eval_exp_cases]
\\ qexistsl_tac [`vR1`, `vR2`, `0`]
\\ fs[perturb_def]));
*)
(**
Inductive ssa predicate, following the definitions from the LVC framework,
......
......@@ -190,6 +190,7 @@ object Main {
backend.CodeGenerationPhase
} else if (ctx.findOption(optionValidators) != None) {
analysis.SpecsProcessingPhase andThen
transform.SSATransformerPhase andThen
analysis.RangeErrorPhase andThen
InfoPhase andThen
backend.CertificatePhase andThen
......
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 +/- 1e-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 +/- 1e-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 +/- 1e-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 +/- 1e-15)
// in paper [-0.17, 0.05]
}
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)
val t1 = 331.4 + 0.6 * T
(- (t1) *v) / ((t1 + u)*(t1 + u))
}
}
\ No newline at end of file
import daisy.lang._
import Real._
object JetEngine {
def jetEngine(x1: Real, x2: Real): Real = {
require(-5 <= x1 && x1 <= 5 && -20 <= x2 && x2 <= 5)
val t = (3*x1*x1 + 2*x2 - x1)
x1 + ((2*x1*(t/(x1*x1 + 1))*
(t/(x1*x1 + 1) - 3) + x1*x1*(4*(t/(x1*x1 + 1))-6))*
(x1*x1 + 1) + 3*x1*x1*(t/(x1*x1 + 1)) + x1*x1*x1 + x1 +
3*((3*x1*x1 + 2*x2 -x1)/(x1*x1 + 1)))
}
}
\ No newline at end of file
import daisy.lang._
import Real._
//Unrolled loops
object Pendulum {
def pendulumT1(t_0: Real, w_0: Real): Real = {
require(-2 <= t_0 && t_0 <= 2 && -5 <= w_0 && w_0 <= 5)
val h: Real = 0.01
val L: Real = 2.0
val m: Real = 1.5
val g: Real = 9.80665
val k1t = w_0
val k1w = -g/L * (t_0 - t_0 * t_0 * t_0/6 + t_0 * t_0 * t_0 * t_0 * t_0/120)
val k2t = w_0 + h/2*k1w
val arg = t_0 + h/2*k1t
val k2w = -g/L * (arg - arg * arg * arg/6 + arg * arg * arg * arg * arg/120)
t_0 + h*k2t
}
def pendulumW1(t_0: Real, w_0: Real): Real = {
require(-2 <= t_0 && t_0 <= 2 && -5 <= w_0 && w_0 <= 5)
val h: Real = 0.01
val L: Real = 2.0
val m: Real = 1.5
val g: Real = 9.80665
val k1t = w_0
val k1w = -g/L * (t_0 - t_0 * t_0 * t_0/6 + t_0 * t_0 * t_0 * t_0 * t_0/120)
val k2t = w_0 + h/2*k1w
val arg = t_0 + h/2*k1t
val k2w = -g/L * (arg - arg * arg * arg/6 + arg * arg * arg * arg * arg/120)
w_0 + h*k2w
}
// TODO: takes forever, maybe because of Rationals getting too big?
def pendulumT3(t_0: Real, w_0: Real): Real = {
require(-2 <= t_0 && t_0 <= 2 && -5 <= w_0 && w_0 <= 5)
val h: Real = 0.01
val L: Real = 2.0
val m: Real = 1.5
val g: Real = 9.80665
// loop 1
val k1t_1 = w_0
val k1w_1 = -g/L * (t_0 - t_0 * t_0 * t_0/6 + t_0 * t_0 * t_0 * t_0 * t_0/120)
val k2t_1 = w_0 + h/2*k1w_1
val arg_1 = t_0 + h/2*k1t_1
val k2w_1 = -g/L * (arg_1 - arg_1 * arg_1 * arg_1/6 + arg_1 * arg_1 * arg_1 * arg_1 * arg_1/120)
val t_1 = t_0 + h*k2t_1
val w_1 = w_0 + h*k2w_1
// loop 2
val k1t_2 = w_1
val k1w_2 = -g/L * (t_1 - t_1 * t_1 * t_1/6 + t_1 * t_1 * t_1 * t_1 * t_1/120)
val k2t_2 = w_1 + h/2*k1w_2
val arg_2 = t_1 + h/2*k1t_2
val k2w_2 = -g/L * (arg_2 - arg_2 * arg_2 * arg_2/6 + arg_2 * arg_2 * arg_2 * arg_2 * arg_2/120)
val t_2 = t_1 + h*k2t_2
val w_2 = w_1 + h*k2w_2
// loop 3
val k1t_3 = w_2
val k1w_3 = -g/L * (t_2 - t_2 * t_2 * t_2/6 + t_2 * t_2 * t_2 * t_2 * t_2/120)
val k2t_3 = w_2 + h/2*k1w_3
val arg_3 = t_2 + h/2*k1t_3
val k2w_3 = -g/L * (arg_3 - arg_3 * arg_3 * arg_3/6 + arg_3 * arg_3 * arg_3 * arg_3 * arg_3/120)
t_2 + h*k2t_3
}
def pendulumW3(t_0: Real, w_0: Real): Real = {
require(-2 <= t_0 && t_0 <= 2 && -5 <= w_0 && w_0 <= 5)
val h: Real = 0.01
val L: Real = 2.0
val m: Real = 1.5
val g: Real = 9.80665
// loop 1
val k1t_1 = w_0
val k1w_1 = -g/L * (t_0 - t_0 * t_0 * t_0/6 + t_0 * t_0 * t_0 * t_0 * t_0/120)
val k2t_1 = w_0 + h/2*k1w_1
val arg_1 = t_0 + h/2*k1t_1
val k2w_1 = -g/L * (arg_1 - arg_1 * arg_1 * arg_1/6 + arg_1 * arg_1 * arg_1 * arg_1 * arg_1/120)
val t_1 = t_0 + h*k2t_1
val w_1 = w_0 + h*k2w_1
// loop 2
val k1t_2 = w_1
val k1w_2 = -g/L * (t_1 - t_1 * t_1 * t_1/6 + t_1 * t_1 * t_1 * t_1 * t_1/120)
val k2t_2 = w_1 + h/2*k1w_2
val arg_2 = t_1 + h/2*k1t_2
val k2w_2 = -g/L * (arg_2 - arg_2 * arg_2 * arg_2/6 + arg_2 * arg_2 * arg_2 * arg_2 * arg_2/120)
val t_2 = t_1 + h*k2t_2
val w_2 = w_1 + h*k2w_2
// loop 3
val k1t_3 = w_2
val k1w_3 = -g/L * (t_2 - t_2 * t_2 * t_2/6 + t_2 * t_2 * t_2 * t_2 * t_2/120)
val k2t_3 = w_2 + h/2*k1w_3
val arg_3 = t_2 + h/2*k1t_3
val k2w_3 = -g/L * (arg_3 - arg_3 * arg_3 * arg_3/6 + arg_3 * arg_3 * arg_3 * arg_3 * arg_3/120)
w_2 + h*k2w_3
}
def pendulumT5(t_0: Real, w_0: Real): Real = {
require(-2 <= t_0 && t_0 <= 2 && -5 <= w_0 && w_0 <= 5)
val h: Real = 0.01
val L: Real = 2.0
val m: Real = 1.5
val g: Real = 9.80665
// loop 1
val k1t_1 = w_0
val k1w_1 = -g/L * (t_0 - t_0 * t_0 * t_0/6 + t_0 * t_0 * t_0 * t_0 * t_0/120)
val k2t_1 = w_0 + h/2*k1w_1
val arg_1 = t_0 + h/2*k1t_1
val k2w_1 = -g/L * (arg_1 - arg_1 * arg_1 * arg_1/6 + arg_1 * arg_1 * arg_1 * arg_1 * arg_1/120)
val t_1 = t_0 + h*k2t_1
val w_1 = w_0 + h*k2w_1
// loop 2
val k1t_2 = w_1
val k1w_2 = -g/L * (t_1 - t_1 * t_1 * t_1/6 + t_1 * t_1 * t_1 * t_1 * t_1/120)
val k2t_2 = w_1 + h/2*k1w_2
val arg_2 = t_1 + h/2*k1t_2
val k2w_2 = -g/L * (arg_2 - arg_2 * arg_2 * arg_2/6 + arg_2 * arg_2 * arg_2 * arg_2 * arg_2/120)
val t_2 = t_1 + h*k2t_2
val w_2 = w_1 + h*k2w_2
// loop 3
val k1t_3 = w_2
val k1w_3 = -g/L * (t_2 - t_2 * t_2 * t_2/6 + t_2 * t_2 * t_2 * t_2 * t_2/120)
val k2t_3 = w_2 + h/2*k1w_3
val arg_3 = t_2 + h/2*k1t_3
val k2w_3 = -g/L * (arg_3 - arg_3 * arg_3 * arg_3/6 + arg_3 * arg_3 * arg_3 * arg_3 * arg_3/120)
val t_3 = t_2 + h*k2t_3
val w_3 = w_2 + h*k2w_3
// loop 4
val k1t_4 = w_3
val k1w_4 = -g/L * (t_3 - t_3 * t_3 * t_3/6 + t_3 * t_3 * t_3 * t_3 * t_3/120)
val k2t_4 = w_3 + h/2*k1w_4
val arg_4 = t_3 + h/2*k1t_4
val k2w_4 = -g/L * (arg_4 - arg_4 * arg_4 * arg_4/6 + arg_4 * arg_4 * arg_4 * arg_4 * arg_4/120)
val t_4 = t_3 + h*k2t_4
val w_4 = w_3 + h*k2w_4
// loop 5
val k1t_5 = w_4
val k1w_5 = -g/L * (t_4 - t_4 * t_4 * t_4/6 + t_4 * t_4 * t_4 * t_4 * t_4/120)
val k2t_5 = w_4 + h/2*k1w_5
val arg_5 = t_4 + h/2*k1t_5
val k2w_5 = -g/L * (arg_5 - arg_5 * arg_5 * arg_5/6 + arg_5 * arg_5 * arg_5 * arg_5 * arg_5/120)
t_4 + h*k2t_5
}
def pendulumW5(t_0: Real, w_0: Real): Real = {
require(-2 <= t_0 && t_0 <= 2 && -5 <= w_0 && w_0 <= 5)
val h: Real = 0.01
val L: Real = 2.0
val m: Real = 1.5
val g: Real = 9.80665
// loop 1
val k1t_1 = w_0
val k1w_1 = -g/L * (t_0 - t_0 * t_0 * t_0/6 + t_0 * t_0 * t_0 * t_0 * t_0/120)
val k2t_1 = w_0 + h/2*k1w_1
val arg_1 = t_0 + h/2*k1t_1
val k2w_1 = -g/L * (arg_1 - arg_1 * arg_1 * arg_1/6 + arg_1 * arg_1 * arg_1 * arg_1 * arg_1/120)
val t_1 = t_0 + h*k2t_1
val w_1 = w_0 + h*k2w_1
// loop 2
val k1t_2 = w_1
val k1w_2 = -g/L * (t_1 - t_1 * t_1 * t_1/6 + t_1 * t_1 * t_1 * t_1 * t_1/120)
val k2t_2 = w_1 + h/2*k1w_2
val arg_2 = t_1 + h/2*k1t_2
val k2w_2 = -g/L * (arg_2 - arg_2 * arg_2 * arg_2/6 + arg_2 * arg_2 * arg_2 * arg_2 * arg_2/120)
val t_2 = t_1 + h*k2t_2
val w_2 = w_1 + h*k2w_2
// loop 3
val k1t_3 = w_2
val k1w_3 = -g/L * (t_2 - t_2 * t_2 * t_2/6 + t_2 * t_2 * t_2 * t_2 * t_2/120)
val k2t_3 = w_2 + h/2*k1w_3
val arg_3 = t_2 + h/2*k1t_3
val k2w_3 = -g/L * (arg_3 - arg_3 * arg_3 * arg_3/6 + arg_3 * arg_3 * arg_3 * arg_3 * arg_3/120)
val t_3 = t_2 + h*k2t_3
val w_3 = w_2 + h*k2w_3
// loop 4
val k1t_4 = w_3
val k1w_4 = -g/L * (t_3 - t_3 * t_3 * t_3/6 + t_3 * t_3 * t_3 * t_3 * t_3/120)
val k2t_4 = w_3 + h/2*k1w_4
val arg_4 = t_3 + h/2*k1t_4
val k2w_4 = -g/L * (arg_4 - arg_4 * arg_4 * arg_4/6 + arg_4 * arg_4 * arg_4 * arg_4 * arg_4/120)
val t_4 = t_3 + h*k2t_4
val w_4 = w_3 + h*k2w_4
// loop 5
val k1t_5 = w_4
val k1w_5 = -g/L * (t_4 - t_4 * t_4 * t_4/6 + t_4 * t_4 * t_4 * t_4 * t_4/120)
val k2t_5 = w_4 + h/2*k1w_5
val arg_5 = t_4 + h/2*k1t_5
val k2w_5 = -g/L * (arg_5 - arg_5 * arg_5 * arg_5/6 + arg_5 * arg_5 * arg_5 * arg_5 * arg_5/120)
w_4 + h*k2w_5
}
}
import daisy.lang._
import Real._
object RigidBody {
//x1, x2, x3: < 1, 16 11>, [-15, 15]
def out1(x1: Real, x2: Real, x3: Real): Real = {
require(-15 <= x1 && x1 <= 15 && -15 <= x2 && x2 <= 15 && -15 <= x3 && x3 <= 15)
( -1 * x1)*x2 - 2*x2*x3 - x1 - x3
def rigidBody1(x1: Real, x2: Real, x3: Real): Real = {
require(-15.0 <= x1 && x1 <= 15 && -15.0 <= x2 && x2 <= 15.0 && -15.0 <= x3 && x3 <= 15)
-x1*x2 - 2*x2*x3 - x1 - x3
}
// apparently this needs 17 bits, or we've not been accurate enough
def out2(x1: Real, x2: Real, x3: Real): Real = {
require(-15 <= x1 && x1 <= 15 && -15 <= x2 && x2 <= 15 && -15 <= x3 && x3 <= 15)
2*x1*x2*x3 + 3*x3*x3 - x2*x1*x2*x3 + 3*x3*x3 - x2
def rigidBody2(x1: Real, x2: Real, x3: Real): Real = {
require(-15.0 <= x1 && x1 <= 15 && -15.0 <= x2 && x2 <= 15.0 &&
-15.0 <= x3 && x3 <= 15)
2*(x1*x2*x3) + (3*x3*x3) - x2*(x1*x2*x3) + (3*x3*x3) - x2
}
}
}
\ No newline at end of file
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)