Commit 5fc14d2d authored by erwan's avatar erwan

Fix: Merge branch '2-issue-with-free-variables-constrained-in-the-type-declaration' (closes #2)

parents 2665211b ccb8b62b
Pipeline #26586 passed with stages
in 8 minutes and 52 seconds
-- ok works fine, but not ko:
node ko () returns (b: int [0; 0]; a: int) = a = b
node ok () returns (a: int [0; 0]; b: int) = a = b
......@@ -106,8 +106,8 @@ let (substl_to_string : subst list -> string) =
fun sl ->
(List.fold_left
(fun acc ((vn, a), ne) ->
(acc ^ " " ^ (Value.num_value_to_string a) ^ "." ^ vn ^
" -> " ^ to_string ne ^ "\n")
(acc ^ " " ^ (Value.num_value_to_string a) ^ "." ^ vn ^
" -> " ^ to_string ne ^ "\n")
)
""
sl
......@@ -369,7 +369,7 @@ let (split : t -> split_res) =
let divide c1 c2 =
match (c1,c2) with
| I i1, I i2 -> Num.eq_num (Num.mod_num i2 i1) (Num.Int 0)
| _ ,_ -> true
| _, _ -> assert false (* used to be "true" instead, but it looked weird! *)
in
let cl = (StringMap.fold (fun v c acc -> (c,v)::acc) ne []) in
let res =
......
......@@ -144,67 +144,61 @@ let default_max_int = (Num.Int lucky_max_int)
let default_min_int = (Num.Int (-lucky_max_int))
let zero = Num.Int 0
let one_of_num = function
| I _ -> I (Num.Int 1)
| F _ -> F 1.0
(* exported *)
let (create : Exp.var list -> t) =
fun var_l ->
let (add_one_var : range_store -> Exp.var -> range_store) =
fun tbl var ->
let (add_one_var : range_store * Ne.subst list -> Exp.var ->
range_store * Ne.subst list) =
fun (tbl,sl) var ->
let to_num_opt = function
| Some(Numer(Ival(min))) -> Some (Ival(min))
| Some(Numer(Uminus(Ival(min)))) -> Some (Ival(Num.minus_num min))
| Some(Numer(Fval(min))) -> Some (Fval(min))
| Some(Numer(Uminus(Fval(min)))) -> Some (Fval(-.min))
| None -> None
| _ ->
output_string stderr "Only immediate constant are allowed in variable ranges.\n";
flush stderr;
assert false
| _ -> output_string stderr
"Only immediate constant are allowed in variable ranges.\n";
flush stderr;
assert false
in
let range = (
let range =
match (to_num_opt (Var.min var)), (to_num_opt (Var.max var)) with
| Some(Ival(min)), Some(Ival(max)) ->
RangeI(min, max)
| None, Some(Ival(max)) ->
RangeI(default_min_int, max)
| Some(Ival(min)), None ->
RangeI(min, default_max_int)
| Some(Fval(min)), Some(Fval(max)) ->
RangeF(min, max)
| None, Some(Fval(max)) ->
RangeF(default_min_float, max)
| Some(Fval(min)), None ->
RangeF(min, default_max_float)
| None, None -> (
match Var.typ var with
Type.IntT -> RangeI(default_min_int, default_max_int)
| Type.FloatT -> RangeF(default_min_float, default_max_float)
| _ -> assert false
)
| _ ->
print_string ((Var.to_string var) ^ "\n");
flush stdout;
assert false
)
| Some(Ival(min)), Some(Ival(max)) -> RangeI(min, max)
| None, Some(Ival(max)) -> RangeI(default_min_int, max)
| Some(Ival(min)), None -> RangeI(min, default_max_int)
| Some(Fval(min)), Some(Fval(max)) -> RangeF(min, max)
| None, Some(Fval(max)) -> RangeF(default_min_float, max)
| Some(Fval(min)), None -> RangeF(min, default_max_float)
| None, None -> (
match Var.typ var with
Type.IntT -> RangeI(default_min_int, default_max_int)
| Type.FloatT -> RangeF(default_min_float, default_max_float)
| _ -> assert false
)
| _ ->
print_string ((Var.to_string var) ^ "\n"); flush stdout;
assert false
in
StringMap.add (Var.name var) range tbl;
let subst_opt = (* sometimes, range are actually subst ! *)
match range with
| RangeI (n1,n2) -> if n1=n2 then Some (I n1) else None
| RangeF (n1,n2) -> if n1=n2 then Some (F n1) else None
in
match subst_opt with
| Some v -> tbl, ((Var.name var, one_of_num v), Ne.make "" v)::sl
| None -> StringMap.add (Var.name var) range tbl, sl
in
let tbl = List.fold_left (add_one_var) StringMap.empty var_l in
{
var = Range(tbl) ;
substl = [];
delay = [];
untouched = var_l
}
let tbl,sl = List.fold_left (add_one_var) (StringMap.empty,[]) var_l in
{
var = Range(tbl) ;
substl = sl;
delay = [];
untouched = var_l
}
(* Normalised atomic constraints *)
......@@ -301,44 +295,44 @@ let (switch_to_polyhedron_representation_do : int -> t -> t' * p) =
fun verb store ->
(* handle delayed constraints using polyhedron *)
match store.var with
Unsat(_,_) ->
print_string ("\nZZZ Dead code reached, oups...\n") ;
flush stdout;
raise No_polyedral_solution (* this ougth to be dead code ... *)
| Range tbl ->
if
store.delay = []
then
(
{ range = tbl; substl' = store.substl; untouched' = store.untouched }
,
[]
)
else
let (tbl2, touched_vars, poly_l) =
(* side effect: this function also removes from [store] variables
that are put into the polyhedron store *)
Polyhedron.build_poly_list_from_delayed_cstr verb tbl store.delay
in
List.iter
(fun (_, poly, _, _) ->
if Poly.is_empty poly then (
if debug_store then (
print_string (to_string store);
print_string "\n The polyhedron is empty .\n";
flush stdout );
raise No_polyedral_solution
)
)
poly_l;
(
{ range = tbl2; substl' = store.substl ;
untouched' = List.fold_left (rm) store.untouched touched_vars
}
,
poly_l
)
Unsat(_,_) ->
print_string ("\nZZZ Dead code reached, oups...\n") ;
flush stdout;
raise No_polyedral_solution (* this ougth to be dead code ... *)
| Range tbl ->
if
store.delay = []
then
(
{ range = tbl; substl' = store.substl; untouched' = store.untouched }
,
[]
)
else
let (tbl2, touched_vars, poly_l) =
(* side effect: this function also removes from [store] variables
that are put into the polyhedron store *)
Polyhedron.build_poly_list_from_delayed_cstr verb tbl store.delay
in
List.iter
(fun (_, poly, _, _) ->
if Poly.is_empty poly then (
if debug_store then (
print_string (to_string store);
print_string "\n The polyhedron is empty .\n";
flush stdout );
raise No_polyedral_solution
)
)
poly_l;
(
{ range = tbl2; substl' = store.substl ;
untouched' = List.fold_left (rm) store.untouched touched_vars
}
,
poly_l
)
(* tabulate the result as this translation is expensive *)
let poly_table = ref (Hashtbl.create 1)
......@@ -583,10 +577,10 @@ let rec (add_constraint : t -> Formula_to_bdd.t -> Constraint.t -> t) =
if debug_store2 then (
print_string (
"add_constraint (" ^
(string_of_int
(Formula_to_bdd.get_index_from_linear_constraint bddt cstr0)) ^
") " ^
(Constraint.to_string cstr) ^ " \n");
(string_of_int
(Formula_to_bdd.get_index_from_linear_constraint bddt cstr0)) ^
") " ^
(Constraint.to_string cstr) ^ " \n");
flush stdout
);
if debug_store then (
......@@ -607,416 +601,416 @@ let rec (add_constraint : t -> Formula_to_bdd.t -> Constraint.t -> t) =
dim = 0
then
( match cstr with
EqZ(ne) -> add_eq_to_store store bddt ne
| Bv _ -> assert false
| Ineq(GZ(ne)) ->
if
( match (Ne.find "" ne) with
Some v -> Value.num_sup_zero v
| None -> false
)
then
store
else (
if debug_store2 then (
print_string (
"\nAdding constraint " ^ (Constraint.to_string cstr) ^
" leads to an empty store.\n") ;
flush stdout);
unsat_store (Ineq(GZ(ne))) store
)
| Ineq(GeqZ(ne)) ->
if
( match (Ne.find "" ne) with
Some v -> Value.num_supeq_zero v
| None -> true
)
then
store
else (
if debug_store2 then (
print_string (
"\nAdding constraint " ^ (Constraint.to_string cstr) ^
" leads to an empty store.\n") ;
flush stdout);
unsat_store (Ineq(GeqZ(ne))) store
)
EqZ(ne) -> add_eq_to_store store bddt ne
| Bv _ -> assert false
| Ineq(GZ(ne)) ->
if
( match (Ne.find "" ne) with
Some v -> Value.num_sup_zero v
| None -> false
)
then
store
else (
if debug_store2 then (
print_string (
"\nAdding constraint " ^ (Constraint.to_string cstr) ^
" leads to an empty store.\n") ;
flush stdout);
unsat_store (Ineq(GZ(ne))) store
)
| Ineq(GeqZ(ne)) ->
if
( match (Ne.find "" ne) with
Some v -> Value.num_supeq_zero v
| None -> true
)
then
store
else (
if debug_store2 then (
print_string (
"\nAdding constraint " ^ (Constraint.to_string cstr) ^
" leads to an empty store.\n") ;
flush stdout);
unsat_store (Ineq(GeqZ(ne))) store
)
)
else if
dim > 1
then
(*
We could also choose not to delay those constraints and
switch to the polyhedron representation for the concerned
variables there.
(*
We could also choose not to delay those constraints and
switch to the polyhedron representation for the concerned
variables there.
What is the better solution really ???
*)
What is the better solution really ???
*)
( match cstr with
EqZ(ne) -> add_eq_to_store store bddt ne
| Bv _ -> assert false
| Ineq ineq ->
if debug_store then (
let cstr_str = (Constraint.to_string cstr) in
print_string "\n ==> delay " ;
print_string cstr_str;
flush stdout
);
{ var=var ; substl=sl ; delay = ineq::d ;
untouched = uvars}
EqZ(ne) -> add_eq_to_store store bddt ne
| Bv _ -> assert false
| Ineq ineq ->
if debug_store then (
let cstr_str = (Constraint.to_string cstr) in
print_string "\n ==> delay " ;
print_string cstr_str;
flush stdout
);
{ var=var ; substl=sl ; delay = ineq::d ;
untouched = uvars}
)
else
(* dim = 1 *)
match store.var with
Unsat(cstr, store) ->
if debug_store2 then
print_string (
"\nAdding constraint " ^ (Constraint.to_string cstr) ^
" leads to an empty store.\n") ;
unsat_store cstr store
| Range(tbl) ->
( match cstr with
EqZ(ne) -> add_eq_to_store store bddt ne
| Bv _ -> assert false
| Ineq ineq ->
let (vn, nac) = normalise ineq in
( match
(
nac,
try
(mfind vn tbl)
with Not_found ->
print_string ("\n" ^ vn ^
" not found in the table!\n");
StringMap.iter
(fun key range ->
print_string (
"\n\t" ^ key ^ " " ^
(Polyhedron.range_to_string range)
);
)
tbl;
flush stdout;
assert false
)
with
(NSupEqI(i), RangeI(min, max)) ->
if
Num.le_num i min
then
{var=Range(tbl) ; substl=sl ; delay=d ;
untouched = rm uvars vn}
else if
Num.gt_num i max
then
{var=Unsat(cstr, store) ; substl=sl ; delay=d ;
untouched = rm uvars vn}
else (* min < i <= max *)
let tbl1, sl1, d1, da =
if
Num.eq_num i max
then
(*
Whenever, a variable becomes bounded, we:
- add it to the list of substitutions
- remove it from the store.
- check if delayed cstr should be awaked
once this new subst has been applied
*)
let s = make_subst vn (I max) in
let d' =
(List.map
(Constraint.apply_subst_ineq s)
d
)
in
let (d_awake, d_delay) =
List.partition
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
d'
in
(StringMap.remove vn tbl,
s::sl,
d_delay,
d_awake)
else
(
StringMap.add vn (RangeI(i, max)) tbl,
sl,
d,
[]
)
in
(* Applying the waked constraints *)
List.fold_left
(fun acc cstr ->
if debug_store2 then (
print_string "\n <== awake ";
print_string
(Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc bddt (Ineq cstr)
)
{ var=Range(tbl1) ; substl=sl1 ; delay=d1 ;
untouched = rm uvars vn}
da
|
(NInfEqI(i), RangeI(min, max)) ->
if
Num.lt_num i min
then
{ var=Unsat(cstr, store) ; substl=sl ; delay=d;
untouched = rm uvars vn }
else if
Num.ge_num i max
then
{ var=Range(tbl) ; substl=sl ; delay=d;
untouched = rm uvars vn }
else (* min <= i < max *)
let tbl1, sl1, d1, da =
if
Num.eq_num i min
then
let s = make_subst vn (I min) in
let (d_awake, d_delay) =
List.partition
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
(StringMap.remove vn tbl,
s::sl, d_delay, d_awake)
else
(
StringMap.add vn (RangeI(min,i)) tbl, sl,
d,
[]
)
in
(* Applying the waked constraints *)
List.fold_left
(fun acc cstr ->
if debug_store2 then (
print_string "\n <== awake ";
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc bddt (Ineq cstr))
{ var=Range(tbl1) ; substl=sl1 ; delay=d1;
untouched = rm uvars vn }
da
(** **)
| (NSupEqF(f), RangeF(min, max)) ->
if
f <= min
then
{var=Range(tbl) ; substl=sl ; delay=d;
untouched = rm uvars vn }
else if
f > max
then
{var=Unsat(cstr, store) ; substl=sl ; delay=d;
untouched = rm uvars vn }
else (* min < f <= max *)
let tbl1, sl1, d1, da =
if
f = max
then
let s = make_subst vn (F max) in
let (d_awake, d_delay) =
List.partition
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
(StringMap.remove vn tbl,
s::sl, d_delay, d_awake)
else
(
StringMap.add vn (RangeF(f, max)) tbl,
sl,
d,
[]
)
in
(* Applying the waked constraints *)
List.fold_left
(fun acc cstr ->
if debug_store2 then (
print_string "\n <== awake ";
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc bddt (Ineq cstr))
{ var=Range(tbl1) ; substl=sl1 ; delay=d1;
untouched = rm uvars vn }
da
|
(NInfEqF(f), RangeF(min, max)) ->
if
f < min
then
{var=Unsat(cstr, store) ; substl=sl ; delay=d ;
untouched = rm uvars vn }
else if
f >= max
then
{var=Range(tbl) ; substl=sl ; delay=d ;
untouched = rm uvars vn }
else (* min <= f < max *)
let tbl1, sl1, d1, da =
if
f = min
then
let s = make_subst vn (F min) in
let (d_awake, d_delay) =
List.partition
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
(StringMap.remove vn tbl,
s::sl, d_delay, d_awake)
else
(
StringMap.add vn (RangeF(min, f)) tbl,
sl,
d,
[]
)
in
(* Applying the waked constraints *)
List.fold_left
(fun acc cstr ->
if debug_store2 then (
print_string "\n <== awake ";
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc bddt (Ineq cstr))
{ var=Range(tbl1) ; substl=sl1 ; delay=d1;
untouched = rm uvars vn }
da
| (NSupF(f), RangeF(min, max)) ->
if
f < min
then
{var=Range(tbl) ; substl=sl ; delay=d ;
untouched = rm uvars vn }
else if
f >= max
then
{var=Unsat(cstr, store) ; substl=sl ; delay=d ;
untouched = rm uvars vn }
else (* min <= f < max *)
let (tbl1, sl1, d1, da) =
if
(f +. eps) = max
then
let s = make_subst vn (F max) in
let (d_awake, d_delay) =
List.partition
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
(StringMap.remove vn tbl,
s::sl, d_delay, d_awake)
else
(
StringMap.add vn (RangeF(f+.eps, max)) tbl,
sl,
d,
[]
)
in
(* Applying the waked constraints *)
List.fold_left
(fun acc cstr ->
if debug_store2 then (
print_string "\n <== awake ";
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc bddt (Ineq cstr))
{ var=Range(tbl1) ; substl=sl1 ; delay=d1 ;
untouched = rm uvars vn }
da
|
(NInfF(f), RangeF(min, max)) ->
if
f <= min
then
{var=Unsat(cstr, store) ; substl=sl ; delay=d ;
untouched = rm uvars vn }
else if
f > max
then
{var=Range(tbl) ; substl=sl ; delay=d ;
untouched = rm uvars vn }
else (* min < f <= max *)
let tbl1, sl1, d1, da =
if
(f -. eps) = min
then
let s = make_subst vn (F min) in
let (d_awake, d_delay) =
List.partition
(fun ineq ->
Constraint.dimension_ineq ineq <= 1)
(List.map
(Constraint.apply_subst_ineq s)
d)
in
(StringMap.remove vn tbl,
s::sl, d_delay, d_awake)
else
(
StringMap.add vn (RangeF(min, f-.eps)) tbl,
sl,
d,
[]
)
in
(* Applying the waked constraints *)
List.fold_left
(fun acc cstr ->
if debug_store2 then (
print_string "\n <== awake ";
print_string (Constraint.ineq_to_string cstr);
flush stdout
);
add_constraint acc bddt (Ineq cstr)
)
{ var=Range(tbl1) ; substl=sl1 ; delay=d1 ;
untouched = rm uvars vn }
da
| _ -> assert false
)
)
Unsat(cstr, store) ->
if debug_store2 then
print_string (
"\nAdding constraint " ^ (Constraint.to_string cstr) ^
" leads to an empty store.\n") ;