diff options
| author |  Jason Koenig <unknown> | 2011-06-23 13:46:04 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-06-23 13:46:04 -0700 |
| commit | f3fe0e55949bc6fb4396e3401f354e3a47566340 (patch) | |
| tree | b249e08e39bdc1c41723e52c7f37e032584fba5d | |
| parent | 00f87bb88242bbcbb561a3af193d2ee8f5372a16 (diff) | |
| parent | 75935b901d668ab0a4def992d9825b6cc394565c (diff) | |
Merge
41 files changed, 783 insertions, 896 deletions
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index 3a9c74ae..ed45c4fc 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -20,11 +20,6 @@ namespace Microsoft.Boogie.Z3 private string logFilename;
private List<string> debugTraces = new List<string>();
- public void SetModelCompletion(bool enabled)
- {
- config.SetParamValue("MODEL_VALUE_COMPLETION", (enabled ? "true" : "false"));
- }
-
public void SetModel(bool enabled)
{
config.SetParamValue("MODEL", (enabled ? "true" : "false"));
@@ -74,50 +69,20 @@ namespace Microsoft.Boogie.Z3 }
}
- public abstract class Z3TermAst { }
- public abstract class Z3PatternAst { }
- public abstract class Z3ConstDeclAst { }
- public abstract class Z3LabeledLiterals { }
-
- public interface Z3Context
- {
- void CreateBacktrackPoint();
- void Backtrack();
- void AddAxiom(VCExpr axiom, LineariserOptions linOptions);
- void AddConjecture(VCExpr vc, LineariserOptions linOptions);
- void AddSmtlibString(string smtlibString);
- string GetDeclName(Z3ConstDeclAst constDeclAst);
- Z3PatternAst MakePattern(List<Z3TermAst> exprs);
- Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);
- ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors);
- void TypeCheckBool(Z3TermAst t);
- void TypeCheckInt(Z3TermAst t);
- void DeclareType(string typeName);
- void DeclareConstant(string constantName, Type boogieType);
- void DeclareFunction(string functionName, List<Type> domain, Type range);
- Z3TermAst GetConstant(string constantName, Type constantType);
- Z3TermAst MakeIntLiteral(string numeral);
- Z3TermAst MakeTrue();
- Z3TermAst MakeFalse();
- Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child);
- Z3LabeledLiterals GetRelevantLabels();
- Z3TermAst Make(string op, List<Z3TermAst> children);
- Z3TermAst MakeArraySelect(List<Z3TermAst> args);
- Z3TermAst MakeArrayStore(List<Z3TermAst> args);
- }
-
internal class PartitionMap
{
private Context ctx;
+ private Model model;
private Dictionary<Term, int> termToPartition = new Dictionary<Term, int>();
private Dictionary<object, int> valueToPartition = new Dictionary<object, int>();
private List<Object> partitionToValue = new List<Object>();
private int partitionCounter = 0;
public int PartitionCounter { get { return partitionCounter; } }
- public PartitionMap(Context ctx)
+ public PartitionMap(Context ctx, Model z3Model)
{
- this.ctx = ctx;
+ this.ctx = ctx;
+ this.model = z3Model;
}
public int GetPartition(Term value)
@@ -141,43 +106,51 @@ namespace Microsoft.Boogie.Z3 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;
- if (ctx.TryGetNumeralInt(v, out i))
- {
- return BigNum.FromInt(i);
- }
- else
- {
- return BigNum.FromString(ctx.GetNumeralString(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 (ctx.TryGetArrayValue(v, out av))
- {
- List<List<int>> arrayValue = new List<List<int>>();
- List<int> tuple;
- for (int i = 0; i < av.Domain.Length; i++)
- {
- tuple = new List<int>();
- tuple.Add(GetPartition(av.Domain[i]));
- tuple.Add(GetPartition(av.Range[i]));
- arrayValue.Add(tuple);
- }
+ else if (model.TryGetArrayValue(v, out av)) {
+ List<List<int>> arrayValue = new List<List<int>>();
+ List<int> tuple;
+ for (int i = 0; i < av.Domain.Length; i++) {
tuple = new List<int>();
- tuple.Add(GetPartition(av.ElseCase));
+ tuple.Add(GetPartition(av.Domain[i]));
+ tuple.Add(GetPartition(av.Range[i]));
arrayValue.Add(tuple);
- return arrayValue;
+ }
+ tuple = new List<int>();
+ tuple.Add(GetPartition(av.ElseCase));
+ arrayValue.Add(tuple);
+ return arrayValue;
}
- else
- {
- // The term is uninterpreted; just return the partition id.
- return GetPartition(v);
+ else {
+ // The term is uninterpreted; just return the partition id.
+ return GetPartition(v);
}
}
@@ -249,10 +222,10 @@ namespace Microsoft.Boogie.Z3 private Z3Context container;
private PartitionMap partitionMap;
- public BoogieErrorModelBuilder(Z3Context container)
+ public BoogieErrorModelBuilder(Z3Context container, Model z3Model)
{
this.container = container;
- this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3);
+ this.partitionMap = new PartitionMap(((Z3Context)container).z3, z3Model);
}
private Dictionary<string, int> CreateConstantToPartition(Model z3Model)
@@ -260,7 +233,7 @@ namespace Microsoft.Boogie.Z3 Dictionary<string, int> constantToPartition = new Dictionary<string, int>();
foreach (FuncDecl c in z3Model.GetModelConstants())
{
- string name = container.GetDeclName(new Z3TypeSafeConstDecl(c));
+ string name = container.GetDeclName(c);
int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0]));
constantToPartition.Add(name, pid);
}
@@ -288,7 +261,7 @@ namespace Microsoft.Boogie.Z3 foreach (KeyValuePair<FuncDecl, FunctionGraph> kv in z3Model.GetFunctionGraphs())
{
List<List<int>> f_tuples = new List<List<int>>();
- string f_name = container.GetDeclName(new Z3TypeSafeConstDecl(kv.Key));
+ string f_name = container.GetDeclName(kv.Key);
FunctionGraph graph = kv.Value;
foreach (FunctionEntry entry in graph.Entries)
{
@@ -313,8 +286,8 @@ namespace Microsoft.Boogie.Z3 Dictionary<string, int> constantToPartition = CreateConstantToPartition(z3Model);
Dictionary<string, List<List<int>>> functionToPartition = CreateFunctionToPartition(z3Model);
List<List<string>> partitionToConstant = CreatePartitionToConstant(constantToPartition);
- List<Object> partitionToValue = partitionMap.PartitionToValue(((Z3SafeContext)container).z3);
- Dictionary<object, int> valueToPartition = partitionMap.ValueToPartition(((Z3SafeContext)container).z3);
+ List<Object> partitionToValue = partitionMap.PartitionToValue(((Z3Context)container).z3);
+ Dictionary<object, int> valueToPartition = partitionMap.ValueToPartition(((Z3Context)container).z3);
return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition);
}
}
@@ -337,4 +310,395 @@ namespace Microsoft.Boogie.Z3 this._relevantLabels = relevantLabels;
}
}
+
+ public class Z3Context {
+ private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();
+ internal BacktrackDictionary<string, Term> constants = new BacktrackDictionary<string, Term>();
+ internal BacktrackDictionary<string, FuncDecl> functions = new BacktrackDictionary<string, FuncDecl>();
+ internal BacktrackDictionary<string, Term> labels = new BacktrackDictionary<string, Term>();
+
+ public Context z3;
+ public Z3Config config;
+ public Z3apiProverContext ctxt;
+ private VCExpressionGenerator gen;
+ private Z3TypeCachedBuilder tm;
+ private UniqueNamer namer;
+ public UniqueNamer Namer {
+ get { return namer; }
+ }
+ private StreamWriter z3log;
+ public Z3Context(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen) {
+ Context z3 = new Context(config.Config);
+ if (config.LogFilename != null)
+ z3.OpenLog(config.LogFilename);
+ foreach (string tag in config.DebugTraces)
+ z3.EnableDebugTrace(tag);
+ this.ctxt = ctxt;
+ this.z3 = z3;
+ this.config = config;
+ this.tm = new Z3TypeCachedBuilder(this);
+ this.gen = gen;
+ this.namer = new UniqueNamer();
+ this.z3.SetPrintMode(PrintMode.Smtlib2Compliant);
+ this.z3log = null;
+ }
+
+ public void log(string format, params object[] args) {
+ // Currently, this is a no-op because z3log is always null
+ // We use the default (automatic) tracing facility of z3
+ if (z3log != null) {
+ var str = string.Format(format, args);
+ // Do standard string replacement
+ str = str.Replace("array", "Array");
+ z3log.WriteLine(str);
+ z3log.Flush();
+ }
+ }
+
+ public void CloseLog() {
+ z3.CloseLog();
+ if (z3log != null) {
+ z3log.Close();
+ }
+ z3log = null;
+ }
+
+ public void CreateBacktrackPoint() {
+ symbols.CreateBacktrackPoint();
+ constants.CreateBacktrackPoint();
+ functions.CreateBacktrackPoint();
+ labels.CreateBacktrackPoint();
+ z3.Push();
+ log("(push)");
+ }
+
+ public void Backtrack() {
+ z3.Pop();
+ labels.Backtrack();
+ functions.Backtrack();
+ constants.Backtrack();
+ symbols.Backtrack();
+ log("(pop)");
+ }
+
+ public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) {
+ Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+ Term term = (Term)axiom.Accept(visitor, linOptions);
+ log("(assert {0})", term);
+ z3.AssertCnstr(term);
+ }
+
+ public void AddConjecture(VCExpr vc, LineariserOptions linOptions) {
+ VCExpr not_vc = (VCExpr)this.gen.Not(vc);
+ Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+ Term term = (Term)not_vc.Accept(visitor, linOptions);
+ log("(assert {0})", term);
+ z3.AssertCnstr(term);
+ }
+
+ public void AddSmtlibString(string smtlibString) {
+ FuncDecl[] decls;
+ Term[] assumptions;
+ Term[] terms;
+ Sort[] sorts;
+ string tmp;
+
+ z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { },
+ out assumptions, out terms, out decls, out sorts, out tmp);
+ // TBD: check with Nikolaj about the correct position of assumptions
+ foreach (FuncDecl decl in decls) {
+ Symbol symbol = z3.GetDeclName(decl);
+ string functionName = z3.GetSymbolString(symbol);
+ functions.Add(functionName, decl);
+ }
+ foreach (Term assumption in assumptions) {
+ log("(assert {0})", assumption);
+ z3.AssertCnstr(assumption);
+ }
+ }
+
+ public string GetDeclName(FuncDecl constDeclAst) {
+ Symbol symbol = z3.GetDeclName(constDeclAst);
+ return z3.GetSymbolString(symbol);
+ }
+
+ public Pattern MakePattern(List<Term> exprs) {
+ Pattern pattern = z3.MkPattern(exprs.ToArray());
+ return pattern;
+ }
+
+ private List<Sort> GetTypes(List<Type> boogieTypes) {
+ List<Sort> z3Types = new List<Sort>();
+ foreach (Type boogieType in boogieTypes) {
+ Sort type = tm.GetType(boogieType);
+ z3Types.Add(type);
+ }
+ return z3Types;
+ }
+
+ public Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Pattern> patterns, List<Term> no_patterns, Term body) {
+ List<Term> bound = new List<Term>();
+ for (int i = 0; i < varNames.Count; i++) {
+ Term t = GetConstant(varNames[i], boogieTypes[i]);
+ bound.Add(t);
+ }
+
+ Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid.ToString()), patterns.ToArray(), no_patterns.ToArray(), bound.ToArray(), body);
+ return termAst;
+ }
+
+ private static bool Equals(List<string> l, List<string> r) {
+ Debug.Assert(l != null);
+ if (r == null)
+ return false;
+
+ if (l.Count != r.Count)
+ return false;
+
+ for (int i = 0; i < l.Count; i++)
+ if (!l[i].Equals(r[i]))
+ return false;
+ return true;
+ }
+
+ private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels) {
+ BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this, z3Model);
+ Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model);
+ return new Z3ErrorModelAndLabels(boogieModel, new List<string>(relevantLabels));
+ }
+
+ private void DisplayRelevantLabels(List<string> relevantLabels) {
+ foreach (string labelName in relevantLabels) {
+ System.Console.Write(labelName + ",");
+ }
+ System.Console.WriteLine("---");
+ }
+
+ public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {
+ Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
+ boogieErrors = new List<Z3ErrorModelAndLabels>();
+ LBool outcome = LBool.Undef;
+ Debug.Assert(0 < this.config.Counterexamples);
+ while (true) {
+ Model z3Model;
+ outcome = z3.CheckAndGetModel(out z3Model);
+ log("(check-sat)");
+ if (outcome == LBool.False)
+ break;
+
+ if (outcome == LBool.Undef && z3Model == null) {
+ // Blame this on timeout
+ return ProverInterface.Outcome.TimeOut;
+ }
+
+ Debug.Assert(z3Model != null);
+ LabeledLiterals labels = z3.GetRelevantLabels();
+ Debug.Assert(labels != null);
+
+ List<string> labelStrings = new List<string>();
+ uint numLabels = labels.GetNumLabels();
+ for (uint i = 0; i < numLabels; ++i) {
+ Symbol sym = labels.GetLabel(i);
+ string labelName = z3.GetSymbolString(sym);
+ if (!labelName.StartsWith("@")) {
+ labels.Disable(i);
+ }
+ labelStrings.Add(labelName);
+ }
+ boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
+
+ if (boogieErrors.Count < this.config.Counterexamples) {
+ z3.BlockLiterals(labels);
+ log("block-literals {0}", labels);
+ }
+
+ labels.Dispose();
+ z3Model.Dispose();
+ if (boogieErrors.Count == this.config.Counterexamples)
+ break;
+ }
+
+ if (boogieErrors.Count > 0) {
+ return ProverInterface.Outcome.Invalid;
+ }
+ else if (outcome == LBool.False) {
+ return ProverInterface.Outcome.Valid;
+ }
+ else {
+ Debug.Assert(outcome == LBool.Undef);
+ return ProverInterface.Outcome.Undetermined;
+ }
+ }
+
+ public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions,
+ out List<Z3ErrorModelAndLabels> boogieErrors,
+ out List<int> unsatCore) {
+ Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
+ boogieErrors = new List<Z3ErrorModelAndLabels>();
+ unsatCore = new List<int>();
+ LBool outcome = LBool.Undef;
+
+ Model z3Model;
+ Term proof;
+ Term[] core;
+ Term[] assumption_terms = new Term[assumptions.Count];
+ var logstring = "";
+ for (int i = 0; i < assumptions.Count; i++) {
+ Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
+ Term z3ast = (Term)assumptions[i].Accept(visitor, linOptions);
+ assumption_terms[i] = z3ast;
+ logstring += string.Format("({0}) ", assumption_terms[i]);
+ }
+
+ log("(get-core {0})", logstring);
+ outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);
+
+ if (outcome != LBool.False) {
+ Debug.Assert(z3Model != null);
+ LabeledLiterals labels = z3.GetRelevantLabels();
+ Debug.Assert(labels != null);
+
+ List<string> labelStrings = new List<string>();
+ uint numLabels = labels.GetNumLabels();
+ for (uint i = 0; i < numLabels; ++i) {
+ Symbol sym = labels.GetLabel(i);
+ string labelName = z3.GetSymbolString(sym);
+ if (!labelName.StartsWith("@")) {
+ labels.Disable(i);
+ }
+ labelStrings.Add(labelName);
+ }
+ boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
+
+ labels.Dispose();
+ z3Model.Dispose();
+ }
+
+ if (boogieErrors.Count > 0) {
+ return ProverInterface.Outcome.Invalid;
+ }
+ else if (outcome == LBool.False) {
+ foreach (Term t in core) {
+ for (int i = 0; i < assumption_terms.Length; i++) {
+ if (t.Equals(assumption_terms[i]))
+ unsatCore.Add(i);
+ }
+ }
+ return ProverInterface.Outcome.Valid;
+ }
+ else {
+ Debug.Assert(outcome == LBool.Undef);
+ return ProverInterface.Outcome.Undetermined;
+ }
+ }
+
+ public void DeclareType(string typeName) {
+ log("(declare-sort {0})", typeName);
+ }
+
+ public void DeclareConstant(string constantName, Type boogieType) {
+ Symbol symbolAst = GetSymbol(constantName);
+ Sort typeAst = tm.GetType(boogieType);
+
+ Term constAst = z3.MkConst(symbolAst, typeAst);
+ constants.Add(constantName, constAst);
+ log("(declare-funs (({0} {1})))", constAst, typeAst);
+ }
+
+ public void DeclareFunction(string functionName, List<Type> domain, Type range) {
+ Symbol symbolAst = GetSymbol(functionName);
+ var domainStr = "";
+ List<Sort> domainAst = new List<Sort>();
+ foreach (Type domainType in domain) {
+ Sort type = tm.GetType(domainType);
+ domainAst.Add(type);
+ domainStr += type.ToString() + " ";
+ }
+ Sort rangeAst = tm.GetType(range);
+ FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), rangeAst);
+ functions.Add(functionName, constDeclAst);
+ log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);
+ }
+
+ private List<Symbol> GetSymbols(List<string> symbolNames) {
+ List<Symbol> symbols = new List<Symbol>();
+ foreach (string symbolName in symbolNames)
+ symbols.Add(GetSymbol(symbolName));
+ return symbols;
+ }
+
+ private Symbol GetSymbol(string symbolName) {
+ if (!symbols.ContainsKey(symbolName)) {
+ Symbol symbolAst = z3.MkSymbol(symbolName);
+ symbols.Add(symbolName, symbolAst);
+ }
+ Symbol result;
+ if (!symbols.TryGetValue(symbolName, out result))
+ throw new Exception("symbol " + symbolName + " is undefined");
+ return result;
+ }
+
+ private FuncDecl GetFunction(string functionName) {
+ FuncDecl function;
+ if (!functions.TryGetValue(functionName, out function))
+ throw new Exception("function " + functionName + " is undefined");
+ return function;
+ }
+
+ public Term GetConstant(string constantName, Type constantType) {
+ Term typeSafeTerm;
+ if (!constants.ContainsKey(constantName))
+ this.DeclareConstant(constantName, constantType);
+
+ if (!constants.TryGetValue(constantName, out typeSafeTerm))
+ throw new Exception("constant " + constantName + " is not defined");
+ return typeSafeTerm;
+ }
+
+ public Term MakeLabel(string labelName, bool pos, Term child) {
+ Symbol labelSymbol = this.GetSymbol(labelName);
+ Term labeledExpr = z3.MkLabel(labelSymbol, pos, child);
+ labels.Add(labelName, labeledExpr);
+ return labeledExpr;
+ }
+
+ public LabeledLiterals GetRelevantLabels() {
+ LabeledLiterals safeLiterals = z3.GetRelevantLabels();
+ log("get-relevant-labels");
+ return safeLiterals;
+ }
+
+ public Term Make(string op, List<Term> 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;
+ }
+ return term;
+ }
+ }
}
\ No newline at end of file diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index 5f776bff..f691cffc 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -47,7 +47,7 @@ namespace Microsoft.Boogie.Z3 public override void Close()
{
base.Close();
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
cm.CloseLog();
cm.z3.Dispose();
cm.config.Config.Dispose();
@@ -55,7 +55,7 @@ namespace Microsoft.Boogie.Z3 public void PushAxiom(VCExpr axiom)
{
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
cm.CreateBacktrackPoint();
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
cm.AddAxiom(axiom, linOptions);
@@ -64,7 +64,7 @@ namespace Microsoft.Boogie.Z3 private void PushConjecture(VCExpr conjecture)
{
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
cm.CreateBacktrackPoint();
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
cm.AddConjecture(conjecture, linOptions);
@@ -78,14 +78,14 @@ namespace Microsoft.Boogie.Z3 public void CreateBacktrackPoint()
{
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
cm.CreateBacktrackPoint();
}
public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
Push();
cm.AddAxiom(context.Axioms, linOptions);
cm.AddConjecture(vc, linOptions);
@@ -95,33 +95,33 @@ namespace Microsoft.Boogie.Z3 public override void Check()
{
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
outcome = cm.Check(out z3LabelModels);
}
public override void CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore)
{
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
outcome = cm.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
}
public override void Push()
{
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
cm.CreateBacktrackPoint();
}
public override void Pop()
{
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
cm.Backtrack();
}
public override void Assert(VCExpr vc, bool polarity)
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
if (polarity)
cm.AddAxiom(vc, linOptions);
else
@@ -131,7 +131,7 @@ namespace Microsoft.Boogie.Z3 public override void AssertAxioms()
{
LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- Z3SafeContext cm = context.cm;
+ Z3Context cm = context.cm;
cm.AddAxiom(context.Axioms, linOptions);
}
@@ -191,18 +191,17 @@ namespace Microsoft.Boogie.Z3 public class Z3apiProverContext : DeclFreeProverContext
{
- public Z3SafeContext cm;
+ public Z3Context cm;
public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)
: base(gen, new VCGenerationOptions(new List<string>()))
{
Z3Config config = BuildConfig(opts.Timeout * 1000, true);
- this.cm = new Z3SafeContext(this, config, gen);
+ this.cm = new Z3Context(this, config, gen);
}
private static Z3Config BuildConfig(int timeout, bool nativeBv)
{
Z3Config config = new Z3Config();
- config.SetModelCompletion(false);
config.SetModel(true);
if (0 <= CommandLineOptions.Clo.ProverCCLimit)
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index a7ed29eb..72192804 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -12,641 +12,5 @@ using Microsoft.Boogie.VCExprAST; namespace Microsoft.Boogie.Z3
{
- internal class Z3TypeSafeTerm : Z3TermAst
- {
- private Term termAst;
- public Z3TypeSafeTerm(Term termAst)
- {
- this.termAst = termAst;
- }
- public Term TermAst
- {
- get { return this.termAst; }
- }
- }
-
- internal class Z3TypeSafePattern : Z3PatternAst
- {
- private Pattern patternAst;
- public Z3TypeSafePattern(Pattern patternAst)
- {
- this.patternAst = patternAst;
- }
- public Pattern PatternAst
- {
- get { return this.patternAst; }
- }
- }
-
- internal class Z3TypeSafeConstDecl : Z3ConstDeclAst
- {
- private FuncDecl constDeclAst;
- public Z3TypeSafeConstDecl(FuncDecl constDeclAst)
- {
- this.constDeclAst = constDeclAst;
- }
- public FuncDecl ConstDeclAst
- {
- get { return this.constDeclAst; }
- }
- }
-
- public class Z3SafeType : Z3Type
- {
- private Sort typeAst;
- public Z3SafeType(Sort typeAst)
- {
- this.typeAst = typeAst;
- }
- public Sort TypeAst
- {
- get { return this.typeAst; }
- }
- }
-
- public class Z3SafeLabeledLiterals : Z3LabeledLiterals
- {
- private LabeledLiterals labeledLiterals;
- public Z3SafeLabeledLiterals(LabeledLiterals labeledLiterals)
- {
- this.labeledLiterals = labeledLiterals;
- }
- public LabeledLiterals LabeledLiterals
- {
- get { return this.labeledLiterals; }
- }
- }
-
- public class Z3SafeContext : Z3Context
- {
- private BacktrackDictionary<string, Symbol> symbols = new BacktrackDictionary<string, Symbol>();
- internal BacktrackDictionary<string, Z3TypeSafeTerm> constants = new BacktrackDictionary<string, Z3TypeSafeTerm>();
- internal BacktrackDictionary<string, Z3TypeSafeConstDecl> functions = new BacktrackDictionary<string, Z3TypeSafeConstDecl>();
- internal BacktrackDictionary<string, Z3TypeSafeTerm> labels = new BacktrackDictionary<string, Z3TypeSafeTerm>();
-
- public Context z3;
- public Z3Config config;
- public Z3apiProverContext ctxt;
- private VCExpressionGenerator gen;
- private Z3TypeCachedBuilder tm;
- private UniqueNamer namer;
- public UniqueNamer Namer
- {
- get { return namer; }
- }
- private StreamWriter z3log;
- public Z3SafeContext(Z3apiProverContext ctxt, Z3Config config, VCExpressionGenerator gen)
- {
- Context z3 = new Context(config.Config);
- if (config.LogFilename != null)
- z3.OpenLog(config.LogFilename);
- foreach (string tag in config.DebugTraces)
- z3.EnableDebugTrace(tag);
- this.ctxt = ctxt;
- this.z3 = z3;
- this.config = config;
- this.tm = new Z3TypeCachedBuilder(this);
- this.gen = gen;
- this.namer = new UniqueNamer();
- this.z3.SetPrintMode(PrintMode.Smtlib2Compliant);
- this.z3log = null;
- }
-
- public void log(string format, params object[] args)
- {
- // Currently, this is a no-op because z3log is always null
- // We use the default (automatic) tracing facility of z3
- if (z3log != null)
- {
- var str = string.Format(format, args);
- // Do standard string replacement
- str = str.Replace("array", "Array");
- z3log.WriteLine(str);
- z3log.Flush();
- }
- }
-
- public void CloseLog()
- {
- z3.CloseLog();
- if (z3log != null)
- {
- z3log.Close();
- }
- z3log = null;
- }
-
- public void CreateBacktrackPoint()
- {
- symbols.CreateBacktrackPoint();
- constants.CreateBacktrackPoint();
- functions.CreateBacktrackPoint();
- labels.CreateBacktrackPoint();
- z3.Push();
- log("(push)");
- }
-
- public void Backtrack()
- {
- z3.Pop();
- labels.Backtrack();
- functions.Backtrack();
- constants.Backtrack();
- symbols.Backtrack();
- log("(pop)");
- }
-
- public void AddAxiom(VCExpr axiom, LineariserOptions linOptions)
- {
- Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
- Z3TermAst z3ast = (Z3TermAst)axiom.Accept(visitor, linOptions);
- Term term = Unwrap(z3ast);
- log("(assert {0})", term);
- z3.AssertCnstr(term);
- }
-
- public void AddConjecture(VCExpr vc, LineariserOptions linOptions)
- {
- VCExpr not_vc = (VCExpr)this.gen.Not(vc);
- Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
- Z3TermAst z3ast = (Z3TermAst)not_vc.Accept(visitor, linOptions);
- Term term = Unwrap(z3ast);
- log("(assert {0})", term);
- z3.AssertCnstr(term);
- }
-
- public void AddSmtlibString(string smtlibString)
- {
- FuncDecl[] decls;
- Term[] assumptions;
- Term[] terms;
- Sort[] sorts;
- string tmp;
-
- z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { },
- out assumptions, out terms, out decls, out sorts, out tmp);
- // TBD: check with Nikolaj about the correct position of assumptions
- foreach (FuncDecl decl in decls)
- {
- Symbol symbol = z3.GetDeclName(decl);
- string functionName = z3.GetSymbolString(symbol);
- functions.Add(functionName, new Z3TypeSafeConstDecl(decl));
- }
- foreach (Term assumption in assumptions)
- {
- log("(assert {0})", assumption);
- z3.AssertCnstr(assumption);
- }
- }
-
- public string GetDeclName(Z3ConstDeclAst constDeclAst)
- {
- Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst;
- Symbol symbol = z3.GetDeclName(typeSafeConstDecl.ConstDeclAst);
- return z3.GetSymbolString(symbol);
- }
-
- private List<Term> Unwrap(List<Z3TermAst> terms)
- {
- List<Term> unwrap = new List<Term>();
- foreach (Z3TermAst term in terms)
- {
- Term unwrapTerm = Unwrap(term);
- unwrap.Add(unwrapTerm);
- }
- return unwrap;
- }
-
- private List<Pattern> Unwrap(List<Z3PatternAst> patterns)
- {
- List<Pattern> unwrap = new List<Pattern>();
- foreach (Z3PatternAst pattern in patterns)
- {
- Z3TypeSafePattern typeSafePattern = (Z3TypeSafePattern)pattern;
- unwrap.Add(typeSafePattern.PatternAst);
- }
- return unwrap;
- }
-
- private Sort Unwrap(Z3Type type)
- {
- Z3SafeType typeSafeTerm = (Z3SafeType)type;
- return typeSafeTerm.TypeAst;
- }
-
- private Term Unwrap(Z3TermAst term)
- {
- Z3TypeSafeTerm typeSafeTerm = (Z3TypeSafeTerm)term;
- return typeSafeTerm.TermAst;
- }
-
- private FuncDecl Unwrap(Z3ConstDeclAst constDeclAst)
- {
- Z3TypeSafeConstDecl typeSafeConstDecl = (Z3TypeSafeConstDecl)constDeclAst;
- return typeSafeConstDecl.ConstDeclAst;
- }
-
- private Z3TypeSafeTerm Wrap(Term term)
- {
- return new Z3TypeSafeTerm(term);
- }
-
- private Z3TypeSafeConstDecl Wrap(FuncDecl constDecl)
- {
- return new Z3TypeSafeConstDecl(constDecl);
- }
-
- private Z3TypeSafePattern Wrap(Pattern pattern)
- {
- return new Z3TypeSafePattern(pattern);
- }
-
- public Z3PatternAst MakePattern(List<Z3TermAst> exprs)
- {
- List<Term> unwrapExprs = Unwrap(exprs);
- Pattern pattern = z3.MkPattern(unwrapExprs.ToArray());
- Z3PatternAst wrapPattern = Wrap(pattern);
- return wrapPattern;
- }
-
- private List<Sort> GetTypes(List<Type> boogieTypes)
- {
- List<Sort> z3Types = new List<Sort>();
- foreach (Type boogieType in boogieTypes)
- {
- Z3Type type = tm.GetType(boogieType);
- Sort unwrapType = Unwrap(type);
- z3Types.Add(unwrapType);
- }
- return z3Types;
- }
-
- public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body)
- {
- List<Pattern> unwrapPatterns = Unwrap(patterns);
- List<Term> unwrapNoPatterns = Unwrap(no_patterns);
- Term unwrapBody = Unwrap(body);
-
- List<Term> bound = new List<Term>();
- for (int i = 0; i < varNames.Count; i++)
- {
- Z3TermAst t = GetConstant(varNames[i], boogieTypes[i]);
- bound.Add(Unwrap(t));
- }
-
- Term termAst = z3.MkQuantifier(isForall, weight, z3.MkSymbol(qid), z3.MkSymbol(skolemid.ToString()), unwrapPatterns.ToArray(), unwrapNoPatterns.ToArray(), bound.ToArray(), unwrapBody);
- return Wrap(termAst);
- }
- private static bool Equals(List<string> l, List<string> r)
- {
- Debug.Assert(l != null);
- if (r == null)
- return false;
-
- if (l.Count != r.Count)
- return false;
-
- for (int i = 0; i < l.Count; i++)
- if (!l[i].Equals(r[i]))
- return false;
- return true;
- }
-
- private Z3ErrorModelAndLabels BuildZ3ErrorModel(Model z3Model, List<string> relevantLabels)
- {
- BoogieErrorModelBuilder boogieErrorBuilder = new BoogieErrorModelBuilder(this);
- Z3ErrorModel boogieModel = boogieErrorBuilder.BuildBoogieModel(z3Model);
- return new Z3ErrorModelAndLabels(boogieModel, new List<string>(relevantLabels));
- }
-
- private void DisplayRelevantLabels(List<string> relevantLabels)
- {
- foreach (string labelName in relevantLabels)
- {
- System.Console.Write(labelName + ",");
- }
- System.Console.WriteLine("---");
- }
-
- public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors)
- {
- Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
- boogieErrors = new List<Z3ErrorModelAndLabels>();
- LBool outcome = LBool.Undef;
- Debug.Assert(0 < this.config.Counterexamples);
- while (true)
- {
- Model z3Model;
- outcome = z3.CheckAndGetModel(out z3Model);
- log("(check-sat)");
- if (outcome == LBool.False)
- break;
-
- if (outcome == LBool.Undef && z3Model == null)
- {
- // Blame this on timeout
- return ProverInterface.Outcome.TimeOut;
- }
-
- Debug.Assert(z3Model != null);
- LabeledLiterals labels = z3.GetRelevantLabels();
- Debug.Assert(labels != null);
-
- List<string> labelStrings = new List<string>();
- uint numLabels = labels.GetNumLabels();
- for (uint i = 0; i < numLabels; ++i)
- {
- Symbol sym = labels.GetLabel(i);
- string labelName = z3.GetSymbolString(sym);
- if (!labelName.StartsWith("@"))
- {
- labels.Disable(i);
- }
- labelStrings.Add(labelName);
- }
- boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
-
- if (boogieErrors.Count < this.config.Counterexamples)
- {
- z3.BlockLiterals(labels);
- log("block-literals {0}", labels);
- }
-
- labels.Dispose();
- z3Model.Dispose();
- if (boogieErrors.Count == this.config.Counterexamples)
- break;
- }
-
- if (boogieErrors.Count > 0)
- {
- return ProverInterface.Outcome.Invalid;
- }
- else if (outcome == LBool.False)
- {
- return ProverInterface.Outcome.Valid;
- }
- else
- {
- Debug.Assert(outcome == LBool.Undef);
- return ProverInterface.Outcome.Undetermined;
- }
- }
-
- public ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, LineariserOptions linOptions,
- out List<Z3ErrorModelAndLabels> boogieErrors,
- out List<int> unsatCore)
- {
- Microsoft.Boogie.Helpers.ExtraTraceInformation("Sending data to the theorem prover");
- boogieErrors = new List<Z3ErrorModelAndLabels>();
- unsatCore = new List<int>();
- LBool outcome = LBool.Undef;
-
- Model z3Model;
- Term proof;
- Term[] core;
- Term[] assumption_terms = new Term[assumptions.Count];
- var logstring = "";
- for (int i = 0; i < assumptions.Count; i++)
- {
- Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
- Z3TermAst z3ast = (Z3TermAst)assumptions[i].Accept(visitor, linOptions);
- assumption_terms[i] = Unwrap(z3ast);
- logstring += string.Format("({0}) ", assumption_terms[i]);
- }
-
- log("(get-core {0})", logstring);
- outcome = z3.CheckAssumptions(out z3Model, assumption_terms, out proof, out core);
-
- if (outcome != LBool.False)
- {
- Debug.Assert(z3Model != null);
- LabeledLiterals labels = z3.GetRelevantLabels();
- Debug.Assert(labels != null);
-
- List<string> labelStrings = new List<string>();
- uint numLabels = labels.GetNumLabels();
- for (uint i = 0; i < numLabels; ++i)
- {
- Symbol sym = labels.GetLabel(i);
- string labelName = z3.GetSymbolString(sym);
- if (!labelName.StartsWith("@"))
- {
- labels.Disable(i);
- }
- labelStrings.Add(labelName);
- }
- boogieErrors.Add(BuildZ3ErrorModel(z3Model, labelStrings));
-
- labels.Dispose();
- z3Model.Dispose();
- }
-
- if (boogieErrors.Count > 0)
- {
- return ProverInterface.Outcome.Invalid;
- }
- else if (outcome == LBool.False)
- {
- foreach (Term t in core)
- {
- for (int i = 0; i < assumption_terms.Length; i++)
- {
- if (t.Equals(assumption_terms[i]))
- unsatCore.Add(i);
- }
- }
- return ProverInterface.Outcome.Valid;
- }
- else
- {
- Debug.Assert(outcome == LBool.Undef);
- return ProverInterface.Outcome.Undetermined;
- }
- }
-
- public void TypeCheckBool(Z3TermAst term)
- {
- Term unwrapTerm = Unwrap(term);
- bool boolType = z3.GetSort(unwrapTerm).Equals(z3.MkBoolSort());
- if (!boolType)
- throw new Exception("Failed Bool Typecheck");
- }
-
- public void TypeCheckInt(Z3TermAst term)
- {
- Term unwrapTerm = Unwrap(term);
- bool intType = z3.GetSort(unwrapTerm).Equals(z3.MkIntSort());
- if (!intType)
- throw new Exception("Failed Int Typecheck");
- }
-
- public void DeclareType(string typeName)
- {
- log("(declare-sort {0})", typeName);
- }
-
- public void DeclareConstant(string constantName, Type boogieType)
- {
- Symbol symbolAst = GetSymbol(constantName);
- Z3Type typeAst = tm.GetType(boogieType);
- Sort unwrapTypeAst = Unwrap(typeAst);
-
- Term constAst = z3.MkConst(symbolAst, unwrapTypeAst);
- constants.Add(constantName, Wrap(constAst));
- log("(declare-funs (({0} {1})))", constAst, unwrapTypeAst);
- }
-
- public void DeclareFunction(string functionName, List<Type> domain, Type range)
- {
- Symbol symbolAst = GetSymbol(functionName);
-
- var domainStr = "";
- List<Sort> domainAst = new List<Sort>();
- foreach (Type domainType in domain)
- {
- Z3Type type = tm.GetType(domainType);
- Sort unwrapType = Unwrap(type);
- domainAst.Add(unwrapType);
- domainStr += unwrapType.ToString() + " ";
- }
- Z3Type rangeAst = tm.GetType(range);
- Sort unwrapRangeAst = Unwrap(rangeAst);
- FuncDecl constDeclAst = z3.MkFuncDecl(symbolAst, domainAst.ToArray(), unwrapRangeAst);
- Z3TypeSafeConstDecl typeSafeConstDecl = Wrap(constDeclAst);
- functions.Add(functionName, typeSafeConstDecl);
- log("(declare-funs (({0} {1} {2})))", functionName, domainStr, unwrapRangeAst);
- }
-
- private List<Symbol> GetSymbols(List<string> symbolNames)
- {
- List<Symbol> symbols = new List<Symbol>();
- foreach (string symbolName in symbolNames)
- symbols.Add(GetSymbol(symbolName));
- return symbols;
- }
-
- private Symbol GetSymbol(string symbolName)
- {
- if (!symbols.ContainsKey(symbolName))
- {
- Symbol symbolAst = z3.MkSymbol(symbolName);
- symbols.Add(symbolName, symbolAst);
- }
- Symbol result;
- if (!symbols.TryGetValue(symbolName, out result))
- throw new Exception("symbol " + symbolName + " is undefined");
- return result;
- }
-
- public Z3TermAst GetConstant(string constantName, Type constantType)
- {
- Z3TypeSafeTerm typeSafeTerm;
- if (!constants.ContainsKey(constantName))
- this.DeclareConstant(constantName, constantType);
-
- if (!constants.TryGetValue(constantName, out typeSafeTerm))
- throw new Exception("constant " + constantName + " is not defined");
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeIntLiteral(string numeral)
- {
- Term term = z3.MkNumeral(numeral, z3.MkIntSort());
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeTrue()
- {
- Term term = z3.MkTrue();
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeFalse()
- {
- Term term = z3.MkFalse();
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child)
- {
- Symbol labelSymbol = this.GetSymbol(labelName);
- Term unwrapChild = Unwrap(child);
-
- Term labeledExpr = z3.MkLabel(labelSymbol, pos, unwrapChild);
-
- Z3TypeSafeTerm wrapLabeledExpr = Wrap(labeledExpr);
- labels.Add(labelName, wrapLabeledExpr);
- return wrapLabeledExpr;
- }
-
- public Z3LabeledLiterals GetRelevantLabels()
- {
- Z3SafeLabeledLiterals safeLiterals = new Z3SafeLabeledLiterals(z3.GetRelevantLabels());
- log("get-relevant-labels");
- return safeLiterals;
- }
-
- public Z3TermAst Make(string op, List<Z3TermAst> children)
- {
- Term[] unwrapChildren = Unwrap(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;
- }
- Z3TypeSafeTerm typeSafeTerm = Wrap(term);
- return typeSafeTerm;
- }
-
- private FuncDecl GetFunction(string functionName)
- {
- Z3TypeSafeConstDecl function;
- if (!functions.TryGetValue(functionName, out function))
- throw new Exception("function " + functionName + " is undefined");
- FuncDecl unwrapFunction = Unwrap(function);
- return unwrapFunction;
- }
-
- public Z3TermAst MakeArraySelect(List<Z3TermAst> args)
- {
- Term[] unwrapChildren = Unwrap(args).ToArray();
- return Wrap(z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]));
- }
-
- public Z3TermAst MakeArrayStore(List<Z3TermAst> args)
- {
- 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 b8aa607f..b129b378 100644 --- a/Source/Provers/Z3api/StubContext.cs +++ b/Source/Provers/Z3api/StubContext.cs @@ -45,6 +45,9 @@ namespace Microsoft.Boogie.Z3 { public Z3TermAst MakeIntLiteral(string numeral) {
return new Z3StubTermAst();
}
+ public Z3TermAst MakeBvLiteral(int i, uint bvSize) {
+ return new Z3StubTermAst();
+ }
public Z3TermAst MakeTrue() {
return new Z3StubTermAst();
}
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index 009a6a59..de5ebd8f 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -65,9 +65,21 @@ namespace Microsoft.Boogie.Z3 }
}
- private Dictionary<MapType, Z3Type> mapTypes = new Dictionary<MapType, Z3Type>(new MapTypeComparator());
- private Dictionary<BvType, Z3Type> bvTypes = new Dictionary<BvType, Z3Type>(new BvTypeComparator());
- private Dictionary<BasicType, Z3Type> basicTypes = new Dictionary<BasicType, Z3Type>(new BasicTypeComparator());
+ private class CtorTypeComparator : IEqualityComparer<CtorType> {
+ public bool Equals(CtorType x, CtorType y) {
+ return (x.Decl.Name == y.Decl.Name);
+ }
+
+ public int GetHashCode(CtorType ctorType) {
+ return ctorType.Decl.Name.GetHashCode();
+ }
+ }
+
+ private Dictionary<MapType, Sort> mapTypes = new Dictionary<MapType, Sort>(new MapTypeComparator());
+ private Dictionary<BvType, Sort> bvTypes = new Dictionary<BvType, Sort>(new BvTypeComparator());
+ private Dictionary<BasicType, Sort> basicTypes = new Dictionary<BasicType, Sort>(new BasicTypeComparator());
+ private Dictionary<CtorType, Sort> ctorTypes = new Dictionary<CtorType, Sort>(new CtorTypeComparator());
+
private Z3Context container;
public Z3TypeCachedBuilder(Z3Context context)
@@ -75,83 +87,91 @@ namespace Microsoft.Boogie.Z3 this.container = context;
}
- private Z3Type GetMapType(MapType mapType)
+ private Sort GetMapType(MapType mapType)
{
- Context z3 = ((Z3SafeContext)container).z3;
+ Context z3 = ((Z3Context)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);
+ Sort domain = GetType(mapType.Arguments[0]);
+ Sort range = GetType(mapType.Result);
+ Sort typeAst = BuildMapType(domain, range);
mapTypes.Add(mapType, typeAst);
}
- Z3Type result;
+ Sort result;
bool containsKey = mapTypes.TryGetValue(mapType, out result);
Debug.Assert(containsKey);
return result;
}
- private Z3Type GetBvType(BvType bvType)
+ private Sort GetBvType(BvType bvType)
{
if (!bvTypes.ContainsKey(bvType))
{
- Z3Type typeAst = BuildBvType(bvType);
+ Sort typeAst = BuildBvType(bvType);
bvTypes.Add(bvType, typeAst);
}
- Z3Type result;
+ Sort result;
bool containsKey = bvTypes.TryGetValue(bvType, out result);
Debug.Assert(containsKey);
return result;
}
- private Z3Type GetBasicType(BasicType basicType)
+ private Sort GetBasicType(BasicType basicType)
{
if (!basicTypes.ContainsKey(basicType))
{
- Z3Type typeAst = BuildBasicType(basicType);
+ Sort typeAst = BuildBasicType(basicType);
basicTypes.Add(basicType, typeAst);
}
- Z3Type result;
+ Sort result;
bool containsKey = basicTypes.TryGetValue(basicType, out result);
Debug.Assert(containsKey);
return result;
}
- public virtual Z3Type GetType(Type boogieType)
- {
- if (boogieType.GetType().Equals(typeof(BvType)))
- 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");
+ private Sort GetCtorType(CtorType ctorType) {
+ if (!ctorTypes.ContainsKey(ctorType)) {
+ Sort typeAst = BuildCtorType(ctorType);
+ ctorTypes.Add(ctorType, typeAst);
+ }
+ Sort result;
+ bool containsKey = ctorTypes.TryGetValue(ctorType, out result);
+ Debug.Assert(containsKey);
+ return result;
}
- private Z3Type WrapType(Sort typeAst)
- {
- return new Z3SafeType(typeAst);
+ public virtual Sort GetType(Type boogieType) {
+ System.Type type = boogieType.GetType();
+ if (type.Equals(typeof(BvType)))
+ return GetBvType((BvType)boogieType);
+ else if (type.Equals(typeof(BasicType)))
+ return GetBasicType((BasicType)boogieType);
+ else if (type.Equals(typeof(MapType)))
+ return GetMapType((MapType)boogieType);
+ else if (type.Equals(typeof(CtorType)))
+ return GetCtorType((CtorType)boogieType);
+ else
+ throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
}
- public Z3Type BuildMapType(Z3Type domain, Z3Type range)
+ public Sort BuildMapType(Sort domain, Sort range)
{
- Context z3 = ((Z3SafeContext)container).z3;
- Sort typeAst = z3.MkArraySort(((Z3SafeType)domain).TypeAst, ((Z3SafeType)range).TypeAst);
- return WrapType(typeAst);
+ Context z3 = ((Z3Context)container).z3;
+ Sort typeAst = z3.MkArraySort(domain, range);
+ return typeAst;
}
- public Z3Type BuildBvType(BvType bvType)
+ public Sort BuildBvType(BvType bvType)
{
- Context z3 = ((Z3SafeContext)container).z3;
+ Context z3 = ((Z3Context)container).z3;
Sort typeAst = z3.MkBvSort((uint)bvType.Bits);
- return WrapType(typeAst);
+ return typeAst;
}
- public Z3Type BuildBasicType(BasicType basicType)
+ public Sort BuildBasicType(BasicType basicType)
{
- Context z3 = ((Z3SafeContext)container).z3;
+ Context z3 = ((Z3Context)container).z3;
Sort typeAst;
if (basicType.IsBool)
{
@@ -163,9 +183,16 @@ namespace Microsoft.Boogie.Z3 }
else
throw new Exception("Unknown Basic Type " + basicType.ToString());
- return WrapType(typeAst);
+ return typeAst;
}
- }
- public class Z3Type { }
+ 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;
+ }
+ }
}
\ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index c2eeb45f..aa47d7e0 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -11,13 +11,14 @@ using System.Collections.Generic; using System.Diagnostics.Contracts;
using Microsoft.Basetypes;
using Microsoft.Boogie.VCExprAST;
+using Microsoft.Z3;
namespace Microsoft.Boogie.Z3
{
- public class Z3apiExprLineariser : IVCExprVisitor<Z3TermAst, LineariserOptions>
+ public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>
{
private Z3apiOpLineariser OpLinObject = null;
- private IVCExprOpVisitor<Z3TermAst, LineariserOptions> OpLineariser
+ private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser
{
get
{
@@ -29,36 +30,36 @@ namespace Microsoft.Boogie.Z3 }
internal readonly UniqueNamer namer;
- internal readonly Dictionary<VCExprVar, Z3TermAst> letBindings;
+ internal readonly Dictionary<VCExprVar, Term> letBindings;
protected Z3Context cm;
public Z3apiExprLineariser(Z3Context cm, UniqueNamer namer)
{
this.cm = cm;
this.namer = namer;
- this.letBindings = new Dictionary<VCExprVar, Z3TermAst>();
+ this.letBindings = new Dictionary<VCExprVar, Term>();
}
- public Z3TermAst Linearise(VCExpr expr, LineariserOptions options)
+ public Term Linearise(VCExpr expr, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(expr != null);
- return expr.Accept<Z3TermAst, LineariserOptions>(this, options);
+ return expr.Accept<Term, LineariserOptions>(this, options);
}
/////////////////////////////////////////////////////////////////////////////////////
- public Z3TermAst Visit(VCExprLiteral node, LineariserOptions options)
+ public Term Visit(VCExprLiteral node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
if (node == VCExpressionGenerator.True)
- return cm.MakeTrue();
+ return cm.z3.MkTrue();
else if (node == VCExpressionGenerator.False)
- return cm.MakeFalse();
+ return cm.z3.MkFalse();
else if (node is VCExprIntLit)
- return cm.MakeIntLiteral(((VCExprIntLit)node).Val.ToString());
+ return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());
else
{
Contract.Assert(false);
@@ -66,7 +67,7 @@ namespace Microsoft.Boogie.Z3 }
}
- public Z3TermAst Visit(VCExprNAry node, LineariserOptions options)
+ public Term Visit(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -76,7 +77,7 @@ namespace Microsoft.Boogie.Z3 if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))
{
// handle these operators without recursion
- List<Z3TermAst> asts = new List<Z3TermAst>();
+ List<Term> asts = new List<Term>();
string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR";
IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
@@ -93,10 +94,10 @@ namespace Microsoft.Boogie.Z3 return cm.Make(opString, asts);
}
- return node.Accept<Z3TermAst, LineariserOptions>(OpLineariser, options);
+ return node.Accept<Term, LineariserOptions>(OpLineariser, options);
}
- public Z3TermAst Visit(VCExprVar node, LineariserOptions options)
+ public Term Visit(VCExprVar node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -111,7 +112,7 @@ namespace Microsoft.Boogie.Z3 }
}
- public Z3TermAst Visit(VCExprQuantifier node, LineariserOptions options)
+ public Term Visit(VCExprQuantifier node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -123,11 +124,11 @@ namespace Microsoft.Boogie.Z3 List<string> varNames;
List<Type> varTypes;
VisitBounds(node.BoundVars, out varNames, out varTypes);
- List<Z3PatternAst> patterns;
- List<Z3TermAst> no_patterns;
+ List<Pattern> patterns;
+ List<Term> no_patterns;
VisitTriggers(node.Triggers, options, out patterns, out no_patterns);
- Z3TermAst body = Linearise(node.Body, options);
- Z3TermAst result;
+ Term body = Linearise(node.Body, options);
+ Term result;
uint weight = 1;
string qid = "";
int skolemid = 0;
@@ -153,9 +154,9 @@ namespace Microsoft.Boogie.Z3 switch (node.Quan)
{
- case Quantifier.ALL:
+ case Microsoft.Boogie.VCExprAST.Quantifier.ALL:
result = cm.MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
- case Quantifier.EX:
+ case Microsoft.Boogie.VCExprAST.Quantifier.EX:
result = cm.MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
default:
throw new Exception("unknown quantifier kind " + node.Quan);
@@ -180,44 +181,44 @@ namespace Microsoft.Boogie.Z3 }
}
- private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Z3PatternAst> patterns, out List<Z3TermAst> no_patterns)
+ private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Pattern> patterns, out List<Term> no_patterns)
{
- patterns = new List<Z3PatternAst>();
- no_patterns = new List<Z3TermAst>();
+ patterns = new List<Pattern>();
+ no_patterns = new List<Term>();
foreach (VCTrigger trigger in triggers)
{
- List<Z3TermAst> exprs = new List<Z3TermAst>();
+ List<Term> exprs = new List<Term>();
foreach (VCExpr expr in trigger.Exprs)
{
System.Diagnostics.Debug.Assert(expr != null);
- Z3TermAst termAst = Linearise(expr, options);
+ Term termAst = Linearise(expr, options);
exprs.Add(termAst);
}
if (exprs.Count > 0)
{
if (trigger.Pos)
{
- Z3PatternAst pattern = cm.MakePattern(exprs);
+ Pattern pattern = cm.MakePattern(exprs);
patterns.Add(pattern);
}
else
{
System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats");
- foreach (Z3TermAst expr in exprs)
+ foreach (Term expr in exprs)
no_patterns.Add(expr);
}
}
}
}
- public Z3TermAst Visit(VCExprLet node, LineariserOptions options)
+ public Term Visit(VCExprLet node, LineariserOptions options)
{
foreach (VCExprLetBinding b in node)
{
- Z3TermAst defAst = Linearise(b.E, options);
+ Term defAst = Linearise(b.E, options);
letBindings.Add(b.V, defAst);
}
- Z3TermAst letAst = Linearise(node.Body, options);
+ Term letAst = Linearise(node.Body, options);
foreach (VCExprLetBinding b in node)
{
letBindings.Remove(b.V);
@@ -227,7 +228,7 @@ namespace Microsoft.Boogie.Z3 /////////////////////////////////////////////////////////////////////////////////////
- internal class Z3apiOpLineariser : IVCExprOpVisitor<Z3TermAst, LineariserOptions>
+ internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions>
{
[ContractInvariantMethod]
void ObjectInvariant()
@@ -245,13 +246,13 @@ namespace Microsoft.Boogie.Z3 ///////////////////////////////////////////////////////////////////////////////////
- private Z3TermAst WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)
+ private Term WriteApplication(string op, IEnumerable<VCExpr> terms, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(op != null);
Contract.Requires(cce.NonNullElements(terms));
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in terms)
{
Contract.Assert(e != null);
@@ -262,51 +263,51 @@ namespace Microsoft.Boogie.Z3 ///////////////////////////////////////////////////////////////////////////////////
- public Z3TermAst VisitNotOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitNotOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("NOT", node, options);
}
- public Z3TermAst VisitEqOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitEqOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("EQ", node, options);
}
- public Z3TermAst VisitNeqOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("NEQ", node, options);
}
- public Z3TermAst VisitAndOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitAndOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("AND", node, options);
}
- public Z3TermAst VisitOrOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitOrOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("OR", node, options);
}
- public Z3TermAst VisitImpliesOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
if (options.InverseImplies)
{
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
args.Add(ExprLineariser.Linearise(node[1], options));
- List<Z3TermAst> t = new List<Z3TermAst>();
+ List<Term> t = new List<Term>();
t.Add(ExprLineariser.Linearise(node[0], options));
args.Add(ExprLineariser.cm.Make("NOT", t));
return ExprLineariser.cm.Make("OR", args);
@@ -317,7 +318,7 @@ namespace Microsoft.Boogie.Z3 }
}
- public Z3TermAst VisitDistinctOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -328,7 +329,7 @@ namespace Microsoft.Boogie.Z3 }
else
{
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in node)
{
Contract.Assert(e != null);
@@ -338,7 +339,7 @@ namespace Microsoft.Boogie.Z3 }
}
- public Z3TermAst VisitLabelOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -347,73 +348,103 @@ namespace Microsoft.Boogie.Z3 return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options));
}
- public Z3TermAst VisitSelectOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitSelectOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in node)
{
Contract.Assert(e != null);
args.Add(ExprLineariser.Linearise(e, options));
}
- return ExprLineariser.cm.MakeArraySelect(args);
+
+ Term[] unwrapChildren = args.ToArray();
+ return ExprLineariser.cm.z3.MkArraySelect(unwrapChildren[0], unwrapChildren[1]);
// return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.SelectOpName(node), args);
}
- public Z3TermAst VisitStoreOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in node)
{
Contract.Assert(e != null);
args.Add(ExprLineariser.Linearise(e, options));
}
- return ExprLineariser.cm.MakeArrayStore(args);
+
+ Term[] unwrapChildren = args.ToArray();
+ return ExprLineariser.cm.z3.MkArrayStore(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);
// return ExprLineariser.cm.Make(SimplifyLikeExprLineariser.StoreOpName(node), args);
}
- public Z3TermAst VisitBvOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitBvOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- return WriteApplication("$make_bv" + node.Type.BvBits, node, options);
+ List<int> args = new List<int>();
+ foreach (VCExpr e in node) {
+ VCExprIntLit literal = e as VCExprIntLit;
+ System.Diagnostics.Debug.Assert(literal != null);
+ args.Add(literal.Val.ToInt);
+ }
+ System.Diagnostics.Debug.Assert(args.Count == 1);
+ return ExprLineariser.cm.z3.MkNumeral(args[0], ExprLineariser.cm.z3.MkBvSort((uint)node.Type.BvBits));
}
- public Z3TermAst VisitBvExtractOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(SimplifyLikeExprLineariser.BvExtractOpName(node), node, options);
+ public Term VisitBvExtractOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+
+ VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op;
+ Contract.Assert(op != null);
+ System.Diagnostics.Debug.Assert(0 <= op.Start && op.Start < op.End);
+
+ List<Term> args = new List<Term>();
+ foreach (VCExpr e in node) {
+ Contract.Assert(e != null);
+ args.Add(ExprLineariser.Linearise(e, options));
+ }
+ System.Diagnostics.Debug.Assert(args.Count == 1);
+ return ExprLineariser.cm.z3.MkBvExtract((uint) op.End - 1, (uint) op.Start, args[0]);
}
- public Z3TermAst VisitBvConcatOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(SimplifyLikeExprLineariser.BvConcatOpName(node), node, options);
+ public Term VisitBvConcatOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+
+ VCExprBvConcatOp op = (VCExprBvConcatOp)node.Op;
+ Contract.Assert(op != null);
+
+ List<Term> args = new List<Term>();
+ foreach (VCExpr e in node) {
+ Contract.Assert(e != null);
+ args.Add(ExprLineariser.Linearise(e, options));
+ }
+ System.Diagnostics.Debug.Assert(args.Count == 2);
+ return ExprLineariser.cm.z3.MkBvConcat(args[0], args[1]);
}
- public Z3TermAst VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
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);
}
- public Z3TermAst VisitCustomOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(node != null);
Contract.Requires(options != null);
VCExprCustomOp op = (VCExprCustomOp)node.Op;
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr arg in node)
{
args.Add(ExprLineariser.Linearise(arg, options));
@@ -421,7 +452,7 @@ namespace Microsoft.Boogie.Z3 return ExprLineariser.cm.Make(op.Name, args);
}
- public Z3TermAst VisitAddOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitAddOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -435,77 +466,77 @@ namespace Microsoft.Boogie.Z3 }
}
- public Z3TermAst VisitSubOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitSubOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("-", node, options);
}
- public Z3TermAst VisitMulOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitMulOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("*", node, options);
}
- public Z3TermAst VisitDivOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitDivOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("/", node, options);
}
- public Z3TermAst VisitModOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitModOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("%", node, options);
}
- public Z3TermAst VisitLtOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitLtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("<", node, options);
}
- public Z3TermAst VisitLeOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitLeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("<=", node, options);
}
- public Z3TermAst VisitGtOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitGtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication(">", node, options);
}
- public Z3TermAst VisitGeOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitGeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication(">=", node, options);
}
- public Z3TermAst VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("<:", node, options);
}
- public Z3TermAst VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
+ public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
return WriteApplication("<::", node, options);
}
- public Z3TermAst VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
+ public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
Contract.Requires(node != null);
@@ -516,7 +547,7 @@ namespace Microsoft.Boogie.Z3 string bvzName = op.Func.FindStringAttribute("external");
if (bvzName != null) funcName = bvzName;
- List<Z3TermAst> args = new List<Z3TermAst>();
+ List<Term> args = new List<Term>();
foreach (VCExpr e in node)
{
Contract.Assert(e != null);
diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index 05cc8f9f..e02243ce 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -169,8 +169,6 @@ </Compile>
<Compile Include="ContextLayer.cs" />
<Compile Include="ProverLayer.cs" />
- <Compile Include="SafeContext.cs" />
- <Compile Include="StubContext.cs" />
<Compile Include="TypeAdapter.cs">
<SubType>Code</SubType>
</Compile>
diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs index 85ceb8e3..0b76387d 100644 --- a/Source/VCGeneration/StratifiedVC.cs +++ b/Source/VCGeneration/StratifiedVC.cs @@ -2485,6 +2485,39 @@ namespace VC }
}
+ public override Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
+ {
+ // Construct the set of inlined procs in the original program
+ var inlinedProcs = new HashSet<string>();
+ foreach (var decl in program.TopLevelDeclarations)
+ {
+ // Implementations
+ if (decl is Implementation)
+ {
+ var impl = decl as Implementation;
+ if (!(impl.Proc is LoopProcedure))
+ {
+ inlinedProcs.Add(impl.Name);
+ }
+ }
+
+ // And recording procedures
+ if (decl is Procedure)
+ {
+ var proc = decl as Procedure;
+ if (proc.Name.StartsWith(recordProcName))
+ {
+ Debug.Assert(!(decl is LoopProcedure));
+ inlinedProcs.Add(proc.Name);
+ }
+ }
+ }
+
+ return extractLoopTraceRec(
+ new CalleeCounterexampleInfo(cex, new List<object>()),
+ mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
+ }
+
protected override bool elIsLoop(string procname)
{
LazyInliningInfo info = null;
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 11db59b0..7c981a0c 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -2463,18 +2463,18 @@ namespace VC { }
}
- public Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
+ public virtual Counterexample extractLoopTrace(Counterexample cex, string mainProcName, Program program, Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
{
// Construct the set of inlined procs in the original program
- var inlinedProcs = new Dictionary<string, Procedure>();
+ var inlinedProcs = new HashSet<string>();
foreach (var decl in program.TopLevelDeclarations)
{
if (decl is Procedure)
- {
+ {
if (!(decl is LoopProcedure))
{
var p = decl as Procedure;
- inlinedProcs.Add(p.Name, p);
+ inlinedProcs.Add(p.Name);
}
}
}
@@ -2484,9 +2484,9 @@ namespace VC { mainProcName, inlinedProcs, extractLoopMappingInfo).counterexample;
}
- private CalleeCounterexampleInfo extractLoopTraceRec(
+ protected CalleeCounterexampleInfo extractLoopTraceRec(
CalleeCounterexampleInfo cexInfo, string currProc,
- Dictionary<string, Procedure> inlinedProcs,
+ HashSet<string> inlinedProcs,
Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo)
{
Contract.Requires(currProc != null);
@@ -2507,7 +2507,11 @@ namespace VC { for (int numInstr = 0; numInstr < block.Cmds.Length; numInstr ++) {
Cmd cmd = block.Cmds[numInstr];
var loc = new TraceLocation(numBlock, numInstr);
- if (!cex.calleeCounterexamples.ContainsKey(loc)) continue;
+ if (!cex.calleeCounterexamples.ContainsKey(loc))
+ {
+ if (getCallee(cex.getTraceCmd(loc), inlinedProcs) != null) callCnt++;
+ continue;
+ }
string callee = cex.getCalledProcName(cex.getTraceCmd(loc));
Contract.Assert(callee != null);
var calleeTrace = cex.calleeCounterexamples[loc];
@@ -2543,33 +2547,13 @@ namespace VC { // return the position of the i^th CallCmd in the block (count only those Calls that call a procedure in inlinedProcs).
// Assert failure if there isn't any.
// Assert that the CallCmd found calls "callee"
- private int getCallCmdPosition(Block block, int i, Dictionary<string, Procedure> inlinedProcs, string callee)
+ private int getCallCmdPosition(Block block, int i, HashSet<string> inlinedProcs, string callee)
{
Debug.Assert(i >= 1);
for (int pos = 0; pos < block.Cmds.Length; pos++)
{
Cmd cmd = block.Cmds[pos];
- string procCalled = null;
- if (cmd is CallCmd)
- {
- var cc = (CallCmd)cmd;
- if (inlinedProcs.ContainsKey(cc.Proc.Name))
- {
- procCalled = cc.Proc.Name;
- }
- }
-
- if (cmd is AssumeCmd)
- {
- var expr = (cmd as AssumeCmd).Expr as NAryExpr;
- if (expr != null)
- {
- if (inlinedProcs.ContainsKey(expr.Fun.FunctionName))
- {
- procCalled = expr.Fun.FunctionName;
- }
- }
- }
+ string procCalled = getCallee(cmd, inlinedProcs);
if (procCalled != null)
{
@@ -2586,6 +2570,32 @@ namespace VC { return -1;
}
+ private string getCallee(Cmd cmd, HashSet<string> inlinedProcs)
+ {
+ string procCalled = null;
+ if (cmd is CallCmd)
+ {
+ var cc = (CallCmd)cmd;
+ if (inlinedProcs.Contains(cc.Proc.Name))
+ {
+ procCalled = cc.Proc.Name;
+ }
+ }
+
+ if (cmd is AssumeCmd)
+ {
+ var expr = (cmd as AssumeCmd).Expr as NAryExpr;
+ if (expr != null)
+ {
+ if (inlinedProcs.Contains(expr.Fun.FunctionName))
+ {
+ procCalled = expr.Fun.FunctionName;
+ }
+ }
+ }
+ return procCalled;
+ }
+
protected virtual bool elIsLoop(string procname)
{
Contract.Requires(procname != null);
diff --git a/Test/z3api/Boog24.bpl b/Test/z3api/Boog24.bpl index c5e2eea6..d3da775d 100644 --- a/Test/z3api/Boog24.bpl +++ b/Test/z3api/Boog24.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(a:bool) returns (int);
axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);
diff --git a/Test/z3api/boog0.bpl b/Test/z3api/boog0.bpl index 1b9bee36..4206152b 100644 --- a/Test/z3api/boog0.bpl +++ b/Test/z3api/boog0.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
const w: Wicket;
var favorite: Wicket;
@@ -6,7 +7,7 @@ function age(Wicket) returns (int); axiom age(w)==7;
procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite;
ensures favorite==p;
@@ -19,7 +20,7 @@ const myRef: ref; const v: Wicket;
axiom 7 < 8;
-axiom 7 <= 8;
+axiom 7 <= 8;
axiom 8 > 7;
axiom 8 >= 7;
axiom 6 != 7;
@@ -37,7 +38,7 @@ axiom ((7==7) && (8==8)); var favorite2: Wicket;
procedure SwapFavorites()
- modifies favorite,favorite2
;
+ modifies favorite,favorite2;
ensures (favorite==old(favorite2)) && (favorite2==old(favorite));
{
diff --git a/Test/z3api/boog1.bpl b/Test/z3api/boog1.bpl index 6b6cce75..9f4d2349 100644 --- a/Test/z3api/boog1.bpl +++ b/Test/z3api/boog1.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
const w: Wicket;
var favorite: Wicket;
@@ -7,7 +8,8 @@ function age(Wicket) returns (int); axiom age(w)==7;
procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog10.bpl b/Test/z3api/boog10.bpl index 5ac43287..075432d7 100644 --- a/Test/z3api/boog10.bpl +++ b/Test/z3api/boog10.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Color;
const unique red: Color;
@@ -9,7 +10,8 @@ var myColor: Color; // procedure
procedure SetTo(c: Color);
- modifies myColor
;
+ modifies myColor
+;
ensures myColor==c;
diff --git a/Test/z3api/boog11.bpl b/Test/z3api/boog11.bpl index e66802ea..5b83de6a 100644 --- a/Test/z3api/boog11.bpl +++ b/Test/z3api/boog11.bpl @@ -1,10 +1,12 @@ +type ref;
// types
const top: ref;
var myRef: ref;
// procedure
procedure SetTo(r: ref);
- modifies myRef
;
+ modifies myRef
+;
ensures myRef==r;
diff --git a/Test/z3api/boog12.bpl b/Test/z3api/boog12.bpl index d20a8f35..c277a674 100644 --- a/Test/z3api/boog12.bpl +++ b/Test/z3api/boog12.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Color;
const blue: Color;
@@ -7,7 +8,8 @@ var myMatrix:[int,int] Color; // procedure
procedure SetTo(c: Color);
- modifies myArray, myMatrix
;
+ modifies myArray, myMatrix
+;
ensures myArray[0]==c;
diff --git a/Test/z3api/boog13.bpl b/Test/z3api/boog13.bpl index a4f854f5..9cd873c6 100644 --- a/Test/z3api/boog13.bpl +++ b/Test/z3api/boog13.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
var favorite: Wicket;
@@ -6,14 +7,16 @@ var v: Wicket; function age(w:Wicket) returns (int);
axiom (exists v:Wicket :: age(v)<8 &&
- (forall v:Wicket
:: age(v)==7)
+ (forall v:Wicket
+ :: age(v)==7)
);
// procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog14.bpl b/Test/z3api/boog14.bpl index c163ed18..41450d85 100644 --- a/Test/z3api/boog14.bpl +++ b/Test/z3api/boog14.bpl @@ -1,3 +1,4 @@ +type ref;
function choose(a:bool, b:int, c:int) returns (x:int);
axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b);
diff --git a/Test/z3api/boog15.bpl b/Test/z3api/boog15.bpl index ef792b2b..428c0f6e 100644 --- a/Test/z3api/boog15.bpl +++ b/Test/z3api/boog15.bpl @@ -1,3 +1,4 @@ +type ref;
function AtLeast(int, int) returns ([int]bool);
axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);
diff --git a/Test/z3api/boog16.bpl b/Test/z3api/boog16.bpl index 48afd41d..a002c166 100644 --- a/Test/z3api/boog16.bpl +++ b/Test/z3api/boog16.bpl @@ -1,3 +1,4 @@ +type ref;
function choose(a:bool, b:int, c:int) returns (x:int);
axiom(forall a:bool, b:int, c:int ::
{choose(a,b,c)} !a ==> choose(a,b,c) == c);
diff --git a/Test/z3api/boog17.bpl b/Test/z3api/boog17.bpl index 6f886f49..89159af1 100644 --- a/Test/z3api/boog17.bpl +++ b/Test/z3api/boog17.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
const unique g : int;
axiom(g != 0);
diff --git a/Test/z3api/boog18.bpl b/Test/z3api/boog18.bpl index fe0cbc10..35f7d48a 100644 --- a/Test/z3api/boog18.bpl +++ b/Test/z3api/boog18.bpl @@ -1,3 +1,4 @@ +type ref;
const A100INT4_name:int;
function Match(a:int, t:int) returns (int);
diff --git a/Test/z3api/boog19.bpl b/Test/z3api/boog19.bpl index 17b199dd..178bb04f 100644 --- a/Test/z3api/boog19.bpl +++ b/Test/z3api/boog19.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
var alloc:[int]name;
diff --git a/Test/z3api/boog2.bpl b/Test/z3api/boog2.bpl index 74c05a28..315c51af 100644 --- a/Test/z3api/boog2.bpl +++ b/Test/z3api/boog2.bpl @@ -1,10 +1,12 @@ +type ref;
type Wicket;
var favorite: Wicket;
var hate: Wicket;
procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog20.bpl b/Test/z3api/boog20.bpl index fa714972..10181400 100644 --- a/Test/z3api/boog20.bpl +++ b/Test/z3api/boog20.bpl @@ -1,3 +1,4 @@ +type ref;
function PLUS(int, int, int) returns (int);
function Rep(int, int) returns (int);
diff --git a/Test/z3api/boog21.bpl b/Test/z3api/boog21.bpl index 1f4fa6dc..8e3abde7 100644 --- a/Test/z3api/boog21.bpl +++ b/Test/z3api/boog21.bpl @@ -1,3 +1,4 @@ +type ref;
function PLUS(int, int, int) returns (int);
function Rep(int,int) returns (int);
@@ -5,7 +6,8 @@ function Rep(int,int) returns (int); // ERROR
-axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z
));
+axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z
+));
axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) == x));
// END ERROR
diff --git a/Test/z3api/boog22.bpl b/Test/z3api/boog22.bpl index 95e45849..c255a3c5 100644 --- a/Test/z3api/boog22.bpl +++ b/Test/z3api/boog22.bpl @@ -1,3 +1,4 @@ +type ref;
type W;
function f1(W,int) returns (int);
diff --git a/Test/z3api/boog23.bpl b/Test/z3api/boog23.bpl index 41c68790..4e0fc4d0 100644 --- a/Test/z3api/boog23.bpl +++ b/Test/z3api/boog23.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
type byte;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/z3api/boog25.bpl b/Test/z3api/boog25.bpl index 0a8b5e92..0ee4163c 100644 --- a/Test/z3api/boog25.bpl +++ b/Test/z3api/boog25.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
type byte;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/z3api/boog28.bpl b/Test/z3api/boog28.bpl index 989dbf75..ab7f4ad2 100644 --- a/Test/z3api/boog28.bpl +++ b/Test/z3api/boog28.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(x:bool) returns (int);
axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
diff --git a/Test/z3api/boog29.bpl b/Test/z3api/boog29.bpl index 8a97944d..035e69fd 100644 --- a/Test/z3api/boog29.bpl +++ b/Test/z3api/boog29.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(x:bool) returns (int);
axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
diff --git a/Test/z3api/boog3.bpl b/Test/z3api/boog3.bpl index 9e04ac5b..207ddbd0 100644 --- a/Test/z3api/boog3.bpl +++ b/Test/z3api/boog3.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
procedure Dummy();
diff --git a/Test/z3api/boog30.bpl b/Test/z3api/boog30.bpl index ae682156..81e04f20 100644 --- a/Test/z3api/boog30.bpl +++ b/Test/z3api/boog30.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(x:bool) returns (int);
axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
diff --git a/Test/z3api/boog31.bpl b/Test/z3api/boog31.bpl index 219effce..86386a90 100644 --- a/Test/z3api/boog31.bpl +++ b/Test/z3api/boog31.bpl @@ -1,3 +1,4 @@ +type ref;
const b1:bool;
const b2:bool;
diff --git a/Test/z3api/boog34.bpl b/Test/z3api/boog34.bpl index 62e7e82b..88a587aa 100644 --- a/Test/z3api/boog34.bpl +++ b/Test/z3api/boog34.bpl @@ -1,3 +1,4 @@ +type ref;
function Rep(int, int) returns (int);
axiom(forall n:int, x:int :: {Rep(n,x)}
diff --git a/Test/z3api/boog4.bpl b/Test/z3api/boog4.bpl index 46eda549..95ec7011 100644 --- a/Test/z3api/boog4.bpl +++ b/Test/z3api/boog4.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
const w: Wicket;
@@ -10,7 +11,8 @@ function age(Wicket) returns (int); axiom age(w)==7;
axiom 7 < 8;
-axiom 7 <= 8;
+axiom 7 <= 8;
+
axiom 8 > 7;
axiom 8 >= 7;
axiom 6 != 7;
@@ -28,7 +30,8 @@ axiom 7!=7; procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog5.bpl b/Test/z3api/boog5.bpl index 0db94bba..4b76fd22 100644 --- a/Test/z3api/boog5.bpl +++ b/Test/z3api/boog5.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
@@ -23,7 +24,8 @@ axiom age(x)==4; // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
@@ -32,7 +34,8 @@ implementation SetToSeven(l: Wicket) { favorite:=l;
} else {
favorite:=v;
- }
+ }
+
}
diff --git a/Test/z3api/boog6.bpl b/Test/z3api/boog6.bpl index 55c1dc7e..f6c3c23f 100644 --- a/Test/z3api/boog6.bpl +++ b/Test/z3api/boog6.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
@@ -10,7 +11,8 @@ axiom b==true; // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog7.bpl b/Test/z3api/boog7.bpl index 36f952d1..78e5e3e6 100644 --- a/Test/z3api/boog7.bpl +++ b/Test/z3api/boog7.bpl @@ -1,3 +1,4 @@ +type ref;
// consts
const w: int;
@@ -7,7 +8,8 @@ var favorite: int; // procedure
procedure SetToSeven(p: int);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog8.bpl b/Test/z3api/boog8.bpl index 0ac4f163..121f27cf 100644 --- a/Test/z3api/boog8.bpl +++ b/Test/z3api/boog8.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
var favorite: Wicket;
@@ -12,7 +13,8 @@ axiom myBool==true; // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog9.bpl b/Test/z3api/boog9.bpl index 55897a1d..3bd6ff63 100644 --- a/Test/z3api/boog9.bpl +++ b/Test/z3api/boog9.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
var favorite: Wicket;
@@ -9,7 +10,8 @@ axiom (exists v:Wicket :: age(v)<8); // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat index 5daa36c0..e9bc968e 100644 --- a/Test/z3api/runtest.bat +++ b/Test/z3api/runtest.bat @@ -3,8 +3,15 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (
+for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog14.bpl boog16.bpl boog17.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /prover:z3api %%f
+ %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f
)
+
+REM boog12.bpl
+REM boog15.bpl
+
+REM boog19.bpl
+REM boog23.bpl
+REM boog25.bpl
\ No newline at end of file |