lurette 1.8 Wed, 22 Oct 2003 18:30:52 +0200 by jahier

Parent-Version:      1.7
Version-Log:

Implement a new drawing policy in polyhedron.

The idea is to base the base (which is not so expensive), and to draw
in othogonal hypercube that is as small as possible until a point in
the polyhedron is found.  However, it may happens in high dimension (>4)
that the volume of the cube is much bigger. In that case, after a few tries,
i call the old (unfair) method.

polyDram.ml/mli:
   new module containing all the thing related to the drawing inside
   a convex polyhedron.

   Give up the idea of random walk (not clear what should be the default
   step and length in big dimension).

Project-Description: Lurette

Makefile.common.source

@@ -12,28 +12,39 @@ OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
 
 LURETTE_PATH = $(HOME)/lurette
 
-SOURCES_LURETTE_LIB =  \
-	$(LURETTE_PATH)/source/util.ml \
+SOURCES_LURETTE_LIB =  $(LURETTE_PATH)/source/util.ml \
+        $(LURETTE_PATH)/source/genlex.mli $(LURETTE_PATH)/source/genlex.ml \
+        $(LURETTE_PATH)/source/lexeme.mli $(LURETTE_PATH)/source/lexeme.ml \
 	$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
 	$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
+        $(LURETTE_PATH)/source/polyDraw.mli  \
+        $(LURETTE_PATH)/source/polyDraw.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/lustreExp.mli $(LURETTE_PATH)/source/lustreExp.ml \
+	$(LURETTE_PATH)/source/parser.mly $(LURETTE_PATH)/source/lexer.mll \
 	$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
-	$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
-	$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
+	$(LURETTE_PATH)/source/parse_luc.mli $(LURETTE_PATH)/source/parse_luc.ml \
 	$(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
-	$(LURETTE_PATH)/source/draw.mli $(LURETTE_PATH)/source/draw.ml  \
 	$(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml  \
 	$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
+        $(LURETTE_PATH)/source/formula_to_bdd.mli  \
+        $(LURETTE_PATH)/source/formula_to_bdd.ml  \
+        $(LURETTE_PATH)/source/bddd.mli  \
+        $(LURETTE_PATH)/source/bddd.ml  \
+        $(LURETTE_PATH)/source/fair_bddd.mli  \
+        $(LURETTE_PATH)/source/fair_bddd.ml  \
 	$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
 	$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
 	$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml  \
 	$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
 	$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
-	$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml
+	$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
+	$(LURETTE_PATH)/source/lurette.ml
+
 
 ALL_SOURCES = $(SOURCES_LURETTE_LIB) $(SOURCES_OCAML)
 

TODO

@@ -10,6 +10,9 @@
  ->  if suffit de refaire en un env_try false 1 0 0 ....
 
 
+* quand une formule s'avere fausse du point de vue des variables 
+numeriques, il ne faut pas repartir du haut du graphe, mais backtraker
+depuis la branche qui s'avere fausse...
 
 * compilé en mode "assert", lurette se fait tuer par un signal 11 
   au bout d'une dizaine de pas...

lurette.prj

 ;; -*- Prcs -*-
 (Created-By-Prcs-Version 1 3 3)
 (Project-Description "Lurette")
-(Project-Version lurette 1 7)
-(Parent-Version lurette 1 6)
+(Project-Version lurette 1 8)
+(Parent-Version lurette 1 7)
 (Version-Log "
+Implement a new drawing policy in polyhedron.
 
-source/fair_bddd.ml: [new]
-source/fair_bddd.mli: [new]
-   The same as bddd, but taking polyhedron volume into account.
+The idea is to base the base (which is not so expensive), and to draw
+in othogonal hypercube that is as small as possible until a point in
+the polyhedron is found.  However, it may happens in high dimension (>4)
+that the volume of the cube is much bigger. In that case, after a few tries,
+i call the old (unfair) method.
 
-source/bddd.ml: 
-   It is useless to store both bdd and not bdd, because it is just
-   so easy to recompute the sol nb of not bdd (by switchinf the 
-   pair of sol numbers!).
+polyDram.ml/mli:
+   new module containing all the thing related to the drawing inside
+   a convex polyhedron.
 
+   Give up the idea of random walk (not clear what should be the default
+   step and length in big dimension).
 
 
-source/lurettetop.ml:
-source/lurette.ml:
-source/luc_exe.ml:
-   add a --compute-poly-volume option that makes lurette use
-   fair_bddd instead of bddd.
-
 
 ")
 (New-Version-Log ""
 )
-(Checkin-Time "Fri, 10 Oct 2003 14:01:43 +0200")
+(Checkin-Time "Wed, 22 Oct 2003 18:30:52 +0200")
 (Checkin-Login jahier)
 (Populate-Ignore ())
 (Project-Keywords)
@@ -38,7 +36,7 @@ source/luc_exe.ml:
 
 ;; Sources files for luc_exe
   (source/luc_exe.mli (lurette/b/31_ima_exe.ml 1.2 644))
-  (source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.37 644))
+  (source/luc_exe.ml (lurette/b/32_ima_exe.ml 1.38 644))
 
   (source/command_line_luc_exe.ml (lurette/b/33_command_li 1.19 644))
   (source/command_line_luc_exe.mli (lurette/b/34_command_li 1.12 644))
@@ -57,24 +55,24 @@ source/luc_exe.ml:
   (source/env.mli (lurette/15_env.mli 1.19 644))
   (source/env.ml (lurette/16_env.ml 1.33 644))
 
-  (source/util.ml (lurette/35_util.ml 1.56 644))
+  (source/util.ml (lurette/35_util.ml 1.57 644))
 
   (source/formula_to_bdd.ml (lurette/g/34_formula_to 1.1 644))
   (source/formula_to_bdd.mli (lurette/g/35_formula_to 1.2 644))
 
-  (source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.1 644))
-  (source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.1 644))
+  (source/fair_bddd.ml (lurette/g/38_fair_bddd. 1.2 644))
+  (source/fair_bddd.mli (lurette/g/39_fair_bddd. 1.2 644))
   (source/bddd.ml (lurette/g/36_bddd.ml 1.3 644))
   (source/bddd.mli (lurette/g/37_bddd.mli 1.3 644))
 
   (source/solver.mli (lurette/38_solver.mli 1.18 644))
   (source/solver.ml (lurette/39_solver.ml 1.56 644))
 
