Add USE_PREDICATES option to TPTP and SMT provers

2 files changed, 22 insertions, 9 deletions

diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index 4b710495..ba4e406b 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -20,14 +20,16 @@ using Microsoft.Boogie.Simplify;
 

 namespace Microsoft.Boogie.TPTP

 {

-  class TPTPProverOptions : ProverOptions

+  public class TPTPProverOptions : ProverOptions

   {

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

+    public bool UsePredicates = false;

 

     protected override bool Parse(string opt)

     {

       return

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

+        ParseBool(opt, "USE_PREDICATES", ref UsePredicates) ||

         base.Parse(opt);

     }

 

@@ -40,6 +42,7 @@ namespace Microsoft.Boogie.TPTP
 TPTP-specific options:

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

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

+USE_PREDICATES=<bool>     Try to use SMT predicates for functions returning bool.

 

 " + base.Help;

         // DIST requires non-public binaries

@@ -166,12 +169,17 @@ OUTPUT=<string>           Store VC in named file. Defaults to boogie-vc-@PROC@.t
       output.Close();

     }

 

+    public TPTPProverOptions Options

+    {

+      get { return (TPTPProverOptions)this.options; } 

+    }

+

     private TextWriter OpenOutputFile(string descriptiveName)

     {

       Contract.Requires(descriptiveName != null);

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

 

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

+      string filename = Options.Output;

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

       return new StreamWriter(filename, false);

     }

@@ -228,8 +236,8 @@ OUTPUT=<string>           Store VC in named file. Defaults to boogie-vc-@PROC@.t
       DeclCollector.Collect(exprWithoutLet);

       FeedTypeDeclsToProver();

 

-      AddAxiom(TPTPExprLineariser.ToString(axiomsWithoutLet, Namer));

-      string res = TPTPExprLineariser.ToString(exprWithoutLet, Namer);

+      AddAxiom(TPTPExprLineariser.ToString(axiomsWithoutLet, Namer, Options));

+      string res = TPTPExprLineariser.ToString(exprWithoutLet, Namer, Options);

       Contract.Assert(res != null);

 

       if (CommandLineOptions.Clo.Trace) {

diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs
index 78b87590..a35d43f0 100644
--- a/Source/Provers/TPTP/TPTPLineariser.cs
+++ b/Source/Provers/TPTP/TPTPLineariser.cs
@@ -53,13 +53,13 @@ void ObjectInvariant()
   // Lineariser for expressions. The result (bool) is currently not used for anything

   public class TPTPExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {

 

-    public static string ToString(VCExpr e, UniqueNamer namer) {

+    public static string ToString(VCExpr e, UniqueNamer namer, TPTPProverOptions opts) {

     Contract.Requires(e != null);

     Contract.Requires(namer != null);

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

 

       StringWriter sw = new StringWriter();

-      TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer);

+      TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer, opts);

       Contract.Assert(lin!=null);

       lin.Linearise(e, LineariserOptions.Default);

       return cce.NonNull(sw.ToString());

@@ -85,11 +85,13 @@ void ObjectInvariant()
     } }

 

     internal readonly UniqueNamer Namer;

+    internal readonly TPTPProverOptions Options;

 

-    public TPTPExprLineariser(TextWriter wr, UniqueNamer namer) {

+    public TPTPExprLineariser(TextWriter wr, UniqueNamer namer, TPTPProverOptions opts) {

       Contract.Requires(wr != null);Contract.Requires(namer != null);

       this.wr = wr;

       this.Namer = namer;

+      this.Options = opts;

     }

 

     public void Linearise(VCExpr expr, LineariserOptions options) {

@@ -724,8 +726,11 @@ void ObjectInvariant()
         string printedName = ExprLineariser.Namer.GetName(op.Func, Lowercase(op.Func.Name));

         Contract.Assert(printedName!=null);

 

-        // arguments are always terms

-        WriteApplicationTermOnly(printedName, node, options);

+        if (ExprLineariser.Options.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool)

+          WriteApplication(printedName, node, options, true);

+        else

+          // arguments are always terms

+          WriteApplicationTermOnly(printedName, node, options);

         return true;

       }