From aef52d9cb67a99600fc09c00e3a2644958d7c5c0 Mon Sep 17 00:00:00 2001 From: Erwan Jahier Date: Wed, 17 Mar 2010 15:35:14 +0100 Subject: [PATCH] lurette 0.116 Wed, 13 Nov 2002 13:56:29 +0100 by jahier Parent-Version: 0.115 Version-Log: source/solver.ml: Give a better error message when users do not initialize pre vars. source/parse_env.ml: source/formula.ml: source/prevar.ml/mli: (new files) Put here everything that handles the internal representation of pre var names. Pretty print internal pre var names. Project-Description: Lurette --- .lurette.prcs_aux | 34 +- OcamlMakefile | 3 +- lurette.prj | 58 ++- source/Makefile.lucky | 7 +- source/Makefile.lurette_lib | 6 +- source/Makefile.lurettetop | 5 +- source/Makefile.show_luc | 3 +- source/formula.ml | 15 +- source/formula.mli | 1 + source/ne.ml | 4 +- source/parse_env.ml | 6 +- source/prevar.ml | 33 ++ source/prevar.mli | 21 + source/rnumsolver.ml | 750 ++++++++++++++++++------------------ source/show_env.ml | 6 +- source/solver.ml | 124 ++++-- test/time.exp | 80 ++-- test/time.res | 80 ++-- user-rules | 15 +- 19 files changed, 696 insertions(+), 555 deletions(-) create mode 100644 source/prevar.ml create mode 100644 source/prevar.mli diff --git a/.lurette.prcs_aux b/.lurette.prcs_aux index 04cda1c..eb3f067 100644 --- a/.lurette.prcs_aux +++ b/.lurette.prcs_aux @@ -2,7 +2,7 @@ ;; REALLY bad things. (Created-By-Prcs-Version 1 3 3) (source/automata.ml 15954 1036675177 b/47_automata.m 1.6) -(source/formula.mli 2805 1033397911 44_formula.ml 1.18) +(source/formula.mli 2806 1037192189 44_formula.ml 1.19) (test/heater_float.lus 177 1034351455 b/44_heater_flo 1.2) (test/passerelle.luc 984 1032789516 b/17_passerelle 1.8) (doc/synthese 2556 1007379917 b/2_synthese 1.1) @@ -19,12 +19,14 @@ (mlcuddidl/sedscript 203 1034006019 c/38_sedscript 1.1) (source/automata.mli 3396 1033738731 b/46_automata.m 1.3) (test/heater_int.rif.exp 886 1034951022 b/28_heater_int 1.10) -(source/ne.ml 9140 1033723811 c/21_ne.ml 1.1) +(source/ne.ml 9160 1037192189 c/21_ne.ml 1.2) +(source/prevar.ml 981 1037192189 d/18_prevar.ml 1.1) (source/value.mli 1101 1033723811 c/24_value.mli 1.1) (user-rules.skel 973 1034006019 c/25_user-rules 1.1) (source/Makefile.gen_stubs 212 1036048863 b/42_Makefile.g 1.5) (test/temp_int.luc 685 1033723811 b/50_temp_int.e 1.3) (source/luc_exe.ml 12191 1036675177 b/32_ima_exe.ml 1.22) +(source/prevar.mli 623 1037192189 d/19_prevar.mli 1.1) (test/heater_float.rif.exp 1485 1034951022 b/30_heater_flo 1.11) (source/graph.ml 2563 1027066799 14_graph.ml 1.7) (ihm/xlurette/makefile 1583 1036048863 c/16_makefile 1.6) @@ -35,34 +37,34 @@ (source/eval.ml 7755 1027066799 49_eval.ml 1.13) (source/env.ml 8013 1027349504 16_env.ml 1.29) (demo/chaudiere/buggy_chaudiere_ctrl.lus 219 1031732392 c/10_buggy_chau 1.1) -(source/Makefile.show_luc 937 1034351455 b/40_Makefile.s 1.7) +(source/Makefile.show_luc 1026 1037192189 b/40_Makefile.s 1.8) (source/env_state.mli 6791 1036675177 50_env_state. 1.25) (mlcuddidl/idd.ml 7061 1034006019 d/0_idd.ml 1.1) (source/print.mli 1145 1033397911 46_print.mli 1.12) (mlcuddidl/rdd.mli 7174 1034006019 c/40_rdd.mli 1.1) (test/Makefile 32 1035531408 c/0_Makefile 1.8) -(source/parse_env.ml 31317 1036585364 41_parse_env. 1.31) +(source/parse_env.ml 31309 1037192189 41_parse_env. 1.32) (ihm/xlurette/xlurette_glade_main.ml 23620 1036675177 c/12_xlurette_g 1.15) (demo/chaudiere/chaudiere_oracle.lus 107 1031732392 c/8_chaudiere_ 1.1) -(source/solver.ml 32174 1036675177 39_solver.ml 1.34) +(source/solver.ml 33352 1037192189 39_solver.ml 1.35) (test/ControleurPorte.lus 3219 1032940601 c/17_Controleur 1.1) (source/gen_fake_lutin.ml 3449 1036048863 d/16_gen_fake_l 1.1) (source/lurette.ml 14219 1036675177 12_lurette.ml 1.60) (source/Makefile 1377 1036585364 c/20_Makefile 1.9) (source/util.ml 20779 1036675177 35_util.ml 1.35) (mlcuddidl/manager.mli 7912 1034006019 c/46_manager.ml 1.1) -(test/time.res 6326 1036675177 b/49_time.res 1.23) +(test/time.res 6325 1037192189 b/49_time.res 1.24) (doc/Interface_draft 5232 1003928781 19_Interface_ 1.1) (source/sim2chro.mli 1455 1027943375 b/23_sim2chro.m 1.5) (source/command_line_luc_exe.mli 1055 1036675177 b/34_command_li 1.6) (test/giro/onlyroll.lus 18298 1031732392 c/7_onlyroll.l 1.1) -(source/Makefile.lucky 2003 1035531408 b/41_Makefile.i 1.8) +(source/Makefile.lucky 2093 1037192189 b/41_Makefile.i 1.9) (TAGS 9825 1007379917 21_TAGS 1.6) (mlcuddidl/rdd.ml 8746 1034006019 c/41_rdd.ml 1.1) -(source/Makefile.lurette_lib 1741 1035531408 c/2_Makefile.l 1.8) +(source/Makefile.lurette_lib 1790 1037192189 c/2_Makefile.l 1.9) (source/parse_env.mli 1028 1036511217 40_parse_env. 1.11) (source/gen_stubs.ml 27065 1036048863 24_generate_l 1.41) -(OcamlMakefile 22626 1034951022 17_OcamlMakef 1.45) +(OcamlMakefile 22696 1037192189 17_OcamlMakef 1.46) (source/command_line.ml 4914 1035557853 b/20_command_li 1.10) (mlcuddidl/bdd.ml 10889 1034006019 d/6_bdd.ml 1.1) (mlcuddidl/idd_caml.c 15964 1034006019 c/50_idd_caml.c 1.1) @@ -74,7 +76,7 @@ (source/lurettetop.ml 30402 1036048863 c/1_lurettetop 1.22) (mlcuddidl/README 1574 1034006019 d/8_README 1.1) (cuddaux/README 1427 1034006019 c/34_README 1.1) -(source/Makefile.lurettetop 300 1035531408 d/14_Makefile.l 1.1) +(source/Makefile.lurettetop 368 1037192189 d/14_Makefile.l 1.2) (source/ne.mli 2376 1033723811 c/22_ne.mli 1.1) (README 2264 1034951022 10_README 1.4) (test/vrai_tram.lus 564 1027066799 b/6_vrai_tram. 1.2) @@ -84,7 +86,7 @@ (source/env.mli 2027 1033738731 15_env.mli 1.16) (mlcuddidl/rdd_caml.c 41613 1034006019 c/39_rdd_caml.c 1.1) (Makefile.common.in 528 1034951022 d/12_Makefile.c 1.2) -(user-rules 14217 1036675177 c/14_myrules 1.18) +(user-rules 14581 1037192189 c/14_myrules 1.19) (doc/archi.fig 3693 1003928781 20_archi.fig 1.1) (source/lurette.mli 448 1016027474 11_lurette.ml 1.12) (source/gne.mli 1552 1033397911 b/36_gne.mli 1.4) @@ -111,10 +113,10 @@ (mlcuddidl/mtbdd.ml 10185 1034006019 c/44_mtbdd.ml 1.1) (demo/chaudiere/chaudiere_ctrl.lus 177 1031732392 c/9_chaudiere_ 1.1) (source/control.mli 3208 1036675177 c/3_control.ml 1.3) -(source/formula.ml 5759 1035898240 45_formula.ml 1.22) +(source/formula.ml 5975 1037192189 45_formula.ml 1.23) (cuddaux/Makefile 3091 1034006019 c/35_Makefile 1.1) -(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1) (test/test_gen_stubs.h 1818 1020068208 b/45_test_gen_s 1.1) +(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1) (mlcuddidl/idd.idl 10595 1034006019 d/1_idd.idl 1.1) (source/gne.ml 2767 1033397911 b/37_gne.ml 1.4) (cuddaux/cuddaux.h 2381 1034006019 c/33_cuddaux.h 1.1) @@ -124,13 +126,13 @@ (mlcuddidl/bdd.mli 8573 1034006019 d/5_bdd.mli 1.1) (doc/automata_format 0 1007379917 b/3_automata_f 1.1) (source/solver.mli 1003 1027092697 38_solver.mli 1.13) -(source/rnumsolver.ml 20806 1036048863 b/27_rnumsolver 1.14) +(source/rnumsolver.ml 21392 1037192189 b/27_rnumsolver 1.15) (mlcuddidl/cudd_caml.c 22890 1034006019 d/3_cudd_caml. 1.1) (source/print.ml 5807 1033723811 47_print.ml 1.21) (test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1) (configure.in 5208 1034351455 d/11_configure. 1.1) (cuddaux/cuddauxBridge.c 6099 1034006019 c/31_cuddauxBri 1.1) -(source/show_env.ml 3594 1036675177 43_show_env.m 1.15) +(source/show_env.ml 3642 1037192189 43_show_env.m 1.16) (mlcuddidl/Changes 64 1034006019 d/10_Changes 1.1) (source/parse_poc.ml 7093 1036048863 d/15_parse_poc. 1.1) (cuddaux/cuddauxAddIte.c 12812 1034006019 c/32_cuddauxAdd 1.1) @@ -139,7 +141,7 @@ (source/command_line_luc_exe.ml 2759 1036675177 b/33_command_li 1.8) (mlcuddidl/cudd_caml.h 1210 1034006019 d/2_cudd_caml. 1.1) (source/value.ml 2355 1033723811 c/23_value.ml 1.1) -(test/time.exp 6326 1036675177 b/48_time.exp 1.20) +(test/time.exp 6325 1037192189 b/48_time.exp 1.21) (test/giro/allocator.lus 1087 1031732392 c/5_allocator. 1.1) (lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2) (mlcuddidl/idd.mli 5470 1034006019 c/51_idd.mli 1.1) diff --git a/OcamlMakefile b/OcamlMakefile index d1aa439..146b13e 100644 --- a/OcamlMakefile +++ b/OcamlMakefile @@ -5,7 +5,7 @@ # For updates see: # http://www.oefai.at/~markus/ocaml_sources # -# $Id: OcamlMakefile 1.45 Fri, 18 Oct 2002 16:23:42 +0200 jahier $ +# $Id: OcamlMakefile 1.46 Wed, 13 Nov 2002 13:56:29 +0100 jahier $ # ########################################################################### @@ -16,6 +16,7 @@ SOURCES_LURETTE_LIB = \ $(LURETTE_PATH)/source/util.ml \ + $(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.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 \ diff --git a/lurette.prj b/lurette.prj index 652888a..fdc3bc0 100644 --- a/lurette.prj +++ b/lurette.prj @@ -1,23 +1,23 @@ ;; -*- Prcs -*- (Created-By-Prcs-Version 1 3 3) (Project-Description "Lurette") -(Project-Version lurette 0 115) -(Parent-Version lurette 0 114) +(Project-Version lurette 0 116) +(Parent-Version lurette 0 115) (Version-Log " -source/automata.ml: - Fix a bug where esp loops were not always cutted properly in some cases. +source/solver.ml: + Give a better error message when users do not initialize pre vars. -source/show_env.ml: - Truncate too long for in the dot output (which bugs dot or gv). +source/parse_env.ml: +source/formula.ml: +source/prevar.ml/mli: (new files) + Put here everything that handles the internal representation of pre var names. -ihm/xlurette/xlurette_glade_main.ml: - Accept both .lut or .lut files as anv files, and make the show buttons - behave properly in both cases. + Pretty print internal pre var names. ") (New-Version-Log "" ) -(Checkin-Time "Thu, 07 Nov 2002 14:19:37 +0100") +(Checkin-Time "Wed, 13 Nov 2002 13:56:29 +0100") (Checkin-Login jahier) (Populate-Ignore ()) (Project-Keywords) @@ -51,19 +51,19 @@ ihm/xlurette/xlurette_glade_main.ml: (source/util.ml (lurette/35_util.ml 1.35 444)) (source/solver.mli (lurette/38_solver.mli 1.13 644)) - (source/solver.ml (lurette/39_solver.ml 1.34 644)) + (source/solver.ml (lurette/39_solver.ml 1.35 644)) (source/rnumsolver.mli (lurette/b/26_rnumsolver 1.9 644)) - (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.14 644)) + (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.15 644)) (source/parse_env.mli (lurette/40_parse_env. 1.11 644)) - (source/parse_env.ml (lurette/41_parse_env. 1.31 644)) + (source/parse_env.ml (lurette/41_parse_env. 1.32 644)) (source/show_env.mli (lurette/42_show_env.m 1.8 644)) - (source/show_env.ml (lurette/43_show_env.m 1.15 644)) + (source/show_env.ml (lurette/43_show_env.m 1.16 644)) - (source/formula.mli (lurette/44_formula.ml 1.18 644)) - (source/formula.ml (lurette/45_formula.ml 1.22 644)) + (source/formula.mli (lurette/44_formula.ml 1.19 644)) + (source/formula.ml (lurette/45_formula.ml 1.23 644)) (source/print.mli (lurette/46_print.mli 1.12 644)) (source/print.ml (lurette/47_print.ml 1.21 644)) @@ -92,12 +92,14 @@ ihm/xlurette/xlurette_glade_main.ml: (source/constraint.mli (lurette/c/18_constraint 1.4 644)) (source/constraint.ml (lurette/c/19_constraint 1.4 644)) - (source/ne.ml (lurette/c/21_ne.ml 1.1 644)) + (source/ne.ml (lurette/c/21_ne.ml 1.2 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)) + (source/prevar.ml (lurette/d/18_prevar.ml 1.1 644)) + (source/prevar.mli (lurette/d/19_prevar.mli 1.1 644)) (source/parse_poc.ml (lurette/d/15_parse_poc. 1.1 644)) (source/gen_fake_lutin.ml (lurette/d/16_gen_fake_l 1.1 644)) @@ -108,18 +110,18 @@ ihm/xlurette/xlurette_glade_main.ml: ;; Make files (configure.in (lurette/d/11_configure. 1.1 644)) (Makefile.common.in (lurette/d/12_Makefile.c 1.2 644)) - (OcamlMakefile (lurette/17_OcamlMakef 1.45 644)) + (OcamlMakefile (lurette/17_OcamlMakef 1.46 644)) (Makefile.lurette (lurette/b/38_Makefile.l 1.15 644)) - (user-rules (lurette/c/14_myrules 1.18 644)) + (user-rules (lurette/c/14_myrules 1.19 644)) (user-rules.skel (lurette/c/25_user-rules 1.1 644)) (Makefile (lurette/d/13_Makefile 1.1 644)) - (source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.1 644)) + (source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.2 644)) (source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.1 644)) - (source/Makefile.show_luc (lurette/b/40_Makefile.s 1.7 644)) - (source/Makefile.lucky (lurette/b/41_Makefile.i 1.8 644)) + (source/Makefile.show_luc (lurette/b/40_Makefile.s 1.8 644)) + (source/Makefile.lucky (lurette/b/41_Makefile.i 1.9 644)) (source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.5 644)) - (source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.8 644)) + (source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.9 644)) (source/Makefile (lurette/c/20_Makefile 1.9 644)) ;; Documentation @@ -137,8 +139,8 @@ ihm/xlurette/xlurette_glade_main.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.20 644)) - (test/time.res (lurette/b/49_time.res 1.23 644)) + (test/time.exp (lurette/b/48_time.exp 1.21 644)) + (test/time.res (lurette/b/49_time.res 1.24 644)) ;; Various files used for testing purposes (test/usager.luc (lurette/b/14_usager.env 1.9 644)) @@ -225,12 +227,6 @@ ihm/xlurette/xlurette_glade_main.ml: (mlcuddidl/Changes (lurette/d/10_Changes 1.1 644)) - - - -;; Files added by populate at Thu, 24 Oct 2002 15:46:40 +0200, -;; to version 0.105(w), by jahier: - ) (Merge-Parents) (New-Merge-Parents) diff --git a/source/Makefile.lucky b/source/Makefile.lucky index a5aec2d..fcf44b9 100644 --- a/source/Makefile.lucky +++ b/source/Makefile.lucky @@ -6,13 +6,13 @@ ####################################################################### -OCAMLNCFLAGS = -inline 10 +OCAMLNCFLAGS = -inline 10 -linkall ifndef OCAMLFLAGS - OCAMLFLAGS := -noassert -unsafe + OCAMLFLAGS := -noassert -unsafe endif # Requires cudd and mldd to be installed! -LIBS = str nums # mlpoly +LIBS = str nums # mlpoly CLIBS = cudd_caml cuddaux cudd camlidl mtr st epd util # libppl libpolyi USE_CAMLP4 = yes @@ -22,6 +22,7 @@ USE_CAMLP4 = yes SOURCES_OCAML = \ $(LURETTE_PATH)/source/util.ml \ $(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \ + $(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \ $(LURETTE_PATH)/source/command_line_luc_exe.mli $(LURETTE_PATH)/source/command_line_luc_exe.ml \ $(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \ $(LURETTE_PATH)/source/ne.mli $(LURETTE_PATH)/source/ne.ml \ diff --git a/source/Makefile.lurette_lib b/source/Makefile.lurette_lib index ea08716..53eb313 100644 --- a/source/Makefile.lurette_lib +++ b/source/Makefile.lurette_lib @@ -6,14 +6,11 @@ ###################################################################### - -OCAMLNCFLAGS = -inline 10 -noassert -unsafe - +OCAMLNCFLAGS = -inline 10 ifndef OCAMLFLAGS OCAMLFLAGS := -noassert -unsafe endif - # Requires cudd and mldd to be installed! LIBS = str nums # mlpoly CLIBS = cudd_caml cuddaux cudd mtr st epd util # libppl libpolyi @@ -24,6 +21,7 @@ USE_CAMLP4 = yes SOURCES = \ $(LURETTE_PATH)/source/util.ml \ + $(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.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 \ diff --git a/source/Makefile.lurettetop b/source/Makefile.lurettetop index 719fd90..7fdb83d 100644 --- a/source/Makefile.lurettetop +++ b/source/Makefile.lurettetop @@ -6,7 +6,10 @@ LIBS = unix str CLIBS = -OCAMLNCFLAGS = -inline 10 +OCAMLNCFLAGS = -inline 10 -linkall +ifndef OCAMLFLAGS + OCAMLFLAGS := -noassert -unsafe +endif USE_CAMLP4 = yes diff --git a/source/Makefile.show_luc b/source/Makefile.show_luc index 3c3dd42..e8b2c97 100644 --- a/source/Makefile.show_luc +++ b/source/Makefile.show_luc @@ -7,7 +7,7 @@ ###################################################################### OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile -OCAMLNCFLAGS = -inline 10 +OCAMLNCFLAGS = -inline 10 -linkall LIBS = str CLIBS = @@ -17,6 +17,7 @@ USE_CAMLP4 = yes SOURCES_OCAML = \ $(LURETTE_PATH)/source/util.ml \ + $(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \ $(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \ $(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \ $(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \ diff --git a/source/formula.ml b/source/formula.ml index b5f6872..0eb19c9 100644 --- a/source/formula.ml +++ b/source/formula.ml @@ -77,6 +77,11 @@ type env_loc = subst list (****************************************************************************) +(* exported *) +let (formula_to_var_value: formula -> Value.t) = function + True -> B(true) + | False -> B(false) + | _ -> assert false let rec @@ -98,7 +103,7 @@ and | EqB(f1, f2) -> ((formula_to_string f1) ^ " = " ^ (formula_to_string f2)) | True -> "true" | False -> "false" - | Bvar(str) -> str + | Bvar(str) -> (Prevar.format str) | Eq(e1, e2) -> ((expr_to_string e1) ^ " = " ^ (expr_to_string e2)) | Neq(e1, e2) -> ((expr_to_string e1) ^ " <> " ^ (expr_to_string e2)) | SupEq(e1, e2) -> ((expr_to_string e1) ^ " >= " ^ (expr_to_string e2)) @@ -118,8 +123,8 @@ and (expr_to_string e2) ^ ")") | Mod(e1, e2) -> ("(" ^ (expr_to_string e1) ^ " mod " ^ (expr_to_string e2) ^ ")") - | Ivar(str) -> str - | Fvar(str) -> str + | Ivar(str) -> (Prevar.format str) + | Fvar(str) -> (Prevar.format str) | Ival(i) -> string_of_int i | Fval(f) -> Util.my_string_of_float f | Ite(f,e1,e2) -> ("(if " ^ (formula_to_string f) ^ " then " ^ @@ -177,7 +182,7 @@ let (print_subst_list : subst list -> out_channel -> unit) = fun sl oc -> List.iter (fun (vn, e) -> - output_string oc vn ; + output_string oc (Prevar.format vn); output_string oc " = "; Value.print oc e; output_string oc "\n\t" @@ -188,7 +193,7 @@ let (print_env_in : env_in -> out_channel -> unit) = fun tbl oc -> Hashtbl.iter (fun vn e -> - output_string oc vn ; + output_string oc (Prevar.format vn) ; output_string oc " = "; Value.print oc e; output_string oc "\n\t" diff --git a/source/formula.mli b/source/formula.mli index 61ceb5c..6a89dc5 100644 --- a/source/formula.mli +++ b/source/formula.mli @@ -102,3 +102,4 @@ val var_type_to_string : var_type -> string val var_type_to_string2 : var_type -> string val print_subst_list : subst list -> out_channel -> unit val print_env_in : env_in -> out_channel -> unit + diff --git a/source/ne.ml b/source/ne.ml index 661b6b9..a961063 100644 --- a/source/ne.ml +++ b/source/ne.ml @@ -229,7 +229,7 @@ let (make : string -> Value.num -> t) = let (find : string -> t -> Value.num) = fun vn ne -> StringMap.find vn ne - + (****************************************************************************) @@ -335,7 +335,7 @@ let (to_string : t -> string) = (fun vn v acc -> if vn = "" then ((num_value_to_string v) ^ acc) - else (" + " ^ (num_value_to_string v ) ^ "*" ^ vn ^ acc )) + else (" + " ^ (num_value_to_string v ) ^ "*" ^ ((Prevar.format vn) ^ acc))) ne "" ) diff --git a/source/parse_env.ml b/source/parse_env.ml index be86e7e..1b388c5 100644 --- a/source/parse_env.ml +++ b/source/parse_env.ml @@ -448,7 +448,7 @@ and (parse_prevar: in_channel -> aut_token -> vnt) = 'Genlex.Kwd ")"; pl = parse_pragma_list ic ; 'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >] -> - let pre_var = ("_pre" ^ (string_of_int i) ^ var) in + let pre_var = Prevar.create_prevar_name i var in ( match typ with "bool" -> (pre_var, BoolT) | "float" -> (pre_var, FloatT(-.default_max_float, default_max_float)) @@ -783,7 +783,7 @@ and (parse_formula: in_channel -> vnt list -> aut_token -> formula) = pl = parse_pragma_list ic >] -> - let pre_id = ("_pre" ^ (string_of_int i) ^ id) in + let pre_id = Prevar.create_prevar_name i id in (* Ditto *) let (_, vt) = List.find (fun (vn,vt) -> vn = pre_id) vars in ( match vt with @@ -907,7 +907,7 @@ and (parse_simple: in_channel -> vnt list -> aut_token -> expr) = | [< 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident id; 'Genlex.Kwd ")"; pl = parse_pragma_list ic >] -> - let s = ("_pre" ^ (string_of_int i) ^ id) in + let s = Prevar.create_prevar_name i id in let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in let var = match vt with diff --git a/source/prevar.ml b/source/prevar.ml new file mode 100644 index 0000000..7ce8a19 --- /dev/null +++ b/source/prevar.ml @@ -0,0 +1,33 @@ +(*----------------------------------------------------------------------- +** Copyright (C) 2002 - Verimag. +** This file may only be copied under the terms of the GNU Library General +** Public License +**----------------------------------------------------------------------- +** +** File: prevar.ml +** Author: jahier@imag.fr +*) + +(* exported *) +let (create_prevar_name : int -> string -> string) = + fun i str -> + ("_pre" ^ (string_of_int i) ^ str) + +let (is_pre_var : string -> bool) = + fun str -> + try (String.sub str 0 4) = "_pre" + with _ -> false + +(* exported *) +let (format: string -> string) = + fun vn -> + try + let l = String.length vn in + let char_reg = Str.regexp "[^0-9]" in + let i = Str.search_forward char_reg vn 4 in + let pre_nb = (int_of_string (String.sub vn 4 (i-4))) in + let pre_list = Util.unfold (fun _ -> "pre ") () pre_nb in + ("(" ^ (String.concat "" pre_list) ^ (String.sub vn i (l-i)) ^ ")") + with + | _ -> vn + diff --git a/source/prevar.mli b/source/prevar.mli new file mode 100644 index 0000000..799d974 --- /dev/null +++ b/source/prevar.mli @@ -0,0 +1,21 @@ +(*----------------------------------------------------------------------- +** Copyright (C) 2002 - Verimag. +** This file may only be copied under the terms of the GNU Library General +** Public License +**----------------------------------------------------------------------- +** +** File: prevar.mli +** Author: jahier@imag.fr +*) + +(** Internal representation of pre variables. *) + + +(** To give an internal name to pre var *) +val create_prevar_name : int -> string -> string + +(** To pretty print pre var *) +val format: string -> string + +(** [is_pre_va vn] returns iff [vn] is a pre variable. *) +val is_pre_var : string -> bool diff --git a/source/rnumsolver.ml b/source/rnumsolver.ml index 3741233..569c414 100644 --- a/source/rnumsolver.ml +++ b/source/rnumsolver.ml @@ -302,7 +302,7 @@ let rec (split_store : store -> Constraint.ineq -> store * store) = fun store cstr0 -> let cstr = Constraint.apply_substl_ineq store.substl cstr0 in (* let _ = *) -(* print_string "\n >>> " ; *) +(* print_string "\n split_store \n" ; *) (* print_string (Constraint.ineq_to_string cstr); *) (* flush stdout *) (* in *) @@ -315,20 +315,30 @@ let rec (split_store : store -> Constraint.ineq -> store * store) = applied store.substl to [cstr] *) and (split_store_do : store -> Constraint.ineq -> store * store) = fun store cstr -> +(* let _ = *) +(* print_string "\n split_store_do\n" ; *) +(* flush stdout *) +(* in *) let (var, sl, d) = (store.var, store.substl, store.delay) in let dim = Constraint.dimension_ineq cstr in if dim = 0 then - match cstr with - GZ(ne) -> - if Value.num_sup_zero (Ne.find "" ne) - then store, {var=None ; substl = [] ; delay = []} - else {var=None ; substl = [] ; delay = []}, store - | GeqZ(ne) -> - if Value.num_supeq_zero (Ne.find "" ne) - then store, store - else raise No_numeric_solution +(* let _ = *) +(* print_string "\n split_store_do 1 \n" ; *) +(* flush stdout *) +(* in *) + ( match cstr with + GZ(ne) -> + if Value.num_sup_zero (Ne.find "" ne) + then store, {var=None ; substl = [] ; delay = []} + else {var=None ; substl = [] ; delay = []}, store + | GeqZ(ne) -> + if Value.num_supeq_zero (Ne.find "" ne) + then store, store + else raise No_numeric_solution + ) + else if dim > 1 then @@ -341,393 +351,397 @@ and (split_store_do : store -> Constraint.ineq -> store * store) = raise No_numeric_solution | Some(tbl) -> let (vn, nac) = normalise cstr in - ( match (nac, (Hashtbl.find tbl vn)) with - (NSupEqI(i), RangeI(min, max)) -> - if i <= min - then ( - {var=Some(tbl) ; substl=sl ; delay=d }, - {var=None ; substl=sl ; delay=d } - ) - else if i > max - then ( - {var=None ; substl=sl ; delay=d }, - {var=Some(tbl) ; substl=sl ; delay=d } - ) - else (* min < i <= max *) - ( - let tbl2 = Hashtbl.copy tbl in - let sl1 = - (* Whenever, a variable become bounded, - we add it to the list of substitutions - and remove it from the store. *) - if i = max - then - ( - Hashtbl.remove tbl vn; - (make_subst vn (I max))::sl - ) - else - ( - Hashtbl.replace tbl vn (RangeI(i, max)); - sl - ) - in - let sl2 = - if min = (i-1) - then - ( - Hashtbl.remove tbl2 vn; - (make_subst vn (I min))::sl - ) - else - ( - Hashtbl.replace tbl2 vn (RangeI(min, i-1)); - sl - ) - in ( - { var=Some(tbl) ; substl=sl1 ; delay=d }, - { var=Some(tbl2) ; substl=sl2 ; delay=d } - ) + ( match (nac, (Hashtbl.find tbl vn)) with + (NSupEqI(i), RangeI(min, max)) -> + if i <= min + then ( + {var=Some(tbl) ; substl=sl ; delay=d }, + {var=None ; substl=sl ; delay=d } ) - | - (NInfEqI(i), RangeI(min, max)) -> - if i < min - then ( - {var=None ; substl=sl ; delay=d }, - {var=Some(tbl) ; substl=sl ; delay=d } - ) - else if i >= max - then ( - {var=Some(tbl) ; substl=sl ; delay=d }, - {var=None ; substl=sl ; delay=d } - ) - else (* min <= i < max *) - ( - let tbl2 = Hashtbl.copy tbl in - let sl1 = - if i = min - then - ( - Hashtbl.remove tbl vn; - (make_subst vn (I min))::sl - ) - else - ( - Hashtbl.replace tbl vn (RangeI(min, i)); - sl - ) - in - let sl2 = - if max = (i+1) - then - ( - Hashtbl.remove tbl2 vn; - (make_subst vn (I max))::sl + else if i > max + then ( + {var=None ; substl=sl ; delay=d }, + {var=Some(tbl) ; substl=sl ; delay=d } + ) + else (* min < i <= max *) + ( + let tbl2 = Hashtbl.copy tbl in + let sl1 = + (* Whenever, a variable become bounded, + we add it to the list of substitutions + and remove it from the store. *) + if i = max + then + ( + Hashtbl.remove tbl vn; + (make_subst vn (I max))::sl + ) + else + ( + Hashtbl.replace tbl vn (RangeI(i, max)); + sl + ) + in + let sl2 = + if min = (i-1) + then + ( + Hashtbl.remove tbl2 vn; + (make_subst vn (I min))::sl + ) + else + ( + Hashtbl.replace tbl2 vn (RangeI(min, i-1)); + sl + ) + in ( + { var=Some(tbl) ; substl=sl1 ; delay=d }, + { var=Some(tbl2) ; substl=sl2 ; delay=d } ) - else + ) + | + (NInfEqI(i), RangeI(min, max)) -> + if i < min + then ( + {var=None ; substl=sl ; delay=d }, + {var=Some(tbl) ; substl=sl ; delay=d } + ) + else if i >= max + then ( + {var=Some(tbl) ; substl=sl ; delay=d }, + {var=None ; substl=sl ; delay=d } + ) + else (* min <= i < max *) + ( + let tbl2 = Hashtbl.copy tbl in + let sl1 = + if i = min + then + ( + Hashtbl.remove tbl vn; + (make_subst vn (I min))::sl + ) + else + ( + Hashtbl.replace tbl vn (RangeI(min, i)); + sl + ) + in + let sl2 = + if max = (i+1) + then + ( + Hashtbl.remove tbl2 vn; + (make_subst vn (I max))::sl + ) + else + ( + Hashtbl.replace tbl2 vn (RangeI(i+1, max)); + sl + ) + in ( - Hashtbl.replace tbl2 vn (RangeI(i+1, max)); - sl + { var=Some(tbl) ; substl=sl1 ; delay=d }, + { var=Some(tbl2) ; substl=sl2 ; delay=d } ) - in - ( - { var=Some(tbl) ; substl=sl1 ; delay=d }, - { var=Some(tbl2) ; substl=sl2 ; delay=d } - ) - ) - - (** **) - | (NSupEqF(f), RangeF(min, max)) -> - if f <= min - then ( - {var=Some(tbl) ; substl=sl ; delay=d }, - {var=None ; substl=sl ; delay=d } - ) - else if f > max - then ( - {var=None ; substl=sl ; delay=d }, - {var=Some(tbl) ; substl=sl ; delay=d } - ) - else (* min < f <= max *) - ( - let tbl2 = Hashtbl.copy tbl in - let sl1 = - if f = max - then - ( - Hashtbl.remove tbl vn; - (make_subst vn (F max))::sl - ) - else - ( - Hashtbl.replace tbl vn (RangeF(f, max)); - sl - ) - in - let sl2 = - if min = (f-.eps) - then - ( - Hashtbl.remove tbl2 vn; - (make_subst vn (F min))::sl - ) - else + ) + + (** **) + | (NSupEqF(f), RangeF(min, max)) -> + if f <= min + then ( + {var=Some(tbl) ; substl=sl ; delay=d }, + {var=None ; substl=sl ; delay=d } + ) + else if f > max + then ( + {var=None ; substl=sl ; delay=d }, + {var=Some(tbl) ; substl=sl ; delay=d } + ) + else (* min < f <= max *) + ( + let tbl2 = Hashtbl.copy tbl in + let sl1 = + if f = max + then + ( + Hashtbl.remove tbl vn; + (make_subst vn (F max))::sl + ) + else + ( + Hashtbl.replace tbl vn (RangeF(f, max)); + sl + ) + in + let sl2 = + if min = (f-.eps) + then + ( + Hashtbl.remove tbl2 vn; + (make_subst vn (F min))::sl + ) + else + ( + Hashtbl.replace tbl2 vn (RangeF(min, f-.eps)); + sl + ) + in ( - Hashtbl.replace tbl2 vn (RangeF(min, f-.eps)); - sl + { var=Some(tbl) ; substl=sl1 ; delay=d }, + { var=Some(tbl2) ; substl=sl2 ; delay=d } ) - in - ( - { var=Some(tbl) ; substl=sl1 ; delay=d }, - { var=Some(tbl2) ; substl=sl2 ; delay=d } - ) - ) - | - (NInfEqF(f), RangeF(min, max)) -> - if f < min - then ( - {var=None ; substl=sl ; delay=d }, - {var=Some(tbl) ; substl=sl ; delay=d } - ) - else if f >= max - then ( - {var=Some(tbl) ; substl=sl ; delay=d }, - {var=None ; substl=sl ; delay=d } - ) - else (* min <= f < max *) - ( - let tbl2 = Hashtbl.copy tbl in - let sl1 = - if f = min - then - ( - Hashtbl.remove tbl vn; - (make_subst vn (F min))::sl - ) - else - ( - Hashtbl.replace tbl vn (RangeF(min, f)); - sl - ) - in - let sl2 = - if max = (f+.eps) - then - ( - Hashtbl.remove tbl2 vn; - (make_subst vn (F max))::sl - ) - else + ) + | + (NInfEqF(f), RangeF(min, max)) -> + if f < min + then ( + {var=None ; substl=sl ; delay=d }, + {var=Some(tbl) ; substl=sl ; delay=d } + ) + else if f >= max + then ( + {var=Some(tbl) ; substl=sl ; delay=d }, + {var=None ; substl=sl ; delay=d } + ) + else (* min <= f < max *) + ( + let tbl2 = Hashtbl.copy tbl in + let sl1 = + if f = min + then + ( + Hashtbl.remove tbl vn; + (make_subst vn (F min))::sl + ) + else + ( + Hashtbl.replace tbl vn (RangeF(min, f)); + sl + ) + in + let sl2 = + if max = (f+.eps) + then + ( + Hashtbl.remove tbl2 vn; + (make_subst vn (F max))::sl + ) + else + ( + Hashtbl.replace tbl2 vn (RangeF(f+.eps, max)); + sl + ) + in ( - Hashtbl.replace tbl2 vn (RangeF(f+.eps, max)); - sl + { var=Some(tbl) ; substl=sl1 ; delay=d }, + { var=Some(tbl2) ; substl=sl2 ; delay=d } ) - in - ( - { var=Some(tbl) ; substl=sl1 ; delay=d }, - { var=Some(tbl2) ; substl=sl2 ; delay=d } - ) - ) - - | (NSupF(f), RangeF(min, max)) -> - if f < min - then ( - {var=Some(tbl) ; substl=sl ; delay=d }, - {var=None ; substl=sl ; delay=d } - ) - else if f >= max - then ( - {var=None ; substl=sl ; delay=d }, - {var=Some(tbl) ; substl=sl ; delay=d } - ) - else (* min <= f < max *) - ( - let tbl2 = Hashtbl.copy tbl in - let sl1 = - if (f+.eps) = max - then - ( - Hashtbl.remove tbl vn; - (make_subst vn (F max))::sl - ) - else - ( - Hashtbl.replace tbl vn (RangeF(f+.eps, max)); - sl - ) - in - let sl2 = - if min = f - then - ( - Hashtbl.remove tbl2 vn; - (make_subst vn (F min))::sl - ) - else + ) + + | (NSupF(f), RangeF(min, max)) -> + if f < min + then ( + {var=Some(tbl) ; substl=sl ; delay=d }, + {var=None ; substl=sl ; delay=d } + ) + else if f >= max + then ( + {var=None ; substl=sl ; delay=d }, + {var=Some(tbl) ; substl=sl ; delay=d } + ) + else (* min <= f < max *) + ( + let tbl2 = Hashtbl.copy tbl in + let sl1 = + if (f+.eps) = max + then + ( + Hashtbl.remove tbl vn; + (make_subst vn (F max))::sl + ) + else + ( + Hashtbl.replace tbl vn (RangeF(f+.eps, max)); + sl + ) + in + let sl2 = + if min = f + then + ( + Hashtbl.remove tbl2 vn; + (make_subst vn (F min))::sl + ) + else + ( + Hashtbl.replace tbl2 vn (RangeF(min, f)); + sl + ) + in ( - Hashtbl.replace tbl2 vn (RangeF(min, f)); - sl + { var=Some(tbl) ; substl=sl1 ; delay=d }, + { var=Some(tbl2) ; substl=sl2 ; delay=d } ) - in - ( - { var=Some(tbl) ; substl=sl1 ; delay=d }, - { var=Some(tbl2) ; substl=sl2 ; delay=d } - ) - ) - | - (NInfF(f), RangeF(min, max)) -> - if f <= min - then ( - {var=None ; substl=sl ; delay=d }, - {var=Some(tbl) ; substl=sl ; delay=d } - ) - else if f > max - then ( - {var=Some(tbl) ; substl=sl ; delay=d }, - {var=None ; substl=sl ; delay=d } - ) - else (* min < f <= max *) - ( - let tbl2 = Hashtbl.copy tbl in - let sl1 = - if (f-.eps) = min - then - ( - Hashtbl.remove tbl vn; - (make_subst vn (F min))::sl - ) - else - ( - Hashtbl.replace tbl vn (RangeF(min, f-.eps)); - sl - ) - in - let sl2 = - if max = f - then - ( - Hashtbl.remove tbl2 vn; - (make_subst vn (F max))::sl - ) - else + ) + | + (NInfF(f), RangeF(min, max)) -> + if f <= min + then ( + {var=None ; substl=sl ; delay=d }, + {var=Some(tbl) ; substl=sl ; delay=d } + ) + else if f > max + then ( + {var=Some(tbl) ; substl=sl ; delay=d }, + {var=None ; substl=sl ; delay=d } + ) + else (* min < f <= max *) + ( + let tbl2 = Hashtbl.copy tbl in + let sl1 = + if (f-.eps) = min + then + ( + Hashtbl.remove tbl vn; + (make_subst vn (F min))::sl + ) + else + ( + Hashtbl.replace tbl vn (RangeF(min, f-.eps)); + sl + ) + in + let sl2 = + if max = f + then + ( + Hashtbl.remove tbl2 vn; + (make_subst vn (F max))::sl + ) + else + ( + Hashtbl.replace tbl2 vn (RangeF(f, max)); + sl + ) + in ( - Hashtbl.replace tbl2 vn (RangeF(f, max)); - sl + { var=Some(tbl) ; substl=sl1 ; delay=d }, + { var=Some(tbl2) ; substl=sl2 ; delay=d } ) - in - ( - { var=Some(tbl) ; substl=sl1 ; delay=d }, - { var=Some(tbl2) ; substl=sl2 ; delay=d } - ) - ) + ) - | _ -> assert false - ) - + | _ -> assert false + ) + + (* exported *) and (split_store_eq : store -> Ne.t -> store * store * store ) = - fun store ne0 -> + fun store ne0 -> let ne = Ne.apply_substl store.substl ne0 in - + (* let _ = *) (* print_string (store_to_string store); *) (* print_string "\n >>> " ; *) (* print_string (Constraint.to_string (EqZ ne)); *) (* flush stdout *) (* in *) - + let dim = Ne.dimension ne in if dim = 0 then - let v = (Ne.find "" ne) - and unsat_store = { var = None ; substl = [] ; delay = [] } in - if - Value.num_eq_zero v - then - store, unsat_store, unsat_store - else if - Value.num_sup_zero v - then - unsat_store, store, unsat_store - else - unsat_store, unsat_store, store - else - (* dim > 0 *) - let (store_inf, store_sup) = split_store_do store (GZ ne) in - let (var, sl, d) = (store.var, store.substl, store.delay) in - let (vn_val_opt, ne_tail) = Ne.split ne in - match vn_val_opt with - None -> - raise No_numeric_solution - | Some (vn, nval0) -> - let nval = Value.neg nval0 in - let s = ((vn, nval), ne_tail) in - let d2 = List.map (Constraint.apply_subst_ineq s) d in - let (waked, new_d) = List.partition - (fun cstr -> Constraint.dimension_ineq cstr = 1) - d2 - in - let new_sl = s::sl in - let range_vn, new_var = - match var with - None -> assert false - | Some(tbl) -> - ( - Hashtbl.find tbl vn, +(* try *) + let v = (Ne.find "" ne) + and unsat_store = { var = None ; substl = [] ; delay = [] } in + if + Value.num_eq_zero v + then + store, unsat_store, unsat_store + else if + Value.num_sup_zero v + then + unsat_store, store, unsat_store + else + unsat_store, unsat_store, store +(* with Not_found -> *) +(* assert false *) + (* store, unsat_store, unsat_store *) + else + (* dim > 0 *) + let (store_inf, store_sup) = split_store_do store (GZ ne) in + let (var, sl, d) = (store.var, store.substl, store.delay) in + let (vn_val_opt, ne_tail) = Ne.split ne in + match vn_val_opt with + None -> + raise No_numeric_solution + | Some (vn, nval0) -> + let nval = Value.neg nval0 in + let s = ((vn, nval), ne_tail) in + let d2 = List.map (Constraint.apply_subst_ineq s) d in + let (waked, new_d) = List.partition + (fun cstr -> Constraint.dimension_ineq cstr = 1) + d2 + in + let new_sl = s::sl in + let range_vn, new_var = + match var with + None -> assert false + | Some(tbl) -> + ( + Hashtbl.find tbl vn, + ( + let tbl2 = Hashtbl.copy tbl in + Hashtbl.remove tbl2 vn; + Some(tbl2) + ) + ) + in + let new_store = + List.fold_left + (fun acc cstr -> fst (split_store acc cstr)) + { var = new_var; substl = new_sl; delay = new_d } + waked + in + if + Ne.is_a_constant ne_tail + then + ( + new_store, + store_inf, + store_sup + ) + else + let c1, c2 = + match range_vn with + RangeI(min, max) -> + GeqZ(Ne.diff (Ne.make "" (I (-min))) ne_tail), + GeqZ(Ne.diff (Ne.make "" (I max)) ne_tail) + | RangeF(min, max) -> + GeqZ(Ne.diff (Ne.make "" (F (-.min))) ne_tail), + GeqZ(Ne.diff (Ne.make "" (F max)) ne_tail) + in + if + dim = 2 + then ( - let tbl2 = Hashtbl.copy tbl in - Hashtbl.remove tbl2 vn; - Some(tbl2) + fst (split_store (fst (split_store new_store c1)) c2), + store_inf, + store_sup ) - ) - in - let new_store = - List.fold_left - (fun acc cstr -> fst (split_store acc cstr)) - { var = new_var; substl = new_sl; delay = new_d } - waked - in - if - Ne.is_a_constant ne_tail - then - ( - new_store, - store_inf, - store_sup - ) - else - let c1, c2 = - match range_vn with - RangeI(min, max) -> - GeqZ(Ne.diff (Ne.make "" (I (-min))) ne_tail), - GeqZ(Ne.diff (Ne.make "" (I max)) ne_tail) - | RangeF(min, max) -> - GeqZ(Ne.diff (Ne.make "" (F (-.min))) ne_tail), - GeqZ(Ne.diff (Ne.make "" (F max)) ne_tail) - in - if - dim = 2 - then - ( - fst (split_store (fst (split_store new_store c1)) c2), - store_inf, - store_sup - ) - else - (* dim > 2 *) - ( - { - var = new_store.var ; - substl = new_store.substl ; - delay = c1::c2::new_store.delay - }, - store_inf, - store_sup - ) - - + else + (* dim > 2 *) + ( + { + var = new_store.var ; + substl = new_store.substl ; + delay = c1::c2::new_store.delay + }, + store_inf, + store_sup + ) + (* exported *) let (is_store_satisfiable : store -> bool) = fun store -> diff --git a/source/show_env.ml b/source/show_env.ml index acc8394..994d3b6 100644 --- a/source/show_env.ml +++ b/source/show_env.ml @@ -113,11 +113,13 @@ let (graph_to_dot: 'node list -> 'node list -> string -> (* Exported *) +let max_label_size = 50 + let arc_to_string_trunc arc = let str = Formula.arc_info_to_string arc in - if String.length str <= 40 + if String.length str <= max_label_size then str - else ((String.sub str 0 40) ^ " ...") + else ((String.sub str 0 max_label_size) ^ " ...") let (luc_to_dot: Formula.node list -> Formula.node list -> string -> (Formula.node, Formula.arc_info) Graph.t -> unit) = diff --git a/source/solver.ml b/source/solver.ml index 7601b30..c79d631 100644 --- a/source/solver.ml +++ b/source/solver.ml @@ -22,9 +22,39 @@ open Rnumsolver let (lookup: env_in -> subst list -> var_name -> Value.t option) = fun input pre vn -> try Some(Hashtbl.find input vn) - with Not_found -> - try Some(List.assoc vn pre) - with Not_found -> None + with + Not_found -> + ( try Some(List.assoc vn pre) + with + Not_found -> + if + Prevar.is_pre_var vn + then + ( + let cnl = List.flatten (Env_state.current_nodes ()) in + let nodes_str = String.concat " " (List.map (string_of_int) cnl) in + let node_msg = + if + (List.length cnl) = 1 + then + ("(current node is " ^ nodes_str ^ ").\n") + else + ("(current nodes are " ^ nodes_str ^ ").\n") + in + print_string ("*** The expression " ^ (Prevar.format vn) ^ + " is undefined at current step " ^ node_msg + ^ "*** You need to rewrite your environment" + ^ " spec in such a way that no pre is used" + ^ " for that variable at that step. \n" + ^ " "); + flush stdout; + exit 2 + ) + else + None + | _ -> assert false + ) + | _ -> assert false (****************************************************************************) @@ -251,7 +281,8 @@ and (* Used (by a Gne.fold) to add the condition [c] to every condition of a garded expression. *) let _ = assert ( - try let _ = Gne.find nexpr acc in + try + let _ = Gne.find nexpr acc in false with Not_found -> true ) @@ -508,21 +539,30 @@ and let rec (is_satisfiable: env_in -> formula -> bool) = fun input f -> -(* let _ = if Env_state.verbose () then *) -(* ( *) -(* print_string (formula_to_string f); *) -(* print_string " ...test whether this formula is satisfiable...\n"; *) -(* flush stdout *) -(* ) *) -(* in *) let (bdd, _) = formula_to_bdd input f in + let is_sat = not (Bdd.is_false bdd) && ( try let (n, m) = Env_state.sol_number bdd in not ((zero_sol, zero_sol) = (n, m)) - with Not_found -> true + with + Not_found -> true + | _ -> assert false + ) + in +(* if Env_state.verbose () then *) +(* ( *) +(* print_string "\n => "; *) +(* print_string (formula_to_string f); *) +(* if is_sat *) +(* then print_string "\n is satisfiable...\n" *) +(* else print_string "\n is not satisfiable...\n"; *) +(* flush stdout *) +(* ); *) + + is_sat @@ -658,7 +698,6 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t -> path in [bdd] leads to a satisfiable set of numeric constraints. *) - if Bdd.is_true bdd then @@ -676,7 +715,7 @@ let rec (draw_in_bdd: subst list * store -> Bdd.t -> Bdd.t -> draw_in_bdd_bool var (sl, store) bdd comb | EqZ(e) -> draw_in_bdd_eq e (sl, store) bdd comb - | Ineq(ineq) -> + | Ineq(ineq) -> draw_in_bdd_ineq ineq (sl, store) bdd comb @@ -742,15 +781,17 @@ and (draw_in_bdd_bool: string -> subst list * store -> Bdd.t -> Bdd.t -> *) try draw_in_bdd (sl1, store) bdd1 new_comb - with No_numeric_solution -> - if not (eq_sol_nb sol_nb2 zero_sol) - then draw_in_bdd (sl2, store) bdd2 new_comb - (* - The second branch is now tried because no path in - the first bdd leaded to a satisfiable set of - numeric constraints. - *) - else raise No_numeric_solution + with + No_numeric_solution -> + if not (eq_sol_nb sol_nb2 zero_sol) + then draw_in_bdd (sl2, store) bdd2 new_comb + (* + The second branch is now tried because no path in + the first bdd leaded to a satisfiable set of + numeric constraints. + *) + else raise No_numeric_solution + | _ -> assert false and (draw_in_bdd_ineq: Constraint.ineq -> subst list * store -> Bdd.t -> Bdd.t -> subst list * store) = @@ -814,6 +855,8 @@ and (draw_in_bdd_ineq: Constraint.ineq -> subst list * store -> Bdd.t -> Bdd.t - then try draw_in_bdd (sl, store1) bdd1 comb with No_numeric_solution -> call_choice_point () + | _ -> assert false + else call_choice_point () @@ -839,10 +882,11 @@ and (draw_in_bdd_eq: Ne.t -> subst list * store -> Bdd.t -> Bdd.t -> if ((eq_sol_nb n zero_sol) && (eq_sol_nb m zero_sol)) then raise No_numeric_solution ; in - let (store_plus_cstr, store_plus_not_cstr, store_plus_not_cstr2) = - split_store_eq store ne + let + (store_plus_cstr, store_plus_not_cstr, store_plus_not_cstr2) = + split_store_eq store ne in - let ( + let ( store1, bdd1, sol_nb1, store2, bdd2, sol_nb2, store3, bdd3, sol_nb3 @@ -887,7 +931,8 @@ and (draw_in_bdd_eq: Ne.t -> subst list * store -> Bdd.t -> Bdd.t -> (store_plus_not_cstr2, (Bdd.delse bdd), m, store_plus_cstr, (Bdd.dthen bdd), n, store_plus_not_cstr, (Bdd.delse bdd), m) - in + in + let call_choice_point3 _ = (* The third possibility is tried if no path is found in the 2 @@ -926,7 +971,10 @@ and (draw_in_bdd_eq: Ne.t -> subst list * store -> Bdd.t -> Bdd.t -> is_store_satisfiable store1 then try draw_in_bdd (sl, store1) bdd1 comb - with No_numeric_solution -> call_choice_point2 () + with + No_numeric_solution -> call_choice_point2 () + | _ -> assert false + else call_choice_point2 () @@ -937,9 +985,10 @@ and (draw_in_bdd_eq: Ne.t -> subst list * store -> Bdd.t -> Bdd.t -> (* exported *) let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) = fun bool_vars_to_gen num_vnt_to_gen comb bdd -> + (** Draw the output and local vars to be generated by the environnent. *) let (bool_subst_l, store) = - draw_in_bdd ([], (new_store num_vnt_to_gen)) bdd comb + draw_in_bdd ([], (new_store num_vnt_to_gen)) bdd comb in let num_subst_l = match Env_state.draw_mode () with @@ -985,16 +1034,19 @@ let (solve_formula: env_in -> int -> formula -> formula -> vnt list -> let _ = if Env_state.verbose () then ( + print_string "\n --> "; print_string (formula_to_string f); - print_string "\n"; + print_string "\n has been elected to be the formula in which solutions are drawn.\n"; flush stdout ) - in + in let bdd = (* The bdd of f has necessarily been computed (by is_satisfiable) *) try Env_state.bdd f with Not_found -> Env_state.bdd_global f + | _ -> assert false + in let (comb0, _) = formula_to_bdd input bool_vars_to_gen_f in let comb = @@ -1030,7 +1082,9 @@ let (solve_formula: env_in -> int -> formula -> formula -> vnt list -> in try Some(Util.unfold (draw bool_vars_to_gen num_vars_to_gen comb) bdd p) - with No_numeric_solution -> - Env_state.set_sol_number bdd (zero_sol, zero_sol); - None - + with + No_numeric_solution -> + Env_state.set_sol_number bdd (zero_sol, zero_sol); + None + | e -> + assert false diff --git a/test/time.exp b/test/time.exp index ecf3924..5af7990 100644 --- a/test/time.exp +++ b/test/time.exp @@ -1,15 +1,15 @@ Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 11.03 - System time (seconds): 0.09 - Percent of CPU this job got: 86% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.90 + User time (seconds): 11.12 + System time (seconds): 0.12 + Percent of CPU this job got: 94% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:11.92 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 258 + Major (requiring I/O) page faults: 281 Minor (reclaiming a frame) page faults: 2457 Voluntary context switches: 0 Involuntary context switches: 0 @@ -23,17 +23,17 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 23.43 - System time (seconds): 0.40 - Percent of CPU this job got: 88% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:26.91 + User time (seconds): 23.81 + System time (seconds): 0.36 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:25.40 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 258 + Major (requiring I/O) page faults: 262 Minor (reclaiming a frame) page faults: 17650 Voluntary context switches: 0 Involuntary context switches: 0 @@ -47,18 +47,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 100 50 50 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 51.85 - System time (seconds): 0.88 - Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:56.79 + User time (seconds): 52.36 + System time (seconds): 0.91 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:55.80 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 258 - Minor (reclaiming a frame) page faults: 37909 + Major (requiring I/O) page faults: 262 + Minor (reclaiming a frame) page faults: 38035 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -71,18 +71,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 3.58 - System time (seconds): 0.10 - Percent of CPU this job got: 82% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.48 + User time (seconds): 3.67 + System time (seconds): 0.09 + Percent of CPU this job got: 92% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.05 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 278 - Minor (reclaiming a frame) page faults: 2452 + Major (requiring I/O) page faults: 280 + Minor (reclaiming a frame) page faults: 2448 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -95,18 +95,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 8.57 - System time (seconds): 0.18 - Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.45 + User time (seconds): 8.42 + System time (seconds): 0.17 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.01 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 278 - Minor (reclaiming a frame) page faults: 7281 + Major (requiring I/O) page faults: 280 + Minor (reclaiming a frame) page faults: 7220 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -119,18 +119,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 3.05 - System time (seconds): 0.09 - Percent of CPU this job got: 81% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.84 + User time (seconds): 3.07 + System time (seconds): 0.04 + Percent of CPU this job got: 91% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.39 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 272 - Minor (reclaiming a frame) page faults: 2452 + Major (requiring I/O) page faults: 277 + Minor (reclaiming a frame) page faults: 2448 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -143,18 +143,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 10.21 - System time (seconds): 0.12 - Percent of CPU this job got: 81% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.66 + User time (seconds): 9.99 + System time (seconds): 0.20 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:10.71 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 272 - Minor (reclaiming a frame) page faults: 7678 + Major (requiring I/O) page faults: 276 + Minor (reclaiming a frame) page faults: 7674 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 diff --git a/test/time.res b/test/time.res index ecf3924..5af7990 100644 --- a/test/time.res +++ b/test/time.res @@ -1,15 +1,15 @@ Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 11.03 - System time (seconds): 0.09 - Percent of CPU this job got: 86% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.90 + User time (seconds): 11.12 + System time (seconds): 0.12 + Percent of CPU this job got: 94% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:11.92 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 258 + Major (requiring I/O) page faults: 281 Minor (reclaiming a frame) page faults: 2457 Voluntary context switches: 0 Involuntary context switches: 0 @@ -23,17 +23,17 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 23.43 - System time (seconds): 0.40 - Percent of CPU this job got: 88% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:26.91 + User time (seconds): 23.81 + System time (seconds): 0.36 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:25.40 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 258 + Major (requiring I/O) page faults: 262 Minor (reclaiming a frame) page faults: 17650 Voluntary context switches: 0 Involuntary context switches: 0 @@ -47,18 +47,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 100 50 50 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/tram.luc /home/jahier/lurette/test/usager.luc /home/jahier/lurette/test/porte.luc /home/jahier/lurette/test/passerelle.luc" - User time (seconds): 51.85 - System time (seconds): 0.88 - Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:56.79 + User time (seconds): 52.36 + System time (seconds): 0.91 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:55.80 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 258 - Minor (reclaiming a frame) page faults: 37909 + Major (requiring I/O) page faults: 262 + Minor (reclaiming a frame) page faults: 38035 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -71,18 +71,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 3.58 - System time (seconds): 0.10 - Percent of CPU this job got: 82% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.48 + User time (seconds): 3.67 + System time (seconds): 0.09 + Percent of CPU this job got: 92% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:04.05 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 278 - Minor (reclaiming a frame) page faults: 2452 + Major (requiring I/O) page faults: 280 + Minor (reclaiming a frame) page faults: 2448 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -95,18 +95,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_float.luc" - User time (seconds): 8.57 - System time (seconds): 0.18 - Percent of CPU this job got: 92% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.45 + User time (seconds): 8.42 + System time (seconds): 0.17 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:09.01 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 278 - Minor (reclaiming a frame) page faults: 7281 + Major (requiring I/O) page faults: 280 + Minor (reclaiming a frame) page faults: 7220 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -119,18 +119,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10000 1 1 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 3.05 - System time (seconds): 0.09 - Percent of CPU this job got: 81% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.84 + User time (seconds): 3.07 + System time (seconds): 0.04 + Percent of CPU this job got: 91% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:03.39 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 272 - Minor (reclaiming a frame) page faults: 2452 + Major (requiring I/O) page faults: 277 + Minor (reclaiming a frame) page faults: 2448 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 @@ -143,18 +143,18 @@ Exit status: 0 Command being timed: "/tmp/lurette56/lurette 10 100 100 --draw-inside -seed 1015403953 --no-oracle -o lurette.rif -ns2c -nlv /home/jahier/lurette/test/temp_int.luc" - User time (seconds): 10.21 - System time (seconds): 0.12 - Percent of CPU this job got: 81% - Elapsed (wall clock) time (h:mm:ss or m:ss): 0:12.66 + User time (seconds): 9.99 + System time (seconds): 0.20 + Percent of CPU this job got: 95% + Elapsed (wall clock) time (h:mm:ss or m:ss): 0:10.71 Average shared text size (kbytes): 0 Average unshared data size (kbytes): 0 Average stack size (kbytes): 0 Average total size (kbytes): 0 Maximum resident set size (kbytes): 0 Average resident set size (kbytes): 0 - Major (requiring I/O) page faults: 272 - Minor (reclaiming a frame) page faults: 7678 + Major (requiring I/O) page faults: 276 + Minor (reclaiming a frame) page faults: 7674 Voluntary context switches: 0 Involuntary context switches: 0 Swaps: 0 diff --git a/user-rules b/user-rules index 06d95d7..f5931be 100644 --- a/user-rules +++ b/user-rules @@ -107,11 +107,18 @@ test3: --do-not-show-step -ns2c -o heater_float.rif temp_float;\ rm -f test3.res; diff -u heater_float.rif.exp heater_float.rif > test3.res -test: test1 test2 test3 +test: clean_lib lib test1 test2 test3 ls -l test1.res test2.res test3.res +# the same as test, but does not remake libs, therefore assertions migth be unchecked +ltest: test1 test2 test3 + ls -l test1.res test2.res test3.res + +clean_lib: + pushd ~/lurette/source ; make -f Makefile.lurette_lib clean ; popd + lib: - pushd ~/lurette/source ; make -f Makefile.lurette_lib OCAMLFLAGS=""; popd + pushd ~/lurette/source ; make -f Makefile.lurette_lib OCAMLFLAGS=""; cp -f *.a ../lib; popd luc: pushd ~/lurette/source ; make -k dc -f Makefile.lucky OCAMLFLAGS=""; popd @@ -204,7 +211,8 @@ install-misc: cp *.cmi $(LUSTRE_MISC)/share/lurette/lib ; \ cp *.cmx $(LUSTRE_MISC)/share/lurette/lib ; \ cp lurette_lib.*a $(LUSTRE_MISC)/share/lurette/lib ;\ - cp ../ihm/xlurette/xlurette $(LUSTRE_MISC)/share/lurette/bin + cp ../VERSION/ $(LUSTRE_MISC)/share/lurette ;\ + cp ../ihm/xlurette/xlurette $(LUSTRE_MISC)/share/lurette/bin release: @@ -228,6 +236,7 @@ release: ../source/lurettetop.ml \ ../source/formula.mli ../source/formula.ml \ ../source/gne.mli ../source/gne.ml \ + ../source/prevar.mli ../source/prevar.ml \ ../source/ne.mli ../source/ne.ml \ ../source/parse_env.mli ../source/parse_env.ml \ ../source/env_state.mli ../source/env_state.ml \ -- GitLab