summaryrefslogtreecommitdiff
path: root/Source/Provers/TPTP
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/TPTP')
-rw-r--r--Source/Provers/TPTP/ProverInterface.cs702
-rw-r--r--Source/Provers/TPTP/TPTP.csproj260
-rw-r--r--Source/Provers/TPTP/TPTPLineariser.cs1480
-rw-r--r--Source/Provers/TPTP/TypeDeclCollector.cs270
4 files changed, 1356 insertions, 1356 deletions
diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs
index b714ed67..669c459f 100644
--- a/Source/Provers/TPTP/ProverInterface.cs
+++ b/Source/Provers/TPTP/ProverInterface.cs
@@ -1,351 +1,351 @@
-//-----------------------------------------------------------------------------
-//
-// 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 TPTPProverOptions : ProverOptions
- {
- public string Output = "boogie-vc-@PROC@.tptp";
- public bool UsePredicates = false;
-
- protected override bool Parse(string opt)
- {
- return
- ParseString(opt, "OUTPUT", ref Output) ||
- ParseBool(opt, "USE_PREDICATES", ref UsePredicates) ||
- base.Parse(opt);
- }
-
- public override string Help
- {
- get
- {
- return
-@"
-TPTP-specific options:
-~~~~~~~~~~~~~~~~~~~~~~
-OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.tptp.
-USE_PREDICATES=<bool> Try to use SMT predicates for functions returning bool.
-
-" + base.Help;
- // DIST requires non-public binaries
- }
- }
- }
-
- public class TPTPProcessTheoremProver : LogProverInterface
- {
- private readonly DeclFreeProverContext ctx;
- private readonly VCExpressionGenerator Gen;
-
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(ctx != null);
- Contract.Invariant(AxBuilder != null);
- Contract.Invariant(Namer != null);
- Contract.Invariant(DeclCollector != 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);
-
- // No bg predicate at the moment
- // InitializeGlobalInformation("UnivBackPred.tptp");
-
- this.ctx = ctx;
- this.Gen = gen;
-
- TypeAxiomBuilder axBuilder;
- switch (CommandLineOptions.Clo.TypeEncodingMethod) {
- case CommandLineOptions.TypeEncoding.Arguments:
- axBuilder = new TypeAxiomBuilderArguments(gen);
- axBuilder.Setup();
- break;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- axBuilder = new TypeAxiomBuilderPremisses(gen);
- break;
- default:
- axBuilder = new TypeAxiomBuilderPremisses(gen);
- axBuilder.Setup();
- break;
- }
- AxBuilder = axBuilder;
- UniqueNamer namer = new UniqueNamer();
- Namer = namer;
- Namer.Spacer = "__";
- 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);
-
- WriteLineAndLog(output, "%------------------------------------------------------------------------------");
- WriteLineAndLog(output, "% Boogie benchmark: " + descriptiveName);
- WriteLineAndLog(output, "%------------------------------------------------------------------------------");
-
- WriteLineAndLog(output, _backgroundPredicates);
-
- if (!AxiomsAreSetup) {
- AddAxiom(VCExpr2String(ctx.Axioms, -1));
- AxiomsAreSetup = true;
- }
-
- string vcString = "fof(vc, conjecture, " + VCExpr2String(vc, 1) + ").";
-
- foreach (string s in TypeDecls) {
- Contract.Assert(s != null);
- WriteLineAndLog(output, s);
- }
- int id = 0;
- foreach (string s in Axioms) {
- Contract.Assert(s != null);
- WriteLineAndLog(output, "fof(ax" + id++ + ", axiom,");
- WriteLineAndLog(output, s);
- WriteLineAndLog(output, ").");
- }
-
- WriteLineAndLog(output, vcString);
-
- output.Close();
- }
-
- public TPTPProverOptions Options
- {
- get { return (TPTPProverOptions)this.options; }
- }
-
- private TextWriter OpenOutputFile(string descriptiveName)
- {
- Contract.Requires(descriptiveName != null);
- Contract.Ensures(Contract.Result<TextWriter>() != null);
-
- string filename = Options.Output;
- 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.UtcNow;
- 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;
- case CommandLineOptions.TypeEncoding.Monomorphic:
- eraser = null;
- break;
- default:
- eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);
- break;
- }
- VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity);
- Contract.Assert(exprWithoutTypes != null);
-
- var letImplier = new Let2ImpliesMutator(Gen);
- var flattener = new TermFormulaFlattener(Gen);
- var exprWithLet = flattener.Flatten(exprWithoutTypes);
- var exprWithoutLet = letImplier.Mutate(exprWithLet);
-
- var axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());
- var axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);
-
- DeclCollector.Collect(axiomsWithoutLet);
- DeclCollector.Collect(exprWithoutLet);
- FeedTypeDeclsToProver();
-
- AddAxiom(TPTPExprLineariser.ToString(axiomsWithoutLet, Namer, Options));
- string res = TPTPExprLineariser.ToString(exprWithoutLet, Namer, Options);
- Contract.Assert(res != null);
-
- if (CommandLineOptions.Clo.Trace) {
- DateTime end = DateTime.UtcNow;
- 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/*!*/>();
- proverCommands.Add("tptp");
- proverCommands.Add("external");
- VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
- Contract.Assert(genOptions != null);
-
- return new DeclFreeProverContext(gen, genOptions);
- }
-
- public override ProverOptions BlankProverOptions()
- {
- return new TPTPProverOptions();
- }
-
- 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);
- }
- }
-}
+//-----------------------------------------------------------------------------
+//
+// 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 TPTPProverOptions : ProverOptions
+ {
+ public string Output = "boogie-vc-@PROC@.tptp";
+ public bool UsePredicates = false;
+
+ protected override bool Parse(string opt)
+ {
+ return
+ ParseString(opt, "OUTPUT", ref Output) ||
+ ParseBool(opt, "USE_PREDICATES", ref UsePredicates) ||
+ base.Parse(opt);
+ }
+
+ public override string Help
+ {
+ get
+ {
+ return
+@"
+TPTP-specific options:
+~~~~~~~~~~~~~~~~~~~~~~
+OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.tptp.
+USE_PREDICATES=<bool> Try to use SMT predicates for functions returning bool.
+
+" + base.Help;
+ // DIST requires non-public binaries
+ }
+ }
+ }
+
+ public class TPTPProcessTheoremProver : LogProverInterface
+ {
+ private readonly DeclFreeProverContext ctx;
+ private readonly VCExpressionGenerator Gen;
+
+ [ContractInvariantMethod]
+ void ObjectInvariant()
+ {
+ Contract.Invariant(ctx != null);
+ Contract.Invariant(AxBuilder != null);
+ Contract.Invariant(Namer != null);
+ Contract.Invariant(DeclCollector != 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);
+
+ // No bg predicate at the moment
+ // InitializeGlobalInformation("UnivBackPred.tptp");
+
+ this.ctx = ctx;
+ this.Gen = gen;
+
+ TypeAxiomBuilder axBuilder;
+ switch (CommandLineOptions.Clo.TypeEncodingMethod) {
+ case CommandLineOptions.TypeEncoding.Arguments:
+ axBuilder = new TypeAxiomBuilderArguments(gen);
+ axBuilder.Setup();
+ break;
+ case CommandLineOptions.TypeEncoding.Monomorphic:
+ axBuilder = new TypeAxiomBuilderPremisses(gen);
+ break;
+ default:
+ axBuilder = new TypeAxiomBuilderPremisses(gen);
+ axBuilder.Setup();
+ break;
+ }
+ AxBuilder = axBuilder;
+ UniqueNamer namer = new UniqueNamer();
+ Namer = namer;
+ Namer.Spacer = "__";
+ 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);
+
+ WriteLineAndLog(output, "%------------------------------------------------------------------------------");
+ WriteLineAndLog(output, "% Boogie benchmark: " + descriptiveName);
+ WriteLineAndLog(output, "%------------------------------------------------------------------------------");
+
+ WriteLineAndLog(output, _backgroundPredicates);
+
+ if (!AxiomsAreSetup) {
+ AddAxiom(VCExpr2String(ctx.Axioms, -1));
+ AxiomsAreSetup = true;
+ }
+
+ string vcString = "fof(vc, conjecture, " + VCExpr2String(vc, 1) + ").";
+
+ foreach (string s in TypeDecls) {
+ Contract.Assert(s != null);
+ WriteLineAndLog(output, s);
+ }
+ int id = 0;
+ foreach (string s in Axioms) {
+ Contract.Assert(s != null);
+ WriteLineAndLog(output, "fof(ax" + id++ + ", axiom,");
+ WriteLineAndLog(output, s);
+ WriteLineAndLog(output, ").");
+ }
+
+ WriteLineAndLog(output, vcString);
+
+ output.Close();
+ }
+
+ public TPTPProverOptions Options
+ {
+ get { return (TPTPProverOptions)this.options; }
+ }
+
+ private TextWriter OpenOutputFile(string descriptiveName)
+ {
+ Contract.Requires(descriptiveName != null);
+ Contract.Ensures(Contract.Result<TextWriter>() != null);
+
+ string filename = Options.Output;
+ 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.UtcNow;
+ 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;
+ case CommandLineOptions.TypeEncoding.Monomorphic:
+ eraser = null;
+ break;
+ default:
+ eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen);
+ break;
+ }
+ VCExpr exprWithoutTypes = eraser == null ? expr : eraser.Erase(expr, polarity);
+ Contract.Assert(exprWithoutTypes != null);
+
+ var letImplier = new Let2ImpliesMutator(Gen);
+ var flattener = new TermFormulaFlattener(Gen);
+ var exprWithLet = flattener.Flatten(exprWithoutTypes);
+ var exprWithoutLet = letImplier.Mutate(exprWithLet);
+
+ var axiomsWithLet = flattener.Flatten(AxBuilder.GetNewAxioms());
+ var axiomsWithoutLet = letImplier.Mutate(axiomsWithLet);
+
+ DeclCollector.Collect(axiomsWithoutLet);
+ DeclCollector.Collect(exprWithoutLet);
+ FeedTypeDeclsToProver();
+
+ AddAxiom(TPTPExprLineariser.ToString(axiomsWithoutLet, Namer, Options));
+ string res = TPTPExprLineariser.ToString(exprWithoutLet, Namer, Options);
+ Contract.Assert(res != null);
+
+ if (CommandLineOptions.Clo.Trace) {
+ DateTime end = DateTime.UtcNow;
+ 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/*!*/>();
+ proverCommands.Add("tptp");
+ proverCommands.Add("external");
+ VCGenerationOptions genOptions = new VCGenerationOptions(proverCommands);
+ Contract.Assert(genOptions != null);
+
+ return new DeclFreeProverContext(gen, genOptions);
+ }
+
+ public override ProverOptions BlankProverOptions()
+ {
+ return new TPTPProverOptions();
+ }
+
+ 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
index a3ee1caa..116492d0 100644
--- a/Source/Provers/TPTP/TPTP.csproj
+++ b/Source/Provers/TPTP/TPTP.csproj
@@ -1,131 +1,131 @@
-<?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 Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
- <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>
- </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>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\Provers.TPTP.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </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>
- </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>
- -->
+<?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 Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
+ <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>
+ </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>
+ <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+ <DebugSymbols>true</DebugSymbols>
+ <OutputPath>bin\Checked\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <DebugType>full</DebugType>
+ <PlatformTarget>AnyCPU</PlatformTarget>
+ <CodeAnalysisLogFile>bin\Debug\Provers.TPTP.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+ <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+ <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+ <ErrorReport>prompt</ErrorReport>
+ <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
+ <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+ <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+ <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+ <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+ <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+ <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+ <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+ <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+ <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+ <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+ <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+ <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+ <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+ <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+ <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+ <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+ <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+ <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+ <CodeContractsCustomRewriterAssembly />
+ <CodeContractsCustomRewriterClass />
+ <CodeContractsLibPaths />
+ <CodeContractsExtraRewriteOptions />
+ <CodeContractsExtraAnalysisOptions />
+ <CodeContractsBaseLineFile />
+ <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+ <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+ <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+ <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+ </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>
+ </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
index a35d43f0..4bdf29b9 100644
--- a/Source/Provers/TPTP/TPTPLineariser.cs
+++ b/Source/Provers/TPTP/TPTPLineariser.cs
@@ -1,740 +1,740 @@
-//-----------------------------------------------------------------------------
-//
-// 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, TPTPProverOptions opts) {
- Contract.Requires(e != null);
- Contract.Requires(namer != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- StringWriter sw = new StringWriter();
- TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer, opts);
- 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;
- internal readonly TPTPProverOptions Options;
-
- public TPTPExprLineariser(TextWriter wr, UniqueNamer namer, TPTPProverOptions opts) {
- Contract.Requires(wr != null);Contract.Requires(namer != null);
- this.wr = wr;
- this.Namer = namer;
- this.Options = opts;
- }
-
- 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));
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- 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 TRUEName:
- case FALSEName:
- case "Array":
- s = "nonkeyword_" + s;
- break;
- }
-
- var res = new StringBuilder();
-
- foreach (char ch in s) {
- if (Char.IsLetterOrDigit(ch))
- res.Append(ch);
- else
- // replace everything else with a _
- res.Append('_');
- }
-
- return res.ToString();
- }
-
- public static string Lowercase(string s)
- {
- if (char.IsLower(s[0])) return MakeIdPrintable(s);
- else return MakeIdPrintable("x" + s);
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- internal const string andName = "&"; // conjunction
- internal const string orName = "|"; // disjunction
- internal const string notName = "~"; // negation
- internal const string impliesName = "=>"; // implication
- internal const string iteName = "$itef"; // if-then-else
- internal const string iffName = "<=>"; // logical equivalence
- internal const string eqName = "="; // equality
- internal const string lessName = "lt";
- internal const string greaterName = "gt";
- internal const string atmostName = "le";
- internal const string atleastName = "ge";
- 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 boolTrueName = "boolTrue";
- internal const string boolFalseName = "boolFalse";
- internal const string boolIteName = "ite";
- internal const string intAddName = "intAdd";
- internal const string intSubName = "intSub";
- internal const string intMulName = "intMul";
- 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) {
- BigNum lit = ((VCExprIntLit)node).Val;
- 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
-
- var sop = op.Equals(VCExpressionGenerator.AndOp) ? andName : orName;
- wr.Write("(");
- IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);
- Contract.Assert(enumerator!=null);
- var cnt = 0;
- while (enumerator.MoveNext()) {
- VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
- if (naryExpr == null || !naryExpr.Op.Equals(op)) {
- if (cnt > 0)
- wr.Write(" {0} ", sop);
- cnt++;
- 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(Lowercase(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})", 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 ? "!" : "?";
- 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, "V" + MakeIdPrintable(var.Name));
- Contract.Assert(printedName!=null);
- Contract.Assert(printedName[0] == 'V');
- if (i > 0) wr.Write(",");
- wr.Write("{0}", printedName);
- }
-
- wr.Write("] : (");
-
- /* 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();
- }
- }
-
-
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public bool Visit(VCExprLet node, LineariserOptions options) {
- throw new NotImplementedException();
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- // 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) {
- Contract.Requires(op != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- WriteApplication(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, args, options, options.AsTerm);
- }
-
-
- private void WriteApplication(string termOp,
- IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,
- // change the AsTerm option for the arguments?
- bool argsAsTerms) {
- Contract.Requires(termOp != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);
- Contract.Assert(newOptions!=null);
-
- var argCnt = 0;
- if (termOp == "~") {
- wr.Write("(~ ");
- foreach (var e in args) {
- ExprLineariser.Linearise(e, newOptions);
- argCnt++;
- }
- Contract.Assert(argCnt == 1);
- wr.Write(")");
- } else if ("&|~=><".IndexOf(termOp[0]) >= 0) {
- wr.Write("(");
- foreach (var e in args) {
- ExprLineariser.Linearise(e, newOptions);
- argCnt++;
- if (argCnt == 1) {
- wr.Write(" {0} ", termOp);
- }
- }
- Contract.Assert(argCnt == 2);
- wr.Write(")");
- } else {
- wr.Write(termOp);
- foreach (var e in args) {
- Contract.Assert(e != null);
- if (argCnt == 0)
- wr.Write("(");
- else
- wr.Write(", ");
- argCnt++;
- ExprLineariser.Linearise(e, newOptions);
- }
-
- if (argCnt > 0)
- wr.Write(")");
- }
- }
-
- // 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("(", 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(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) {
- throw new NotImplementedException();
- } 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("(~ ");
- 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(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(orName, node, options);
- return true;
- }
-
- public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(impliesName, node, options);
- return true;
- }
-
- public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- throw new NotImplementedException();
- }
-
- 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("distinct", options);
-
- if (node.Length < 2) {
- ExprLineariser.Linearise(VCExpressionGenerator.True, options);
- } else {
- var bits = 0;
- var cnt = node.Length;
- while (cnt > 0) {
- cnt >>= 1;
- bits++;
- }
-
- wr.Write("($true ");
- foreach (VCExpr e in node) {
- for (var i = 0; i < bits; ++i) {
- var neg = (cnt & (1 << i)) != 0 ? "~" : "";
- wr.Write(" & {0}distinct__f__{1}(", neg, i);
- ExprLineariser.LineariseAsTerm(e, options);
- wr.Write(")");
- }
- wr.WriteLine();
- cnt++;
- }
- 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(options != null);
- //Contract.Requires(node != null);
- var name = Lowercase(SimplifyLikeExprLineariser.SelectOpName(node));
- wr.Write(name + "(");
- var cnt = 0;
- foreach (VCExpr/*!*/ e in node) {
- Contract.Assert(e != null);
- if (cnt++ > 0)
- wr.Write(", ");
- ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
- }
- wr.Write(")");
- return true;
- }
-
- public bool VisitStoreOp(VCExprNAry node, LineariserOptions options)
- {
- //Contract.Requires(options != null);
- //Contract.Requires(node != null);
- var name = Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));
- wr.Write(name + "(");
- var cnt = 0;
- foreach (VCExpr e in node) {
- Contract.Assert(e != null);
- if (cnt++ > 0)
- wr.Write(", ");
- ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
- }
- wr.Write(")");
- return true;
- }
-
- 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(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(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(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(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, Lowercase(op.Func.Name));
- Contract.Assert(printedName!=null);
-
- if (ExprLineariser.Options.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool)
- WriteApplication(printedName, node, options, true);
- else
- // arguments are always terms
- WriteApplicationTermOnly(printedName, node, options);
- return true;
- }
-
- }
- }
-
-}
+//-----------------------------------------------------------------------------
+//
+// 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, TPTPProverOptions opts) {
+ Contract.Requires(e != null);
+ Contract.Requires(namer != null);
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ StringWriter sw = new StringWriter();
+ TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer, opts);
+ 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;
+ internal readonly TPTPProverOptions Options;
+
+ public TPTPExprLineariser(TextWriter wr, UniqueNamer namer, TPTPProverOptions opts) {
+ Contract.Requires(wr != null);Contract.Requires(namer != null);
+ this.wr = wr;
+ this.Namer = namer;
+ this.Options = opts;
+ }
+
+ 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));
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ 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 TRUEName:
+ case FALSEName:
+ case "Array":
+ s = "nonkeyword_" + s;
+ break;
+ }
+
+ var res = new StringBuilder();
+
+ foreach (char ch in s) {
+ if (Char.IsLetterOrDigit(ch))
+ res.Append(ch);
+ else
+ // replace everything else with a _
+ res.Append('_');
+ }
+
+ return res.ToString();
+ }
+
+ public static string Lowercase(string s)
+ {
+ if (char.IsLower(s[0])) return MakeIdPrintable(s);
+ else return MakeIdPrintable("x" + s);
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ internal const string andName = "&"; // conjunction
+ internal const string orName = "|"; // disjunction
+ internal const string notName = "~"; // negation
+ internal const string impliesName = "=>"; // implication
+ internal const string iteName = "$itef"; // if-then-else
+ internal const string iffName = "<=>"; // logical equivalence
+ internal const string eqName = "="; // equality
+ internal const string lessName = "lt";
+ internal const string greaterName = "gt";
+ internal const string atmostName = "le";
+ internal const string atleastName = "ge";
+ 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 boolTrueName = "boolTrue";
+ internal const string boolFalseName = "boolFalse";
+ internal const string boolIteName = "ite";
+ internal const string intAddName = "intAdd";
+ internal const string intSubName = "intSub";
+ internal const string intMulName = "intMul";
+ 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) {
+ BigNum lit = ((VCExprIntLit)node).Val;
+ 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
+
+ var sop = op.Equals(VCExpressionGenerator.AndOp) ? andName : orName;
+ wr.Write("(");
+ IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);
+ Contract.Assert(enumerator!=null);
+ var cnt = 0;
+ while (enumerator.MoveNext()) {
+ VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
+ if (naryExpr == null || !naryExpr.Op.Equals(op)) {
+ if (cnt > 0)
+ wr.Write(" {0} ", sop);
+ cnt++;
+ 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(Lowercase(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})", 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 ? "!" : "?";
+ 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, "V" + MakeIdPrintable(var.Name));
+ Contract.Assert(printedName!=null);
+ Contract.Assert(printedName[0] == 'V');
+ if (i > 0) wr.Write(",");
+ wr.Write("{0}", printedName);
+ }
+
+ wr.Write("] : (");
+
+ /* 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();
+ }
+ }
+
+
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLet node, LineariserOptions options) {
+ throw new NotImplementedException();
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ // 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) {
+ Contract.Requires(op != null);
+ Contract.Requires(cce.NonNullElements(args ));
+ Contract.Requires(options != null);
+ WriteApplication(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, args, options, options.AsTerm);
+ }
+
+
+ private void WriteApplication(string termOp,
+ IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,
+ // change the AsTerm option for the arguments?
+ bool argsAsTerms) {
+ Contract.Requires(termOp != null);
+ Contract.Requires(cce.NonNullElements(args ));
+ Contract.Requires(options != null);
+ LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);
+ Contract.Assert(newOptions!=null);
+
+ var argCnt = 0;
+ if (termOp == "~") {
+ wr.Write("(~ ");
+ foreach (var e in args) {
+ ExprLineariser.Linearise(e, newOptions);
+ argCnt++;
+ }
+ Contract.Assert(argCnt == 1);
+ wr.Write(")");
+ } else if ("&|~=><".IndexOf(termOp[0]) >= 0) {
+ wr.Write("(");
+ foreach (var e in args) {
+ ExprLineariser.Linearise(e, newOptions);
+ argCnt++;
+ if (argCnt == 1) {
+ wr.Write(" {0} ", termOp);
+ }
+ }
+ Contract.Assert(argCnt == 2);
+ wr.Write(")");
+ } else {
+ wr.Write(termOp);
+ foreach (var e in args) {
+ Contract.Assert(e != null);
+ if (argCnt == 0)
+ wr.Write("(");
+ else
+ wr.Write(", ");
+ argCnt++;
+ ExprLineariser.Linearise(e, newOptions);
+ }
+
+ if (argCnt > 0)
+ wr.Write(")");
+ }
+ }
+
+ // 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("(", 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(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) {
+ throw new NotImplementedException();
+ } 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("(~ ");
+ 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(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(orName, node, options);
+ return true;
+ }
+
+ public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+
+ WriteApplication(impliesName, node, options);
+ return true;
+ }
+
+ public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(node != null);
+ //Contract.Requires(options != null);
+ throw new NotImplementedException();
+ }
+
+ 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("distinct", options);
+
+ if (node.Length < 2) {
+ ExprLineariser.Linearise(VCExpressionGenerator.True, options);
+ } else {
+ var bits = 0;
+ var cnt = node.Length;
+ while (cnt > 0) {
+ cnt >>= 1;
+ bits++;
+ }
+
+ wr.Write("($true ");
+ foreach (VCExpr e in node) {
+ for (var i = 0; i < bits; ++i) {
+ var neg = (cnt & (1 << i)) != 0 ? "~" : "";
+ wr.Write(" & {0}distinct__f__{1}(", neg, i);
+ ExprLineariser.LineariseAsTerm(e, options);
+ wr.Write(")");
+ }
+ wr.WriteLine();
+ cnt++;
+ }
+ 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(options != null);
+ //Contract.Requires(node != null);
+ var name = Lowercase(SimplifyLikeExprLineariser.SelectOpName(node));
+ wr.Write(name + "(");
+ var cnt = 0;
+ foreach (VCExpr/*!*/ e in node) {
+ Contract.Assert(e != null);
+ if (cnt++ > 0)
+ wr.Write(", ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitStoreOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ var name = Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));
+ wr.Write(name + "(");
+ var cnt = 0;
+ foreach (VCExpr e in node) {
+ Contract.Assert(e != null);
+ if (cnt++ > 0)
+ wr.Write(", ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ 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(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(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(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(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, Lowercase(op.Func.Name));
+ Contract.Assert(printedName!=null);
+
+ if (ExprLineariser.Options.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool)
+ WriteApplication(printedName, node, options, true);
+ else
+ // arguments are always terms
+ WriteApplicationTermOnly(printedName, node, options);
+ return true;
+ }
+
+ }
+ }
+
+}
diff --git a/Source/Provers/TPTP/TypeDeclCollector.cs b/Source/Provers/TPTP/TypeDeclCollector.cs
index b7495659..1daf19a5 100644
--- a/Source/Provers/TPTP/TypeDeclCollector.cs
+++ b/Source/Provers/TPTP/TypeDeclCollector.cs
@@ -1,136 +1,136 @@
-//-----------------------------------------------------------------------------
-//
-// 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 HashSet<string/*!*/>/*!*/ KnownStoreFunctions = new HashSet<string>();
- private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions = new HashSet<string>();
-
- private readonly UniqueNamer Namer;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(Namer != null);
- Contract.Invariant(AllDecls != null);
- Contract.Invariant(IncDecls != null);
- Contract.Invariant(cce.NonNull(KnownFunctions));
- Contract.Invariant(cce.NonNull(KnownVariables));
- }
-
-
- 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 HashSet<Function/*!*/>/*!*/ KnownFunctions = new HashSet<Function/*!*/>();
- private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables = new HashSet<VCExprVar/*!*/>();
-
- 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);
- }
-
- ///////////////////////////////////////////////////////////////////////////
-
-
- public override bool Visit(VCExprNAry node, bool arg) {
- Contract.Requires(node != null);
-
- if (node.Op is VCExprStoreOp) {
- string name = TPTPExprLineariser.Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));
- if (!KnownStoreFunctions.Contains(name)) {
- var id = KnownStoreFunctions.Count;
-
- if (CommandLineOptions.Clo.MonomorphicArrays) {
- var sel = TPTPExprLineariser.Lowercase(SimplifyLikeExprLineariser.SelectOpName(node));
-
- var eq = "=";
- if (node[node.Arity - 1].Type.IsBool)
- eq = "<=>";
-
- string xS = "", yS = "";
- string dist = "";
-
- for (int i = 0; i < node.Arity - 2; i++) {
- if (i != 0) {
- dist += " | ";
- xS += ",";
- yS += ",";
- }
- var x = "X" + i;
- var y = "Y" + i;
- xS += x;
- yS += y;
- dist += string.Format("({0} != {1})", x, y);
- }
-
- string ax1 = "fof(selectEq" + id + ", axiom, ! [M,V," + xS + "] : (" +
- string.Format("{0}({1}(M,{2},V),{2}) {3} V", sel, name, xS, eq) + ")).";
- string ax2 = "fof(selectNeq" + id + ", axiom, ! [M,V," + xS + "," + yS + "] : (" +
- string.Format("( {0} ) => ", dist) +
- string.Format("{0}({1}(M,{2},V),{3}) {4} {0}(M,{3})", sel, name, xS, yS, eq) + ")).";
-
- AddDeclaration(ax1);
- AddDeclaration(ax2);
- }
-
- KnownStoreFunctions.Add(name);
- }
- //
- }
-
- return base.Visit(node, arg);
- }
-
- public override bool Visit(VCExprVar node, bool arg) {
-
- return base.Visit(node, arg);
- }
- }
-
+//-----------------------------------------------------------------------------
+//
+// 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 HashSet<string/*!*/>/*!*/ KnownStoreFunctions = new HashSet<string>();
+ private readonly HashSet<string/*!*/>/*!*/ KnownSelectFunctions = new HashSet<string>();
+
+ private readonly UniqueNamer Namer;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(Namer != null);
+ Contract.Invariant(AllDecls != null);
+ Contract.Invariant(IncDecls != null);
+ Contract.Invariant(cce.NonNull(KnownFunctions));
+ Contract.Invariant(cce.NonNull(KnownVariables));
+ }
+
+
+ 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 HashSet<Function/*!*/>/*!*/ KnownFunctions = new HashSet<Function/*!*/>();
+ private readonly HashSet<VCExprVar/*!*/>/*!*/ KnownVariables = new HashSet<VCExprVar/*!*/>();
+
+ 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);
+ }
+
+ ///////////////////////////////////////////////////////////////////////////
+
+
+ public override bool Visit(VCExprNAry node, bool arg) {
+ Contract.Requires(node != null);
+
+ if (node.Op is VCExprStoreOp) {
+ string name = TPTPExprLineariser.Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));
+ if (!KnownStoreFunctions.Contains(name)) {
+ var id = KnownStoreFunctions.Count;
+
+ if (CommandLineOptions.Clo.MonomorphicArrays) {
+ var sel = TPTPExprLineariser.Lowercase(SimplifyLikeExprLineariser.SelectOpName(node));
+
+ var eq = "=";
+ if (node[node.Arity - 1].Type.IsBool)
+ eq = "<=>";
+
+ string xS = "", yS = "";
+ string dist = "";
+
+ for (int i = 0; i < node.Arity - 2; i++) {
+ if (i != 0) {
+ dist += " | ";
+ xS += ",";
+ yS += ",";
+ }
+ var x = "X" + i;
+ var y = "Y" + i;
+ xS += x;
+ yS += y;
+ dist += string.Format("({0} != {1})", x, y);
+ }
+
+ string ax1 = "fof(selectEq" + id + ", axiom, ! [M,V," + xS + "] : (" +
+ string.Format("{0}({1}(M,{2},V),{2}) {3} V", sel, name, xS, eq) + ")).";
+ string ax2 = "fof(selectNeq" + id + ", axiom, ! [M,V," + xS + "," + yS + "] : (" +
+ string.Format("( {0} ) => ", dist) +
+ string.Format("{0}({1}(M,{2},V),{3}) {4} {0}(M,{3})", sel, name, xS, yS, eq) + ")).";
+
+ AddDeclaration(ax1);
+ AddDeclaration(ax2);
+ }
+
+ KnownStoreFunctions.Add(name);
+ }
+ //
+ }
+
+ return base.Visit(node, arg);
+ }
+
+ public override bool Visit(VCExprVar node, bool arg) {
+
+ return base.Visit(node, arg);
+ }
+ }
+
} \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 20:01:38 +0000