Skip to content

Commit

Permalink
Merge pull request #1 from OCamlPro-Iguernlala/bugfix_with_inconsiste…
Browse files Browse the repository at this point in the history 
…nt_bounds

Bugfix with inconsistent bounds
  • Loading branch information
Mohamed Iguernlala authored Aug 24, 2016
2 parents f7447da + 69125af commit 6071026
Show file tree
Hide file tree
Showing 13 changed files with 616 additions and 101 deletions.
33 changes: 31 additions & 2 deletions Makefile.in
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,8 +149,8 @@ uninstall:
#######

clean:
@for dd in src; do \
rm -f $$dd/*.cm* $$dd/*.a $$dd/*.o $$dd/*~ $$dd/*.annot $$dd/*.owz $(GENERATED);\
@for dd in . src tests; do \
rm -f $$dd/*.cm* $$dd/*.a $$dd/*.o $$dd/*~ $$dd/*.annot $$dd/*.owz $(GENERATED) *.byte *.opt;\
done
@rm -rf META

Expand Down Expand Up @@ -197,3 +197,32 @@ opam-deps:
repin:
opam remove ocplib-simplex
opam pin add . --y


local-tests: all
## minimal example with solve: byte and opt >> lib is local
$(OCAMLC) -o standalone_minimal_local.byte -I src -I tests ocplibSimplex.cma nums.cma tests/standalone_minimal.ml
./standalone_minimal_local.byte 2> /dev/null
$(OCAMLOPT) -o standalone_minimal_local.opt -I src -I tests ocplibSimplex.cmxa nums.cmxa tests/standalone_minimal.ml
./standalone_minimal_local.opt 2> /dev/null

## minimal example with maximization: byte and opt >> lib is local
$(OCAMLC) -o standalone_minimal_maximization_local.byte -I src -I tests ocplibSimplex.cma nums.cma tests/standalone_minimal_maximization.ml
./standalone_minimal_maximization_local.byte 2> /dev/null
$(OCAMLOPT) -o standalone_minimal_maximization_local.opt -I src -I tests ocplibSimplex.cmxa nums.cmxa tests/standalone_minimal_maximization.ml
./standalone_minimal_maximization_local.opt 2> /dev/null

opam-installed-tests: repin
## minimal example with solve: byte and opt >> lib is pinned with OPAM
$(OCAMLC) -o standalone_minimal_opam.byte -I `ocamlfind query ocplib-simplex` -I tests ocplibSimplex.cma nums.cma tests/standalone_minimal.ml
./standalone_minimal_opam.byte 2> /dev/null
$(OCAMLOPT) -o standalone_minimal_opam.opt -I `ocamlfind query ocplib-simplex` -I tests ocplibSimplex.cmxa nums.cmxa tests/standalone_minimal.ml
./standalone_minimal_opam.opt 2> /dev/null

## minimal example with maximization: byte and opt >> lib is pinned with OPAM
$(OCAMLC) -o standalone_minimal_maximization_opam.byte -I `ocamlfind query ocplib-simplex` -I tests ocplibSimplex.cma nums.cma tests/standalone_minimal_maximization.ml
./standalone_minimal_maximization_opam.byte 2> /dev/null
$(OCAMLOPT) -o standalone_minimal_maximization_opam.opt -I `ocamlfind query ocplib-simplex` -I tests ocplibSimplex.cmxa nums.cmxa tests/standalone_minimal_maximization.ml
./standalone_minimal_maximization_opam.opt 2> /dev/null

tests: local-tests opam-installed-tests
36 changes: 20 additions & 16 deletions src/assertBounds.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -65,12 +65,16 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct

(* *)

let new_status_non_basic x stt ({mini; maxi; value; _} as info) =
assert (not (violates_min_bound value mini));
assert (not (violates_max_bound value maxi));
let new_status_non_basic x stt fixme ({mini; maxi; value; _} as info) =
match stt with
| UNSAT _ -> stt
| SAT | UNK -> if consistent_bounds info then stt else UNSAT x
| UNSAT _ -> stt, fixme
| SAT | UNK when consistent_bounds info ->
assert (not (violates_min_bound value mini));
assert (not (violates_max_bound value maxi));
assert (stt != SAT || fixme == SX.empty);
stt, fixme
| SAT | UNK ->
UNSAT x, SX.empty

let adapt_values_of_basic_vars env _old _new x use =
let {basic; _} = env in
Expand Down Expand Up @@ -98,27 +102,27 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
let info = set_max_bound info maxi max_ex in
let old_val = info.value in
let info, changed = ajust_value_of_non_basic info in
let status = new_status_non_basic x env.status info in
let status, fixme = new_status_non_basic x env.status env.fixme info in
let env =
{env with
non_basic = MX.add x (info, use) env.non_basic; status}
non_basic = MX.add x (info, use) env.non_basic; status; fixme}
in
if not changed then env
else adapt_values_of_basic_vars env old_val info.value x use


(* exported function: check_invariants called before and after *)
let var env x mini ex_min maxi ex_max =
debug "[entry of assert_var]" env Result.get;
check_invariants env Result.get;
debug "[entry of assert_var]" env (Result.get None);
check_invariants env (Result.get None);
let env =
if MX.mem x env.basic then
assert_basic_var env x mini ex_min maxi ex_max
else
assert_non_basic_var env x mini ex_min maxi ex_max
in
debug "[exit of assert_var]" env Result.get;
check_invariants env Result.get;
debug "[exit of assert_var]" env (Result.get None);
check_invariants env (Result.get None);
env

let register_slake slk p env =
Expand Down Expand Up @@ -185,8 +189,8 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct

(* exported function: check_invariants called before and after *)
let poly env p slk mini min_ex maxi max_ex =
debug "[entry of assert_poly]" env Result.get;
check_invariants env Result.get;
debug "[entry of assert_poly]" env (Result.get None);
check_invariants env (Result.get None);
assert (P.is_polynomial p);
let env, is_fresh = register_slake slk p env in
let info, is_basic, env =
Expand Down Expand Up @@ -232,11 +236,11 @@ module Make(Core : CoreSig.SIG) : SIG with module Core = Core = struct
new_status_basic env.status env.fixme slk info
(consistent_bounds info)
else
new_status_non_basic slk env.status info, env.fixme
new_status_non_basic slk env.status env.fixme info
in
let env = {env with status; fixme } in
debug "[exit of assert_poly]" env Result.get;
check_invariants env Result.get;
debug "[exit of assert_poly]" env (Result.get None);
check_invariants env (Result.get None);
env


Expand Down
Loading

0 comments on commit 6071026

Please sign in to comment.