-  (source/polyhedron.ml (lurette/d/25_polyhedron 1.9 644))
-  (source/polyhedron.mli (lurette/d/26_polyhedron 1.4 644))
+  (source/polyhedron.ml (lurette/d/25_polyhedron 1.10 644))
+  (source/polyhedron.mli (lurette/d/26_polyhedron 1.5 644))
 
-  (source/store.mli (lurette/b/26_rnumsolver 1.20 644))
-  (source/store.ml (lurette/b/27_rnumsolver 1.28 644))
+  (source/store.mli (lurette/b/26_rnumsolver 1.21 644))
+  (source/store.ml (lurette/b/27_rnumsolver 1.29 644))
 
   (source/pnumsolver.ml (lurette/d/23_pnumsolver 1.2 644))
   (source/pnumsolver.mli (lurette/d/24_pnumsolver 1.2 644))
@@ -98,7 +96,7 @@ source/luc_exe.ml:
   (source/env_state.ml (lurette/51_env_state. 1.49 644))
 
   (source/automata.mli (lurette/b/46_automata.m 1.5 644))
-  (source/automata.ml (lurette/b/47_automata.m 1.14 644))
+  (source/automata.ml (lurette/b/47_automata.m 1.15 644))
 
   (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.7 644))
   (source/sim2chro.ml (lurette/b/24_sim2chro.m 1.20 644))
@@ -124,11 +122,11 @@ source/luc_exe.ml:
   (source/control.mli (lurette/c/3_control.ml 1.3 644))
   (source/control.ml (lurette/c/4_control.ml 1.5 644))
 
-  (source/constraint.mli (lurette/c/18_constraint 1.6 644))
-  (source/constraint.ml (lurette/c/19_constraint 1.8 644))
+  (source/constraint.mli (lurette/c/18_constraint 1.7 644))
+  (source/constraint.ml (lurette/c/19_constraint 1.9 644))
 
-  (source/ne.ml (lurette/c/21_ne.ml 1.9 644))
-  (source/ne.mli (lurette/c/22_ne.mli 1.7 644))
+  (source/ne.ml (lurette/c/21_ne.ml 1.10 644))
+  (source/ne.mli (lurette/c/22_ne.mli 1.8 644))
 
   (source/value.ml (lurette/c/23_value.ml 1.6 644))
   (source/value.mli (lurette/c/24_value.mli 1.4 644))
