Conjecture printing for duality and child user time tracking.

4 files changed, 271 insertions, 32 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 4e895931..56907a89 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -66,6 +66,12 @@ namespace Microsoft.Boogie.SMTLib
       ctx.parent = this;

       this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer);

 

+      if (CommandLineOptions.Clo.PrintFixedPoint != null || CommandLineOptions.Clo.PrintConjectures != null)

+      {

+          declHandler = new MyDeclHandler();

+          DeclCollector.SetDeclHandler(declHandler);

+      }

+

       SetupProcess();

 

       if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)

@@ -82,6 +88,7 @@ namespace Microsoft.Boogie.SMTLib
           }

           PrepareCommon();

       }

+		

     }

 

     private void SetupAxiomBuilder(VCExpressionGenerator gen)

@@ -677,27 +684,9 @@ namespace Microsoft.Boogie.SMTLib
 			// get all the predicate definitions

 			for (int i = 0; i < lines.Length; i++) {

 				var line = lines [i];

-				if(line.Name != "define-fun"){

-					HandleProverError ("Prover error: expected define-fun but got:" + line.Name);

-					throw new BadExprFromProver ();

-				}

-				if(line.ArgCount != 4){

-					HandleProverError ("Prover error: define-fun has wrong number of arguments");

-					throw new BadExprFromProver ();

-				}

-				var pname = StripCruft(line.Arguments[0].Name);

-				var pvars = line.Arguments[1];

-				var pbody = line.Arguments[3]; // range has to be Bool

-				var binding = new Dictionary<string,VCExpr>();

-				var pvs = new List<VCExpr>();

-				foreach(var b in pvars.Arguments){

-					var e = SExprToVar (b);

-					pvs.Add (e);

-					binding.Add (b.Name,e);

-				}

-				VCExpr bexpr = SExprToVCExpr(pbody,binding);

-				

-				var annot = rpfp.CreateRelation(pvs.ToArray(),bexpr);

+                string pname;

+                RPFP.Transformer annot;

+                GetDefun(line, out pname, out annot);

 				

 				if(pmap.ContainsKey(pname)){

 					var node = pmap[pname];

@@ -710,6 +699,34 @@ namespace Microsoft.Boogie.SMTLib
 			}

 			

 		}

+

+        private void GetDefun(SExpr line, out string pname, out RPFP.Transformer annot)

+        {

+            if (line.Name != "define-fun")

+            {

+                HandleProverError("Prover error: expected define-fun but got:" + line.Name);

+                throw new BadExprFromProver();

+            }

+            if (line.ArgCount != 4)

+            {

+                HandleProverError("Prover error: define-fun has wrong number of arguments");

+                throw new BadExprFromProver();

+            }

+            pname = StripCruft(line.Arguments[0].Name);

+            var pvars = line.Arguments[1];

+            var pbody = line.Arguments[3]; // range has to be Bool

+            var binding = new Dictionary<string, VCExpr>();

+            var pvs = new List<VCExpr>();

+            foreach (var b in pvars.Arguments)

+            {

+                var e = SExprToVar(b);

+                pvs.Add(e);

+                binding.Add(StripCruft(b.Name), e);

+            }

+            VCExpr bexpr = SExprToVCExpr(pbody, binding);

+

+            annot = rpfp.CreateRelation(pvs.ToArray(), bexpr);

+        }

 		

     private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, 

                                  Dictionary<int,Dictionary<string,string>> varSubst)

@@ -887,10 +904,6 @@ namespace Microsoft.Boogie.SMTLib
         rpfp = _rpfp;

         cex = null;

 			

-		if(CommandLineOptions.Clo.PrintFixedPoint != null){

-			declHandler = new MyDeclHandler();

-		    DeclCollector.SetDeclHandler(declHandler);

-		}

 			

         if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen

 

@@ -900,6 +913,8 @@ namespace Microsoft.Boogie.SMTLib
             currentLogFile.Write(common.ToString());

         }

 

+        PrepareCommon(); 

+        

         Push();

         SendThisVC("(fixedpoint-push)");

         foreach (var node in rpfp.nodes)

