diff options
| author |  tabarbe <unknown> | 2010-08-13 00:43:11 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-13 00:43:11 +0000 |
| commit | 85ffcd8f1392bf871e585fe8efb60e38bfdb2f72 (patch) | |
| tree | e697a9f2d08a51d866aaa19a53b016b2749c090b /Source/VCExpr/SimplifyLikeLineariser.cs | |
| parent | eb284abb4172c6162ac31b865dc2a7e9661fe413 (diff) | |
Boogie: Renaming VCExpr sources in preparation for port commit
Diffstat (limited to 'Source/VCExpr/SimplifyLikeLineariser.cs')
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.cs | 844 |
1 files changed, 844 insertions, 0 deletions
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs new file mode 100644 index 00000000..30779f22 --- /dev/null +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -0,0 +1,844 @@ +//-----------------------------------------------------------------------------
+//
+// 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;
+
+// a naive method to turn VCExprs into strings that can be fed into Simplify
+
+namespace Microsoft.Boogie.VCExprAST
+{
+
+ // Options for the linearisation. Here one can choose, for instance,
+ // whether Simplify or Z3 output is to be produced
+ public abstract class LineariserOptions {
+
+ public readonly bool AsTerm;
+ public abstract LineariserOptions! SetAsTerm(bool newVal);
+
+ public abstract bool QuantifierIds { get; }
+
+ public virtual bool UseWeights { get { return false; } }
+
+ public virtual bool InverseImplies { get { return false; } }
+
+ // whether to include type specifications in quantifiers
+ public abstract bool UseTypes { get; }
+
+ public virtual CommandLineOptions.BvHandling Bitvectors { get {
+ return CommandLineOptions.BvHandling.None;
+ } }
+
+ // variables representing formulas in let-bindings have to be
+ // printed in a different way than other variables
+ public virtual List<VCExprVar!>! LetVariables { get {
+ return EmptyList;
+ } }
+
+ public virtual LineariserOptions! AddLetVariable(VCExprVar! furtherVar) {
+ return this;
+ }
+
+ public virtual LineariserOptions! AddLetVariables(List<VCExprVar!>! furtherVars) {
+ return this;
+ }
+
+ private static readonly List<VCExprVar!>! EmptyList = new List<VCExprVar!>();
+
+ public bool NativeBv { get {
+ return Bitvectors == CommandLineOptions.BvHandling.Z3Native;
+ } }
+
+ public bool IntBv { get {
+ return Bitvectors == CommandLineOptions.BvHandling.ToInt;
+ } }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ protected LineariserOptions(bool asTerm) {
+ this.AsTerm = asTerm;
+ }
+
+ public static readonly LineariserOptions! SimplifyDefault = new SimplifyOptions (false);
+ internal static readonly LineariserOptions! SimplifyDefaultTerm = new SimplifyOptions (true);
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ private class SimplifyOptions : LineariserOptions {
+ internal SimplifyOptions(bool asTerm) {
+ base(asTerm);
+ }
+ public override bool QuantifierIds { get {
+ return false;
+ } }
+ public override bool UseTypes { get {
+ return false;
+ } }
+ public override LineariserOptions! SetAsTerm(bool newVal) {
+ if (newVal)
+ return SimplifyDefaultTerm;
+ else
+ return SimplifyDefault;
+ }
+ }
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for expressions. The result (bool) is currently not used for anything
+ public class SimplifyLikeExprLineariser : IVCExprVisitor<bool, LineariserOptions!> {
+
+ public static string! ToSimplifyString(VCExpr! e, UniqueNamer! namer) {
+ return ToString(e, LineariserOptions.SimplifyDefault, namer);
+ }
+
+ public static string! ToString(VCExpr! e, LineariserOptions! options,
+ UniqueNamer! namer) {
+ StringWriter sw = new StringWriter();
+ SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer);
+ lin.Linearise(e, options);
+ return sw.ToString();
+ }
+
+ ////////////////////////////////////////////////////////////////////////////////////////
+
+ private readonly TextWriter! wr;
+ private SimplifyLikeOpLineariser OpLinObject = null;
+ private IVCExprOpVisitor<bool, LineariserOptions!>! OpLineariser { get {
+ if (OpLinObject == null)
+ OpLinObject = new SimplifyLikeOpLineariser (this, wr);
+ return OpLinObject;
+ } }
+
+ internal readonly UniqueNamer! Namer;
+
+ public SimplifyLikeExprLineariser(TextWriter! wr, UniqueNamer! namer) {
+ this.wr = wr;
+ this.Namer = namer;
+ }
+
+ public void Linearise(VCExpr! expr, LineariserOptions! options) {
+ expr.Accept<bool, LineariserOptions!>(this, options);
+ }
+
+ public void LineariseAsTerm(VCExpr! expr, LineariserOptions! options) {
+ Linearise(expr, options.SetAsTerm(true));
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ 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 neqName:
+ case distinctName:
+ case TRUEName:
+ case FALSEName:
+ s = "nonkeyword_" + s;
+ break;
+ }
+
+ if (CommandLineOptions.Clo.BracketIdsInVC == 0) {
+ // In this form, we go with any identifier, so we don't ever bother about brackets.
+ // Except: @true and @false are always written with brackets
+ return s;
+ }
+ bool looksLikeOperator = true;
+ bool looksLikeSimpleId = true;
+ bool useBrackets = false;
+ foreach (char ch in s) {
+ switch (ch) {
+ case '=':
+ case '<':
+ case '>':
+ case '+':
+ case '-':
+ case '*':
+ case '/':
+ case '%':
+ case ':':
+ // looks like operator, not simple id
+ looksLikeSimpleId = false;
+ break;
+ default:
+ if (Char.IsLetterOrDigit(ch)) {
+ // looks like simple id, not operator
+ looksLikeOperator = false;
+ } else {
+ // looks like neither operator nor simple id
+ looksLikeOperator = false;
+ looksLikeSimpleId = false;
+ }
+ break;
+ }
+ if (!looksLikeOperator && !looksLikeSimpleId) {
+ useBrackets = true;
+ break;
+ }
+ }
+ if (useBrackets) {
+ return "|" + s + "|";
+ } else {
+ return s;
+ }
+ }
+
+ private static string! TypeToStringHelper(Type! t) {
+ System.IO.StringWriter buffer = new System.IO.StringWriter();
+ using (TokenTextWriter stream = new TokenTextWriter("<buffer>", buffer, false)) {
+ t.Emit(stream);
+ }
+ return buffer.ToString();
+ }
+ public static string! TypeToString(Type! t) {
+ if (t.IsBool)
+ return "$bool";
+ else if (t.IsInt)
+ return "$int";
+ else if (t.IsBv)
+ return "$bv" + t.BvBits;
+ else if (t.IsMap)
+ return TypeToStringHelper(t);
+ else {
+ // at this point, only the types U, T, and bitvector types should be left
+ if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic)
+ return "U";
+ else
+ return TypeToStringHelper(t);
+ }
+ }
+
+ public static string! BvConcatOpName(VCExprNAry! node)
+ requires node.Op is VCExprBvConcatOp; {
+ int bits1 = node[0].Type.BvBits;
+ int bits2 = node[1].Type.BvBits;
+ return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]";
+ }
+
+ public static string! BvExtractOpName(VCExprNAry! node)
+ requires node.Op is VCExprBvExtractOp; {
+ VCExprBvExtractOp! op = (VCExprBvExtractOp)node.Op;
+ return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]";
+ }
+
+ public static string! StoreOpName(VCExprNAry! node)
+ requires node.Op is VCExprStoreOp; {
+ return "Store_" + TypeToString(node[0].Type);
+ }
+
+ public static string! SelectOpName(VCExprNAry! node)
+ requires node.Op is VCExprSelectOp; {
+ return "Select_" + TypeToString(node[0].Type);
+ }
+
+ internal void WriteId(string! s) {
+ wr.Write(MakeIdPrintable(s));
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ /// <summary>
+ /// The name for logical conjunction in Simplify
+ /// </summary>
+ 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! iffName = "IFF"; // logical equivalence
+ internal const string! eqName = "EQ"; // equality
+ internal const string! neqName = "NEQ"; // inequality
+ 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 = "<:";
+ internal const string! subtypeArgsName = "<::";
+
+ internal const string! distinctName = "DISTINCT";
+ /// <summary>
+ /// name of the main inclusion relation
+ /// </summary>
+ internal const string! boolTrueName = "|@true|";
+ internal const string! boolFalseName = "|@false|";
+ internal const string! boolAndName = "boolAnd";
+ internal const string! boolOrName = "boolOr";
+ internal const string! boolNotName = "boolNot";
+ internal const string! termEqName = "anyEqual";
+ internal const string! termNeqName = "anyNeq";
+ 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! intAddNameReflect = "Reflect$Add";
+ internal const string! intSubName = "-";
+ internal const string! intMulName = "*";
+ internal const string! intDivName = "/";
+ internal const string! intModName = "%";
+
+ 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(options.UseTypes ? TRUEName : boolTrueName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write(options.UseTypes ? FALSEName : boolFalseName);
+ else if (node is VCExprIntLit) {
+ wr.Write(((VCExprIntLit)node).Val);
+ } else
+ assert false;
+
+ } else {
+
+ if (node == VCExpressionGenerator.True)
+ wr.Write(TRUEName);
+ else if (node == VCExpressionGenerator.False)
+ wr.Write(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<bool, LineariserOptions!>(OpLineariser, options);
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprVar! node, LineariserOptions! options) {
+ string! printedName = Namer.GetName(node, node.Name);
+
+ if (options.AsTerm ||
+ // variables for formulas bound in a let-binding are never
+ // written as an equation
+ options.LetVariables.Contains(node) ||
+ // if variables are properly typed, they cannot be written as
+ // equation either
+ options.UseTypes) {
+ WriteId(printedName);
+ } else {
+ wr.Write("({0} ", eqName);
+ WriteId(printedName);
+ wr.Write(" {0})", 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];
+ string! printedName = Namer.GetLocalName(var, var.Name);
+ if (i != 0)
+ wr.Write(" ");
+ WriteId(printedName);
+ if (options.UseTypes)
+ wr.Write(" :TYPE {0}", TypeToString(var.Type));
+ }
+ wr.Write(") ");
+
+ WriteTriggers(node.Triggers, options);
+
+ 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(") ");
+ }
+ }
+
+ if (options.UseWeights) {
+ int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);
+ if (weight != 1) {
+ wr.Write("(WEIGHT ");
+ wr.Write(weight);
+ wr.Write(") ");
+ }
+ }
+
+ Linearise(node.Body, options);
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ private void WriteTriggers(List<VCTrigger!>! 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) {
+ wr.Write("(PATS");
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (vcTrig.Pos) {
+ if (vcTrig.Exprs.Count > 1) {
+ wr.Write(" (MPAT");
+ }
+ foreach (VCExpr! e in vcTrig.Exprs) {
+ wr.Write(" ");
+ LineariseAsTerm(e, options);
+ }
+ if (vcTrig.Exprs.Count > 1) {
+ wr.Write(")");
+ }
+ }
+ }
+ 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
+ wr.Write("(NOPATS");
+ foreach (VCTrigger! vcTrig in triggers) {
+ if (!vcTrig.Pos) {
+ wr.Write(" ");
+ assert vcTrig.Exprs.Count == 1;
+ LineariseAsTerm(vcTrig.Exprs[0], options);
+ }
+ }
+ wr.Write(") ");
+ }
+
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ public bool Visit(VCExprLet! node, LineariserOptions! options) {
+ Namer.PushScope(); try {
+
+ wr.Write("(LET (");
+
+ LineariserOptions! optionsWithVars = options.AddLetVariables(node.BoundVars);
+
+ string s = "(";
+ foreach (VCExprLetBinding! b in node) {
+ wr.Write(s);
+ string! printedName = Namer.GetLocalName(b.V, b.V.Name);
+
+ bool formula = b.V.Type.IsBool;
+ if (formula)
+ wr.Write("FORMULA ");
+ else
+ wr.Write("TERM ");
+ WriteId(printedName);
+ wr.Write(" ");
+ Linearise(b.E, optionsWithVars.SetAsTerm(!formula));
+ wr.Write(")");
+ s = " (";
+ }
+ wr.Write(") ");
+ Linearise(node.Body, optionsWithVars);
+ wr.Write(")");
+
+ return true;
+
+ } finally {
+ Namer.PopScope();
+ }
+ }
+
+ /////////////////////////////////////////////////////////////////////////////////////
+
+ // Lineariser for operator terms. The result (bool) is currently not used for anything
+ internal class SimplifyLikeOpLineariser : IVCExprOpVisitor<bool, LineariserOptions!> {
+ private readonly SimplifyLikeExprLineariser! ExprLineariser;
+ private readonly TextWriter! wr;
+
+ public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser! ExprLineariser, TextWriter! wr) {
+ this.ExprLineariser = ExprLineariser;
+ this.wr = wr;
+ }
+
+ ///////////////////////////////////////////////////////////////////////////////////
+
+ private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options,
+ bool argsAsTerms) {
+ WriteApplication(op, op, args, options, argsAsTerms);
+ }
+
+ private void WriteApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options) {
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteTermApplication(string! op, IEnumerable<VCExpr!>! args,
+ LineariserOptions! options) {
+ ExprLineariser.AssertAsTerm(op, options);
+ WriteApplication(op, op, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string! termOp, string! predOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options) {
+ WriteApplication(termOp, predOp, args, options, options.AsTerm);
+ }
+
+ private void WriteApplication(string! termOp, string! predOp,
+ IEnumerable<VCExpr!>! args, LineariserOptions! options,
+ // change the AsTerm option for the arguments?
+ bool argsAsTerms) {
+ wr.Write("({0}", options.AsTerm ? termOp : predOp);
+
+ LineariserOptions! newOptions = options.SetAsTerm(argsAsTerms);
+ foreach (VCExpr! e in args) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, newOptions);
+ }
+
+ 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) {
+ 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;
+ }
+
+ public bool VisitEqOp (VCExprNAry! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+ // use equality on terms, also if the arguments have type bool
+ WriteApplication(termEqName, node, options);
+ } else {
+ if (node[0].Type.IsBool) {
+ assert node[1].Type.IsBool;
+ // use equivalence
+ WriteApplication(iffName, node, options);
+ } else {
+ assert !node[1].Type.IsBool;
+ // use equality and write the arguments as terms
+ WriteApplication(eqName, node, options, true);
+ }
+ }
+
+ return true;
+ }
+
+ public bool VisitNeqOp (VCExprNAry! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+ // use equality on terms, also if the arguments have type bool
+ WriteApplication(termNeqName, node, options);
+ } else {
+ if (node[0].Type.IsBool) {
+ assert node[1].Type.IsBool;
+ // use equivalence and negate the whole thing
+ wr.Write("({0} ", notName);
+ WriteApplication(iffName, node, options);
+ wr.Write(")");
+ } else {
+ // use equality and write the arguments as terms
+ WriteApplication(neqName, node, options, true);
+ }
+ }
+
+ return true;
+ }
+
+ public bool VisitAndOp (VCExprNAry! node, LineariserOptions! options) {
+ assert options.AsTerm;
+ WriteApplication(boolAndName, andName, node, options); // arguments can be both terms and formulas
+ return true;
+ }
+
+ public bool VisitOrOp (VCExprNAry! node, LineariserOptions! options) {
+ assert options.AsTerm;
+ WriteApplication(boolOrName, orName, node, options); // arguments can be both terms and formulas
+ return true;
+ }
+
+ public bool VisitImpliesOp (VCExprNAry! node, LineariserOptions! options) {
+ if (options.AsTerm) {
+ wr.Write("({0} ({1} ", boolOrName, boolNotName);
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write(") ");
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(")");
+ } else if (options.InverseImplies) {
+ wr.Write("({0} ", orName);
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(" ({0} ", notName);
+ ExprLineariser.Linearise(node[0], options);
+ wr.Write("))");
+ } else {
+ WriteApplication(impliesName, 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;
+ 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) {
+ wr.Write("(" + SelectOpName(node));
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitStoreOp (VCExprNAry! node, LineariserOptions! options) {
+ wr.Write("(" + StoreOpName(node));
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitBvOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);
+ return true;
+ }
+
+ public bool VisitBvExtractOp(VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(BvExtractOpName(node), node, options);
+ return true;
+ }
+
+ public bool VisitBvConcatOp (VCExprNAry! node, LineariserOptions! options) {
+ WriteTermApplication(BvConcatOpName(node), node, options);
+ return true;
+ }
+
+ public bool VisitIfThenElseOp (VCExprNAry! node, LineariserOptions! options) {
+
+ wr.Write("(ITE ");
+ ExprLineariser.Linearise(node[0], options.SetAsTerm(false));
+ wr.Write(" ");
+ ExprLineariser.Linearise(node[1], options);
+ wr.Write(" ");
+ ExprLineariser.Linearise(node[2], options);
+ wr.Write(")");
+
+ return true;
+ }
+
+ public bool VisitCustomOp (VCExprNAry! node, LineariserOptions! options) {
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+ wr.Write("({0}", op.Name);
+ foreach (VCExpr arg in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(arg, options);
+ }
+ wr.Write(")");
+ return true;
+ }
+
+ public bool VisitAddOp (VCExprNAry! node, LineariserOptions! options) {
+ if (CommandLineOptions.Clo.ReflectAdd) {
+ WriteTermApplication(intAddNameReflect, node, options);
+ } else {
+ 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! funcName = op.Func.Name;
+ string? bvzName = op.Func.FindStringAttribute("external");
+ string! printedName = ExprLineariser.Namer.GetName(op.Func, funcName);
+ if (bvzName != null) printedName = bvzName;
+
+ if (options.UseTypes) {
+ // we use term notation for arguments whose type is not bool, and
+ // formula notation for boolean arguments
+
+ wr.Write("(");
+ ExprLineariser.WriteId(printedName);
+
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
+
+ wr.Write(")");
+ } else {
+ // arguments are always terms
+ WriteApplicationTermOnly(SimplifyLikeExprLineariser.MakeIdPrintable(printedName),
+ node, options);
+ }
+ return true;
+ }
+
+ }
+ }
+
+}
|