From 65b6bdc20226d1bf6c587b2124f2b423877b786c Mon Sep 17 00:00:00 2001 From: tabarbe Date: Thu, 22 Jul 2010 21:23:48 +0000 Subject: Boogie: Renaming the source files for the SMTLib project in preparation for commiting my port of the project. --- Source/Provers/SMTLib/ProverInterface.cs | 240 +++++++++++ Source/Provers/SMTLib/ProverInterface.ssc | 240 ----------- Source/Provers/SMTLib/SMTLib.csproj | 120 ++++++ Source/Provers/SMTLib/SMTLib.sscproj | 120 ------ Source/Provers/SMTLib/SMTLibLineariser.cs | 642 ++++++++++++++++++++++++++++ Source/Provers/SMTLib/SMTLibLineariser.ssc | 642 ---------------------------- Source/Provers/SMTLib/TypeDeclCollector.cs | 107 +++++ Source/Provers/SMTLib/TypeDeclCollector.ssc | 107 ----- 8 files changed, 1109 insertions(+), 1109 deletions(-) create mode 100644 Source/Provers/SMTLib/ProverInterface.cs delete mode 100644 Source/Provers/SMTLib/ProverInterface.ssc create mode 100644 Source/Provers/SMTLib/SMTLib.csproj delete mode 100644 Source/Provers/SMTLib/SMTLib.sscproj create mode 100644 Source/Provers/SMTLib/SMTLibLineariser.cs delete mode 100644 Source/Provers/SMTLib/SMTLibLineariser.ssc create mode 100644 Source/Provers/SMTLib/TypeDeclCollector.cs delete mode 100644 Source/Provers/SMTLib/TypeDeclCollector.ssc diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs new file mode 100644 index 00000000..b55cc403 --- /dev/null +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -0,0 +1,240 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using ExternalProver; +using System.Diagnostics; +using Microsoft.Contracts; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.VCExprAST; +using Microsoft.Boogie.Clustering; +using Microsoft.Boogie.TypeErasure; +using Microsoft.Boogie.Simplify; + +namespace Microsoft.Boogie.SMTLib +{ + public class SMTLibProcessTheoremProver : LogProverInterface + { + private readonly DeclFreeProverContext! ctx; + + [NotDelayed] + public SMTLibProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, + DeclFreeProverContext! ctx) + { + InitializeGlobalInformation("UnivBackPred2.smt"); + + this.ctx = ctx; + + TypeAxiomBuilder! axBuilder; + switch (CommandLineOptions.Clo.TypeEncodingMethod) { + case CommandLineOptions.TypeEncoding.Arguments: + axBuilder = new TypeAxiomBuilderArguments (gen); + break; + default: + axBuilder = new TypeAxiomBuilderPremisses (gen); + break; + } + axBuilder.Setup(); + AxBuilder = axBuilder; + UniqueNamer namer = new UniqueNamer (); + Namer = namer; + this.DeclCollector = new TypeDeclCollector (namer); + base(options, "", "", "", "", gen); + } + + public override ProverContext! Context { get { + return ctx; + } } + + private readonly TypeAxiomBuilder! AxBuilder; + private readonly UniqueNamer! Namer; + private readonly TypeDeclCollector! DeclCollector; + + private void FeedTypeDeclsToProver() { + foreach (string! s in DeclCollector.GetNewDeclarations()) + AddTypeDecl(s); + } + + public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler) { + TextWriter! output = OpenOutputFile(descriptiveName); + + string! name = + MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName)); + WriteLineAndLog(output, "(benchmark " + name); + WriteLineAndLog(output, _backgroundPredicates); + + if (!AxiomsAreSetup) { + AddAxiom(VCExpr2String(ctx.Axioms, -1)); + AxiomsAreSetup = true; + } + + string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")"; + string! prelude = ctx.GetProverCommands(true); + WriteLineAndLog(output, prelude); + + foreach (string! s in TypeDecls) { + WriteLineAndLog(output, s); + } + foreach (string! s in Axioms) { + WriteLineAndLog(output, ":assumption"); + WriteLineAndLog(output, s); + } + + WriteLineAndLog(output, vcString); + WriteLineAndLog(output, ")"); + + output.Close(); + } + + // certain words that should not occur in the name of a benchmark + // because some solvers don't like them + private readonly static List! BadBenchmarkWords = new List (); + static SMTLibProcessTheoremProver() { + BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray"); + } + + private string! MakeBenchmarkNameSafe(string! name) { + for (int i = 0; i < BadBenchmarkWords.Count; i = i + 2) + name = name.Replace(BadBenchmarkWords[i], BadBenchmarkWords[i+1]); + return name; + } + + private TextWriter! OpenOutputFile(string! descriptiveName) { + string filename = CommandLineOptions.Clo.SMTLibOutputPath; + filename = Helpers.SubstituteAtPROC(descriptiveName, (!)filename); + return new StreamWriter(filename, false); + } + + private void WriteLineAndLog(TextWriter! output, string! msg) { + LogActivity(msg); + output.WriteLine(msg); + } + + [NoDefaultContract] + public override Outcome CheckOutcome(ErrorHandler! handler) + throws UnexpectedProverOutputException; { + return Outcome.Undetermined; + } + + protected string! VCExpr2String(VCExpr! expr, int polarity) { + DateTime start = DateTime.Now; + if (CommandLineOptions.Clo.Trace) + Console.Write("Linearising ... "); + + // handle the types in the VCExpr + TypeEraser! eraser; + switch (CommandLineOptions.Clo.TypeEncodingMethod) { + case CommandLineOptions.TypeEncoding.Arguments: + eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen); + break; + default: + eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen); + break; + } + VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity); + + LetBindingSorter! letSorter = new LetBindingSorter(gen); + VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true); + VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true); + + DeclCollector.Collect(sortedAxioms); + DeclCollector.Collect(sortedExpr); + FeedTypeDeclsToProver(); + + AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer)); + string! res = SMTLibExprLineariser.ToString(sortedExpr, Namer); + + if (CommandLineOptions.Clo.Trace) { + DateTime end = DateTime.Now; + TimeSpan elapsed = end - start; + Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds); + } + return res; + } + + // the list of all known axioms, where have to be included in each + // verification condition + private readonly List! 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) { + Axioms.Add(axiom); +// if (thmProver != null) { +// LogActivity(":assume " + axiom); +// thmProver.AddAxioms(axiom); +// } + } + + protected void AddTypeDecl(string! decl) { + TypeDecls.Add(decl); + // if (thmProver != null) { + // LogActivity(decl); + // thmProver.Feed(decl, 0); + // } + } + + //////////////////////////////////////////////////////////////////////////// + + private static string! _backgroundPredicates; + + static void InitializeGlobalInformation(string! backgroundPred) + ensures _backgroundPredicates != null; + //throws ProverException, System.IO.FileNotFoundException; + { + if (_backgroundPredicates == null) { + string! codebaseString = + (!) Path.GetDirectoryName((!)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) + { + return this.SpawnProver(options, + ((DeclFreeProverContext!)ctxt).ExprGen, + (DeclFreeProverContext!)ctxt); + } + + public override object! NewProverContext(ProverOptions! options) { + if (CommandLineOptions.Clo.BracketIdsInVC < 0) { + CommandLineOptions.Clo.BracketIdsInVC = 0; + } + + VCExpressionGenerator! gen = new VCExpressionGenerator (); + List! proverCommands = new List (); +// TODO: what is supported? +// proverCommands.Add("all"); +// proverCommands.Add("simplify"); +// proverCommands.Add("simplifyLike"); + VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands); + + return new DeclFreeProverContext(gen, genOptions); + } + + protected virtual SMTLibProcessTheoremProver! SpawnProver(ProverOptions! options, + VCExpressionGenerator! gen, + DeclFreeProverContext! ctx) { + return new SMTLibProcessTheoremProver(options, gen, ctx); + } + } +} diff --git a/Source/Provers/SMTLib/ProverInterface.ssc b/Source/Provers/SMTLib/ProverInterface.ssc deleted file mode 100644 index b55cc403..00000000 --- a/Source/Provers/SMTLib/ProverInterface.ssc +++ /dev/null @@ -1,240 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections; -using System.Collections.Generic; -using System.Threading; -using System.IO; -using ExternalProver; -using System.Diagnostics; -using Microsoft.Contracts; -using Microsoft.Boogie.AbstractInterpretation; -using Microsoft.Boogie; -using Microsoft.Boogie.VCExprAST; -using Microsoft.Boogie.Clustering; -using Microsoft.Boogie.TypeErasure; -using Microsoft.Boogie.Simplify; - -namespace Microsoft.Boogie.SMTLib -{ - public class SMTLibProcessTheoremProver : LogProverInterface - { - private readonly DeclFreeProverContext! ctx; - - [NotDelayed] - public SMTLibProcessTheoremProver(ProverOptions! options, VCExpressionGenerator! gen, - DeclFreeProverContext! ctx) - { - InitializeGlobalInformation("UnivBackPred2.smt"); - - this.ctx = ctx; - - TypeAxiomBuilder! axBuilder; - switch (CommandLineOptions.Clo.TypeEncodingMethod) { - case CommandLineOptions.TypeEncoding.Arguments: - axBuilder = new TypeAxiomBuilderArguments (gen); - break; - default: - axBuilder = new TypeAxiomBuilderPremisses (gen); - break; - } - axBuilder.Setup(); - AxBuilder = axBuilder; - UniqueNamer namer = new UniqueNamer (); - Namer = namer; - this.DeclCollector = new TypeDeclCollector (namer); - base(options, "", "", "", "", gen); - } - - public override ProverContext! Context { get { - return ctx; - } } - - private readonly TypeAxiomBuilder! AxBuilder; - private readonly UniqueNamer! Namer; - private readonly TypeDeclCollector! DeclCollector; - - private void FeedTypeDeclsToProver() { - foreach (string! s in DeclCollector.GetNewDeclarations()) - AddTypeDecl(s); - } - - public override void BeginCheck(string! descriptiveName, VCExpr! vc, ErrorHandler! handler) { - TextWriter! output = OpenOutputFile(descriptiveName); - - string! name = - MakeBenchmarkNameSafe(SMTLibExprLineariser.MakeIdPrintable(descriptiveName)); - WriteLineAndLog(output, "(benchmark " + name); - WriteLineAndLog(output, _backgroundPredicates); - - if (!AxiomsAreSetup) { - AddAxiom(VCExpr2String(ctx.Axioms, -1)); - AxiomsAreSetup = true; - } - - string vcString = ":formula (not " + VCExpr2String(vc, 1) + ")"; - string! prelude = ctx.GetProverCommands(true); - WriteLineAndLog(output, prelude); - - foreach (string! s in TypeDecls) { - WriteLineAndLog(output, s); - } - foreach (string! s in Axioms) { - WriteLineAndLog(output, ":assumption"); - WriteLineAndLog(output, s); - } - - WriteLineAndLog(output, vcString); - WriteLineAndLog(output, ")"); - - output.Close(); - } - - // certain words that should not occur in the name of a benchmark - // because some solvers don't like them - private readonly static List! BadBenchmarkWords = new List (); - static SMTLibProcessTheoremProver() { - BadBenchmarkWords.Add("Array"); BadBenchmarkWords.Add("Arrray"); - } - - private string! MakeBenchmarkNameSafe(string! name) { - for (int i = 0; i < BadBenchmarkWords.Count; i = i + 2) - name = name.Replace(BadBenchmarkWords[i], BadBenchmarkWords[i+1]); - return name; - } - - private TextWriter! OpenOutputFile(string! descriptiveName) { - string filename = CommandLineOptions.Clo.SMTLibOutputPath; - filename = Helpers.SubstituteAtPROC(descriptiveName, (!)filename); - return new StreamWriter(filename, false); - } - - private void WriteLineAndLog(TextWriter! output, string! msg) { - LogActivity(msg); - output.WriteLine(msg); - } - - [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler! handler) - throws UnexpectedProverOutputException; { - return Outcome.Undetermined; - } - - protected string! VCExpr2String(VCExpr! expr, int polarity) { - DateTime start = DateTime.Now; - if (CommandLineOptions.Clo.Trace) - Console.Write("Linearising ... "); - - // handle the types in the VCExpr - TypeEraser! eraser; - switch (CommandLineOptions.Clo.TypeEncodingMethod) { - case CommandLineOptions.TypeEncoding.Arguments: - eraser = new TypeEraserArguments((TypeAxiomBuilderArguments)AxBuilder, gen); - break; - default: - eraser = new TypeEraserPremisses((TypeAxiomBuilderPremisses)AxBuilder, gen); - break; - } - VCExpr! exprWithoutTypes = eraser.Erase(expr, polarity); - - LetBindingSorter! letSorter = new LetBindingSorter(gen); - VCExpr! sortedExpr = letSorter.Mutate(exprWithoutTypes, true); - VCExpr! sortedAxioms = letSorter.Mutate(AxBuilder.GetNewAxioms(), true); - - DeclCollector.Collect(sortedAxioms); - DeclCollector.Collect(sortedExpr); - FeedTypeDeclsToProver(); - - AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer)); - string! res = SMTLibExprLineariser.ToString(sortedExpr, Namer); - - if (CommandLineOptions.Clo.Trace) { - DateTime end = DateTime.Now; - TimeSpan elapsed = end - start; - Console.WriteLine("finished [{0} s] ", elapsed.TotalSeconds); - } - return res; - } - - // the list of all known axioms, where have to be included in each - // verification condition - private readonly List! 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) { - Axioms.Add(axiom); -// if (thmProver != null) { -// LogActivity(":assume " + axiom); -// thmProver.AddAxioms(axiom); -// } - } - - protected void AddTypeDecl(string! decl) { - TypeDecls.Add(decl); - // if (thmProver != null) { - // LogActivity(decl); - // thmProver.Feed(decl, 0); - // } - } - - //////////////////////////////////////////////////////////////////////////// - - private static string! _backgroundPredicates; - - static void InitializeGlobalInformation(string! backgroundPred) - ensures _backgroundPredicates != null; - //throws ProverException, System.IO.FileNotFoundException; - { - if (_backgroundPredicates == null) { - string! codebaseString = - (!) Path.GetDirectoryName((!)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) - { - return this.SpawnProver(options, - ((DeclFreeProverContext!)ctxt).ExprGen, - (DeclFreeProverContext!)ctxt); - } - - public override object! NewProverContext(ProverOptions! options) { - if (CommandLineOptions.Clo.BracketIdsInVC < 0) { - CommandLineOptions.Clo.BracketIdsInVC = 0; - } - - VCExpressionGenerator! gen = new VCExpressionGenerator (); - List! proverCommands = new List (); -// TODO: what is supported? -// proverCommands.Add("all"); -// proverCommands.Add("simplify"); -// proverCommands.Add("simplifyLike"); - VCGenerationOptions! genOptions = new VCGenerationOptions(proverCommands); - - return new DeclFreeProverContext(gen, genOptions); - } - - protected virtual SMTLibProcessTheoremProver! SpawnProver(ProverOptions! options, - VCExpressionGenerator! gen, - DeclFreeProverContext! ctx) { - return new SMTLibProcessTheoremProver(options, gen, ctx); - } - } -} diff --git a/Source/Provers/SMTLib/SMTLib.csproj b/Source/Provers/SMTLib/SMTLib.csproj new file mode 100644 index 00000000..884f3084 --- /dev/null +++ b/Source/Provers/SMTLib/SMTLib.csproj @@ -0,0 +1,120 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + \ No newline at end of file diff --git a/Source/Provers/SMTLib/SMTLib.sscproj b/Source/Provers/SMTLib/SMTLib.sscproj deleted file mode 100644 index 884f3084..00000000 --- a/Source/Provers/SMTLib/SMTLib.sscproj +++ /dev/null @@ -1,120 +0,0 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - \ No newline at end of file diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs new file mode 100644 index 00000000..7efa109f --- /dev/null +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -0,0 +1,642 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.IO; +using System.Collections; +using System.Collections.Generic; +using Microsoft.Contracts; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; + +// Method to turn VCExprs into strings that can be fed into SMT +// solvers. This is currently quite similar to the +// SimplifyLikeLineariser (but the code is independent) + +namespace Microsoft.Boogie.SMTLib +{ + + // Options for the linearisation + public class LineariserOptions { + + public readonly bool AsTerm; + public LineariserOptions! SetAsTerm(bool newVal) { + if (newVal) + return DefaultTerm; + else + return Default; + } + + internal LineariserOptions(bool asTerm) { + this.AsTerm = asTerm; + } + + public static readonly LineariserOptions! Default = new LineariserOptions (false); + internal static readonly LineariserOptions! DefaultTerm = new LineariserOptions (true); + } + + + //////////////////////////////////////////////////////////////////////////////////////// + + // Lineariser for expressions. The result (bool) is currently not used for anything + public class SMTLibExprLineariser : IVCExprVisitor { + + public static string! ToString(VCExpr! e, UniqueNamer! namer) { + StringWriter sw = new StringWriter(); + SMTLibExprLineariser! lin = new SMTLibExprLineariser (sw, namer); + lin.Linearise(e, LineariserOptions.Default); + return (!)sw.ToString(); + } + + //////////////////////////////////////////////////////////////////////////////////////// + + private readonly TextWriter! wr; + private SMTLibOpLineariser OpLinObject = null; + private IVCExprOpVisitor! OpLineariser { get { + if (OpLinObject == null) + OpLinObject = new SMTLibOpLineariser (this, wr); + return OpLinObject; + } } + + internal readonly UniqueNamer! Namer; + + public SMTLibExprLineariser(TextWriter! wr, UniqueNamer! namer) { + this.wr = wr; + this.Namer = namer; + } + + public void Linearise(VCExpr! expr, LineariserOptions! options) { + expr.Accept(this, options); + } + + public void LineariseAsTerm(VCExpr! expr, LineariserOptions! options) { + Linearise(expr, options.SetAsTerm(true)); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + internal static string! TypeToString(Type! t) { + if (t.IsBool) + return "TermBool"; + else if (t.IsInt) + return "Int"; + else if (t.IsBv) + assert false; // bitvectors are currently not handled for SMT-Lib solvers + else { + // at this point, only the types U, T should be left + System.IO.StringWriter buffer = new System.IO.StringWriter(); + using (TokenTextWriter stream = new TokenTextWriter("", buffer, false)) { + t.Emit(stream); + } + return "boogie" + buffer.ToString(); + } + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public static string! MakeIdPrintable(string! s) { + // make sure that no keywords are used as identifiers + switch(s) { + case andName: + case orName: + case notName: + case impliesName: + case iffName: + case eqName: + case distinctName: + case TRUEName: + case FALSEName: + case "Array": + s = "nonkeyword_" + s; + break; + } + + string! newS = ""; + foreach (char ch in s) { + if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_') + newS = newS + ch; + else + // replace everything else with a . + newS = newS + '.'; + } + + // ensure that the first character is not . or _ (some SMT-solvers do + // not like that, e.g., yices and cvc3) + if (newS[0] == '.' || newS[0] == '_') + newS = "x" + newS; + + return newS; + } + + ///////////////////////////////////////////////////////////////////////////////////// + + /// + /// The name for logical conjunction in Simplify + /// + internal const string! andName = "and"; // conjunction + internal const string! orName = "or"; // disjunction + internal const string! notName = "not"; // negation + internal const string! impliesName = "implies"; // implication + internal const string! iteName = "ite"; // if-then-else + internal const string! iffName = "iff"; // logical equivalence + internal const string! eqName = "="; // equality + internal const string! lessName = "<"; + internal const string! greaterName = ">"; + internal const string! atmostName = "<="; + internal const string! atleastName = ">="; + internal const string! TRUEName = "true"; // nullary predicate that is always true + internal const string! FALSEName = "false"; // nullary predicate that is always false + internal const string! subtypeName = "UOrdering2"; + internal const string! subtypeArgsName = "UOrdering3"; + + internal const string! distinctName = "distinct"; + + internal const string! boolTrueName = "boolTrue"; + internal const string! boolFalseName = "boolFalse"; + internal const string! boolAndName = "boolAnd"; + internal const string! boolOrName = "boolOr"; + internal const string! boolNotName = "boolNot"; + internal const string! boolIffName = "boolIff"; + internal const string! boolImpliesName = "boolImplies"; + internal const string! boolIteName = "ite"; + internal const string! termUEqual = "UEqual"; + internal const string! termTEqual = "TEqual"; + internal const string! termIntEqual = "IntEqual"; + internal const string! termLessName = "intLess"; + internal const string! termGreaterName = "intGreater"; + internal const string! termAtmostName = "intAtMost"; + internal const string! termAtleastName = "intAtLeast"; + internal const string! intAddName = "+"; + internal const string! intSubName = "-"; + internal const string! intMulName = "*"; + internal const string! intDivName = "boogieIntDiv"; + internal const string! intModName = "boogieIntMod"; + + internal void AssertAsTerm(string! x, LineariserOptions! options) { + if (!options.AsTerm) + System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!"); + } + + internal void AssertAsFormula(string! x, LineariserOptions! options) { + if (options.AsTerm) + System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!"); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprLiteral! node, LineariserOptions! options) { + if (options.AsTerm) { + + if (node == VCExpressionGenerator.True) + wr.Write("{0}", boolTrueName); + else if (node == VCExpressionGenerator.False) + wr.Write("{0}", boolFalseName); + else if (node is VCExprIntLit) { + // some SMT-solvers do not understand negative literals + // (e.g., yices) + BigNum lit = ((VCExprIntLit)node).Val; + if (lit.IsNegative) + wr.Write("({0} 0 {1})", intSubName, lit.Abs); + else + wr.Write(lit); + } else + assert false; + + } 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 + assert false; + + } + + return true; + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprNAry! node, LineariserOptions! options) { + VCExprOp! op = node.Op; + + if (!options.AsTerm && + (op.Equals(VCExpressionGenerator.AndOp) || + op.Equals(VCExpressionGenerator.OrOp))) { + // handle these operators without recursion + + wr.Write("({0}", + op.Equals(VCExpressionGenerator.AndOp) ? andName : orName); + IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node); + while (enumerator.MoveNext()) { + VCExprNAry naryExpr = enumerator.Current as VCExprNAry; + if (naryExpr == null || !naryExpr.Op.Equals(op)) { + wr.Write(" "); + Linearise((VCExpr!)enumerator.Current, options); + } + } + + wr.Write(")"); + + return true; + } + + return node.Accept(OpLineariser, options); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprVar! node, LineariserOptions! options) { + string! printedName = Namer.GetName(node, MakeIdPrintable(node.Name)); + + if (options.AsTerm || + // formula variables are easy to identify in SMT-Lib + printedName[0] == '$') + wr.Write("{0}", printedName); + else + wr.Write("({0} {1} {2})", eqName, printedName, boolTrueName); + + return true; + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprQuantifier! node, LineariserOptions! options) { + AssertAsFormula(node.Quan.ToString(), options); + assert node.TypeParameters.Count == 0; + + Namer.PushScope(); try { + + string! kind = node.Quan == Quantifier.ALL ? "forall" : "exists"; + wr.Write("({0} ", kind); + + for (int i = 0; i < node.BoundVars.Count; i++) + { + VCExprVar! var = node.BoundVars[i]; + // ensure that the variable name starts with ? + string! printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name)); + assert printedName[0] == '?'; + wr.Write("({0} {1}) ", printedName, TypeToString(var.Type)); + } + + /* if (options.QuantifierIds) { + // only needed for Z3 + VCQuantifierInfos! infos = node.Infos; + if (infos.qid != null) { + wr.Write("(QID "); + wr.Write(infos.qid); + wr.Write(") "); + } + if (0 <= infos.uniqueId) { + wr.Write("(SKOLEMID "); + wr.Write(infos.uniqueId); + wr.Write(") "); + } + } */ + + Linearise(node.Body, options); + + WriteTriggers(node.Triggers, options); + wr.Write(")"); + + return true; + + } finally { + Namer.PopScope(); + } + } + + private void WriteTriggers(List! triggers, LineariserOptions! options) { + // first, count how many neg/pos triggers there are + int negTriggers = 0; + int posTriggers = 0; + foreach (VCTrigger! vcTrig in triggers) { + if (vcTrig.Pos) { + posTriggers++; + } else { + negTriggers++; + } + } + + if (posTriggers > 0) { + foreach (VCTrigger! vcTrig in triggers) { + if (vcTrig.Pos) { + wr.Write(" :pat {"); + foreach (VCExpr! e in vcTrig.Exprs) { + wr.Write(" "); + LineariseAsTerm(e, options); + } + wr.Write(" } "); + } + } + } else if (negTriggers > 0) { + // if also positive triggers are given, the SMT solver (at least Z3) + // will ignore the negative patterns and output a warning. Therefore + // we never specify both negative and positive triggers + foreach (VCTrigger! vcTrig in triggers) { + if (!vcTrig.Pos) { + wr.Write(" :nopat { "); + assert vcTrig.Exprs.Count == 1; + wr.Write(" "); + LineariseAsTerm(vcTrig.Exprs[0], options); + wr.Write(" } "); + } + } + } + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprLet! node, LineariserOptions! options) { + Namer.PushScope(); try { + + foreach (VCExprLetBinding! b in node) { + bool formula = b.V.Type.IsBool; + + wr.Write("({0} (", formula ? "flet" : "let"); + string! printedName = Namer.GetLocalName(b.V, "$" + MakeIdPrintable(b.V.Name)); + assert printedName[0] == '$'; + + wr.Write("{0} ", printedName); + Linearise(b.E, options.SetAsTerm(!formula)); + wr.Write(") "); + } + Linearise(node.Body, options); + + for (int i = 0; i < node.Length; ++i) + wr.Write(")"); + + return true; + + } finally { + Namer.PopScope(); + } + } + + ///////////////////////////////////////////////////////////////////////////////////// + + // Lineariser for operator terms. The result (bool) is currently not used for anything + internal class SMTLibOpLineariser : IVCExprOpVisitor { + private readonly SMTLibExprLineariser! ExprLineariser; + private readonly TextWriter! wr; + + public SMTLibOpLineariser(SMTLibExprLineariser! ExprLineariser, TextWriter! wr) { + this.ExprLineariser = ExprLineariser; + this.wr = wr; + } + + /////////////////////////////////////////////////////////////////////////////////// + + private void WriteApplication(string! op, IEnumerable! args, + LineariserOptions! options, + bool argsAsTerms) { + WriteApplication(op, op, args, options, argsAsTerms); + } + + private void WriteApplication(string! op, IEnumerable! args, + LineariserOptions! options) { + WriteApplication(op, op, args, options, options.AsTerm); + } + + private void WriteTermApplication(string! op, IEnumerable! args, + LineariserOptions! options) { + ExprLineariser.AssertAsTerm(op, options); + WriteApplication(op, op, args, options, options.AsTerm); + } + + private void WriteApplication(string! termOp, string! predOp, + IEnumerable! args, LineariserOptions! options) { + WriteApplication(termOp, predOp, args, options, options.AsTerm); + } + + private void WriteApplication(string! termOp, string! predOp, + IEnumerable! args, LineariserOptions! options, + // change the AsTerm option for the arguments? + bool argsAsTerms) { + string! opName = options.AsTerm ? termOp : predOp; + LineariserOptions! newOptions = options.SetAsTerm(argsAsTerms); + + bool hasArgs = false; + foreach (VCExpr! e in args) { + if (!hasArgs) + wr.Write("({0}", opName); + wr.Write(" "); + ExprLineariser.Linearise(e, newOptions); + hasArgs = true; + } + + if (hasArgs) + wr.Write(")"); + else + wr.Write("{0}", opName); + } + + // write an application that can only be a term. + // if the expression is supposed to be printed as a formula, + // it is turned into an equation (EQ (f args) |@true|) + private void WriteApplicationTermOnly(string! termOp, + IEnumerable! args, LineariserOptions! options) { + if (!options.AsTerm) + // Write: (EQ (f args) |@true|) + // where "args" are written as terms + wr.Write("({0} ", eqName); + + WriteApplication(termOp, args, options, true); + + if (!options.AsTerm) + wr.Write(" {0})", boolTrueName); + } + + /////////////////////////////////////////////////////////////////////////////////// + + public bool VisitNotOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas + return true; + } + + private bool PrintEq(VCExprNAry! node, LineariserOptions! options) { + if (options.AsTerm) { + // use equality on terms, also if the arguments have type bool + assert node[0].Type.Equals(node[1].Type); + if (node[0].Type.IsBool) { + WriteApplication(boolIffName, node, options); + } else if (node[0].Type.IsInt) { + WriteApplication(termIntEqual, node, options); + } else { + // TODO: make this less hackish + CtorType t = node[0].Type as CtorType; + if (t != null && t.Decl.Name.Equals("U")) { + WriteApplication(termUEqual, node, options); + } else if (t != null && t.Decl.Name.Equals("T")) { + WriteApplication(termTEqual, node, options); + } else { + assert false; // unknown type + } + } + } else { + if (node[0].Type.IsBool) { + 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) { + return PrintEq(node, options); + } + + public bool VisitNeqOp (VCExprNAry! node, LineariserOptions! options) { + wr.Write("({0} ", options.AsTerm ? boolNotName : notName); + PrintEq(node, options); + wr.Write(")"); + return true; + } + + public bool VisitAndOp (VCExprNAry! node, LineariserOptions! options) { + assert options.AsTerm; + WriteApplication(boolAndName, andName, node, options); + return true; + } + + public bool VisitOrOp (VCExprNAry! node, LineariserOptions! options) { + assert options.AsTerm; + WriteApplication(boolOrName, orName, node, options); + return true; + } + + public bool VisitImpliesOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(boolImpliesName, impliesName, node, options); + return true; + } + + public bool VisitIfThenElseOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(boolIteName, iteName, node, options); + return true; + } + + public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) { + ExprLineariser.AssertAsFormula(distinctName, options); + + if (node.Length < 2) { + ExprLineariser.Linearise(VCExpressionGenerator.True, options); + } else { + wr.Write("({0}", distinctName); + foreach (VCExpr! e in node) { + wr.Write(" "); + ExprLineariser.LineariseAsTerm(e, options); + } + wr.Write(")"); + } + + return true; + } + + public bool VisitLabelOp (VCExprNAry! node, LineariserOptions! options) { + // 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) { + assert false; // should not occur in the output + } + + public bool VisitStoreOp (VCExprNAry! node, LineariserOptions! options) { + assert false; // should not occur in the output + } + + public bool VisitBvOp (VCExprNAry! node, LineariserOptions! options) { + assert false; // TODO + } + + public bool VisitBvExtractOp(VCExprNAry! node, LineariserOptions! options) { + assert false; // TODO + } + + public bool VisitBvConcatOp (VCExprNAry! node, LineariserOptions! options) { + assert false; // TODO + } + + public bool VisitAddOp (VCExprNAry! node, LineariserOptions! options) { + WriteTermApplication(intAddName, node, options); + return true; + } + + public bool VisitSubOp (VCExprNAry! node, LineariserOptions! options) { + WriteTermApplication(intSubName, node, options); + return true; + } + + public bool VisitMulOp (VCExprNAry! node, LineariserOptions! options) { + WriteTermApplication(intMulName, node, options); + return true; + } + + public bool VisitDivOp (VCExprNAry! node, LineariserOptions! options) { + WriteTermApplication(intDivName, node, options); + return true; + } + + public bool VisitModOp (VCExprNAry! node, LineariserOptions! options) { + WriteTermApplication(intModName, node, options); + return true; + } + + public bool VisitLtOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitLeOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitGtOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitGeOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitSubtypeOp (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(subtypeName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitSubtype3Op (VCExprNAry! node, LineariserOptions! options) { + WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitBoogieFunctionOp (VCExprNAry! node, LineariserOptions! options) { + VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op; + string! printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name)); + + // arguments are always terms + WriteApplicationTermOnly(printedName, node, options); + return true; + } + + } + } + +} diff --git a/Source/Provers/SMTLib/SMTLibLineariser.ssc b/Source/Provers/SMTLib/SMTLibLineariser.ssc deleted file mode 100644 index 7efa109f..00000000 --- a/Source/Provers/SMTLib/SMTLibLineariser.ssc +++ /dev/null @@ -1,642 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Text; -using System.IO; -using System.Collections; -using System.Collections.Generic; -using Microsoft.Contracts; -using Microsoft.Basetypes; -using Microsoft.Boogie.VCExprAST; - -// Method to turn VCExprs into strings that can be fed into SMT -// solvers. This is currently quite similar to the -// SimplifyLikeLineariser (but the code is independent) - -namespace Microsoft.Boogie.SMTLib -{ - - // Options for the linearisation - public class LineariserOptions { - - public readonly bool AsTerm; - public LineariserOptions! SetAsTerm(bool newVal) { - if (newVal) - return DefaultTerm; - else - return Default; - } - - internal LineariserOptions(bool asTerm) { - this.AsTerm = asTerm; - } - - public static readonly LineariserOptions! Default = new LineariserOptions (false); - internal static readonly LineariserOptions! DefaultTerm = new LineariserOptions (true); - } - - - //////////////////////////////////////////////////////////////////////////////////////// - - // Lineariser for expressions. The result (bool) is currently not used for anything - public class SMTLibExprLineariser : IVCExprVisitor { - - public static string! ToString(VCExpr! e, UniqueNamer! namer) { - StringWriter sw = new StringWriter(); - SMTLibExprLineariser! lin = new SMTLibExprLineariser (sw, namer); - lin.Linearise(e, LineariserOptions.Default); - return (!)sw.ToString(); - } - - //////////////////////////////////////////////////////////////////////////////////////// - - private readonly TextWriter! wr; - private SMTLibOpLineariser OpLinObject = null; - private IVCExprOpVisitor! OpLineariser { get { - if (OpLinObject == null) - OpLinObject = new SMTLibOpLineariser (this, wr); - return OpLinObject; - } } - - internal readonly UniqueNamer! Namer; - - public SMTLibExprLineariser(TextWriter! wr, UniqueNamer! namer) { - this.wr = wr; - this.Namer = namer; - } - - public void Linearise(VCExpr! expr, LineariserOptions! options) { - expr.Accept(this, options); - } - - public void LineariseAsTerm(VCExpr! expr, LineariserOptions! options) { - Linearise(expr, options.SetAsTerm(true)); - } - - ///////////////////////////////////////////////////////////////////////////////////// - - internal static string! TypeToString(Type! t) { - if (t.IsBool) - return "TermBool"; - else if (t.IsInt) - return "Int"; - else if (t.IsBv) - assert false; // bitvectors are currently not handled for SMT-Lib solvers - else { - // at this point, only the types U, T should be left - System.IO.StringWriter buffer = new System.IO.StringWriter(); - using (TokenTextWriter stream = new TokenTextWriter("", buffer, false)) { - t.Emit(stream); - } - return "boogie" + buffer.ToString(); - } - } - - ///////////////////////////////////////////////////////////////////////////////////// - - public static string! MakeIdPrintable(string! s) { - // make sure that no keywords are used as identifiers - switch(s) { - case andName: - case orName: - case notName: - case impliesName: - case iffName: - case eqName: - case distinctName: - case TRUEName: - case FALSEName: - case "Array": - s = "nonkeyword_" + s; - break; - } - - string! newS = ""; - foreach (char ch in s) { - if (Char.IsLetterOrDigit(ch) || ch == '.' || ch == '\'' || ch == '_') - newS = newS + ch; - else - // replace everything else with a . - newS = newS + '.'; - } - - // ensure that the first character is not . or _ (some SMT-solvers do - // not like that, e.g., yices and cvc3) - if (newS[0] == '.' || newS[0] == '_') - newS = "x" + newS; - - return newS; - } - - ///////////////////////////////////////////////////////////////////////////////////// - - /// - /// The name for logical conjunction in Simplify - /// - internal const string! andName = "and"; // conjunction - internal const string! orName = "or"; // disjunction - internal const string! notName = "not"; // negation - internal const string! impliesName = "implies"; // implication - internal const string! iteName = "ite"; // if-then-else - internal const string! iffName = "iff"; // logical equivalence - internal const string! eqName = "="; // equality - internal const string! lessName = "<"; - internal const string! greaterName = ">"; - internal const string! atmostName = "<="; - internal const string! atleastName = ">="; - internal const string! TRUEName = "true"; // nullary predicate that is always true - internal const string! FALSEName = "false"; // nullary predicate that is always false - internal const string! subtypeName = "UOrdering2"; - internal const string! subtypeArgsName = "UOrdering3"; - - internal const string! distinctName = "distinct"; - - internal const string! boolTrueName = "boolTrue"; - internal const string! boolFalseName = "boolFalse"; - internal const string! boolAndName = "boolAnd"; - internal const string! boolOrName = "boolOr"; - internal const string! boolNotName = "boolNot"; - internal const string! boolIffName = "boolIff"; - internal const string! boolImpliesName = "boolImplies"; - internal const string! boolIteName = "ite"; - internal const string! termUEqual = "UEqual"; - internal const string! termTEqual = "TEqual"; - internal const string! termIntEqual = "IntEqual"; - internal const string! termLessName = "intLess"; - internal const string! termGreaterName = "intGreater"; - internal const string! termAtmostName = "intAtMost"; - internal const string! termAtleastName = "intAtLeast"; - internal const string! intAddName = "+"; - internal const string! intSubName = "-"; - internal const string! intMulName = "*"; - internal const string! intDivName = "boogieIntDiv"; - internal const string! intModName = "boogieIntMod"; - - internal void AssertAsTerm(string! x, LineariserOptions! options) { - if (!options.AsTerm) - System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!"); - } - - internal void AssertAsFormula(string! x, LineariserOptions! options) { - if (options.AsTerm) - System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!"); - } - - ///////////////////////////////////////////////////////////////////////////////////// - - public bool Visit(VCExprLiteral! node, LineariserOptions! options) { - if (options.AsTerm) { - - if (node == VCExpressionGenerator.True) - wr.Write("{0}", boolTrueName); - else if (node == VCExpressionGenerator.False) - wr.Write("{0}", boolFalseName); - else if (node is VCExprIntLit) { - // some SMT-solvers do not understand negative literals - // (e.g., yices) - BigNum lit = ((VCExprIntLit)node).Val; - if (lit.IsNegative) - wr.Write("({0} 0 {1})", intSubName, lit.Abs); - else - wr.Write(lit); - } else - assert false; - - } 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 - assert false; - - } - - return true; - } - - ///////////////////////////////////////////////////////////////////////////////////// - - public bool Visit(VCExprNAry! node, LineariserOptions! options) { - VCExprOp! op = node.Op; - - if (!options.AsTerm && - (op.Equals(VCExpressionGenerator.AndOp) || - op.Equals(VCExpressionGenerator.OrOp))) { - // handle these operators without recursion - - wr.Write("({0}", - op.Equals(VCExpressionGenerator.AndOp) ? andName : orName); - IEnumerator! enumerator = new VCExprNAryUniformOpEnumerator (node); - while (enumerator.MoveNext()) { - VCExprNAry naryExpr = enumerator.Current as VCExprNAry; - if (naryExpr == null || !naryExpr.Op.Equals(op)) { - wr.Write(" "); - Linearise((VCExpr!)enumerator.Current, options); - } - } - - wr.Write(")"); - - return true; - } - - return node.Accept(OpLineariser, options); - } - - ///////////////////////////////////////////////////////////////////////////////////// - - public bool Visit(VCExprVar! node, LineariserOptions! options) { - string! printedName = Namer.GetName(node, MakeIdPrintable(node.Name)); - - if (options.AsTerm || - // formula variables are easy to identify in SMT-Lib - printedName[0] == '$') - wr.Write("{0}", printedName); - else - wr.Write("({0} {1} {2})", eqName, printedName, boolTrueName); - - return true; - } - - ///////////////////////////////////////////////////////////////////////////////////// - - public bool Visit(VCExprQuantifier! node, LineariserOptions! options) { - AssertAsFormula(node.Quan.ToString(), options); - assert node.TypeParameters.Count == 0; - - Namer.PushScope(); try { - - string! kind = node.Quan == Quantifier.ALL ? "forall" : "exists"; - wr.Write("({0} ", kind); - - for (int i = 0; i < node.BoundVars.Count; i++) - { - VCExprVar! var = node.BoundVars[i]; - // ensure that the variable name starts with ? - string! printedName = Namer.GetLocalName(var, "?" + MakeIdPrintable(var.Name)); - assert printedName[0] == '?'; - wr.Write("({0} {1}) ", printedName, TypeToString(var.Type)); - } - - /* if (options.QuantifierIds) { - // only needed for Z3 - VCQuantifierInfos! infos = node.Infos; - if (infos.qid != null) { - wr.Write("(QID "); - wr.Write(infos.qid); - wr.Write(") "); - } - if (0 <= infos.uniqueId) { - wr.Write("(SKOLEMID "); - wr.Write(infos.uniqueId); - wr.Write(") "); - } - } */ - - Linearise(node.Body, options); - - WriteTriggers(node.Triggers, options); - wr.Write(")"); - - return true; - - } finally { - Namer.PopScope(); - } - } - - private void WriteTriggers(List! triggers, LineariserOptions! options) { - // first, count how many neg/pos triggers there are - int negTriggers = 0; - int posTriggers = 0; - foreach (VCTrigger! vcTrig in triggers) { - if (vcTrig.Pos) { - posTriggers++; - } else { - negTriggers++; - } - } - - if (posTriggers > 0) { - foreach (VCTrigger! vcTrig in triggers) { - if (vcTrig.Pos) { - wr.Write(" :pat {"); - foreach (VCExpr! e in vcTrig.Exprs) { - wr.Write(" "); - LineariseAsTerm(e, options); - } - wr.Write(" } "); - } - } - } else if (negTriggers > 0) { - // if also positive triggers are given, the SMT solver (at least Z3) - // will ignore the negative patterns and output a warning. Therefore - // we never specify both negative and positive triggers - foreach (VCTrigger! vcTrig in triggers) { - if (!vcTrig.Pos) { - wr.Write(" :nopat { "); - assert vcTrig.Exprs.Count == 1; - wr.Write(" "); - LineariseAsTerm(vcTrig.Exprs[0], options); - wr.Write(" } "); - } - } - } - } - - ///////////////////////////////////////////////////////////////////////////////////// - - public bool Visit(VCExprLet! node, LineariserOptions! options) { - Namer.PushScope(); try { - - foreach (VCExprLetBinding! b in node) { - bool formula = b.V.Type.IsBool; - - wr.Write("({0} (", formula ? "flet" : "let"); - string! printedName = Namer.GetLocalName(b.V, "$" + MakeIdPrintable(b.V.Name)); - assert printedName[0] == '$'; - - wr.Write("{0} ", printedName); - Linearise(b.E, options.SetAsTerm(!formula)); - wr.Write(") "); - } - Linearise(node.Body, options); - - for (int i = 0; i < node.Length; ++i) - wr.Write(")"); - - return true; - - } finally { - Namer.PopScope(); - } - } - - ///////////////////////////////////////////////////////////////////////////////////// - - // Lineariser for operator terms. The result (bool) is currently not used for anything - internal class SMTLibOpLineariser : IVCExprOpVisitor { - private readonly SMTLibExprLineariser! ExprLineariser; - private readonly TextWriter! wr; - - public SMTLibOpLineariser(SMTLibExprLineariser! ExprLineariser, TextWriter! wr) { - this.ExprLineariser = ExprLineariser; - this.wr = wr; - } - - /////////////////////////////////////////////////////////////////////////////////// - - private void WriteApplication(string! op, IEnumerable! args, - LineariserOptions! options, - bool argsAsTerms) { - WriteApplication(op, op, args, options, argsAsTerms); - } - - private void WriteApplication(string! op, IEnumerable! args, - LineariserOptions! options) { - WriteApplication(op, op, args, options, options.AsTerm); - } - - private void WriteTermApplication(string! op, IEnumerable! args, - LineariserOptions! options) { - ExprLineariser.AssertAsTerm(op, options); - WriteApplication(op, op, args, options, options.AsTerm); - } - - private void WriteApplication(string! termOp, string! predOp, - IEnumerable! args, LineariserOptions! options) { - WriteApplication(termOp, predOp, args, options, options.AsTerm); - } - - private void WriteApplication(string! termOp, string! predOp, - IEnumerable! args, LineariserOptions! options, - // change the AsTerm option for the arguments? - bool argsAsTerms) { - string! opName = options.AsTerm ? termOp : predOp; - LineariserOptions! newOptions = options.SetAsTerm(argsAsTerms); - - bool hasArgs = false; - foreach (VCExpr! e in args) { - if (!hasArgs) - wr.Write("({0}", opName); - wr.Write(" "); - ExprLineariser.Linearise(e, newOptions); - hasArgs = true; - } - - if (hasArgs) - wr.Write(")"); - else - wr.Write("{0}", opName); - } - - // write an application that can only be a term. - // if the expression is supposed to be printed as a formula, - // it is turned into an equation (EQ (f args) |@true|) - private void WriteApplicationTermOnly(string! termOp, - IEnumerable! args, LineariserOptions! options) { - if (!options.AsTerm) - // Write: (EQ (f args) |@true|) - // where "args" are written as terms - wr.Write("({0} ", eqName); - - WriteApplication(termOp, args, options, true); - - if (!options.AsTerm) - wr.Write(" {0})", boolTrueName); - } - - /////////////////////////////////////////////////////////////////////////////////// - - public bool VisitNotOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas - return true; - } - - private bool PrintEq(VCExprNAry! node, LineariserOptions! options) { - if (options.AsTerm) { - // use equality on terms, also if the arguments have type bool - assert node[0].Type.Equals(node[1].Type); - if (node[0].Type.IsBool) { - WriteApplication(boolIffName, node, options); - } else if (node[0].Type.IsInt) { - WriteApplication(termIntEqual, node, options); - } else { - // TODO: make this less hackish - CtorType t = node[0].Type as CtorType; - if (t != null && t.Decl.Name.Equals("U")) { - WriteApplication(termUEqual, node, options); - } else if (t != null && t.Decl.Name.Equals("T")) { - WriteApplication(termTEqual, node, options); - } else { - assert false; // unknown type - } - } - } else { - if (node[0].Type.IsBool) { - 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) { - return PrintEq(node, options); - } - - public bool VisitNeqOp (VCExprNAry! node, LineariserOptions! options) { - wr.Write("({0} ", options.AsTerm ? boolNotName : notName); - PrintEq(node, options); - wr.Write(")"); - return true; - } - - public bool VisitAndOp (VCExprNAry! node, LineariserOptions! options) { - assert options.AsTerm; - WriteApplication(boolAndName, andName, node, options); - return true; - } - - public bool VisitOrOp (VCExprNAry! node, LineariserOptions! options) { - assert options.AsTerm; - WriteApplication(boolOrName, orName, node, options); - return true; - } - - public bool VisitImpliesOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(boolImpliesName, impliesName, node, options); - return true; - } - - public bool VisitIfThenElseOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(boolIteName, iteName, node, options); - return true; - } - - public bool VisitDistinctOp (VCExprNAry! node, LineariserOptions! options) { - ExprLineariser.AssertAsFormula(distinctName, options); - - if (node.Length < 2) { - ExprLineariser.Linearise(VCExpressionGenerator.True, options); - } else { - wr.Write("({0}", distinctName); - foreach (VCExpr! e in node) { - wr.Write(" "); - ExprLineariser.LineariseAsTerm(e, options); - } - wr.Write(")"); - } - - return true; - } - - public bool VisitLabelOp (VCExprNAry! node, LineariserOptions! options) { - // 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) { - assert false; // should not occur in the output - } - - public bool VisitStoreOp (VCExprNAry! node, LineariserOptions! options) { - assert false; // should not occur in the output - } - - public bool VisitBvOp (VCExprNAry! node, LineariserOptions! options) { - assert false; // TODO - } - - public bool VisitBvExtractOp(VCExprNAry! node, LineariserOptions! options) { - assert false; // TODO - } - - public bool VisitBvConcatOp (VCExprNAry! node, LineariserOptions! options) { - assert false; // TODO - } - - public bool VisitAddOp (VCExprNAry! node, LineariserOptions! options) { - WriteTermApplication(intAddName, node, options); - return true; - } - - public bool VisitSubOp (VCExprNAry! node, LineariserOptions! options) { - WriteTermApplication(intSubName, node, options); - return true; - } - - public bool VisitMulOp (VCExprNAry! node, LineariserOptions! options) { - WriteTermApplication(intMulName, node, options); - return true; - } - - public bool VisitDivOp (VCExprNAry! node, LineariserOptions! options) { - WriteTermApplication(intDivName, node, options); - return true; - } - - public bool VisitModOp (VCExprNAry! node, LineariserOptions! options) { - WriteTermApplication(intModName, node, options); - return true; - } - - public bool VisitLtOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms - return true; - } - - public bool VisitLeOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms - return true; - } - - public bool VisitGtOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms - return true; - } - - public bool VisitGeOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms - return true; - } - - public bool VisitSubtypeOp (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(subtypeName, node, options, true); // arguments are always terms - return true; - } - - public bool VisitSubtype3Op (VCExprNAry! node, LineariserOptions! options) { - WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms - return true; - } - - public bool VisitBoogieFunctionOp (VCExprNAry! node, LineariserOptions! options) { - VCExprBoogieFunctionOp! op = (VCExprBoogieFunctionOp)node.Op; - string! printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name)); - - // arguments are always terms - WriteApplicationTermOnly(printedName, node, options); - return true; - } - - } - } - -} diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs new file mode 100644 index 00000000..08c0e6a3 --- /dev/null +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -0,0 +1,107 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics; +using Microsoft.Contracts; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.SMTLib +{ + // Visitor for collecting the occurring function symbols in a VCExpr, + // and for creating the corresponding declarations + + public class TypeDeclCollector : BoundVarTraversingVCExprVisitor { + + private readonly UniqueNamer! Namer; + + public TypeDeclCollector(UniqueNamer! namer) { + this.Namer = namer; + } + + // not used + protected override bool StandardResult(VCExpr! node, bool arg) { + return true; + } + + private readonly List! AllDecls = new List (); + private readonly List! IncDecls = new List (); + + private readonly IDictionary! KnownFunctions = + new Dictionary (); + private readonly IDictionary! KnownVariables = + new Dictionary (); + + public List! AllDeclarations { get { + List! res = new List (); + res.AddRange(AllDecls); + return res; + } } + + public List! GetNewDeclarations() { + List! res = new List (); + res.AddRange(IncDecls); + IncDecls.Clear(); + return res; + } + + private void AddDeclaration(string! decl) { + AllDecls.Add(decl); + IncDecls.Add(decl); + } + + public void Collect(VCExpr! expr) { + Traverse(expr, true); + } + + /////////////////////////////////////////////////////////////////////////// + + private static string! TypeToString(Type! t) { + return SMTLibExprLineariser.TypeToString(t); + } + + public override bool Visit(VCExprNAry! node, bool arg) { + // there are a couple of cases where operators have to be + // registered by generating appropriate statements + + VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; + if (op != null && !KnownFunctions.ContainsKey(op.Func)) { + Function! f = op.Func; + string! printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name)); + string! decl = ":extrafuns ((" + printedName; + + foreach (Variable! v in f.InParams) { + decl += " " + TypeToString(v.TypedIdent.Type); + } + assert f.OutParams.Length == 1; + foreach (Variable! v in f.OutParams) { + decl += " " + TypeToString(v.TypedIdent.Type); + } + + decl += "))"; + + AddDeclaration(decl); + KnownFunctions.Add(f, true); + } + + return base.Visit(node, arg); + } + + public override bool Visit(VCExprVar! node, bool arg) { + if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) { + string! printedName = Namer.GetName(node, SMTLibExprLineariser.MakeIdPrintable(node.Name)); + string! decl = + ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))"; + AddDeclaration(decl); + KnownVariables.Add(node, true); + } + + return base.Visit(node, arg); + } + } + +} \ No newline at end of file diff --git a/Source/Provers/SMTLib/TypeDeclCollector.ssc b/Source/Provers/SMTLib/TypeDeclCollector.ssc deleted file mode 100644 index 08c0e6a3..00000000 --- a/Source/Provers/SMTLib/TypeDeclCollector.ssc +++ /dev/null @@ -1,107 +0,0 @@ -//----------------------------------------------------------------------------- -// -// Copyright (C) Microsoft Corporation. All Rights Reserved. -// -//----------------------------------------------------------------------------- -using System; -using System.Collections; -using System.Collections.Generic; -using System.Diagnostics; -using Microsoft.Contracts; -using Microsoft.Boogie.VCExprAST; - -namespace Microsoft.Boogie.SMTLib -{ - // Visitor for collecting the occurring function symbols in a VCExpr, - // and for creating the corresponding declarations - - public class TypeDeclCollector : BoundVarTraversingVCExprVisitor { - - private readonly UniqueNamer! Namer; - - public TypeDeclCollector(UniqueNamer! namer) { - this.Namer = namer; - } - - // not used - protected override bool StandardResult(VCExpr! node, bool arg) { - return true; - } - - private readonly List! AllDecls = new List (); - private readonly List! IncDecls = new List (); - - private readonly IDictionary! KnownFunctions = - new Dictionary (); - private readonly IDictionary! KnownVariables = - new Dictionary (); - - public List! AllDeclarations { get { - List! res = new List (); - res.AddRange(AllDecls); - return res; - } } - - public List! GetNewDeclarations() { - List! res = new List (); - res.AddRange(IncDecls); - IncDecls.Clear(); - return res; - } - - private void AddDeclaration(string! decl) { - AllDecls.Add(decl); - IncDecls.Add(decl); - } - - public void Collect(VCExpr! expr) { - Traverse(expr, true); - } - - /////////////////////////////////////////////////////////////////////////// - - private static string! TypeToString(Type! t) { - return SMTLibExprLineariser.TypeToString(t); - } - - public override bool Visit(VCExprNAry! node, bool arg) { - // there are a couple of cases where operators have to be - // registered by generating appropriate statements - - VCExprBoogieFunctionOp op = node.Op as VCExprBoogieFunctionOp; - if (op != null && !KnownFunctions.ContainsKey(op.Func)) { - Function! f = op.Func; - string! printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name)); - string! decl = ":extrafuns ((" + printedName; - - foreach (Variable! v in f.InParams) { - decl += " " + TypeToString(v.TypedIdent.Type); - } - assert f.OutParams.Length == 1; - foreach (Variable! v in f.OutParams) { - decl += " " + TypeToString(v.TypedIdent.Type); - } - - decl += "))"; - - AddDeclaration(decl); - KnownFunctions.Add(f, true); - } - - return base.Visit(node, arg); - } - - public override bool Visit(VCExprVar! node, bool arg) { - if (!BoundTermVars.Contains(node) && !KnownVariables.ContainsKey(node)) { - string! printedName = Namer.GetName(node, SMTLibExprLineariser.MakeIdPrintable(node.Name)); - string! decl = - ":extrafuns ((" + printedName + " " + TypeToString(node.Type) + "))"; - AddDeclaration(decl); - KnownVariables.Add(node, true); - } - - return base.Visit(node, arg); - } - } - -} \ No newline at end of file -- cgit v1.2.3