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

1 files changed, 6 insertions, 19 deletions

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