@@ -168,19 +166,19 @@ source/luc_exe.ml:
   (share/pixmaps/button-close.xpm (lurette/f/24_button-clo 1.1 644))
   (share/config.guess (lurette/f/25_config.gue 1.1 755))
   (share/configure.in (lurette/d/11_configure. 1.14 644))
-  (Makefile.common.source (lurette/e/33_Makefile.c 1.5 644))
+  (Makefile.common.source (lurette/e/33_Makefile.c 1.6 644))
   (OcamlMakefile (lurette/17_OcamlMakef 1.51 644))
   (share/Makefile.lurette.in (lurette/b/38_Makefile.l 1.27 644))
-  (user-rules (lurette/c/14_myrules 1.45 644))
+  (user-rules (lurette/c/14_myrules 1.46 644))
   (share/Makefile.test.in (lurette/c/25_user-rules 1.10 644))
   (Makefile (lurette/d/13_Makefile 1.4 644))
 
   (source/Makefile.lurettetop (lurette/d/14_Makefile.l 1.5 644))
   (source/Makefile.gen_fake_lutin (lurette/d/17_Makefile.g 1.4 644))
   (source/Makefile.show_luc (lurette/b/40_Makefile.s 1.11 644))
-  (source/Makefile.lucky (lurette/b/41_Makefile.i 1.25 644))
+  (source/Makefile.lucky (lurette/b/41_Makefile.i 1.26 644))
   (source/Makefile.gen_stubs (lurette/b/42_Makefile.g 1.8 644))
-  (source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.23 644))
+  (source/Makefile.lurette_lib (lurette/c/2_Makefile.l 1.24 644))
   (source/Makefile (lurette/c/20_Makefile 1.24 644))
 
 ;; Documentation
@@ -196,19 +194,19 @@ source/luc_exe.ml:
   (ID_EN_VRAC (lurette/0_ID_EN_VRAC 1.1 644))
   (INSTALL (lurette/f/26_INSTALL 1.2 744))
   (TAGS (lurette/21_TAGS 1.6 644))
-  (TODO (lurette/d/22_TODO 1.26 644))
+  (TODO (lurette/d/22_TODO 1.27 644))
   (share/lucky_init.csh.in (lurette/e/23_lucky_init 1.8 644))
   (share/lucky_init.sh.in (lurette/e/24_lucky_init 1.11 644))
 
   (share/gnuplot-rif (lurette/e/34_gnuplot-ri 1.5 744))
   (share/plot (lurette/e/35_plot 1.4 744))
 
-  (test/time-ossau.exp (lurette/b/48_time.exp 1.50 644))
-  (test/time-ossau.res (lurette/b/49_time.res 1.54 644))
-  (test/time-ecrins.res (lurette/d/20_time-ecrin 1.29 644))
-  (test/time-ecrins.exp (lurette/d/21_time-ecrin 1.28 644))
-  (test/time-moucherotte.exp (lurette/e/37_time-mouch 1.8 644))
-  (test/time-moucherotte.res (lurette/e/38_time-mouch 1.9 644))
+  (test/time-ossau.exp (lurette/b/48_time.exp 1.51 644))
+  (test/time-ossau.res (lurette/b/49_time.res 1.55 644))
+  (test/time-ecrins.res (lurette/d/20_time-ecrin 1.30 644))
+  (test/time-ecrins.exp (lurette/d/21_time-ecrin 1.29 644))
+  (test/time-moucherotte.exp (lurette/e/37_time-mouch 1.9 644))
+  (test/time-moucherotte.res (lurette/e/38_time-mouch 1.10 644))
 
 ;; Various files used for testing purposes
   (test/cudd_gc_problem.luc (lurette/e/29_cudd_gc_pr 1.2 644))
@@ -228,9 +226,9 @@ source/luc_exe.ml:
   (test/vrai_tram.lus (lurette/b/6_vrai_tram. 1.2 644))
 
   (test/test_losange.lus (lurette/f/27_test_losan 1.1 644))
-  (test/losange-3d2.luc (lurette/e/32_losange-3d 1.4 644))
+  (test/losange-3d2.luc (lurette/e/32_losange-3d 1.5 644))
   (test/onlyroll.lus (../demo-xlurette/Gyro/onlyroll.lus) :symlink)
