diff options
author | qadeer <qadeer@microsoft.com> | 2011-10-05 19:31:21 -0700 |
---|---|---|
committer | qadeer <qadeer@microsoft.com> | 2011-10-05 19:31:21 -0700 |
commit | 7ea78551342ff1a1bfe36e2c7f9eaa44a2096a35 (patch) | |
tree | 39253d3c9014af50b1ec1d0eedb7ebd720ddbd2f /Source/Provers | |
parent | 696796e1dcea137ee9b5c270b233892dd3267155 (diff) |
added membership tests
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 7 |
1 files changed, 5 insertions, 2 deletions
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)
|