From 726e88e1ece4047db1cedbbd886b8ef701bc4bbd Mon Sep 17 00:00:00 2001 From: qadeer Date: Tue, 24 Aug 2010 22:35:20 +0000 Subject: fixed z3api so that it works on small examples now. --- Source/Provers/Z3api/ContextLayer.cs | 11 +-- Source/Provers/Z3api/ProverLayer.cs | 12 +++ Source/Provers/Z3api/SafeContext.cs | 107 ++++++++++---------------- Source/Provers/Z3api/StubContext.cs | 15 ++-- Source/Provers/Z3api/TypeAdapter.cs | 92 ++++++++++++++++++++--- Source/Provers/Z3api/VCExprVisitor.cs | 136 ++++++++++++---------------------- Source/VCGeneration/VC.cs | 20 +++-- 7 files changed, 207 insertions(+), 186 deletions(-) diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index e3ba1fa7..64533c02 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -15,10 +15,6 @@ namespace Microsoft.Boogie.Z3 { public class Z3Config { - ~Z3Config() - { - config.Dispose(); - } private Config config = new Config(); private int counterexamples; private string logFilename; @@ -92,15 +88,14 @@ namespace Microsoft.Boogie.Z3 void AddSmtlibString(string smtlibString); string GetDeclName(Z3ConstDeclAst constDeclAst); Z3PatternAst MakePattern(List exprs); - Z3TermAst MakeForall(List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body); - Z3TermAst MakeExists(List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body); + Z3TermAst MakeForall(uint weight, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body); + Z3TermAst MakeExists(uint weight, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body); List BuildConflictClause(Z3LabeledLiterals relevantLabels); ProverInterface.Outcome Check(out List boogieErrors); void TypeCheckBool(Z3TermAst t); void TypeCheckInt(Z3TermAst t); void DeclareType(string typeName); void DeclareConstant(string constantName, Type boogieType); - Z3TermAst MakeBoundVariable(uint deBruijnIndex, Type boogieType); void DeclareFunction(string functionName, List domain, Type range); Z3TermAst GetConstant(string constantName, Type constantType); Z3TermAst MakeIntLiteral(string numeral); @@ -109,6 +104,8 @@ namespace Microsoft.Boogie.Z3 Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child); Z3LabeledLiterals GetRelevantLabels(); Z3TermAst Make(string op, List children); + Z3TermAst MakeArraySelect(List args); + Z3TermAst MakeArrayStore(List args); } internal class PartitionMap diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index f3dfab69..7c41f25c 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -30,6 +30,12 @@ namespace Microsoft.Boogie.Z3 this.z3ContextIsUsed = false; } + public override void Close() + { + base.Close(); + ((Z3apiProverContext)Context).cm.z3.Dispose(); + ((Z3apiProverContext)Context).cm.config.Config.Dispose(); + } private bool z3ContextIsUsed; public void PushAxiom(VCExpr axiom) @@ -39,6 +45,7 @@ namespace Microsoft.Boogie.Z3 LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); cm.AddAxiom((VCExpr)axiom, linOptions); } + private void PushConjecture(VCExpr conjecture) { Z3SafeContext cm = ((Z3apiProverContext)ctx).cm; @@ -60,6 +67,11 @@ namespace Microsoft.Boogie.Z3 outcome = cm.Check(out z3LabelModels); } + public override void PushVCExpression(VCExpr vc) + { + PushAxiom(vc); + } + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) { LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List()); diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index 70b7f35c..9ce303f4 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -67,7 +67,6 @@ namespace Microsoft.Boogie.Z3 public class Z3SafeLabeledLiterals : Z3LabeledLiterals { - private LabeledLiterals labeledLiterals; public Z3SafeLabeledLiterals(LabeledLiterals labeledLiterals) { @@ -86,12 +85,10 @@ namespace Microsoft.Boogie.Z3 internal BacktrackDictionary functions = new BacktrackDictionary(); internal BacktrackDictionary labels = new BacktrackDictionary(); - ~Z3SafeContext() - { - z3.Dispose(); - } public Context z3; - private Z3Config config; + public Z3Config config; + private VCExpressionGenerator gen; + private Z3TypeCachedBuilder tm; public void CreateBacktrackPoint() { @@ -233,47 +230,60 @@ namespace Microsoft.Boogie.Z3 return z3Types; } - private const int DEFAULT_QUANTIFIER_WEIGHT = 0; - - public Z3TermAst MakeForall(List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) + public Z3TermAst MakeForall(uint weight, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) { - List unwrapPatterns = Unwrap(patterns); - List unwrapNoPatterns = Unwrap(no_patterns); - List z3Types = GetTypes(boogieTypes); - List symbols = GetSymbols(varNames); + // List unwrapNoPatterns = Unwrap(no_patterns); + // List z3Types = GetTypes(boogieTypes); + // List symbols = GetSymbols(varNames); Term unwrapBody = Unwrap(body); + List bound = new List(); + for (int i = 0; i < varNames.Count; i++) + { + Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]); + bound.Add(Unwrap(t)); + } + Term termAst = z3.MkForall(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody); + /* Term termAst = z3.MkQuantifier(true, - DEFAULT_QUANTIFIER_WEIGHT, + weight, unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), z3Types.ToArray(), symbols.ToArray(), unwrapBody); - + */ return Wrap(termAst); } - public Z3TermAst MakeExists(List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) + public Z3TermAst MakeExists(uint weight, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) { List unwrapPatterns = Unwrap(patterns); - List unwrapNoPatterns = Unwrap(no_patterns); - List z3Types = GetTypes(boogieTypes); - List symbols = GetSymbols(varNames); + // List unwrapNoPatterns = Unwrap(no_patterns); + // List z3Types = GetTypes(boogieTypes); + // List symbols = GetSymbols(varNames); Term unwrapBody = Unwrap(body); + List bound = new List(); + for (int i = 0; i < varNames.Count; i++) + { + Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]); + bound.Add(Unwrap(t)); + } + Term termAst = z3.MkExists(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody); + /* Term termAst = z3.MkQuantifier(false, - DEFAULT_QUANTIFIER_WEIGHT, + weight, unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), z3Types.ToArray(), symbols.ToArray(), unwrapBody); + */ return Wrap(termAst); } - private static bool Equals(List l, List r) { Debug.Assert(l != null); @@ -380,8 +390,6 @@ namespace Microsoft.Boogie.Z3 throw new Exception("Failed Int Typecheck"); } - private VCExpressionGenerator gen; - public Z3SafeContext(Z3Config config, VCExpressionGenerator gen) { Context z3 = new Context(config.Config); @@ -392,7 +400,7 @@ namespace Microsoft.Boogie.Z3 z3.EnableDebugTrace(tag); this.z3 = z3; this.config = config; - this.tm = new Z3TypeCachedBuilder(new Z3SafeTypeBuilder(z3)); + this.tm = new Z3TypeCachedBuilder(this); this.gen = gen; } @@ -410,18 +418,6 @@ namespace Microsoft.Boogie.Z3 constants.Add(constantName, Wrap(constAst)); } - public Z3TermAst MakeBoundVariable(uint deBruijnIndex, Type boogieType) - { - Z3Type typeAst = tm.GetType(boogieType); - Sort unwrapTypeAst = Unwrap(typeAst); - - Term boundVariable = z3.MkBound(deBruijnIndex, unwrapTypeAst); - Z3TermAst wrappedBoundVariable = Wrap(boundVariable); - return wrappedBoundVariable; - } - - private Z3TypeCachedBuilder tm; - public void DeclareFunction(string functionName, List domain, Type range) { Symbol symbolAst = GetSymbol(functionName); @@ -504,6 +500,7 @@ namespace Microsoft.Boogie.Z3 labels.Add(labelName, wrapLabeledExpr); return wrapLabeledExpr; } + public Z3LabeledLiterals GetRelevantLabels() { Z3SafeLabeledLiterals safeLiterals = new Z3SafeLabeledLiterals(z3.GetRelevantLabels()); @@ -555,43 +552,17 @@ namespace Microsoft.Boogie.Z3 FuncDecl unwrapFunction = Unwrap(function); return unwrapFunction; } - } - - public class Z3SafeTypeBuilder : Z3TypeBuilder - { - protected Context z3; - - public Z3SafeTypeBuilder(Context z3) - { - this.z3 = z3; - } - private Z3Type WrapType(Sort typeAst) + public Z3TermAst MakeArraySelect(List args) { - return new Z3SafeType(typeAst); + Term[] unwrapChildren = Unwrap(args).ToArray(); + return Wrap(z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1])); } - public Z3Type BuildBvType(BvType bvType) + public Z3TermAst MakeArrayStore(List args) { - Sort typeAst = z3.MkBvSort((uint)bvType.Bits); - return WrapType(typeAst); - } - - public Z3Type BuildBasicType(BasicType basicType) - { - Sort typeAst; - if (basicType.IsBool) - { - typeAst = z3.MkBoolSort(); - } - else if (basicType.IsInt) - { - typeAst = z3.MkIntSort(); - } - else - throw new Exception("Unknown Basic Type " + basicType.ToString()); - return WrapType(typeAst); + Term[] unwrapChildren = Unwrap(args).ToArray(); + return Wrap(z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2])); } - } } \ No newline at end of file diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs index e4dd9318..0284d219 100644 --- a/Source/Provers/Z3api/StubContext.cs +++ b/Source/Provers/Z3api/StubContext.cs @@ -28,10 +28,10 @@ namespace Microsoft.Boogie.Z3 { public Z3PatternAst MakePattern(List exprs) { return new Z3StubPatternAst(); } - public Z3TermAst MakeForall(List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) { + public Z3TermAst MakeForall(uint weight, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) { return new Z3StubTermAst(); } - public Z3TermAst MakeExists(List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) { + public Z3TermAst MakeExists(uint weight, List varNames, List boogieTypes, List patterns, List no_patterns, Z3TermAst body) { return new Z3StubTermAst(); } public List BuildConflictClause(Z3LabeledLiterals relevantLabels) { @@ -45,9 +45,6 @@ namespace Microsoft.Boogie.Z3 { public void TypeCheckInt(Z3TermAst t){} public void DeclareType(string typeName) {} public void DeclareConstant(string constantName, Type boogieType) {} - public Z3TermAst MakeBoundVariable(uint deBruijnIndex,Type boogieType) { - return new Z3StubTermAst(); - } public void DeclareFunction(string functionName, List domain, Type range) {} public Z3TermAst GetConstant(string constantName, Type constantType) { return new Z3StubTermAst(); @@ -70,5 +67,13 @@ namespace Microsoft.Boogie.Z3 { public Z3TermAst Make(string op, List children) { return new Z3StubTermAst(); } + public Z3TermAst MakeArraySelect(List args) + { + return new Z3StubTermAst(); + } + public Z3TermAst MakeArrayStore(List args) + { + return new Z3StubTermAst(); + } } } \ No newline at end of file diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index 280e93e9..0d79bd5a 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -15,6 +15,26 @@ namespace Microsoft.Boogie.Z3 { internal class Z3TypeCachedBuilder { + private class MapTypeComparator : IEqualityComparer + { + public bool Equals(MapType x, MapType y) + { + if (x.MapArity != y.MapArity) + return false; + for (int i = 0; i < x.MapArity; i++) + { + if (!Equals(x.Arguments[i], y.Arguments[i])) + return false; + } + return Equals(x.Result, y.Result); + + } + public int GetHashCode(MapType mapType) + { + return mapType.GetHashCode(); + } + } + private class BvTypeComparator : IEqualityComparer { public bool Equals(BvType x, BvType y) @@ -46,20 +66,38 @@ namespace Microsoft.Boogie.Z3 } } - private Z3TypeBuilder builder; + private Dictionary mapTypes = new Dictionary(new MapTypeComparator()); private Dictionary bvTypes = new Dictionary(new BvTypeComparator()); private Dictionary basicTypes = new Dictionary(new BasicTypeComparator()); + private Z3Context container; + + public Z3TypeCachedBuilder(Z3Context context) + { + this.container = context; + } - public Z3TypeCachedBuilder(Z3TypeBuilder builder) + private Z3Type GetMapType(MapType mapType) { - this.builder = builder; + Context z3 = ((Z3SafeContext)container).z3; + if (!mapTypes.ContainsKey(mapType)) + { + Debug.Assert(mapType.Arguments.Length == 1, "Z3api only supports maps of arity 1"); + Z3Type domain = GetType(mapType.Arguments[0]); + Z3Type range = GetType(mapType.Result); + Z3Type typeAst = BuildMapType(domain, range); + mapTypes.Add(mapType, typeAst); + } + Z3Type result; + bool containsKey = mapTypes.TryGetValue(mapType, out result); + Debug.Assert(containsKey); + return result; } private Z3Type GetBvType(BvType bvType) { if (!bvTypes.ContainsKey(bvType)) { - Z3Type typeAst = builder.BuildBvType(bvType); + Z3Type typeAst = BuildBvType(bvType); bvTypes.Add(bvType, typeAst); } Z3Type result; @@ -72,7 +110,7 @@ namespace Microsoft.Boogie.Z3 { if (!basicTypes.ContainsKey(basicType)) { - Z3Type typeAst = builder.BuildBasicType(basicType); + Z3Type typeAst = BuildBasicType(basicType); basicTypes.Add(basicType, typeAst); } Z3Type result; @@ -87,16 +125,48 @@ namespace Microsoft.Boogie.Z3 return GetBvType((BvType)boogieType); else if (boogieType.GetType().Equals(typeof(BasicType))) return GetBasicType((BasicType)boogieType); + else if (boogieType.GetType().Equals(typeof(MapType))) + return GetMapType((MapType)boogieType); else throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown"); } - } - public class Z3Type { } + private Z3Type WrapType(Sort typeAst) + { + return new Z3SafeType(typeAst); + } - interface Z3TypeBuilder - { - Z3Type BuildBvType(BvType bvType); - Z3Type BuildBasicType(BasicType basicType); + public Z3Type BuildMapType(Z3Type domain, Z3Type range) + { + Context z3 = ((Z3SafeContext)container).z3; + Sort typeAst = z3.MkArraySort(((Z3SafeType)domain).TypeAst, ((Z3SafeType)range).TypeAst); + return WrapType(typeAst); + } + + public Z3Type BuildBvType(BvType bvType) + { + Context z3 = ((Z3SafeContext)container).z3; + Sort typeAst = z3.MkBvSort((uint)bvType.Bits); + return WrapType(typeAst); + } + + public Z3Type BuildBasicType(BasicType basicType) + { + Context z3 = ((Z3SafeContext)container).z3; + Sort typeAst; + if (basicType.IsBool) + { + typeAst = z3.MkBoolSort(); + } + else if (basicType.IsInt) + { + typeAst = z3.MkIntSort(); + } + else + throw new Exception("Unknown Basic Type " + basicType.ToString()); + return WrapType(typeAst); + } } + + public class Z3Type { } } \ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index 25b674a7..b2a84c8f 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -28,13 +28,15 @@ namespace Microsoft.Boogie.Z3 } } - internal readonly UniqueNamer Namer; + internal readonly UniqueNamer namer; + internal readonly Dictionary letBindings; protected Z3Context cm; public Z3apiExprLineariser(Z3Context cm) { this.cm = cm; - this.Namer = new UniqueNamer(); + this.namer = new UniqueNamer(); + this.letBindings = new Dictionary(); } public Z3TermAst Linearise(VCExpr expr, LineariserOptions options) @@ -64,8 +66,6 @@ namespace Microsoft.Boogie.Z3 } } - ///////////////////////////////////////////////////////////////////////////////////// - public Z3TermAst Visit(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); @@ -96,25 +96,28 @@ namespace Microsoft.Boogie.Z3 return node.Accept(OpLineariser, options); } - ///////////////////////////////////////////////////////////////////////////////////// - public Z3TermAst Visit(VCExprVar node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - string varName = Namer.GetName(node, node.Name); - return cm.GetConstant(varName, node.Type); + if (letBindings.ContainsKey(node)) + { + return letBindings[node]; + } + else + { + string varName = namer.GetName(node, node.Name); + return cm.GetConstant(varName, node.Type); + } } - ///////////////////////////////////////////////////////////////////////////////////// - public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); Contract.Assert(node.TypeParameters.Count == 0); - Namer.PushScope(); + namer.PushScope(); try { List varNames; @@ -125,6 +128,7 @@ namespace Microsoft.Boogie.Z3 VisitTriggers(node.Triggers, options, out patterns, out no_patterns); Z3TermAst body = Linearise(node.Body, options); Z3TermAst result; + uint weight = 1; /* if (options.QuantifierIds) @@ -145,25 +149,19 @@ namespace Microsoft.Boogie.Z3 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(") "); - } + weight = (uint) QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1); } - */ switch (node.Quan) { case Quantifier.ALL: - result = cm.MakeForall(varNames, varTypes, patterns, no_patterns, body); break; + result = cm.MakeForall(weight, varNames, varTypes, patterns, no_patterns, body); break; case Quantifier.EX: - result = cm.MakeExists(varNames, varTypes, patterns, no_patterns, body); break; + result = cm.MakeExists(weight, varNames, varTypes, patterns, no_patterns, body); break; default: throw new Exception("unknown quantifier kind " + node.Quan); } @@ -171,7 +169,7 @@ namespace Microsoft.Boogie.Z3 } finally { - Namer.PopScope(); + namer.PopScope(); } } @@ -181,7 +179,7 @@ namespace Microsoft.Boogie.Z3 varTypes = new List(); foreach (VCExprVar var in boundVars) { - string varName = Namer.GetLocalName(var, var.Name); + string varName = namer.GetLocalName(var, var.Name); varNames.Add(varName); varTypes.Add(var.Type); } @@ -209,6 +207,7 @@ namespace Microsoft.Boogie.Z3 } else { + System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats"); foreach (Z3TermAst expr in exprs) no_patterns.Add(expr); } @@ -216,51 +215,32 @@ namespace Microsoft.Boogie.Z3 } } - ///////////////////////////////////////////////////////////////////////////////////// - public Z3TermAst Visit(VCExprLet node, LineariserOptions options) { - Namer.PushScope(); - try + foreach (VCExprLetBinding b in node) { - List equations = new List(); - foreach (VCExprLetBinding b in node) - { - string varName = Namer.GetLocalName(b.V, b.V.Name); - Z3TermAst varAst = cm.GetConstant(varName, b.V.Type); - Z3TermAst defAst = Linearise(b.E, options); - List args = new List(); - args.Add(varAst); - args.Add(defAst); - equations.Add(cm.Make("EQ", args)); - } - System.Diagnostics.Debug.Assert(equations.Count > 0); - Z3TermAst eqAst = cm.Make("AND", equations); - List t = new List(); - t.Add(eqAst); - t.Add(Linearise(node.Body, options)); - return cm.Make("IMPLIES", t); + Z3TermAst defAst = Linearise(b.E, options); + letBindings.Add(b.V, defAst); } - finally + Z3TermAst letAst = Linearise(node.Body, options); + foreach (VCExprLetBinding b in node) { - Namer.PopScope(); + letBindings.Remove(b.V); } + return letAst; } ///////////////////////////////////////////////////////////////////////////////////// - // Lineariser for operator terms. The result (bool) is currently not used for anything - internal class Z3apiOpLineariser : IVCExprOpVisitor + internal class Z3apiOpLineariser : IVCExprOpVisitor { [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(ExprLineariser != null); - Contract.Invariant(wr != null); } - private readonly Z3apiExprLineariser/*!*/ ExprLineariser; - private readonly TextWriter/*!*/ wr; + private readonly Z3apiExprLineariser ExprLineariser; public Z3apiOpLineariser(Z3apiExprLineariser ExprLineariser) { @@ -298,38 +278,14 @@ namespace Microsoft.Boogie.Z3 { Contract.Requires(options != null); Contract.Requires(node != null); - if (node[0].Type.IsBool) - { - Contract.Assert(node[1].Type.IsBool); - // use equivalence - return WriteApplication("IFF", node, options); - } - else - { - Contract.Assert(!node[1].Type.IsBool); - // use equality and write the arguments as terms - return WriteApplication("EQ", node, options); - } + return WriteApplication("EQ", node, options); } public Z3TermAst VisitNeqOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - - if (node[0].Type.IsBool) - { - Contract.Assert(node[1].Type.IsBool); - // use equivalence and negate the whole thing - List args = new List(); - args.Add(WriteApplication("IFF", node, options)); - return ExprLineariser.cm.Make("NOT", args); - } - else - { - // use equality and write the arguments as terms - return WriteApplication("NEQ", node, options); - } + return WriteApplication("NEQ", node, options); } public Z3TermAst VisitAndOp(VCExprNAry node, LineariserOptions options) @@ -393,7 +349,7 @@ namespace Microsoft.Boogie.Z3 Contract.Requires(node != null); VCExprLabelOp op = (VCExprLabelOp)node.Op; Contract.Assert(op != null); - return ExprLineariser.Linearise(node[0], options); + return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); } public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options) @@ -401,12 +357,13 @@ namespace Microsoft.Boogie.Z3 Contract.Requires(options != null); Contract.Requires(node != null); List args = new List(); - foreach (VCExpr/*!*/ e in node) + foreach (VCExpr e in node) { Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } - return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args); + return ExprLineariser.cm.MakeArraySelect(args); + // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args); } public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options) @@ -419,7 +376,8 @@ namespace Microsoft.Boogie.Z3 Contract.Assert(e != null); args.Add(ExprLineariser.Linearise(e, options)); } - return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args); + return ExprLineariser.cm.MakeArrayStore(args); + // return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args); } public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options) @@ -455,7 +413,7 @@ namespace Microsoft.Boogie.Z3 return ExprLineariser.cm.Make("ITE", args); } - public Z3TermAst VisitCustomOp(VCExprNAry/*!*/ node, LineariserOptions/*!*/ options) + public Z3TermAst VisitCustomOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(node != null); Contract.Requires(options != null); @@ -514,42 +472,42 @@ namespace Microsoft.Boogie.Z3 { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<", node, options); // arguments are always terms + return WriteApplication("<", node, options); } public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<=", node, options); // arguments are always terms + return WriteApplication("<=", node, options); } public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication(">", node, options); // arguments are always terms + return WriteApplication(">", node, options); } public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication(">=", node, options); // arguments are always terms + return WriteApplication(">=", node, options); } public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<:", node, options); // arguments are always terms + return WriteApplication("<:", node, options); } public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options) { Contract.Requires(options != null); Contract.Requires(node != null); - return WriteApplication("<::", node, options); // arguments are always terms + return WriteApplication("<::", node, options); } public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) @@ -561,7 +519,7 @@ namespace Microsoft.Boogie.Z3 string funcName = op.Func.Name; Contract.Assert(funcName != null); string bvzName = op.Func.FindStringAttribute("external"); - string printedName = ExprLineariser.Namer.GetName(op.Func, funcName); + string printedName = ExprLineariser.namer.GetName(op.Func, funcName); Contract.Assert(printedName != null); if (bvzName != null) printedName = bvzName; diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 42626ed7..7d994160 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -93,7 +93,7 @@ namespace VC { public Hashtable /*GotoCmd->returnCmd*/ gotoCmdOrigins; public Hashtable/**/ label2absy; - public LazyInliningInfo(Implementation impl, Program program, int uniqueId) { + public LazyInliningInfo(Implementation impl, Program program, ProverContext ctxt, int uniqueId) { Contract.Requires(impl != null); Contract.Requires(program != null); this.impl = impl; @@ -145,6 +145,7 @@ namespace VC { Formal returnVar = new Formal(Token.NoToken, ti, false); Contract.Assert(returnVar != null); this.function = new Function(Token.NoToken, proc.Name, functionInterfaceVars, returnVar); + ctxt.DeclareFunction(this.function, ""); } } [ContractInvariantMethod] @@ -159,6 +160,13 @@ namespace VC { Contract.Requires(program != null); Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); Contract.Assert(checker != null); + + VCExpr a = checker.VCExprGen.Integer(BigNum.ONE); + VCExpr b = checker.VCExprGen.Integer(BigNum.ONE); + VCExprNAry c = (VCExprNAry) checker.VCExprGen.ControlFlowFunctionApplication(a, b); + VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)c.Op; + checker.TheoremProver.Context.DeclareFunction(op.Func, ""); + foreach (Declaration decl in program.TopLevelDeclarations) { Contract.Assert(decl != null); Implementation impl = decl as Implementation; @@ -166,7 +174,7 @@ namespace VC { continue; Procedure proc = cce.NonNull(impl.Proc); if (proc.FindExprAttribute("inline") != null) { - LazyInliningInfo info = new LazyInliningInfo(impl, program, QuantifierExpr.GetNextSkolemId()); + LazyInliningInfo info = new LazyInliningInfo(impl, program, checker.TheoremProver.Context, QuantifierExpr.GetNextSkolemId()); implName2LazyInliningInfo[impl.Name] = info; impl.LocVars.Add(info.controlFlowVariable); ExprSeq exprs = new ExprSeq(); @@ -287,8 +295,8 @@ namespace VC { public VCExpr funcExpr; public VCExpr falseExpr; - public StratifiedInliningInfo(Implementation impl, Program program, int uniqueid) - : base(impl, program, uniqueid) { + public StratifiedInliningInfo(Implementation impl, Program program, ProverContext ctxt, int uniqueid) + : base(impl, program, ctxt, uniqueid) { Contract.Requires(impl != null); Contract.Requires(program != null); inline_cnt = 0; @@ -303,7 +311,7 @@ namespace VC { public void GenerateVCsForStratifiedInlining(Program program) { Contract.Requires(program != null); - //Checker! checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); + Checker checker = FindCheckerFor(null, CommandLineOptions.Clo.ProverKillTime); foreach (Declaration decl in program.TopLevelDeclarations) { Contract.Assert(decl != null); Implementation impl = decl as Implementation; @@ -311,7 +319,7 @@ namespace VC { continue; Procedure proc = cce.NonNull(impl.Proc); if (proc.FindExprAttribute("inline") != null) { - StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, QuantifierExpr.GetNextSkolemId()); + StratifiedInliningInfo info = new StratifiedInliningInfo(impl, program, checker.TheoremProver.Context, QuantifierExpr.GetNextSkolemId()); implName2StratifiedInliningInfo[impl.Name] = info; // We don't need controlFlowVariable for stratified Inlining //impl.LocVars.Add(info.controlFlowVariable); -- cgit v1.2.3