various changes for duality from dead codeplex repo

5 files changed, 55 insertions, 27 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index be371fcb..1564b76b 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -418,6 +418,8 @@ namespace Microsoft.Boogie {
     public string SimplifyLogFilePath = null;

     public bool PrintInstrumented = false;

     public bool InstrumentWithAsserts = false;

+    public string ProverPreamble = null;

+

     public enum InstrumentationPlaces {

       LoopHeaders,

       Everywhere

@@ -938,7 +940,14 @@ namespace Microsoft.Boogie {
           }

           return true;

 

-        case "logPrefix":

+        case "proverPreamble": 

+          if (ps.ConfirmArgumentCount(1))

+          {

+            ProverPreamble = args[ps.i];

+          }

+           return true;

+          

+          case "logPrefix":

           if (ps.ConfirmArgumentCount(1)) {

             string s = cce.NonNull(args[ps.i]);

             LogPrefix += s.Replace('/', '-').Replace('\\', '-');

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index afb38986..c6c04b89 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -321,6 +321,8 @@ namespace Microsoft.Boogie.SMTLib
             SendCommon("(declare-datatypes () (" + datatypeString + "))");

           }

         }

+        if (CommandLineOptions.Clo.ProverPreamble != null)

+            SendCommon("(include \"" + CommandLineOptions.Clo.ProverPreamble + "\")");

       }

 

       if (!AxiomsAreSetup)

@@ -1016,6 +1018,9 @@ namespace Microsoft.Boogie.SMTLib
                 case "unknown":

                     result = Outcome.Invalid;

                     break;

+                case "bounded":

+                    result = Outcome.Bounded;

+                    break;

                 case "error":

                     if (resp.ArgCount > 0 && resp.Arguments[0].Name.Contains("canceled"))

                     {

@@ -1053,7 +1058,8 @@ namespace Microsoft.Boogie.SMTLib
                             HandleProverError("Unexpected prover response: " + resp.ToString());

                         break;

                     }

-				case Outcome.Valid:

+                case Outcome.Valid:

+                case Outcome.Bounded:

 				    {

 						resp = Process.GetProverResponse();

                         if (resp.Name == "fixedpoint")

@@ -1170,6 +1176,7 @@ namespace Microsoft.Boogie.SMTLib
         usedLogNames.Add(curFilename);

       }

 

+      Console.WriteLine("opening log file {0}", curFilename);

       return new StreamWriter(curFilename, false);

     }

 

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index 250e04c9..ffa4e0cb 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -248,7 +248,8 @@ namespace Microsoft.Boogie.SMTLib
             // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more.

 

             // the following will make the :weight option more usable

-            if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|(+ weight generation)|"); // TODO: this doesn't seem to work

+              // KLM: this QI cost function is the default

+            // if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|(+ weight generation)|"); // TODO: this doesn't seem to work

 

             //if (options.Inspector != null)

             //  options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 33baf798..71ae21c6 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -449,7 +449,8 @@ namespace Microsoft.Boogie {
       Invalid,

       TimeOut,

       OutOfMemory,

-      Undetermined

+      Undetermined,

