Commit ccb8b62b authored by erwan's avatar erwan

Fix: variables contraint to a value at declaration were buggy (close #2)

cf example/Bug/freevar.lut node ko
parent e53b6f05
Pipeline #26584 passed with stages
in 9 minutes and 43 seconds
......@@ -2,3 +2,4 @@
node ko () returns (b: int [0; 0]; a: int) = a = b
node ok () returns (a: int [0; 0]; b: int) = a = b
......@@ -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,64 +144,58 @@ 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";
| _ -> 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)
| 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;
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
let tbl,sl = List.fold_left (add_one_var) (StringMap.empty,[]) var_l in
{
var = Range(tbl) ;
substl = [];
substl = sl;
delay = [];
untouched = var_l
}
......@@ -646,12 +640,12 @@ let rec (add_constraint : t -> Formula_to_bdd.t -> Constraint.t -> t) =
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
......@@ -717,12 +711,12 @@ let rec (add_constraint : t -> Formula_to_bdd.t -> Constraint.t -> t) =
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
*)
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
......@@ -1045,17 +1039,17 @@ and (add_eq_to_store : t -> Formula_to_bdd.t -> Ne.t -> t) =
| Ne.Split(vn, coef, ne_rest) ->
(*
if ne = "a0 + a1x1 + a2x2 + ...", then
- vn,coef = ("x1", a1)
if ne = "a0 + a1x1 + a2x2 + ...", then
- vn,coef = ("x1", a1)
(or any other indexes except the constant one !!!),
- and ne_rest = "a0 + a2x2 + ..."
*)
*)
let coef_neg = Value.neg coef in
let store1 =
(*
Propagates the bounds of vn (min and max) to what
(-a0).vn will be substituted to.
*)
*)
match store.var with
Unsat(_,_) -> assert false
| Range(tbl) ->
......
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