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

Secondary decision procedure for integer coefficients

parent 4990a611
......@@ -4,8 +4,11 @@ type a
function (+) a a : a
function ( *) a a : a
function (-_) a : a
function azero: a
function aone: a
predicate ale a a
clone algebra.OrderedUnitaryCommutativeRing as A with type t = a, function (+) = (+), function ( *) = ( *), function (-_) = (-_)
clone algebra.OrderedUnitaryCommutativeRing as A with type t = a, function (+) = (+), function ( *) = ( *), function (-_) = (-_), constant zero = azero, constant one=aone, predicate (<=) = ale
type t
type vars = int -> a
......@@ -17,10 +20,9 @@ function interp t vars : a
val constant czero : t
val constant cone : t
axiom zero_def: forall y. interp czero y = A.zero
axiom one_def: forall y. interp cone y = A.one
axiom zero_def: forall y. interp czero y = azero
axiom one_def: forall y. interp cone y = aone
predicate (<=) t t
val add (a b: t) : t
ensures { forall v: vars. interp result v = interp a v + interp b v }
......@@ -39,13 +41,12 @@ axiom eq_def: forall a b: t. a=b -> eq a b
val inv (a:t) : t
requires { not (eq a czero) }
ensures { forall v: vars. interp result v * interp a v = A.one }
ensures { forall v: vars. interp result v * interp a v = aone }
ensures { not (eq result czero) }
raises { Unknown -> true }
val le (a b:t) : bool
ensures { result <-> a <= b }
ensures { result -> forall y:vars. A.(<=) (interp a y) (interp b y) }
ensures { result -> forall y:vars. ale (interp a y) (interp b y) }
raises { Unknown -> true }
......@@ -410,6 +411,7 @@ let linear_decision (l: context) (g: equality) : bool
let a = Matrix.make (length l) (nv+1) C.czero in
let b = Array.make (length l) C.czero in (* ax = b *)
let v = Array.make (nv+1) C.czero in (* goal *)
(*v[0] <- any coeff;*)
let rec fill_expr (ex: expr) (i:int): unit
variant { ex }
requires { no_cst ex }
......@@ -447,7 +449,7 @@ let linear_decision (l: context) (g: equality) : bool
| Term c j -> v[j] <- C.add v[j] c
| UTerm j -> v[j] <- C.add v[j] C.cone
| Add e1 e2 -> fill_goal e1; fill_goal e2
end in
end in
fill_ctx l 0;
let (ex, d) = norm_eq g in
fill_goal ex;
......@@ -565,12 +567,81 @@ use import RationalCoeffs
use import real.RealInfix
use import real.FromInt
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( *) = ( *.), type coeff = t, function C.interp=rinterp, val C.czero=rzero, val C.cone=rone, 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, lemma C.eq_def, predicate C.(<=)=(<=), val C.le=rle(*, goal ZeroLessOne, goal C.CompatOrderAdd, goal C.CompatOrderMult, goal C.Unitary, goal C.NonTrivialRing, goal C.Mul_distr_l, goal C.Mul_distr_r, goal C.Inv_def_l, goal C.Inv_def_r, goal C.MulAssoc.Assoc, goal C.Assoc, goal C.MulComm.Comm, goal C.Comm, goal C.Unit_def_l, goal C.Unit_def_r*)
clone export LinearEquationsDecision with type C.a = real, function C.(+) = (+.), function C.( *) = ( *.), type coeff = t, function C.interp=rinterp, constant C.azero = Real.zero, constant C.aone = Real.one, predicate C.ale = (<=.), val C.czero=rzero, val C.cone=rone, 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, lemma C.eq_def, val C.le=rle(*, goal ZeroLessOne, goal C.CompatOrderAdd, goal C.CompatOrderMult, goal C.Unitary, goal C.NonTrivialRing, goal C.Mul_distr_l, goal C.Mul_distr_r, goal C.Inv_def_l, goal C.Inv_def_r, goal C.MulAssoc.Assoc, goal C.Assoc, goal C.MulComm.Comm, goal C.Comm, goal C.Unit_def_l, goal C.Unit_def_r*)
end
module LinearDecisionInt
use import int.Int
function id (t:int) (v:int -> int) : int = t
let predicate eq (a b:int) = a=b
exception Unknown
let inv (t:int) : int
ensures { forall v: int -> int. id result v * id t v = one }
ensures { not (eq result zero) }
raises { Unknown -> true }
= raise Unknown
clone export LinearEquationsDecision with type C.a = int, function C.(+)=(+), function C.(*) = (*), type coeff = int, function C.interp = id, constant C.azero = zero, constant C.aone = one, predicate C.ale= (<=), val C.czero = zero, val C.cone = one, lemma C.zero_def, lemma C.one_def, val C.add = (+), val C.mul = ( *), val C.opp = (-_), val C.eq = eq, val C.inv = inv, lemma C.eq_def, val C.le = (<=)(*, goal ZeroLessOne, goal C.CompatOrderAdd, goal C.CompatOrderMult, goal C.Unitary, goal C.NonTrivialRing, goal C.Mul_distr_l, goal C.Mul_distr_r, goal C.Inv_def_l, goal C.Inv_def_r, goal C.MulAssoc.Assoc, goal C.Assoc, goal C.MulComm.Comm, goal C.Comm, goal C.Unit_def_l, goal C.Unit_def_r*)
use import real.FromInt
axiom from_int_ext: forall x y: int. from_int x = from_int y -> x = y
(*FIXME put this in real.why ?*)
use import RationalCoeffs
use LinearDecisionRational as R
use import list.List
let function m (x:int) : (int, int)
ensures { forall z. rinterp result z = from_int x }
= (x,1)
val function m_y (y:int->int): (int -> real)
ensures { forall i. result i = from_int (y i) }
let rec function m_expr (e:expr) : R.expr
ensures { forall y z. R.interp result (m_y y) (m_y z) = from_int (interp e y z) }
ensures { valid_expr e -> R.valid_expr result }
= match e with
| Cst c -> R.Cst (m c)
| Add e1 e2 -> R.Add (m_expr e1) (m_expr e2)
| Term c n -> R.Term (m c) n
| UTerm n -> R.UTerm n
end
let function m_eq (eq:equality) : R.equality
ensures { forall y z. R.interp_eq result (m_y y) (m_y z)
<-> interp_eq eq y z }
ensures { valid_eq eq -> R.valid_eq result }
= match eq with (e1,e2) -> (m_expr e1, m_expr e2) end
let rec function m_ctx (ctx:context) : R.context
ensures { forall y z g. R.interp_ctx result (m_eq g) (m_y y) (m_y z) <->
interp_ctx ctx g y z }
ensures { valid_ctx ctx -> R.valid_ctx result }
variant { ctx }
= match ctx with
| Nil -> Nil
| Cons h t ->
let r = Cons (m_eq h) (m_ctx t) in
r
end
let int_decision (l: context) (g: equality) : bool
requires { valid_ctx l }
requires { valid_eq g }
ensures { forall y z. result -> interp_ctx l g y z }
(*raises { R.Unknown -> true } ??? *)
= R.linear_decision (m_ctx l) (m_eq g)
end
theory Test
module Test
use import RationalCoeffs
use import LinearDecisionRational
......@@ -584,4 +655,16 @@ goal g: forall x y: real.
(from_int 3 /. from_int 1) *. x +. (from_int 2/. from_int 1) *. y = (from_int 21/. from_int 1) ->
(from_int 7 /. from_int 1) *. x +. (from_int 4/. from_int 1) *. y = (from_int 47/. from_int 1) ->
x = (from_int 5 /. from_int 1)
end
module TestInt
use import LinearDecisionInt
use import int.Int
goal g: forall x y:int.
3 * x + 2 * y = 21 ->
7 * x + 4 * y = 47 ->
x = 5
end
\ No newline at end of file
......@@ -7,7 +7,7 @@
<prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<file name="../lineardecision.mlw">
<theory name="LinearEquationsCoeffs" proved="true" sum="9a492c8352466a6dee74d1090e1a1957">
<theory name="LinearEquationsCoeffs" proved="true" sum="685014f973f4d07d28f06838ac5cdd5b">
<goal name="VC czero" expl="VC for czero" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
......@@ -16,7 +16,7 @@
</transf>
</goal>
</theory>
<theory name="LinearEquationsDecision" sum="91c33aade3c83b1b80d8470fd201fc98">
<theory name="LinearEquationsDecision" sum="b695f28a460bd340d97cabf1d4fc961e">
<goal name="VC valid_expr" expl="VC for valid_expr" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -915,7 +915,7 @@
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="LinearDecisionRational" sum="144503a85d2c74be8d0cd6efa1bcf82a">
<theory name="LinearDecisionRational" sum="6d1c037b8daef1dcbc5771dc012e19e8">
<goal name="C.VC czero" expl="VC for czero" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
......@@ -930,7 +930,9 @@
<goal name="one_def.0" proved="true">
<transf name="replace" proved="true" arg1="one" arg2="1.0">
<goal name="one_def.0.0" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="one_def.0.1" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......@@ -940,41 +942,132 @@
</transf>
</goal>
<goal name="C.VC add" expl="VC for add">
<proof prover="0" timelimit="1" memlimit="1000"><result status="timeout" time="1.01"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.01"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
<transf name="compute_in_goal" >
<goal name="VC add.0" expl="VC for add">
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.05"/></proof>
<transf name="split_goal_wp" >
<goal name="VC add.0.0" expl="postcondition">
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.01"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2" obsolete="true"><result status="unknown" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="C.VC mul" expl="VC for mul">
<proof prover="0" timelimit="1" memlimit="1000"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="C.VC opp" expl="VC for opp">
<proof prover="0" timelimit="1" memlimit="1000"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="unknown" time="0.08"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="C.VC eq" expl="VC for eq">
<proof prover="0" timelimit="1" memlimit="1000"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="unknown" time="2.02"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="C.eq_def" proved="true">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="7"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="C.VC inv" expl="VC for inv">
<proof prover="0" timelimit="1" memlimit="1000"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="unknown" time="1.83"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="C.VC le" expl="VC for le">
<proof prover="0" timelimit="1" memlimit="1000"><result status="timeout" time="1.00"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="timeout" time="1.00"/></proof>
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
</theory>
<theory name="Test" proved="true" sum="33853f7837c4f4d6bab68b027a33b66e">
<theory name="LinearDecisionInt" proved="true" sum="afb9a8464da81d5b3ccb3102d55744d8">
<goal name="VC eq" expl="VC for eq" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC inv" expl="VC for inv" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="C.VC czero" expl="VC for czero" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="C.VC cone" expl="VC for cone" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="C.zero_def" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="C.one_def" proved="true">
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="unknown" time="0.02"/></proof>
<proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="C.VC add" expl="VC for add" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="C.VC mul" expl="VC for mul" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="C.VC opp" expl="VC for opp" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="C.VC eq" expl="VC for eq" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="C.eq_def" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="C.VC inv" expl="VC for inv" proved="true">
<proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="unknown" time="0.02"/></proof>
<proof prover="1" obsolete="true"><result status="unknown" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.03"/></proof>
<proof prover="3" obsolete="true"><result status="timeout" time="4.90"/></proof>
</goal>
<goal name="C.VC le" expl="VC for le" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC le.0" expl="postcondition" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</transf>
</goal>
<goal name="VC m" expl="VC for m" proved="true">
<proof prover="2"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC m_expr" expl="VC for m_expr" proved="true">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.22" steps="948"/></proof>
</goal>
<goal name="VC m_eq" expl="VC for m_eq" proved="true">
<proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.20" steps="502"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC m_ctx" expl="VC for m_ctx" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC int_decision" expl="VC for int_decision" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC int_decision.0" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC int_decision.1" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC int_decision.2" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Test" proved="true" sum="ab0b253dc8934f6b8b809d076e773229">
<goal name="g" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="g.0" proved="true">
......@@ -1007,5 +1100,34 @@
</transf>
</goal>
</theory>
<theory name="TestInt" proved="true" sum="0beb25acdb946ef5d3faa0985649b949">
<goal name="g" proved="true">
<transf name="reflection_f" proved="true" arg1="int_decision">
<goal name="g.0" expl="reification check" proved="true">
<transf name="revert" proved="true" arg1="HR">
<goal name="g.0.0" expl="reification check" proved="true">
<transf name="compute_in_goal" proved="true" >
<goal name="g.0.0.0" expl="reification check" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="g.1" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g.2" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
<goal name="g.3" proved="true">
<transf name="compute_in_goal" proved="true" >
</transf>
</goal>
</transf>
</goal>
</theory>
</file>
</why3session>
......@@ -41,6 +41,13 @@ let init_renv kn lv env task =
task = task;
}
let rec is_const t = match t.t_node with
| Tconst _ -> true
| Tvar _ -> false
| Tapp (_, []) -> false
| Tapp (_, l) -> List.for_all is_const l
| _ -> false
let rec reify_term renv t rt =
let rec invert_nonvar_pat vl (renv:reify_env) interp (p,f) t =
if debug
......@@ -86,6 +93,7 @@ let rec reify_term renv t rt =
-> if debug then Format.printf "case interp@.";
invert_interp renv ls t
| Papp (cs, [{pat_node = Pvar _}]), Tapp(ls, _hd::_tl), _
when is_const t
-> if debug then Format.printf "case const@.";
let renv, rt = invert_interp renv ls t in
renv, (t_app cs [rt] (Some p.pat_ty))
......@@ -132,6 +140,13 @@ let rec reify_term renv t rt =
end
| _ -> raise NoReification
and invert_pat vl renv interp (p,f) t =
(if not (oty_equal f.t_ty t.t_ty)
then
(if debug
then Format.printf "type mismatch between %a and %a@."
Pretty.print_ty (Opt.get f.t_ty)
Pretty.print_ty (Opt.get t.t_ty);
raise NoReification));
try invert_nonvar_pat vl renv interp (p,f) t
with NoReification -> invert_var_pat vl renv interp (p,f) t
and invert_interp renv ls (t:term) = (*la ?*)
......@@ -229,7 +244,7 @@ let rec reify_term renv t rt =
(renv,(t_app cons [req; ctx] (Some ty_list_g)))
with
| NoReification -> renv,ctx
| TypeMismatch _ -> raise NoReification
(* | TypeMismatch _ -> raise NoReification*)
end
| _-> renv,ctx)
(renv, (t_app nil [] (Some ty_list_g))) renv.task in
......@@ -1017,18 +1032,25 @@ let reflection_by_function s env = Trans.store (fun task ->
let (lp, lv, rt) = Apply.intros p in
let lv = lv @ args in
let renv = reify_term (init_renv kn lv env prev) g rt in
if debug then Format.printf "computing args@.";
let vars =
List.fold_left
(fun vars (vs, t) ->
if List.mem vs args
then begin
if debug then Format.printf "value of term %a for arg %a@."
Pretty.print_term t
Pretty.print_vs vs;
Mid.add vs.vs_name (value_of_term t) vars end
else vars)
Mid.empty
(Mvs.bindings renv.subst) in
let info = { env = env;
mm = mm;
funs = Mrs.empty;
recs = Mrs.empty;
vars =
List.fold_left
(fun vars (vs, t) ->
if List.mem vs args
then Mid.add vs.vs_name (value_of_term t) vars
else vars)
Mid.empty
(Mvs.bindings renv.subst) } in
vars = vars
} in
if debug then Format.printf "eval_fun@.";
let res = term_of_value (eval_fun decl info) in
if debug then Format.printf "res %a@." Pretty.print_term res;
......
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