diff options
| author |  Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-06-23 20:29:14 +0530 |
|---|---|---|
| committer | Unknown <akashl@MSRI-Akashlal.fareast.corp.microsoft.com> | 2011-06-23 20:29:14 +0530 |
| commit | 2b30cf9c15df211baf5e4371b3134363d6b598f0 (patch) | |
| tree | c71b0bd20554e0f67392c9e37d3da5d64bc1a714 | |
| parent | 1036f1a10fc08338adf55c899615e5836602227f (diff) | |
| parent | 2b81b9d7e787409913f4c0488c0b3310a4e9e5a0 (diff) | |
Bug fix for trace generation with extractLoop option
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 4 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 499 | ||||
| -rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 26 | ||||
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 636 | ||||
| -rw-r--r-- | Source/Provers/Z3api/StubContext.cs | 3 | ||||
| -rw-r--r-- | Source/Provers/Z3api/TypeAdapter.cs | 73 | ||||
| -rw-r--r-- | Source/Provers/Z3api/VCExprVisitor.cs | 191 | ||||
| -rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 2 | ||||
| -rw-r--r-- | Test/z3api/runtest.bat | 7 |
9 files changed, 599 insertions, 842 deletions
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index af0926fe..ec28a910 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -192,6 +192,10 @@ <Project>{A598ED5A-93AD-4125-A555-3921A2F936FA}</Project>
<Name>TPTP</Name>
</ProjectReference>
+ <ProjectReference Include="..\Provers\Z3api\Z3api.csproj">
+ <Project>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</Project>
+ <Name>Z3api</Name>
+ </ProjectReference>
<ProjectReference Include="..\Provers\Z3\Z3.csproj">
<Project>{BB49B90B-BE21-4BE8-85BA-359FDB55F4DF}</Project>
<Name>Z3</Name>
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index e6ba7b66..ed45c4fc 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -69,38 +69,6 @@ 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;
@@ -138,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 (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.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,7 +225,7 @@ namespace Microsoft.Boogie.Z3 public BoogieErrorModelBuilder(Z3Context container, Model z3Model)
{
this.container = container;
- this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3, z3Model);
+ this.partitionMap = new PartitionMap(((Z3Context)container).z3, z3Model);
}
private Dictionary<string, int> CreateConstantToPartition(Model z3Model)
@@ -257,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);
}
@@ -285,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)
{
@@ -310,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);
}
}
@@ -334,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 7bdc07a0..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,13 +191,13 @@ 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)
{
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index 30207e75..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, 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);
- 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 dec25e97..de5ebd8f 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -75,10 +75,10 @@ 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 Dictionary<CtorType, Z3Type> ctorTypes = new Dictionary<CtorType, Z3Type>(new CtorTypeComparator());
+ 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;
@@ -87,61 +87,61 @@ 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;
}
- private Z3Type GetCtorType(CtorType ctorType) {
+ private Sort GetCtorType(CtorType ctorType) {
if (!ctorTypes.ContainsKey(ctorType)) {
- Z3Type typeAst = BuildCtorType(ctorType);
+ Sort typeAst = BuildCtorType(ctorType);
ctorTypes.Add(ctorType, typeAst);
}
- Z3Type result;
+ Sort result;
bool containsKey = ctorTypes.TryGetValue(ctorType, out result);
Debug.Assert(containsKey);
return result;
}
- public virtual Z3Type GetType(Type boogieType) {
+ public virtual Sort GetType(Type boogieType) {
System.Type type = boogieType.GetType();
if (type.Equals(typeof(BvType)))
return GetBvType((BvType)boogieType);
@@ -155,28 +155,23 @@ namespace Microsoft.Boogie.Z3 throw new Exception("Boogie Type " + boogieType.GetType() + " is unknown");
}
- private Z3Type WrapType(Sort typeAst)
+ public Sort BuildMapType(Sort domain, Sort range)
{
- return new Z3SafeType(typeAst);
+ Context z3 = ((Z3Context)container).z3;
+ Sort typeAst = z3.MkArraySort(domain, range);
+ return typeAst;
}
- public Z3Type BuildMapType(Z3Type domain, Z3Type range)
+ public Sort BuildBvType(BvType bvType)
{
- 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;
+ 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)
{
@@ -188,18 +183,16 @@ namespace Microsoft.Boogie.Z3 }
else
throw new Exception("Unknown Basic Type " + basicType.ToString());
- return WrapType(typeAst);
+ return typeAst;
}
- public Z3Type BuildCtorType(CtorType ctorType) {
- Context z3 = ((Z3SafeContext)container).z3;
+ public Sort BuildCtorType(CtorType ctorType) {
+ Context z3 = ((Z3Context)container).z3;
Sort typeAst;
if (ctorType.Arguments.Length > 0)
throw new Exception("Type constructor of non-zero arity are not handled");
typeAst = z3.MkSort(ctorType.Decl.Name);
- return WrapType(typeAst);
+ return 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 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/Test/z3api/runtest.bat b/Test/z3api/runtest.bat index 08a27b9b..e9bc968e 100644 --- a/Test/z3api/runtest.bat +++ b/Test/z3api/runtest.bat @@ -3,17 +3,14 @@ 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 boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.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 /typeEncoding:m /prover:z3api %%f
)
-REM boog8.bpl
+
REM boog12.bpl
-REM boog14.bpl
REM boog15.bpl
-REM boog16.bpl
-REM boog17.bpl
REM boog19.bpl
REM boog23.bpl
|