Adding fixedpoint engine backend

10 files changed, 594 insertions, 185 deletions

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index f3f068d7..7d27c011 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -1,5 +1,5 @@
 

-Microsoft Visual Studio Solution File, Format Version 12.00

+Microsoft Visual Studio Solution File, Format Version 11.00

 # Visual Studio 2012

 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Provers", "Provers", "{B758C1E3-824A-439F-AA2F-0BA1143E8C8D}"

 EndProject

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index c12ba47d..1ee9bab6 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -743,10 +743,18 @@ namespace Microsoft.Boogie {
       try {

         if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Doomed) {

           vcgen = new DCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        } else if (CommandLineOptions.Clo.StratifiedInlining > 0) {

-          vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

-        } else {

-          vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        }

+        else if (CommandLineOptions.Clo.FixedPointEngine != null)

+        {

+            vcgen = new FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        }

+        else if (CommandLineOptions.Clo.StratifiedInlining > 0)

+        {

+            vcgen = new StratifiedVCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

+        }

+        else

+        {

+            vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend);

         }

       } catch (ProverException e) {

         ErrorWriteLine("Fatal Error: ProverException: {0}", e);

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index e94367ad..3e923ee9 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -574,6 +574,7 @@ namespace Microsoft.Boogie {
     public bool ExtractLoops = false;

     public bool DeterministicExtractLoops = false;

     public int StratifiedInlining = 0;

+    public string FixedPointEngine = null;

     public int StratifiedInliningOption = 0;

     public bool StratifiedInliningWithoutModels = false; // disable model generation for SI

     public int StratifiedInliningVerbose = 0; // verbosity level

@@ -583,6 +584,16 @@ namespace Microsoft.Boogie {
     public string CoverageReporterPath = null;

     public Process coverageReporter = null; // used internally for debugging

 

+    // Inference mode for fixed point engine

+    public enum FixedPointInferenceMode {

+       Corral,

+       OldCorral,

+       Flat,

+       Procedure,

+       Call

+    };

+    public FixedPointInferenceMode FixedPointMode = FixedPointInferenceMode.Procedure;

+

     public enum TypeEncoding {

       None,

       Predicates,

@@ -1002,6 +1013,38 @@ namespace Microsoft.Boogie {
             }

           }

           return true;

+        case "fixedPointEngine":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              FixedPointEngine = args[ps.i];

+          }

+          return true;

+        case "fixedPointInfer":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              switch (args[ps.i])

+              {

+                  case "corral":

+                      FixedPointMode = FixedPointInferenceMode.Corral;

+                      break;

+                  case "oldCorral":

+                      FixedPointMode = FixedPointInferenceMode.OldCorral;

+                      break;

+                  case "flat":

+                      FixedPointMode = FixedPointInferenceMode.Flat;

+                      break;

+                  case "procedure":

+                      FixedPointMode = FixedPointInferenceMode.Procedure;

+                      break;

+                  case "call":

+                      FixedPointMode = FixedPointInferenceMode.Call;

+                      break;

+                  default:

+                      ps.Error("Invalid argument \"{0}\" to option {1}", args[ps.i], ps.s);

+                      break;

+              }

+          }

+          return true;

         case "siVerbose":

           if (ps.ConfirmArgumentCount(1)) {

             StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));

