From 06771adc7acf710f055bfeeedc2c604c75ce945b Mon Sep 17 00:00:00 2001
From: Pantazis Deligiannis <pdeligia@me.com>
Date: Mon, 30 Sep 2013 09:59:01 +0100
Subject: changes to support a configured errorLimit

---
 Source/Houdini/Checker.cs           |  8 ++++----
 Source/Houdini/ConcurrentHoudini.cs | 17 +++++++++++++++--
 Source/Houdini/Houdini.cs           |  4 ++--
 3 files changed, 21 insertions(+), 8 deletions(-)

(limited to 'Source/Houdini')

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 30d6062f..252321b6 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -130,13 +130,13 @@ namespace Microsoft.Boogie.Houdini {
       return false;
     }
 
-    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int houdiniID = -1) {
+    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int taskID = -1) {
       this.descriptiveName = impl.Name;
       this.stats = stats;
       collector = new ConditionGeneration.CounterexampleCollector();
       collector.OnProgress("HdnVCGen", 0, 0, 0.0);
 
-      vcgen.ConvertCFG2DAG(impl, threadID: houdiniID);
+      vcgen.ConvertCFG2DAG(impl, taskID: taskID);
       ModelViewInfo mvInfo;
       var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);
 
@@ -222,7 +222,7 @@ namespace Microsoft.Boogie.Houdini {
       return expr;
     }
 
-    public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {
+    public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors, int taskID = -1) {
       collector.examples.Clear();
 
       if (CommandLineOptions.Clo.Trace) {
@@ -232,7 +232,7 @@ namespace Microsoft.Boogie.Houdini {
 
       VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);
       proverInterface.BeginCheck(descriptiveName, vc, handler);
-      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);
+      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, taskID: taskID);
 
       double queryTime = (DateTime.UtcNow - now).TotalSeconds;
       stats.proverTime += queryTime;
diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index a75cc054..f4bab257 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -43,7 +43,7 @@ namespace Microsoft.Boogie.Houdini
       Inline();
 
       this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, id);
 
       vcgenFailures = new HashSet<Implementation>();
       Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
@@ -53,7 +53,7 @@ namespace Microsoft.Boogie.Houdini
         try {
           if (CommandLineOptions.Clo.Trace)
             Console.WriteLine("Generating VC for {0}", impl.Name);
-          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, id);
+          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: id);
           houdiniSessions.Add(impl, session);
         }
         catch (VCGenException) {
@@ -260,5 +260,18 @@ namespace Microsoft.Boogie.Houdini
         }
       } 
     }
+
+    protected override ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
+      ProverInterface.Outcome outcome;
+      try {
+        outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors, taskID: id);
+      }
+      catch (UnexpectedProverOutputException upo) {
+        Contract.Assume(upo != null);
+        errors = null;
+        outcome = ProverInterface.Outcome.Undetermined;
+      }
+      return outcome;
+    }
   }
 }
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 12c972f3..c3575800 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -1086,7 +1086,7 @@ namespace Microsoft.Boogie.Houdini {
       return null;
     }
 
-    protected ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
+    protected virtual ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
       ProverInterface.Outcome outcome;
       try {
         outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors);
@@ -1099,7 +1099,7 @@ namespace Microsoft.Boogie.Houdini {
       return outcome;
     }
 
-    private Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)
+    protected Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)
     {
       Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);
       foreach (var c in program.TopLevelDeclarations.OfType<Constant>())
-- 
cgit v1.2.3