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/TPTPLineariser.cs | 1480 ++++++++++++++++----------------- 1 file changed, 740 insertions(+), 740 deletions(-) (limited to 'Source/Provers/TPTP/TPTPLineariser.cs') 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() != 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 { - - public static string ToString(VCExpr e, UniqueNamer namer, TPTPProverOptions opts) { - Contract.Requires(e != null); - Contract.Requires(namer != null); - Contract.Ensures(Contract.Result() != 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/*!>!*/ OpLineariser { get { - Contract.Ensures(Contract.Result>() !=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(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() != 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(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 { - 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!*/> 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!*/> 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/*!>!*/ 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/*!>!*/ 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() != 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 { + + public static string ToString(VCExpr e, UniqueNamer namer, TPTPProverOptions opts) { + Contract.Requires(e != null); + Contract.Requires(namer != null); + Contract.Ensures(Contract.Result() != 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/*!>!*/ OpLineariser { get { + Contract.Ensures(Contract.Result>() !=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(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() != 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(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 { + 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!*/> 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!*/> 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/*!>!*/ 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/*!>!*/ 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; + } + + } + } + +} -- cgit v1.2.3