Improve support for identifying unnecessary assumes.

5 files changed, 73 insertions, 47 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 432d7f3e..300fbc10 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -86,6 +86,21 @@ namespace Microsoft.Boogie.SMTLib
       }
     }
 
+    public override void AssertNamed(VCExpr vc, bool polarity, string name)
+    {
+      string vcString;
+      if (polarity)
+      {
+        vcString = VCExpr2String(vc, 1);
+      }
+      else
+      {
+        vcString = "(not " + VCExpr2String(vc, 1) + ")";
+      }
+      AssertAxioms();
+      SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
+    }
+
     private void SetupAxiomBuilder(VCExpressionGenerator gen)
     {
       switch (CommandLineOptions.Clo.TypeEncodingMethod)
@@ -424,7 +439,7 @@ namespace Microsoft.Boogie.SMTLib
           Process.Inspector.NewProblem(descriptiveName, vc, handler);
       }
 
-      SendThisVC("(check-sat)");
+      SendCheckSat();
       FlushLogFile();
     }
 
@@ -474,6 +489,8 @@ namespace Microsoft.Boogie.SMTLib
         ctx.KnownDatatypeConstructors.Clear();
         ctx.parent = this;
         DeclCollector.Reset();
+        NamedAssumes.Clear();
+        UsedNamedAssumes = null;
         SendThisVC("; did a full reset");
       }
     }
@@ -1284,17 +1301,33 @@ namespace Microsoft.Boogie.SMTLib
 
             var reporter = handler as VC.VCGen.ErrorReporter;
             // TODO(wuestholz): Is the reporter ever null?
-            if (CommandLineOptions.Clo.PrintNecessaryAssumes && ContainsNamedAssumes && result == Outcome.Valid && reporter != null)
+            if (usingUnsatCore && result == Outcome.Valid && reporter != null && 0 < NamedAssumes.Count)
             {
-              SendThisVC("(get-unsat-core)");
-              var resp = Process.GetProverResponse();
-              if (resp.Name != "")
+              if (usingUnsatCore)
               {
-                 reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+                UsedNamedAssumes = new HashSet<string>();
+                SendThisVC("(get-unsat-core)");
+                var resp = Process.GetProverResponse();
+                if (resp.Name != "")
+                {
+                  UsedNamedAssumes.Add(resp.Name);
+                  if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+                  {
+                    reporter.AddNecessaryAssume(resp.Name.Substring("aux$$assume$$".Length));
+                  }
+                }
+                foreach (var arg in resp.Arguments)
+                {
+                  UsedNamedAssumes.Add(arg.Name);
+                  if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+                  {
+                    reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+                  }
+                }
               }
-              foreach (var arg in resp.Arguments)
+              else
               {
-                reporter.AddNecessaryAssume(arg.Name.Substring("aux$$assume$$".Length));
+                UsedNamedAssumes = null;
               }
             }
 
@@ -1457,13 +1490,13 @@ namespace Microsoft.Boogie.SMTLib
               expr = "false";
             }
             SendThisVC("(assert " + expr + ")");
-            SendThisVC("(check-sat)");
+            SendCheckSat();
           }
           else {
             string source = labels[labels.Length - 2];
             string target = labels[labels.Length - 1];
             SendThisVC("(assert (not (= (ControlFlow 0 " + source + ") (- " + target + "))))");
-            SendThisVC("(check-sat)");
+            SendCheckSat();
           }
         }
 
@@ -1508,7 +1541,7 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)");
       }
       FlushLogFile();
-      SendThisVC("(check-sat)");
+      SendCheckSat();
       queries++;
       return GetResponse();
     }
@@ -1984,8 +2017,6 @@ namespace Microsoft.Boogie.SMTLib
 
     readonly IList<string> OptimizationRequests = new List<string>();
 
-    bool ContainsNamedAssumes;
-
     protected string VCExpr2String(VCExpr expr, int polarity)
     {
       Contract.Requires(expr != null);
@@ -2025,8 +2056,8 @@ namespace Microsoft.Boogie.SMTLib
         DeclCollector.Collect(sortedExpr);
         FeedTypeDeclsToProver();
 
-        AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, ref ContainsNamedAssumes));
-        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, ref ContainsNamedAssumes, OptimizationRequests);
+        AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options, namedAssumes: NamedAssumes));
+        string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options, NamedAssumes, OptimizationRequests);
         Contract.Assert(res != null);
 
         if (CommandLineOptions.Clo.Trace)
@@ -2167,9 +2198,15 @@ namespace Microsoft.Boogie.SMTLib
     public override void Check()
     {
         PrepareCommon();
-        SendThisVC("(check-sat)");
+        SendCheckSat();
         FlushLogFile();
     }
+
+    public void SendCheckSat()
+    {
+      UsedNamedAssumes = null;
+      SendThisVC("(check-sat)");
+    }
 	
     public override void SetTimeOut(int ms)
     {
@@ -2366,21 +2403,6 @@ namespace Microsoft.Boogie.SMTLib
           return opts;
       }
 
