summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
diff options
context:
space:
mode:
authorGravatar tabarbe <unknown>2010-07-22 21:25:01 +0000
committerGravatar tabarbe <unknown>2010-07-22 21:25:01 +0000
commit076a19dcb301759813af468478a36e530183b76e (patch)
tree7b95c3f44bee6225b1ce98be27939d2a4653ede0 /Source/Provers/SMTLib
parent65b6bdc20226d1bf6c587b2124f2b423877b786c (diff)
Boogie: Committing my port of the SMTLib project
Diffstat (limited to 'Source/Provers/SMTLib')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs172
-rw-r--r--Source/Provers/SMTLib/SMTLib.csproj240
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs472
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs83
4 files changed, 618 insertions, 349 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index b55cc403..4b4d7431 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -8,9 +8,9 @@ using System.Collections;
using System.Collections.Generic;
using System.Threading;
using System.IO;
-using ExternalProver;
+//using ExternalProver;
using System.Diagnostics;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie;
using Microsoft.Boogie.VCExprAST;
@@ -22,17 +22,35 @@ namespace Microsoft.Boogie.SMTLib
{
public class SMTLibProcessTheoremProver : LogProverInterface
{
- private readonly DeclFreeProverContext! ctx;
+ 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 SMTLibProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen,
- DeclFreeProverContext! ctx)
+ public SMTLibProcessTheoremProver(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;
+ TypeAxiomBuilder axBuilder;
switch (CommandLineOptions.Clo.TypeEncodingMethod) {
case CommandLineOptions.TypeEncoding.Arguments:
axBuilder = new TypeAxiomBuilderArguments (gen);
@@ -46,27 +64,36 @@ namespace Microsoft.Boogie.SMTLib
UniqueNamer namer = new UniqueNamer ();
Namer = namer;
this.DeclCollector = new TypeDeclCollector (namer);
- base(options, "", "", "", "", gen);
+
}
- public override ProverContext! Context { get {
+ 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 readonly TypeAxiomBuilder AxBuilder;
+ private readonly UniqueNamer Namer;
+ private readonly TypeDeclCollector DeclCollector;
private void FeedTypeDeclsToProver() {
- foreach (string! s in DeclCollector.GetNewDeclarations())
+ foreach (string s in DeclCollector.GetNewDeclarations())
+ {
+ Contract.Assert(s!=null);
AddTypeDecl(s);
- }
+ }}
- public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler) {
- TextWriter! output = OpenOutputFile(descriptiveName);
+ 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 =
+ string name =
MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName));
+ Contract.Assert(name!=null);
WriteLineAndLog(output, "(benchmark " + name);
WriteLineAndLog(output, _backgroundPredicates);
@@ -76,13 +103,16 @@ namespace Microsoft.Boogie.SMTLib
}
string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")";
- string! prelude = ctx.GetProverCommands(true);
+ string prelude = ctx.GetProverCommands(true);
+ Contract.Assert(prelude!=null);
WriteLineAndLog(output, prelude);
- foreach (string! s in TypeDecls) {
+ foreach (string s in TypeDecls) {
+ Contract.Assert(s!=null);
WriteLineAndLog(output, s);
}
- foreach (string! s in Axioms) {
+ foreach (string s in Axioms) {
+ Contract.Assert(s!=null);
WriteLineAndLog(output, ":assumption");
WriteLineAndLog(output, s);
}
@@ -95,41 +125,53 @@ namespace Microsoft.Boogie.SMTLib
// 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!> ();
+ private readonly static List<string/*!>!*/> BadBenchmarkWords = new List<string/*!*/> ();
static SMTLibProcessTheoremProver() {
BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray");
}
- private string! MakeBenchmarkNameSafe(string! name) {
+ 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) {
+ private TextWriter OpenOutputFile(string descriptiveName) {
+ Contract.Requires(descriptiveName != null);
+ Contract.Ensures(Contract.Result<TextWriter>() != null);
+
string filename = CommandLineOptions.Clo.SMTLibOutputPath;
- filename = Helpers.SubstituteAtPROC(descriptiveName, (!)filename);
+ filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
return new StreamWriter(filename, false);
}
- private void WriteLineAndLog(TextWriter! output, string! msg) {
+ 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)
- throws UnexpectedProverOutputException; {
+ public override Outcome CheckOutcome(ErrorHandler handler)
+ {Contract.Requires(handler != null);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
return Outcome.Undetermined;
}
- protected string! VCExpr2String(VCExpr! expr, int polarity) {
+ 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;
+ TypeEraser eraser;
switch (CommandLineOptions.Clo.TypeEncodingMethod) {
case CommandLineOptions.TypeEncoding.Arguments:
eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen);
@@ -138,18 +180,24 @@ namespace Microsoft.Boogie.SMTLib
eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);
break;
}
- VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity);
+ Contract.Assert(eraser!=null);
+ VCExpr exprWithoutTypes = eraser.Erase(expr, polarity);
+ Contract.Assert(exprWithoutTypes!=null);
- LetBindingSorter! letSorter = new LetBindingSorter(gen);
- VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true);
- VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true);
+ 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(SMTLibExprLineariser.ToString(sortedAxioms, Namer));
- string! res = SMTLibExprLineariser.ToString(sortedExpr, Namer);
+ string res = SMTLibExprLineariser.ToString(sortedExpr, Namer);
+ Contract.Assert(res!=null);
if (CommandLineOptions.Clo.Trace) {
DateTime end = DateTime.Now;
@@ -161,13 +209,17 @@ namespace Microsoft.Boogie.SMTLib
// the list of all known axioms, where have to be included in each
// verification condition
- private readonly List<string!>! Axioms = new List<string!> ();
+ 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!> ();
+ private readonly List<string/*!>!*/> TypeDecls = new List<string/*!*/> ();
- protected void AddAxiom(string! axiom) {
+ protected void AddAxiom(string axiom) {
+ Contract.Requires(axiom != null);
Axioms.Add(axiom);
// if (thmProver != null) {
// LogActivity(":assume " + axiom);
@@ -175,7 +227,8 @@ namespace Microsoft.Boogie.SMTLib
// }
}
- protected void AddTypeDecl(string! decl) {
+ protected void AddTypeDecl(string decl) {
+ Contract.Requires(decl != null);
TypeDecls.Add(decl);
// if (thmProver != null) {
// LogActivity(decl);
@@ -185,15 +238,15 @@ namespace Microsoft.Boogie.SMTLib
////////////////////////////////////////////////////////////////////////////
- private static string! _backgroundPredicates;
+ private static string _backgroundPredicates;
- static void InitializeGlobalInformation(string! backgroundPred)
- ensures _backgroundPredicates != null;
+ static void InitializeGlobalInformation(string backgroundPred)
+ {Contract.Requires(backgroundPred != null);
+ Contract.Ensures(_backgroundPredicates != null);
//throws ProverException, System.IO.FileNotFoundException;
- {
if (_backgroundPredicates == null) {
- string! codebaseString =
- (!) Path.GetDirectoryName((!)System.Reflection.Assembly.GetExecutingAssembly().Location);
+ string codebaseString =
+ cce.NonNull(Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
// Initialize '_backgroundPredicates'
string univBackPredPath = Path.Combine(codebaseString, backgroundPred);
@@ -208,32 +261,45 @@ namespace Microsoft.Boogie.SMTLib
public class Factory : ProverFactory
{
- public override object! SpawnProver(ProverOptions! options, object! ctxt)
+ 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,
- ((DeclFreeProverContext!)ctxt).ExprGen,
- (DeclFreeProverContext!)ctxt);
+ cce.NonNull((DeclFreeProverContext)ctxt).ExprGen,
+ cce.NonNull((DeclFreeProverContext)ctxt));
}
- public override object! NewProverContext(ProverOptions! options) {
+ 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!> ();
+ 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);
+ VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
+ Contract.Assert(genOptions!=null);
return new DeclFreeProverContext(gen, genOptions);
}
- protected virtual SMTLibProcessTheoremProver! SpawnProver(ProverOptions! options,
- VCExpressionGenerator! gen,
- DeclFreeProverContext! ctx) {
+ protected virtual SMTLibProcessTheoremProver SpawnProver(ProverOptions options,
+ VCExpressionGenerator gen,
+ DeclFreeProverContext ctx) {
+ Contract.Requires(options != null);
+ Contract.Requires(gen != null);
+ Contract.Requires(ctx != null);
+ Contract.Ensures(Contract.Result<SMTLibProcessTheoremProver>() != null);
+
return new SMTLibProcessTheoremProver(options, gen, ctx);
}
}
diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj
index 884f3084..37ea2536 100644
--- a/Source/Provers/SMTLib/SMTLib.csproj
+++ b/Source/Provers/SMTLib/SMTLib.csproj
@@ -1,120 +1,120 @@
-<?xml version="1.0" encoding="utf-8"?>
-<VisualStudioProject>
- <XEN ProjectType="Local"
- SchemaVersion="1.0"
- Name="SMTLib"
- ProjectGuid="13c3a68c-462a-4cda-a480-738046e37c5a"
- >
- <Build>
- <Settings ApplicationIcon=""
- AssemblyName="Provers.SMTLib"
- OutputType="Library"
- RootNamespace="Microsoft.Boogie.SMTLib"
- StartupObject=""
- StandardLibraryLocation=""
- TargetPlatform="v2"
- TargetPlatformLocation=""
- ShadowedAssembly=""
- NoStandardLibraries="False"
- >
- <Config Name="Debug"
- AllowUnsafeBlocks="False"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="False"
- ConfigurationOverrideFile=""
- DefineConstants="DEBUG;TRACE"
- DocumentationFile=""
- DebugSymbols="True"
- FileAlignment="4096"
- IncrementalBuild="True"
- Optimize="False"
- OutputPath="bin\debug"
- RegisterForComInterop="False"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="False"
- WarningLevel="4"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- <Config Name="Release"
- AllowUnsafeBlocks="false"
- BaseAddress="285212672"
- CheckForOverflowUnderflow="false"
- ConfigurationOverrideFile=""
- DefineConstants="TRACE"
- DocumentationFile=""
- DebugSymbols="false"
- FileAlignment="4096"
- IncrementalBuild="false"
- Optimize="true"
- OutputPath="bin\release"
- RegisterForComInterop="false"
- RemoveIntegerChecks="false"
- TreatWarningsAsErrors="false"
- WarningLevel="4"
- CheckContractAdmissibility="True"
- CheckPurity="False"
- />
- </Settings>
- <References>
- <Reference Name="System"
- AssemblyName="System"
- Private="false"
- />
- <Reference Name="System.Data"
- AssemblyName="System.Data"
- Private="false"
- />
- <Reference Name="System.Xml"
- AssemblyName="System.Xml"
- Private="false"
- />
- <Reference Name="Basetypes"
- Project="{0C692837-77EC-415F-BF04-395E3ED06E9A}"
- Private="true"
- />
- <Reference Name="Core"
- Project="{47BC34F1-A173-40BE-84C2-9332B4418387}"
- Private="true"
- />
- <Reference Name="VCExpr"
- Project="{CF42B700-10AA-4DA9-8992-48A800251C11}"
- Private="true"
- />
- <Reference Name="VCGeneration"
- Project="{F65666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- <Reference Name="Mscorlib.Contracts"
- AssemblyName="Mscorlib.Contracts"
- Private="false"
- HintPath="../../../Binaries/Mscorlib.Contracts.dll"
- />
- <Reference Name="Simplify"
- Project="{F75666DE-FB56-457C-8782-09BE243450FC}"
- Private="true"
- />
- </References>
- </Build>
- <Files>
- <Include>
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="ProverInterface.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="SMTLibLineariser.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="TypeDeclCollector.ssc"
- />
- <File BuildAction="Compile"
- SubType="Code"
- RelPath="AssemblyInfo.ssc"
- />
- </Include>
- </Files>
- </XEN>
-</VisualStudioProject> \ No newline at end of file
+<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="3.5" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>9.0.30729</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectGuid>{9B163AA3-36BC-4AFB-88AB-79BC9E97E401}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>Microsoft.Boogie.SMTLib</RootNamespace>
+ <AssemblyName>Provers.SMTLib</AssemblyName>
+ <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
+ </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>
+ <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly>
+ </CodeContractsCustomRewriterAssembly>
+ <CodeContractsCustomRewriterClass>
+ </CodeContractsCustomRewriterClass>
+ <CodeContractsLibPaths>
+ </CodeContractsLibPaths>
+ <CodeContractsExtraRewriteOptions>
+ </CodeContractsExtraRewriteOptions>
+ <CodeContractsExtraAnalysisOptions>
+ </CodeContractsExtraAnalysisOptions>
+ <CodeContractsBaseLineFile>
+ </CodeContractsBaseLineFile>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+ </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="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\AIFramework\bin\debug\AIFramework.dll</HintPath>
+ </Reference>
+ <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Basetypes\bin\debug\Basetypes.dll</HintPath>
+ </Reference>
+ <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\Core\bin\Debug\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>
+ </Reference>
+ <Reference Include="Provers.Simplify, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\Simplify\bin\debug\Provers.Simplify.dll</HintPath>
+ </Reference>
+ <Reference Include="System" />
+ <Reference Include="System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\Binaries\System.Compiler.Runtime.dll</HintPath>
+ </Reference>
+ <Reference Include="System.Core">
+ <RequiredTargetFramework>3.5</RequiredTargetFramework>
+ </Reference>
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ <Reference Include="VCExpr, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\VCExpr\bin\debug\VCExpr.dll</HintPath>
+ </Reference>
+ <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\VCGeneration\bin\debug\VCGeneration.dll</HintPath>
+ </Reference>
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="cce.cs" />
+ <Compile Include="ProverInterface.cs" />
+ <Compile Include="SMTLibLineariser.cs" />
+ <Compile Include="TypeDeclCollector.cs" />
+ </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/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 7efa109f..b211b8f4 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -8,7 +8,7 @@ using System.Text;
using System.IO;
using System.Collections;
using System.Collections.Generic;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
@@ -23,7 +23,9 @@ namespace Microsoft.Boogie.SMTLib
public class LineariserOptions {
public readonly bool AsTerm;
- public LineariserOptions! SetAsTerm(bool newVal) {
+ public LineariserOptions SetAsTerm(bool newVal) {
+ Contract.Ensures(Contract.Result<LineariserOptions>() != null);
+
if (newVal)
return DefaultTerm;
else
@@ -34,57 +36,88 @@ namespace Microsoft.Boogie.SMTLib
this.AsTerm = asTerm;
}
- public static readonly LineariserOptions! Default = new LineariserOptions (false);
- internal static readonly LineariserOptions! DefaultTerm = new LineariserOptions (true);
+ [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 SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {
+ public class SMTLibExprLineariser : 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);
- public static string! ToString(VCExpr! e, UniqueNamer! namer) {
StringWriter sw = new StringWriter();
- SMTLibExprLineariser! lin = new SMTLibExprLineariser (sw, namer);
+ SMTLibExprLineariser lin = new SMTLibExprLineariser (sw, namer);
+ Contract.Assert(lin!=null);
lin.Linearise(e, LineariserOptions.Default);
- return (!)sw.ToString();
+ return cce.NonNull(sw.ToString());
}
////////////////////////////////////////////////////////////////////////////////////////
- private readonly TextWriter! wr;
+ private readonly TextWriter wr;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(wr!=null);
+ Contract.Invariant(Namer != null);
+}
+
private SMTLibOpLineariser OpLinObject = null;
- private IVCExprOpVisitor<bool, LineariserOptions!>! OpLineariser { get {
+ private IVCExprOpVisitor<bool, LineariserOptions>/*!>!*/ OpLineariser { get {
+ Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool,LineariserOptions>>() !=null);
+
if (OpLinObject == null)
- OpLinObject = new SMTLibOpLineariser (this, wr);
+ OpLinObject = new SMTLibOpLineariser(this, wr);
return OpLinObject;
} }
- internal readonly UniqueNamer! Namer;
+ internal readonly UniqueNamer Namer;
- public SMTLibExprLineariser(TextWriter! wr, UniqueNamer! namer) {
+ public SMTLibExprLineariser(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) {
- expr.Accept<bool, LineariserOptions!>(this, options);
+ 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) {
+ 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) {
+ 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)
- assert false; // bitvectors are currently not handled for SMT-Lib solvers
+ 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();
@@ -97,7 +130,10 @@ namespace Microsoft.Boogie.SMTLib
/////////////////////////////////////////////////////////////////////////////////////
- public static string! MakeIdPrintable(string! s) {
+ 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:
@@ -114,7 +150,7 @@ namespace Microsoft.Boogie.SMTLib
break;
}
- string! newS = "";
+ string newS = "";
foreach (char ch in s) {
if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_')
newS = newS + ch;
@@ -136,58 +172,64 @@ namespace Microsoft.Boogie.SMTLib
/// <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) {
+ 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) {
+ 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) {
+ public bool Visit(VCExprLiteral node, LineariserOptions options) {
+ Contract.Requires(node != null);
+ Contract.Requires(options != null);
if (options.AsTerm) {
if (node == VCExpressionGenerator.True)
@@ -202,8 +244,10 @@ namespace Microsoft.Boogie.SMTLib
wr.Write("({0} 0 {1})", intSubName, lit.Abs);
else
wr.Write(lit);
- } else
- assert false;
+ } else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
} else {
@@ -214,7 +258,7 @@ namespace Microsoft.Boogie.SMTLib
else if (node is VCExprIntLit) {
System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");
} else
- assert false;
+ {Contract.Assert(false); throw new cce.UnreachableException();}
}
@@ -223,8 +267,12 @@ namespace Microsoft.Boogie.SMTLib
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprNAry! node, LineariserOptions! options) {
- VCExprOp! op = node.Op;
+ 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) ||
@@ -233,12 +281,13 @@ namespace Microsoft.Boogie.SMTLib
wr.Write("({0}",
op.Equals(VCExpressionGenerator.AndOp) ? andName : orName);
- IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node);
+ 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((VCExpr!)enumerator.Current, options);
+ Linearise(cce.NonNull((VCExpr)enumerator.Current), options);
}
}
@@ -247,13 +296,16 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
- return node.Accept<bool, LineariserOptions!>(OpLineariser, options);
+ return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);
}
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprVar! node, LineariserOptions! options) {
- string! printedName = Namer.GetName(node, MakeIdPrintable(node.Name));
+ 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
@@ -267,21 +319,25 @@ namespace Microsoft.Boogie.SMTLib
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprQuantifier! node, LineariserOptions! options) {
+ public bool Visit(VCExprQuantifier node, LineariserOptions options) {
+ Contract.Requires(node != null);
+ Contract.Requires(options != null);
AssertAsFormula(node.Quan.ToString(), options);
- assert node.TypeParameters.Count == 0;
+ Contract.Assert(node.TypeParameters.Count == 0);
Namer.PushScope(); try {
- string! kind = node.Quan == Quantifier.ALL ? "forall" : "exists";
+ 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];
+ VCExprVar var = node.BoundVars[i];
+ Contract.Assert(var!=null);
// ensure that the variable name starts with ?
- string! printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));
- assert printedName[0] == '?';
+ string printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name));
+ Contract.Assert(printedName!=null);
+ Contract.Assert(printedName[0] == '?');
wr.Write("({0} {1}) ", printedName, TypeToString(var.Type));
}
@@ -312,11 +368,14 @@ namespace Microsoft.Boogie.SMTLib
}
}
- private void WriteTriggers(List<VCTrigger!>! triggers, LineariserOptions! options) {
+ 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) {
+ foreach (VCTrigger vcTrig in triggers) {
+ Contract.Assert(vcTrig!=null);
if (vcTrig.Pos) {
posTriggers++;
} else {
@@ -325,10 +384,12 @@ namespace Microsoft.Boogie.SMTLib
}
if (posTriggers > 0) {
- foreach (VCTrigger! vcTrig in triggers) {
+ foreach (VCTrigger vcTrig in triggers) {
+ Contract.Assert(vcTrig!=null);
if (vcTrig.Pos) {
wr.Write(" :pat {");
- foreach (VCExpr! e in vcTrig.Exprs) {
+ foreach (VCExpr e in vcTrig.Exprs) {
+ Contract.Assert(e!=null);
wr.Write(" ");
LineariseAsTerm(e, options);
}
@@ -339,10 +400,11 @@ namespace Microsoft.Boogie.SMTLib
// 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) {
+ foreach (VCTrigger vcTrig in triggers) {
+ Contract.Assert(vcTrig!=null);
if (!vcTrig.Pos) {
wr.Write(" :nopat { ");
- assert vcTrig.Exprs.Count == 1;
+ Contract.Assert(vcTrig.Exprs.Count == 1);
wr.Write(" ");
LineariseAsTerm(vcTrig.Exprs[0], options);
wr.Write(" } ");
@@ -353,15 +415,18 @@ namespace Microsoft.Boogie.SMTLib
/////////////////////////////////////////////////////////////////////////////////////
- public bool Visit(VCExprLet! node, LineariserOptions! options) {
+ public bool Visit(VCExprLet node, LineariserOptions options) {
+ Contract.Requires(node != null);
+ Contract.Requires(options != null);
Namer.PushScope(); try {
- foreach (VCExprLetBinding! b in node) {
+ 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));
- assert printedName[0] == '$';
+ string printedName = Namer.GetLocalName(b.V, "$" + MakeIdPrintable(b.V.Name));
+ Contract.Assert(printedName[0] == '$');
wr.Write("{0} ", printedName);
Linearise(b.E, options.SetAsTerm(!formula));
@@ -382,48 +447,77 @@ namespace Microsoft.Boogie.SMTLib
/////////////////////////////////////////////////////////////////////////////////////
// Lineariser for operator terms. The result (bool) is currently not used for anything
- internal class SMTLibOpLineariser : IVCExprOpVisitor<bool, LineariserOptions!> {
- private readonly SMTLibExprLineariser! ExprLineariser;
- private readonly TextWriter! wr;
+ internal class SMTLibOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/> {
+ private readonly SMTLibExprLineariser ExprLineariser;
+ private readonly TextWriter wr;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(wr!=null);
+ Contract.Invariant(ExprLineariser!=null);
+}
+
- public SMTLibOpLineariser(SMTLibExprLineariser! ExprLineariser, TextWriter! wr) {
+ public SMTLibOpLineariser(SMTLibExprLineariser 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,
+ 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) {
+ 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) {
+ 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) {
+ 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,
+ private void WriteApplication(string termOp, string predOp,
+ IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,
// change the AsTerm option for the arguments?
bool argsAsTerms) {
- string! opName = options.AsTerm ? termOp : predOp;
- LineariserOptions! newOptions = options.SetAsTerm(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) {
+ foreach (VCExpr e in args) {
+ Contract.Assert(e!=null);
if (!hasArgs)
wr.Write("({0}", opName);
wr.Write(" ");
@@ -440,8 +534,11 @@ namespace Microsoft.Boogie.SMTLib
// 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) {
+ 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
@@ -455,15 +552,19 @@ namespace Microsoft.Boogie.SMTLib
///////////////////////////////////////////////////////////////////////////////////
- public bool VisitNotOp (VCExprNAry! node, LineariserOptions! options) {
+ 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) {
+ 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
- assert node[0].Type.Equals(node[1].Type);
+ Contract.Assert(node[0].Type.Equals(node[1].Type));
if (node[0].Type.IsBool) {
WriteApplication(boolIffName, node, options);
} else if (node[0].Type.IsInt) {
@@ -476,12 +577,12 @@ namespace Microsoft.Boogie.SMTLib
} else if (t != null && t.Decl.Name.Equals("T")) {
WriteApplication(termTEqual, node, options);
} else {
- assert false; // unknown type
+ {Contract.Assert(false); throw new cce.UnreachableException();} // unknown type
}
}
} else {
if (node[0].Type.IsBool) {
- assert node[1].Type.IsBool;
+ Contract.Assert(node[1].Type.IsBool);
// use equivalence
WriteApplication(iffName, node, options);
} else {
@@ -493,47 +594,66 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
- public bool VisitEqOp (VCExprNAry! node, LineariserOptions! options) {
+ 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) {
+ 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) {
- assert options.AsTerm;
+ 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) {
- assert options.AsTerm;
+ 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) {
+ 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) {
+ public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(node != null);
+ Contract.Requires(options != null);
+
WriteApplication(boolIteName, iteName, node, options);
return true;
}
- public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) {
+ 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) {
+ foreach (VCExpr e in node) {
+ Contract.Assert(e!=null);
wr.Write(" ");
ExprLineariser.LineariseAsTerm(e, options);
}
@@ -543,7 +663,10 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
- public bool VisitLabelOp (VCExprNAry! node, LineariserOptions! options) {
+ 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));
@@ -552,84 +675,137 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
- public bool VisitSelectOp (VCExprNAry! node, LineariserOptions! options) {
- assert false; // should not occur in the output
+ 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) {
- assert false; // 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) {
- assert false; // TODO
+ 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) {
- assert false; // 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) {
- assert false; // 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
+ 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) {
- VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op;
- string! printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));
+ 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);
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 08c0e6a3..a0d56601 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -7,7 +7,7 @@ using System;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
using Microsoft.Boogie.VCExprAST;
namespace Microsoft.Boogie.SMTLib
@@ -17,68 +17,93 @@ namespace Microsoft.Boogie.SMTLib
public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
- private readonly UniqueNamer! Namer;
+ 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) {
+ public TypeDeclCollector(UniqueNamer namer) {
+ Contract.Requires(namer != null);
this.Namer = namer;
}
// not used
- protected override bool StandardResult(VCExpr! node, bool arg) {
+ 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 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> ();
- 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>>() ));
- public List<string!>! AllDeclarations { get {
- List<string!>! res = new List<string!> ();
+ List<string>/*!>!*/ res = new List<string/*!*/> ();
res.AddRange(AllDecls);
return res;
} }
- public List<string!>! GetNewDeclarations() {
- List<string!>! res = new List<string!> ();
+ 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) {
+ private void AddDeclaration(string decl) {
+ Contract.Requires(decl != null);
AllDecls.Add(decl);
IncDecls.Add(decl);
}
- public void Collect(VCExpr! expr) {
+ public void Collect(VCExpr expr) {
+ Contract.Requires(expr != null);
Traverse(expr, true);
}
///////////////////////////////////////////////////////////////////////////
- private static string! TypeToString(Type! t) {
+ private static string TypeToString(Type t) {
+ Contract.Requires(t != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
return SMTLibExprLineariser.TypeToString(t);
}
- public override bool Visit(VCExprNAry! node, bool arg) {
+ 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;
- string! printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name));
- string! decl = ":extrafuns ((" + printedName;
-
- foreach (Variable! v in f.InParams) {
+ Function f = op.Func;
+ Contract.Assert(f!=null);
+ string printedName = Namer.GetName(f, SMTLibExprLineariser.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);
}
- assert f.OutParams.Length == 1;
- foreach (Variable! v in f.OutParams) {
+ Contract.Assert(f.OutParams.Length == 1);
+ foreach (Variable v in f.OutParams) {
+ Contract.Assert(v!=null);
decl += " " + TypeToString(v.TypedIdent.Type);
}
@@ -91,10 +116,12 @@ namespace Microsoft.Boogie.SMTLib
return base.Visit(node, arg);
}
- public override bool Visit(VCExprVar! node, bool 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, SMTLibExprLineariser.MakeIdPrintable(node.Name));
- string! decl =
+ string printedName = Namer.GetName(node, SMTLibExprLineariser.MakeIdPrintable(node.Name));
+ Contract.Assert(printedName!=null);
+ string decl =
":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))";
AddDeclaration(decl);
KnownVariables.Add(node, true);
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-19 15:53:59 +0000