Record the SMT input size for each split

Source/Core/Xml.cs

@@ -112,7 +112,7 @@ public void WriteEndMethod(string outcome, DateTime endTime, TimeSpan elapsed, i
     }
 
     public void WriteSplit(int splitNum, int iteration, IEnumerable<AssertCmd> asserts, DateTime startTime,
-                           string outcome, TimeSpan elapsed, int? resourceCount)
+                           string outcome, TimeSpan elapsed, int? resourceCount, int? smtInputSize)
     {
       Contract.Requires(splitNum > 0);
       Contract.Requires(outcome != null);
@@ -145,6 +145,10 @@ public void WriteSplit(int splitNum, int iteration, IEnumerable<AssertCmd> asser
         {
           wr.WriteAttributeString("resourceCount", resourceCount.ToString());
         }
+        if (smtInputSize is not null)
+        {
+          wr.WriteAttributeString("smtInputSize", smtInputSize.ToString());
+        }
         wr.WriteEndElement(); // conclusion
 
         wr.WriteEndElement(); // assertionBatch

Source/ExecutionEngine/ImplementationRunResult.cs

@@ -78,7 +78,7 @@ public void ProcessXml(ExecutionEngine engine) {
 
       foreach (var vcResult in RunResults.OrderBy(s => (vcNum: s.VcNum, iteration: s.Iteration))) {
         engine.Options.XmlSink.WriteSplit(vcResult.VcNum, vcResult.Iteration, vcResult.Asserts, vcResult.StartTime,
-          vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount);
+          vcResult.Outcome.ToString().ToLowerInvariant(), vcResult.RunTime, vcResult.ResourceCount, vcResult.CheckInputs.TotalSize);
       }
 
       engine.Options.XmlSink.WriteEndMethod(VcOutcome.ToString().ToLowerInvariant(),

Source/Provers/SMTLib/ProverInterface.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Text;
 using System.Threading;
 using System.Threading.Tasks;
 using Microsoft.Boogie.SMTLib;
@@ -21,6 +22,9 @@ public enum SolverOutcome
 
 public abstract class ProverInterface
 {
+  public int VCExprSize { get; protected set; }
+  public abstract int CommonSize { get; }
+
   public static ProverInterface CreateProver(SMTLibOptions libOptions, Program prog,
     string /*?*/ logFilePath, bool appendLogFile, uint timeout,
     int taskID = -1)

Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs

@@ -71,11 +71,9 @@ public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr v
         SetupProcess();
         checkSatSent = false;
         FullReset(gen);
-
         if (options.LogFilename != null && currentLogFile == null)
         {
           currentLogFile = OpenOutputFile(descriptiveName);
-          await currentLogFile.WriteAsync(common.ToString());
         }
 
         SendVCOptions();
@@ -84,8 +82,9 @@ public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr v
 
         OptimizationRequests.Clear();
 
-        string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
+        string vcString = "(assert (not\n" + VcExpr2String(vc, 1) + "\n))";
         FlushAxioms();
+        VCExprSize = vcString.Length;
 
         Push();
         SendVCId(descriptiveName);
@@ -284,7 +283,8 @@ protected override void Send(string s, bool isCommon)
       // Boogie emits comments after the solver has responded. In batch
       // mode, sending these to the solver is problematic. But they'll
       // still get sent to the log below.
-      if (Process != null && !checkSatSent) {
+      if (Process != null && !checkSatSent)
+      {
         Process.Send(s);
       }
 

Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs

@@ -46,7 +46,8 @@ private void PossiblyRestart()
       if (Process != null && processNeedsRestart) {
         processNeedsRestart = false;
         SetupProcess();
-        Process.Send(common.ToString());
+        var c = common.ToString();
+        Process.Send(c);
       }
     }
 
@@ -63,7 +64,8 @@ public override int FlushAxiomsToTheoremProver()
     }
 
     private bool hasReset = true;
-    public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, int errorLimit, CancellationToken cancellationToken)
+    public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr vc, ErrorHandler handler, 
+      int errorLimit, CancellationToken cancellationToken)
     {
       currentErrorHandler = handler;
       try
@@ -100,7 +102,8 @@ public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr v
 
         SendThisVC("(push 1)");
         DeclCollector.Push();
-        string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
+        string vcString = "(assert (not\n" + VcExpr2String(vc, 1) + "\n))";
+        VCExprSize = vcString.Length;
         FlushAxioms();
         SendVCId(descriptiveName);
         SendVCOptions();
@@ -145,7 +148,7 @@ public override async Task Reset(VCExpressionGenerator generator)
         Process.Send(c);
         if (currentLogFile != null)
         {
-          currentLogFile.WriteLine(c);
+          await currentLogFile.WriteLineAsync(c);
         }
       }
 
@@ -433,7 +436,7 @@ private Task<SolverOutcome> CheckSplit(SortedSet<int> split, uint timeLimit, uin
         expr = VCExprGen.AndSimp(expr, lit);
       }
 
-      SendThisVC("(assert " + VCExpr2String(expr, 1) + ")");
+      SendThisVC("(assert " + VcExpr2String(expr, 1) + ")");
       if (options.Solver == SolverKind.Z3)
       {
         SendThisVC("(apply (then (using-params propagate-values :max_rounds 1) simplify) :print false)");
@@ -533,7 +536,7 @@ private async Task<SolverOutcome> CheckSatAndGetResponse(CancellationToken cance
 
     public override async Task<object> Evaluate(VCExpr expr)
     {
-      string vcString = VCExpr2String(expr, 1);
+      string vcString = VcExpr2String(expr, 1);
       var resp = await SendVcRequest($"(get-value ({vcString}))");
       if (resp == null)
       {
@@ -697,7 +700,7 @@ public override int GetRCount()
           nameCounter++;
           nameToAssumption.Add(name, i);
 
-          string vcString = VCExpr2String(vc, 1);
+          string vcString = VcExpr2String(vc, 1);
           AssertAxioms();
           SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
           i++;
@@ -748,13 +751,13 @@ public override int GetRCount()
         var hardAssumptionStrings = new List<string>();
         foreach (var a in hardAssumptions)
         {
-          hardAssumptionStrings.Add(VCExpr2String(a, 1));
+          hardAssumptionStrings.Add(VcExpr2String(a, 1));
         }
 
         var currAssumptionStrings = new List<string>();
         foreach (var a in softAssumptions)
         {
-          currAssumptionStrings.Add(VCExpr2String(a, 1));
+          currAssumptionStrings.Add(VcExpr2String(a, 1));
         }
 
         Push();

Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs

@@ -91,11 +91,11 @@ public override void AssertNamed(VCExpr vc, bool polarity, string name)
       string vcString;
       if (polarity)
       {
-        vcString = VCExpr2String(vc, 1);
+        vcString = VcExpr2String(vc, 1);
       }
       else
       {
-        vcString = "(not " + VCExpr2String(vc, 1) + ")";
+        vcString = "(not " + VcExpr2String(vc, 1) + ")";
       }
 
       AssertAxioms();
@@ -149,6 +149,8 @@ protected static string Sanitize(string msg)
       return msg;
     }
 
+    public override int CommonSize => common.Length;
+
     public override void LogComment(string comment)
     {
       SendCommon("; " + comment);
@@ -191,63 +193,65 @@ private void FindDependentTypes(Type type, List<DatatypeTypeCtorDecl> dependentT
 
     private void PrepareDataTypes()
     {
-      if (ctx.KnownDatatypes.Count > 0)
+      if (ctx.KnownDatatypes.Count <= 0)
       {
-        GraphUtil.Graph<DatatypeTypeCtorDecl> dependencyGraph = new GraphUtil.Graph<DatatypeTypeCtorDecl>();
-        foreach (var datatype in ctx.KnownDatatypes)
+        return;
+      }
+
+      var dependencyGraph = new GraphUtil.Graph<DatatypeTypeCtorDecl>();
+      foreach (var datatype in ctx.KnownDatatypes)
+      {
+        dependencyGraph.AddSource(datatype);
+        foreach (DatatypeConstructor f in datatype.Constructors)
         {
-          dependencyGraph.AddSource(datatype);
-          foreach (Function f in datatype.Constructors)
+          var dependentTypes = new List<DatatypeTypeCtorDecl>();
+          foreach (Variable v in f.InParams)
           {
-            var dependentTypes = new List<DatatypeTypeCtorDecl>();
-            foreach (Variable v in f.InParams)
-            {
-              FindDependentTypes(v.TypedIdent.Type, dependentTypes);
-            }
-            foreach (var result in dependentTypes)
-            {
-              dependencyGraph.AddEdge(datatype, result);
-            }
+            FindDependentTypes(v.TypedIdent.Type, dependentTypes);
+          }
+          foreach (var result in dependentTypes)
+          {
+            dependencyGraph.AddEdge(datatype, result);
           }
         }
+      }
 
-        GraphUtil.StronglyConnectedComponents<DatatypeTypeCtorDecl> sccs =
-          new GraphUtil.StronglyConnectedComponents<DatatypeTypeCtorDecl>(dependencyGraph.Nodes, dependencyGraph.Predecessors,
-            dependencyGraph.Successors);
-        sccs.Compute();
-        foreach (GraphUtil.SCC<DatatypeTypeCtorDecl> scc in sccs)
+      var sccs =
+        new GraphUtil.StronglyConnectedComponents<DatatypeTypeCtorDecl>(dependencyGraph.Nodes, dependencyGraph.Predecessors,
+          dependencyGraph.Successors);
+      sccs.Compute();
+      foreach (var scc in sccs)
+      {
+        string datatypesString = "";
+        string datatypeConstructorsString = "";
+        foreach (var datatype in scc)
         {
-          string datatypesString = "";
-          string datatypeConstructorsString = "";
-          foreach (var datatype in scc)
+          datatypesString += "(" + new SMTLibExprLineariser(libOptions).TypeToString(new CtorType(Token.NoToken, datatype, new List<Type>())) + " 0)";
+          string datatypeConstructorString = "";
+          foreach (Function f in datatype.Constructors)
           {
-            datatypesString += "(" + new SMTLibExprLineariser(libOptions).TypeToString(new CtorType(Token.NoToken, datatype, new List<Type>())) + " 0)";
-            string datatypeConstructorString = "";
-            foreach (Function f in datatype.Constructors)
+            string quotedConstructorName = Namer.GetQuotedName(f, f.Name);
+            datatypeConstructorString += "(" + quotedConstructorName + " ";
+            foreach (Variable v in f.InParams)
             {
-              string quotedConstructorName = Namer.GetQuotedName(f, f.Name);
-              datatypeConstructorString += "(" + quotedConstructorName + " ";
-              foreach (Variable v in f.InParams)
-              {
-                string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);
-                datatypeConstructorString += "(" + quotedSelectorName + " " +
-                                             DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
-              }
-
-              datatypeConstructorString += ") ";
+              string quotedSelectorName = Namer.GetQuotedName(v, v.Name + "#" + f.Name);
+              datatypeConstructorString += "(" + quotedSelectorName + " " +
+                                           DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
             }
 
-            datatypeConstructorsString += "(" + datatypeConstructorString + ") ";
+            datatypeConstructorString += ") ";
           }
 
-          List<string> decls = DeclCollector.GetNewDeclarations();
-          foreach (string decl in decls)
-          {
-            SendCommon(decl);
-          }
+          datatypeConstructorsString += "(" + datatypeConstructorString + ") ";
+        }
 
-          SendCommon("(declare-datatypes (" + datatypesString + ") (" + datatypeConstructorsString + "))");
+        List<string> decls = DeclCollector.GetNewDeclarations();
+        foreach (string decl in decls)
+        {
+          SendCommon(decl);
         }
+
+        SendCommon("(declare-datatypes (" + datatypesString + ") (" + datatypeConstructorsString + "))");
       }
     }
 
@@ -318,7 +322,7 @@ private void PrepareFunctionDefinitions()
           funcDef += ") ";
 
           funcDef += new SMTLibExprLineariser(libOptions).TypeToString(defBody[0].Type) + " ";
-          funcDef += VCExpr2String(defBody[1], -1);
+          funcDef += VcExpr2String(defBody[1], -1);
           funcDef += ")";
           generatedFuncDefs.Add(funcDef);
           definitionAdded.Add(f);
@@ -402,13 +406,13 @@ private void SetupAxioms()
       var axioms = ctx.Axioms;
       if (axioms is VCExprNAry nary && nary.Op == VCExpressionGenerator.AndOp) {
         foreach (var expr in nary.UniformArguments) {
-          var str = VCExpr2String(expr, -1);
+          var str = VcExpr2String(expr, -1);
           if (str != "true") {
             AddAxiom(str);
           }
         }
       } else {
-        AddAxiom(VCExpr2String(axioms, -1));
+        AddAxiom(VcExpr2String(axioms, -1));
       }
 
       AxiomsAreSetup = true;
@@ -970,7 +974,7 @@ private void ConvertErrorModel(StringBuilder m)
 
     protected readonly IList<string> OptimizationRequests = new List<string>();
 
-    protected string VCExpr2String(VCExpr expr, int polarity)
+    public string VcExpr2String(VCExpr expr, int polarity)
     {
       Contract.Requires(expr != null);
       Contract.Ensures(Contract.Result<string>() != null);
@@ -1101,7 +1105,7 @@ public override VCExpressionGenerator VCExprGen
     //int numRealPushes;
     public override string VCExpressionToString(VCExpr vc)
     {
-      return VCExpr2String(vc, 1);
+      return VcExpr2String(vc, 1);
     }
 
     public override void PushVCExpression(VCExpr vc)
@@ -1135,7 +1139,7 @@ public override void Assert(VCExpr vc, bool polarity, bool isSoft = false, int w
         assert += "-soft";
       }
 
-      var expr = polarity ? VCExpr2String(vc, 1) : "(not\n" + VCExpr2String(vc, 1) + "\n)";
+      var expr = polarity ? VcExpr2String(vc, 1) : "(not\n" + VcExpr2String(vc, 1) + "\n)";
       if (options.Solver == SolverKind.Z3 && isSoft)
       {
         expr += " :weight " + weight;
@@ -1157,7 +1161,7 @@ public override void DefineMacro(Macro f, VCExpr vc)
       string printedName = Namer.GetQuotedName(f, f.Name);
       var argTypes = string.Join(" ", f.InParams.Select(p => DeclCollector.TypeToStringReg(p.TypedIdent.Type)));
       string decl = "(define-fun " + printedName + " (" + argTypes + ") " +
-                    DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VCExpr2String(vc, 1) + ")";
+                    DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VcExpr2String(vc, 1) + ")";
       AssertAxioms();
       SendThisVC(decl);
     }