-      public override void AssertNamed(VCExpr vc, bool polarity, string name)
-      {
-          string vcString;
-          if (polarity)
-          {
-              vcString = VCExpr2String(vc, 1);
-          }
-          else
-          {
-              vcString = "(not " + VCExpr2String(vc, 1) + ")";
-          }
-          AssertAxioms();
-          SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
-      }
-
       public override VCExpr ComputeInterpolant(VCExpr A, VCExpr B)
       {
           string A_str = VCExpr2String(A, 1);
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 06554fcb..06aa5bbe 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -34,17 +34,16 @@ namespace Microsoft.Boogie.SMTLib
   public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/>
   {
 
-    public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ref bool containsNamedAssumes, IList<string> optReqs = null)
+    public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null, ISet<VCExprVar> tryAssumes = null)
     {
       Contract.Requires(e != null);
       Contract.Requires(namer != null);
       Contract.Ensures(Contract.Result<string>() != null);
 
       StringWriter sw = new StringWriter();
-      SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, optReqs);
+      SMTLibExprLineariser lin = new SMTLibExprLineariser(sw, namer, opts, namedAssumes, optReqs);
       Contract.Assert(lin != null);
       lin.Linearise(e, LineariserOptions.Default);
-      containsNamedAssumes |= lin.ContainsNamedAssumes;
       return cce.NonNull(sw.ToString());
     }
 
@@ -76,20 +75,16 @@ namespace Microsoft.Boogie.SMTLib
     internal readonly SMTLibProverOptions ProverOptions;
 
     readonly IList<string> OptimizationRequests;
+    readonly ISet<VCExprVar> NamedAssumes;
 
-    bool containsNamedAssumes;
-    public bool ContainsNamedAssumes
-    {
-      get { return containsNamedAssumes; }
-    }
-
-    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, IList<string> optReqs = null)
+    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts, ISet<VCExprVar> namedAssumes = null, IList<string> optReqs = null)
     {
       Contract.Requires(wr != null); Contract.Requires(namer != null);
       this.wr = wr;
       this.Namer = namer;
       this.ProverOptions = opts;
       this.OptimizationRequests = optReqs;
+      this.NamedAssumes = namedAssumes;
     }
 
     public void Linearise(VCExpr expr, LineariserOptions options)
@@ -277,7 +272,7 @@ namespace Microsoft.Boogie.SMTLib
             && (node.Op.Equals(VCExpressionGenerator.MinimizeOp) || node.Op.Equals(VCExpressionGenerator.MaximizeOp)))
         {
           string optOp = node.Op.Equals(VCExpressionGenerator.MinimizeOp) ? "minimize" : "maximize";
-          OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, ref containsNamedAssumes)));
+          OptimizationRequests.Add(string.Format("({0} {1})", optOp, ToString(node[0], Namer, ProverOptions, NamedAssumes)));
           Linearise(node[1], options);
           return true;
         }
@@ -288,7 +283,8 @@ namespace Microsoft.Boogie.SMTLib
         }
         if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp))
         {
-          containsNamedAssumes = true;
+          var exprVar = node[0] as VCExprVar;
+          NamedAssumes.Add(exprVar);
           Linearise(node[1], options);
           return true;
         }
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index d911ce58..eaed83e9 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -217,7 +217,10 @@ void ObjectInvariant()
       } else if (node.Op.Equals(VCExpressionGenerator.NamedAssumeOp)) {
         var exprVar = node[0] as VCExprVar;
         AddDeclaration(string.Format("(declare-fun {0} () Bool)", exprVar.Name));
-        AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name));
+        if (CommandLineOptions.Clo.PrintNecessaryAssumes)
+        {
+          AddDeclaration(string.Format("(assert (! {0} :named {1}))", exprVar.Name, "aux$$" + exprVar.Name));
+        }
       } else {
         VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
         if (op != null && 
@@ -263,7 +266,7 @@ void ObjectInvariant()
         RegisterType(node.Type);
         string decl =
           "(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
-        if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$")))
+        if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$")))
         {
           AddDeclaration(decl);
         }
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index ae4d158a..7bda0022 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -453,6 +453,10 @@ namespace Microsoft.Boogie {
       Undetermined,
       Bounded
     }
+
+    public readonly ISet<VCExprVar> NamedAssumes = new HashSet<VCExprVar>();
+    public ISet<string> UsedNamedAssumes { get; protected set; }
+
     public class ErrorHandler {
       // Used in CheckOutcomeCore
       public virtual int StartingProcId()
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs
index d18c544a..cad5914b 100644
--- a/Source/VCGeneration/Wlp.cs
+++ b/Source/VCGeneration/Wlp.cs
@@ -193,9 +193,10 @@ namespace VC {
         var expr = ctxt.Ctxt.BoogieExprTranslator.Translate(ac.Expr);
         
         var aid = QKeyValue.FindStringAttribute(ac.Attributes, "id");
-        if (CommandLineOptions.Clo.PrintNecessaryAssumes && aid != null)
+        if (aid != null)
         {
-          var v = gen.Variable("assume$$" + aid, Microsoft.Boogie.Type.Bool);
+          var isTry = QKeyValue.FindBoolAttribute(ac.Attributes, "try");
+          var v = gen.Variable((isTry ? "try$$" : "assume$$") + aid, Microsoft.Boogie.Type.Bool);
           expr = gen.Function(VCExpressionGenerator.NamedAssumeOp, v, gen.ImpliesSimp(v, expr));
         }
         var soft = QKeyValue.FindBoolAttribute(ac.Attributes, "soft");