Commit 55429026 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Shorten some clone declarations

parent 8ad23fe1
...@@ -986,7 +986,7 @@ use RationalCoeffs ...@@ -986,7 +986,7 @@ use RationalCoeffs
use real.RealInfix use real.RealInfix
use real.FromInt use real.FromInt
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal . clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( * ) = ( *. ), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=int -> real, function C.interp=rinterp, exception C.Unknown = QError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, goal .
end end
...@@ -1031,7 +1031,7 @@ let iinv (t:t') : t' ...@@ -1031,7 +1031,7 @@ let iinv (t:t') : t'
raises { NError -> true } raises { NError -> true }
= raise NError = raise NError
clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t', type C.cvars = int->int,function C.interp = interp_id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = izero, val C.cone = ione, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = iadd, val C.mul = imul, val C.opp = iopp, val C.eq = ieq, val C.inv = iinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal . clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t', type C.cvars = int->int,function C.interp = interp_id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = izero, val C.cone = ione, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = iadd, val C.mul = imul, val C.opp = iopp, val C.eq = ieq, val C.inv = iinv, goal .
use real.FromInt use real.FromInt
...@@ -1402,7 +1402,7 @@ use real.RealInfix ...@@ -1402,7 +1402,7 @@ use real.RealInfix
type coeff = t type coeff = t
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.(*) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = MPError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal . clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.(*) = ( *.), function C.(-_) = (-._), function C.(-) = (-.), type coeff = t, type C.cvars=evars, function C.interp=minterp, exception C.Unknown = MPError, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=mzero, val C.cone=mone, lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add=madd, val C.mul=mmul, val C.opp=mopp, val C.eq=meq, val C.inv=minv, goal .
end end
module LinearDecisionIntMP module LinearDecisionIntMP
...@@ -1452,7 +1452,7 @@ let mpinv (a:t) : t ...@@ -1452,7 +1452,7 @@ let mpinv (a:t) : t
= raise MPError = raise MPError
clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal C.A.ZeroLessOne, goal C.A.CompatOrderAdd, goal C.A.CompatOrderMult, goal C.A.Unitary, goal C.A.NonTrivialRing, goal C.A.Mul_distr_l, goal C.A.Mul_distr_r, goal C.A.Inv_def_l, goal C.A.Inv_def_r, goal C.A.MulAssoc.Assoc, goal C.A.Assoc, goal C.A.MulComm.Comm, goal C.A.Comm, goal C.A.Unit_def_l, goal C.A.Unit_def_r, goal . clone export LinearEquationsDecision with type C.a = int, function C.(+) = (+), function C.(*) = (*), function C.(-_) = (-_), function C.(-) = (-), type coeff = t, type C.cvars = int->int, function C.interp = mpinterp, constant C.azero = zero, constant C.aone = one, val C.czero = mpzero, val C.cone = mpone, predicate C.ale = (<=), lemma C.sub_def, lemma C.zero_def, lemma C.one_def, val C.add = mpadd, val C.mul = mpmul, val C.opp = mpopp, val C.eq = mpeq, val C.inv = mpinv, goal .
use LinearDecisionRationalMP as R use LinearDecisionRationalMP as R
use real.FromInt use real.FromInt
......
...@@ -169,10 +169,10 @@ ...@@ -169,10 +169,10 @@
<proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="15"/></proof> <proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="15"/></proof>
</goal> </goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true"> <goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
<proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="10"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC sprod.4" expl="exceptional postcondition" proved="true"> <goal name="VC sprod.4" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="4" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="10"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -1316,7 +1316,7 @@ ...@@ -1316,7 +1316,7 @@
</goal> </goal>
<goal name="VC linear_decision.17" expl="precondition" proved="true"> <goal name="VC linear_decision.17" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof> <proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="32"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="32"/></proof>
</goal> </goal>
<goal name="VC linear_decision.18" expl="precondition" proved="true"> <goal name="VC linear_decision.18" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="82"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="82"/></proof>
...@@ -1326,24 +1326,24 @@ ...@@ -1326,24 +1326,24 @@
</goal> </goal>
<goal name="VC linear_decision.20" expl="precondition" proved="true"> <goal name="VC linear_decision.20" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof> <proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="32"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="32"/></proof>
</goal> </goal>
<goal name="VC linear_decision.21" expl="precondition" proved="true"> <goal name="VC linear_decision.21" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="82"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="82"/></proof>
</goal> </goal>
<goal name="VC linear_decision.22" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.22" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.23" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.23" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.24" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.24" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.25" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.25" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.26" expl="assertion" proved="true"> <goal name="VC linear_decision.26" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof> <proof prover="2"><result status="valid" time="0.04"/></proof>
...@@ -1361,10 +1361,10 @@ ...@@ -1361,10 +1361,10 @@
<proof prover="4"><result status="valid" time="0.02" steps="96"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="96"/></proof>
</goal> </goal>
<goal name="VC linear_decision.31" expl="integer overflow" proved="true"> <goal name="VC linear_decision.31" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="37"/></proof>
</goal> </goal>
<goal name="VC linear_decision.32" expl="variant decrease" proved="true"> <goal name="VC linear_decision.32" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="37"/></proof>
</goal> </goal>
<goal name="VC linear_decision.33" expl="precondition" proved="true"> <goal name="VC linear_decision.33" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
...@@ -1377,13 +1377,12 @@ ...@@ -1377,13 +1377,12 @@
</goal> </goal>
<goal name="VC linear_decision.36" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.36" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.37" expl="integer overflow" proved="true"> <goal name="VC linear_decision.37" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal> </goal>
<goal name="VC linear_decision.38" expl="variant decrease" proved="true"> <goal name="VC linear_decision.38" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
</goal> </goal>
<goal name="VC linear_decision.39" expl="precondition" proved="true"> <goal name="VC linear_decision.39" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="94"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="94"/></proof>
...@@ -1396,6 +1395,7 @@ ...@@ -1396,6 +1395,7 @@
</goal> </goal>
<goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.42" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.43" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
...@@ -1426,16 +1426,16 @@ ...@@ -1426,16 +1426,16 @@
<proof prover="4"><result status="valid" time="0.02" steps="92"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="92"/></proof>
</goal> </goal>
<goal name="VC linear_decision.52" expl="integer overflow" proved="true"> <goal name="VC linear_decision.52" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="35"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal> </goal>
<goal name="VC linear_decision.53" expl="variant decrease" proved="true"> <goal name="VC linear_decision.53" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="35"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="35"/></proof>
</goal> </goal>
<goal name="VC linear_decision.54" expl="precondition" proved="true"> <goal name="VC linear_decision.54" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="90"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="90"/></proof>
</goal> </goal>
<goal name="VC linear_decision.55" expl="precondition" proved="true"> <goal name="VC linear_decision.55" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="40"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="40"/></proof>
</goal> </goal>
<goal name="VC linear_decision.56" expl="precondition" proved="true"> <goal name="VC linear_decision.56" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
...@@ -1444,16 +1444,16 @@ ...@@ -1444,16 +1444,16 @@
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.58" expl="integer overflow" proved="true"> <goal name="VC linear_decision.58" expl="integer overflow" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof> <proof prover="4"><result status="valid" time="0.03" steps="35"/></proof>
</goal> </goal>
<goal name="VC linear_decision.59" expl="variant decrease" proved="true"> <goal name="VC linear_decision.59" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="35"/></proof> <proof prover="4"><result status="valid" time="0.01" steps="35"/></proof>
</goal> </goal>
<goal name="VC linear_decision.60" expl="precondition" proved="true"> <goal name="VC linear_decision.60" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="90"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="90"/></proof>
</goal> </goal>
<goal name="VC linear_decision.61" expl="precondition" proved="true"> <goal name="VC linear_decision.61" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="40"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="40"/></proof>
</goal> </goal>
<goal name="VC linear_decision.62" expl="precondition" proved="true"> <goal name="VC linear_decision.62" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="37"/></proof> <proof prover="4"><result status="valid" time="0.02" steps="37"/></proof>
...@@ -1511,17 +1511,17 @@ ...@@ -1511,17 +1511,17 @@
</goal> </goal>
<goal name="VC linear_decision.80" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.80" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.81" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.81" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.82" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.82" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.83" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.83" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="10"/></proof>
</goal> </goal>
<goal name="VC linear_decision.84" expl="precondition" proved="true"> <goal name="VC linear_decision.84" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
...@@ -1572,16 +1572,16 @@ ...@@ -1572,16 +1572,16 @@
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.99" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.99" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC linear_decision.100" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.100" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.101" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.101" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC linear_decision.102" expl="exceptional postcondition" proved="true"> <goal name="VC linear_decision.102" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
...@@ -3174,13 +3174,13 @@ ...@@ -3174,13 +3174,13 @@
<proof prover="2"><result status="valid" time="0.23"/></proof> <proof prover="2"><result status="valid" time="0.23"/></proof>
</goal> </goal>
<goal name="VC mp_decision.4" expl="exceptional postcondition" proved="true"> <goal name="VC mp_decision.4" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.02"/></proof>
</goal> </goal>
<goal name="VC mp_decision.5" expl="exceptional postcondition" proved="true"> <goal name="VC mp_decision.5" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
<goal name="VC mp_decision.6" expl="exceptional postcondition" proved="true"> <goal name="VC mp_decision.6" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof> <proof prover="2"><result status="valid" time="0.01"/></proof>
</goal> </goal>
</transf> </transf>
</goal> </goal>
......
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