Add USE_PREDICATES option to TPTP and SMT provers

3 files changed, 39 insertions, 16 deletions

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

 namespace Microsoft.Boogie.SMTLib

 {

-  class SMTLibProverOptions : ProverOptions

+  public class SMTLibProverOptions : ProverOptions

   {

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

+    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.SMTLib
 SMT-specific options:

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

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

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

 

 " + base.Help;

         // DIST requires non-public binaries

@@ -96,7 +99,7 @@ void ObjectInvariant()
       UniqueNamer namer = new UniqueNamer ();

       Namer = namer;

       Namer.Spacer = "__";

-      this.DeclCollector = new TypeDeclCollector (namer);

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

       

     }

     

@@ -195,6 +198,11 @@ void ObjectInvariant()
       return Outcome.Undetermined;

     }

 

+    protected SMTLibProverOptions Options

+    {

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

+    }

+

     protected string VCExpr2String(VCExpr expr, int polarity) {

       Contract.Requires(expr != null);

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

@@ -230,8 +238,8 @@ void ObjectInvariant()
       DeclCollector.Collect(sortedExpr);

       FeedTypeDeclsToProver();

 

-      AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer));

-      string res = SMTLibExprLineariser.ToString(sortedExpr, Namer);

+      AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, Options));

+      string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, Options);

       Contract.Assert(res!=null);

 

       if (CommandLineOptions.Clo.Trace) {

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 677ff296..7b5e51b0 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -54,13 +54,13 @@ void ObjectInvariant()
   // Lineariser for expressions. The result (bool) is currently not used for anything

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

 

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

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

     Contract.Requires(e != null);

     Contract.Requires(namer != null);

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

 

       StringWriter sw = new StringWriter();

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

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

       Contract.Assert(lin!=null);

       lin.Linearise(e, LineariserOptions.Default);

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

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

 

     internal readonly UniqueNamer Namer;

+    internal readonly SMTLibProverOptions ProverOptions;

 

-    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer) {

+    public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts) {

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

       this.wr = wr;

       this.Namer = namer;

+      this.ProverOptions = opts;

     }

 

     public void Linearise(VCExpr expr, LineariserOptions options) {

@@ -847,8 +849,13 @@ void ObjectInvariant()
         string printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));

         Contract.Assert(printedName!=null);

 

-        // arguments are always terms

-        WriteApplicationTermOnly(printedName, node, options);

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

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

+        } else {

+          // arguments are always terms

+          WriteApplicationTermOnly(printedName, node, options);

+        }

+

         return true;

       }

       

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index a60b01ee..f617e899 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -18,6 +18,8 @@ namespace Microsoft.Boogie.SMTLib
   public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {

 

     private readonly UniqueNamer Namer;

+    private readonly SMTLibProverOptions Options;

+

     [ContractInvariantMethod]

 void ObjectInvariant() 

 {

@@ -29,9 +31,10 @@ void ObjectInvariant()
 }

 

 

-    public TypeDeclCollector(UniqueNamer namer) {

+    public TypeDeclCollector(SMTLibProverOptions opts, UniqueNamer namer) {

       Contract.Requires(namer != null);

       this.Namer = namer;

+      this.Options = opts;

     }

 

     // not used

@@ -102,19 +105,24 @@ void ObjectInvariant()
           Contract.Assert(f != null);

           string printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name));

           Contract.Assert(printedName != null);

-          string decl = ":extrafuns ((" + printedName;

+

+          bool isPred = Options.UsePredicates && f.OutParams[0].TypedIdent.Type.IsBool;

+          string decl = (isPred ? ":extrapreds" : ":extrafuns") + " ((" + printedName;

 

           foreach (Variable v in f.InParams) {

             Contract.Assert(v != null);

             RegisterType(v.TypedIdent.Type);

             decl += " " + TypeToString(v.TypedIdent.Type);

           }

+

+

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

-          foreach (Variable v in f.OutParams) {

-            Contract.Assert(v != null);

-            RegisterType(v.TypedIdent.Type);

-            decl += " " + TypeToString(v.TypedIdent.Type);

-          }

+          if (!isPred)

+            foreach (Variable v in f.OutParams) {

+              Contract.Assert(v != null);

+              RegisterType(v.TypedIdent.Type);

+              decl += " " + TypeToString(v.TypedIdent.Type);

+            }

 

           decl += "))";