From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Source/Provers/TPTP/ProverInterface.cs | 702 ++++++++++++++++----------------- 1 file changed, 351 insertions(+), 351 deletions(-) (limited to 'Source/Provers/TPTP/ProverInterface.cs') 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= Store VC in named file. Defaults to boogie-vc-@PROC@.tptp. -USE_PREDICATES= 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() != 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() != 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(true); - return Outcome.Undetermined; - } - - protected string VCExpr2String(VCExpr expr, int polarity) - { - Contract.Requires(expr != null); - Contract.Ensures(Contract.Result() != 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!*/> Axioms = new List(); - private bool AxiomsAreSetup = false; - - - - - // similarly, a list of function/predicate declarations - private readonly List!*/> TypeDecls = new List(); - - 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() != 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() != null); - - if (CommandLineOptions.Clo.BracketIdsInVC < 0) { - CommandLineOptions.Clo.BracketIdsInVC = 0; - } - - VCExpressionGenerator gen = new VCExpressionGenerator(); - List/*!>!*/ proverCommands = new List(); - 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() != 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= Store VC in named file. Defaults to boogie-vc-@PROC@.tptp. +USE_PREDICATES= 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() != 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() != 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(true); + return Outcome.Undetermined; + } + + protected string VCExpr2String(VCExpr expr, int polarity) + { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != 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!*/> Axioms = new List(); + private bool AxiomsAreSetup = false; + + + + + // similarly, a list of function/predicate declarations + private readonly List!*/> TypeDecls = new List(); + + 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() != 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() != null); + + if (CommandLineOptions.Clo.BracketIdsInVC < 0) { + CommandLineOptions.Clo.BracketIdsInVC = 0; + } + + VCExpressionGenerator gen = new VCExpressionGenerator(); + List/*!>!*/ proverCommands = new List(); + 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() != null); + + return new TPTPProcessTheoremProver(options, gen, ctx); + } + } +} -- cgit v1.2.3