Commit 42c10bc1 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.96 Mon, 30 Sep 2002 16:58:31 +0200 by jahier

Parent-Version:      0.95
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 ...)

Project-Description: Lurette
parent 9f11061a
......@@ -3,20 +3,21 @@
(Created-By-Prcs-Version 1 3 3)
(source/command_line_ima_exe.mli 1082 1021651153 b/34_command_li 1.3)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(bin/Makefile 684 1033397911 c/20_Makefile 1.1)
(source/env_state.ml 20707 1033125605 51_env_state. 1.29)
(source/graph.ml 2563 1027066799 14_graph.ml 1.7)
(bin/Makefile.ima_exe 2013 1027066799 b/41_Makefile.i 1.3)
(test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1)
(source/util.ml 15446 1032510467 35_util.ml 1.26)
(test/time.exp 5580 1033371165 b/48_time.exp 1.6)
(source/solver.ml 28777 1033371165 39_solver.ml 1.29)
(test/time.exp 5580 1033397911 b/48_time.exp 1.7)
(source/solver.ml 28611 1033397911 39_solver.ml 1.30)
(test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1)
(source/command_line.ml 4625 1031053030 b/20_command_li 1.8)
(source/lurette.ml 13388 1032510467 12_lurette.ml 1.52)
(myrules 10516 1033125605 c/14_myrules 1.5)
(myrules 10657 1033397911 c/14_myrules 1.6)
(source/solver.mli 1003 1027092697 38_solver.mli 1.13)
(source/env.mli 2028 1027349504 15_env.mli 1.15)
(test/heater_float.rif.exp 1468 1033371165 b/30_heater_flo 1.8)
(test/heater_float.rif.exp 1459 1033397911 b/30_heater_flo 1.9)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8013 1027349504 16_env.ml 1.29)
(make_lurette 1303 1032940601 27_make_luret 1.16)
......@@ -25,32 +26,32 @@
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/porte.ima 1050 1032789516 b/16_porte.env 1.8)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/constraint.ml 2387 1033125605 c/19_constraint 1.1)
(source/rnumsolver.ml 16394 1033371165 b/27_rnumsolver 1.9)
(source/constraint.ml 995 1033397911 c/19_constraint 1.2)
(source/rnumsolver.ml 16759 1033397911 b/27_rnumsolver 1.10)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/parse_env.mli 1025 1027066799 40_parse_env. 1.9)
(source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5)
(ihm/xlurette/xlurette_glade_interface.ml 28245 1032531447 c/15_xlurette_g 1.3)
(test/passerelle.ima 984 1032789516 b/17_passerelle 1.8)
(source/ima_exe.ml 12101 1032355637 b/32_ima_exe.ml 1.18)
(source/ima_exe.ml 12108 1033397911 b/32_ima_exe.ml 1.19)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/control.ml 4416 1030975996 c/4_control.ml 1.3)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 34425 1033125605 24_generate_l 1.35)
(source/gen_stubs.ml 34420 1033397911 24_generate_l 1.36)
(source/parse_env.ml 24436 1032940601 41_parse_env. 1.28)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
(source/sim2chro.ml 2732 1033125605 b/24_sim2chro.m 1.13)
(source/formula.mli 2813 1033125605 44_formula.ml 1.17)
(source/sim2chro.ml 2721 1033397911 b/24_sim2chro.m 1.14)
(source/formula.mli 2805 1033397911 44_formula.ml 1.18)
(demo/chaudiere/chaudiere.ima 446 1032789516 c/11_chaudiere. 1.5)
(demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1)
(demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1)
(test/time.res 5580 1033371165 b/49_time.res 1.9)
(test/time.res 5580 1033397911 b/49_time.res 1.10)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/command_line.mli 1442 1031053030 b/21_command_li 1.7)
(source/env_state.mli 6734 1033125605 50_env_state. 1.24)
(source/rnumsolver.mli 2246 1033371165 b/26_rnumsolver 1.6)
(source/rnumsolver.mli 2114 1033397911 b/26_rnumsolver 1.7)
(source/ima_exe.mli 447 1016127950 b/31_ima_exe.ml 1.1)
(source/eval.mli 1395 1027066799 48_eval.mli 1.10)
(test/giro/giro.ima 2828 1032789516 c/6_giro.ima 1.2)
......@@ -58,39 +59,39 @@
(README 74 1011881677 10_README 1.2)
(demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 22451 1033125605 17_OcamlMakef 1.41)
(OcamlMakefile 22581 1033397911 17_OcamlMakef 1.42)
(source/command_line_ima_exe.ml 2792 1031732392 b/33_command_li 1.5)
(test/ControleurPorte.rif.exp 4756 1032789516 b/29_Controleur 1.9)
(Makefile.lurette 698 1032940601 b/38_Makefile.l 1.11)
(source/show_env.ml 3603 1030532285 43_show_env.m 1.12)
(source/gne.mli 1093 1033125605 b/36_gne.mli 1.3)
(source/gne.mli 1552 1033397911 b/36_gne.mli 1.4)
(source/automata.ml 15818 1032355637 b/47_automata.m 1.4)
(ihm/xlurette/xlurette_glade_main.ml 16705 1032789516 c/12_xlurette_g 1.6)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(bin/Makefile.lurette_lib 1846 1033125605 c/2_Makefile.l 1.3)
(bin/Makefile.lurette_lib 1976 1033397911 c/2_Makefile.l 1.4)
(bin/Makefile.gen_stubs 472 1030532285 b/42_Makefile.g 1.2)
(test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
(source/show_env.mli 1091 1027066799 42_show_env.m 1.7)
(test/Makefile 105 1031732392 c/0_Makefile 1.4)
(ihm/xlurette/makefile 783 1032355637 c/16_makefile 1.1)
(test/temp_int.ima 686 1032789516 b/50_temp_int.e 1.2)
(source/gne.ml 8168 1033125605 b/37_gne.ml 1.3)
(source/gne.ml 2767 1033397911 b/37_gne.ml 1.4)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(test/temp_float.ima 728 1032789516 b/51_temp_float 1.3)
(test/tram.ima 1079 1032789516 b/15_tram.env 1.8)
(test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1)
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(source/print.mli 1158 1033125605 46_print.mli 1.11)
(source/print.mli 1145 1033397911 46_print.mli 1.12)
(source/lurettetop.ml 24867 1032510467 c/1_lurettetop 1.10)
(ihm/xlurette/xlurette.glade 43485 1032531447 c/13_xlurette.g 1.4)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 850 1033371165 b/28_heater_int 1.7)
(source/formula.ml 5786 1033125605 45_formula.ml 1.20)
(test/heater_int.rif.exp 860 1033397911 b/28_heater_int 1.8)
(source/formula.ml 5765 1033397911 45_formula.ml 1.21)
(source/lurette.mli 448 1016027474 11_lurette.ml 1.12)
(source/constraint.mli 1619 1033125605 c/18_constraint 1.1)
(source/print.ml 5831 1033125605 47_print.ml 1.19)
(source/constraint.mli 830 1033397911 c/18_constraint 1.2)
(source/print.ml 5825 1033397911 47_print.ml 1.20)
(test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
(bin/Makefile.show_ima 1039 1027066799 b/40_Makefile.s 1.4)
(source/control.mli 3202 1030975671 c/3_control.ml 1.2)
......@@ -5,7 +5,7 @@
# For updates see:
# http://www.oefai.at/~markus/ocaml_sources
#
# $Id: OcamlMakefile 1.41 Fri, 27 Sep 2002 13:20:05 +0200 jahier $
# $Id: OcamlMakefile 1.42 Mon, 30 Sep 2002 16:58:31 +0200 jahier $
#
###########################################################################
......@@ -16,6 +16,8 @@ SOURCES_LURETTE_LIB = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/ne.mli $(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
......
lib:
make -f Makefile.lurette_lib OCAMLFLAGS=""
ima:
make -k dc -f Makefile.ima_exe OCAMLFLAGS=""
luc:lucky
lucky:
make -k dc -f Makefile.lucky OCAMLFLAGS=""
ltop:
make -k dc -f Makefile.lurettetop OCAMLFLAGS=""
show:
make -k dc -f Makefile.show_ima OCAMLFLAGS=""
stubs:
make -k dc -f Makefile.gen_stubs OCAMLFLAGS=""
all: lib ima ltop show
clean_all:
make -k clean -f Makefile.ima_exe ; \
make -k clean -f Makefile.lurettetop ; \
make -k clean -f Makefile.lurette_lib ; \
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"
......@@ -32,6 +32,8 @@ SOURCES = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/ne.mli $(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 95)
(Parent-Version lurette 0 94)
(Project-Version lurette 0 96)
(Parent-Version lurette 0 95)
(Version-Log "
Continue to prepare things for the next change (which will try to
handle equalities smartly).
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.
test/test*.res:
fix the expected results as this change adds a random toss
that disturbs the random values.
source/ne.ml,mli:
source/gne.ml,mli:
Make the normal expressions and the guarded normal expression abstract.
source/solver.ml:
source/rnumsolver.ml:
Add code to handle the fact that the negation of a equality
is the disjunction of two inegalities, which can not be added
to store as it is. So we first try with >, and if it fails,
we try with < (or the other way aroung, depending on a fair toss).
also fix a bug in the previous change (forgot to try make test ...)
Also split up the code in Solver.draw_in_bdd depending on the
fact that the current constraint is a boolean, an eq, or an ineg.
source/solver.ml:
split toss_up_one_var into toss_up_one_var and toss_up_one_var_index,
one performing the the toss from a var, the other one from a var index.
")
(New-Version-Log ""
)
(Checkin-Time "Mon, 30 Sep 2002 09:32:45 +0200")
(Checkin-Time "Mon, 30 Sep 2002 16:58:31 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -41,7 +33,7 @@ source/solver.ml:
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.18 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.19 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.5 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.3 644))
......@@ -63,10 +55,10 @@ source/solver.ml:
(source/util.ml (lurette/35_util.ml 1.26 644))
(source/solver.mli (lurette/38_solver.mli 1.13 644))
(source/solver.ml (lurette/39_solver.ml 1.29 644))
(source/solver.ml (lurette/39_solver.ml 1.30 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.6 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.9 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.7 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.10 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.28 644))
......@@ -74,11 +66,11 @@ source/solver.ml:
(source/show_env.mli (lurette/42_show_env.m 1.7 644))
(source/show_env.ml (lurette/43_show_env.m 1.12 644))
(source/formula.mli (lurette/44_formula.ml 1.17 644))
(source/formula.ml (lurette/45_formula.ml 1.20 644))
(source/formula.mli (lurette/44_formula.ml 1.18 644))
(source/formula.ml (lurette/45_formula.ml 1.21 644))
(source/print.mli (lurette/46_print.mli 1.11 644))
(source/print.ml (lurette/47_print.ml 1.19 644))
(source/print.mli (lurette/46_print.mli 1.12 644))
(source/print.ml (lurette/47_print.ml 1.20 644))
(source/eval.mli (lurette/48_eval.mli 1.10 644))
(source/eval.ml (lurette/49_eval.ml 1.13 644))
......@@ -90,32 +82,33 @@ source/solver.ml:
(source/automata.ml (lurette/b/47_automata.m 1.4 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.13 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.14 644))
(source/gne.mli (lurette/b/36_gne.mli 1.3 644))
(source/gne.ml (lurette/b/37_gne.ml 1.3 644))
(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/gen_stubs.ml (lurette/24_generate_l 1.35 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.1 644))
(source/constraint.ml (lurette/c/19_constraint 1.1 644))
(source/constraint.mli (lurette/c/18_constraint 1.2 644))
(source/constraint.ml (lurette/c/19_constraint 1.2 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.16 755))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.41 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.42 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.11 644))
(myrules (lurette/c/14_myrules 1.5 644))
(myrules (lurette/c/14_myrules 1.6 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.3 644))
(bin/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.4 644))
(bin/Makefile (lurette/c/20_Makefile 1.1 644))
;; Documentation
(doc/Interface_draft (lurette/19_Interface_ 1.1 644))
......@@ -132,8 +125,8 @@ 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.6 644))
(test/time.res (lurette/b/49_time.res 1.9 644))
(test/time.exp (lurette/b/48_time.exp 1.7 644))
(test/time.res (lurette/b/49_time.res 1.10 644))
;; Various files used for testing purposes
(test/usager.ima (lurette/b/14_usager.env 1.9 644))
......@@ -145,15 +138,16 @@ source/solver.ml:
(test/ControleurPorte.h (lurette/b/18_Controleur 1.1 644))
(test/ControleurPorte.c (lurette/b/19_Controleur 1.1 644))
(test/ControleurPorte.lus (lurette/c/17_Controleur 1.1 644))
(test/vrai_tram.lus (lurette/b/6_vrai_tram. 1.2 644))
(test/vrai_tram.h (lurette/b/7_vrai_tram. 1.3 644))
(test/vrai_tram.c (lurette/b/8_vrai_tram. 1.3 644))
(test/tram_simple.h (lurette/b/25_tram_simpl 1.1 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.7 644))
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.8 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.9 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.8 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.9 644))
(test/heater_int.lus (lurette/b/43_heater_int 1.1 644))
(test/heater_float.lus (lurette/b/44_heater_flo 1.1 644))
(test/test_gen_stubs.h (lurette/b/45_test_gen_s 1.1 644))
......@@ -186,8 +180,6 @@ source/solver.ml:
;; Files added by populate at Tue, 24 Sep 2002 15:30:27 +0200,
;; to version 0.92(w), by jahier:
(test/ControleurPorte.lus (lurette/c/17_Controleur 1.1 644))
)
(Merge-Parents)
(New-Merge-Parents)
......@@ -202,8 +202,10 @@ release:
$(LURETTE_PATH)/source/command_line_ima_exe.mli $(LURETTE_PATH)/source/command_line_ima_exe.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/ne.mli $(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/rnumsolver.mli $(LURETTE_PATH)/source/rnumsolver.ml \
......
......@@ -9,82 +9,32 @@
*)
(****************************************************************************)
(* exported *)
type num_value = I of int | F of float
type var_value = B of bool | N of num_value
(****************************************************************************)
(* exported *)
module NeMap = struct
include Map.Make(struct type t = string let compare = compare end)
end
(* exported *)
type n_expr = num_value NeMap.t
(* exported *)
let (is_n_expr_a_constant : n_expr -> bool) =
fun ne ->
(NeMap.remove "" ne) = NeMap.empty
(* exported *)
let (neg_nexpr : n_expr -> n_expr) =
fun ne ->
NeMap.map (fun x -> match x with I(i) -> I(-i) | F(f) -> F(-.f)) ne
(****************************************************************************)
(* exported *)
type t =
| Bv of string (** booleans *)
| GZ of n_expr (** expr > 0 *)
| GeqZ of n_expr (** expr >= 0 *)
| EqZ of n_expr (** expr = 0 *)
| GZ of Ne.t (** expr > 0 *)
| GeqZ of Ne.t (** expr >= 0 *)
| EqZ of Ne.t (** expr = 0 *)
(****************************************************************************)
(* Pretty prints formula and expressions *)
(* exported *)
let (num_value_to_string : num_value -> string) =
fun n ->
match n with
I(i) -> string_of_int i
| F(f) -> Util.my_string_of_float f
(* exported *)
let (n_expr_to_string : n_expr -> string) =
fun ne ->
(NeMap.fold
(fun vn v acc ->
if vn = ""
then ((num_value_to_string v) ^ acc)
else (" + " ^ (num_value_to_string v ) ^ "*" ^ vn ^ acc ))
ne
""
)
(* exported *)
let (linear_constraint_to_string : t -> string) =
fun f ->
match f with
| Bv(str) -> str
| GZ(ne) -> ((n_expr_to_string ne) ^ " > 0 ")
| GeqZ(ne) -> ((n_expr_to_string ne) ^ " >= 0 ")
| EqZ(ne) -> ((n_expr_to_string ne) ^ " = 0 ")
| GZ(ne) -> ((Ne.to_string ne) ^ " > 0 ")
| GeqZ(ne) -> ((Ne.to_string ne) ^ " >= 0 ")
| EqZ(ne) -> ((Ne.to_string ne) ^ " = 0 ")
(* exported *)
let print_var_value oc e =
match e with
N(I(i)) -> output_string oc ((string_of_int i) ^ " ")
| N(F(f)) -> output_string oc ((Util.my_string_of_float f) ^ " ")
| B(true) -> output_string oc "t "
| B(false) -> output_string oc "f "
let (dimension : t -> int) =
fun cstr ->
match cstr with
Bv(_) -> 1
| GZ(ne) -> Ne.dimension ne
| GeqZ(ne) -> Ne.dimension ne
| EqZ(ne) -> Ne.dimension ne
......@@ -8,47 +8,19 @@
** Main author: jahier@imag.fr
*)
(** Defines internal representation of constraints used in formula,
namely, linear constraints over booleans, intergers, and floats. *)
(** Internal representation of values. *)
type num_value = I of int | F of float
type var_value = B of bool | N of num_value
(** Map indexed by strings (variable names). *)
module NeMap : Map.S with type key = string
(** 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 n_expr = num_value NeMap.t
(** [is_n_expr_a_constant ne] returns true iff [ne] is a constant. *)
val is_n_expr_a_constant : n_expr -> bool
(** [neg_nexpr ne] returns the opposite of [ne], namely, [-ne]. *)
val neg_nexpr : n_expr -> n_expr
(** Internal representation of constraints used in formula, namely,
linear constraints over booleans, intergers, and floats. *)
(** Normalised linear constraints. *)
type t =
| Bv of string (** booleans *)
| GZ of n_expr (** expr > 0 *)
| GeqZ of n_expr (** expr >= 0 *)
| EqZ of n_expr (** expr = 0 *)
| 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
(** Pretty printing. *)
val num_value_to_string : num_value -> string
val n_expr_to_string : n_expr -> string
val print_var_value : out_channel -> var_value -> unit
val linear_constraint_to_string : t -> string
......@@ -8,7 +8,7 @@
** Main author: jahier@imag.fr
*)
open Constraint
open Value
(****************************************************************************)
......@@ -62,14 +62,14 @@ type arc_info = weight * formula_eps * string
type var_name = string
type vn = var_name
type subst = (var_name * var_value)
type subst = (var_name * Value.t)
type var_type = BoolT | IntT of int * int | FloatT of float * float
type vnt = var_name * var_type
type vne = var_name * (expr * expr)
type vnf = var_name * (formula * formula)
type env_in = (var_name, var_value) Hashtbl.t
type env_in = (var_name, Value.t) Hashtbl.t
type env_out = subst list
type env_loc = subst list
......@@ -179,7 +179,7 @@ let (print_subst_list : subst list -> out_channel -> unit) =
(fun (vn, e) ->
output_string oc vn ;
output_string oc " = \n\t\t";
print_var_value oc e;
Value.print oc e;
output_string oc "\n\t"
)
(Util.sort_list_string_pair sl)
......@@ -190,7 +190,7 @@ let (print_env_in : env_in -> out_channel -> unit) =
(fun vn e ->
output_string oc vn ;
output_string oc " = \n\t\t";
print_var_value oc e;
Value.print oc e;
output_string oc "\n\t"
)
tbl
......@@ -198,14 +198,14 @@ let (print_env_in : env_in -> out_channel -> unit) =
(****************************************************************************)
(* exported *)
let (expr_to_var_value: expr -> var_value) = function
let (expr_to_var_value: expr -> Value.t) = function
Ival(i) -> N(I(i))
| Fval(f) -> N(F(f))
| _ -> assert false
(* exported *)
let (formula_to_var_value: formula -> var_value) = function
let (formula_to_var_value: formula -> Value.t) = function
True -> B(true)
| False -> B(false)
| _ -> assert false
......@@ -66,14 +66,14 @@ type var_name = string
type vn = var_name
type subst = (var_name * var_value)
type subst = (var_name * Value.t)
type var_type = BoolT | IntT of int * int | FloatT of float * float
type vnt = var_name * var_type
type vne = var_name * (expr * expr)
type vnf = var_name * (formula * formula)
type env_in = (var_name, var_value) Hashtbl.t
type env_in = (var_name, Value.t) Hashtbl.t
type env_out = subst list
type env_loc = subst list
......@@ -83,11 +83,11 @@ val support : formula -> vn list
(** [expr_to_var_value e] translate the expression [e] into a value
if possible, fails otherwise *)
val expr_to_var_value: expr -> var_value
val expr_to_var_value: expr -> Value.t
(** [formula_to_var_value f] translates the formula [f] into values
if possible, fails otherwise. *)
val formula_to_var_value: formula -> var_value
val formula_to_var_value: formula -> Value.t
(****************************************************************************)
......
......@@ -627,7 +627,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
put "open Format\n";
put "open Hashtbl\n";
put "open Formula\n\n";
put "open Constraint\n\n";
put "open Value\n\n";
(*
** Defines the type of sut inputs and outputs.
......
......@@ -8,246 +8,26 @@
** Main author: jahier@imag.fr
*)
open Constraint
(* exported *)
module GneMap = struct
include Map.Make(struct type t = n_expr let compare = compare end)
module NeMap = struct
include Map.Make(struct type t = Ne.t let compare = compare end)
end
(* exported *)
type t = (Bdd.t * bool) GneMap.t
(****************************************************************************)
(****************************************************************************)