From 7ea78551342ff1a1bfe36e2c7f9eaa44a2096a35 Mon Sep 17 00:00:00 2001
From: qadeer <qadeer@microsoft.com>
Date: Wed, 5 Oct 2011 19:31:21 -0700
Subject: added membership tests

---
 Source/BoogieDriver/BoogieDriver.cs       | 1 +
 Source/Provers/SMTLib/SMTLibLineariser.cs | 7 +++++--
 Test/datatypes/t1.bpl                     | 6 +++++-
 3 files changed, 11 insertions(+), 3 deletions(-)

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index 722bc99e..b5c45943 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -157,6 +157,7 @@ namespace Microsoft.Boogie {
         Formal inv = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);
         Formal outv = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "", Type.Bool), false);
         Function isConstructor = new Function(f.tok, "is#" + f.Name, new VariableSeq(inv), outv);
+        isConstructor.AddAttribute("membership");
         program.TopLevelDeclarations.Add(isConstructor);
       }
     }
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f008bb88..f4973efd 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -655,10 +655,13 @@ namespace Microsoft.Boogie.SMTLib
         return true;
       }
 
-      private string ExtractDatatypeSelector(Function func) {
+      private string ExtractDatatype(Function func) {
         if (QKeyValue.FindBoolAttribute(func.Attributes, "selector")) {
           return func.Name.Remove(func.Name.IndexOf('#'));
         }
+        else if (QKeyValue.FindBoolAttribute(func.Attributes, "membership")) {
+          return func.Name.Replace('#', '-');
+        }
         else {
           return null;
         }
@@ -670,7 +673,7 @@ namespace Microsoft.Boogie.SMTLib
         string printedName;
 
         var builtin = ExtractBuiltin(op.Func);
-        var datatype = ExtractDatatypeSelector(op.Func);
+        var datatype = ExtractDatatype(op.Func);
         if (builtin != null)
           printedName = builtin;
         else if (datatype != null)
diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl
index 61409465..b56e26ae 100644
--- a/Test/datatypes/t1.bpl
+++ b/Test/datatypes/t1.bpl
@@ -16,5 +16,9 @@ procedure foo()
   assert value#node(node(x, nil())) == x;
   assert children#node(node(x, nil())) == nil();
   
-  assert (cons(leaf(), nil()) == nil());
+  assert (cons(leaf(), nil()) != nil());
+
+  assert is#nil(nil());
+
+  assert is#node(leaf());
 }
\ No newline at end of file
-- 
cgit v1.2.3