diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2012-12-10 12:21:16 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2012-12-10 12:21:16 +0530 |
| commit | edd49fda92881753f149d667d39bba9ad07cbb70 (patch) | |
| tree | f1f69c293f20138f210ca0cf13e0a357cf8beee3 /Source/BoogieDriver | |
| parent | 5f5ee3308c77a0d75fea79c394ba38eccf6ad127 (diff) | |
More stuff for abstract houdini; updated test case
Diffstat (limited to 'Source/BoogieDriver')
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 70 |
1 files changed, 39 insertions, 31 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index a99f1f47..25eb1bc6 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -616,10 +616,14 @@ namespace Microsoft.Boogie { }
#region Run Houdini and verify
- if (CommandLineOptions.Clo.ContractInfer) {
+ if (CommandLineOptions.Clo.ContractInfer)
+ {
if (CommandLineOptions.Clo.AbstractHoudini != null)
{
CommandLineOptions.Clo.PrintErrorModel = 1;
+ CommandLineOptions.Clo.UseArrayTheory = true;
+ CommandLineOptions.Clo.TypeEncodingMethod = CommandLineOptions.TypeEncoding.Monomorphic;
+
// Run Abstract Houdini
Houdini.PredicateAbs.Initialize(program);
var abs = new Houdini.AbstractHoudini(program);
@@ -627,39 +631,43 @@ namespace Microsoft.Boogie { return PipelineOutcome.Done;
}
- Houdini.Houdini houdini = new Houdini.Houdini(program);
- Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
- if (CommandLineOptions.Clo.PrintAssignment) {
- Console.WriteLine("Assignment computed by Houdini:");
- foreach (var x in outcome.assignment) {
- Console.WriteLine(x.Key + " = " + x.Value);
+ Houdini.Houdini houdini = new Houdini.Houdini(program);
+ Houdini.HoudiniOutcome outcome = houdini.PerformHoudiniInference();
+ if (CommandLineOptions.Clo.PrintAssignment)
+ {
+ Console.WriteLine("Assignment computed by Houdini:");
+ foreach (var x in outcome.assignment)
+ {
+ Console.WriteLine(x.Key + " = " + x.Value);
+ }
}
- }
- if (CommandLineOptions.Clo.Trace)
- {
- int numTrueAssigns = 0;
- foreach (var x in outcome.assignment) {
- if (x.Value)
- numTrueAssigns++;
+ if (CommandLineOptions.Clo.Trace)
+ {
+ int numTrueAssigns = 0;
+ foreach (var x in outcome.assignment)
+ {
+ if (x.Value)
+ numTrueAssigns++;
+ }
+ Console.WriteLine("Number of true assignments = " + numTrueAssigns);
+ Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
+ Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
+ Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime);
+ Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
+ Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
+ Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
}
- Console.WriteLine("Number of true assignments = " + numTrueAssigns);
- Console.WriteLine("Number of false assignments = " + (outcome.assignment.Count - numTrueAssigns));
- Console.WriteLine("Prover time = " + Houdini.HoudiniSession.proverTime);
- Console.WriteLine("Unsat core prover time = " + Houdini.HoudiniSession.unsatCoreProverTime);
- Console.WriteLine("Number of prover queries = " + Houdini.HoudiniSession.numProverQueries);
- Console.WriteLine("Number of unsat core prover queries = " + Houdini.HoudiniSession.numUnsatCoreProverQueries);
- Console.WriteLine("Number of unsat core prunings = " + Houdini.HoudiniSession.numUnsatCorePrunings);
- }
- foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values) {
- ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
- }
- //errorCount = outcome.ErrorCount;
- //verified = outcome.Verified;
- //inconclusives = outcome.Inconclusives;
- //timeOuts = outcome.TimeOuts;
- //outOfMemories = 0;
- return PipelineOutcome.Done;
+ foreach (Houdini.VCGenOutcome x in outcome.implementationOutcomes.Values)
+ {
+ ProcessOutcome(x.outcome, x.errors, "", ref errorCount, ref verified, ref inconclusives, ref timeOuts, ref outOfMemories);
+ }
+ //errorCount = outcome.ErrorCount;
+ //verified = outcome.Verified;
+ //inconclusives = outcome.Inconclusives;
+ //timeOuts = outcome.TimeOuts;
+ //outOfMemories = 0;
+ return PipelineOutcome.Done;
}
#endregion
|