From 4760c55b4a09e4b11039e9537371a98f657d7704 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 11 Feb 2011 19:38:00 +0000
Subject: Add USE_PREDICATES option to TPTP and SMT provers

---
 Source/Provers/SMTLib/ProverInterface.cs | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'Source/Provers/SMTLib/ProverInterface.cs')

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) {
-- 
cgit v1.2.3