Worked on the parallelization.

4 files changed, 162 insertions, 116 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 9f82fd4a..fa41173b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -59,22 +59,8 @@ namespace Microsoft.Boogie.SMTLib
       this.gen = gen;

       this.usingUnsatCore = false;

 

-      TypeAxiomBuilder axBuilder;

-      switch (CommandLineOptions.Clo.TypeEncodingMethod) {

-        case CommandLineOptions.TypeEncoding.Arguments:

-          axBuilder = new TypeAxiomBuilderArguments(gen);

-          axBuilder.Setup();

-          break;

-        case CommandLineOptions.TypeEncoding.Monomorphic:

-          axBuilder = new TypeAxiomBuilderPremisses(gen);

-          break;

-        default:

-          axBuilder = new TypeAxiomBuilderPremisses(gen);

-          axBuilder.Setup();

-          break;

-      }

+      SetupAxiomBuilder(gen);

 

-      AxBuilder = axBuilder;

       Namer = new SMTLibNamer();

       ctx.parent = this;

       this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);

@@ -97,6 +83,24 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    private void SetupAxiomBuilder(VCExpressionGenerator gen)

+    {

+      switch (CommandLineOptions.Clo.TypeEncodingMethod)

+      {

+        case CommandLineOptions.TypeEncoding.Arguments:

+          AxBuilder = new TypeAxiomBuilderArguments(gen);

+          AxBuilder.Setup();

+          break;

+        case CommandLineOptions.TypeEncoding.Monomorphic:

+          AxBuilder = new TypeAxiomBuilderPremisses(gen);

+          break;

+        default:

+          AxBuilder = new TypeAxiomBuilderPremisses(gen);

+          AxBuilder.Setup();

+          break;

+      }

+    }

