From 4428ac1f7e5520a23d256638c98c9570bd943169 Mon Sep 17 00:00:00 2001 From: akashlal Date: Fri, 3 May 2013 11:07:05 +0530 Subject: Some code refactoring --- Source/BoogieDriver/BoogieDriver.cs | 31 +------------------------------ 1 file changed, 1 insertion(+), 30 deletions(-) (limited to 'Source/BoogieDriver') diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index c12ba47d..52e3c3fc 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -656,36 +656,7 @@ namespace Microsoft.Boogie { CommandLineOptions.Clo.ModelViewFile = "z3model"; CommandLineOptions.Clo.UseArrayTheory = true; CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic; - // Declare abstract domains - var domains = new List>(new System.Tuple[] { - System.Tuple.Create("HoudiniConst", Houdini.HoudiniConst.GetBottom() as Houdini.IAbstractDomain), - System.Tuple.Create("Intervals", new Houdini.Intervals() as Houdini.IAbstractDomain), - System.Tuple.Create("ConstantProp", Houdini.ConstantProp.GetBottom() as Houdini.IAbstractDomain), - System.Tuple.Create("PredicateAbs", new Houdini.PredicateAbsElem() as Houdini.IAbstractDomain), - System.Tuple.Create("IA[HoudiniConst]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), - System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain), - System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute() as Houdini.IAbstractDomain) - }); - - domains.Iter(tup => Houdini.AbstractDomainFactory.Register(tup.Item2)); - - // Find the abstract domain - Houdini.IAbstractDomain domain = null; - foreach (var tup in domains) - { - if (tup.Item1 == CommandLineOptions.Clo.AbstractHoudini) - { - domain = tup.Item2; - break; - } - } - if (domain == null) - { - Console.WriteLine("Domain {0} not found", CommandLineOptions.Clo.AbstractHoudini); - Console.WriteLine("Supported domains are:"); - domains.Iter(tup => Console.WriteLine(" {0}", tup.Item1)); - throw new Houdini.AbsHoudiniInternalError("Domain not found"); - } + var domain = Houdini.AbstractDomainFactory.Initialize(CommandLineOptions.Clo.AbstractHoudini); // Run Abstract Houdini var abs = new Houdini.AbsHoudini(program, domain); -- cgit v1.2.3