Isolate numerical part of domain. Next: isolate numerical part of equations.

7 files changed, 124 insertions, 51 deletions

diff --git a/abstract/abs_domain.ml b/abstract/abs_domain.ml
new file mode 100644
index 0000000..ddc34ab
--- /dev/null
+++ b/abstract/abs_domain.ml
@@ -0,0 +1,88 @@
+open Ast
+open Formula
+open Num_domain
+open Typing
+
+module type ENVIRONMENT_DOMAIN = sig
+    type t
+    type itv
+
+    (* construction *)
+    val init              : t
+    val bottom            : t
+    val vbottom           : t -> t      (* bottom value with same environment *)
+    val is_bot            : t -> bool
+
+    (* variable management *)
+    val addvar            : t -> id -> Typing.typ -> t
+    val rmvar             : t -> id -> t
+    val vars              : t -> (id * Typing.typ) list
+
+    val forgetvar         : t -> id -> t
+    val var_itv           : t -> id -> itv
+
+    (* set_theoretic operations *)
+    val join              : t -> t -> t   (* union *)
+    val meet              : t -> t -> t   (* intersection *)
+    val widen             : t -> t -> t
+
+    val subset            : t -> t -> bool
+    val eq                : t -> t -> bool
+
+    (* abstract operations *)
+    val apply_f           : t -> bool_expr -> t
+    val apply_cl          : t -> conslist -> t
+    val assign            : t -> (id * num_expr) list -> t
+
+    (* pretty-printing *)
+    val print_vars  : Format.formatter -> t -> id list -> unit
+    val print_all   : Format.formatter -> t -> unit
+    val print_itv   : Format.formatter -> itv -> unit
+
+end
+
+module D (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+
+    type t = ND.t
+    type itv = ND.itv
+
+    let init = ND.init
+    let bottom = ND.bottom
+    let vbottom = ND.vbottom
+    let is_bot = ND.is_bot
+
+    let addvar x id ty = ND.addvar x id (ty = TReal)
+    let rmvar = ND.rmvar
+    let vars x = List.map (fun (id, r) -> id, if r then TReal else TInt) (ND.vars x)
+
+    let forgetvar = ND.forgetvar
+    let var_itv = ND.var_itv
+
+    let join = ND.join
+    let meet = ND.meet
+    let widen = ND.widen
+
+    let subset = ND.subset
+    let eq = ND.eq
+
+    let rec apply_cl x (cons, rest) = match rest with
+        | CLTrue ->
+          ND.apply_ncl x cons
+        | CLFalse -> vbottom x
+        | CLAnd(a, b) ->
+          let y = apply_cl x (cons, a) in
+          apply_cl y (cons, b)
+        | CLOr((ca, ra), (cb, rb)) ->
+          let y = apply_cl x (cons@ca, ra) in
+          let z = apply_cl x (cons@cb, rb) in
+          join y z
+
+    let apply_f x f = apply_cl x (conslist_of_f f)
+
+    let assign = ND.assign
+
+    let print_vars = ND.print_vars
+    let print_all = ND.print_all
+    let print_itv = ND.print_itv
+
+end
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index c621734..1d3e20a 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -4,7 +4,8 @@ open Formula
 open Typing
 
 open Util
-open Environment_domain
+open Abs_domain
+open Num_domain
 
 module I (E : ENVIRONMENT_DOMAIN) : sig
 
@@ -36,8 +37,7 @@ end = struct
       let cl_g = Formula.conslist_of_f f_g in
 
       let env = List.fold_left
-        (fun env (_, id, ty) ->
-          E.addvar env id (ty = TReal))
+        (fun env (_, id, ty) -> E.addvar env id ty)
         E.init
         rp.all_vars
       in
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index cef6b66..369f4b7 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -2,11 +2,11 @@ open Formula
 open Ast
 
 open Util
-open Environment_domain
+open Num_domain
 
 open Apron
 
-module D : ENVIRONMENT_DOMAIN = struct
+module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
 
     (* manager *)
     type man = Polka.loose Polka.t
@@ -93,27 +93,14 @@ module D : ENVIRONMENT_DOMAIN = struct
         Abstract1.bound_variable manager x (Var.of_string id)
 
     (* Apply some formula to the environment *)
-    let rec apply_cl x (cons, rest) =
+    let rec apply_ncl x cons =
         let env = Abstract1.env x in
         let tca = Array.of_list (List.map (tcons_of_cons env) cons) in
         let ar = Tcons1.array_make env (Array.length tca) in
         Array.iteri (Tcons1.array_set ar) tca;
-        let y = Abstract1.meet_tcons_array manager x ar in
-        apply_cl_r y rest
-
-    and apply_cl_r x = function
-        | CLTrue -> x
-        | CLFalse -> vbottom x
-        | CLAnd(a, b) ->
-          let y = apply_cl_r x a in
-          apply_cl_r y b
-        | CLOr(a, b) ->
-          let y = apply_cl x a in
-          let z = apply_cl x b in
-          Abstract1.join manager y z
-
-    let apply_f x f = apply_cl x (conslist_of_f f)
-    
+        Abstract1.meet_tcons_array manager x ar
+
+
     let assign x eqs =
       let env = Abstract1.env x in
       let vars = Array.of_list
diff --git a/abstract/domain.ml b/abstract/domain.ml
new file mode 100644
index 0000000..76635d1
--- /dev/null
+++ b/abstract/domain.ml
@@ -0,0 +1,3 @@
+open Ast
+open Formula
+
diff --git a/abstract/formula.ml b/abstract/formula.ml
index f3c1df1..a598750 100644
--- a/abstract/formula.ml
+++ b/abstract/formula.ml
@@ -2,6 +2,9 @@ open Ast
 
 (* AST for logical formulas *)
 
+
+(* Numerical part *)
+
 type num_expr =
   (* constants *)
   | NIntConst of int
@@ -12,6 +15,13 @@ type num_expr =
   (* identifier *)
   | NIdent of id
 
+type num_cons_op =
+  | CONS_EQ | CONS_NE
+  | CONS_GT | CONS_GE
+type num_cons = num_expr * num_cons_op  (* always imply right member = 0 *)
+
+
+(* Logical part *)
 
 type bool_expr =
   (* constants *)
@@ -24,7 +34,6 @@ type bool_expr =
   | BOr of bool_expr * bool_expr
   | BNot of bool_expr
 
-
 let f_and a b = match a, b with
   | BConst false, _ | _, BConst false -> BConst false
   | BConst true, b -> b
@@ -67,17 +76,14 @@ and eliminate_not_negate = function
   | BOr(a, b) ->
     BAnd(eliminate_not_negate a, eliminate_not_negate b)
 
+
+
 (*
   In big ANDs, try to separate levels of /\ and levels of \/
   We also use this step to simplify trues and falses that may be present.
 *)
 
-type cons_op =
-  | CONS_EQ | CONS_NE
-  | CONS_GT | CONS_GE
-type cons = num_expr * cons_op  (* always imply right member = 0 *)
-
-type conslist = cons list * conslist_bool_expr
+type conslist = num_cons list * conslist_bool_expr
 and conslist_bool_expr =
   | CLTrue
   | CLFalse
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 855f970..492b547 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -3,13 +3,13 @@ open Util
 open Ast
 
 open Value_domain
-open Environment_domain
+open Num_domain
 
 let debug = false
 
 (* Restricted domain, only support integers *)
 
-module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
+module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
     type env = V.t VarMap.t
 
     type t = Env of env | Bot
@@ -167,20 +167,9 @@ module D (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct
         List.fold_left restrict_var env
           (extract_var (expr, zop, NIntConst 0))
 
-    let rec apply_cl x (cons, rest) = match rest with
-        | CLTrue ->
-          let apply_cl_l x = List.fold_left apply_cons x cons in
-          fix eq apply_cl_l x
-        | CLFalse -> vbottom x
-        | CLAnd(a, b) ->
-          let y = apply_cl x (cons, a) in
-          apply_cl y (cons, b)
-        | CLOr((ca, ra), (cb, rb)) ->
-          let y = apply_cl x (cons@ca, ra) in
-          let z = apply_cl x (cons@cb, rb) in
-          join y z
-
-    let apply_f x f = apply_cl x (conslist_of_f f)
+    let apply_ncl x cl =
+        let f x = List.fold_left apply_cons x cl in
+        fix eq f x
 
     (* Assignment *)
     let assign x exprs =
diff --git a/abstract/environment_domain.ml b/abstract/num_domain.ml
index 6e84c75..59ed1a0 100644
--- a/abstract/environment_domain.ml
+++ b/abstract/num_domain.ml
@@ -1,21 +1,22 @@
 open Ast
 open Formula
 
-module type ENVIRONMENT_DOMAIN = sig
+module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
     type t
     type itv
 
     (* construction *)
     val init        : t
     val bottom      : t
+    val vbottom     : t -> t       (* bottom value with same environment *)
     val is_bot      : t -> bool
 
     (* variable management *)
-    val addvar      : t -> id -> bool -> t     (* integer or float variable ? *)
-    val forgetvar   : t -> id -> t             (* remove var from constraints *)
+    val addvar      : t -> id -> bool -> t     (* integer or real variable ? *)
     val rmvar       : t -> id -> t
     val vars        : t -> (id * bool) list
-    val vbottom     : t -> t       (* bottom value with same environment *)
+
+    val forgetvar   : t -> id -> t             (* remove var from constraints *)
     val var_itv     : t -> id -> itv
 
     (* set-theoretic operations *)
@@ -28,8 +29,7 @@ module type ENVIRONMENT_DOMAIN = sig
     val eq          : t -> t -> bool
 
     (* abstract operation *)
-    val apply_f     : t -> bool_expr -> t
-    val apply_cl    : t -> conslist -> t
+    val apply_ncl   : t -> num_cons list -> t
     val assign      : t -> (id * num_expr) list -> t
 
     (* pretty-printing *)