Implement support for alternative SMT solvers -- CVC3 and CVC4

7 files changed, 84 insertions, 27 deletions

diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2
index 97c052c9..d3e3777f 100644
--- a/Binaries/UnivBackPred2.smt2
+++ b/Binaries/UnivBackPred2.smt2
@@ -7,5 +7,3 @@
 (declare-fun int_mod (Int Int) Int)

 (declare-fun UOrdering2 (|T@U| |T@U|) Bool)

 (declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)

-(declare-fun tickleBool (Bool) Bool)

-(assert (and (tickleBool true) (tickleBool false)))

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 4e134b3c..f45b76ba 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -1266,6 +1266,12 @@ namespace Microsoft.Boogie {
         ProverName = "SMTLib".ToUpper();

       }

 

+      var proverOpts = TheProverFactory.BlankProverOptions();

+      proverOpts.Parse(ProverOptions);

+      if (!TheProverFactory.SupportsLabels(proverOpts)) {

+        UseLabels = false;

+      }

+

       if (vcVariety == VCVariety.Unspecified) {

         vcVariety = TheProverFactory.DefaultVCVariety;

       }

diff --git a/Source/Core/VCExp.cs b/Source/Core/VCExp.cs
index 6bc43e14..1e82224c 100644
--- a/Source/Core/VCExp.cs
+++ b/Source/Core/VCExp.cs
@@ -202,6 +202,10 @@ The generic options may or may not be used by the prover plugin.
       }

     }

 

+    public virtual bool SupportsLabels(ProverOptions options) {

+      return true;

+    }

+

     public virtual void Close() {

     }

 

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 8c6ad875..89bd9d6e 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -94,17 +94,33 @@ namespace Microsoft.Boogie.SMTLib
       }

     }

 

-    void SetupProcess()

+    ProcessStartInfo ComputeProcessStartInfo()

     {

-      if (!this.options.UseZ3)

-        return;

+      var path = this.options.ProverPath;

+      switch (options.Solver) {

+        case SolverKind.Z3:

+          if (path == null)

+            path = Z3.ExecutablePath();

+          return SMTLibProcess.ComputerProcessStartInfo(path, "AUTO_CONFIG=false -smt2 -in");

+        case SolverKind.CVC3:

+          if (path == null)

+            path = "cvc3";

+          return SMTLibProcess.ComputerProcessStartInfo(path, "-lang smt2 +interactive -showPrompt");

+        case SolverKind.CVC4:

+          if (path == null)

+            path = "cvc4";

+          return SMTLibProcess.ComputerProcessStartInfo(path, "--smtlib2 --no-strict-parsing");

+        default:

+          Debug.Assert(false);

+          return null;

+      }

+    }

 

+    void SetupProcess()

+    {

       if (Process != null) return;

 

-      var path = this.options.ProverPath;

-      if (path == null)

-        path = Z3.ExecutablePath();

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

+      var psi = ComputeProcessStartInfo();

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

       Process.ErrorHandler += this.HandleProverError;

     }

@@ -197,6 +213,10 @@ namespace Microsoft.Boogie.SMTLib
         SendCommon("; done setting options\n");

         SendCommon(_backgroundPredicates);

 

+        if (options.UseTickleBool) {

+          SendCommon("(declare-fun tickleBool (Bool) Bool)");

+          SendCommon("(assert (and (tickleBool true) (tickleBool false)))");

+        }

         

         if (ctx.KnownDatatypeConstructors.Count > 0) {

           string datatypeString = "";

@@ -986,7 +1006,7 @@ namespace Microsoft.Boogie.SMTLib
       List<string>/*!>!*/ proverCommands = new List<string/*!*/>();

       proverCommands.Add("smtlib");

       var opts = (SMTLibProverOptions)options ;

-      if (opts.UseZ3)

+      if (opts.Solver == SolverKind.Z3)

         proverCommands.Add("z3");

       else

         proverCommands.Add("external");

@@ -1010,5 +1030,10 @@ namespace Microsoft.Boogie.SMTLib
 

       return new SMTLibProcessTheoremProver(options, gen, ctx);

     }

+

+    public override bool SupportsLabels(ProverOptions options)

+    {

+      return ((SMTLibProverOptions)options).SupportsLabels;

+    }

   }

 }

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 0a0e37a2..6a2cbb6a 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -416,14 +416,7 @@ namespace Microsoft.Boogie.SMTLib
         Contract.Requires(node != null);

         Contract.Requires(options != null);

 

-        // not sure if this is needed

-        if (node[0].Type.IsBool) {

-          Contract.Assert(node[1].Type.IsBool);

-          // use equivalence

-          WriteApplication("iff", node, options);

-        } else {

-          WriteApplication("=", node, options);

-        }

+        WriteApplication("=", node, options);

 

         return true;

       }

