From 9a9991f2131de8e78035581ea2569ba187318ff0 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 7 May 2013 17:40:40 -0700 Subject: Adding fixedpoint engine backend --- Source/Provers/SMTLib/TypeDeclCollector.cs | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'Source/Provers/SMTLib/TypeDeclCollector.cs') diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index bff949ea..9d908138 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -20,6 +20,7 @@ namespace Microsoft.Boogie.SMTLib private readonly UniqueNamer Namer; private readonly SMTLibProverOptions Options; + private HashSet/*!*/ RegisteredRelations = new HashSet(); [ContractInvariantMethod] void ObjectInvariant() @@ -170,6 +171,13 @@ void ObjectInvariant() KnownFunctions.Add(func); } + public void RegisterRelation(Function func) + { + if (RegisteredRelations.Contains(func)) + return; + RegisteredRelations.Add(func); + } + public override bool Visit(VCExprNAry node, bool arg) { Contract.Requires(node != null); @@ -190,7 +198,11 @@ void ObjectInvariant() Contract.Assert(f.OutParams.Length == 1); var argTypes = f.InParams.Cast().MapConcat(p => TypeToStringReg(p.TypedIdent.Type), " "); - string decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")"; + string decl; + if(RegisteredRelations.Contains(op.Func)) + decl = "(declare-rel " + printedName + " (" + argTypes + ") " + ")"; + else + decl = "(declare-fun " + printedName + " (" + argTypes + ") " + TypeToStringReg(f.OutParams[0].TypedIdent.Type) + ")"; AddDeclaration(decl); } KnownFunctions.Add(f); -- cgit v1.2.3