@@ -1574,6 +1617,8 @@ namespace Microsoft.Boogie {
                 Use the lazy inlining algorithm

   /stratifiedInline:1

                 Use the stratified inlining algorithm

+  /fixedPointEngine:<engine>

+                Use the specified fixed point engine for inference

   /recursionBound:<n>

                 Set the recursion bound for stratified inlining to

                 be n (default 500)

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 3df1bd32..3004fafa 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -19,6 +19,8 @@ using Microsoft.Boogie.Clustering;
 using Microsoft.Boogie.TypeErasure;

 using System.Text;

 

+using RPFP = Microsoft.Boogie.RPFP;

+

 namespace Microsoft.Boogie.SMTLib

 {

   public class SMTLibProcessTheoremProver : ProverInterface

@@ -27,6 +29,7 @@ namespace Microsoft.Boogie.SMTLib
     private readonly VCExpressionGenerator gen;

     private readonly SMTLibProverOptions options;

     private bool usingUnsatCore;

+    private RPFP rpfp = null;

 

     [ContractInvariantMethod]

     void ObjectInvariant()

@@ -361,6 +364,7 @@ namespace Microsoft.Boogie.SMTLib
       //Contract.Requires(descriptiveName != null);

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

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

+      rpfp = null;

 

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

 

@@ -391,6 +395,191 @@ namespace Microsoft.Boogie.SMTLib
       FlushLogFile();

     }

 

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

+    {

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

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

+

+        RPFP.Node topnode = null;

+        var lines = resp.Arguments;

+

+        // last line of derivation is from query, skip it

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

+        {

+            var line = lines[i];

+            if (line.ArgCount != 5)

+            {

+                HandleProverError("bad derivation line from prover: " + line.ToString());

+                return null;

+            }

+            var name = line[0];

+            var conseq = line[1];

+            var subst = line[2];

+            var labs = line[3];

+            var refs = line[4];

+            var predName = conseq.Name;

+            RPFP.Node node = null;

+            if (!pmap.TryGetValue(predName, out node))

+            {

+                HandleProverError("unknown predicate from prover: " + predName.ToString());

+                return null;

+            }

+            RPFP.Node cexnode = rpfp.CloneNode(node);

+            cexnode.map = node;

+            nmap.Add(name.Name, cexnode);

+            List<RPFP.Node> Chs = new List<RPFP.Node>();

+

+            if (refs.Name != "ref")

+            {

+                HandleProverError("bad references from prover: " + refs.ToString());

+                return null;

+            }

+            foreach (var c in refs.Arguments)

+            {

+                if (c.Name == "true")

+                    Chs.Add(null);

+                else

+                {

+                    RPFP.Node ch = null;

+                    if (!nmap.TryGetValue(c.Name, out ch))

+                    {

+                        HandleProverError("unknown reference from prover: " + c.ToString());

+                        return null;

+                    }

+                    Chs.Add(ch);

+                }

+            }

+            RPFP.Edge e = rpfp.CreateEdge(cexnode, node.Outgoing.F, Chs.ToArray());

+            topnode = cexnode;

+

+            if (labs.Name != "labels")

+            {

+                HandleProverError("bad labels from prover: " + refs.ToString());

+                return null;

+            }

+            e.labels = new HashSet<string>();

+            foreach (var l in labs.Arguments)

+                e.labels.Add(l.Name);

+

+        }

+        if (topnode == null)

+        {

+            HandleProverError("empty derivation from prover: " + resp.ToString());

+        }

+        return topnode;

+    }

+

+    public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler, out RPFP.Node cex)

+    {

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

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

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

+        rpfp = _rpfp;

+        cex = null;

+

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

+

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

+        {

+            currentLogFile = OpenOutputFile(descriptiveName);

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

+        }

+

+        foreach (var node in rpfp.nodes)

+        {

+            DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);

+        }

+

+        PrepareCommon();

+

+        LineariserOptions.Default.LabelsBelowQuantifiers = true;

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

+        foreach (var edge in rpfp.edges)

+        {

+            string ruleString = "(rule " + VCExpr2String(rpfp.GetRule(edge), 1) + "\n)";

+            ruleStrings.Add(ruleString);

+        }

+        string queryString = "(query " + VCExpr2String(rpfp.GetQuery(), 1) + "\n   :engine duality\n  :print-certificate true\n)";

+        LineariserOptions.Default.LabelsBelowQuantifiers = false;

+        FlushAxioms();

+

+        PossiblyRestart();

+

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

+        foreach(var rs in ruleStrings)

+            SendThisVC(rs);

+        FlushLogFile();

+

+        if (Process != null)

+        {

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

+

+#if false

+            // TODO: this is not going to work

+            if (Process.Inspector != null)

+                Process.Inspector.NewProblem(descriptiveName, vc, handler);

+#endif

+        }

+

+        SendThisVC(queryString);

+        FlushLogFile();

+

+        var result = Outcome.Undetermined;

+

+        if (Process != null)

+        {

+            

+            var resp = Process.GetProverResponse();

+            

+            switch (resp.Name)

+            {

+                case "unsat":

+                    result = Outcome.Valid;

+                    break;

+                case "sat":

+                    result = Outcome.Invalid;

+                    break;

+                case "unknown":

+                    result = Outcome.Invalid;

+                    break;

+                default:

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

+                    break;

+            }

+            

+            switch (result)

+            {

+                case Outcome.Invalid:

+                    {

+                        resp = Process.GetProverResponse();

+                        if (resp.Name == "derivation")

+                        {

+                            cex = SExprToCex(resp, handler);

+                        }

+                        else

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

+                        break;

+                    }

+                default:

+                    break;

+            }

+

+#if false

+            while (true)

+            {

+                resp = Process.GetProverResponse();

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

+                    break;

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

+            }

+#endif

+        }

