Commit 5d9a1618 authored by Erwan Jahier's avatar Erwan Jahier

lurette 0.97 Fri, 04 Oct 2002 11:30:11 +0200 by jahier

Parent-Version:      0.96
Version-Log:

Handling equalities smartlier.    .

Project-Description: Lurette
parent 42c10bc1
This diff is collapsed.
......@@ -3,6 +3,17 @@
lib:
make -f Makefile.lurette_lib OCAMLFLAGS=""
lib_debug:
make -f Makefile.lurette_lib dc OCAMLFLAGS=""
lib_nc:
make nc -f Makefile.lurette_lib OCAMLFLAGS="-noassert -unsafe"
lib_clean:
make -f Makefile.lurette_lib clean
ima:
make -k dc -f Makefile.ima_exe OCAMLFLAGS=""
......@@ -35,8 +46,6 @@ clean_all:
make -k clean -f Makefile.show_ima
lib_nc:
make nc -f Makefile.lurette_lib OCAMLFLAGS="-noassert -unsafe"
ima_nc:
make -k nc -f Makefile.ima_exe OCAMLFLAGS="-noassert -unsafe"
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 96)
(Parent-Version lurette 0 95)
(Project-Version lurette 0 97)
(Parent-Version lurette 0 96)
(Version-Log "
source/ne.ml,mli:
source/value.ml,mli:
(new files) put everything that is related to normal expressions
and values in thoses 2 new modules.
source/ne.ml,mli:
source/gne.ml,mli:
Make the normal expressions and the guarded normal expression abstract.
source/solver.ml:
also fix a bug in the previous change (forgot to try make test ...)
Handling equalities smartlier. .
")
(New-Version-Log ""
)
(Checkin-Time "Mon, 30 Sep 2002 16:58:31 +0200")
(Checkin-Time "Fri, 04 Oct 2002 11:30:11 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -40,7 +27,7 @@ source/solver.ml:
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.52 644))
(source/lurette.ml (lurette/12_lurette.ml 1.53 644))
(source/command_line.ml (lurette/b/20_command_li 1.8 644))
(source/command_line.mli (lurette/b/21_command_li 1.7 644))
......@@ -52,16 +39,16 @@ source/solver.ml:
(source/env.mli (lurette/15_env.mli 1.15 644))
(source/env.ml (lurette/16_env.ml 1.29 644))
(source/util.ml (lurette/35_util.ml 1.26 644))
(source/util.ml (lurette/35_util.ml 1.27 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.30 644))
(source/solver.ml (lurette/39_solver.ml 1.31 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.7 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.10 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.8 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.11 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.28 644))
(source/parse_env.ml (lurette/41_parse_env. 1.29 644))
(source/show_env.mli (lurette/42_show_env.m 1.7 644))
(source/show_env.ml (lurette/43_show_env.m 1.12 644))
......@@ -70,7 +57,7 @@ source/solver.ml:
(source/formula.ml (lurette/45_formula.ml 1.21 644))
(source/print.mli (lurette/46_print.mli 1.12 644))
(source/print.ml (lurette/47_print.ml 1.20 644))
(source/print.ml (lurette/47_print.ml 1.21 644))
(source/eval.mli (lurette/48_eval.mli 1.10 644))
(source/eval.ml (lurette/49_eval.ml 1.13 644))
......@@ -79,7 +66,7 @@ source/solver.ml:
(source/env_state.ml (lurette/51_env_state. 1.29 644))
(source/automata.mli (lurette/b/46_automata.m 1.2 644))
(source/automata.ml (lurette/b/47_automata.m 1.4 644))
(source/automata.ml (lurette/b/47_automata.m 1.5 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.14 644))
......@@ -87,14 +74,20 @@ source/solver.ml:
(source/gne.mli (lurette/b/36_gne.mli 1.4 644))
(source/gne.ml (lurette/b/37_gne.ml 1.4 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.10 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.11 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.36 644))
(source/control.mli (lurette/c/3_control.ml 1.2 644))
(source/control.ml (lurette/c/4_control.ml 1.3 644))
(source/constraint.mli (lurette/c/18_constraint 1.2 644))
(source/constraint.ml (lurette/c/19_constraint 1.2 644))
(source/constraint.mli (lurette/c/18_constraint 1.3 644))
(source/constraint.ml (lurette/c/19_constraint 1.3 644))
(source/ne.ml (lurette/c/21_ne.ml 1.1 644))
(source/ne.mli (lurette/c/22_ne.mli 1.1 644))
(source/value.ml (lurette/c/23_value.ml 1.1 644))
(source/value.mli (lurette/c/24_value.mli 1.1 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.16 755))
......@@ -102,13 +95,13 @@ source/solver.ml:
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.42 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.11 644))
(myrules (lurette/c/14_myrules 1.6 644))
(myrules (lurette/c/14_myrules 1.7 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
(bin/Makefile.ima_exe (lurette/b/41_Makefile.i 1.3 644))
(bin/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.2 644))
(bin/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.4 644))
(bin/Makefile (lurette/c/20_Makefile 1.1 644))
(bin/Makefile (lurette/c/20_Makefile 1.2 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -125,15 +118,15 @@ source/solver.ml:
(lurette.depfull.dot (lurette/b/5_lurette.de 1.2 644))
(TAGS (lurette/21_TAGS 1.6 644))
(test/time.exp (lurette/b/48_time.exp 1.7 644))
(test/time.res (lurette/b/49_time.res 1.10 644))
(test/time.exp (lurette/b/48_time.exp 1.8 644))
(test/time.res (lurette/b/49_time.res 1.11 644))
;; Various files used for testing purposes
(test/usager.ima (lurette/b/14_usager.env 1.9 644))
(test/tram.ima (lurette/b/15_tram.env 1.8 644))
(test/porte.ima (lurette/b/16_porte.env 1.8 644))
(test/passerelle.ima (lurette/b/17_passerelle 1.8 644))
(test/temp_int.ima (lurette/b/50_temp_int.e 1.2 644))
(test/temp_int.ima (lurette/b/50_temp_int.e 1.3 644))
(test/temp_float.ima (lurette/b/51_temp_float 1.3 644))
(test/ControleurPorte.h (lurette/b/18_Controleur 1.1 644))
......@@ -165,7 +158,7 @@ source/solver.ml:
;; to version 0.83(w), by jahier:
(test/giro/allocator.lus (lurette/c/5_allocator. 1.1 644))
(test/giro/giro.ima (lurette/c/6_giro.ima 1.2 644))
(test/giro/giro.ima (lurette/c/6_giro.ima 1.3 644))
(test/giro/onlyroll.lus (lurette/c/7_onlyroll.l 1.1 644))
;; Files added by populate at Wed, 04 Sep 2002 09:47:29 +0200,
......@@ -176,10 +169,6 @@ source/solver.ml:
(demo/chaudiere/buggy_chaudiere_ctrl.lus (lurette/c/10_buggy_chau 1.1 644))
(demo/chaudiere/chaudiere.ima (lurette/c/11_chaudiere. 1.5 644))
;; Files added by populate at Tue, 24 Sep 2002 15:30:27 +0200,
;; to version 0.92(w), by jahier:
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -4,13 +4,17 @@ ifndef OCAMLDOT
OCAMLDOT := ocamldot
endif
ifndef OTAGS
OTAGS := otags
endif
export OCAMLDOT
# Generates emacs tags
tags:
$(OTAGS) -v $(SOURCES) ; cp TAGS ../source
$(OTAGS) -v $(ALL_SOURCES) ; cp TAGS ../source
# Generates the modules dependency graph using ocamldot
# (results in lurette.dep.ps and lurette.depfull.ps).
......@@ -122,7 +126,7 @@ heater_make:
$(LURETTE_PATH)/make_lurette heater_int
heater:
lurettetop -l 30 -go --sut heater_int temp_int
lurettetop -l 30 -go --sut heater_int temp_int_eq
heaterf:
......
......@@ -490,7 +490,6 @@ let rec (choose_n_formula_acc: int -> t -> accT -> accT) =
choose_n_formula_acc (n-1) a ((ntl, f, st)::nt_f_st_l0)
with Not_found ->
let nodes_str = intset_to_string (fst a) in
Env_state.dump_env_state_stat stderr;
if (IntSet.cardinal (fst a)) = 1
then failwith ("*** No (more) transition(s) can be made from node "
^ nodes_str ^ ". \n")
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -18,17 +18,6 @@ type t =
(* exported *)
let (linear_constraint_to_string : t -> string) =
fun f ->
match f with
| Bv(str) -> str
| GZ(ne) -> ((Ne.to_string ne) ^ " > 0 ")
| GeqZ(ne) -> ((Ne.to_string ne) ^ " >= 0 ")
| EqZ(ne) -> ((Ne.to_string ne) ^ " = 0 ")
(* exported *)
let (dimension : t -> int) =
fun cstr ->
......@@ -38,3 +27,51 @@ let (dimension : t -> int) =
| GeqZ(ne) -> Ne.dimension ne
| EqZ(ne) -> Ne.dimension ne
(* exported *)
let (neg_ineq : t -> t) =
fun cstr ->
match cstr with
Bv(_) -> assert false
| GZ(ne) -> GeqZ(Ne.neg_nexpr ne)
| GeqZ(ne) -> GZ(Ne.neg_nexpr ne)
| EqZ(ne) -> assert false
(* exported *)
let (opp_ineq : t -> t) =
fun cstr ->
match cstr with
Bv(_) -> assert false
| GZ(ne) -> GZ(Ne.neg_nexpr ne)
| GeqZ(ne) -> GeqZ(Ne.neg_nexpr ne)
| EqZ(ne) -> EqZ(Ne.neg_nexpr ne)
(* exported *)
let (apply_subst : Ne.subst -> t -> t) =
fun s cstr ->
match cstr with
Bv(_) -> cstr
| GZ(ne) -> GZ(Ne.apply_subst ne s)
| GeqZ(ne) -> GeqZ(Ne.apply_subst ne s)
| EqZ(ne) -> EqZ(Ne.apply_subst ne s)
(* exported *)
let (apply_substl : Ne.subst list -> t -> t) =
fun s cstr ->
match cstr with
Bv(_) -> cstr
| GZ(ne) -> GZ(Ne.apply_substl s ne)
| GeqZ(ne) -> GeqZ(Ne.apply_substl s ne)
| EqZ(ne) -> EqZ(Ne.apply_substl s ne)
(* exported *)
let (to_string : t -> string) =
fun f ->
match f with
| Bv(str) -> str
| GZ(ne) -> ((Ne.to_string ne) ^ " > 0 ")
| GeqZ(ne) -> ((Ne.to_string ne) ^ " >= 0 ")
| EqZ(ne) -> ((Ne.to_string ne) ^ " = 0 ")
(*-----------------------------------------------------------------------
** Copyright (C) 2001 - Verimag.
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
......@@ -14,13 +14,24 @@
(** Normalised linear constraints. *)
type t =
| Bv of string (** booleans *)
| GZ of Ne.t (** expr > 0 *)
| GeqZ of Ne.t (** expr >= 0 *)
| EqZ of Ne.t (** expr = 0 *)
| Bv of string (** boolean variable *)
| GZ of Ne.t (** expr > 0 *)
| GeqZ of Ne.t (** expr >= 0 *)
| EqZ of Ne.t (** expr = 0 *)
(** Returns the number of variables involved in the constraint *)
val dimension : t -> int
(** [apply_subst cstr s] applies [s] to [cstr]. Note that the result could
have been multiplied by a constant. *)
val apply_subst : Ne.subst -> t -> t
val apply_substl : Ne.subst list -> t -> t
(** [neg_ineq cstr] returns the negation of an inequality constraint. *)
val neg_ineq : t -> t
(** [neg_ineq cstr] returns [cstr] where its Ne.t is replaces by its opposite. *)
val opp_ineq : t -> t
(** Pretty printing. *)
val linear_constraint_to_string : t -> string
val to_string : t -> string
......@@ -132,10 +132,16 @@ let rec (main : unit -> 'a) =
else () ;
res
with
Failure(errmsg) -> output_string stderr errmsg
Failure(errmsg) ->
if options.verbose then Env_state.dump_env_state_stat stdout;
print_string errmsg;
flush stdout;
exit 2
| e ->
if options.verbose then Env_state.dump_env_state_stat stderr;
raise e
if options.verbose then Env_state.dump_env_state_stat stdout;
print_string (Printexc.to_string e);
flush stdout;
exit 2
and
(get_lurette_options: int -> int) =
......@@ -147,17 +153,17 @@ and
Step -> options.step_by_step <- true ; (n+1)
| NoStep -> options.step_by_step <- false ; (n+1)
| DisplayLocalVar -> options.display_local_var <- true ; (n+1)
| NoDisplayLocalVar -> options.display_local_var <- false ; (n+1)
| DisplayLocalVar -> options.display_local_var <- true ; (n+1)
| NoDisplayLocalVar -> options.display_local_var <- false ; (n+1)
| Sim2chro -> options.display_sim2chro <- true ; (n+1)
| NoSim2chro -> options.display_sim2chro <- false ; (n+1)
| NoSim2chro -> options.display_sim2chro <- false ; (n+1)
| NoOracle -> options.oracle <- false ; (n+1)
| NoOracle -> options.oracle <- false ; (n+1)
| Verbose -> options.verbose <- true ; (n+1)
| Edges -> Env_state.set_draw_mode Env_state.Edges ; (n+1)
| Verteces -> Env_state.set_draw_mode Env_state.Verteces ; (n+1)
| Help -> options.help <- true ; (n+1)
| Edges -> Env_state.set_draw_mode Env_state.Edges ; (n+1)
| Verteces -> Env_state.set_draw_mode Env_state.Verteces ; (n+1)
| Help -> options.help <- true ; (n+1)
| Output ->
let str = (Sys.argv.(n+1)) in
options.output <- str ;
......
......@@ -680,6 +680,7 @@ let rec (main_loop : string -> string -> string -> int -> unit) =
result <> 0
then
output_string stdout "\n*** Can not run lurette, sorry.\n"
else
(output_string stderr " ... lurette ok.\n"; flush stderr)
)
......@@ -689,7 +690,9 @@ let rec (main_loop : string -> string -> string -> int -> unit) =
Unix.chdir lurette_tmp_dir;
true
| Show -> let _ = Sys.command ("show_ima " ^ user_dir ^ "/" ^ flag.env) in true
| Show ->
let _ = Sys.command ("show_ima " ^ user_dir ^ "/" ^ flag.env) in
true
| CallSim2chro ->
let sim_cmd = "sim2chro -ecran -in " ^ user_dir ^ "/" ^ flag.output ^
" > /dev/null &\n" in
......@@ -835,7 +838,7 @@ let _ =
(run lurette_tmp_dir) <> 0
then
(
print_string "Can not run lurette, sorry\n";
print_string "Can not create dir in /tmp/\n";
exit 1
);
rm_dir lurette_tmp_dir;
......
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: ne.ml
** Main author: jahier@imag.fr
*)
open Value
module StringMap = struct
include Map.Make(struct type t = string let compare = compare end)
end
(* exported *)
(** Normal expressions.
Keys are var names, and the content is the coefficient of the
monomial. By convention, "" maps the constant value. For instance,
[("a" -> I(3) ; "b" -> I(-2) ; "" -> I(11))] represents the
expression [3*a - 2*b + 11].
*)
type t = Value.num StringMap.t
type subst = (string * Value.num) * t
(****************************************************************************)
(* exported *)
let (is_a_constant : t -> bool) =
fun ne ->
(StringMap.remove "" ne) = StringMap.empty
(****************************************************************************)
let (add: t -> t -> t) =
fun ne1 ne2 ->
( StringMap.fold
(fun vn1 val1 acc ->
try
let val2 = StringMap.find vn1 acc in
let valr = (add_num val1 val2) in
if ((not (num_eq_zero valr)) || (vn1 = "") )
then StringMap.add vn1 valr acc
else StringMap.remove vn1 acc
with Not_found ->
StringMap.add vn1 val1 acc
)
ne1
ne2
)
let _ = assert (
let ne1 = StringMap.add "" (I(1)) (StringMap.add "toto" (I(2)) StringMap.empty)
and ne2 = StringMap.add "" (I(2)) (StringMap.add "toto" (I(-3)) StringMap.empty)
and ne_res = StringMap.add "" (I(3)) (StringMap.add "toto" (I(-1)) StringMap.empty)
in
let ne_cal = add ne1 ne2 in
((StringMap.find "toto" ne_res) = (StringMap.find "toto" ne_cal))
&&
((StringMap.find "" ne_res) = (StringMap.find "" ne_cal))
)
(****************************************************************************)
let (diff: t -> t -> t) =
fun ne1 ne2 ->
( StringMap.fold
(fun vn2 val2 acc ->
try
let val1 = StringMap.find vn2 acc in
let valr = (diff_num val1 val2) in
if (not (num_eq_zero valr) || vn2 = "" )
then StringMap.add vn2 valr acc
else StringMap.remove vn2 acc
with Not_found ->
let minus_val2 =
match val2 with
I(i) -> I(-i)
| F(f) -> F(-. f)
in
StringMap.add vn2 minus_val2 acc
)
ne2
ne1
)
let _ = assert (
let ne1 = StringMap.add "" (I(1)) (StringMap.add "toto" (I(2)) StringMap.empty)
and ne2 = StringMap.add "" (I(2)) (StringMap.add "titi" (I(3))
(StringMap.add "toto" (I(3)) StringMap.empty))
and ne_res = StringMap.add "" (I(-1)) (StringMap.add "toto" (I(-1))
(StringMap.add "titi" (I(3)) StringMap.empty))
in
let ne_cal = diff ne1 ne2
in
((StringMap.find "toto" ne_res) = (StringMap.find "toto" ne_cal))
&&
((StringMap.find "" ne_res) = (StringMap.find "" ne_cal))
)
(****************************************************************************)
let (mult: t -> t -> t) =
fun ne1 ne2 ->
if is_a_constant ne1
then
let coeff = StringMap.find "" ne1 in
if num_eq_zero coeff
then ne1
else
( StringMap.fold
(fun vn value acc ->
StringMap.add vn (mult_num coeff value) acc
)
ne2
StringMap.empty
)
else if is_a_constant ne2
then
let coeff = StringMap.find "" ne2 in
if num_eq_zero coeff
then ne2
else
( StringMap.fold
(fun vn value acc ->
StringMap.add vn (mult_num coeff value) acc
)
ne1
StringMap.empty
)
else
failwith "*** Cannot solve non-linear constraints, sorry. \n"
let _ = assert (
let ne1 = StringMap.add "" (I(1)) (StringMap.add "toto" (I(2)) StringMap.empty) in
let ne2 = StringMap.add "" (I(2)) StringMap.empty in
let ne_res = StringMap.add "" (I(2)) (StringMap.add "toto" (I(4)) StringMap.empty) in
let ne_cal = mult ne1 ne2 in
((StringMap.find "toto" ne_res) = (StringMap.find "toto" ne_cal))
&&
((StringMap.find "" ne_res) = (StringMap.find "" ne_cal))
)
(****************************************************************************)
let (quot: t -> t -> t) =
fun ne1 ne2 ->
if is_a_constant ne2
then
let coeff = StringMap.find "" ne2 in
( StringMap.fold
(fun vn value acc ->
let valr = (quot_num value coeff) in
if ((num_eq_zero valr) && (vn <> ""))
then acc
else StringMap.add vn valr acc
)
ne1
StringMap.empty
)
else
failwith "*** Cannot solve non-linear constraints, sorry. \n"
let _ = assert (
let ne1 = StringMap.add "" (I(1)) (StringMap.add "toto" (I(2)) StringMap.empty) in
let ne2 = StringMap.add "" (I(2)) StringMap.empty in
let ne_res = StringMap.add "" (I(0)) (StringMap.add "toto" (I(1)) StringMap.empty) in
let ne_cal = quot ne1 ne2 in
((StringMap.find "toto" ne_res) = (StringMap.find "toto" ne_cal))
&&
((StringMap.find "" ne_res) = (StringMap.find "" ne_cal))
)
(****************************************************************************)
let (modulo: t -> t -> t) =
fun ne1 ne2 ->
if is_a_constant ne2
then
let coeff = StringMap.find "" ne2 in
( StringMap.fold
(fun vn value acc ->
let valr = (modulo_num value coeff) in
if ((num_eq_zero valr) && (vn <> ""))
then acc
else StringMap.add vn (modulo_num value coeff) acc
)
ne1
StringMap.empty
)
else
failwith "*** Cannot solve non-linear constraints, sorry. \n"
let _ = assert (
let ne1 = StringMap.add "" (I(1)) (StringMap.add "toto" (I(2)) StringMap.empty) in
let ne2 = StringMap.add "" (I(2)) StringMap.empty in
let ne_res = StringMap.add "" (I(1)) (StringMap.add "toto" (I(0)) StringMap.empty) in
let ne_cal = modulo ne1 ne2 in
((StringMap.find "" ne_res) = (StringMap.find "" ne_cal))
)
(****************************************************************************)
(* exported *)
let (fold : (string -> Value.num -> 'acc -> 'acc) -> t -> 'acc -> 'acc) =
fun f ne acc0 ->
StringMap.fold f ne acc0
(* exported *)
let (make : string -> Value.num -> t) =
fun vn nval ->
(StringMap.add vn nval StringMap.empty)
(* exported *)
let (find : string -> t -> Value.num) =
fun vn ne ->
StringMap.find vn ne
(****************************************************************************)
(* exported *)
let (neg_nexpr : t -> t) =
fun ne ->
StringMap.map (fun x -> match x with I(i) -> I(-i) | F(f) -> F(-.f)) ne
(* exported *)
let (split : t -> (string * Value.num) option * t) =
fun ne ->
let f = fun var num_val acc ->
match acc with
None, ne -> Some(var, num_val), ne
| Some(v, nv), ne -> Some(v, nv), (StringMap.add var num_val ne)
in
StringMap.fold f ne (None, StringMap.empty)
(* exported *)
let (dimension : t -> int) =
fun ne ->
StringMap.fold (fun vn _ cpt -> if vn = "" then cpt else cpt+1) ne 0
(* exported *)
let (nexpr_add : (Value.num * string) -> t -> t) =
fun (nval, vn) ne2 ->
StringMap.add vn nval ne2
(* exported *)
let (apply_subst : t -> subst -> t) =
fun ne2 ((vn, b), ne1) ->
try
let a = StringMap.find vn ne2 in
let new_ne1 =
StringMap.map
(fun x -> Value.mult_num x a)
ne1
in
let new_ne2 =
StringMap.map
(fun x -> Value.mult_num x b)
(StringMap.remove vn ne2)
in
add new_ne1 new_ne2
with
Not_found -> ne2
(* exported *)
let (apply_substl : subst list -> t -> t) =
fun sl ne ->
List.fold_left (apply_subst) ne sl
(* exported *)
let (apply_simple_subst : t -> string * Value.num -> t) =
fun ne (vn, v) ->
try
let a = StringMap.find vn ne in
let b = StringMap.find "" ne in
let ne2 = StringMap.remove vn ne in
StringMap.add "" ((Value.add_num b (Value.mult_num v a))) ne2
with
Not_found -> ne
(* exported *)
exception Not_triangular
(* exported *)
let rec (resolve_triangular_system :((string * Value.num) * t) list ->
(string * Value.num) list) =
fun sl ->
match sl with
[] -> []
| ((vn, v), ne)::tail ->
let cst = StringMap.find "" ne
and ne2 = StringMap.remove "" ne in
if
ne2 <> StringMap.empty
then
raise Not_triangular
else
let s = (vn, Value.quot_num cst v) in
let new_tail =
List.map
(fun (x, ne) -> x, apply_simple_subst ne s)