diff options
Diffstat (limited to 'Source/Provers/TPTP/TPTPLineariser.cs')
| -rw-r--r-- | Source/Provers/TPTP/TPTPLineariser.cs | 1480 |
1 files changed, 740 insertions, 740 deletions
diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs index a35d43f0..4bdf29b9 100644 --- a/Source/Provers/TPTP/TPTPLineariser.cs +++ b/Source/Provers/TPTP/TPTPLineariser.cs @@ -1,740 +1,740 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-
-// Method to turn VCExprs into strings that can be fed into TPTP provers.
-// This is currently quite similar to the
-// SimplifyLikeLineariser (but the code is independent)
-
-namespace Microsoft.Boogie.TPTP
-{
-
- // Options for the linearisation
- public class LineariserOptions {
-
- public readonly bool AsTerm;
- public LineariserOptions SetAsTerm(bool newVal) {
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- if (newVal)
- return DefaultTerm;
- else
- return Default;
- }
-
- internal LineariserOptions(bool asTerm) {
- this.AsTerm = asTerm;
- }
-
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Default!=null);
- Contract.Invariant(DefaultTerm!=null);
-}
-
- public static readonly LineariserOptions Default = new LineariserOptions (false);
- internal static readonly LineariserOptions DefaultTerm = new LineariserOptions (true);
- }
-
-
- ////////////////////////////////////////////////////////////////////////////////////////
-
- // Lineariser for expressions. The result (bool) is currently not used for anything
- public class TPTPExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {
-
- public static string ToString(VCExpr e, UniqueNamer namer, TPTPProverOptions opts) {
- Contract.Requires(e != null);
- Contract.Requires(namer != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- StringWriter sw = new StringWriter();
- TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer, opts);
- Contract.Assert(lin!=null);
- lin.Linearise(e, LineariserOptions.Default);
- return cce.NonNull(sw.ToString());
- }
-
- ////////////////////////////////////////////////////////////////////////////////////////
-
- private readonly TextWriter wr;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(wr!=null);
- Contract.Invariant(Namer != null);
-}
-
- private TPTPOpLineariser OpLinObject = null;
- private IVCExprOpVisitor<bool, LineariserOptions>/*!>!*/ OpLineariser { get {
- Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool,LineariserOptions>>() !=null);
-
- if (OpLinObject == null)
- OpLinObject = new TPTPOpLineariser(this, wr);
- return OpLinObject;
- } }
-
- internal readonly UniqueNamer Namer;
- internal readonly TPTPProverOptions Options;
-
- public TPTPExprLineariser(TextWriter wr, UniqueNamer namer, TPTPProverOptions opts) {
- Contract.Requires(wr != null);Contract.Requires(namer != null);
- this.wr = wr;
- this.Namer = namer;
- this.Options = opts;
- }
-
- public void Linearise(VCExpr expr, LineariserOptions options) {
- Contract.Requires(expr != null);
- Contract.Requires(options != null);
- expr.Accept<bool, LineariserOptions>(this, options);
- }
-
- public void LineariseAsTerm(VCExpr expr, LineariserOptions options) {
- Contract.Requires(expr != null);
- Contract.Requires(options != null);
- Linearise(expr, options.SetAsTerm(true));
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public static string MakeIdPrintable(string s) {
- Contract.Requires(s != null);
- Contract.Ensures(Contract.Result<string>() != null);
-
- // make sure that no keywords are used as identifiers
- switch(s) {
- case andName:
- case orName:
- case notName:
- case impliesName:
- case iffName:
- case eqName:
- case TRUEName:
- case FALSEName:
- case "Array":
- s = "nonkeyword_" + s;
- break;
- }
-
- var res = new StringBuilder();
-
- foreach (char ch in s) {
- if (Char.IsLetterOrDigit(ch))
- res.Append(ch);
- else
- // replace everything else with a _
- res.Append('_');
- }
-
- return res.ToString();
- }
-
- public static string Lowercase(string s)
- {
- if (char.IsLower(s[0])) return MakeIdPrintable(s);
- else return MakeIdPrintable("x" + s);
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- internal const string andName = "&"; // conjunction
- internal const string orName = "|"; // disjunction
- internal const string notName = "~"; // negation
- internal const string impliesName = "=>"; // implication
- internal const string iteName = "$itef"; // if-then-else
- internal const string iffName = "<=>"; // logical equivalence
- internal const string eqName = "="; // equality
- internal const string lessName = "lt";
- internal const string greaterName = "gt";
- internal const string atmostName = "le";
- internal const string atleastName = "ge";
- internal const string TRUEName = "$true"; // nullary predicate that is always true
- internal const string FALSEName = "$false"; // nullary predicate that is always false
- internal const string subtypeName = "UOrdering2";
- internal const string subtypeArgsName = "UOrdering3";
-
- internal const string boolTrueName = "boolTrue";
- internal const string boolFalseName = "boolFalse";
- internal const string boolIteName = "ite";
- internal const string intAddName = "intAdd";
- internal const string intSubName = "intSub";
- internal const string intMulName = "intMul";
- internal const string intDivName = "boogieIntDiv";
- internal const string intModName = "boogieIntMod";
-
- internal void AssertAsTerm(string x, LineariserOptions options) {
- Contract.Requires(x != null);
- Contract.Requires(options != null);
- if (!options.AsTerm)
- System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!");
- }
-
- internal void AssertAsFormula(string x, LineariserOptions options) {
- Contract.Requires(x != null);
- Contract.Requires(options != null);
- if (options.AsTerm)
- System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!");
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public bool Visit(VCExprLiteral node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- if (options.AsTerm) {
-
- if (node == VCExpressionGenerator.True)
- wr.Write("{0}", boolTrueName);
- else if (node == VCExpressionGenerator.False)
- wr.Write("{0}", boolFalseName);
- else if (node is VCExprIntLit) {
- BigNum lit = ((VCExprIntLit)node).Val;
- wr.Write(lit);
- } else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
-
- } else {
-
- if (node == VCExpressionGenerator.True)
- wr.Write("{0}", TRUEName);
- else if (node == VCExpressionGenerator.False)
- wr.Write("{0}", FALSEName);
- else if (node is VCExprIntLit) {
- System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!");
- } else
- {Contract.Assert(false); throw new cce.UnreachableException();}
-
- }
-
- return true;
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public bool Visit(VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- VCExprOp op = node.Op;
- Contract.Assert(op!=null);
-
- if (!options.AsTerm &&
- (op.Equals(VCExpressionGenerator.AndOp) ||
- op.Equals(VCExpressionGenerator.OrOp))) {
- // handle these operators without recursion
-
- var sop = op.Equals(VCExpressionGenerator.AndOp) ? andName : orName;
- wr.Write("(");
- IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node);
- Contract.Assert(enumerator!=null);
- var cnt = 0;
- while (enumerator.MoveNext()) {
- VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
- if (naryExpr == null || !naryExpr.Op.Equals(op)) {
- if (cnt > 0)
- wr.Write(" {0} ", sop);
- cnt++;
- Linearise(cce.NonNull((VCExpr)enumerator.Current), options);
- }
- }
-
- wr.Write(")");
-
- return true;
- }
-
- return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options);
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public bool Visit(VCExprVar node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- string printedName = Namer.GetName(node, MakeIdPrintable(Lowercase(node.Name)));
- Contract.Assert(printedName!=null);
-
- if (options.AsTerm ||
- // formula variables are easy to identify in SMT-Lib
- printedName[0] == '$')
- wr.Write("{0}", printedName);
- else
- wr.Write("({0} = {1})", printedName, boolTrueName);
-
- return true;
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public bool Visit(VCExprQuantifier node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- AssertAsFormula(node.Quan.ToString(), options);
- Contract.Assert(node.TypeParameters.Count == 0);
-
- Namer.PushScope(); try {
-
- string kind = node.Quan == Quantifier.ALL ? "!" : "?";
- wr.Write("{0} [", kind);
-
- for (int i = 0; i < node.BoundVars.Count; i++)
- {
- VCExprVar var = node.BoundVars[i];
- Contract.Assert(var!=null);
- // ensure that the variable name starts with ?
- string printedName = Namer.GetLocalName(var, "V" + MakeIdPrintable(var.Name));
- Contract.Assert(printedName!=null);
- Contract.Assert(printedName[0] == 'V');
- if (i > 0) wr.Write(",");
- wr.Write("{0}", printedName);
- }
-
- wr.Write("] : (");
-
- /* if (options.QuantifierIds) {
- // only needed for Z3
- VCQuantifierInfos! infos = node.Infos;
- if (infos.qid != null) {
- wr.Write("(QID ");
- wr.Write(infos.qid);
- wr.Write(") ");
- }
- if (0 <= infos.uniqueId) {
- wr.Write("(SKOLEMID ");
- wr.Write(infos.uniqueId);
- wr.Write(") ");
- }
- } */
-
- Linearise(node.Body, options);
-
- // WriteTriggers(node.Triggers, options);
- wr.Write(")");
-
- return true;
-
- } finally {
- Namer.PopScope();
- }
- }
-
-
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public bool Visit(VCExprLet node, LineariserOptions options) {
- throw new NotImplementedException();
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- // Lineariser for operator terms. The result (bool) is currently not used for anything
- internal class TPTPOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/> {
- private readonly TPTPExprLineariser ExprLineariser;
- private readonly TextWriter wr;
- [ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(wr!=null);
- Contract.Invariant(ExprLineariser!=null);
-}
-
-
- public TPTPOpLineariser(TPTPExprLineariser ExprLineariser, TextWriter wr) {
- Contract.Requires(ExprLineariser != null);
- Contract.Requires(wr != null);
- this.ExprLineariser = ExprLineariser;
- this.wr = wr;
- }
-
- ///////////////////////////////////////////////////////////////////////////////////
-
- private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
- LineariserOptions options) {
- Contract.Requires(op != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- WriteApplication(op, args, options, options.AsTerm);
- }
-
- private void WriteTermApplication(string op, IEnumerable<VCExpr/*!>!*/> args,
- LineariserOptions options) {
- Contract.Requires(op != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- ExprLineariser.AssertAsTerm(op, options);
- WriteApplication(op, args, options, options.AsTerm);
- }
-
-
- private void WriteApplication(string termOp,
- IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options,
- // change the AsTerm option for the arguments?
- bool argsAsTerms) {
- Contract.Requires(termOp != null);
- Contract.Requires(cce.NonNullElements(args ));
- Contract.Requires(options != null);
- LineariserOptions newOptions = options.SetAsTerm(argsAsTerms);
- Contract.Assert(newOptions!=null);
-
- var argCnt = 0;
- if (termOp == "~") {
- wr.Write("(~ ");
- foreach (var e in args) {
- ExprLineariser.Linearise(e, newOptions);
- argCnt++;
- }
- Contract.Assert(argCnt == 1);
- wr.Write(")");
- } else if ("&|~=><".IndexOf(termOp[0]) >= 0) {
- wr.Write("(");
- foreach (var e in args) {
- ExprLineariser.Linearise(e, newOptions);
- argCnt++;
- if (argCnt == 1) {
- wr.Write(" {0} ", termOp);
- }
- }
- Contract.Assert(argCnt == 2);
- wr.Write(")");
- } else {
- wr.Write(termOp);
- foreach (var e in args) {
- Contract.Assert(e != null);
- if (argCnt == 0)
- wr.Write("(");
- else
- wr.Write(", ");
- argCnt++;
- ExprLineariser.Linearise(e, newOptions);
- }
-
- if (argCnt > 0)
- wr.Write(")");
- }
- }
-
- // write an application that can only be a term.
- // if the expression is supposed to be printed as a formula,
- // it is turned into an equation (EQ (f args) |@true|)
- private void WriteApplicationTermOnly(string termOp,
- IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options) {
- Contract.Requires(termOp != null);
- Contract.Requires(cce.NonNullElements(args));
- Contract.Requires(options != null);
- if (!options.AsTerm)
- // Write: (EQ (f args) |@true|)
- // where "args" are written as terms
- wr.Write("(", eqName);
-
- WriteApplication(termOp, args, options, true);
-
- if (!options.AsTerm)
- wr.Write(" = {0})", boolTrueName);
- }
-
- ///////////////////////////////////////////////////////////////////////////////////
-
- public bool VisitNotOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- WriteApplication(notName, node, options); // arguments can be both terms and formulas
- return true;
- }
-
- private bool PrintEq(VCExprNAry node, LineariserOptions options) {
- Contract.Requires(node != null);
- Contract.Requires(options != null);
- if (options.AsTerm) {
- throw new NotImplementedException();
- } else {
- if (node[0].Type.IsBool) {
- Contract.Assert(node[1].Type.IsBool);
- // use equivalence
- WriteApplication(iffName, node, options);
- } else {
- // use equality and write the arguments as terms
- WriteApplication(eqName, node, options, true);
- }
- }
-
- return true;
- }
-
- public bool VisitEqOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- return PrintEq(node, options);
- }
-
- public bool VisitNeqOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- wr.Write("(~ ");
- PrintEq(node, options);
- wr.Write(")");
- return true;
- }
-
- public bool VisitAndOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- Contract.Assert(options.AsTerm);
- WriteApplication(andName, node, options);
- return true;
- }
-
- public bool VisitOrOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- Contract.Assert(options.AsTerm);
- WriteApplication(orName, node, options);
- return true;
- }
-
- public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(impliesName, node, options);
- return true;
- }
-
- public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- throw new NotImplementedException();
- }
-
- public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- VCExprCustomOp op = (VCExprCustomOp)node.Op;
- WriteApplicationTermOnly(op.Name, node, options);
- return true;
- }
-
- public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- ExprLineariser.AssertAsFormula("distinct", options);
-
- if (node.Length < 2) {
- ExprLineariser.Linearise(VCExpressionGenerator.True, options);
- } else {
- var bits = 0;
- var cnt = node.Length;
- while (cnt > 0) {
- cnt >>= 1;
- bits++;
- }
-
- wr.Write("($true ");
- foreach (VCExpr e in node) {
- for (var i = 0; i < bits; ++i) {
- var neg = (cnt & (1 << i)) != 0 ? "~" : "";
- wr.Write(" & {0}distinct__f__{1}(", neg, i);
- ExprLineariser.LineariseAsTerm(e, options);
- wr.Write(")");
- }
- wr.WriteLine();
- cnt++;
- }
- wr.Write(")");
- }
-
- return true;
- }
-
- public bool VisitLabelOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
- //Contract.Requires(node.Length>=1);
- // VCExprLabelOp! op = (VCExprLabelOp)node.Op;
- // TODO
- // wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label));
- ExprLineariser.Linearise(node[0], options);
- // wr.Write(")");
- return true;
- }
-
- public bool VisitSelectOp(VCExprNAry node, LineariserOptions options)
- {
- //Contract.Requires(options != null);
- //Contract.Requires(node != null);
- var name = Lowercase(SimplifyLikeExprLineariser.SelectOpName(node));
- wr.Write(name + "(");
- var cnt = 0;
- foreach (VCExpr/*!*/ e in node) {
- Contract.Assert(e != null);
- if (cnt++ > 0)
- wr.Write(", ");
- ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
- }
- wr.Write(")");
- return true;
- }
-
- public bool VisitStoreOp(VCExprNAry node, LineariserOptions options)
- {
- //Contract.Requires(options != null);
- //Contract.Requires(node != null);
- var name = Lowercase(SimplifyLikeExprLineariser.StoreOpName(node));
- wr.Write(name + "(");
- var cnt = 0;
- foreach (VCExpr e in node) {
- Contract.Assert(e != null);
- if (cnt++ > 0)
- wr.Write(", ");
- ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
- }
- wr.Write(")");
- return true;
- }
-
- public bool VisitBvOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- {Contract.Assert(false); throw new NotImplementedException();} // TODO
- }
-
- public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- {Contract.Assert(false); throw new NotImplementedException();} // TODO
- }
-
- public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- {Contract.Assert(false); throw new NotImplementedException();} // TODO
- }
-
- public bool VisitAddOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intAddName, node, options);
- return true;
- }
-
- public bool VisitSubOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intSubName, node, options);
- return true;
- }
-
- public bool VisitMulOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intMulName, node, options);
- return true;
- }
-
- public bool VisitDivOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intDivName, node, options);
- return true;
- }
-
- public bool VisitModOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteTermApplication(intModName, node, options);
- return true;
- }
-
- public bool VisitLtOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(lessName, node, options, true); // arguments are always terms
- return true;
- }
-
- public bool VisitLeOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(atmostName, node, options, true); // arguments are always terms
- return true;
- }
-
- public bool VisitGtOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(greaterName, node, options, true); // arguments are always terms
- return true;
- }
-
- public bool VisitGeOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(atleastName, node, options, true); // arguments are always terms
- return true;
- }
-
- public bool VisitSubtypeOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(subtypeName, node, options, true); // arguments are always terms
- return true;
- }
-
- public bool VisitSubtype3Op (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms
- return true;
- }
-
- public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options) {
- //Contract.Requires(node != null);
- //Contract.Requires(options != null);
-
- VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op;
- Contract.Assert(op!=null);
- string printedName = ExprLineariser.Namer.GetName(op.Func, Lowercase(op.Func.Name));
- Contract.Assert(printedName!=null);
-
- if (ExprLineariser.Options.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool)
- WriteApplication(printedName, node, options, true);
- else
- // arguments are always terms
- WriteApplicationTermOnly(printedName, node, options);
- return true;
- }
-
- }
- }
-
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.IO; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; + +// Method to turn VCExprs into strings that can be fed into TPTP provers. +// This is currently quite similar to the +// SimplifyLikeLineariser (but the code is independent) + +namespace Microsoft.Boogie.TPTP +{ + + // Options for the linearisation + public class LineariserOptions { + + public readonly bool AsTerm; + public LineariserOptions SetAsTerm(bool newVal) { + Contract.Ensures(Contract.Result<LineariserOptions>() != null); + + if (newVal) + return DefaultTerm; + else + return Default; + } + + internal LineariserOptions(bool asTerm) { + this.AsTerm = asTerm; + } + + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(Default!=null); + Contract.Invariant(DefaultTerm!=null); +} + + public static readonly LineariserOptions Default = new LineariserOptions (false); + internal static readonly LineariserOptions DefaultTerm = new LineariserOptions (true); + } + + + //////////////////////////////////////////////////////////////////////////////////////// + + // Lineariser for expressions. The result (bool) is currently not used for anything + public class TPTPExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> { + + public static string ToString(VCExpr e, UniqueNamer namer, TPTPProverOptions opts) { + Contract.Requires(e != null); + Contract.Requires(namer != null); + Contract.Ensures(Contract.Result<string>() != null); + + StringWriter sw = new StringWriter(); + TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer, opts); + Contract.Assert(lin!=null); + lin.Linearise(e, LineariserOptions.Default); + return cce.NonNull(sw.ToString()); + } + + //////////////////////////////////////////////////////////////////////////////////////// + + private readonly TextWriter wr; + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(wr!=null); + Contract.Invariant(Namer != null); +} + + private TPTPOpLineariser OpLinObject = null; + private IVCExprOpVisitor<bool, LineariserOptions>/*!>!*/ OpLineariser { get { + Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool,LineariserOptions>>() !=null); + + if (OpLinObject == null) + OpLinObject = new TPTPOpLineariser(this, wr); + return OpLinObject; + } } + + internal readonly UniqueNamer Namer; + internal readonly TPTPProverOptions Options; + + public TPTPExprLineariser(TextWriter wr, UniqueNamer namer, TPTPProverOptions opts) { + Contract.Requires(wr != null);Contract.Requires(namer != null); + this.wr = wr; + this.Namer = namer; + this.Options = opts; + } + + public void Linearise(VCExpr expr, LineariserOptions options) { + Contract.Requires(expr != null); + Contract.Requires(options != null); + expr.Accept<bool, LineariserOptions>(this, options); + } + + public void LineariseAsTerm(VCExpr expr, LineariserOptions options) { + Contract.Requires(expr != null); + Contract.Requires(options != null); + Linearise(expr, options.SetAsTerm(true)); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public static string MakeIdPrintable(string s) { + Contract.Requires(s != null); + Contract.Ensures(Contract.Result<string>() != null); + + // make sure that no keywords are used as identifiers + switch(s) { + case andName: + case orName: + case notName: + case impliesName: + case iffName: + case eqName: + case TRUEName: + case FALSEName: + case "Array": + s = "nonkeyword_" + s; + break; + } + + var res = new StringBuilder(); + + foreach (char ch in s) { + if (Char.IsLetterOrDigit(ch)) + res.Append(ch); + else + // replace everything else with a _ + res.Append('_'); + } + + return res.ToString(); + } + + public static string Lowercase(string s) + { + if (char.IsLower(s[0])) return MakeIdPrintable(s); + else return MakeIdPrintable("x" + s); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + internal const string andName = "&"; // conjunction + internal const string orName = "|"; // disjunction + internal const string notName = "~"; // negation + internal const string impliesName = "=>"; // implication + internal const string iteName = "$itef"; // if-then-else + internal const string iffName = "<=>"; // logical equivalence + internal const string eqName = "="; // equality + internal const string lessName = "lt"; + internal const string greaterName = "gt"; + internal const string atmostName = "le"; + internal const string atleastName = "ge"; + internal const string TRUEName = "$true"; // nullary predicate that is always true + internal const string FALSEName = "$false"; // nullary predicate that is always false + internal const string subtypeName = "UOrdering2"; + internal const string subtypeArgsName = "UOrdering3"; + + internal const string boolTrueName = "boolTrue"; + internal const string boolFalseName = "boolFalse"; + internal const string boolIteName = "ite"; + internal const string intAddName = "intAdd"; + internal const string intSubName = "intSub"; + internal const string intMulName = "intMul"; + internal const string intDivName = "boogieIntDiv"; + internal const string intModName = "boogieIntMod"; + + internal void AssertAsTerm(string x, LineariserOptions options) { + Contract.Requires(x != null); + Contract.Requires(options != null); + if (!options.AsTerm) + System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!"); + } + + internal void AssertAsFormula(string x, LineariserOptions options) { + Contract.Requires(x != null); + Contract.Requires(options != null); + if (options.AsTerm) + System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!"); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprLiteral node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + if (options.AsTerm) { + + if (node == VCExpressionGenerator.True) + wr.Write("{0}", boolTrueName); + else if (node == VCExpressionGenerator.False) + wr.Write("{0}", boolFalseName); + else if (node is VCExprIntLit) { + BigNum lit = ((VCExprIntLit)node).Val; + wr.Write(lit); + } else { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + + } else { + + if (node == VCExpressionGenerator.True) + wr.Write("{0}", TRUEName); + else if (node == VCExpressionGenerator.False) + wr.Write("{0}", FALSEName); + else if (node is VCExprIntLit) { + System.Diagnostics.Debug.Fail("One should never write IntLit as a predicate!"); + } else + {Contract.Assert(false); throw new cce.UnreachableException();} + + } + + return true; + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + VCExprOp op = node.Op; + Contract.Assert(op!=null); + + if (!options.AsTerm && + (op.Equals(VCExpressionGenerator.AndOp) || + op.Equals(VCExpressionGenerator.OrOp))) { + // handle these operators without recursion + + var sop = op.Equals(VCExpressionGenerator.AndOp) ? andName : orName; + wr.Write("("); + IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node); + Contract.Assert(enumerator!=null); + var cnt = 0; + while (enumerator.MoveNext()) { + VCExprNAry naryExpr = enumerator.Current as VCExprNAry; + if (naryExpr == null || !naryExpr.Op.Equals(op)) { + if (cnt > 0) + wr.Write(" {0} ", sop); + cnt++; + Linearise(cce.NonNull((VCExpr)enumerator.Current), options); + } + } + + wr.Write(")"); + + return true; + } + + return node.Accept<bool, LineariserOptions/*!*/>(OpLineariser, options); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprVar node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + string printedName = Namer.GetName(node, MakeIdPrintable(Lowercase(node.Name))); + Contract.Assert(printedName!=null); + + if (options.AsTerm || + // formula variables are easy to identify in SMT-Lib + printedName[0] == '$') + wr.Write("{0}", printedName); + else + wr.Write("({0} = {1})", printedName, boolTrueName); + + return true; + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprQuantifier node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + AssertAsFormula(node.Quan.ToString(), options); + Contract.Assert(node.TypeParameters.Count == 0); + + Namer.PushScope(); try { + + string kind = node.Quan == Quantifier.ALL ? "!" : "?"; + wr.Write("{0} [", kind); + + for (int i = 0; i < node.BoundVars.Count; i++) + { + VCExprVar var = node.BoundVars[i]; + Contract.Assert(var!=null); + // ensure that the variable name starts with ? + string printedName = Namer.GetLocalName(var, "V" + MakeIdPrintable(var.Name)); + Contract.Assert(printedName!=null); + Contract.Assert(printedName[0] == 'V'); + if (i > 0) wr.Write(","); + wr.Write("{0}", printedName); + } + + wr.Write("] : ("); + + /* if (options.QuantifierIds) { + // only needed for Z3 + VCQuantifierInfos! infos = node.Infos; + if (infos.qid != null) { + wr.Write("(QID "); + wr.Write(infos.qid); + wr.Write(") "); + } + if (0 <= infos.uniqueId) { + wr.Write("(SKOLEMID "); + wr.Write(infos.uniqueId); + wr.Write(") "); + } + } */ + + Linearise(node.Body, options); + + // WriteTriggers(node.Triggers, options); + wr.Write(")"); + + return true; + + } finally { + Namer.PopScope(); + } + } + + + + ///////////////////////////////////////////////////////////////////////////////////// + + public bool Visit(VCExprLet node, LineariserOptions options) { + throw new NotImplementedException(); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + // Lineariser for operator terms. The result (bool) is currently not used for anything + internal class TPTPOpLineariser : IVCExprOpVisitor<bool, LineariserOptions/*!*/> { + private readonly TPTPExprLineariser ExprLineariser; + private readonly TextWriter wr; + [ContractInvariantMethod] +void ObjectInvariant() +{ + Contract.Invariant(wr!=null); + Contract.Invariant(ExprLineariser!=null); +} + + + public TPTPOpLineariser(TPTPExprLineariser ExprLineariser, TextWriter wr) { + Contract.Requires(ExprLineariser != null); + Contract.Requires(wr != null); + this.ExprLineariser = ExprLineariser; + this.wr = wr; + } + + /////////////////////////////////////////////////////////////////////////////////// + + private void WriteApplication(string op, IEnumerable<VCExpr/*!>!*/> args, + LineariserOptions options) { + Contract.Requires(op != null); + Contract.Requires(cce.NonNullElements(args )); + Contract.Requires(options != null); + WriteApplication(op, args, options, options.AsTerm); + } + + private void WriteTermApplication(string op, IEnumerable<VCExpr/*!>!*/> args, + LineariserOptions options) { + Contract.Requires(op != null); + Contract.Requires(cce.NonNullElements(args )); + Contract.Requires(options != null); + ExprLineariser.AssertAsTerm(op, options); + WriteApplication(op, args, options, options.AsTerm); + } + + + private void WriteApplication(string termOp, + IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options, + // change the AsTerm option for the arguments? + bool argsAsTerms) { + Contract.Requires(termOp != null); + Contract.Requires(cce.NonNullElements(args )); + Contract.Requires(options != null); + LineariserOptions newOptions = options.SetAsTerm(argsAsTerms); + Contract.Assert(newOptions!=null); + + var argCnt = 0; + if (termOp == "~") { + wr.Write("(~ "); + foreach (var e in args) { + ExprLineariser.Linearise(e, newOptions); + argCnt++; + } + Contract.Assert(argCnt == 1); + wr.Write(")"); + } else if ("&|~=><".IndexOf(termOp[0]) >= 0) { + wr.Write("("); + foreach (var e in args) { + ExprLineariser.Linearise(e, newOptions); + argCnt++; + if (argCnt == 1) { + wr.Write(" {0} ", termOp); + } + } + Contract.Assert(argCnt == 2); + wr.Write(")"); + } else { + wr.Write(termOp); + foreach (var e in args) { + Contract.Assert(e != null); + if (argCnt == 0) + wr.Write("("); + else + wr.Write(", "); + argCnt++; + ExprLineariser.Linearise(e, newOptions); + } + + if (argCnt > 0) + wr.Write(")"); + } + } + + // write an application that can only be a term. + // if the expression is supposed to be printed as a formula, + // it is turned into an equation (EQ (f args) |@true|) + private void WriteApplicationTermOnly(string termOp, + IEnumerable<VCExpr>/*!>!*/ args, LineariserOptions options) { + Contract.Requires(termOp != null); + Contract.Requires(cce.NonNullElements(args)); + Contract.Requires(options != null); + if (!options.AsTerm) + // Write: (EQ (f args) |@true|) + // where "args" are written as terms + wr.Write("(", eqName); + + WriteApplication(termOp, args, options, true); + + if (!options.AsTerm) + wr.Write(" = {0})", boolTrueName); + } + + /////////////////////////////////////////////////////////////////////////////////// + + public bool VisitNotOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + WriteApplication(notName, node, options); // arguments can be both terms and formulas + return true; + } + + private bool PrintEq(VCExprNAry node, LineariserOptions options) { + Contract.Requires(node != null); + Contract.Requires(options != null); + if (options.AsTerm) { + throw new NotImplementedException(); + } else { + if (node[0].Type.IsBool) { + Contract.Assert(node[1].Type.IsBool); + // use equivalence + WriteApplication(iffName, node, options); + } else { + // use equality and write the arguments as terms + WriteApplication(eqName, node, options, true); + } + } + + return true; + } + + public bool VisitEqOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + return PrintEq(node, options); + } + + public bool VisitNeqOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + wr.Write("(~ "); + PrintEq(node, options); + wr.Write(")"); + return true; + } + + public bool VisitAndOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + Contract.Assert(options.AsTerm); + WriteApplication(andName, node, options); + return true; + } + + public bool VisitOrOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + Contract.Assert(options.AsTerm); + WriteApplication(orName, node, options); + return true; + } + + public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteApplication(impliesName, node, options); + return true; + } + + public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + throw new NotImplementedException(); + } + + public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + VCExprCustomOp op = (VCExprCustomOp)node.Op; + WriteApplicationTermOnly(op.Name, node, options); + return true; + } + + public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + ExprLineariser.AssertAsFormula("distinct", options); + + if (node.Length < 2) { + ExprLineariser.Linearise(VCExpressionGenerator.True, options); + } else { + var bits = 0; + var cnt = node.Length; + while (cnt > 0) { + cnt >>= 1; + bits++; + } + + wr.Write("($true "); + foreach (VCExpr e in node) { + for (var i = 0; i < bits; ++i) { + var neg = (cnt & (1 << i)) != 0 ? "~" : ""; + wr.Write(" & {0}distinct__f__{1}(", neg, i); + ExprLineariser.LineariseAsTerm(e, options); + wr.Write(")"); + } + wr.WriteLine(); + cnt++; + } + wr.Write(")"); + } + + return true; + } + + public bool VisitLabelOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + //Contract.Requires(node.Length>=1); + // VCExprLabelOp! op = (VCExprLabelOp)node.Op; + // TODO + // wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label)); + ExprLineariser.Linearise(node[0], options); + // wr.Write(")"); + return true; + } + + public bool VisitSelectOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + var name = Lowercase(SimplifyLikeExprLineariser.SelectOpName(node)); + wr.Write(name + "("); + var cnt = 0; + foreach (VCExpr/*!*/ e in node) { + Contract.Assert(e != null); + if (cnt++ > 0) + wr.Write(", "); + ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool)); + } + wr.Write(")"); + return true; + } + + public bool VisitStoreOp(VCExprNAry node, LineariserOptions options) + { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + var name = Lowercase(SimplifyLikeExprLineariser.StoreOpName(node)); + wr.Write(name + "("); + var cnt = 0; + foreach (VCExpr e in node) { + Contract.Assert(e != null); + if (cnt++ > 0) + wr.Write(", "); + ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool)); + } + wr.Write(")"); + return true; + } + + public bool VisitBvOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + {Contract.Assert(false); throw new NotImplementedException();} // TODO + } + + public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + {Contract.Assert(false); throw new NotImplementedException();} // TODO + } + + public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + {Contract.Assert(false); throw new NotImplementedException();} // TODO + } + + public bool VisitAddOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteTermApplication(intAddName, node, options); + return true; + } + + public bool VisitSubOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteTermApplication(intSubName, node, options); + return true; + } + + public bool VisitMulOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteTermApplication(intMulName, node, options); + return true; + } + + public bool VisitDivOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteTermApplication(intDivName, node, options); + return true; + } + + public bool VisitModOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteTermApplication(intModName, node, options); + return true; + } + + public bool VisitLtOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteApplication(lessName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitLeOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteApplication(atmostName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitGtOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteApplication(greaterName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitGeOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteApplication(atleastName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitSubtypeOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteApplication(subtypeName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitSubtype3Op (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms + return true; + } + + public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options) { + //Contract.Requires(node != null); + //Contract.Requires(options != null); + + VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op; + Contract.Assert(op!=null); + string printedName = ExprLineariser.Namer.GetName(op.Func, Lowercase(op.Func.Name)); + Contract.Assert(printedName!=null); + + if (ExprLineariser.Options.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool) + WriteApplication(printedName, node, options, true); + else + // arguments are always terms + WriteApplicationTermOnly(printedName, node, options); + return true; + } + + } + } + +} |