summaryrefslogtreecommitdiff
path: root/Source/Provers
diff options
context:
space:
mode:
authorGravatar Mike Barnett <mbarnett@microsoft.com>2011-10-31 13:04:13 -0700
committerGravatar Mike Barnett <mbarnett@microsoft.com>2011-10-31 13:04:13 -0700
commit36be8fc06b5d08fcf023a9b095a9ee948afcb94d (patch)
tree01f6ec85d3a99738e9050e29faa63062b5d26e71 /Source/Provers
parent16a9a020f90b1702eabf32a667960b5748bfe0b5 (diff)
Fixed the generation of names for datatype functions to use the API for
getting SMT-approved names. Fixed a bug in VisitDistinctOp where a bad axiom was being generated when no grouping had more than one occurrence.
Diffstat (limited to 'Source/Provers')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs4
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs32
2 files changed, 20 insertions, 16 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d5e9b797..0c9a7513 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -201,10 +201,10 @@ namespace Microsoft.Boogie.SMTLib
datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";
foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
if (f.InParams.Length == 0) {
- datatypeString += f.Name + " ";
+ datatypeString += Namer.GetQuotedName(f, f.Name) + " ";
}
else {
- datatypeString += "(" + f.Name + " ";
+ datatypeString += "(" + Namer.GetQuotedName(f, f.Name) + " ";
foreach (Variable v in f.InParams) {
datatypeString += "(" + v.Name + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
}
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f4973efd..8d4a4256 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -483,23 +483,27 @@ namespace Microsoft.Boogie.SMTLib
ExprLineariser.Linearise(VCExpressionGenerator.True, options);
} else {
var groupings = node.GroupBy(e => e.Type).Where(g => g.Count() > 1).ToArray();
+ if (groupings.Length == 0) {
+ ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+ } else {
+ if (groupings.Length > 1)
+ wr.Write("(and ");
+
+ foreach (var g in groupings) {
+ wr.Write("(distinct");
+ foreach (VCExpr e in g) {
+ Contract.Assert(e != null);
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options);
+ }
+ wr.Write(")");
+ }
- if (groupings.Length > 1)
- wr.Write("(and ");
+ if (groupings.Length > 1)
+ wr.Write(")");
- foreach (var g in groupings) {
- wr.Write("(distinct");
- foreach (VCExpr e in g) {
- Contract.Assert(e != null);
- wr.Write(" ");
- ExprLineariser.Linearise(e, options);
- }
- wr.Write(")");
+ wr.Write("\n");
}
-
- if (groupings.Length > 1)
- wr.Write(")");
- wr.Write("\n");
}
return true;