Some code refactoring

2 files changed, 49 insertions, 34 deletions

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<System.Tuple<string, Houdini.IAbstractDomain>>(new System.Tuple<string, Houdini.IAbstractDomain>[] {

-                  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<Houdini.HoudiniConst>()  as Houdini.IAbstractDomain),

-                  System.Tuple.Create("IA[ConstantProp]", new Houdini.IndependentAttribute<Houdini.ConstantProp>()  as Houdini.IAbstractDomain),

-                  System.Tuple.Create("IA[Intervals]", new Houdini.IndependentAttribute<Houdini.Intervals>()  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);

diff --git a/Source/Houdini/AbstractHoudini.cs b/Source/Houdini/AbstractHoudini.cs
index a730ec8f..6d7d67e7 100644
--- a/Source/Houdini/AbstractHoudini.cs
+++ b/Source/Houdini/AbstractHoudini.cs
@@ -225,6 +225,18 @@ namespace Microsoft.Boogie.Houdini {
             }

         }

 

+        public IEnumerable<Function> GetAssignment()

+        {

+            var ret = new List<Function>();

+            foreach (var func in existentialFunctions.Values)

+            {

+                var invars = new List<Expr>(func.InParams.OfType<Variable>().Select(v => Expr.Ident(v)));

+                func.Body = function2Value[func.Name].Gamma(invars);

+                ret.Add(func);

+            }

+            return ret;

+        }

+

         private void PrintFunction(Function function)

         {

             var tt = new TokenTextWriter(Console.Out);

@@ -1119,6 +1131,42 @@ namespace Microsoft.Boogie.Houdini {
             Debug.Assert(abstractDomainInstances.ContainsKey(Name));

             return abstractDomainInstances[Name] as IAbstractDomain;

         }

+

+        public static IAbstractDomain Initialize(string domainName)

+        {

+            // Declare abstract domains

+            var domains = new List<System.Tuple<string, IAbstractDomain>>(new System.Tuple<string, IAbstractDomain>[] {

+                  System.Tuple.Create("HoudiniConst", HoudiniConst.GetBottom() as IAbstractDomain),

+                  System.Tuple.Create("Intervals", new Intervals() as IAbstractDomain),

+                  System.Tuple.Create("ConstantProp", ConstantProp.GetBottom() as IAbstractDomain),

+                  System.Tuple.Create("PredicateAbs", new PredicateAbsElem() as IAbstractDomain),

+                  System.Tuple.Create("IA[HoudiniConst]", new IndependentAttribute<HoudiniConst>()  as IAbstractDomain),

+                  System.Tuple.Create("IA[ConstantProp]", new IndependentAttribute<ConstantProp>()  as IAbstractDomain),

+                  System.Tuple.Create("IA[Intervals]", new IndependentAttribute<Intervals>()  as IAbstractDomain)

+              });

+

+            domains.Iter(tup => AbstractDomainFactory.Register(tup.Item2));

+

+            // Find the abstract domain

+            IAbstractDomain domain = null;

+            foreach (var tup in domains)

+            {

+                if (tup.Item1 == domainName)

+                {

+                    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 AbsHoudiniInternalError("Domain not found");

+            }

+            return domain;

+        }

+

     }

 

     public interface IAbstractDomain

@@ -3559,10 +3607,6 @@ namespace Microsoft.Boogie.Houdini {
         }

     }

 

-    public class AbsHoudiniAssemblyLocator

-    {

-    }

-

     public class AbsHoudiniInternalError : System.ApplicationException

     {

         public AbsHoudiniInternalError(string msg) : base(msg) { }