+

     ProcessStartInfo ComputeProcessStartInfo()

     {

       var path = this.options.ProverPath;

@@ -149,7 +153,7 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

-    internal readonly TypeAxiomBuilder AxBuilder;

+    internal TypeAxiomBuilder AxBuilder { get; private set; }

     internal readonly UniqueNamer Namer;

     readonly TypeDeclCollector DeclCollector;

     SMTLibProcess Process;

@@ -218,103 +222,103 @@ namespace Microsoft.Boogie.SMTLib
 

     private void PrepareCommon()

     {

-        if (common.Length == 0)

+      if (common.Length == 0)

+      {

+        SendCommon("(set-option :print-success false)");

+        SendCommon("(set-info :smt-lib-version 2.0)");

+        if (options.ProduceModel())

+          SendCommon("(set-option :produce-models true)");

+        foreach (var opt in options.SmtOptions)

         {

-            SendCommon("(set-option :print-success false)");

-            SendCommon("(set-info :smt-lib-version 2.0)");

-            if (options.ProduceModel())

-                SendCommon("(set-option :produce-models true)");

-            foreach (var opt in options.SmtOptions)

-            {

-                SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

-            }

+          SendCommon("(set-option :" + opt.Option + " " + opt.Value + ")");

+        }

 

-            if (!string.IsNullOrEmpty(options.Logic))

-            {

-                SendCommon("(set-logic " + options.Logic + ")");

-            }

+        if (!string.IsNullOrEmpty(options.Logic))

+        {

+          SendCommon("(set-logic " + options.Logic + ")");

+        }

+

+        SendCommon("; done setting options\n");

+        SendCommon(_backgroundPredicates);

 

-            SendCommon("; done setting options\n");

-            SendCommon(_backgroundPredicates);

+        if (options.UseTickleBool)

+        {

+          SendCommon("(declare-fun tickleBool (Bool) Bool)");

+          SendCommon("(assert (and (tickleBool true) (tickleBool false)))");

+        }

 

-            if (options.UseTickleBool)

+        if (ctx.KnownDatatypeConstructors.Count > 0)

+        {

+          GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();

+          foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys)

+          {

+            dependencyGraph.AddSource(datatype);

+            foreach (Function f in ctx.KnownDatatypeConstructors[datatype])

             {

-                SendCommon("(declare-fun tickleBool (Bool) Bool)");

-                SendCommon("(assert (and (tickleBool true) (tickleBool false)))");

+              List<CtorType> dependentTypes = new List<CtorType>();

+              foreach (Variable v in f.InParams)

+              {

+                FindDependentTypes(v.TypedIdent.Type, dependentTypes);

+              }

+              foreach (CtorType result in dependentTypes)

+              {

+                dependencyGraph.AddEdge(datatype, result);

+              }

             }

-

-            if (ctx.KnownDatatypeConstructors.Count > 0)

+          }

+          GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType>(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);

+          sccs.Compute();

+          foreach (GraphUtil.SCC<CtorType> scc in sccs)

+          {

+            string datatypeString = "";

+            foreach (CtorType datatype in scc)

             {

-                GraphUtil.Graph<CtorType> dependencyGraph = new GraphUtil.Graph<CtorType>();

-                foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys)

+              datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";

+              foreach (Function f in ctx.KnownDatatypeConstructors[datatype])

+              {

+                string quotedConstructorName = Namer.GetQuotedName(f, f.Name);

+                if (f.InParams.Length == 0)

                 {

-                    dependencyGraph.AddSource(datatype);

-                    foreach (Function f in ctx.KnownDatatypeConstructors[datatype])

-                    {

-                        List<CtorType> dependentTypes = new List<CtorType>();

-                        foreach (Variable v in f.InParams)

-                        {

-                            FindDependentTypes(v.TypedIdent.Type, dependentTypes);

-                        }

-                        foreach (CtorType result in dependentTypes)

-                        {

-                            dependencyGraph.AddEdge(datatype, result);

-                        }

-                    }

+                  datatypeString += quotedConstructorName + " ";

                 }

-                GraphUtil.StronglyConnectedComponents<CtorType> sccs = new GraphUtil.StronglyConnectedComponents<CtorType>(dependencyGraph.Nodes, dependencyGraph.Predecessors, dependencyGraph.Successors);

-                sccs.Compute();

-                foreach (GraphUtil.SCC<CtorType> scc in sccs)

+                else

                 {

-                    string datatypeString = "";

-                    foreach (CtorType datatype in scc)

-                    {

-                        datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";

-                        foreach (Function f in ctx.KnownDatatypeConstructors[datatype])

-                        {

-                            string quotedConstructorName = Namer.GetQuotedName(f, f.Name);

-                            if (f.InParams.Length == 0)

-                            {

-                                datatypeString += quotedConstructorName + " ";

-                            }

-                            else

-                            {

-                                datatypeString += "(" + quotedConstructorName + " ";

-                                foreach (Variable v in f.InParams)

-                                {

-                                    string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);

-                                    datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

-                                }

-                                datatypeString += ") ";

-                            }

-                        }

-                        datatypeString += ") ";

-                    }

-                    List<string> decls = DeclCollector.GetNewDeclarations();

-                    foreach (string decl in decls)

-                    {

-                        SendCommon(decl);

-                    }

-                    SendCommon("(declare-datatypes () (" + datatypeString + "))");

+                  datatypeString += "(" + quotedConstructorName + " ";

+                  foreach (Variable v in f.InParams)

+                  {

+                    string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);

+                    datatypeString += "(" + quotedSelectorName + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";

+                  }

+                  datatypeString += ") ";

                 }

+              }

+              datatypeString += ") ";

             }

+            List<string> decls = DeclCollector.GetNewDeclarations();

+            foreach (string decl in decls)

+            {

+              SendCommon(decl);

+            }

+            SendCommon("(declare-datatypes () (" + datatypeString + "))");

+          }

         }

+      }

 

-        if (!AxiomsAreSetup)

-        {

-            var axioms = ctx.Axioms;

-            var nary = axioms as VCExprNAry;

-            if (nary != null && nary.Op == VCExpressionGenerator.AndOp)

-                foreach (var expr in nary.UniformArguments)

-                {

-                    var str = VCExpr2String(expr, -1);

-                    if (str != "true")

-                        AddAxiom(str);

-                }

-            else

-                AddAxiom(VCExpr2String(axioms, -1));

-            AxiomsAreSetup = true;

-        }

+      if (!AxiomsAreSetup)

+      {

+        var axioms = ctx.Axioms;

+        var nary = axioms as VCExprNAry;

+        if (nary != null && nary.Op == VCExpressionGenerator.AndOp)

+          foreach (var expr in nary.UniformArguments)

+          {

+            var str = VCExpr2String(expr, -1);

+            if (str != "true")

+              AddAxiom(str);

+          }

+        else

+          AddAxiom(VCExpr2String(axioms, -1));

+        AxiomsAreSetup = true;

+      }

     }

 

     public override int FlushAxiomsToTheoremProver()

@@ -368,7 +372,8 @@ namespace Microsoft.Boogie.SMTLib
 

       if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen

 