+        return result;

+    }

+

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

 

     private TextWriter OpenOutputFile(string descriptiveName)

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index da73dea1..1f4b6a7f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -23,7 +23,8 @@ namespace Microsoft.Boogie.SMTLib
   // Options for the linearisation

   public class LineariserOptions

   {

-    public static readonly LineariserOptions Default = new LineariserOptions();

+    public static LineariserOptions Default = new LineariserOptions();

+    public bool LabelsBelowQuantifiers = false;

   }

 

 

@@ -518,23 +519,28 @@ namespace Microsoft.Boogie.SMTLib
 

       public bool VisitLabelOp(VCExprNAry node, LineariserOptions options)

       {

-        if (ExprLineariser.UnderQuantifier > 0) {

+        if (ExprLineariser.UnderQuantifier > 0 && !options.LabelsBelowQuantifiers) {

           ExprLineariser.Linearise(node[0], options);

           return true;

         }

 

         var op = (VCExprLabelOp)node.Op;

-        if (CommandLineOptions.Clo.UseLabels) {

-          // Z3 extension

-          //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

-          wr.Write("(! ");

+

+        if (CommandLineOptions.Clo.UseLabels)

+        {

+            // Z3 extension

+            //wr.Write("({0} {1} ", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

+            wr.Write("(! ");

         }

 

-        wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label)));

-            

+        if(!options.LabelsBelowQuantifiers)

+            wr.Write("({0} {1} ", op.pos ? "and" : "or", SMTLibNamer.QuoteId(SMTLibNamer.LabelVar(op.label)));

+

         ExprLineariser.Linearise(node[0], options);

 

-        wr.Write(")");

+

+        if (!options.LabelsBelowQuantifiers) 

+            wr.Write(")");

 

         if (CommandLineOptions.Clo.UseLabels)

           wr.Write(" :{0} {1})", op.pos ? "lblpos" : "lblneg", SMTLibNamer.QuoteId(op.label));

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index bff949ea..9d908138 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -20,6 +20,7 @@ namespace Microsoft.Boogie.SMTLib
 

     private readonly UniqueNamer Namer;

     private readonly SMTLibProverOptions Options;

+    private HashSet<Function/*!*/>/*!*/ RegisteredRelations = new HashSet<Function>();

 

     [ContractInvariantMethod]

 void ObjectInvariant() 

@@ -170,6 +171,13 @@ void ObjectInvariant()
       KnownFunctions.Add(func);

     }

 

+    public void RegisterRelation(Function func)

+    {

+      if (RegisteredRelations.Contains(func))

+        return;

+      RegisteredRelations.Add(func);

+    }

+

     public override bool Visit(VCExprNAry node, bool arg) {

       Contract.Requires(node != null);

 

@@ -190,7 +198,11 @@ void ObjectInvariant()
 

             Contract.Assert(f.OutParams.Length == 1);

             var argTypes = f.InParams.Cast<Variable>().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " ");

-            string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

+            string decl;

+            if(RegisteredRelations.Contains(op.Func))

+                decl = "(declare-rel " + printedName + " (" + argTypes + ") " + ")";

+            else

+                decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")";

             AddDeclaration(decl);

           }

           KnownFunctions.Add(f);

diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs
index addfa3de..8081603e 100644
--- a/Source/Provers/SMTLib/Z3.cs
+++ b/Source/Provers/SMTLib/Z3.cs
@@ -14,195 +14,336 @@ using System.Text.RegularExpressions;
 

 namespace Microsoft.Boogie.SMTLib

 {

-  class Z3

-  {

-    static string _proverPath;

-

-    static string CodebaseString()

+    class Z3

     {

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

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

-    }

+        static string _proverPath;

 

-    public static string ExecutablePath()

-    {

-      if (_proverPath == null)

-        FindExecutable();

-      return _proverPath;

-    }

+        static string CodebaseString()

+        {

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

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

+        }

 

-    static void FindExecutable()

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

-    {

-      Contract.Ensures(_proverPath != null);

+        public static string ExecutablePath()

+        {

+            if (_proverPath == null)

+                FindExecutable();

+            return _proverPath;

+        }

 

-     // Command line option 'z3exe' always has priority if set 

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

-        _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;

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

-          throw new ProverException("Cannot find prover specified with z3exe: " + _proverPath);

+        static void FindExecutable()

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

+        {

+            Contract.Ensures(_proverPath != null);

+

+            // Command line option 'z3exe' always has priority if set 

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

+            {

+                _proverPath = CommandLineOptions.Clo.Z3ExecutablePath;

+                if (!File.Exists(_proverPath))

+                {

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

+                }

+                if (CommandLineOptions.Clo.Trace)

+                {

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

+                }

+                return;

+            }

+

+            var proverExe = "z3.exe";

+

+            if (_proverPath == null)

+            {

+                // Initialize '_proverPath'

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

+                string firstTry = _proverPath;

+

+                if (File.Exists(firstTry))

+                {

+                    if (CommandLineOptions.Clo.Trace)

+                    {

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

+                    }

+                    return;

+                }

+

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

+

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

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

+                    }

+

+

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

+                    }

+                }

+

+                int minMajor = 3, minMinor = 2;

+

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

+                }

+

+                if (major < minMajor || (major == minMajor && minor < minMinor))

+                {

+                    throw new ProverException(string.Format("Found version {0}.{1} of Z3. Please install version {2}.{3} or later. " +

+                                                            "(More conservative users might opt to supply -prover:Z3 option instead to get the historic Simplify back-end)",

+                                                            major, minor, minMajor, minMinor));

+                }

+            }

         }

-        if (CommandLineOptions.Clo.Trace) {

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

+

+

+        static int Z3MajorVersion = 0;

+        static int Z3MinorVersion = 0;

+        static bool Z3VersionObtained = false;

+

+        public static void GetVersion(out int major, out int minor)

+        {

+            if (!Z3VersionObtained)

+            {

+                var proc = new System.Diagnostics.Process();

+                proc.StartInfo.FileName = _proverPath;

+                proc.StartInfo.Arguments = "--version";

+                proc.StartInfo.RedirectStandardOutput = true;

+                proc.StartInfo.RedirectStandardError = true;

+                proc.StartInfo.UseShellExecute = false;

+                proc.StartInfo.CreateNoWindow = true;

+                proc.Start();

+                proc.WaitForExit();

+                if (proc.ExitCode == 0)

+                {

+                    string answer = proc.StandardOutput.ReadToEnd();

+                    var firstdot = answer.IndexOf('.');

+                    if (firstdot >= 0)

+                    {

+                        var seconddot = answer.IndexOf('.', firstdot + 1);

+                        if (seconddot >= firstdot + 1)

+                        {

+                            var spacebeforefirstdot = answer.LastIndexOf(' ', firstdot);

+                            if (spacebeforefirstdot >= 0)

+                            {

+                                var majorstr = answer.Substring(spacebeforefirstdot, firstdot - spacebeforefirstdot);

+                                var minorstr = answer.Substring(firstdot + 1, seconddot - firstdot - 1);

+                                Z3MajorVersion = Convert.ToInt32(majorstr);

+                                Z3MinorVersion = Convert.ToInt32(minorstr);

+                            }

+                        }

+                    }

+                }

+                Z3VersionObtained = true;

+            }

+            major = Z3MajorVersion;

+            minor = Z3MinorVersion;

         }

-        return;

-      }

 

-      var proverExe = "z3.exe";

+        // options that work only on the command line

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

 

