summaryrefslogtreecommitdiff
path: root/main.ml
diff options
context:
space:
mode:
Diffstat (limited to 'main.ml')
-rw-r--r--main.ml29
1 files changed, 17 insertions, 12 deletions
diff --git a/main.ml b/main.ml
index f130b6c..0dc0408 100644
--- a/main.ml
+++ b/main.ml
@@ -8,6 +8,8 @@ open Num_domain
open Nonrelational
open Apron_domain
+open Abs_domain
+
open Enum_domain_edd
open Abs_interp_dynpart
@@ -16,23 +18,26 @@ module Interpret = Interpret.I
module ItvND = Apron_domain.ND_Box (* Nonrelational.ND(Intervals_domain.VD) *)
module PolyND = Apron_domain.ND_Poly
module OctND = Apron_domain.ND_Oct
+module ItvOND = NumDomainOnly(ItvND)
+module PolyOND = NumDomainOnly(PolyND)
+module OctOND = NumDomainOnly(OctND)
+module ItvEND = NumEnumDomain(Enum_domain.MultiValuation)(ItvND)
+module PolyEND = NumEnumDomain(Enum_domain.MultiValuation)(PolyND)
+module ItvENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(ItvND)
+module PolyENDEdd = NumEnumDomain(Enum_domain_edd.EDD)(PolyND)
module AI_Itv = Abs_interp.I(Enum_domain.MultiValuation)(ItvND)
module AI_Poly = Abs_interp.I(Enum_domain.MultiValuation)(PolyND)
module AI_Oct = Abs_interp.I(Enum_domain.MultiValuation)(OctND)
-module AI_Itv_EDD = Abs_interp_edd.I(ItvND)
-module AI_Poly_EDD = Abs_interp_edd.I(PolyND)
-module AI_Oct_EDD = Abs_interp_edd.I(OctND)
-
-module AI_S_Itv_DP = Abs_interp_dynpart.I
- (Enum_domain.MultiValuation)(ItvND)
-module AI_S_Rel_DP = Abs_interp_dynpart.I
- (Enum_domain.MultiValuation)(PolyND)
-module AI_EDD_Itv_DP = Abs_interp_dynpart.I
- (Enum_domain_edd.EDD)(ItvND)
-module AI_EDD_Rel_DP = Abs_interp_dynpart.I
- (Enum_domain_edd.EDD)(PolyND)
+module AI_Itv_EDD = Abs_interp_edd.I(ItvOND)
+module AI_Poly_EDD = Abs_interp_edd.I(PolyOND)
+module AI_Oct_EDD = Abs_interp_edd.I(OctOND)
+
+module AI_S_Itv_DP = Abs_interp_dynpart.I(ItvEND)
+module AI_S_Rel_DP = Abs_interp_dynpart.I(PolyEND)
+module AI_EDD_Itv_DP = Abs_interp_dynpart.I(ItvENDEdd)
+module AI_EDD_Rel_DP = Abs_interp_dynpart.I(PolyENDEdd)
(* command line options *)
let times = ref false