-  (test/gyro.rif.exp (lurette/e/36_gyro.rif.e 1.5 644))
+  (test/gyro.rif.exp (lurette/e/36_gyro.rif.e 1.6 644))
   (test/giro.luc (../demo-xlurette/Gyro/giro.luc) :symlink)
   (test/allocator.lus (../demo-xlurette/Gyro/allocator.lus) :symlink)
 
@@ -294,7 +292,7 @@ source/luc_exe.ml:
 
   (test/losange.luc (lurette/d/27_losange.lu 1.2 644))
   (test/losange-3d.luc (lurette/d/28_losange-3d 1.4 644))
-  (test/losange-3d.rif.exp (lurette/e/31_losange-3d 1.4 644))
+  (test/losange-3d.rif.exp (lurette/e/31_losange-3d 1.5 644))
 
   (test/test7.rif.exp (lurette/g/12_test7.rif. 1.1 644))
   (test/infinite_weight.luc (lurette/g/13_infinite_w 1.1 644))
@@ -454,11 +452,6 @@ source/luc_exe.ml:
   (test/heater.lus (lurette/g/33_heater.lus 1.1 644))
 
 
-
-;; Files added by populate at Fri, 26 Sep 2003 09:12:12 +0200,
-;; to version 1.6(w), by jahier:
-
-
 ;; Files added by populate at Mon, 29 Sep 2003 09:41:23 +0200,
 ;; to version 1.6(w), by jahier:
 
@@ -472,7 +465,17 @@ source/luc_exe.ml:
 ;; Files added by populate at Wed, 01 Oct 2003 13:55:59 +0200,
 ;; to version 1.6(w), by jahier:
 
-  (test/losange-10d.luc (lurette/g/42_losange-10 1.1 644))
+  (test/losange-10d.luc (lurette/g/42_losange-10 1.2 644))
+
+;; Files added by populate at Fri, 17 Oct 2003 12:22:17 +0200,
+;; to version 1.7(w), by jahier:
+
+  (source/polyDraw.ml (lurette/g/43_polyDraw.m 1.1 644))
+
+;; Files added by populate at Fri, 17 Oct 2003 12:22:20 +0200,
+;; to version 1.7(w), by jahier:
+
+  (source/polyDraw.mli (lurette/g/44_polyDraw.m 1.1 644))
 )
 (Merge-Parents)
 (New-Merge-Parents)

source/Makefile.lucky

@@ -34,6 +34,8 @@ SOURCES_OCAML = \
           $(LURETTE_PATH)/source/lexeme.mli $(LURETTE_PATH)/source/lexeme.ml \
           $(LURETTE_PATH)/source/graph.mli  \
           $(LURETTE_PATH)/source/graph.ml \
+          $(LURETTE_PATH)/source/polyDraw.mli  \
+          $(LURETTE_PATH)/source/polyDraw.ml \
           $(LURETTE_PATH)/source/prevar.mli  \
           $(LURETTE_PATH)/source/prevar.ml \
           $(LURETTE_PATH)/source/command_line_luc_exe.mli  \

source/Makefile.lurette_lib

@@ -38,6 +38,8 @@ SOURCES = $(SOURCES_C) \
         $(LURETTE_PATH)/source/lexeme.mli $(LURETTE_PATH)/source/lexeme.ml \
 	$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
 	$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
+        $(LURETTE_PATH)/source/polyDraw.mli  \
+        $(LURETTE_PATH)/source/polyDraw.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 \

source/automata.ml

@@ -154,7 +154,7 @@ let show_automata str a =
 
 (**
    The resulting automaton should not contain any cycle (which would be useless
-   anyway) otherwise I would loop^during ther draw.
+   anyway) otherwise I would loop during the draw.
    
    Moreover, the automaton should not be a dag, otherwise, I am into trouble 
    whenever I want to remove a path that leaded to an unsatisfiable formula.

source/constraint.ml

@@ -98,7 +98,13 @@ let (apply_substl : Ne.subst list -> t -> t) =
       | EqZ(ne)  -> EqZ(Ne.apply_substl s ne)
 
 
-
+(* exported *)
+let (eval_ineq : Formula.num_subst list -> ineq ->  bool) =
+  fun s ineq -> 
+    match ineq with
+	GZ(ne)   -> Value.num_sup_zero(Ne.eval ne s)
+      | GeqZ(ne) -> Value.num_supeq_zero(Ne.eval ne s)
+    
 
 
 (* exported *)
@@ -110,8 +116,8 @@ let (get_vars_ineq : ineq -> string list) =
 
 (* exported *)
 let (get_vars : t -> string list) =