@@ -907,8 +922,6 @@ namespace Microsoft.Boogie.SMTLib
             DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);

         }

 

-        PrepareCommon();

-

         LineariserOptions.Default.LabelsBelowQuantifiers = true;

         List<string> ruleStrings = new List<string>();

         foreach (var edge in rpfp.edges)

@@ -1047,11 +1060,74 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC("(fixedpoint-pop)");

         Pop();

         AxiomsAreSetup = false;

-		DeclCollector.SetDeclHandler(null);

-		declHandler = null; // just so we can GC it

+

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

+        {

+            ReadConjectures(CommandLineOptions.Clo.PrintConjectures);

+        }

+

         return result;

     }

 

+    class MyFileParser : SExpr.Parser

+    {

+        SMTLibProcessTheoremProver parent;

+

+        public MyFileParser(System.IO.StreamReader _sr, SMTLibProcessTheoremProver _parent)

+            : base(_sr)

+        {

+            parent = _parent;

+        }

+        public override void ParseError(string msg)

+        {

+            parent.HandleProverError("Error in conjecture file from prover: " + msg);

+        }

+    }

+

+    void ReadConjectures(string filename)

+    {

+        try

+        {

+            System.IO.StreamReader sr = new StreamReader(filename + ".tmp");

+            SExpr.Parser p = new MyFileParser(sr, this);

+            var sexps = p.ParseSExprs(false);

+            Dictionary<string, RPFP.Node> pmap = GetNodeMap();

+            foreach (var e in sexps)

+            {

+                string pname;

+                RPFP.Transformer annot;

+                GetDefun(e, out pname, out annot);

+

+                if (pmap.ContainsKey(pname))

+                {

+                    var c = new RPFP.Conjecture();

+                    c.node = pmap[pname];

+                    c.bound = annot;

+                    rpfp.conjectures.Add(c);

+                }

+                else if (pname[0] != '@')

+                { // if not an internal symbol

+                    HandleProverError("Prover error: got unknown predicate:" + pname);

+                    throw new BadExprFromProver();

+                }

+            }

+            sr.Close();

+        }

+        catch (Exception)

+        {

+            HandleProverError("No conjecture file from prover");

+            throw new BadExprFromProver();

+        }

+    }

+

+    private Dictionary<string, RPFP.Node> GetNodeMap()

+    {

+        Dictionary<string, RPFP.Node> pmap = new Dictionary<string, RPFP.Node>();

+        foreach (var node in rpfp.nodes)

+            pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name, node);

+        return pmap;

+    }

+

     private static HashSet<string> usedLogNames = new HashSet<string>();

 

     private TextWriter OpenOutputFile(string descriptiveName)

diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs
index 461e1ee8..ba07ec27 100644
--- a/Source/Provers/SMTLib/SExpr.cs
+++ b/Source/Provers/SMTLib/SExpr.cs
@@ -106,6 +106,156 @@ namespace Microsoft.Boogie
     }

     #endregion

 

+    #region parsing

+

+    public abstract class Parser

+    {

+        System.IO.StreamReader sr;

+        int linePos = 0;

+        string currLine = null;

+

+        public Parser(System.IO.StreamReader _sr)

+        {

+            sr = _sr;

+        }

+        string Read()

+        {

+            return sr.ReadLine();

+        }

+        char SkipWs()

+        {

+            while (true)

+            {

+                if (currLine == null)

+                {

+                    currLine = Read();

+                    if (currLine == null)

+                        return '\0';

+                }

+

+                while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos]))

+                    linePos++;

+

+                if (linePos < currLine.Length)

+                    return currLine[linePos];

+                else

+                {

+                    currLine = null;

+                    linePos = 0;

+                }

+            }

+        }

+

+        void Shift()

+        {

+            linePos++;

+        }

+

+        string ParseId()