-      if (_proverPath == null) {

-        // Initialize '_proverPath'

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

-        string firstTry = _proverPath;

+        public static void SetupOptions(SMTLibProverOptions options)

+        {

+            FindExecutable();

+            int major, minor;

+            GetVersion(out major, out minor);

+            if (major > 4 || major == 4 && minor >= 3)

+            {

 

-        if (File.Exists(firstTry)) {

-          if (CommandLineOptions.Clo.Trace) {

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

-          }

-          return;

-        }

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

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

 

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

-

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

-        if (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");

-          }

-

-

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

-          }

-        }

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

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

+

+                // options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false"); TODO: what does this do?

+

+                options.AddWeakSmtOption("MODEL.V2", "true");

+                //options.AddWeakSmtOption("ASYNC_COMMANDS", "false"); TODO: is this needed?

+

+                if (!options.OptimizeForBv)

+                {

+                    // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.

+                    // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.

+                    options.AddWeakSmtOption("smt.PHASE_SELECTION", "0");

+                    options.AddWeakSmtOption("smt.RESTART_STRATEGY", "0");

+                    options.AddWeakSmtOption("smt.RESTART_FACTOR", "|1.5|");

+

+                    // Make the integer model more diverse by default, speeds up some benchmarks a lot.

+                    options.AddWeakSmtOption("smt.ARITH.RANDOM_INITIAL_VALUE", "true");

+

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

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

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

+

+                    // In addition delay adding unit conflicts.

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

+                    //options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16"); TODO: what?

+                }

+

+                // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,

+                // the foo(x0) will be activated for e-matching when x is skolemized to x0.

+                options.AddWeakSmtOption("NNF.SK_HACK", "true");

+

+                // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

+                options.AddWeakSmtOption("smt.MBQI", "false");

+

+                // More or less like MAM=0.

+                options.AddWeakSmtOption("smt.QI.EAGER_THRESHOLD", "100");

+                // 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 (options.Inspector != null)

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

+

+                options.AddWeakSmtOption("TYPE_CHECK", "true");

+                options.AddWeakSmtOption("smt.BV.REFLECT", "true");

+

+                if (options.TimeLimit > 0)

+                {

+                    options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

+                    // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

+                    // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

+                }

+

+                if (options.Inspector != null)

+                    options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

 

-        int minMajor = 3, minMinor = 2;

-

-        // 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;

             }

-          }

-        }

+            else

+            {

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

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

 

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

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

-        }

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

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

+                options.AddWeakSmtOption("MODEL_HIDE_UNUSED_PARTITIONS", "false");

+                options.AddWeakSmtOption("MODEL_V2", "true");

+                options.AddWeakSmtOption("ASYNC_COMMANDS", "false");

 

-        Contract.Assert(winner != null);

+                if (!options.OptimizeForBv)

+                {

+                    // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.

+                    // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.

+                    options.AddWeakSmtOption("PHASE_SELECTION", "0");

+                    options.AddWeakSmtOption("RESTART_STRATEGY", "0");

+                    options.AddWeakSmtOption("RESTART_FACTOR", "|1.5|");

 

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

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

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

-        }

+                    // Make the integer model more diverse by default, speeds up some benchmarks a lot.

+                    options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");

 

-        if (CommandLineOptions.Clo.Trace) {

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

-        }

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

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

+                    options.AddWeakSmtOption("CASE_SPLIT", "3");

 

-        if (major < minMajor || (major == minMajor && minor < minMinor)) {

-          throw new ProverException(string.Format("Found version {0}.{1} of Z3. Please install version {2}.{3} or later. " +

-                                                  "(More conservative users might opt to supply -prover:Z3 option instead to get the historic Simplify back-end)",

-                                                  major, minor, minMajor, minMinor));

-        }

-      }

-    }

+                    // In addition delay adding unit conflicts.

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

+                    options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16");

+                }

 

-    // options that work only on the command line

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

+                // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,

+                // the foo(x0) will be activated for e-matching when x is skolemized to x0.

+                options.AddWeakSmtOption("NNF_SK_HACK", "true");

 

-    public static void SetupOptions(SMTLibProverOptions options)