-  fun ineq -> 
-    match ineq with
+  fun cstr -> 
+    match cstr with
 	Bv vn -> [vn.n]
       | EqZ ne -> Ne.get_vars ne
       | Ineq ineq   -> get_vars_ineq ineq

source/constraint.mli

@@ -49,3 +49,4 @@ val opp_ineq : ineq -> ineq
 val to_string : t -> string
 val ineq_to_string : ineq -> string
 
+val eval_ineq : Formula.num_subst list -> ineq ->  bool

source/fair_bddd.ml

@@ -90,7 +90,6 @@ let (init_snt : unit -> unit) =
 let (clear_snt: unit -> unit) =
   fun _ -> 
     Hashtbl.clear !snt_ref;
-    Hashtbl.clear !(Store.store_volume);
     init_snt ()
 
 let (sol_number_exists : Bdd.t -> Store.t -> snt -> bool) =

source/fair_bddd.mli

@@ -66,7 +66,7 @@ val clear_snt : unit -> unit
 
 
 val draw_in_bdd :  Formula.var list -> Bdd.t -> Bdd.t -> 
-  Formula.subst list * Store.t' * Store.p
+  Formula.subst list * Store.t' * Store.p 
 (** 
   [draw_in_bdd varl bdd comb] returns a draw of the Boolean variables
   as well as a range base and a polyhedron based representation of 

source/luc_exe.ml

@@ -527,8 +527,9 @@ try main () with e ->
 
 
 
-print_string "\n";;
+(* output_string stderr ("\n cpt = " ^ (string_of_int !(Store.cpt)) ^ "/" ^ (string_of_int !(Store.cpt2)) ^ "\n") ;; *)
 
+print_string "\n";;
 
 (* let _ = Callback.register "lurette_main" main;; *)
 

source/ne.ml

@@ -367,6 +367,24 @@ let (get_vars : t -> string list) =
        []
     )
 
+
+(* exported *)
+let (eval : t -> Formula.num_subst list -> num) =
+  fun ne s -> 
+    let acc0 = match (snd (List.hd s)) with I _ -> I 0 | F _ ->  F 0.0 in
+      (StringMap.fold
+	 (fun vn v acc -> 
+	    if 
+	      vn = "" 
+	    then 
+	      Value.add_num acc v 
+	    else
+	      Value.add_num acc (Value.mult_num v (List.assoc vn s))
+	 )
+	 ne
+	 acc0
+      )
+
 (****************************************************************************)
 
 

source/ne.mli

@@ -74,3 +74,4 @@ val substl_to_string : subst list -> string
 val to_string_gen : (Value.num -> string) -> string -> t -> string
 val to_string : t -> string
 val print : t -> unit
+val eval : t -> Formula.num_subst list -> Value.num

source/polyDraw.mli

+(*-----------------------------------------------------------------------
+** Copyright (C) 2003 - Verimag.
+** This file may only be copied under the terms of the GNU Library General
+** Public License 
+**-----------------------------------------------------------------------
+**
+** File: polyDraw.mli
+** Main author: jahier@imag.fr
+*)
+
+(** implement an algorithm to draw uniformally in a convex polyhedron *)
+
+
+type point = float list
+type vector = float list
+
+val print_points : point list -> unit
+
+val scal_prod : vector -> vector -> float
+val vect_norm : vector -> float
+
+(** returns the cooedinate of the smallest hypercube containing a
+  convex Polyhedron defined by a set of generators *)
+val hypercube : point list -> (float * float) list
+
+
+
+type parallelogram
+(**  parallelogram envelopping a convex Polyhedron defined by
+  a set of generators.
+*)
+
+val compute_parellelogram : point list -> parallelogram 
+
+(** Draw one point in a parallelogram. *)
+val one_point_parellelogram : parallelogram -> point
+
+(** Draw n points in a parallelogram. *)
+val n_points_parellelogram : parallelogram -> int -> point list
+
+
+
+(** This one is cheaper, but a little bit unfair (i.e., not uniform) *)
+val draw_point_cheap : point list -> point
+
+
+(** draw n points among pl (any point may be drawn several times) *)
+
+val draw_n_distinc_points : int -> point list -> point list
+val draw_n_points : int -> point list -> point list
+val parallelogram_volume : parallelogram -> float

source/polyhedron.ml

