diff options
| author |  MichalMoskal <unknown> | 2011-01-18 02:55:38 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-01-18 02:55:38 +0000 |
| commit | 63ea533b33f9820f9672fb54be34f84c96b9365b (patch) | |
| tree | 1dd87859ba08d5b66da116ccf07eff0806c5dfc5 /Source/Provers/TPTP/TypeDeclCollector.cs | |
| parent | 6b1d70967f9b2b87f431dc46212b1189119830ea (diff) | |
Copy SMTLib "prover" as a basis for TPTP "prover".
Diffstat (limited to 'Source/Provers/TPTP/TypeDeclCollector.cs')
| -rw-r--r-- | Source/Provers/TPTP/TypeDeclCollector.cs | 134 |
1 files changed, 134 insertions, 0 deletions
diff --git a/Source/Provers/TPTP/TypeDeclCollector.cs b/Source/Provers/TPTP/TypeDeclCollector.cs new file mode 100644 index 00000000..ab14c0e2 --- /dev/null +++ b/Source/Provers/TPTP/TypeDeclCollector.cs @@ -0,0 +1,134 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie.VCExprAST;
+
+namespace Microsoft.Boogie.TPTP
+{
+ // Visitor for collecting the occurring function symbols in a VCExpr,
+ // and for creating the corresponding declarations
+
+ public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
+
+ private readonly UniqueNamer Namer;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Namer!=null);
+ Contract.Invariant(AllDecls != null);
+ Contract.Invariant(IncDecls != null);
+ Contract.Invariant(KnownFunctions != null);
+ Contract.Invariant(KnownVariables != null);
+}
+
+
+ public TypeDeclCollector(UniqueNamer namer) {
+ Contract.Requires(namer != null);
+ this.Namer = namer;
+ }
+
+ // not used
+ protected override bool StandardResult(VCExpr node, bool arg) {
+ //Contract.Requires(node != null);
+ return true;
+ }
+
+ private readonly List<string/*!>!*/> AllDecls = new List<string/*!*/> ();
+ private readonly List<string/*!>!*/> IncDecls = new List<string/*!*/> ();
+
+ private readonly IDictionary<Function/*!*/, bool>/*!*/ KnownFunctions =
+ new Dictionary<Function/*!*/, bool> ();
+ private readonly IDictionary<VCExprVar/*!*/, bool>/*!*/ KnownVariables =
+ new Dictionary<VCExprVar/*!*/, bool> ();
+
+ public List<string/*!>!*/> AllDeclarations { get {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));
+
+ List<string>/*!>!*/ res = new List<string/*!*/> ();
+ res.AddRange(AllDecls);
+ return res;
+ } }
+
+ public List<string/*!>!*/> GetNewDeclarations() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<List<string>>() ));
+ List<string>/*!>!*/ res = new List<string/*!*/>();
+ res.AddRange(IncDecls);
+ IncDecls.Clear();
+ return res;
+ }
+
+ private void AddDeclaration(string decl) {
+ Contract.Requires(decl != null);
+ AllDecls.Add(decl);
+ IncDecls.Add(decl);
+ }
+
+ public void Collect(VCExpr expr) {
+ Contract.Requires(expr != null);
+ Traverse(expr, true);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+ private static string TypeToString(Type t) {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ return TPTPExprLineariser.TypeToString(t);
+ }
+
+ public override bool Visit(VCExprNAry node, bool arg) {
+ Contract.Requires(node != null);
+ // there are a couple of cases where operators have to be
+ // registered by generating appropriate statements
+
+ VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp;
+ if (op != null && !KnownFunctions.ContainsKey(op.Func)) {
+ Function f = op.Func;
+ Contract.Assert(f!=null);
+ string printedName = Namer.GetName(f, TPTPExprLineariser.MakeIdPrintable(f.Name));
+ Contract.Assert(printedName!=null);
+ string decl = ":extrafuns ((" + printedName;
+
+ foreach (Variable v in f.InParams) {
+ Contract.Assert(v!=null);
+ decl += " " + TypeToString(v.TypedIdent.Type);
+ }
+ Contract.Assert(f.OutParams.Length == 1);
+ foreach (Variable v in f.OutParams) {
+ Contract.Assert(v!=null);
+ decl += " " + TypeToString(v.TypedIdent.Type);
+ }
+
+ decl += "))";
+
+ AddDeclaration(decl);
+ KnownFunctions.Add(f, true);
+ }
+
+ return base.Visit(node, arg);
+ }
+
+ public override bool Visit(VCExprVar node, bool arg) {
+ Contract.Requires(node != null);
+ if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) {
+ string printedName = Namer.GetName(node, TPTPExprLineariser.MakeIdPrintable(node.Name));
+ Contract.Assert(printedName!=null);
+ string decl =
+ ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";
+ AddDeclaration(decl);
+ KnownVariables.Add(node, true);
+ }
+
+ return base.Visit(node, arg);
+ }
+ }
+
+}
\ No newline at end of file |