@@ -470,7 +463,10 @@ namespace Microsoft.Boogie.SMTLib
       public bool VisitCustomOp(VCExprNAry node, LineariserOptions options)

       {

         VCExprCustomOp op = (VCExprCustomOp)node.Op;

-        WriteApplication(op.Name, node, options);

+        if (!ExprLineariser.ProverOptions.UseTickleBool && op.Name == "tickleBool")

+          ExprLineariser.Linearise(VCExpressionGenerator.True, options);

+        else

+          WriteApplication(op.Name, node, options);

         return true;

       }

 

@@ -517,7 +513,7 @@ namespace Microsoft.Boogie.SMTLib
         }

 

         var op = (VCExprLabelOp)node.Op;

-        if (ExprLineariser.ProverOptions.UseLabels) {

+        if (CommandLineOptions.Clo.UseLabels) {

           // Z3 extension

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

           wr.Write("(! ");

@@ -529,7 +525,7 @@ namespace Microsoft.Boogie.SMTLib
 

         wr.Write(")");

 

-        if (ExprLineariser.ProverOptions.UseLabels)

+        if (CommandLineOptions.Clo.UseLabels)

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

 

         return true;

diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index 1dcfdbff..f4fa5e75 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -162,6 +162,11 @@ namespace Microsoft.Boogie.SMTLib
               sb.Clear();

             }

           }

+        } else if (resp.Name == "unsupported") {

+          // Skip -- this may be a benign "unsupported" from a previous command.

+          // Of course, this is suboptimal.  We should really be using

+          // print-success to identify the errant command and determine whether

+          // the response is benign.

         } else {

           return resp;

         }

diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs
index 8aea84c5..4d002956 100644
--- a/Source/Provers/SMTLib/SMTLibProverOptions.cs
+++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs
@@ -27,17 +27,20 @@ namespace Microsoft.Boogie.SMTLib
     }

   }

 

+  public enum SolverKind { Z3, CVC3, CVC4 };

+

   public class SMTLibProverOptions : ProverOptions

   {

     public bool UseWeights = true;

-    public bool UseLabels { get { return UseZ3; } }

+    public bool SupportsLabels { get { return Solver == SolverKind.Z3; } }

+    public bool UseTickleBool { get { return Solver == SolverKind.Z3; } }

+    public SolverKind Solver = SolverKind.Z3;

     public List<OptionValue> SmtOptions = new List<OptionValue>();

     public List<string> SolverArguments = new List<string>();

     public bool MultiTraces = false;

     public string Logic = "";

 

     // Z3 specific (at the moment; some of them make sense also for other provers)

-    public bool UseZ3 = true;

     public string Inspector = null;

     public bool OptimizeForBv = false;

 

@@ -80,6 +83,27 @@ namespace Microsoft.Boogie.SMTLib
 

     protected override bool Parse(string opt)

     {

+      string SolverStr = null;

+      if (ParseString(opt, "SOLVER", ref SolverStr)) {

+        switch (SolverStr) {

+          case "z3":

+            Solver = SolverKind.Z3;

+            break;

+          case "cvc3":

+            Solver = SolverKind.CVC3;

+            Logic = "ALL";

+            break;

+          case "cvc4":

+            Solver = SolverKind.CVC4;

+            Logic = "ALL_SUPPORTED";

+            break;

+          default:

+            ReportError("Invalid SOLVER value; must be 'z3', 'cvc3' or 'cvc4'");

+            return false;

+        }

+        return true;

+      }

+

       if (opt.StartsWith("O:")) {

         AddSmtOption(opt.Substring(2));

         return true;

@@ -93,7 +117,6 @@ namespace Microsoft.Boogie.SMTLib
       return

         ParseBool(opt, "MULTI_TRACES", ref MultiTraces) ||

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

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

         ParseString(opt, "INSPECTOR", ref Inspector) ||

         ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||

         ParseString(opt, "LOGIC", ref Logic) ||

@@ -103,7 +126,7 @@ namespace Microsoft.Boogie.SMTLib
     public override void PostParse()

     {

       base.PostParse();

-      if (UseZ3)

+      if (Solver == SolverKind.Z3)

         Z3.SetupOptions(this);

     }

 

@@ -115,18 +138,18 @@ namespace Microsoft.Boogie.SMTLib
 @"

 SMT-specific options:

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

+SOLVER=<string>           Use the given SMT solver (z3, cvc3, cvc4; default: z3)

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

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

 O:<name>=<value>          Pass (set-option :<name> <value>) to the SMT solver.

 C:<string>                Pass <string> to the SMT on the command line. 

-LOGIC=<string>            Pass (set-logic <string>) to the prover (default: empty)

+LOGIC=<string>            Pass (set-logic <string>) to the prover (default: empty, 'ALL' for CVC3 or 'ALL_SUPPORTED' for CVC4)

 

 Z3-specific options:

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

 MULTI_TRACES=<bool>       Report errors with multiple paths leading to the same assertion.

 INSPECTOR=<string>        Use the specified Z3Inspector binary.

 OPTIMIZE_FOR_BV=<bool>    Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.

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

 " + base.Help;

       }

     }