From f82f137fe74fe6200d172b4b2751b07eb6ff34bf Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Tue, 17 Apr 2012 12:35:29 -0700
Subject: various changes for using unsat cores in Houdini

---
 Source/Provers/SMTLib/ProverInterface.cs   | 16 +++++++++++++---
 Source/Provers/SMTLib/TypeDeclCollector.cs |  5 +++++
 2 files changed, 18 insertions(+), 3 deletions(-)

(limited to 'Source/Provers')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 08322ebb..014af458 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -78,14 +78,14 @@ namespace Microsoft.Boogie.SMTLib
 
       SetupProcess();
 
-      if (CommandLineOptions.Clo.StratifiedInlining > 0)
+      if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)
       {
           // Prepare for ApiChecker usage
           if (options.LogFilename != null && currentLogFile == null)
           {
               currentLogFile = OpenOutputFile("");
           }
-          if (CommandLineOptions.Clo.ProcedureCopyBound > 0)
+          if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.ContractInfer)
           {
               SendThisVC("(set-option :produce-unsat-cores true)");
               this.usingUnsatCore = true;
@@ -770,6 +770,14 @@ namespace Microsoft.Boogie.SMTLib
         SendThisVC(a);
     }
 
+    public override void DefineMacro(Function fun, VCExpr vc) {
+      DeclCollector.AddFunction(fun);
+      string name = Namer.GetName(fun, fun.Name);
+      string a = "(define-fun " + name + "() Bool " + VCExpr2String(vc, 1) + ")";
+      AssertAxioms();
+      SendThisVC(a);
+    }
+
     public override void AssertAxioms()
     {
         FlushAxioms();
@@ -805,7 +813,9 @@ namespace Microsoft.Boogie.SMTLib
             nameCounter++;
             nameToAssumption.Add(name, i);
 
-            SendThisVC(string.Format("(assert (! {0} :named {1}))", VCExpr2String(vc, 1), name));
+            string vcString = VCExpr2String(vc, 1);
+            AssertAxioms();
+            SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
             i++;
         }
         Check();
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 05a6caf3..a4bdee51 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -164,6 +164,11 @@ void ObjectInvariant()
       return TypeToString(t);
     }
 
+    public void AddFunction(Function func) {
+      if (KnownFunctions.Contains(func))
+        return;
+      KnownFunctions.Add(func);
+    }
 
     public override bool Visit(VCExprNAry node, bool arg) {
       Contract.Requires(node != null);
-- 
cgit v1.2.3