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 | |
| parent | 6b1d70967f9b2b87f431dc46212b1189119830ea (diff) | |
Copy SMTLib "prover" as a basis for TPTP "prover".
| -rw-r--r-- | Source/Boogie.sln | 21 | ||||
| -rw-r--r-- | Source/Provers/TPTP/ProverInterface.cs | 322 | ||||
| -rw-r--r-- | Source/Provers/TPTP/TPTP.csproj | 94 | ||||
| -rw-r--r-- | Source/Provers/TPTP/TPTPLineariser.cs | 827 | ||||
| -rw-r--r-- | Source/Provers/TPTP/TypeDeclCollector.cs | 134 |
5 files changed, 1398 insertions, 0 deletions
diff --git a/Source/Boogie.sln b/Source/Boogie.sln index 3f459d16..4578a1a3 100644 --- a/Source/Boogie.sln +++ b/Source/Boogie.sln @@ -37,6 +37,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "Model\Model.csproj EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelper\ParserHelper.csproj", "{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}"
EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TPTP", "Provers\TPTP\TPTP.csproj", "{A598ED5A-93AD-4125-A555-3921A2F936FA}"
+EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|.NET = Debug|.NET
@@ -365,6 +367,24 @@ Global {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Debug|x86.ActiveCfg = Debug|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|.NET.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Any CPU.Build.0 = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|Mixed Platforms.Build.0 = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.Release|x86.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|.NET.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Any CPU.Build.0 = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU
+ {A598ED5A-93AD-4125-A555-3921A2F936FA}.z3apidebug|x86.ActiveCfg = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
@@ -375,5 +395,6 @@ Global {9B163AA3-36BC-4AFB-88AB-79BC9E97E401} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{FEE9F01B-9722-4A76-A24B-72A4016DFA8E} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
{966DD87B-A29D-4F3C-9406-F680A61DC0E0} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
+ {A598ED5A-93AD-4125-A555-3921A2F936FA} = {B758C1E3-824A-439F-AA2F-0BA1143E8C8D}
EndGlobalSection
EndGlobal
diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs new file mode 100644 index 00000000..d4bc7dc8 --- /dev/null +++ b/Source/Provers/TPTP/ProverInterface.cs @@ -0,0 +1,322 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading;
+using System.IO;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using Microsoft.Boogie;
+using Microsoft.Boogie.VCExprAST;
+using Microsoft.Boogie.Clustering;
+using Microsoft.Boogie.TypeErasure;
+using Microsoft.Boogie.Simplify;
+
+namespace Microsoft.Boogie.TPTP
+{
+ public class TPTPProcessTheoremProver : LogProverInterface
+ {
+ private readonly DeclFreeProverContext ctx;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(ctx != null);
+ Contract.Invariant(AxBuilder != null);
+ Contract.Invariant(Namer != null);
+ Contract.Invariant(DeclCollector != null);
+ Contract.Invariant(BadBenchmarkWords != null);
+ Contract.Invariant(cce.NonNullElements(Axioms));
+ Contract.Invariant(cce.NonNullElements(TypeDecls));
+ Contract.Invariant(_backgroundPredicates != null);
+
+ }
+
+
+ [NotDelayed]
+ public TPTPProcessTheoremProver(ProverOptions options, VCExpressionGenerator gen,
+ DeclFreeProverContext ctx)
+ : base(options, "", "", "", "", gen)
+ {
+ Contract.Requires(options != null);
+ Contract.Requires(gen != null);
+ Contract.Requires(ctx != null);
+ InitializeGlobalInformation("UnivBackPred2.smt");
+
+ this.ctx = ctx;
+
+ TypeAxiomBuilder axBuilder;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ axBuilder = new TypeAxiomBuilderArguments(gen);
+ break;
+ default:
+ axBuilder = new TypeAxiomBuilderPremisses(gen);
+ break;
+ }
+ axBuilder.Setup();
+ AxBuilder = axBuilder;
+ UniqueNamer namer = new UniqueNamer();
+ Namer = namer;
+ this.DeclCollector = new TypeDeclCollector(namer);
+
+ }
+
+ public override ProverContext Context
+ {
+ get
+ {
+ Contract.Ensures(Contract.Result<ProverContext>() != null);
+
+ return ctx;
+ }
+ }
+
+ private readonly TypeAxiomBuilder AxBuilder;
+ private readonly UniqueNamer Namer;
+ private readonly TypeDeclCollector DeclCollector;
+
+ private void FeedTypeDeclsToProver()
+ {
+ foreach (string s in DeclCollector.GetNewDeclarations()) {
+ Contract.Assert(s != null);
+ AddTypeDecl(s);
+ }
+ }
+
+ public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
+ {
+ //Contract.Requires(descriptiveName != null);
+ //Contract.Requires(vc != null);
+ //Contract.Requires(handler != null);
+ TextWriter output = OpenOutputFile(descriptiveName);
+ Contract.Assert(output != null);
+
+ string name =
+ MakeBenchmarkNameSafe(TPTPExprLineariser.MakeIdPrintable(descriptiveName));
+ Contract.Assert(name != null);
+ WriteLineAndLog(output, "(benchmark " + name);
+ WriteLineAndLog(output, _backgroundPredicates);
+
+ if (!AxiomsAreSetup) {
+ AddAxiom(VCExpr2String(ctx.Axioms, -1));
+ AxiomsAreSetup = true;
+ }
+
+ string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")";
+ string prelude = ctx.GetProverCommands(true);
+ Contract.Assert(prelude != null);
+ WriteLineAndLog(output, prelude);
+
+ foreach (string s in TypeDecls) {
+ Contract.Assert(s != null);
+ WriteLineAndLog(output, s);
+ }
+ foreach (string s in Axioms) {
+ Contract.Assert(s != null);
+ WriteLineAndLog(output, ":assumption");
+ WriteLineAndLog(output, s);
+ }
+
+ WriteLineAndLog(output, vcString);
+ WriteLineAndLog(output, ")");
+
+ output.Close();
+ }
+
+ // certain words that should not occur in the name of a benchmark
+ // because some solvers don't like them
+ private readonly static List<string/*!>!*/> BadBenchmarkWords = new List<string/*!*/>();
+ static TPTPProcessTheoremProver()
+ {
+ BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray");
+ }
+
+ private string MakeBenchmarkNameSafe(string name)
+ {
+ Contract.Requires(name != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ for (int i = 0; i < BadBenchmarkWords.Count; i = i + 2)
+ name = name.Replace(BadBenchmarkWords[i], BadBenchmarkWords[i + 1]);
+ return name;
+ }
+
+ private TextWriter OpenOutputFile(string descriptiveName)
+ {
+ Contract.Requires(descriptiveName != null);
+ Contract.Ensures(Contract.Result<TextWriter>() != null);
+
+ string filename = CommandLineOptions.Clo.SMTLibOutputPath;
+ filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
+ return new StreamWriter(filename, false);
+ }
+
+ private void WriteLineAndLog(TextWriter output, string msg)
+ {
+ Contract.Requires(output != null);
+ Contract.Requires(msg != null);
+ LogActivity(msg);
+ output.WriteLine(msg);
+ }
+
+ [NoDefaultContract]
+ public override Outcome CheckOutcome(ErrorHandler handler)
+ { //Contract.Requires(handler != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
+ return Outcome.Undetermined;
+ }
+
+ protected string VCExpr2String(VCExpr expr, int polarity)
+ {
+ Contract.Requires(expr != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ DateTime start = DateTime.Now;
+ if (CommandLineOptions.Clo.Trace)
+ Console.Write("Linearising ... ");
+
+ // handle the types in the VCExpr
+ TypeEraser eraser;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);
+ break;
+ default:
+ eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);
+ break;
+ }
+ Contract.Assert(eraser != null);
+ VCExpr exprWithoutTypes = eraser.Erase(expr, polarity);
+ Contract.Assert(exprWithoutTypes != null);
+
+ LetBindingSorter letSorter = new LetBindingSorter(gen);
+ Contract.Assert(letSorter != null);
+ VCExpr sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
+ Contract.Assert(sortedExpr != null);
+ VCExpr sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
+ Contract.Assert(sortedAxioms != null);
+
+ DeclCollector.Collect(sortedAxioms);
+ DeclCollector.Collect(sortedExpr);
+ FeedTypeDeclsToProver();
+
+ AddAxiom(TPTPExprLineariser.ToString(sortedAxioms, Namer));
+ string res = TPTPExprLineariser.ToString(sortedExpr, Namer);
+ Contract.Assert(res != null);
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.Now;
+ TimeSpan elapsed = end - start;
+ Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds);
+ }
+ return res;
+ }
+
+ // the list of all known axioms, where have to be included in each
+ // verification condition
+ private readonly List<string/*!>!*/> Axioms = new List<string/*!*/>();
+ private bool AxiomsAreSetup = false;
+
+
+
+
+ // similarly, a list of function/predicate declarations
+ private readonly List<string/*!>!*/> TypeDecls = new List<string/*!*/>();
+
+ protected void AddAxiom(string axiom)
+ {
+ Contract.Requires(axiom != null);
+ Axioms.Add(axiom);
+ // if (thmProver != null) {
+ // LogActivity(":assume " + axiom);
+ // thmProver.AddAxioms(axiom);
+ // }
+ }
+
+ protected void AddTypeDecl(string decl)
+ {
+ Contract.Requires(decl != null);
+ TypeDecls.Add(decl);
+ // if (thmProver != null) {
+ // LogActivity(decl);
+ // thmProver.Feed(decl, 0);
+ // }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////
+
+ private static string _backgroundPredicates;
+
+ static void InitializeGlobalInformation(string backgroundPred)
+ {
+ Contract.Requires(backgroundPred != null);
+ Contract.Ensures(_backgroundPredicates != null);
+ //throws ProverException, System.IO.FileNotFoundException;
+ if (_backgroundPredicates == null) {
+ string codebaseString =
+ cce.NonNull(Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
+
+ // Initialize '_backgroundPredicates'
+ string univBackPredPath = Path.Combine(codebaseString, backgroundPred);
+ using (StreamReader reader = new System.IO.StreamReader(univBackPredPath)) {
+ _backgroundPredicates = reader.ReadToEnd();
+ }
+ }
+ }
+ }
+
+ public class Factory : ProverFactory
+ {
+
+ public override object SpawnProver(ProverOptions options, object ctxt)
+ {
+ //Contract.Requires(ctxt != null);
+ //Contract.Requires(options != null);
+ Contract.Ensures(Contract.Result<object>() != null);
+
+ return this.SpawnProver(options,
+ cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,
+ cce.NonNull((DeclFreeProverContext)ctxt));
+ }
+
+ public override object NewProverContext(ProverOptions options)
+ {
+ //Contract.Requires(options != null);
+ Contract.Ensures(Contract.Result<object>() != null);
+
+ if (CommandLineOptions.Clo.BracketIdsInVC < 0) {
+ CommandLineOptions.Clo.BracketIdsInVC = 0;
+ }
+
+ VCExpressionGenerator gen = new VCExpressionGenerator();
+ List<string>/*!>!*/ proverCommands = new List<string/*!*/>();
+ // TODO: what is supported?
+ // proverCommands.Add("all");
+ // proverCommands.Add("simplify");
+ // proverCommands.Add("simplifyLike");
+ VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
+ Contract.Assert(genOptions != null);
+
+ return new DeclFreeProverContext(gen, genOptions);
+ }
+
+ protected virtual TPTPProcessTheoremProver SpawnProver(ProverOptions options,
+ VCExpressionGenerator gen,
+ DeclFreeProverContext ctx)
+ {
+ Contract.Requires(options != null);
+ Contract.Requires(gen != null);
+ Contract.Requires(ctx != null);
+ Contract.Ensures(Contract.Result<TPTPProcessTheoremProver>() != null);
+
+ return new TPTPProcessTheoremProver(options, gen, ctx);
+ }
+ }
+}
diff --git a/Source/Provers/TPTP/TPTP.csproj b/Source/Provers/TPTP/TPTP.csproj new file mode 100644 index 00000000..f83c38ff --- /dev/null +++ b/Source/Provers/TPTP/TPTP.csproj @@ -0,0 +1,94 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>8.0.30703</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{A598ED5A-93AD-4125-A555-3921A2F936FA}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Microsoft.Boogie.TPTP</RootNamespace>
+ <AssemblyName>Provers.TPTP</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <TargetFrameworkProfile>Client</TargetFrameworkProfile>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="System" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Xml.Linq" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="ProverInterface.cs" />
+ <Compile Include="..\..\version.cs" />
+ <Compile Include="TPTPLineariser.cs" />
+ <Compile Include="TypeDeclCollector.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <ProjectReference Include="..\..\AbsInt\AbsInt.csproj">
+ <Project>{0EFA3E43-690B-48DC-A72C-384A3EA7F31F}</Project>
+ <Name>AbsInt</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\AIFramework\AIFramework.csproj">
+ <Project>{39B0658D-C955-41C5-9A43-48C97A1EF5FD}</Project>
+ <Name>AIFramework</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
+ <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
+ <Name>Basetypes</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj">
+ <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+ <Name>CodeContractsExtender</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\Core\Core.csproj">
+ <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
+ <Name>Core</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
+ <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
+ <Name>VCExpr</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">
+ <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
+ <Name>VCGeneration</Name>
+ </ProjectReference>
+ <ProjectReference Include="..\Simplify\Simplify.csproj">
+ <Project>{FEE9F01B-9722-4A76-A24B-72A4016DFA8E}</Project>
+ <Name>Simplify</Name>
+ </ProjectReference>
+ </ItemGroup>
+ <ItemGroup>
+ <Folder Include="Properties\" />
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs new file mode 100644 index 00000000..f1ac4f33 --- /dev/null +++ b/Source/Provers/TPTP/TPTPLineariser.cs @@ -0,0 +1,827 @@ +//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.IO;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+// Method to turn VCExprs into strings that can be fed into TPTP provers.
+// This is currently quite similar to the
+// SimplifyLikeLineariser (but the code is independent)
+
+namespace Microsoft.Boogie.TPTP
+{
+
+ // Options for the linearisation
+ public class LineariserOptions {
+
+ public readonly bool AsTerm;
+ public LineariserOptions SetAsTerm(bool newVal) {
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
+ if (newVal)
+ return DefaultTerm;
+ else
+ return Default;
+ }
+
+ internal LineariserOptions(bool asTerm) {
+ this.AsTerm = asTerm;
+ }
+
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Default!=null);
+ Contract.Invariant(DefaultTerm!=null);
+}
+
+ public static readonly LineariserOptions Default = new LineariserOptions (false);
+ internal static readonly LineariserOptions DefaultTerm = new LineariserOptions (true);
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for expressions. The result (bool) is currently not used for anything
+ public class TPTPExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {
+
+ public static string ToString(VCExpr e, UniqueNamer namer) {
+ Contract.Requires(e != null);
+ Contract.Requires(namer != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ StringWriter sw = new StringWriter();
+ TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer);
+ Contract.Assert(lin!=null);
+ lin.Linearise(e, LineariserOptions.Default);
+ return cce.NonNull(sw.ToString());
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ private readonly TextWriter wr;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(wr!=null);
+ Contract.Invariant(Namer != null);
+}
+
+ private TPTPOpLineariser OpLinObject = null;
+ private IVCExprOpVisitor<bool, LineariserOptions>/*!>!*/ OpLineariser { get {
+ Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool,LineariserOptions>>() !=null);
+
+ if (OpLinObject == null)
+ OpLinObject = new TPTPOpLineariser(this, wr);
+ return OpLinObject;
+ } }
+
+ internal readonly UniqueNamer Namer;
+
+ public TPTPExprLineariser(TextWriter wr, UniqueNamer namer) {
+ Contract.Requires(wr != null);Contract.Requires(namer != null);
+ this.wr = wr;
+ this.Namer = namer;
+ }
+
+ public void Linearise(VCExpr expr, LineariserOptions options) {
+ Contract.Requires(expr != null);
+ Contract.Requires(options != null);
+ expr.Accept<bool, LineariserOptions>(this, options);
+ }
+
+ public void LineariseAsTerm(VCExpr expr, LineariserOptions options) {
+ Contract.Requires(expr != null);
+ Contract.Requires(options != null);
+ Linearise(expr, options.SetAsTerm(true));
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ internal static string TypeToString(Type t) {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ if (t.IsBool)
+ return "TermBool";
+ else if (t.IsInt)
+ return "Int";
+ else if (t.IsBv) {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ } // bitvectors are currently not handled for SMT-Lib solvers
+ else {
+ // at this point, only the types U, T should be left
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+ t.Emit(stream);
+ }
+ return "boogie" + buffer.ToString();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public static string MakeIdPrintable(string s) {
+ Contract.Requires(s != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ // make sure that no keywords are used as identifiers
+ switch(s) {
+ case andName:
+ case orName:
+ case notName:
+ case impliesName:
+ case iffName:
+ case eqName:
+ case distinctName:
+ case TRUEName:
+ case FALSEName:
+ case "Array":
+ s = "nonkeyword_" + s;
+ break;
+ }
+
+ string newS = "";
+ foreach (char ch in s) {
+ if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_')
+ newS = newS + ch;
+ else
+ // replace everything else with a .
+ newS = newS + '.';
+ }
+
+ // ensure that the first character is not . or _ (some SMT-solvers do
+ // not like that, e.g., yices and cvc3)
+ if (newS[0] == '.' || newS[0] == '_')
+ newS = "x" + newS;
+
+ return newS;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// The name for logical conjunction in Simplify
+ /// </summary>
+ internal const string andName = "and"; // conjunction
+ internal const string orName = "or"; // disjunction
+ internal const string notName = "not"; // negation
+ internal const string impliesName = "implies"; // implication
+ internal const string iteName = "ite"; // if-then-else
+ internal const string iffName = "iff"; // logical equivalence
+ internal const string eqName = "="; // equality
+ internal const string lessName = "<";
+ internal const string greaterName = ">";
+ internal const string atmostName = "<=";
+ internal const string atleastName = ">=";
+ internal const string TRUEName = "true"; // nullary predicate that is always true
+ internal const string FALSEName = "false"; // nullary predicate that is always false
+ internal const string subtypeName = "UOrdering2";
+ internal const string subtypeArgsName = "UOrdering3";
+
+ internal const string distinctName = "distinct";
+
+ internal const string boolTrueName = "boolTrue";
+ internal const string boolFalseName = "boolFalse";
+ internal const string boolAndName = "boolAnd";
+ internal const string boolOrName = "boolOr";
+ internal const string boolNotName = "boolNot";
+ internal const string boolIffName = "boolIff";
+ internal const string boolImpliesName = "boolImplies";
+ internal const string boolIteName = "ite";
+ internal const string termUEqual = "UEqual";
+ internal const string termTEqual = "TEqual";
+ internal const string termIntEqual = "IntEqual";
+ internal const string termLessName = "intLess";
+ internal const string termGreaterName = "intGreater";
+ internal const string termAtmostName = "intAtMost";
+ internal const string termAtleastName = "intAtLeast";
+ internal const string intAddName = "+";
+ internal const string intSubName = "-";
+ internal const string intMulName = "*";
+ internal const string intDivName = "boogieIntDiv";
+ internal const string intModName = "boogieIntMod";
+
+ internal void AssertAsTerm(string x, LineariserOptions options) {
+ Contract.Requires(x != null);
+ Contract.Requires(options != null);
+ if (!options.AsTerm)
+ System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");
+ }
+
+ internal void AssertAsFormula(string x, LineariserOptions options) {
+ Contract.Requires(x != null);
+ Contract.Requires(options != null);
+ if (options.AsTerm)
+ System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLiteral node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ if (options.AsTerm) {
+
+ if (node == VCExpressionGenerator.True)
+ wr.Write("{0}", boolTrueName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write("{0}", boolFalseName);
+ else if (node is VCExprIntLit) {
+ // some SMT-solvers do not understand negative literals
+ // (e.g., yices)
+ BigNum lit = ((VCExprIntLit)node).Val;
+ if (lit.IsNegative)
+ wr.Write("({0} 0 {1})", intSubName, lit.Abs);
+ else
+ wr.Write(lit);
+ } else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+
+ } else {
+
+ if (node == VCExpressionGenerator.True)
+ wr.Write("{0}", TRUEName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write("{0}", FALSEName);
+ else if (node is VCExprIntLit) {
+ System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");
+ } else
+ {Contract.Assert(false); throw new cce.UnreachableException();}
+
+ }
+
+ return true;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ VCExprOp op = node.Op;
+ Contract.Assert(op!=null);
+
+ if (!options.AsTerm &&
+ (op.Equals(VCExpressionGenerator.AndOp) ||
+ op.Equals(VCExpressionGenerator.OrOp))) {
+ // handle these operators without recursion
+
+ wr.Write("({0}",
+ op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);
+ IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);
+ Contract.Assert(enumerator!=null);
+ while (enumerator.MoveNext()) {
+ VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ wr.Write(" ");
+ Linearise(cce.NonNull((VCExpr)enumerator.Current), options);
+ }
+ }
+
+ wr.Write(")");
+
+ return true;
+ }
+
+ return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprVar node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ string printedName = Namer.GetName(node, MakeIdPrintable(node.Name));
+ Contract.Assert(printedName!=null);
+
+ if (options.AsTerm ||
+ // formula variables are easy to identify in SMT-Lib
+ printedName[0] == '$')
+ wr.Write("{0}", printedName);
+ else
+ wr.Write("({0} {1} {2})", eqName, printedName, boolTrueName);
+
+ return true;
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprQuantifier node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ AssertAsFormula(node.Quan.ToString(), options);
+ Contract.Assert(node.TypeParameters.Count == 0);
+
+ Namer.PushScope(); try {
+
+ string kind = node.Quan == Quantifier.ALL ? "forall" : "exists";
+ wr.Write("({0} ", kind);
+
+ for (int i = 0; i < node.BoundVars.Count; i++)
+ {
+ VCExprVar var = node.BoundVars[i];
+ Contract.Assert(var!=null);
+ // ensure that the variable name starts with ?
+ string printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));
+ Contract.Assert(printedName!=null);
+ Contract.Assert(printedName[0] == '?');
+ wr.Write("({0} {1}) ", printedName, TypeToString(var.Type));
+ }
+
+ /* if (options.QuantifierIds) {
+ // only needed for Z3
+ VCQuantifierInfos! infos = node.Infos;
+ if (infos.qid != null) {
+ wr.Write("(QID ");
+ wr.Write(infos.qid);
+ wr.Write(") ");
+ }
+ if (0 <= infos.uniqueId) {
+ wr.Write("(SKOLEMID ");
+ wr.Write(infos.uniqueId);
+ wr.Write(") ");
+ }
+ } */
+
+ Linearise(node.Body, options);
+
+ WriteTriggers(node.Triggers, options);
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ private void WriteTriggers(List<VCTrigger/*!>!*/> triggers, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(triggers != null);
+ // first, count how many neg/pos triggers there are
+ int negTriggers = 0;
+ int posTriggers = 0;
+ foreach (VCTrigger vcTrig in triggers) {
+ Contract.Assert(vcTrig!=null);
+ if (vcTrig.Pos) {
+ posTriggers++;
+ } else {
+ negTriggers++;
+ }
+ }
+
+ if (posTriggers > 0) {
+ foreach (VCTrigger vcTrig in triggers) {
+ Contract.Assert(vcTrig!=null);
+ if (vcTrig.Pos) {
+ wr.Write(" :pat {");
+ foreach (VCExpr e in vcTrig.Exprs) {
+ Contract.Assert(e!=null);
+ wr.Write(" ");
+ LineariseAsTerm(e, options);
+ }
+ wr.Write(" } ");
+ }
+ }
+ } else if (negTriggers > 0) {
+ // if also positive triggers are given, the SMT solver (at least Z3)
+ // will ignore the negative patterns and output a warning. Therefore
+ // we never specify both negative and positive triggers
+ foreach (VCTrigger vcTrig in triggers) {
+ Contract.Assert(vcTrig!=null);
+ if (!vcTrig.Pos) {
+ wr.Write(" :nopat { ");
+ Contract.Assert(vcTrig.Exprs.Count == 1);
+ wr.Write(" ");
+ LineariseAsTerm(vcTrig.Exprs[0], options);
+ wr.Write(" } ");
+ }
+ }
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLet node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ Namer.PushScope(); try {
+
+ foreach (VCExprLetBinding b in node) {
+ Contract.Assert(b != null);
+ bool formula = b.V.Type.IsBool;
+
+ wr.Write("({0} (", formula ? "flet" : "let");
+ string printedName = Namer.GetLocalName(b.V, "$" + MakeIdPrintable(b.V.Name));
+ Contract.Assert(printedName[0] == '$');
+
+ wr.Write("{0} ", printedName);
+ Linearise(b.E, options.SetAsTerm(!formula));
+ wr.Write(") ");
+ }
+ Linearise(node.Body, options);
+
+ for (int i = 0; i < node.Length; ++i)
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for operator terms. The result (bool) is currently not used for anything
+ internal class TPTPOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/> {
+ private readonly TPTPExprLineariser ExprLineariser;
+ private readonly TextWriter wr;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(wr!=null);
+ Contract.Invariant(ExprLineariser!=null);
+}
+
+
+ public TPTPOpLineariser(TPTPExprLineariser ExprLineariser, TextWriter wr) {
+ Contract.Requires(ExprLineariser != null);
+ Contract.Requires(wr != null);
+ this.ExprLineariser = ExprLineariser;
+ this.wr = wr;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
+ LineariserOptions options,
+ bool argsAsTerms) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args ));
+ Contract.Requires(options != null);
+ WriteApplication(op, op, args, options, argsAsTerms);
+ }
+
+ private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
+ LineariserOptions options) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args ));
+ Contract.Requires(options != null);
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteTermApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
+ LineariserOptions options) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args ));
+ Contract.Requires(options != null);
+ ExprLineariser.AssertAsTerm(op, options);
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string termOp, string predOp,
+ IEnumerable<VCExpr/*!>!*/> args, LineariserOptions options) {
+ Contract.Requires(predOp != null);
+ Contract.Requires(termOp != null);
+ Contract.Requires(cce.NonNullElements(args ));
+ Contract.Requires(options != null);
+ WriteApplication(termOp, predOp, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string termOp, string predOp,
+ IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,
+ // change the AsTerm option for the arguments?
+ bool argsAsTerms) {
+ Contract.Requires(predOp != null);
+ Contract.Requires(termOp != null);
+ Contract.Requires(cce.NonNullElements(args ));
+ Contract.Requires(options != null);
+ string opName = options.AsTerm ? termOp : predOp;
+ Contract.Assert(opName!=null);
+ LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);
+ Contract.Assert(newOptions!=null);
+
+ bool hasArgs = false;
+ foreach (VCExpr e in args) {
+ Contract.Assert(e!=null);
+ if (!hasArgs)
+ wr.Write("({0}", opName);
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, newOptions);
+ hasArgs = true;
+ }
+
+ if (hasArgs)
+ wr.Write(")");
+ else
+ wr.Write("{0}", opName);
+ }
+
+ // write an application that can only be a term.
+ // if the expression is supposed to be printed as a formula,
+ // it is turned into an equation (EQ (f args) |@true|)
+ private void WriteApplicationTermOnly(string termOp,
+ IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options) {
+ Contract.Requires(termOp != null);
+ Contract.Requires(cce.NonNullElements(args));
+ Contract.Requires(options != null);
+ if (!options.AsTerm)
+ // Write: (EQ (f args) |@true|)
+ // where "args" are written as terms
+ wr.Write("({0} ", eqName);
+
+ WriteApplication(termOp, args, options, true);
+
+ if (!options.AsTerm)
+ wr.Write(" {0})", boolTrueName);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ public bool VisitNotOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas
+ return true;
+ }
+
+ private bool PrintEq(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(node != null);
+ Contract.Requires(options != null);
+ if (options.AsTerm) {
+ // use equality on terms, also if the arguments have type bool
+ Contract.Assert(node[0].Type.Equals(node[1].Type));
+ if (node[0].Type.IsBool) {
+ WriteApplication(boolIffName, node, options);
+ } else if (node[0].Type.IsInt) {
+ WriteApplication(termIntEqual, node, options);
+ } else {
+ // TODO: make this less hackish
+ CtorType t = node[0].Type as CtorType;
+ if (t != null && t.Decl.Name.Equals("U")) {
+ WriteApplication(termUEqual, node, options);
+ } else if (t != null && t.Decl.Name.Equals("T")) {
+ WriteApplication(termTEqual, node, options);
+ } else {
+ {Contract.Assert(false); throw new cce.UnreachableException();} // unknown type
+ }
+ }
+ } else {
+ if (node[0].Type.IsBool) {
+ Contract.Assert(node[1].Type.IsBool);
+ // use equivalence
+ WriteApplication(iffName, node, options);
+ } else {
+ // use equality and write the arguments as terms
+ WriteApplication(eqName, node, options, true);
+ }
+ }
+
+ return true;
+ }
+
+ public bool VisitEqOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ return PrintEq(node, options);
+ }
+
+ public bool VisitNeqOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ wr.Write("({0} ", options.AsTerm ? boolNotName : notName);
+ PrintEq(node, options);
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitAndOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ Contract.Assert(options.AsTerm);
+ WriteApplication(boolAndName, andName, node, options);
+ return true;
+ }
+
+ public bool VisitOrOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ Contract.Assert(options.AsTerm);
+ WriteApplication(boolOrName, orName, node, options);
+ return true;
+ }
+
+ public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(boolImpliesName, impliesName, node, options);
+ return true;
+ }
+
+ public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(boolIteName, iteName, node, options);
+ return true;
+ }
+
+ public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+ WriteApplicationTermOnly(op.Name, node, options);
+ return true;
+ }
+
+ public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ ExprLineariser.AssertAsFormula(distinctName, options);
+
+ if (node.Length < 2) {
+ ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+ } else {
+ wr.Write("({0}", distinctName);
+ foreach (VCExpr e in node) {
+ Contract.Assert(e!=null);
+ wr.Write(" ");
+ ExprLineariser.LineariseAsTerm(e, options);
+ }
+ wr.Write(")");
+ }
+
+ return true;
+ }
+
+ public bool VisitLabelOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ //Contract.Requires(node.Length>=1);
+ // VCExprLabelOp! op = (VCExprLabelOp)node.Op;
+ // TODO
+ // wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));
+ ExprLineariser.Linearise(node[0], options);
+ // wr.Write(")");
+ return true;
+ }
+
+ public bool VisitSelectOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ {Contract.Assert(false); throw new cce.UnreachableException();} // should not occur in the output
+ }
+
+ public bool VisitStoreOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ {Contract.Assert(false); throw new cce.UnreachableException();} // should not occur in the output
+ }
+
+ public bool VisitBvOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ {Contract.Assert(false); throw new NotImplementedException();} // TODO
+ }
+
+ public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ {Contract.Assert(false); throw new NotImplementedException();} // TODO
+ }
+
+ public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ {Contract.Assert(false); throw new NotImplementedException();} // TODO
+ }
+
+ public bool VisitAddOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteTermApplication(intAddName, node, options);
+ return true;
+ }
+
+ public bool VisitSubOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteTermApplication(intSubName, node, options);
+ return true;
+ }
+
+ public bool VisitMulOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteTermApplication(intMulName, node, options);
+ return true;
+ }
+
+ public bool VisitDivOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteTermApplication(intDivName, node, options);
+ return true;
+ }
+
+ public bool VisitModOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteTermApplication(intModName, node, options);
+ return true;
+ }
+
+ public bool VisitLtOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitLeOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitGtOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitGeOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitSubtypeOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(subtypeName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitSubtype3Op (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms
+ return true;
+ }
+
+ public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
+ Contract.Assert(op!=null);
+ string printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));
+ Contract.Assert(printedName!=null);
+
+ // arguments are always terms
+ WriteApplicationTermOnly(printedName, node, options);
+ return true;
+ }
+
+ }
+ }
+
+}
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 |