Make it possible to run Z3 on pipe; use generic PROVER_LOG options

5 files changed, 255 insertions, 45 deletions

diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2
index 33c82099..4490d2cb 100644
--- a/Binaries/UnivBackPred2.smt2
+++ b/Binaries/UnivBackPred2.smt2
@@ -1,4 +1,3 @@
-; -------------------------------------------------------------------------

 ; Boogie universal background predicate

 ; Copyright (c) 2004-2010, Microsoft Corp.

 

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 16801a65..8f1542ce 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -17,12 +17,12 @@ using Microsoft.Boogie.VCExprAST;
 using Microsoft.Boogie.Clustering;

 using Microsoft.Boogie.TypeErasure;

 using Microsoft.Boogie.Simplify;

+using System.Text;

 

 namespace Microsoft.Boogie.SMTLib

 {

   public class SMTLibProverOptions : ProverOptions

   {

-    public string Output = "boogie-vc-@PROC@.smt2";

     public bool UseWeights = true;

     public bool UseLabels { get { return UseZ3; } }

     public bool UseZ3 = true;

@@ -30,7 +30,6 @@ namespace Microsoft.Boogie.SMTLib
     protected override bool Parse(string opt)

     {

       return

-        ParseString(opt, "OUTPUT", ref Output) ||

         ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||

         ParseBool(opt, "USE_Z3", ref UseZ3) ||

         base.Parse(opt);

@@ -44,11 +43,10 @@ namespace Microsoft.Boogie.SMTLib
 @"

 SMT-specific options:

 ~~~~~~~~~~~~~~~~~~~~~

-OUTPUT=<string>           Store VC in named file (default: boogie-vc-@PROC@.smt2)

-USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (default: true)

 USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (default: true)

+USE_WEIGHTS=<bool>        Pass :weight annotations on quantified formulas (default: true)

+VERBOSITY=<int>           1 - print prover output (default: 0)

 " + base.Help;

-        // DIST requires non-public binaries

       }

     }

   }

@@ -105,6 +103,11 @@ USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (defau
       Namer = new SMTLibNamer();

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

 

+      if (this.options.UseZ3) {

+        var psi = SMTLibProcess.ComputerProcessStartInfo(Z3.Z3ExecutablePath(), "AUTO_CONFIG=false -smt2 -in");

+        Process = new SMTLibProcess(psi, this.options);

+        Process.ErrorHandler += this.HandleProverError;

+      }

     }

 

     public override ProverContext Context

@@ -117,10 +120,14 @@ USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (defau
       }

     }

 

-    private readonly TypeAxiomBuilder AxBuilder;

-    private readonly UniqueNamer Namer;

-    private readonly TypeDeclCollector DeclCollector;

-    private readonly SMTLibProcess Process;

+    readonly TypeAxiomBuilder AxBuilder;

+    readonly UniqueNamer Namer;

+    readonly TypeDeclCollector DeclCollector;

+    readonly SMTLibProcess Process;

+    readonly List<string> proverErrors = new List<string>();

+    readonly StringBuilder common = new StringBuilder();

+    TextWriter currentLogFile;

+    ErrorHandler currentErrorHandler;

 

     private void FeedTypeDeclsToProver()

     {

@@ -130,17 +137,41 @@ USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (defau
       }

     }

 

-    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)

+    private string Sanitize(string msg)

     {

-      //Contract.Requires(descriptiveName != null);

-      //Contract.Requires(vc != null);

-      //Contract.Requires(handler != null);

-      TextWriter output = OpenOutputFile(descriptiveName);

-      Contract.Assert(output != null);

+      var idx = msg.IndexOf('\n');

+      if (idx > 0)

+        msg = msg.Replace("\r", "").Replace("\n", "\r\n");

+      return msg;

+    }

 

-      WriteLineAndLog(output, _backgroundPredicates);

-      string name = SMTLibNamer.QuoteId(descriptiveName);