-      if (options.LogFilename != null && currentLogFile == null) {

+      if (options.LogFilename != null && currentLogFile == null)

+      {

         currentLogFile = OpenOutputFile(descriptiveName);

         currentLogFile.Write(common.ToString());

       }

@@ -398,16 +403,31 @@ namespace Microsoft.Boogie.SMTLib
     public override void Reset()

     {

       SendThisVC("(reset)");

-      Process.Send(common.ToString());

+      

+      if (0 < common.Length)

+      {

+        var c = common.ToString();

+        Process.Send(c);

+        if (currentLogFile != null)

+        {

+          currentLogFile.WriteLine(c);

+        }

+      }

     }

 

     public override void FullReset()

     {

-      SendThisVC("(reset)");

+      Namer.Reset();

       common.Clear();

+      SetupAxiomBuilder(gen);

+      Axioms.Clear();

+      TypeDecls.Clear();

       AxiomsAreSetup = false;

       ctx.Clear();

+      ctx.KnownDatatypeConstructors.Clear();

+      ctx.parent = this;

       DeclCollector.Reset();

+      SendThisVC("; doing a full reset...");

     }

 

     private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, 

@@ -1194,7 +1214,10 @@ namespace Microsoft.Boogie.SMTLib
 

     public override void SetTimeOut(int ms)

     {

-        SendThisVC("(set-option :" + Z3.SetTimeoutOption() + " " + ms.ToString() + ")");

+        var name = Z3.SetTimeoutOption();

+        var value = ms.ToString();

+        options.AddSmtOption(name, value);

+        SendThisVC(string.Format("(set-option :{0} {1})", name, value));

     }

 

     public override object Evaluate(VCExpr expr)

diff --git a/Source/VCExpr/NameClashResolver.cs b/Source/VCExpr/NameClashResolver.cs
index a78a6103..ac6ea33a 100644
--- a/Source/VCExpr/NameClashResolver.cs
+++ b/Source/VCExpr/NameClashResolver.cs
@@ -53,6 +53,15 @@ namespace Microsoft.Boogie.VCExprAST {
       return new UniqueNamer(this);

     }

 

+    public void Reset()

+    {

+      GlobalNames.Clear();

+      LocalNames.Clear();

+      UsedNames.Clear();

+      CurrentCounters.Clear();

+      GlobalPlusLocalNames.Clear();

+    }

+

     ////////////////////////////////////////////////////////////////////////////

 

     private readonly IDictionary<Object/*!*/, string/*!*/>/*!*/ GlobalNames;

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index a3f266ef..1e588760 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -178,17 +178,23 @@ namespace Microsoft.Boogie {
 

     public void Retarget(Program prog, ProverContext ctx, int timeout = 0)

     {

+        TheoremProver.FullReset();

         ctx.Clear();

         Setup(prog, ctx);

-        if (0 < timeout)

-        {

-          TheoremProver.SetTimeOut(timeout * 1000);

-        }

-        else

-        {

-          TheoremProver.SetTimeOut(0);

-        }

-        TheoremProver.FullReset();

+        this.timeout = timeout;

+        SetTimeout();

+    }

+

+    public void SetTimeout()

+    {

+      if (0 < timeout)

+      {

+        TheoremProver.SetTimeOut(timeout * 1000);

+      }

+      else

+      {

+        TheoremProver.SetTimeOut(0);

+      }

     }

 

     private static void Setup(Program prog, ProverContext ctx)

@@ -316,6 +322,7 @@ namespace Microsoft.Boogie {
       this.handler = handler;

 

       thmProver.Reset();

+      SetTimeout();

       proverStart = DateTime.UtcNow;

       thmProver.BeginCheck(descriptiveName, vc, handler);

       //  gen.ClearSharedFormulas();    PR: don't know yet what to do with this guy

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 484ce226..a836b6fb 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -104,10 +104,8 @@ public abstract class ProverContextContracts:ProverContext{
       this.genOptions = genOptions;

       Boogie2VCExprTranslator t = new Boogie2VCExprTranslator (gen, genOptions);

       this.translator = t;

-      OrderingAxiomBuilder oab = new OrderingAxiomBuilder(gen, t);

-      Contract.Assert(oab != null);

-      oab.Setup();

-      this.orderingAxiomBuilder = oab;

+

+      SetupOrderingAxiomBuilder(gen, t);

 

       distincts = new List<Variable>();

       axiomConjuncts = new List<VCExpr>();

@@ -115,8 +113,17 @@ public abstract class ProverContextContracts:ProverContext{
       exprTranslator = null;

     }

 

+    private void SetupOrderingAxiomBuilder(VCExpressionGenerator gen, Boogie2VCExprTranslator t)

+    {

+      OrderingAxiomBuilder oab = new OrderingAxiomBuilder(gen, t);

+      Contract.Assert(oab != null);

+      oab.Setup();

+      this.orderingAxiomBuilder = oab;

+    }

+

     public override void Clear()

     {

+        SetupOrderingAxiomBuilder(gen, translator);

         distincts = new List<Variable>();

         axiomConjuncts = new List<VCExpr>();

     }