@@ -12,6 +12,7 @@ open Formula
 open Constraint
 open Value
 open Util
+open PolyDraw
 
 module StringSet = struct
    include Set.Make(struct type t = string let compare = compare end)
@@ -193,9 +194,11 @@ let polka_init = ref 100
 let poly_cache_tbl = Hashtbl.create 1
 
 
-let rec (build_poly_list_from_delayed_cstr : 
-	   range Util.StringMap.t -> Constraint.ineq list -> range Util.StringMap.t *
-	     var_name list * (Formula.vnt list * Poly.t * (int -> string)) list) =
+let rec (build_poly_list_from_delayed_cstr : range Util.StringMap.t -> 
+  Constraint.ineq list -> 
+    range Util.StringMap.t *
+    var_name list * 
+    (Formula.vnt list * Poly.t * (int -> string) * Constraint.ineq list) list ) =
   fun tbl delayed ->
     try
       Hashtbl.find poly_cache_tbl (tbl, delayed)
@@ -238,10 +241,11 @@ let rec (build_poly_list_from_delayed_cstr :
 		   0
 	       in
 	       let (name_to_rank : string -> int) = Hashtbl.find rank_of_name_tbl
-	       and (rank_to_name : int -> string) = Hashtbl.find name_of_rank_tbl in
-	       let (vntl0, poly0) =
+	       and (rank_to_name : int -> string) = Hashtbl.find name_of_rank_tbl 
+	       in
+	       let (vntl0, poly0, cl_init) =
 		 StringSet.fold 
-		   (fun  var (vntl, poly)-> 
+		   (fun  var (vntl, poly, cl_init)-> 
 		      (* 
 			 Add the constraint present in tbl to the polyhedron 
 			 for each variables in [vars_of_cl] 
@@ -285,11 +289,12 @@ let rec (build_poly_list_from_delayed_cstr :
 		      in
 			(
 			  vnt::vntl,
-			  Poly.add_constraint (Poly.add_constraint poly v1) v2
+			  Poly.add_constraint (Poly.add_constraint poly v1) v2,
+			  ineq_min::ineq_max::cl_init
 			)
 		   )
 		   vars_of_cl
-		   ([], (Poly.universe dim))
+		   ([], (Poly.universe dim), [])
 	       in
 	       let poly1 =
 		 List.fold_left 
@@ -303,7 +308,7 @@ let rec (build_poly_list_from_delayed_cstr :
 		   poly0
 		   cl
 	       in
-		 (vntl0, poly1, rank_to_name)
+		 (vntl0, poly1, rank_to_name, List.rev_append cl cl_init)
 	    )
 	    cll
 	in
@@ -328,19 +333,6 @@ let rec (build_poly_list_from_delayed_cstr :
 
 type point = float list
 
-let (point_to_vector : point -> Vector.t) =
-  fun point -> 
-    let row = Vector.make ((List.length point) + 3) in
-    let i = ref 3 in
-    let denom = 1.0 /. !(Util.eps) in
-    let point_int = List.map (fun p -> int_of_float (p *. denom)) point in 
-      Vector.set row 0 1; (* it is not a line *)
-      Vector.set row 1 (int_of_float denom); 
-      Vector.set row 2 0; (* this is the epsilon dimension *) 
-      List.iter
-	(fun p -> Vector.set row !i p; i:=!i+1)
-	point_int;
-      row
 
 
 
@@ -414,7 +406,6 @@ let (get_vertices : Poly.t ->  (int -> string) -> point list) =
 		   (fun l -> (List.hd l) = 0.) 
 		   generators
 		)
-(* 	      generators *)
 	| None -> assert false 
 
 
@@ -424,49 +415,63 @@ let (get_vertices : Poly.t ->  (int -> string) -> point list) =
 (****************************************************************************)
 
 
+let (point_to_vector : point -> Vector.t) =
+  fun point -> 
+    let row = Vector.make ((List.length point) + 3) in
+    let denom = 1.0 /. !(Util.eps) in
+    let point_int = List.map (fun p -> int_of_float (p *. denom)) point in 
+    let i = ref 3 in
+      Vector.set row 0 1; (* it is not a line *)
+      Vector.set row 1 (int_of_float denom); 
+      Vector.set row 2 0; (* this is the epsilon dimension *) 
+      List.iter
+	(fun p -> Vector.set row !i p; i:=!i+1)
+	point_int;
+      row
+
+(* let (point_is_in_poly : point -> Poly.t -> bool) = *)
+(*   fun p poly ->  *)
+(*     let v = point_to_vector p in *)
+(*       Poly.is_generator_included_in v poly  *)
+
+
+
+(* exported *)
+let (point_is_in_poly : point -> (int -> string) -> Constraint.ineq list -> bool) =
+  fun p r2n cstrl ->
+    let s = 
+      snd (List.fold_left 
+	     (fun (i, acc) x -> (i+1,(r2n i, F x)::acc))
+	     (0, []) 
+	     p) 
+    in 
+      List.for_all (Constraint.eval_ineq s) cstrl 
+
 let (volume: Poly.t -> (int -> string) -> float) =
   fun poly r2n ->
-    (* Really perform that computation it required by an option 
-       --compute-poly-vol ? 
-    *)
   let pl = get_vertices poly r2n in
-  let (unit_cube : (float * float) list) = 
-    (* I could deforest this one ... *)
-    List.combine
-      (List.fold_left (fun acc p -> List.map2 min p acc) (List.hd pl) (List.tl pl))
-      (List.fold_left (fun acc p -> List.map2 max p acc) (List.hd pl) (List.tl pl))
-  in
-  let (draw_one_point : (float * float) list -> float list) =
-    List.map (fun (min, max) -> min +. (Random.float (max -. min +. !(Util.eps))))
-  in
-  let ni = 1000 in
-  let nf = float_of_int ni in
-  let random_points = Util.unfold draw_one_point unit_cube ni in
-  let pertencage_in = 
-    max
-      1. (* even if no points appear to be in [poly], at least we pretend 
-	   that the volume of poly is 1% the volume of the unit cube. *)
-      (List.fold_left 
-	 (fun cpt p -> 
-	    let v = point_to_vector p in
-	      if 
-		Poly.is_generator_included_in v poly 
-	      then 
-		  cpt +. 1.
-	      else 
-		  cpt
-	 )
-	 0.
-	 random_points
-      )
-  in
-  let unit_cube_volume = 
-    List.fold_left 
-      (fun acc (min, max) -> (max -. min +. !(Util.eps)) *. acc) 
-      1.0 
-      unit_cube
+  let paral = PolyDraw.compute_parellelogram pl in
+  let parallogram_vol = PolyDraw.parallelogram_volume paral in 
+
+(*   let ni = 100 in *)
+(*   let nf = float_of_int ni in *)
+(*   let random_points = PolyDraw.n_points_parellelogram o vl ni in *)
+(*   let pertencage_in =  *)
+(*     max *)
+(*       1. (* even if no points appear to be in [poly], at least we pretend  *)
+(* 	   that the volume of poly is 1% the volume of the unit cube. *) *)
+(*       (List.fold_left  *)
+(* 	 (fun cpt p -> if point_is_in_poly p poly then cpt +. 1. else cpt) *)
+(* 	 0. *)
+(* 	 random_points *)
+(*       ) *)
+(*   in *)
+    
+  (* The volume of the parallelogram is not a so bad approximation after all *)
+  let volume = 
+    parallogram_vol 
+(*     *. (pertencage_in /. nf)  *)
   in
-  let volume = unit_cube_volume *. (pertencage_in /. nf) in
 (*     print_string ( *)
 (*       " " ^ (string_of_float (pertencage_in /. nf *. 100.0)) ^ "  "); *)
 (*     flush stdout; *)

source/polyhedron.mli

@@ -31,8 +31,8 @@ val build_poly_list_from_delayed_cstr :
   range Util.StringMap.t -> Constraint.ineq list -> 
       ( range Util.StringMap.t 
       * Formula.var_name list 
-      * (Formula.vnt list * Poly.t * (int -> string)) list)
-
+      * (Formula.vnt list * Poly.t * (int -> string) * Constraint.ineq list) list)
+      
 
 type point = float list
 
@@ -42,3 +42,5 @@ val get_vertices : Poly.t ->  (int -> string) -> point list
 (** Returns the volume (approximation) of a Polyhedron using
   a monte-carlo like method. *)
 val volume : Poly.t -> (int -> string) -> float
+
+val point_is_in_poly : point -> (int -> string) -> Constraint.ineq list -> bool

source/store.mli

@@ -99,4 +99,5 @@ val get_all_vertices : t' -> p -> Formula.num_subst list ->
   (** returns the solutions corresponding to the vertices of the solution 
     hull contained in [s]. *)