-    {

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

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

-

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

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

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

-      options.AddWeakSmtOption("MODEL_V2", "true");

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

-

-      if (!options.OptimizeForBv) {

-        // Phase selection means to always try the negative literal polarity first, seems to be good for Boogie.

-        // The restart parameters change the restart behavior to match Z3 v1, which also seems to be good.

-        options.AddWeakSmtOption("PHASE_SELECTION", "0");

-        options.AddWeakSmtOption("RESTART_STRATEGY", "0");

-        options.AddWeakSmtOption("RESTART_FACTOR", "|1.5|");

-

-        // Make the integer model more diverse by default, speeds up some benchmarks a lot.

-        options.AddWeakSmtOption("ARITH_RANDOM_INITIAL_VALUE", "true");

-

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

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

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

-

-        // In addition delay adding unit conflicts.

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

-        options.AddWeakSmtOption("DELAY_UNITS_THRESHOLD", "16");

-      }

-

-      // This is used by VCC, but could be also useful for others, if sk_hack(foo(x)) is included as trigger,

-      // the foo(x0) will be activated for e-matching when x is skolemized to x0.

-      options.AddWeakSmtOption("NNF_SK_HACK", "true");

-

-      // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

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

-

-      // More or less like MAM=0.

-      options.AddWeakSmtOption("QI_EAGER_THRESHOLD", "100");

-      // 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("QI_COST", "|\"(+ weight generation)\"|");

-

-      //if (options.Inspector != null)

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

-

-      options.AddWeakSmtOption("TYPE_CHECK", "true");

-      options.AddWeakSmtOption("BV_REFLECT", "true");

-

-      if (options.TimeLimit > 0) {

-        options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

-        // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

-        // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

-      }

-

-      if (options.Inspector != null)

-        options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

-

-      // legacy option handling

-      if (!CommandLineOptions.Clo.z3AtFlag)

-        options.MultiTraces = true;

-

-      foreach (string opt in CommandLineOptions.Clo.Z3Options) {

-        Contract.Assert(opt != null);

-        int eq = opt.IndexOf("=");

-        if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(opt.Substring(0, eq))) {

-          options.AddSmtOption(opt.Substring(0, eq), opt.Substring(eq + 1));

-        } else {

-          options.AddSolverArgument(opt);

+                // don't use model-based quantifier instantiation; it never finishes on non-trivial Boogie problems

+                options.AddWeakSmtOption("MBQI", "false");

+

+                // More or less like MAM=0.

+                options.AddWeakSmtOption("QI_EAGER_THRESHOLD", "100");

+                // 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("QI_COST", "|\"(+ weight generation)\"|");

+

+                //if (options.Inspector != null)

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

+

+                options.AddWeakSmtOption("TYPE_CHECK", "true");

+                options.AddWeakSmtOption("BV_REFLECT", "true");

+

+                if (options.TimeLimit > 0)

+                {

+                    options.AddWeakSmtOption("SOFT_TIMEOUT", options.TimeLimit.ToString());

+                    // This kills the Z3 *instance* after the specified time, not a particular query, so we cannot use it.

+                    // options.AddSolverArgument("/T:" + (options.TimeLimit + 1000) / 1000);

+                }

+

+                if (options.Inspector != null)

+                    options.AddWeakSmtOption("PROGRESS_SAMPLING_FREQ", "200");

+

+

+            }

+

+            // legacy option handling

+            if (!CommandLineOptions.Clo.z3AtFlag)

+                options.MultiTraces = true;

+

+

+            foreach (string opt in CommandLineOptions.Clo.Z3Options)

+            {

+                Contract.Assert(opt != null);

+                int eq = opt.IndexOf("=");

+                if (eq > 0 && 'A' <= opt[0] && opt[0] <= 'Z' && !commandLineOnly.Contains(opt.Substring(0, eq)))

+                {

+                    options.AddSmtOption(opt.Substring(0, eq), opt.Substring(eq + 1));

+                }

+                else

+                {

+                    options.AddSolverArgument(opt);

+                }

+            }

         }

-      }

-    }

 

 

-  }

+    }

 }

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index fe4b4b99..607476e7 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -405,6 +405,11 @@ namespace Microsoft.Boogie {
       }

     }

     public abstract void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler);

+    

+    public virtual Outcome CheckRPFP(string descriptiveName, RPFP vc, ErrorHandler handler, out RPFP.Node cex)

+    {

+        throw new System.NotImplementedException();

+    }

     [NoDefaultContract]

     public abstract Outcome CheckOutcome(ErrorHandler handler);

     public virtual string[] CalculatePath(int controlFlowConstant) {

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index bcf0b0e5..3748d7f7 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1356,7 +1356,7 @@ namespace VC {
           vc = NestedBlockVC(impl, label2absy, true, proverContext, out assertionCount);

           break;

         case CommandLineOptions.VCVariety.Dag:

-          if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags) {

+          if (cce.NonNull(CommandLineOptions.Clo.TheProverFactory).SupportsDags || CommandLineOptions.Clo.FixedPointEngine != null) {

             vc = DagVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, new Hashtable/*<Block, VCExpr!>*/(), proverContext, out assertionCount);

           } else {

             vc = LetVC(cce.NonNull(impl.Blocks[0]), controlFlowVariableExpr, label2absy, proverContext, out assertionCount);

diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 0c98a891..f724307b 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -147,7 +147,10 @@
     <Compile Include="Check.cs" />

     <Compile Include="ConditionGeneration.cs" />

     <Compile Include="Context.cs" />

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

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

     <Compile Include="OrderingAxioms.cs" />

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

     <Compile Include="StratifiedVC.cs" />

     <Compile Include="VC.cs" />

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