Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP provers. Add handling of help message about /proverOpt.

1 files changed, 33 insertions, 1 deletions

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index a0686adc..f1c4efcd 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -20,6 +20,33 @@ using Microsoft.Boogie.Simplify;
 

 namespace Microsoft.Boogie.SMTLib

 {

+  class SMTLibProverOptions : ProverOptions

+  {

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

+

+    protected override bool Parse(string opt)

+    {

+      return

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

+        base.Parse(opt);

+    }

+

+    public override string Help

+    {

+      get

+      {

+        return

+@"

+SMT-specific options:

+~~~~~~~~~~~~~~~~~~~~~

+OUTPUT=<string>           Store VC in named file. Defaults to boogie-vc-@PROC@.smt.

+

+" + base.Help;

+        // DIST requires non-public binaries

+      }

+    }

+  }

+

   public class SMTLibProcessTheoremProver : LogProverInterface

   {

     private readonly DeclFreeProverContext ctx;

@@ -149,7 +176,7 @@ void ObjectInvariant()
       Contract.Requires(descriptiveName != null);

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

 

-        string filename = CommandLineOptions.Clo.SMTLibOutputPath;

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

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

         return new StreamWriter(filename, false);

     }

@@ -300,6 +327,11 @@ void ObjectInvariant()
       return new DeclFreeProverContext(gen, genOptions);

     }

 

+    public override ProverOptions BlankProverOptions()

+    {

+      return new SMTLibProverOptions();

+    }

+

     protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options,

                                                               VCExpressionGenerator gen,

                                                               DeclFreeProverContext ctx) {