diff options
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.cs | 24 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 40 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 12 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 22 | ||||
| -rw-r--r-- | Test/datatypes/t1.bpl | 20 |
5 files changed, 114 insertions, 4 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs index 5a1f8dc5..722bc99e 100644 --- a/Source/BoogieDriver/BoogieDriver.cs +++ b/Source/BoogieDriver/BoogieDriver.cs @@ -139,6 +139,28 @@ namespace Microsoft.Boogie { Dafny
};
+ static void CreateDatatypeSelectors(Program program) {
+ List<Function> constructors = new List<Function>();
+ foreach (Declaration decl in program.TopLevelDeclarations) {
+ if (decl is Function && QKeyValue.FindBoolAttribute(decl.Attributes, "constructor"))
+ constructors.Add((Function)decl);
+ }
+
+ foreach (Function f in constructors) {
+ foreach (Variable v in f.InParams) {
+ Formal inVar = new Formal(Token.NoToken, f.OutParams[0].TypedIdent, true);
+ Formal outVar = new Formal(Token.NoToken, v.TypedIdent, false);
+ Function selector = new Function(f.tok, v.Name + "#" + f.Name, new VariableSeq(inVar), outVar);
+ selector.AddAttribute("selector");
+ program.TopLevelDeclarations.Add(selector);
+ }
+ 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);
+ program.TopLevelDeclarations.Add(isConstructor);
+ }
+ }
+
static void ProcessFiles(List<string> fileNames) {
Contract.Requires(cce.NonNullElements(fileNames));
using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count - 1])) {
@@ -150,6 +172,8 @@ namespace Microsoft.Boogie { PrintBplFile(CommandLineOptions.Clo.PrintFile, program, false);
}
+ CreateDatatypeSelectors(program);
+
PipelineOutcome oc = ResolveAndTypecheck(program, fileNames[fileNames.Count - 1]);
if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 9b4429f9..acad7833 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -161,6 +161,32 @@ namespace Microsoft.Boogie.SMTLib SendCommon("; done setting options\n");
SendCommon(_backgroundPredicates);
+
+
+ if (ctx.KnownDatatypeConstructors.Count > 0) {
+ string datatypeString = "";
+ foreach (CtorType datatype in ctx.KnownDatatypeConstructors.Keys) {
+ datatypeString += "(" + SMTLibExprLineariser.TypeToString(datatype) + " ";
+ foreach (Function f in ctx.KnownDatatypeConstructors[datatype]) {
+ if (f.InParams.Length == 0) {
+ datatypeString += f.Name + " ";
+ }
+ else {
+ datatypeString += "(" + f.Name + " ";
+ foreach (Variable v in f.InParams) {
+ datatypeString += "(" + v.Name + " " + DeclCollector.TypeToStringReg(v.TypedIdent.Type) + ") ";
+ }
+ datatypeString += ") ";
+ }
+ }
+ datatypeString += ") ";
+ }
+ List<string> decls = DeclCollector.GetNewDeclarations();
+ foreach (string decl in decls) {
+ SendCommon(decl);
+ }
+ SendCommon("(declare-datatypes () (" + datatypeString + "))");
+ }
}
if (!AxiomsAreSetup) {
@@ -524,6 +550,8 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.Collect(sortedExpr);
FeedTypeDeclsToProver();
+
+
AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, options));
string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, options);
Contract.Assert(res != null);
@@ -638,6 +666,8 @@ namespace Microsoft.Boogie.SMTLib {
internal SMTLibProcessTheoremProver parent;
+ public readonly Dictionary<CtorType, List<Function>> KnownDatatypeConstructors = new Dictionary<CtorType, List<Function>>();
+
public SMTLibProverContext(VCExpressionGenerator gen,
VCGenerationOptions genOptions)
: base(gen, genOptions)
@@ -662,6 +692,16 @@ namespace Microsoft.Boogie.SMTLib }
return parent.Namer.Lookup(var);
}
+
+ public override void DeclareFunction(Function f, string attributes) {
+ if (QKeyValue.FindBoolAttribute(f.Attributes, "constructor")) {
+ CtorType datatype = (CtorType) f.OutParams[0].TypedIdent.Type;
+ if (!KnownDatatypeConstructors.ContainsKey(datatype))
+ KnownDatatypeConstructors[datatype] = new List<Function>();
+ KnownDatatypeConstructors[datatype].Add(f);
+ }
+ base.DeclareFunction(f, attributes);
+ }
}
public class Factory : ProverFactory
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 36df38e3..f008bb88 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -655,14 +655,26 @@ namespace Microsoft.Boogie.SMTLib return true;
}
+ private string ExtractDatatypeSelector(Function func) {
+ if (QKeyValue.FindBoolAttribute(func.Attributes, "selector")) {
+ return func.Name.Remove(func.Name.IndexOf('#'));
+ }
+ else {
+ return null;
+ }
+ }
+
public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {
VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
Contract.Assert(op != null);
string printedName;
var builtin = ExtractBuiltin(op.Func);
+ var datatype = ExtractDatatypeSelector(op.Func);
if (builtin != null)
printedName = builtin;
+ else if (datatype != null)
+ printedName = datatype;
else
printedName = ExprLineariser.Namer.GetQuotedName(op.Func, op.Func.Name);
Contract.Assert(printedName != null);
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index c64dbf5e..23475242 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -55,7 +55,6 @@ void ObjectInvariant() private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions = new HashSet<string>();
private readonly HashSet<string> KnownLBL = new HashSet<string>();
-
public List<string/*!>!*/> AllDeclarations { get {
Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));
@@ -92,7 +91,7 @@ void ObjectInvariant() return SMTLibExprLineariser.TypeToString(t);
}
- private string TypeToStringReg(Type t)
+ public string TypeToStringReg(Type t)
{
RegisterType(t);
return TypeToString(t);
@@ -105,7 +104,7 @@ void ObjectInvariant() else if (node.Op is VCExprSelectOp) RegisterSelect(node);
else {
VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
- if (op != null && !KnownFunctions.Contains(op.Func)) {
+ if (op != null && !IsDatatypeConstructor(op.Func) && !KnownFunctions.Contains(op.Func)) {
Function f = op.Func;
Contract.Assert(f != null);
@@ -184,13 +183,28 @@ void ObjectInvariant() if (type.IsBool || type.IsInt || type.IsBv)
return;
- if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic) {
+ if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic && !IsDatatype(type)) {
AddDeclaration("(declare-sort " + TypeToString(type) + " 0)");
KnownTypes.Add(type);
return;
}
}
+ public static bool IsDatatype(Type t) {
+ CtorType ctorType = t.AsCtor;
+ if (t == null)
+ return false;
+ return QKeyValue.FindBoolAttribute(ctorType.Decl.Attributes, "datatype");
+ }
+
+ public static bool IsDatatypeConstructor(Function f) {
+ return QKeyValue.FindBoolAttribute(f.Attributes, "constructor");
+ }
+
+ public static bool IsDatatypeSelector(Function f) {
+ return QKeyValue.FindBoolAttribute(f.Attributes, "selector");
+ }
+
private void RegisterSelect(VCExprNAry node)
{
RegisterType(node[0].Type);
diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl new file mode 100644 index 00000000..61409465 --- /dev/null +++ b/Test/datatypes/t1.bpl @@ -0,0 +1,20 @@ +type TT;
+type {:datatype} Tree;
+function {:constructor} leaf() : Tree;
+function {:constructor} node(value:TT, children:TreeList) : Tree;
+
+type {:datatype} TreeList;
+function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;
+function {:constructor} nil() : TreeList;
+
+procedure foo()
+{
+ var a: Tree;
+ var b: TreeList;
+ var x: TT;
+
+ assert value#node(node(x, nil())) == x;
+ assert children#node(node(x, nil())) == nil();
+
+ assert (cons(leaf(), nil()) == nil());
+}
\ No newline at end of file |