From c57b12c920527690c1fd234e14ef7ca1c09e4185 Mon Sep 17 00:00:00 2001 From: qadeer Date: Fri, 24 Jun 2011 06:53:00 -0700 Subject: fixes to z3api --- Source/Provers/Z3api/ContextLayer.cs | 336 ++++++++++++---------------------- Source/Provers/Z3api/ProverLayer.cs | 9 +- Source/Provers/Z3api/TypeAdapter.cs | 34 ++-- Source/Provers/Z3api/VCExprVisitor.cs | 150 ++++++--------- Source/Provers/Z3api/Z3api.csproj | 8 + 5 files changed, 190 insertions(+), 347 deletions(-) (limited to 'Source/Provers/Z3api') diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index ed45c4fc..390d875d 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -11,6 +11,9 @@ using Microsoft.Z3; using Microsoft.Boogie.VCExprAST; using Microsoft.Basetypes; +using Z3Model = Microsoft.Z3.Model; +using BoogieModel = Microsoft.Boogie.Model; + namespace Microsoft.Boogie.Z3 { public class Z3Config @@ -20,21 +23,6 @@ namespace Microsoft.Boogie.Z3 private string logFilename; private List debugTraces = new List(); - public void SetModel(bool enabled) - { - config.SetParamValue("MODEL", (enabled ? "true" : "false")); - } - - public void SetSoftTimeout(string timeout) - { - config.SetParamValue("SOFT_TIMEOUT", timeout); - } - - public void SetTypeCheck(bool enabled) - { - config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false")); - } - public void SetCounterExample(int counterexample) { this.counterexamples = counterexample; @@ -69,102 +57,6 @@ namespace Microsoft.Boogie.Z3 } } - internal class PartitionMap - { - private Context ctx; - private Model model; - private Dictionary termToPartition = new Dictionary(); - private Dictionary valueToPartition = new Dictionary(); - private List partitionToValue = new List(); - private int partitionCounter = 0; - public int PartitionCounter { get { return partitionCounter; } } - - public PartitionMap(Context ctx, Model z3Model) - { - this.ctx = ctx; - this.model = z3Model; - } - - public int GetPartition(Term value) - { - int result; - if (!termToPartition.TryGetValue(value, out result)) - { - result = partitionCounter++; - termToPartition.Add(value, result); - partitionToValue.Add(null); - object constant = Evaluate(value); - valueToPartition.Add(constant, result); - partitionToValue[result] = constant; - } - return result; - } - - private object Evaluate(Term v) - { - Sort s = v.GetSort(); - Sort boolSort = ctx.MkBoolSort(); - Sort intSort = ctx.MkIntSort(); - ArrayValue av; - - if (s.Equals(boolSort)) - { - return ctx.GetBoolValue(v); - } - else if (s.Equals(intSort)) { - int i; - long il; - uint u; - ulong ul; - if (ctx.TryGetNumeralInt(v, out i)) { - return BigNum.FromInt(i); - } - else if (ctx.TryGetNumeralInt64(v, out il)) { - return BigNum.FromLong(il); - } - else if (ctx.TryGetNumeralUInt(v, out u)) { - return BigNum.FromUInt(u); - } - else if (ctx.TryGetNumeralUInt64(v, out ul)) { - return BigNum.FromULong(ul); - } - else { - string str = v.ToString(); - return GetPartition(v); - //return BigNum.FromString(ctx.GetNumeralString(v)); - } - } - else if (model.TryGetArrayValue(v, out av)) { - List> arrayValue = new List>(); - List tuple; - for (int i = 0; i < av.Domain.Length; i++) { - tuple = new List(); - tuple.Add(GetPartition(av.Domain[i])); - tuple.Add(GetPartition(av.Range[i])); - arrayValue.Add(tuple); - } - tuple = new List(); - tuple.Add(GetPartition(av.ElseCase)); - arrayValue.Add(tuple); - return arrayValue; - } - else { - // The term is uninterpreted; just return the partition id. - return GetPartition(v); - } - } - - public List PartitionToValue(Context ctx) - { - return partitionToValue; - } - - public Dictionary ValueToPartition(Context ctx) - { - return valueToPartition; - } - } - internal class BacktrackDictionary { private Dictionary dictionary = new Dictionary(); @@ -217,86 +109,11 @@ namespace Microsoft.Boogie.Z3 } } - internal class BoogieErrorModelBuilder - { - private Z3Context container; - private PartitionMap partitionMap; - - public BoogieErrorModelBuilder(Z3Context container, Model z3Model) - { - this.container = container; - this.partitionMap = new PartitionMap(((Z3Context)container).z3, z3Model); - } - - private Dictionary CreateConstantToPartition(Model z3Model) - { - Dictionary constantToPartition = new Dictionary(); - foreach (FuncDecl c in z3Model.GetModelConstants()) - { - string name = container.GetDeclName(c); - int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0])); - constantToPartition.Add(name, pid); - } - return constantToPartition; - } - - private List> CreatePartitionToConstant(Dictionary constantToPartition) - { - List> partitionToConstant = new List>(); - for (int i = 0; i < partitionMap.PartitionCounter; i++) - { - partitionToConstant.Add(new List()); - } - foreach (string s in constantToPartition.Keys) - { - partitionToConstant[constantToPartition[s]].Add(s); - } - return partitionToConstant; - } - - private Dictionary>> CreateFunctionToPartition(Model z3Model) - { - Dictionary>> functionToPartition = new Dictionary>>(); - - foreach (KeyValuePair kv in z3Model.GetFunctionGraphs()) - { - List> f_tuples = new List>(); - string f_name = container.GetDeclName(kv.Key); - FunctionGraph graph = kv.Value; - foreach (FunctionEntry entry in graph.Entries) - { - List tuple = new List(); - foreach (Term v in entry.Arguments) - { - tuple.Add(partitionMap.GetPartition(z3Model.Eval(v))); - } - tuple.Add(partitionMap.GetPartition(z3Model.Eval(entry.Result))); - f_tuples.Add(tuple); - } - List else_tuple = new List(); - else_tuple.Add(partitionMap.GetPartition(z3Model.Eval(graph.Else))); - f_tuples.Add(else_tuple); - functionToPartition.Add(f_name, f_tuples); - } - return functionToPartition; - } - - public Z3ErrorModel BuildBoogieModel(Model z3Model) - { - Dictionary constantToPartition = CreateConstantToPartition(z3Model); - Dictionary>> functionToPartition = CreateFunctionToPartition(z3Model); - List> partitionToConstant = CreatePartitionToConstant(constantToPartition); - List partitionToValue = partitionMap.PartitionToValue(((Z3Context)container).z3); - Dictionary valueToPartition = partitionMap.ValueToPartition(((Z3Context)container).z3); - return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition); - } - } - public class Z3ErrorModelAndLabels { - private Z3ErrorModel _errorModel; + private ErrorModel _errorModel; private List _relevantLabels; - public Z3ErrorModel ErrorModel + public ErrorModel ErrorModel { get { return this._errorModel; } } @@ -304,7 +121,7 @@ namespace Microsoft.Boogie.Z3 { get { return this._relevantLabels; } } - public Z3ErrorModelAndLabels(Z3ErrorModel errorModel, List relevantLabels) + public Z3ErrorModelAndLabels(ErrorModel errorModel, List relevantLabels) { this._errorModel = errorModel; this._relevantLabels = relevantLabels; @@ -461,12 +278,13 @@ namespace Microsoft.Boogie.Z3 return true; } - private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List relevantLabels) { + /* + private Z3ErrorModelAndLabels BuildZ3ErrorModel(Z3Model z3Model, List relevantLabels) { BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model); Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model); return new Z3ErrorModelAndLabels(boogieModel, new List(relevantLabels)); } - + */ private void DisplayRelevantLabels(List relevantLabels) { foreach (string labelName in relevantLabels) { System.Console.Write(labelName + ","); @@ -480,8 +298,9 @@ namespace Microsoft.Boogie.Z3 LBool outcome = LBool.Undef; Debug.Assert(0 < this.config.Counterexamples); while (true) { - Model z3Model; + Z3Model z3Model; outcome = z3.CheckAndGetModel(out z3Model); + log("(check-sat)"); if (outcome == LBool.False) break; @@ -505,13 +324,27 @@ namespace Microsoft.Boogie.Z3 } labelStrings.Add(labelName); } - boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); + + var sw = new StringWriter(); + sw.WriteLine("*** MODEL"); + z3Model.Display(sw); + sw.WriteLine("*** END_MODEL"); + var sr = new StringReader(sw.ToString()); + var models = Microsoft.Boogie.Model.ParseModels(sr); + + + Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List(labelStrings)); + + + boogieErrors.Add(e); if (boogieErrors.Count < this.config.Counterexamples) { z3.BlockLiterals(labels); log("block-literals {0}", labels); } + + labels.Dispose(); z3Model.Dispose(); if (boogieErrors.Count == this.config.Counterexamples) @@ -538,7 +371,7 @@ namespace Microsoft.Boogie.Z3 unsatCore = new List(); LBool outcome = LBool.Undef; - Model z3Model; + Z3Model z3Model; Term proof; Term[] core; Term[] assumption_terms = new Term[assumptions.Count]; @@ -568,7 +401,16 @@ namespace Microsoft.Boogie.Z3 } labelStrings.Add(labelName); } - boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings)); + + var sw = new StringWriter(); + sw.WriteLine("*** MODEL"); + z3Model.Display(sw); + sw.WriteLine("*** END_MODEL"); + var sr = new StringReader(sw.ToString()); + var models = Microsoft.Boogie.Model.ParseModels(sr); + + Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(new ErrorModel(models[0]), new List(labelStrings)); + boogieErrors.Add(e); labels.Dispose(); z3Model.Dispose(); @@ -668,37 +510,83 @@ namespace Microsoft.Boogie.Z3 return safeLiterals; } - public Term Make(string op, List children) { + public Term Make(VCExprOp op, List children) { Term[] unwrapChildren = children.ToArray(); - Term term; - switch (op) { - // formulas - case "AND": term = z3.MkAnd(unwrapChildren); break; - case "OR": term = z3.MkOr(unwrapChildren); break; - case "IMPLIES": term = z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); break; - case "NOT": term = z3.MkNot(unwrapChildren[0]); break; - case "IFF": term = z3.MkIff(unwrapChildren[0], unwrapChildren[1]); break; - // terms - case "EQ": term = z3.MkEq(unwrapChildren[0], unwrapChildren[1]); break; - case "NEQ": term = z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); break; - case "DISTINCT": term = z3.MkDistinct(unwrapChildren); break; - // terms - case "<": term = z3.MkLt(unwrapChildren[0], unwrapChildren[1]); break; - case ">": term = z3.MkGt(unwrapChildren[0], unwrapChildren[1]); break; - case "<=": term = z3.MkLe(unwrapChildren[0], unwrapChildren[1]); break; - case ">=": term = z3.MkGe(unwrapChildren[0], unwrapChildren[1]); break; - case "+": term = z3.MkAdd(unwrapChildren); break; - case "-": term = z3.MkSub(unwrapChildren); break; - case "/": term = z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); break; - case "%": term = z3.MkMod(unwrapChildren[0], unwrapChildren[1]); break; - case "*": term = z3.MkMul(unwrapChildren); break; - default: { - FuncDecl f = GetFunction(op); - term = z3.MkApp(f, unwrapChildren); - } - break; + VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp; + if (boogieFunctionOp != null) { + FuncDecl f = GetFunction(boogieFunctionOp.Func.Name); + return z3.MkApp(f, unwrapChildren); + } + VCExprDistinctOp distinctOp = op as VCExprDistinctOp; + if (distinctOp != null) { + return z3.MkDistinct(unwrapChildren); + } + + if (op == VCExpressionGenerator.AndOp) { + return z3.MkAnd(unwrapChildren); + } + + if (op == VCExpressionGenerator.OrOp) { + return z3.MkOr(unwrapChildren); + } + + if (op == VCExpressionGenerator.ImpliesOp) { + return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.NotOp) { + return z3.MkNot(unwrapChildren[0]); + } + + if (op == VCExpressionGenerator.EqOp) { + return z3.MkEq(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.NeqOp) { + return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); + } + + if (op == VCExpressionGenerator.LtOp) { + return z3.MkLt(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.LeOp) { + return z3.MkLe(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.GtOp) { + return z3.MkGt(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.GeOp) { + return z3.MkGe(unwrapChildren[0], unwrapChildren[1]); } - return term; + + if (op == VCExpressionGenerator.AddOp) { + return z3.MkAdd(unwrapChildren); + } + + if (op == VCExpressionGenerator.SubOp) { + return z3.MkSub(unwrapChildren); + } + + if (op == VCExpressionGenerator.DivOp) { + return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.MulOp) { + return z3.MkMul(unwrapChildren); + } + + if (op == VCExpressionGenerator.ModOp) { + return z3.MkMod(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.IfThenElseOp) { + return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]); + } + + throw new Exception("unhandled boogie operator"); } } } \ No newline at end of file diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index f691cffc..39acc5db 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -202,7 +202,10 @@ namespace Microsoft.Boogie.Z3 private static Z3Config BuildConfig(int timeout, bool nativeBv) { Z3Config config = new Z3Config(); - config.SetModel(true); + config.Config.SetParamValue("MODEL", "true"); + config.Config.SetParamValue("MODEL_V2", "true"); + config.Config.SetParamValue("MODEL_COMPLETION", "true"); + config.Config.SetParamValue("MBQI", "false"); if (0 <= CommandLineOptions.Clo.ProverCCLimit) { @@ -211,7 +214,7 @@ namespace Microsoft.Boogie.Z3 if (0 <= timeout) { - config.SetSoftTimeout(timeout.ToString()); + config.Config.SetParamValue("SOFT_TIMEOUT", timeout.ToString()); } if (CommandLineOptions.Clo.SimplifyLogFilePath != null) @@ -219,7 +222,7 @@ namespace Microsoft.Boogie.Z3 config.SetLogFilename(CommandLineOptions.Clo.SimplifyLogFilePath); } - config.SetTypeCheck(true); + config.Config.SetParamValue("TYPE_CHECK", "true"); return config; } diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index de5ebd8f..b0dd1eb4 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -87,21 +87,17 @@ namespace Microsoft.Boogie.Z3 this.container = context; } - private Sort GetMapType(MapType mapType) - { - Context z3 = ((Z3Context)container).z3; - if (!mapTypes.ContainsKey(mapType)) - { - Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1"); - Sort domain = GetType(mapType.Arguments[0]); - Sort range = GetType(mapType.Result); - Sort typeAst = BuildMapType(domain, range); - mapTypes.Add(mapType, typeAst); + private Sort GetMapType(MapType mapType) { + Context z3 = ((Z3Context)container).z3; + if (!mapTypes.ContainsKey(mapType)) { + Type result = mapType.Result; + for (int i = mapType.Arguments.Length-1; i > 0; i--) { + GetType(result); + result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result); } - Sort result; - bool containsKey = mapTypes.TryGetValue(mapType, out result); - Debug.Assert(containsKey); - return result; + mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result))); + } + return mapTypes[mapType]; } private Sort GetBvType(BvType bvType) @@ -158,15 +154,13 @@ namespace Microsoft.Boogie.Z3 public Sort BuildMapType(Sort domain, Sort range) { Context z3 = ((Z3Context)container).z3; - Sort typeAst = z3.MkArraySort(domain, range); - return typeAst; + return z3.MkArraySort(domain, range); } public Sort BuildBvType(BvType bvType) { Context z3 = ((Z3Context)container).z3; - Sort typeAst = z3.MkBvSort((uint)bvType.Bits); - return typeAst; + return z3.MkBvSort((uint)bvType.Bits); } public Sort BuildBasicType(BasicType basicType) @@ -188,11 +182,9 @@ namespace Microsoft.Boogie.Z3 public Sort BuildCtorType(CtorType ctorType) { Context z3 = ((Z3Context)container).z3; - Sort typeAst; if (ctorType.Arguments.Length > 0) throw new Exception("Type constructor of non-zero arity are not handled"); - typeAst = z3.MkSort(ctorType.Decl.Name); - return typeAst; + return z3.MkSort(ctorType.Decl.Name); } } } \ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index aa47d7e0..bf6dab94 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -17,15 +17,15 @@ namespace Microsoft.Boogie.Z3 { public class Z3apiExprLineariser : IVCExprVisitor { - private Z3apiOpLineariser OpLinObject = null; + private Z3apiOpLineariser opLineariser = null; private IVCExprOpVisitor OpLineariser { get { Contract.Ensures(Contract.Result>() != null); - if (OpLinObject == null) - OpLinObject = new Z3apiOpLineariser(this); - return OpLinObject; + if (opLineariser == null) + opLineariser = new Z3apiOpLineariser(this); + return opLineariser; } } @@ -91,7 +91,7 @@ namespace Microsoft.Boogie.Z3 } } - return cm.Make(opString, asts); + return cm.Make(op, asts); } return node.Accept(OpLineariser, options); @@ -246,7 +246,7 @@ namespace Microsoft.Boogie.Z3 /////////////////////////////////////////////////////////////////////////////////// - private Term WriteApplication(string op, IEnumerable terms, LineariserOptions options) + private Term WriteApplication(VCExprOp op, IEnumerable terms, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(op != null); @@ -267,76 +267,49 @@ namespace Microsoft.Boogie.Z3 { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("NOT", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitEqOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("EQ", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitNeqOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("NEQ", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitAndOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("AND", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitOrOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("OR", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - if (options.InverseImplies) - { - List args = new List(); - - args.Add(ExprLineariser.Linearise(node[1], options)); - List t = new List(); - t.Add(ExprLineariser.Linearise(node[0], options)); - args.Add(ExprLineariser.cm.Make("NOT", t)); - return ExprLineariser.cm.Make("OR", args); - } - else - { - return WriteApplication("IMPLIES", node, options); - } + return WriteApplication(node.Op, node, options); } - public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) + public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) { - Contract.Requires(options != null); - Contract.Requires(node != null); - - if (node.Length < 2) - { - return ExprLineariser.Linearise(VCExpressionGenerator.True, options); - } - else - { - List args = new List(); - foreach (VCExpr e in node) - { - Contract.Assert(e != null); - args.Add(ExprLineariser.Linearise(e, options)); - } - return ExprLineariser.cm.Make("DISTINCT", args); - } + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); } public Term VisitLabelOp(VCExprNAry node, LineariserOptions options) @@ -358,10 +331,24 @@ namespace Microsoft.Boogie.Z3 Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } + System.Diagnostics.Debug.Assert(args.Count >= 2); - Term[] unwrapChildren = args.ToArray(); - return ExprLineariser.cm.z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]); - // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args); + Term selectTerm = args[0]; + for (int i = 1; i < args.Count; i++) { + selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]); + } + return selectTerm; + } + + private Term ConstructStoreTerm(Term mapTerm, List args, int index) { + System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1); + if (index == args.Count - 2) { + return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]); + } + else { + Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1); + return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t); + } } public Term VisitStoreOp(VCExprNAry node, LineariserOptions options) @@ -374,10 +361,7 @@ namespace Microsoft.Boogie.Z3 Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } - - Term[] unwrapChildren = args.ToArray(); - return ExprLineariser.cm.z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]); - // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args); + return ConstructStoreTerm(args[0], args, 1); } public Term VisitBvOp(VCExprNAry node, LineariserOptions options) @@ -431,129 +415,97 @@ namespace Microsoft.Boogie.Z3 { Contract.Requires(options != null); Contract.Requires(node != null); - - List args = new List(); - args.Add(ExprLineariser.Linearise(node[0], options)); - args.Add(ExprLineariser.Linearise(node[1], options)); - args.Add(ExprLineariser.Linearise(node[2], options)); - return ExprLineariser.cm.Make("ITE", args); + return WriteApplication(node.Op, node, options); } public Term VisitCustomOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(node != null); Contract.Requires(options != null); - VCExprCustomOp op = (VCExprCustomOp)node.Op; - List args = new List(); - foreach (VCExpr arg in node) - { - args.Add(ExprLineariser.Linearise(arg, options)); - } - return ExprLineariser.cm.Make(op.Name, args); + return WriteApplication(node.Op, node, options); } - public Term VisitAddOp(VCExprNAry node, LineariserOptions options) - { - Contract.Requires(options != null); - Contract.Requires(node != null); - if (CommandLineOptions.Clo.ReflectAdd) - { - return WriteApplication("Reflect$Add", node, options); - } - else - { - return WriteApplication("+", node, options); - } + public Term VisitAddOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); } public Term VisitSubOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("-", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitMulOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("*", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitDivOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("/", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitModOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("%", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitLtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitLeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<=", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitGtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication(">", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitGeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication(">=", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<:", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<::", node, options); + return WriteApplication(node.Op, node, options); } public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op; - Contract.Assert(op != null); - string funcName = op.Func.Name; - Contract.Assert(funcName != null); - string bvzName = op.Func.FindStringAttribute("external"); - if (bvzName != null) funcName = bvzName; - - List args = new List(); - foreach (VCExpr e in node) - { - Contract.Assert(e != null); - args.Add(ExprLineariser.Linearise(e, options)); - } - return ExprLineariser.cm.Make(funcName, args); + return WriteApplication(node.Op, node, options); } } } diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index e02243ce..94184957 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -146,6 +146,14 @@ {B230A69C-C466-4065-B9C1-84D80E76D802} Core + + {ACEF88D5-DADD-46DA-BAE1-2144D63F4C83} + Model + + + {FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5} + ParserHelper + {56FFDBCA-7D14-43B8-A6CA-22A20E417EE1} VCExpr -- cgit v1.2.3