+      Bounded

     }

     public class ErrorHandler {

       // Used in CheckOutcomeCore

diff --git a/Source/VCGeneration/FixedpointVC.cs b/Source/VCGeneration/FixedpointVC.cs
index 5c698633..70ce5a8f 100644
--- a/Source/VCGeneration/FixedpointVC.cs
+++ b/Source/VCGeneration/FixedpointVC.cs
@@ -480,13 +480,6 @@ namespace Microsoft.Boogie
                 List<Variable> interfaceVars = new List<Variable>();

                 Expr assertExpr = new LiteralExpr(Token.NoToken, true);

                 Contract.Assert(assertExpr != null);

-                foreach (Variable v in program.GlobalVariables)

-                {

-                    Contract.Assert(v != null);

-                    interfaceVars.Add(v);

-                    if (v.Name == "error")

-                        inputErrorVariable = v;

-                }

                 // InParams must be obtained from impl and not proc

                 foreach (Variable v in impl.InParams)

                 {

@@ -503,6 +496,13 @@ namespace Microsoft.Boogie
                     Expr eqExpr = Expr.Eq(new IdentifierExpr(Token.NoToken, c), new IdentifierExpr(Token.NoToken, v));

                     assertExpr = Expr.And(assertExpr, eqExpr);

                 }

+                foreach (Variable v in program.GlobalVariables)

+                {

+                    Contract.Assert(v != null);

+                    interfaceVars.Add(v);

+                    if (v.Name == "error")

+                        inputErrorVariable = v;

+                }

                 if (errorVariable != null)

                 {

                     proc.Modifies.Add(new IdentifierExpr(Token.NoToken, errorVariable));

@@ -657,11 +657,6 @@ namespace Microsoft.Boogie
                     }

                     else if (mode == Mode.Corral || proc.FindExprAttribute("inline") != null || proc is LoopProcedure)

                     {

-                        foreach (Variable v in program.GlobalVariables)

-                        {

-                            Contract.Assert(v != null);

-                            exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

-                        }

                         foreach (Variable v in proc.InParams)

                         {

                             Contract.Assert(v != null);

@@ -672,6 +667,11 @@ namespace Microsoft.Boogie
                             Contract.Assert(v != null);

                             exprs.Add(new IdentifierExpr(Token.NoToken, v));

                         }

+                        foreach (Variable v in program.GlobalVariables)

+                        {

+                            Contract.Assert(v != null);

+                            exprs.Add(new OldExpr(Token.NoToken, new IdentifierExpr(Token.NoToken, v)));

+                        }

                         foreach (IdentifierExpr ie in proc.Modifies)

                         {

                             Contract.Assert(ie != null);

@@ -1513,7 +1513,7 @@ namespace Microsoft.Boogie
 

         /** Check the RPFP, and return a counterexample if there is one. */

 

-        public RPFP.LBool Check(ref RPFP.Node cexroot)

+        public VC.ConditionGeneration.Outcome Check(ref RPFP.Node cexroot)

         {

             var start = DateTime.Now;

 

@@ -1548,11 +1548,15 @@ namespace Microsoft.Boogie
             switch(outcome)

             {

                 case ProverInterface.Outcome.Valid:

-                   return RPFP.LBool.False;

+                    return VC.ConditionGeneration.Outcome.Correct;

+                case ProverInterface.Outcome.Bounded:

+                    return VC.ConditionGeneration.Outcome.ReachedBound;

                 case ProverInterface.Outcome.Invalid:

-                   return RPFP.LBool.True;

+                    return VC.ConditionGeneration.Outcome.Errors;

+                case ProverInterface.Outcome.TimeOut:

+                    return VC.ConditionGeneration.Outcome.TimedOut;

                 default:

-                   return RPFP.LBool.Undef;

+                   return VC.ConditionGeneration.Outcome.Inconclusive;

             }

         }

 

@@ -1598,7 +1602,7 @@ namespace Microsoft.Boogie
                     Console.WriteLine("check: {0}s", (DateTime.Now - start).TotalSeconds);

                     switch (checkres)

                     {

-                        case RPFP.LBool.True:

+                        case Outcome.Errors:

                             Console.WriteLine("Counterexample found.\n");

                             // start = DateTime.Now;

                             Counterexample cex = CreateBoogieCounterExample(cexroot.owner, cexroot, impl);

@@ -1607,17 +1611,23 @@ namespace Microsoft.Boogie
                             collector.OnCounterexample(cex, "assertion failure");

                             Console.WriteLine("cex: {0}s", (DateTime.Now - start).TotalSeconds);

                             ConjecturesToSpecs();

-                            return VC.ConditionGeneration.Outcome.Errors;

-                        case RPFP.LBool.False:

-                            Console.WriteLine("Procedure is correct.");

+                            break;

+                        case Outcome.Correct:

+                            Console.WriteLine("Procedure is correct. (fixed point reached)");

 							FixedPointToSpecs();

                             ConjecturesToSpecs();

-                            return Outcome.Correct;

-                        case RPFP.LBool.Undef:

+                            break;

+                        case Outcome.ReachedBound:

+                            Console.WriteLine("Procedure is correct. (recursion bound reached)");

+                            FixedPointToSpecs();

+                            ConjecturesToSpecs();

+                            break;

+                        default:

                             Console.WriteLine("Inconclusive result.");

                             ConjecturesToSpecs();

-                            return Outcome.ReachedBound;

+                            break;

                     }

+                    return checkres;

                     

                 }