-      WriteLineAndLog(output, "(set-info :boogie-vc-id " + name + ")");

+    private void SendCommon(string s)

+    {

+      Send(s, true);

+    }

+

+    private void SendThisVC(string s)

+    {

+      Send(s, false);

+    }

+

+    private void Send(string s, bool isCommon)

+    {

+      s = Sanitize(s);

+

+      if (isCommon)

+        common.Append(s).Append("\r\n");

+

+      if (Process != null)

+        Process.Send(s);

+      if (currentLogFile != null)

+        currentLogFile.WriteLine(s);

+    }

+

+    private void PrepareCommon()

+    {

+      if (common.Length == 0)

+        SendCommon(_backgroundPredicates);

 

       if (!AxiomsAreSetup) {

         var axioms = ctx.Axioms;

@@ -154,26 +185,56 @@ USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (defau
           AddAxiom(VCExpr2String(axioms, -1));

         AxiomsAreSetup = true;

       }

+    }

 

-      string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";

-      string prelude = ctx.GetProverCommands(true);

-      Contract.Assert(prelude != null);

-      WriteLineAndLog(output, prelude);

-

-      foreach (string s in TypeDecls) {

-        Contract.Assert(s != null);

-        WriteLineAndLog(output, s);

-      }

+    private void FlushAxioms()

+    {

+      TypeDecls.Iter(SendCommon);

+      TypeDecls.Clear();

       foreach (string s in Axioms) {

         Contract.Assert(s != null);

         if (s != "true")

-          WriteLineAndLog(output, "(assert " + s + ")");

+          SendCommon("(assert " + s + ")");

       }

+      Axioms.Clear();

+    }

 

-      WriteLineAndLog(output, vcString);

-      WriteLineAndLog(output, "(check-sat)");

+    private void CloseLogFile()

+    {

+      if (currentLogFile != null) {

+        currentLogFile.Close();

+        currentLogFile = null;

+      }

+    }

+

+    public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)

+    {

+      //Contract.Requires(descriptiveName != null);

+      //Contract.Requires(vc != null);

+      //Contract.Requires(handler != null);

+

+      currentErrorHandler = handler;

+

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

+

+      if (options.LogFilename != null && currentLogFile == null) {

+        currentLogFile = OpenOutputFile(descriptiveName);

+        currentLogFile.Write(common.ToString());

+      }

+

+      PrepareCommon();

+      string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";

+      FlushAxioms();

+

+      SendThisVC("(push)");

+      SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");

+      SendThisVC(vcString);

 

-      output.Close();

+      if (Process != null)

+        Process.PingPong(); // flush any errors

+

+      SendThisVC("(check-sat)");

+      SendThisVC("(pop 1)");

     }

 

     private TextWriter OpenOutputFile(string descriptiveName)

@@ -181,27 +242,52 @@ USE_Z3=<bool>             Use z3.exe as the prover, and use Z3 extensions (defau
       Contract.Requires(descriptiveName != null);

       Contract.Ensures(Contract.Result<TextWriter>() != null);

 

-      string filename = ((SMTLibProverOptions)options).Output;

+      string filename = options.LogFilename;

       filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));

       return new StreamWriter(filename, false);

     }

 

-    private void WriteLineAndLog(TextWriter output, string msg)

+    private void HandleProverError(string s)

     {

-      Contract.Requires(output != null);

-      Contract.Requires(msg != null);

-      var idx = msg.IndexOf('\n');

-      if (idx > 0) {

-        msg = msg.Replace("\r", "").Replace("\n", "\r\n");

+      lock (proverErrors) {

+        proverErrors.Add(s);

+        Console.Error.WriteLine("Prover error: " + s);

       }

-      output.WriteLine(msg);

     }

 

     [NoDefaultContract]

     public override Outcome CheckOutcome(ErrorHandler handler)

     {  //Contract.Requires(handler != null);

       Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);

-      return Outcome.Undetermined;

+

+      var result = Outcome.Undetermined;

+

+      if (Process == null)

+        return result;

+

+      Process.Ping();

+      

+

+      while (true) {

+        var resp = Process.GetProverResponse();

+        if (resp == null || Process.IsPong(resp))

+          break;

+

+        switch (resp.Name) {

+          case "unsat":

+            result = Outcome.Valid;

+            break;

+          case "sat":

+          case "unknown":

+            result = Outcome.Invalid;

+            break;

+          default:

+            HandleProverError("Unexpected prover response: " + resp.ToString());

+            break;

+        }

+      }

+

+      return result;

     }

 

     protected string VCExpr2String(VCExpr expr, int polarity)

diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index c0ade351..536fd43e 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -114,6 +114,7 @@
     <Compile Include="SMTLibProcess.cs" />

     <Compile Include="TypeDeclCollector.cs" />

     <Compile Include="..\..\version.cs" />

+    <Compile Include="Z3.cs" />

   </ItemGroup>

   <ItemGroup>

     <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index da058ab6..4a631960 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -18,6 +18,7 @@ namespace Microsoft.Boogie.SMTLib
   public class SMTLibProcess

   {

     readonly Process prover;

+    readonly SMTLibProverOptions options;

     readonly Queue<string> proverOutput = new Queue<string>();

     readonly Queue<string> proverErrors = new Queue<string>();

     readonly TextWriter toProver;    

@@ -34,12 +35,14 @@ namespace Microsoft.Boogie.SMTLib
       };

     }

 

-    public SMTLibProcess(ProcessStartInfo psi)

+    public SMTLibProcess(ProcessStartInfo psi, SMTLibProverOptions options)

     {

+      this.options = options;

+

       try {

-        prover.ErrorDataReceived += prover_ErrorDataReceived;

-        prover.OutputDataReceived += prover_OutputDataReceived;

         prover = Process.Start(psi);

+        prover.ErrorDataReceived += prover_ErrorDataReceived;

+        prover.OutputDataReceived += prover_OutputDataReceived;        

         prover.BeginErrorReadLine();

         prover.BeginOutputReadLine();

         toProver = prover.StandardInput;

@@ -50,6 +53,13 @@ namespace Microsoft.Boogie.SMTLib
 

     public void Send(string cmd)

     {

+      if (options.Verbosity >= 2) {

+        var log = cmd;

+        if (log.Length > 50)

+          log = log.Substring(0, 50) + "...";

+        log = log.Replace("\r", "").Replace("\n", " ");

+        Console.WriteLine("[SMT-INP] {0}", log);

+      }

       toProver.WriteLine(cmd);

     }

 

@@ -78,6 +88,8 @@ namespace Microsoft.Boogie.SMTLib
 

     public SExpr GetProverResponse()

     {

+      toProver.Flush();

+

       while (true) {

         var exprs = ParseSExprs(true).ToArray();

         Contract.Assert(exprs.Length <= 1);

@@ -114,8 +126,10 @@ namespace Microsoft.Boogie.SMTLib
 

         if (linePos < currLine.Length)

           return currLine[linePos];

-        else

+        else {

           currLine = null;

+          linePos = 0;

+        }

       }

     }

 

@@ -138,6 +152,7 @@ namespace Microsoft.Boogie.SMTLib
           if (quoted) {

             sb.Append("\n");

             currLine = ReadProver();

+            linePos = 0;

             if (currLine == null)

               break;

           } else break;

@@ -176,6 +191,7 @@ namespace Microsoft.Boogie.SMTLib
         if (c == ')') {

           if (top)

             ParseError("stray ')'");

+          break;

         }

 

         string id;

@@ -245,6 +261,8 @@ namespace Microsoft.Boogie.SMTLib
     void prover_OutputDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

+        if (options.Verbosity >= 1)

+          Console.WriteLine("[SMT-OUT] {0}", e.Data);

         proverOutput.Enqueue(e.Data);

         Monitor.Pulse(this);

       }

@@ -253,6 +271,8 @@ namespace Microsoft.Boogie.SMTLib
     void prover_ErrorDataReceived(object sender, DataReceivedEventArgs e)

     {

       lock (this) {

+        if (options.Verbosity >= 1)

+          Console.WriteLine("[SMT-ERR] {0}", e.Data);

         proverErrors.Enqueue(e.Data);

         Monitor.Pulse(this);

       }

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
new file mode 100644
index 00000000..3867a55b
--- /dev/null
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -0,0 +1,104 @@
+//-----------------------------------------------------------------------------

+//

+// Copyright (C) Microsoft Corporation.  All Rights Reserved.

+//

+//-----------------------------------------------------------------------------

+

+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using System.Diagnostics.Contracts;

+using System.IO;

+using System.Text.RegularExpressions;

+

+namespace Microsoft.Boogie.SMTLib

+{

+  class Z3

+  {

+    static string _proverPath;

+

+    static string CodebaseString()

+    {

+      Contract.Ensures(Contract.Result<string>() != null);

+      return Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location));

+    }

+

+    public static string Z3ExecutablePath()

+    {

+      if (_proverPath == null)

+        FindZ3Executable();

+      return _proverPath;

+    }

+

+    static void FindZ3Executable()

+    // throws ProverException, System.IO.FileNotFoundException;

+    {      

+      Contract.Ensures(_proverPath != null);

+

+      var proverExe = "z3.exe";

+

+      if (_proverPath == null) {

+        // Initialize '_proverPath'

+        _proverPath = Path.Combine(CodebaseString(), proverExe);

+        string firstTry = _proverPath;

+

+        if (File.Exists(firstTry))

+          return;

+

+        string programFiles = Environment.GetEnvironmentVariable("ProgramFiles");

+        Contract.Assert(programFiles != null);

+        string programFilesX86 = Environment.GetEnvironmentVariable("ProgramFiles(x86)");

+        if (programFiles.Equals(programFilesX86)) {

+          // If both %ProgramFiles% and %ProgramFiles(x86)% point to "ProgramFiles (x86)", use %ProgramW6432% instead.

+          programFiles = Environment.GetEnvironmentVariable("ProgramW6432");

+        }

+

+

+        List<string> z3Dirs = new List<string>();

+        if (Directory.Exists(programFiles + @"\Microsoft Research\")) {

+          string msrDir = programFiles + @"\Microsoft Research\";

+          z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));

+        }

+        if (Directory.Exists(programFilesX86 + @"\Microsoft Research\")) {

+          string msrDir = programFilesX86 + @"\Microsoft Research\";

+          z3Dirs.AddRange(Directory.GetDirectories(msrDir, "Z3-*"));

+        }

+

+        // Look for the most recent version of Z3.

+        int minor = 0, major = 0;

+        string winner = null;

+        Regex r = new Regex(@"^Z3-(\d+)\.(\d+)$");

+        foreach (string d in z3Dirs) {

+          string name = new DirectoryInfo(d).Name;

+          foreach (Match m in r.Matches(name)) {

+            int ma, mi;

+            ma = int.Parse(m.Groups[1].ToString());

+            mi = int.Parse(m.Groups[2].ToString());

+            if (major < ma || (major == ma && minor < mi)) {

+              major = ma;

+              minor = mi;

+              winner = d;

+            }

+          }

+        }

+

+        if (major == 0 && minor == 0) {

+          throw new ProverException("Cannot find executable: " + firstTry);

+        }

+        Contract.Assert(winner != null);

+

+        _proverPath = Path.Combine(Path.Combine(winner, "bin"), proverExe);

+        if (!File.Exists(_proverPath)) {

+          throw new ProverException("Cannot find prover: " + _proverPath);

+        }

+

+        if (CommandLineOptions.Clo.Trace) {

+          Console.WriteLine("[TRACE] Using prover: " + _proverPath);

+        }

+      }

+    }

+

+

+  }

+}