+        {

+            var sb = new StringBuilder();

+

+            var beg = SkipWs();

+

+            var quoted = beg == '"' || beg == '|';

+            if (quoted)

+                Shift();

+            while (true)

+            {

+                if (linePos >= currLine.Length)

+                {

+                    if (quoted)

+                    {

+                        sb.Append("\n");

+                        currLine = Read();

+                        linePos = 0;

+                        if (currLine == null)

+                            break;

+                    }

+                    else break;

+                }

+

+                var c = currLine[linePos++];

+                if (quoted && c == beg)

+                    break;

+                if (!quoted && (char.IsWhiteSpace(c) || c == '(' || c == ')'))

+                {

+                    linePos--;

+                    break;

+                }

+                if (quoted && c == '\\' && linePos < currLine.Length && currLine[linePos] == '"')

+                {

+                    sb.Append('"');

+                    linePos++;

+                    continue;

+                }

+                sb.Append(c);

+            }

+

+            return sb.ToString();

+        }

+

+        public abstract void ParseError(string msg);

+

+        public IEnumerable<SExpr> ParseSExprs(bool top)

+        {

+            while (true)

+            {

+                var c = SkipWs();

+                if (c == '\0')

+                    break;

+

+                if (c == ')')

+                {

+                    if (top)

+                        ParseError("stray ')'");

+                    break;

+                }

+

+                string id;

+

+                if (c == '(')

+                {

+                    Shift();

+                    c = SkipWs();

+                    if (c == '\0')

+                    {

+                        ParseError("expecting something after '('");

+                        break;

+                    }

+                    else if (c == '(')

+                    {

+                        id = "";

+                    }

+                    else

+                    {

+                        id = ParseId();

+                    }

+

+                    var args = ParseSExprs(false).ToArray();

+

+                    c = SkipWs();

+                    if (c == ')')

+                    {

+                        Shift();

+                    }

+                    else

+                    {

+                        ParseError("unclosed '(" + id + "'");

+                    }

+                    yield return new SExpr(id, args);

+                }

+                else

+                {

+                    id = ParseId();

+                    yield return new SExpr(id);

+                }

+

+                if (top) break;

+            }

+        }

+    }

+    #endregion

   }

 }

 

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 2374a157..439557c0 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -175,8 +175,11 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

+    public static System.TimeSpan TotalUserTime = System.TimeSpan.Zero;

+

     public void Close()

     {

+      TotalUserTime += prover.UserProcessorTime;

       try {

         prover.Kill();

       } catch {

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index ed8f0908..c8f49603 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -4,6 +4,7 @@
 //

 //-----------------------------------------------------------------------------

 

+

 using System;

 using System.Collections.Generic;

 using System.Linq;

@@ -200,6 +201,7 @@ namespace Microsoft.Boogie.SMTLib
         // options that work only on the command line

         static string[] commandLineOnly = { "TRACE", "PROOF_MODE" };

 

+

         public static void SetupOptions(SMTLibProverOptions options)

         {

           FindExecutable();

@@ -208,8 +210,10 @@ namespace Microsoft.Boogie.SMTLib
           if (major > 4 || major == 4 && minor >= 3)

           {

 

+              bool fp = false; // CommandLineOptions.Clo.FixedPointEngine != null;

+

             // don't bother with auto-config - it would disable explicit settings for eager threshold and so on

-            options.AddWeakSmtOption("AUTO_CONFIG", "false");

+            if(!fp) options.AddWeakSmtOption("AUTO_CONFIG", "false");

 

             //options.AddWeakSmtOption("MODEL_PARTIAL", "true");

             //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false");

@@ -232,7 +236,8 @@ namespace Microsoft.Boogie.SMTLib
 

               // The left-to-right structural case-splitting strategy.

               //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now

-              options.AddWeakSmtOption("smt.CASE_SPLIT", "3");

+

+              if (!fp) options.AddWeakSmtOption("smt.CASE_SPLIT", "3");

 

               // In addition delay adding unit conflicts.

               options.AddWeakSmtOption("smt.DELAY_UNITS", "true");

@@ -251,7 +256,7 @@ 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

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

+            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");

@@ -275,6 +280,11 @@ namespace Microsoft.Boogie.SMTLib
               options.AddWeakSmtOption("smt.array.weak", "true");

               options.AddWeakSmtOption("smt.array.extensional", "false");

             }

+

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

+            {

+                options.AddWeakSmtOption("fixedpoint.conjecture_file", CommandLineOptions.Clo.PrintConjectures + ".tmp");

+            }

           }

           else

           {