diff options
Diffstat (limited to 'Source/Provers/Z3api')
-rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 1454 | ||||
-rw-r--r-- | Source/Provers/Z3api/ProverLayer.cs | 706 | ||||
-rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 30 | ||||
-rw-r--r-- | Source/Provers/Z3api/StubContext.cs | 148 | ||||
-rw-r--r-- | Source/Provers/Z3api/TypeAdapter.cs | 392 | ||||
-rw-r--r-- | Source/Provers/Z3api/VCExprVisitor.cs | 1298 | ||||
-rw-r--r-- | Source/Provers/Z3api/Z3api.csproj | 376 | ||||
-rw-r--r-- | Source/Provers/Z3api/cce.cs | 384 |
8 files changed, 2394 insertions, 2394 deletions
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index ad0c2239..87fd8c17 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -1,728 +1,728 @@ -using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Diagnostics;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Z3;
-using Microsoft.Z3;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Basetypes;
-
-using Z3Model = Microsoft.Z3.Model;
-using BoogieModel = Microsoft.Boogie.Model;
-
-namespace Microsoft.Boogie.Z3 {
- public class Z3apiProverContext : DeclFreeProverContext {
- 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>();
- internal BacktrackDictionary<Term, VCExpr> constants_inv = null;
- internal BacktrackDictionary<FuncDecl, Function> functions_inv = null;
-
- public Config config;
- public Context z3;
-
- private Z3TypeCachedBuilder tm;
- private UniqueNamer namer;
- private StreamWriter z3log;
-
- private int counterexamples;
- private string logFilename;
- private List<string> debugTraces;
-
- public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen)
- : base(gen, new VCGenerationOptions(new List<string>())) {
- int timeout = opts.Timeout * 1000;
- config = new Config();
- config.SetParamValue("MODEL", "true");
- config.SetParamValue("MODEL_V2", "true");
- config.SetParamValue("MODEL_COMPLETION", "true");
- config.SetParamValue("MBQI", "false");
- config.SetParamValue("TYPE_CHECK", "true");
- if (0 <= timeout) {
- config.SetParamValue("SOFT_TIMEOUT", timeout.ToString());
- }
-
- if (0 <= CommandLineOptions.Clo.ProverCCLimit) {
- this.counterexamples = CommandLineOptions.Clo.ProverCCLimit;
- }
- if (CommandLineOptions.Clo.SimplifyLogFilePath != null) {
- logFilename = CommandLineOptions.Clo.SimplifyLogFilePath;
- }
- this.debugTraces = new List<string>();
-
- z3 = new Context(config);
- z3.SetPrintMode(PrintMode.Smtlib2Compliant);
- if (logFilename != null)
- {
-#if true
- Z3Log.Open(logFilename);
-#else
- z3.OpenLog(logFilename);
-#endif
- }
- foreach (string tag in debugTraces)
- z3.EnableDebugTrace(tag);
-
- this.z3log = null;
- this.tm = new Z3TypeCachedBuilder(this);
- this.namer = new UniqueNamer();
- }
-
- public Z3apiProverContext(Context ctx, VCExpressionGenerator gen)
- : base(gen, new VCGenerationOptions(new List<string>()))
- {
- z3 = ctx;
-
- this.z3log = null;
- this.tm = new Z3TypeCachedBuilder(this);
- this.namer = new UniqueNamer();
-
- // For external
-
- constants_inv = new BacktrackDictionary<Term, VCExpr>();
- functions_inv = new BacktrackDictionary<FuncDecl, Function>();
- }
-
- public Term VCExprToTerm(VCExpr expr, LineariserOptions linOptions) {
- Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer);
- return (Term)expr.Accept(visitor, linOptions);
- }
-
-
- private class fromZ3
- {
- private VCExpressionGenerator gen;
- private Dictionary<Term, VCExpr> memo;
- private BacktrackDictionary<Term, VCExpr> constants_inv;
- private BacktrackDictionary<FuncDecl, Function> functions_inv;
- private List<VCExprLetBinding> lets;
- private int let_ctr = 0;
-
- private VCExpr create_let(Term t, VCExpr u)
- {
- var name = "$x" + let_ctr.ToString();
- let_ctr++;
- var sym = gen.Variable(name, u.Type);
- memo.Remove(t);
- memo.Add(t, sym);
- lets.Add(gen.LetBinding(sym, u));
- return sym;
- }
-
- public fromZ3(VCExpressionGenerator _gen,
- BacktrackDictionary<Term, VCExpr> _constants_inv,
- BacktrackDictionary<FuncDecl, Function> _functions_inv)
- {
- gen = _gen;
- constants_inv = _constants_inv;
- functions_inv = _functions_inv;
- memo = new Dictionary<Term, VCExpr>();
- lets = new List<VCExprLetBinding>();
- }
-
- public void clear()
- {
- memo.Clear();
- lets.Clear();
- }
- public VCExpr get(Term arg)
- {
- if (memo.ContainsKey(arg))
- return memo[arg];
- VCExpr res = null;
- switch (arg.GetKind())
- {
- case TermKind.Numeral:
- var numstr = arg.GetNumeralString();
- if (arg.GetSort().GetSortKind() == SortKind.Int) {
- res = gen.Integer(Basetypes.BigNum.FromString(numstr));
- }
- else {
- res = gen.Real(Basetypes.BigDec.FromString(numstr));
- }
- break;
- case TermKind.App:
- var args = arg.GetAppArgs();
- var vcargs = new VCExpr[args.Length];
- for (int i = 0; i < args.Length; i++)
- vcargs[i] = get(args[i]);
-
- switch (arg.GetAppDecl().GetKind())
- {
- case DeclKind.Add:
- if (vcargs.Length == 0) {
- if (arg.GetSort().GetSortKind() == SortKind.Int) {
- res = gen.Integer(Basetypes.BigNum.ZERO);
- }
- else {
- res = gen.Real(Basetypes.BigDec.ZERO);
- }
- }
- else
- {
- res = vcargs[0];
- for (int k = 1; k < vcargs.Length; k++)
- res = gen.Add(res, vcargs[k]);
- }
- break;
- case DeclKind.And:
- res = VCExpressionGenerator.True;
- for (int i = 0; i < vcargs.Length; i++)
- res = gen.AndSimp(res, vcargs[i]);
- break;
- case DeclKind.Div:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.RealDivOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.Eq:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Eq(vcargs[0], vcargs[1]);
- break;
- case DeclKind.False:
- res = VCExpressionGenerator.False;
- break;
- case DeclKind.Ge:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.GeOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.Gt:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Gt(vcargs[0], vcargs[1]);
- break;
- case DeclKind.IDiv:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.Iff:
- Debug.Assert(vcargs.Length == 2);
- var l = create_let(args[0], vcargs[0]);
- var r = create_let(args[1], vcargs[1]);
- return gen.And(gen.Implies(l, r), gen.Implies(r, l));
- case DeclKind.Implies:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Implies(vcargs[0], vcargs[1]);
- break;
- case DeclKind.Ite:
- Debug.Assert(vcargs.Length == 3);
- res = gen.Function(VCExpressionGenerator.IfThenElseOp, vcargs[0], vcargs[1], vcargs[2]);
- break;
- case DeclKind.Le:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.LeOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.Lt:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.LtOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.Mod:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.ModOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.Mul:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.MulOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.Not:
- Debug.Assert(vcargs.Length == 1);
- res = gen.Not(vcargs[0]);
- break;
- case DeclKind.Or:
- res = VCExpressionGenerator.False;
- for (int i = 0; i < vcargs.Length; i++)
- res = gen.OrSimp(res, vcargs[i]);
- break;
- case DeclKind.Select:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Select(vcargs[0], vcargs[1]);
- break;
- case DeclKind.Store:
- Debug.Assert(vcargs.Length == 3);
- res = gen.Store(vcargs[0], vcargs[1], vcargs[2]);
- break;
- case DeclKind.Sub:
- Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.SubOp, vcargs[0], vcargs[1]);
- break;
- case DeclKind.True:
- res = VCExpressionGenerator.True;
- break;
- case DeclKind.Uminus:
- Debug.Assert(vcargs.Length == 1);
- var argzero = null;
- if (vcargs[0].Type.IsInt) {
- argzero = gen.Integer(Basetypes.BigNum.ZERO);
- }
- else {
- argzero = gen.Real(Basetypes.BigDec.ZERO);
- }
- res = gen.Function(VCExpressionGenerator.SubOp, argzero, vcargs[0]);
- break;
- case DeclKind.ToInt:
- Debug.Assert(vcargs.Length == 1);
- res = gen.Function(VCExpressionGenerator.ToIntOp, vcargs[0]);
- break;
- case DeclKind.ToReal:
- Debug.Assert(vcargs.Length == 1);
- res = gen.Function(VCExpressionGenerator.ToRealOp, vcargs[0]);
- break;
- case DeclKind.Uninterpreted:
- var name = arg.GetAppDecl().GetDeclName();
- if (args.Length == 0)
- { // a 0-ary constant is a VCExprVar
- if (!constants_inv.TryGetValue(arg, out res))
- throw new Exception("Z3 returned unknown constant: " + name);
- }
- else
- {
- Function f;
- if (!functions_inv.TryGetValue(arg.GetAppDecl(), out f))
- throw new Exception("Z3 returned unknown function: " + name);
- List<VCExpr> vcargsList = new List<VCExpr>(vcargs);
- res = gen.Function(f, vcargsList);
- }
- break;
- default:
- throw new Exception("Unknown Z3 operator");
- }
- break;
- default:
- Debug.Assert(false);
- throw new Exception("Unknown Z3 AST kind");
- }
-
- memo.Add(arg, res);
- return res;
- }
- public VCExpr add_lets(VCExpr e)
- {
- foreach (var let in lets)
- {
- e = gen.Let(e, let);
- }
- return e;
- }
- }
-
- public VCExpr TermToVCExpr(Term t)
- {
- var fZ = new fromZ3(gen, constants_inv, functions_inv);
- return fZ.add_lets(fZ.get(t));
- }
-
-
-
-
-
- public override void DeclareType(TypeCtorDecl t, string attributes) {
- base.DeclareType(t, attributes);
- log("(declare-sort {0})", t.Name);
- }
-
- public override void DeclareConstant(Constant c, bool uniq, string attributes) {
- base.DeclareConstant(c, uniq, attributes);
- DeclareConstant(c.Name, c.TypedIdent.Type);
- }
-
- public override void DeclareFunction(Function f, string attributes) {
- base.DeclareFunction(f, attributes);
- List<Type> domain = new List<Type>();
- foreach (Variable v in f.InParams) {
- domain.Add(v.TypedIdent.Type);
- }
- if (f.OutParams.Length != 1)
- throw new Exception("Cannot handle functions with " + f.OutParams + " out parameters.");
- Type range = f.OutParams[0].TypedIdent.Type;
-
- string functionName = f.Name;
- 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);
- if(functions_inv != null)functions_inv.Add(constDeclAst, f);
- log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);
- }
-
- public override void DeclareGlobalVariable(GlobalVariable v, string attributes) {
- base.DeclareGlobalVariable(v, attributes);
- DeclareConstant(v.Name, v.TypedIdent.Type);
- }
-
- public override string Lookup(VCExprVar var) {
- return namer.Lookup(var);
- }
-
- 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() {
-#if true
- Z3Log.Close();
-#else
- z3.CloseLog();
-#endif
- if (z3log != null) {
- z3log.Close();
- }
- z3log = null;
- }
-
- public void CreateBacktrackPoint() {
- symbols.CreateBacktrackPoint();
- constants.CreateBacktrackPoint();
- functions.CreateBacktrackPoint();
- labels.CreateBacktrackPoint();
- if(constants_inv != null)constants_inv.CreateBacktrackPoint();
- if(functions_inv != null)functions_inv.CreateBacktrackPoint();
- z3.Push();
- log("(push)");
- }
-
- public void Backtrack() {
- z3.Pop();
- labels.Backtrack();
- functions.Backtrack();
- constants.Backtrack();
- symbols.Backtrack();
- if (constants_inv != null) constants_inv.Backtrack();
- if (functions_inv != null) functions_inv.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);
- }
- }
-
- 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;
- }
-
- 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 void DisplayRelevantLabels(List<string> relevantLabels) {
- foreach (string labelName in relevantLabels) {
- System.Console.Write(labelName + ",");
- }
- System.Console.WriteLine("---");
- }
-
- private 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 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.counterexamples);
- while (true) {
- Z3Model 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);
- }
-
- var sw = new StringWriter();
- sw.WriteLine("*** MODEL");
- z3Model.Display(sw);
- sw.WriteLine("*** END_MODEL");
- var sr = new StringReader(sw.ToString());
- var models = Microsoft.Boogie.Model.ParseModels(sr);
- Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
- boogieErrors.Add(e);
-
- if (boogieErrors.Count < this.counterexamples) {
- z3.BlockLiterals(labels);
- log("block-literals {0}", labels);
- }
-
- labels.Dispose();
- z3Model.Dispose();
- if (boogieErrors.Count == this.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;
-
- Z3Model 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);
- }
-
- var sw = new StringWriter();
- sw.WriteLine("*** MODEL");
- z3Model.Display(sw);
- sw.WriteLine("*** END_MODEL");
- var sr = new StringReader(sw.ToString());
- var models = Microsoft.Boogie.Model.ParseModels(sr);
- Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings));
- boogieErrors.Add(e);
-
- 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;
- }
- }
-
- 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 Term GetConstant(string constantName, Type constantType, VCExpr node)
- {
- Term typeSafeTerm;
- if (!constants.ContainsKey(constantName))
- this.DeclareConstant(constantName, constantType);
-
- if (!constants.TryGetValue(constantName, out typeSafeTerm))
- throw new Exception("constant " + constantName + " is not defined");
-
- if (constants_inv != null && !constants_inv.ContainsKey(typeSafeTerm))
- constants_inv.Add(typeSafeTerm, node);
-
- return typeSafeTerm;
- }
-
- public FuncDecl GetFunction(string functionName) {
- FuncDecl f;
- if (!functions.TryGetValue(functionName, out f))
- throw new Exception("function " + functionName + " is undefined");
- return f;
- }
-
- 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;
- }
- }
-
- internal class BacktrackDictionary<K, V> {
- private Dictionary<K, V> dictionary = new Dictionary<K, V>();
- private Stack<List<K>> keyStack = new Stack<List<K>>();
-
- public BacktrackDictionary() {
- CreateBacktrackPoint();
- }
-
- public bool TryGetValue(K key, out V val) {
- return dictionary.TryGetValue(key, out val);
- }
-
- public void Add(K key, V v) {
- if (dictionary.ContainsKey(key)) {
- dictionary.Remove(key);
- }
- dictionary.Add(key, v);
- keyStack.Peek().Add(key);
- }
-
- public bool ContainsKey(K k) {
- return dictionary.ContainsKey(k);
- }
-
- public void CreateBacktrackPoint() {
- keyStack.Push(new List<K>());
- }
-
- public void Backtrack() {
- List<K> keysToErase = keyStack.Pop();
- foreach (K key in keysToErase) {
- dictionary.Remove(key);
- }
- if (keyStack.Count == 0)
- this.CreateBacktrackPoint();
- }
-
- public IEnumerator GetEnumerator() {
- return dictionary.Keys.GetEnumerator();
- }
- }
-
- public class Z3ErrorModelAndLabels {
- private Model _model;
- private List<string> _relevantLabels;
- public Model Model {
- get { return this._model; }
- }
- public List<string> RelevantLabels {
- get { return this._relevantLabels; }
- }
- public Z3ErrorModelAndLabels(Model model, List<string> relevantLabels) {
- this._model = model;
- this._relevantLabels = relevantLabels;
- }
- }
-
-
-
+using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using System.Diagnostics; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.Z3; +using Microsoft.Z3; +using Microsoft.Boogie.VCExprAST; +using Microsoft.Basetypes; + +using Z3Model = Microsoft.Z3.Model; +using BoogieModel = Microsoft.Boogie.Model; + +namespace Microsoft.Boogie.Z3 { + public class Z3apiProverContext : DeclFreeProverContext { + 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>(); + internal BacktrackDictionary<Term, VCExpr> constants_inv = null; + internal BacktrackDictionary<FuncDecl, Function> functions_inv = null; + + public Config config; + public Context z3; + + private Z3TypeCachedBuilder tm; + private UniqueNamer namer; + private StreamWriter z3log; + + private int counterexamples; + private string logFilename; + private List<string> debugTraces; + + public Z3apiProverContext(Z3InstanceOptions opts, VCExpressionGenerator gen) + : base(gen, new VCGenerationOptions(new List<string>())) { + int timeout = opts.Timeout * 1000; + config = new Config(); + config.SetParamValue("MODEL", "true"); + config.SetParamValue("MODEL_V2", "true"); + config.SetParamValue("MODEL_COMPLETION", "true"); + config.SetParamValue("MBQI", "false"); + config.SetParamValue("TYPE_CHECK", "true"); + if (0 <= timeout) { + config.SetParamValue("SOFT_TIMEOUT", timeout.ToString()); + } + + if (0 <= CommandLineOptions.Clo.ProverCCLimit) { + this.counterexamples = CommandLineOptions.Clo.ProverCCLimit; + } + if (CommandLineOptions.Clo.SimplifyLogFilePath != null) { + logFilename = CommandLineOptions.Clo.SimplifyLogFilePath; + } + this.debugTraces = new List<string>(); + + z3 = new Context(config); + z3.SetPrintMode(PrintMode.Smtlib2Compliant); + if (logFilename != null) + { +#if true + Z3Log.Open(logFilename); +#else + z3.OpenLog(logFilename); +#endif + } + foreach (string tag in debugTraces) + z3.EnableDebugTrace(tag); + + this.z3log = null; + this.tm = new Z3TypeCachedBuilder(this); + this.namer = new UniqueNamer(); + } + + public Z3apiProverContext(Context ctx, VCExpressionGenerator gen) + : base(gen, new VCGenerationOptions(new List<string>())) + { + z3 = ctx; + + this.z3log = null; + this.tm = new Z3TypeCachedBuilder(this); + this.namer = new UniqueNamer(); + + // For external + + constants_inv = new BacktrackDictionary<Term, VCExpr>(); + functions_inv = new BacktrackDictionary<FuncDecl, Function>(); + } + + public Term VCExprToTerm(VCExpr expr, LineariserOptions linOptions) { + Z3apiExprLineariser visitor = new Z3apiExprLineariser(this, namer); + return (Term)expr.Accept(visitor, linOptions); + } + + + private class fromZ3 + { + private VCExpressionGenerator gen; + private Dictionary<Term, VCExpr> memo; + private BacktrackDictionary<Term, VCExpr> constants_inv; + private BacktrackDictionary<FuncDecl, Function> functions_inv; + private List<VCExprLetBinding> lets; + private int let_ctr = 0; + + private VCExpr create_let(Term t, VCExpr u) + { + var name = "$x" + let_ctr.ToString(); + let_ctr++; + var sym = gen.Variable(name, u.Type); + memo.Remove(t); + memo.Add(t, sym); + lets.Add(gen.LetBinding(sym, u)); + return sym; + } + + public fromZ3(VCExpressionGenerator _gen, + BacktrackDictionary<Term, VCExpr> _constants_inv, + BacktrackDictionary<FuncDecl, Function> _functions_inv) + { + gen = _gen; + constants_inv = _constants_inv; + functions_inv = _functions_inv; + memo = new Dictionary<Term, VCExpr>(); + lets = new List<VCExprLetBinding>(); + } + + public void clear() + { + memo.Clear(); + lets.Clear(); + } + public VCExpr get(Term arg) + { + if (memo.ContainsKey(arg)) + return memo[arg]; + VCExpr res = null; + switch (arg.GetKind()) + { + case TermKind.Numeral: + var numstr = arg.GetNumeralString(); + if (arg.GetSort().GetSortKind() == SortKind.Int) { + res = gen.Integer(Basetypes.BigNum.FromString(numstr)); + } + else { + res = gen.Real(Basetypes.BigDec.FromString(numstr)); + } + break; + case TermKind.App: + var args = arg.GetAppArgs(); + var vcargs = new VCExpr[args.Length]; + for (int i = 0; i < args.Length; i++) + vcargs[i] = get(args[i]); + + switch (arg.GetAppDecl().GetKind()) + { + case DeclKind.Add: + if (vcargs.Length == 0) { + if (arg.GetSort().GetSortKind() == SortKind.Int) { + res = gen.Integer(Basetypes.BigNum.ZERO); + } + else { + res = gen.Real(Basetypes.BigDec.ZERO); + } + } + else + { + res = vcargs[0]; + for (int k = 1; k < vcargs.Length; k++) + res = gen.Add(res, vcargs[k]); + } + break; + case DeclKind.And: + res = VCExpressionGenerator.True; + for (int i = 0; i < vcargs.Length; i++) + res = gen.AndSimp(res, vcargs[i]); + break; + case DeclKind.Div: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.RealDivOp, vcargs[0], vcargs[1]); + break; + case DeclKind.Eq: + Debug.Assert(vcargs.Length == 2); + res = gen.Eq(vcargs[0], vcargs[1]); + break; + case DeclKind.False: + res = VCExpressionGenerator.False; + break; + case DeclKind.Ge: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.GeOp, vcargs[0], vcargs[1]); + break; + case DeclKind.Gt: + Debug.Assert(vcargs.Length == 2); + res = gen.Gt(vcargs[0], vcargs[1]); + break; + case DeclKind.IDiv: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]); + break; + case DeclKind.Iff: + Debug.Assert(vcargs.Length == 2); + var l = create_let(args[0], vcargs[0]); + var r = create_let(args[1], vcargs[1]); + return gen.And(gen.Implies(l, r), gen.Implies(r, l)); + case DeclKind.Implies: + Debug.Assert(vcargs.Length == 2); + res = gen.Implies(vcargs[0], vcargs[1]); + break; + case DeclKind.Ite: + Debug.Assert(vcargs.Length == 3); + res = gen.Function(VCExpressionGenerator.IfThenElseOp, vcargs[0], vcargs[1], vcargs[2]); + break; + case DeclKind.Le: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.LeOp, vcargs[0], vcargs[1]); + break; + case DeclKind.Lt: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.LtOp, vcargs[0], vcargs[1]); + break; + case DeclKind.Mod: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.ModOp, vcargs[0], vcargs[1]); + break; + case DeclKind.Mul: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.MulOp, vcargs[0], vcargs[1]); + break; + case DeclKind.Not: + Debug.Assert(vcargs.Length == 1); + res = gen.Not(vcargs[0]); + break; + case DeclKind.Or: + res = VCExpressionGenerator.False; + for (int i = 0; i < vcargs.Length; i++) + res = gen.OrSimp(res, vcargs[i]); + break; + case DeclKind.Select: + Debug.Assert(vcargs.Length == 2); + res = gen.Select(vcargs[0], vcargs[1]); + break; + case DeclKind.Store: + Debug.Assert(vcargs.Length == 3); + res = gen.Store(vcargs[0], vcargs[1], vcargs[2]); + break; + case DeclKind.Sub: + Debug.Assert(vcargs.Length == 2); + res = gen.Function(VCExpressionGenerator.SubOp, vcargs[0], vcargs[1]); + break; + case DeclKind.True: + res = VCExpressionGenerator.True; + break; + case DeclKind.Uminus: + Debug.Assert(vcargs.Length == 1); + var argzero = null; + if (vcargs[0].Type.IsInt) { + argzero = gen.Integer(Basetypes.BigNum.ZERO); + } + else { + argzero = gen.Real(Basetypes.BigDec.ZERO); + } + res = gen.Function(VCExpressionGenerator.SubOp, argzero, vcargs[0]); + break; + case DeclKind.ToInt: + Debug.Assert(vcargs.Length == 1); + res = gen.Function(VCExpressionGenerator.ToIntOp, vcargs[0]); + break; + case DeclKind.ToReal: + Debug.Assert(vcargs.Length == 1); + res = gen.Function(VCExpressionGenerator.ToRealOp, vcargs[0]); + break; + case DeclKind.Uninterpreted: + var name = arg.GetAppDecl().GetDeclName(); + if (args.Length == 0) + { // a 0-ary constant is a VCExprVar + if (!constants_inv.TryGetValue(arg, out res)) + throw new Exception("Z3 returned unknown constant: " + name); + } + else + { + Function f; + if (!functions_inv.TryGetValue(arg.GetAppDecl(), out f)) + throw new Exception("Z3 returned unknown function: " + name); + List<VCExpr> vcargsList = new List<VCExpr>(vcargs); + res = gen.Function(f, vcargsList); + } + break; + default: + throw new Exception("Unknown Z3 operator"); + } + break; + default: + Debug.Assert(false); + throw new Exception("Unknown Z3 AST kind"); + } + + memo.Add(arg, res); + return res; + } + public VCExpr add_lets(VCExpr e) + { + foreach (var let in lets) + { + e = gen.Let(e, let); + } + return e; + } + } + + public VCExpr TermToVCExpr(Term t) + { + var fZ = new fromZ3(gen, constants_inv, functions_inv); + return fZ.add_lets(fZ.get(t)); + } + + + + + + public override void DeclareType(TypeCtorDecl t, string attributes) { + base.DeclareType(t, attributes); + log("(declare-sort {0})", t.Name); + } + + public override void DeclareConstant(Constant c, bool uniq, string attributes) { + base.DeclareConstant(c, uniq, attributes); + DeclareConstant(c.Name, c.TypedIdent.Type); + } + + public override void DeclareFunction(Function f, string attributes) { + base.DeclareFunction(f, attributes); + List<Type> domain = new List<Type>(); + foreach (Variable v in f.InParams) { + domain.Add(v.TypedIdent.Type); + } + if (f.OutParams.Length != 1) + throw new Exception("Cannot handle functions with " + f.OutParams + " out parameters."); + Type range = f.OutParams[0].TypedIdent.Type; + + string functionName = f.Name; + 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); + if(functions_inv != null)functions_inv.Add(constDeclAst, f); + log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst); + } + + public override void DeclareGlobalVariable(GlobalVariable v, string attributes) { + base.DeclareGlobalVariable(v, attributes); + DeclareConstant(v.Name, v.TypedIdent.Type); + } + + public override string Lookup(VCExprVar var) { + return namer.Lookup(var); + } + + 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() { +#if true + Z3Log.Close(); +#else + z3.CloseLog(); +#endif + if (z3log != null) { + z3log.Close(); + } + z3log = null; + } + + public void CreateBacktrackPoint() { + symbols.CreateBacktrackPoint(); + constants.CreateBacktrackPoint(); + functions.CreateBacktrackPoint(); + labels.CreateBacktrackPoint(); + if(constants_inv != null)constants_inv.CreateBacktrackPoint(); + if(functions_inv != null)functions_inv.CreateBacktrackPoint(); + z3.Push(); + log("(push)"); + } + + public void Backtrack() { + z3.Pop(); + labels.Backtrack(); + functions.Backtrack(); + constants.Backtrack(); + symbols.Backtrack(); + if (constants_inv != null) constants_inv.Backtrack(); + if (functions_inv != null) functions_inv.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); + } + } + + 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; + } + + 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 void DisplayRelevantLabels(List<string> relevantLabels) { + foreach (string labelName in relevantLabels) { + System.Console.Write(labelName + ","); + } + System.Console.WriteLine("---"); + } + + private 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 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.counterexamples); + while (true) { + Z3Model 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); + } + + var sw = new StringWriter(); + sw.WriteLine("*** MODEL"); + z3Model.Display(sw); + sw.WriteLine("*** END_MODEL"); + var sr = new StringReader(sw.ToString()); + var models = Microsoft.Boogie.Model.ParseModels(sr); + Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings)); + boogieErrors.Add(e); + + if (boogieErrors.Count < this.counterexamples) { + z3.BlockLiterals(labels); + log("block-literals {0}", labels); + } + + labels.Dispose(); + z3Model.Dispose(); + if (boogieErrors.Count == this.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; + + Z3Model 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); + } + + var sw = new StringWriter(); + sw.WriteLine("*** MODEL"); + z3Model.Display(sw); + sw.WriteLine("*** END_MODEL"); + var sr = new StringReader(sw.ToString()); + var models = Microsoft.Boogie.Model.ParseModels(sr); + Z3ErrorModelAndLabels e = new Z3ErrorModelAndLabels(models[0], new List<string>(labelStrings)); + boogieErrors.Add(e); + + 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; + } + } + + 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 Term GetConstant(string constantName, Type constantType, VCExpr node) + { + Term typeSafeTerm; + if (!constants.ContainsKey(constantName)) + this.DeclareConstant(constantName, constantType); + + if (!constants.TryGetValue(constantName, out typeSafeTerm)) + throw new Exception("constant " + constantName + " is not defined"); + + if (constants_inv != null && !constants_inv.ContainsKey(typeSafeTerm)) + constants_inv.Add(typeSafeTerm, node); + + return typeSafeTerm; + } + + public FuncDecl GetFunction(string functionName) { + FuncDecl f; + if (!functions.TryGetValue(functionName, out f)) + throw new Exception("function " + functionName + " is undefined"); + return f; + } + + 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; + } + } + + internal class BacktrackDictionary<K, V> { + private Dictionary<K, V> dictionary = new Dictionary<K, V>(); + private Stack<List<K>> keyStack = new Stack<List<K>>(); + + public BacktrackDictionary() { + CreateBacktrackPoint(); + } + + public bool TryGetValue(K key, out V val) { + return dictionary.TryGetValue(key, out val); + } + + public void Add(K key, V v) { + if (dictionary.ContainsKey(key)) { + dictionary.Remove(key); + } + dictionary.Add(key, v); + keyStack.Peek().Add(key); + } + + public bool ContainsKey(K k) { + return dictionary.ContainsKey(k); + } + + public void CreateBacktrackPoint() { + keyStack.Push(new List<K>()); + } + + public void Backtrack() { + List<K> keysToErase = keyStack.Pop(); + foreach (K key in keysToErase) { + dictionary.Remove(key); + } + if (keyStack.Count == 0) + this.CreateBacktrackPoint(); + } + + public IEnumerator GetEnumerator() { + return dictionary.Keys.GetEnumerator(); + } + } + + public class Z3ErrorModelAndLabels { + private Model _model; + private List<string> _relevantLabels; + public Model Model { + get { return this._model; } + } + public List<string> RelevantLabels { + get { return this._relevantLabels; } + } + public Z3ErrorModelAndLabels(Model model, List<string> relevantLabels) { + this._model = model; + this._relevantLabels = relevantLabels; + } + } + + + }
\ No newline at end of file diff --git a/Source/Provers/Z3api/ProverLayer.cs b/Source/Provers/Z3api/ProverLayer.cs index d72705f3..cb7df8d7 100644 --- a/Source/Provers/Z3api/ProverLayer.cs +++ b/Source/Provers/Z3api/ProverLayer.cs @@ -1,354 +1,354 @@ -using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Diagnostics;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Z3;
-using Microsoft.Boogie.VCExprAST;
-using System.Diagnostics.Contracts;
-
-using TypeAst = System.IntPtr;
-using TermAst = System.IntPtr;
-using ConstDeclAst = System.IntPtr;
-using ConstAst = System.IntPtr;
-using Value = System.IntPtr;
-using PatternAst = System.IntPtr;
-
-namespace Microsoft.Boogie.Z3
-{
- public class Z3InstanceOptions : ProverOptions {
- public int Timeout { get { return TimeLimit / 1000; } }
- public int Lets {
- get {
- Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4);
- return CommandLineOptions.Clo.Z3lets;
- }
- }
- public bool DistZ3 = false;
- public string ExeName = "z3.exe";
- public bool InverseImplies = false;
- public string Inspector = null;
- public bool OptimizeForBv = false;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(ExeName != null);
- }
-
- protected override bool Parse(string opt) {
- //Contract.Requires(opt!=null);
- return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) ||
- ParseString(opt, "INSPECTOR", ref Inspector) ||
- ParseBool(opt, "DIST", ref DistZ3) ||
- ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
- base.Parse(opt);
- }
-
- public override void PostParse() {
- base.PostParse();
-
- if (DistZ3) {
- ExeName = "z3-dist.exe";
- CommandLineOptions.Clo.RestartProverPerVC = true;
- }
- }
-
- public override string Help {
- get {
- return
-@"
-Z3-specific options:
-~~~~~~~~~~~~~~~~~~~~
-INSPECTOR=<string> Use the specified Z3Inspector binary.
-OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
-
-Obscure options:
-~~~~~~~~~~~~~~~~
-DIST=<bool> Use z3-dist.exe binary.
-REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P.
-
-" + base.Help;
- // DIST requires non-public binaries
- }
- }
- }
-
- public class Z3LineariserOptions : LineariserOptions {
- private readonly Z3InstanceOptions opts;
-
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(opts != null);
- }
-
-
- public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables)
- : base(asTerm) {
- Contract.Requires(opts != null);
- Contract.Requires(cce.NonNullElements(letVariables));
-
- this.opts = opts;
- this.LetVariablesAttr = letVariables;
- }
-
- public override bool UseWeights {
- get {
- return true;
- }
- }
-
- public override bool UseTypes {
- get {
- return true;
- }
- }
-
- public override bool QuantifierIds {
- get {
- return true;
- }
- }
-
- public override bool InverseImplies {
- get {
- return opts.InverseImplies;
- }
- }
-
- public override LineariserOptions SetAsTerm(bool newVal) {
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- if (newVal == AsTerm)
- return this;
- return new Z3LineariserOptions(newVal, opts, LetVariables);
- }
-
- // variables representing formulas in let-bindings have to be
- // printed in a different way than other variables
- private readonly List<VCExprVar/*!>!*/> LetVariablesAttr;
- public override List<VCExprVar/*!>!*/> LetVariables {
- get {
- Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>()));
-
- return LetVariablesAttr;
- }
- }
-
- public override LineariserOptions AddLetVariable(VCExprVar furtherVar) {
- //Contract.Requires(furtherVar != null);
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
- allVars.AddRange(LetVariables);
- allVars.Add(furtherVar);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
-
- public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) {
- //Contract.Requires(furtherVars != null);
- Contract.Ensures(Contract.Result<LineariserOptions>() != null);
-
- List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>();
- allVars.AddRange(LetVariables);
- allVars.AddRange(furtherVars);
- return new Z3LineariserOptions(AsTerm, opts, allVars);
- }
- }
-
- public class Z3apiProcessTheoremProver : ProverInterface
- {
- public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt)
- {
- this.options = opts;
- this.context = (Z3apiProverContext) ctxt;
- this.numAxiomsPushed = 0;
- }
-
- private Z3InstanceOptions options;
-
- private Z3apiProverContext context;
- public override ProverContext Context
- {
- get { return context; }
- }
-
- public override VCExpressionGenerator VCExprGen
- {
- get { return context.ExprGen; }
- }
-
- private int numAxiomsPushed;
-
- public override void Close()
- {
- base.Close();
- context.CloseLog();
- context.z3.Dispose();
- context.config.Dispose();
- }
-
- public void PushAxiom(VCExpr axiom)
- {
- context.CreateBacktrackPoint();
- LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- context.AddAxiom(axiom, linOptions);
- }
-
- private void PushConjecture(VCExpr conjecture)
- {
- context.CreateBacktrackPoint();
- LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- context.AddConjecture(conjecture, linOptions);
- }
-
- public override void PushVCExpression(VCExpr vc)
- {
- PushAxiom(vc);
- numAxiomsPushed++;
- }
-
- public void CreateBacktrackPoint()
- {
- context.CreateBacktrackPoint();
- }
-
- public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler)
- {
- LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- Push();
- context.AddAxiom(context.Axioms, linOptions);
- context.AddConjecture(vc, linOptions);
- outcome = context.Check(out z3LabelModels);
- Pop();
- }
-
- public override void Check()
- {
- outcome = context.Check(out z3LabelModels);
- }
-
- public override ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler)
- {
- LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore);
- }
-
- public override void Push()
- {
- context.CreateBacktrackPoint();
- }
-
- public override void Pop()
- {
- context.Backtrack();
- }
-
- public override void Assert(VCExpr vc, bool polarity)
- {
- LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- if (polarity)
- context.AddAxiom(vc, linOptions);
- else
- context.AddConjecture(vc, linOptions);
- }
-
- public override void AssertAxioms()
- {
- LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>());
- context.AddAxiom(context.Axioms, linOptions);
- }
-
- // Number of axioms pushed since the last call to FlushAxioms
- public override int NumAxiomsPushed()
- {
- return numAxiomsPushed;
- }
-
- public override int FlushAxiomsToTheoremProver()
- {
- var ret = numAxiomsPushed;
- numAxiomsPushed = 0;
- return ret;
- }
-
- private Outcome outcome;
- private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>();
-
- [NoDefaultContract]
- public override Outcome CheckOutcome(ErrorHandler handler)
- {
- if (outcome == Outcome.Invalid)
- {
- foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels)
- {
- List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
- handler.OnModel(unprefixedLabels, z3LabelModel.Model);
- }
- }
- return outcome;
- }
-
- public override Outcome CheckOutcomeCore(ErrorHandler handler) {
- if (outcome == Outcome.Invalid) {
- foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) {
- List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels);
- handler.OnModel(unprefixedLabels, z3LabelModel.Model);
- }
- }
- return outcome;
- }
-
- private List<string> RemovePrefixes(List<string> labels)
- {
- List<string> result = new List<string>();
- foreach (string label in labels)
- {
- if (label.StartsWith("+"))
- {
- result.Add(label.Substring(1));
- }
- else if (label.StartsWith("|"))
- {
- result.Add(label.Substring(1));
- }
- else if (label.StartsWith("@"))
- {
- result.Add(label.Substring(1));
- }
- else
- throw new Exception("Unknown prefix in label " + label);
- }
- return result;
- }
- }
-}
-
-namespace Microsoft.Boogie.Z3api
-{
- public class Factory : ProverFactory
- {
- public override object SpawnProver(ProverOptions options, object ctxt)
- {
- return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt);
- }
-
- public override object NewProverContext(ProverOptions opts)
- {
- if (CommandLineOptions.Clo.BracketIdsInVC < 0)
- {
- CommandLineOptions.Clo.BracketIdsInVC = 0;
- }
-
- VCExpressionGenerator gen = new VCExpressionGenerator();
- return new Z3apiProverContext((Z3InstanceOptions)opts, gen);
- }
-
- public override ProverOptions BlankProverOptions()
- {
- return new Z3InstanceOptions();
- }
- }
+using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using System.Diagnostics; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.Z3; +using Microsoft.Boogie.VCExprAST; +using System.Diagnostics.Contracts; + +using TypeAst = System.IntPtr; +using TermAst = System.IntPtr; +using ConstDeclAst = System.IntPtr; +using ConstAst = System.IntPtr; +using Value = System.IntPtr; +using PatternAst = System.IntPtr; + +namespace Microsoft.Boogie.Z3 +{ + public class Z3InstanceOptions : ProverOptions { + public int Timeout { get { return TimeLimit / 1000; } } + public int Lets { + get { + Contract.Ensures(0 <= Contract.Result<int>() && Contract.Result<int>() < 4); + return CommandLineOptions.Clo.Z3lets; + } + } + public bool DistZ3 = false; + public string ExeName = "z3.exe"; + public bool InverseImplies = false; + public string Inspector = null; + public bool OptimizeForBv = false; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(ExeName != null); + } + + protected override bool Parse(string opt) { + //Contract.Requires(opt!=null); + return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) || + ParseString(opt, "INSPECTOR", ref Inspector) || + ParseBool(opt, "DIST", ref DistZ3) || + ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) || + base.Parse(opt); + } + + public override void PostParse() { + base.PostParse(); + + if (DistZ3) { + ExeName = "z3-dist.exe"; + CommandLineOptions.Clo.RestartProverPerVC = true; + } + } + + public override string Help { + get { + return +@" +Z3-specific options: +~~~~~~~~~~~~~~~~~~~~ +INSPECTOR=<string> Use the specified Z3Inspector binary. +OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false. + +Obscure options: +~~~~~~~~~~~~~~~~ +DIST=<bool> Use z3-dist.exe binary. +REVERSE_IMPLIES=<bool> Encode P==>Q as Q||!P. + +" + base.Help; + // DIST requires non-public binaries + } + } + } + + public class Z3LineariserOptions : LineariserOptions { + private readonly Z3InstanceOptions opts; + + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(opts != null); + } + + + public Z3LineariserOptions(bool asTerm, Z3InstanceOptions opts, List<VCExprVar/*!>!*/> letVariables) + : base(asTerm) { + Contract.Requires(opts != null); + Contract.Requires(cce.NonNullElements(letVariables)); + + this.opts = opts; + this.LetVariablesAttr = letVariables; + } + + public override bool UseWeights { + get { + return true; + } + } + + public override bool UseTypes { + get { + return true; + } + } + + public override bool QuantifierIds { + get { + return true; + } + } + + public override bool InverseImplies { + get { + return opts.InverseImplies; + } + } + + public override LineariserOptions SetAsTerm(bool newVal) { + Contract.Ensures(Contract.Result<LineariserOptions>() != null); + + if (newVal == AsTerm) + return this; + return new Z3LineariserOptions(newVal, opts, LetVariables); + } + + // variables representing formulas in let-bindings have to be + // printed in a different way than other variables + private readonly List<VCExprVar/*!>!*/> LetVariablesAttr; + public override List<VCExprVar/*!>!*/> LetVariables { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result<List<VCExprVar>>())); + + return LetVariablesAttr; + } + } + + public override LineariserOptions AddLetVariable(VCExprVar furtherVar) { + //Contract.Requires(furtherVar != null); + Contract.Ensures(Contract.Result<LineariserOptions>() != null); + + List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>(); + allVars.AddRange(LetVariables); + allVars.Add(furtherVar); + return new Z3LineariserOptions(AsTerm, opts, allVars); + } + + public override LineariserOptions AddLetVariables(List<VCExprVar/*!>!*/> furtherVars) { + //Contract.Requires(furtherVars != null); + Contract.Ensures(Contract.Result<LineariserOptions>() != null); + + List<VCExprVar/*!>!*/> allVars = new List<VCExprVar/*!*/>(); + allVars.AddRange(LetVariables); + allVars.AddRange(furtherVars); + return new Z3LineariserOptions(AsTerm, opts, allVars); + } + } + + public class Z3apiProcessTheoremProver : ProverInterface + { + public Z3apiProcessTheoremProver(Z3InstanceOptions opts, DeclFreeProverContext ctxt) + { + this.options = opts; + this.context = (Z3apiProverContext) ctxt; + this.numAxiomsPushed = 0; + } + + private Z3InstanceOptions options; + + private Z3apiProverContext context; + public override ProverContext Context + { + get { return context; } + } + + public override VCExpressionGenerator VCExprGen + { + get { return context.ExprGen; } + } + + private int numAxiomsPushed; + + public override void Close() + { + base.Close(); + context.CloseLog(); + context.z3.Dispose(); + context.config.Dispose(); + } + + public void PushAxiom(VCExpr axiom) + { + context.CreateBacktrackPoint(); + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>()); + context.AddAxiom(axiom, linOptions); + } + + private void PushConjecture(VCExpr conjecture) + { + context.CreateBacktrackPoint(); + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>()); + context.AddConjecture(conjecture, linOptions); + } + + public override void PushVCExpression(VCExpr vc) + { + PushAxiom(vc); + numAxiomsPushed++; + } + + public void CreateBacktrackPoint() + { + context.CreateBacktrackPoint(); + } + + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>()); + Push(); + context.AddAxiom(context.Axioms, linOptions); + context.AddConjecture(vc, linOptions); + outcome = context.Check(out z3LabelModels); + Pop(); + } + + public override void Check() + { + outcome = context.Check(out z3LabelModels); + } + + public override ProverInterface.Outcome CheckAssumptions(List<VCExpr> assumptions, out List<int> unsatCore, ErrorHandler handler) + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>()); + return context.CheckAssumptions(assumptions, linOptions, out z3LabelModels, out unsatCore); + } + + public override void Push() + { + context.CreateBacktrackPoint(); + } + + public override void Pop() + { + context.Backtrack(); + } + + public override void Assert(VCExpr vc, bool polarity) + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>()); + if (polarity) + context.AddAxiom(vc, linOptions); + else + context.AddConjecture(vc, linOptions); + } + + public override void AssertAxioms() + { + LineariserOptions linOptions = new Z3LineariserOptions(false, (Z3InstanceOptions)this.options, new List<VCExprVar>()); + context.AddAxiom(context.Axioms, linOptions); + } + + // Number of axioms pushed since the last call to FlushAxioms + public override int NumAxiomsPushed() + { + return numAxiomsPushed; + } + + public override int FlushAxiomsToTheoremProver() + { + var ret = numAxiomsPushed; + numAxiomsPushed = 0; + return ret; + } + + private Outcome outcome; + private List<Z3ErrorModelAndLabels> z3LabelModels = new List<Z3ErrorModelAndLabels>(); + + [NoDefaultContract] + public override Outcome CheckOutcome(ErrorHandler handler) + { + if (outcome == Outcome.Invalid) + { + foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) + { + List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels); + handler.OnModel(unprefixedLabels, z3LabelModel.Model); + } + } + return outcome; + } + + public override Outcome CheckOutcomeCore(ErrorHandler handler) { + if (outcome == Outcome.Invalid) { + foreach (Z3ErrorModelAndLabels z3LabelModel in z3LabelModels) { + List<string> unprefixedLabels = RemovePrefixes(z3LabelModel.RelevantLabels); + handler.OnModel(unprefixedLabels, z3LabelModel.Model); + } + } + return outcome; + } + + private List<string> RemovePrefixes(List<string> labels) + { + List<string> result = new List<string>(); + foreach (string label in labels) + { + if (label.StartsWith("+")) + { + result.Add(label.Substring(1)); + } + else if (label.StartsWith("|")) + { + result.Add(label.Substring(1)); + } + else if (label.StartsWith("@")) + { + result.Add(label.Substring(1)); + } + else + throw new Exception("Unknown prefix in label " + label); + } + return result; + } + } +} + +namespace Microsoft.Boogie.Z3api +{ + public class Factory : ProverFactory + { + public override object SpawnProver(ProverOptions options, object ctxt) + { + return new Z3apiProcessTheoremProver((Z3InstanceOptions) options, (Z3apiProverContext) ctxt); + } + + public override object NewProverContext(ProverOptions opts) + { + if (CommandLineOptions.Clo.BracketIdsInVC < 0) + { + CommandLineOptions.Clo.BracketIdsInVC = 0; + } + + VCExpressionGenerator gen = new VCExpressionGenerator(); + return new Z3apiProverContext((Z3InstanceOptions)opts, gen); + } + + public override ProverOptions BlankProverOptions() + { + return new Z3InstanceOptions(); + } + } }
\ No newline at end of file diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index 72192804..b83d6dff 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -1,16 +1,16 @@ -using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Diagnostics;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Z3;
-using Microsoft.Z3;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
-
+using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using System.Diagnostics; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.Z3; +using Microsoft.Z3; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.Z3 +{ + }
\ No newline at end of file diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs index b129b378..79f140aa 100644 --- a/Source/Provers/Z3api/StubContext.cs +++ b/Source/Provers/Z3api/StubContext.cs @@ -1,75 +1,75 @@ -using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Diagnostics;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Z3;
-using Microsoft.Z3;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3 {
- public class Z3StubContext : Z3Context {
- class Z3StubPatternAst: Z3PatternAst {}
- class Z3StubTermAst: Z3TermAst {}
- class Z3StubLabeledLiterals: Z3LabeledLiterals {}
-
- public void CreateBacktrackPoint(){}
- public void Backtrack(){}
- public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) { }
- public void AddConjecture(VCExpr vc, LineariserOptions linOptions){}
- public void AddSmtlibString(string smtlibString) {}
- public string GetDeclName(Z3ConstDeclAst constDeclAst) {
- return "";
- }
- public Z3PatternAst MakePattern(List<Z3TermAst> exprs) {
- return new Z3StubPatternAst();
- }
- 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) {
- return new Z3StubTermAst();
- }
- public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) {
- boogieErrors = new List<Z3ErrorModelAndLabels>();
- return ProverInterface.Outcome.Undetermined;
- }
- public void TypeCheckBool(Z3TermAst t){}
- public void TypeCheckInt(Z3TermAst t){}
- public void DeclareType(string typeName) {}
- public void DeclareConstant(string constantName, Type boogieType) {}
- public void DeclareFunction(string functionName, List<Type> domain, Type range) {}
- public Z3TermAst GetConstant(string constantName, Type constantType) {
- return new Z3StubTermAst();
- }
- public Z3TermAst MakeIntLiteral(string numeral) {
- return new Z3StubTermAst();
- }
- public Z3TermAst MakeBvLiteral(int i, uint bvSize) {
- return new Z3StubTermAst();
- }
- public Z3TermAst MakeTrue() {
- return new Z3StubTermAst();
- }
- public Z3TermAst MakeFalse() {
- return new Z3StubTermAst();
- }
- public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child) {
- return new Z3StubTermAst();
- }
- public Z3LabeledLiterals GetRelevantLabels() {
- return new Z3StubLabeledLiterals();
- }
- public Z3TermAst Make(string op, List<Z3TermAst> children) {
- return new Z3StubTermAst();
- }
- public Z3TermAst MakeArraySelect(List<Z3TermAst> args)
- {
- return new Z3StubTermAst();
- }
- public Z3TermAst MakeArrayStore(List<Z3TermAst> args)
- {
- return new Z3StubTermAst();
- }
- }
+using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using System.Diagnostics; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.Z3; +using Microsoft.Z3; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.Z3 { + public class Z3StubContext : Z3Context { + class Z3StubPatternAst: Z3PatternAst {} + class Z3StubTermAst: Z3TermAst {} + class Z3StubLabeledLiterals: Z3LabeledLiterals {} + + public void CreateBacktrackPoint(){} + public void Backtrack(){} + public void AddAxiom(VCExpr axiom, LineariserOptions linOptions) { } + public void AddConjecture(VCExpr vc, LineariserOptions linOptions){} + public void AddSmtlibString(string smtlibString) {} + public string GetDeclName(Z3ConstDeclAst constDeclAst) { + return ""; + } + public Z3PatternAst MakePattern(List<Z3TermAst> exprs) { + return new Z3StubPatternAst(); + } + 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) { + return new Z3StubTermAst(); + } + public ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors) { + boogieErrors = new List<Z3ErrorModelAndLabels>(); + return ProverInterface.Outcome.Undetermined; + } + public void TypeCheckBool(Z3TermAst t){} + public void TypeCheckInt(Z3TermAst t){} + public void DeclareType(string typeName) {} + public void DeclareConstant(string constantName, Type boogieType) {} + public void DeclareFunction(string functionName, List<Type> domain, Type range) {} + public Z3TermAst GetConstant(string constantName, Type constantType) { + return new Z3StubTermAst(); + } + public Z3TermAst MakeIntLiteral(string numeral) { + return new Z3StubTermAst(); + } + public Z3TermAst MakeBvLiteral(int i, uint bvSize) { + return new Z3StubTermAst(); + } + public Z3TermAst MakeTrue() { + return new Z3StubTermAst(); + } + public Z3TermAst MakeFalse() { + return new Z3StubTermAst(); + } + public Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child) { + return new Z3StubTermAst(); + } + public Z3LabeledLiterals GetRelevantLabels() { + return new Z3StubLabeledLiterals(); + } + public Z3TermAst Make(string op, List<Z3TermAst> children) { + return new Z3StubTermAst(); + } + public Z3TermAst MakeArraySelect(List<Z3TermAst> args) + { + return new Z3StubTermAst(); + } + public Z3TermAst MakeArrayStore(List<Z3TermAst> args) + { + return new Z3StubTermAst(); + } + } }
\ No newline at end of file diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index 879211f7..f2a9a8fd 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -1,197 +1,197 @@ -using System;
-using System.Collections;
-using System.Collections.Generic;
-using System.Threading;
-using System.IO;
-using System.Diagnostics;
-using Microsoft.Boogie.AbstractInterpretation;
-using Microsoft.Boogie;
-using Microsoft.Boogie.Z3;
-using Microsoft.Z3;
-using Microsoft.Boogie.VCExprAST;
-
-namespace Microsoft.Boogie.Z3
-{
- internal class Z3TypeCachedBuilder
- {
- private class MapTypeComparator : IEqualityComparer<MapType>
- {
- public bool Equals(MapType x, MapType y)
- {
- if (x.MapArity != y.MapArity)
- return false;
- for (int i = 0; i < x.MapArity; i++)
- {
- if (!Equals(x.Arguments[i], y.Arguments[i]))
- return false;
- }
- return Equals(x.Result, y.Result);
-
- }
- public int GetHashCode(MapType mapType)
- {
- return mapType.GetHashCode();
- }
- }
-
- private class BvTypeComparator : IEqualityComparer<BvType>
- {
- public bool Equals(BvType x, BvType y)
- {
- return x.Bits == y.Bits;
- }
- public int GetHashCode(BvType bvType)
- {
- return bvType.Bits;
- }
- }
-
- private class BasicTypeComparator : IEqualityComparer<BasicType>
- {
- public bool Equals(BasicType x, BasicType y)
- {
- return (x.IsBool == y.IsBool) &&
- (x.IsInt == y.IsInt) &&
- (x.IsReal == y.IsReal);
- }
-
- public int GetHashCode(BasicType basicType)
- {
- if (basicType.IsBool)
- return 1;
- else if (basicType.IsInt)
- return 2;
- else if (basicType.IsReal)
- return 3;
- else
- throw new Exception("Basic Type " + basicType.ToString() + " is unkwown");
- }
- }
-
- 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 Z3apiProverContext container;
-
- public Z3TypeCachedBuilder(Z3apiProverContext context)
- {
- this.container = context;
- }
-
- private Sort GetMapType(MapType mapType) {
- Context z3 = ((Z3apiProverContext)container).z3;
- if (!mapTypes.ContainsKey(mapType)) {
- Type result = mapType.Result;
- for (int i = mapType.Arguments.Length-1; i > 0; i--) {
- GetType(result);
- result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result);
- }
- mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result)));
- }
- return mapTypes[mapType];
- }
-
- private Sort GetBvType(BvType bvType)
- {
- if (!bvTypes.ContainsKey(bvType))
- {
- Sort typeAst = BuildBvType(bvType);
- bvTypes.Add(bvType, typeAst);
- }
- Sort result;
- bool containsKey = bvTypes.TryGetValue(bvType, out result);
- Debug.Assert(containsKey);
- return result;
- }
-
- private Sort GetBasicType(BasicType basicType)
- {
- if (!basicTypes.ContainsKey(basicType))
- {
- Sort typeAst = BuildBasicType(basicType);
- basicTypes.Add(basicType, typeAst);
- }
- Sort result;
- bool containsKey = basicTypes.TryGetValue(basicType, out result);
- Debug.Assert(containsKey);
- return result;
- }
-
- 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;
- }
-
- 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 Sort BuildMapType(Sort domain, Sort range)
- {
- Context z3 = ((Z3apiProverContext)container).z3;
- return z3.MkArraySort(domain, range);
- }
-
- public Sort BuildBvType(BvType bvType)
- {
- Context z3 = ((Z3apiProverContext)container).z3;
- return z3.MkBvSort((uint)bvType.Bits);
- }
-
- public Sort BuildBasicType(BasicType basicType)
- {
- Context z3 = ((Z3apiProverContext)container).z3;
- Sort typeAst;
- if (basicType.IsBool)
- {
- typeAst = z3.MkBoolSort();
- }
- else if (basicType.IsInt)
- {
- typeAst = z3.MkIntSort();
- }
- else if (basicType.IsReal)
- {
- typeAst = z3.MkRealSort();
- }
- else
- throw new Exception("Unknown Basic Type " + basicType.ToString());
- return typeAst;
- }
-
- public Sort BuildCtorType(CtorType ctorType) {
- Context z3 = ((Z3apiProverContext)container).z3;
- if (ctorType.Arguments.Length > 0)
- throw new Exception("Type constructor of non-zero arity are not handled");
- return z3.MkSort(ctorType.Decl.Name);
- }
- }
+using System; +using System.Collections; +using System.Collections.Generic; +using System.Threading; +using System.IO; +using System.Diagnostics; +using Microsoft.Boogie.AbstractInterpretation; +using Microsoft.Boogie; +using Microsoft.Boogie.Z3; +using Microsoft.Z3; +using Microsoft.Boogie.VCExprAST; + +namespace Microsoft.Boogie.Z3 +{ + internal class Z3TypeCachedBuilder + { + private class MapTypeComparator : IEqualityComparer<MapType> + { + public bool Equals(MapType x, MapType y) + { + if (x.MapArity != y.MapArity) + return false; + for (int i = 0; i < x.MapArity; i++) + { + if (!Equals(x.Arguments[i], y.Arguments[i])) + return false; + } + return Equals(x.Result, y.Result); + + } + public int GetHashCode(MapType mapType) + { + return mapType.GetHashCode(); + } + } + + private class BvTypeComparator : IEqualityComparer<BvType> + { + public bool Equals(BvType x, BvType y) + { + return x.Bits == y.Bits; + } + public int GetHashCode(BvType bvType) + { + return bvType.Bits; + } + } + + private class BasicTypeComparator : IEqualityComparer<BasicType> + { + public bool Equals(BasicType x, BasicType y) + { + return (x.IsBool == y.IsBool) && + (x.IsInt == y.IsInt) && + (x.IsReal == y.IsReal); + } + + public int GetHashCode(BasicType basicType) + { + if (basicType.IsBool) + return 1; + else if (basicType.IsInt) + return 2; + else if (basicType.IsReal) + return 3; + else + throw new Exception("Basic Type " + basicType.ToString() + " is unkwown"); + } + } + + 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 Z3apiProverContext container; + + public Z3TypeCachedBuilder(Z3apiProverContext context) + { + this.container = context; + } + + private Sort GetMapType(MapType mapType) { + Context z3 = ((Z3apiProverContext)container).z3; + if (!mapTypes.ContainsKey(mapType)) { + Type result = mapType.Result; + for (int i = mapType.Arguments.Length-1; i > 0; i--) { + GetType(result); + result = new MapType(mapType.tok, new TypeVariableSeq(), new TypeSeq(mapType.Arguments[i]), result); + } + mapTypes.Add(mapType, BuildMapType(GetType(mapType.Arguments[0]), GetType(result))); + } + return mapTypes[mapType]; + } + + private Sort GetBvType(BvType bvType) + { + if (!bvTypes.ContainsKey(bvType)) + { + Sort typeAst = BuildBvType(bvType); + bvTypes.Add(bvType, typeAst); + } + Sort result; + bool containsKey = bvTypes.TryGetValue(bvType, out result); + Debug.Assert(containsKey); + return result; + } + + private Sort GetBasicType(BasicType basicType) + { + if (!basicTypes.ContainsKey(basicType)) + { + Sort typeAst = BuildBasicType(basicType); + basicTypes.Add(basicType, typeAst); + } + Sort result; + bool containsKey = basicTypes.TryGetValue(basicType, out result); + Debug.Assert(containsKey); + return result; + } + + 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; + } + + 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 Sort BuildMapType(Sort domain, Sort range) + { + Context z3 = ((Z3apiProverContext)container).z3; + return z3.MkArraySort(domain, range); + } + + public Sort BuildBvType(BvType bvType) + { + Context z3 = ((Z3apiProverContext)container).z3; + return z3.MkBvSort((uint)bvType.Bits); + } + + public Sort BuildBasicType(BasicType basicType) + { + Context z3 = ((Z3apiProverContext)container).z3; + Sort typeAst; + if (basicType.IsBool) + { + typeAst = z3.MkBoolSort(); + } + else if (basicType.IsInt) + { + typeAst = z3.MkIntSort(); + } + else if (basicType.IsReal) + { + typeAst = z3.MkRealSort(); + } + else + throw new Exception("Unknown Basic Type " + basicType.ToString()); + return typeAst; + } + + public Sort BuildCtorType(CtorType ctorType) { + Context z3 = ((Z3apiProverContext)container).z3; + if (ctorType.Arguments.Length > 0) + throw new Exception("Type constructor of non-zero arity are not handled"); + return z3.MkSort(ctorType.Decl.Name); + } + } }
\ No newline at end of file diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index e56a7950..52c7d8fd 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -1,649 +1,649 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-using System;
-using System.Text;
-using System.IO;
-using System.Collections;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using Microsoft.Basetypes;
-using Microsoft.Boogie.VCExprAST;
-using Microsoft.Z3;
-
-namespace Microsoft.Boogie.Z3
-{
- using System.Numerics.BigInteger;
-
- public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>
- {
- private Z3apiOpLineariser opLineariser = null;
- private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser
- {
- get
- {
- Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null);
- if (opLineariser == null)
- opLineariser = new Z3apiOpLineariser(this);
- return opLineariser;
- }
- }
-
- internal readonly UniqueNamer namer;
- internal readonly Dictionary<VCExprVar, Term> letBindings;
- protected Z3apiProverContext cm;
-
- public Z3apiExprLineariser(Z3apiProverContext cm, UniqueNamer namer)
- {
- this.cm = cm;
- this.namer = namer;
- this.letBindings = new Dictionary<VCExprVar, Term>();
- }
-
- public Term Linearise(VCExpr expr, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(expr != null);
- return expr.Accept<Term, LineariserOptions>(this, options);
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- public Term Make(VCExprOp op, List<Term> children) {
- Context z3 = cm.z3;
- Term[] unwrapChildren = children.ToArray();
- VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp;
- if (boogieFunctionOp != null) {
- FuncDecl f = cm.GetFunction(boogieFunctionOp.Func.Name);
- return z3.MkApp(f, unwrapChildren);
- }
- VCExprDistinctOp distinctOp = op as VCExprDistinctOp;
- if (distinctOp != null) {
- return z3.MkDistinct(unwrapChildren);
- }
-
- if (op == VCExpressionGenerator.AndOp) {
- return z3.MkAnd(unwrapChildren);
- }
-
- if (op == VCExpressionGenerator.OrOp) {
- return z3.MkOr(unwrapChildren);
- }
-
- if (op == VCExpressionGenerator.ImpliesOp) {
- return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.NotOp) {
- return z3.MkNot(unwrapChildren[0]);
- }
-
- if (op == VCExpressionGenerator.EqOp) {
- return z3.MkEq(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.NeqOp) {
- return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1]));
- }
-
- if (op == VCExpressionGenerator.LtOp) {
- return z3.MkLt(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.LeOp) {
- return z3.MkLe(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.GtOp) {
- return z3.MkGt(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.GeOp) {
- return z3.MkGe(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.AddOp) {
- return z3.MkAdd(unwrapChildren);
- }
-
- if (op == VCExpressionGenerator.SubOp) {
- return z3.MkSub(unwrapChildren);
- }
-
- if (op == VCExpressionGenerator.DivOp || op == VCExpressionGenerator.RealDivOp) {
- return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.MulOp) {
- return z3.MkMul(unwrapChildren);
- }
-
- if (op == VCExpressionGenerator.ModOp) {
- return z3.MkMod(unwrapChildren[0], unwrapChildren[1]);
- }
-
- if (op == VCExpressionGenerator.IfThenElseOp) {
- return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);
- }
-
- if (op == VCExpressionGenerator.ToIntOp) {
- return z3.MkToInt(unwrapChildren[0]);
- }
-
- if (op == VCExpressionGenerator.ToRealOp) {
- return z3.MkToReal(unwrapChildren[0]);
- }
-
- throw new Exception("unhandled boogie operator");
- }
-
- public Term Visit(VCExprLiteral node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
-
- if (node == VCExpressionGenerator.True)
- return cm.z3.MkTrue();
- else if (node == VCExpressionGenerator.False)
- return cm.z3.MkFalse();
- else if (node is VCExprIntLit)
- return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());
- else if (node is VCExprRealLit) {
- string m = ((VCExprRealLit)node).Val.Mantissa.ToString();
- BigInteger e = ((VCExprRealLit)node).Val.Exponent;
- string f = BigInteger.Pow(10, e.Abs);
-
- if (e == 0) {
- return cm.z3.MkNumeral(m, cm.z3.MkRealSort());
- }
- else if (((VCExprRealLit)node).Val.Exponent > 0) {
- return cm.z3.MkMul(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));
- }
- else {
- return cm.z3.MkDiv(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));
- }
- }
- else {
- Contract.Assert(false);
- throw new cce.UnreachableException();
- }
- }
-
- public Term Visit(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- VCExprOp op = node.Op;
- Contract.Assert(op != null);
-
- if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp))
- {
- // handle these operators without recursion
- List<Term> asts = new List<Term>();
- string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR";
-
- IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node);
- Contract.Assert(enumerator != null);
- while (enumerator.MoveNext())
- {
- VCExprNAry naryExpr = enumerator.Current as VCExprNAry;
- if (naryExpr == null || !naryExpr.Op.Equals(op))
- {
- asts.Add(Linearise(cce.NonNull((VCExpr)enumerator.Current), options));
- }
- }
-
- return Make(op, asts);
- }
-
- return node.Accept<Term, LineariserOptions>(OpLineariser, options);
- }
-
- public Term Visit(VCExprVar node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- if (letBindings.ContainsKey(node))
- {
- return letBindings[node];
- }
- else
- {
- string varName = namer.GetName(node, node.Name);
- return cm.GetConstant(varName, node.Type,node);
- }
- }
-
- public Term Visit(VCExprQuantifier node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- Contract.Assert(node.TypeParameters.Count == 0);
-
- namer.PushScope();
- try
- {
- List<string> varNames;
- List<Type> varTypes;
- VisitBounds(node.BoundVars, out varNames, out varTypes);
- List<Pattern> patterns;
- List<Term> no_patterns;
- VisitTriggers(node.Triggers, options, out patterns, out no_patterns);
- Term body = Linearise(node.Body, options);
- Term result;
- uint weight = 1;
- string qid = "";
- int skolemid = 0;
-
- if (options.QuantifierIds)
- {
- VCQuantifierInfos infos = node.Infos;
- Contract.Assert(infos != null);
- if (infos.qid != null)
- {
- qid = infos.qid;
- }
- if (0 <= infos.uniqueId)
- {
- skolemid = infos.uniqueId;
- }
- }
-
- if (options.UseWeights)
- {
- weight = (uint) QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1);
- }
-
- switch (node.Quan)
- {
- case Microsoft.Boogie.VCExprAST.Quantifier.ALL:
- result = MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
- case Microsoft.Boogie.VCExprAST.Quantifier.EX:
- result = MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break;
- default:
- throw new Exception("unknown quantifier kind " + node.Quan);
- }
- return result;
- }
- finally
- {
- namer.PopScope();
- }
- }
-
- private 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 = cm.GetConstant(varNames[i], boogieTypes[i], null);
- bound.Add(t);
- }
-
- Term termAst = cm.z3.MkQuantifier(isForall, weight, cm.z3.MkSymbol(qid), cm.z3.MkSymbol(skolemid.ToString()), patterns.ToArray(), no_patterns.ToArray(), bound.ToArray(), body);
- return termAst;
- }
-
- private void VisitBounds(List<VCExprVar> boundVars, out List<string> varNames, out List<Type> varTypes)
- {
- varNames = new List<string>();
- varTypes = new List<Type>();
- foreach (VCExprVar var in boundVars)
- {
- string varName = namer.GetLocalName(var, var.Name);
- varNames.Add(varName);
- varTypes.Add(var.Type);
- }
- }
-
- private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Pattern> patterns, out List<Term> no_patterns)
- {
- patterns = new List<Pattern>();
- no_patterns = new List<Term>();
- foreach (VCTrigger trigger in triggers)
- {
- List<Term> exprs = new List<Term>();
- foreach (VCExpr expr in trigger.Exprs)
- {
- System.Diagnostics.Debug.Assert(expr != null);
- Term termAst = Linearise(expr, options);
- exprs.Add(termAst);
- }
- if (exprs.Count > 0)
- {
- if (trigger.Pos) {
- Pattern pattern = cm.z3.MkPattern(exprs.ToArray());
- patterns.Add(pattern);
- }
- else {
- System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats");
- foreach (Term expr in exprs)
- no_patterns.Add(expr);
- }
- }
- }
- }
-
- public Term Visit(VCExprLet node, LineariserOptions options)
- {
- foreach (VCExprLetBinding b in node)
- {
- Term defAst = Linearise(b.E, options);
- letBindings.Add(b.V, defAst);
- }
- Term letAst = Linearise(node.Body, options);
- foreach (VCExprLetBinding b in node)
- {
- letBindings.Remove(b.V);
- }
- return letAst;
- }
-
- /////////////////////////////////////////////////////////////////////////////////////
-
- internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions>
- {
- [ContractInvariantMethod]
- void ObjectInvariant()
- {
- Contract.Invariant(ExprLineariser != null);
- }
-
- private readonly Z3apiExprLineariser ExprLineariser;
-
- public Z3apiOpLineariser(Z3apiExprLineariser ExprLineariser)
- {
- Contract.Requires(ExprLineariser != null);
- this.ExprLineariser = ExprLineariser;
- }
-
- ///////////////////////////////////////////////////////////////////////////////////
-
- private Term WriteApplication(VCExprOp op, IEnumerable<VCExpr> terms, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(op != null);
- Contract.Requires(cce.NonNullElements(terms));
-
- List<Term> args = new List<Term>();
- foreach (VCExpr e in terms)
- {
- Contract.Assert(e != null);
- args.Add(ExprLineariser.Linearise(e, options));
- }
- return ExprLineariser.Make(op, args);
- }
-
- ///////////////////////////////////////////////////////////////////////////////////
-
- public Term VisitNotOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitEqOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitNeqOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitAndOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitOrOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitLabelOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- VCExprLabelOp op = (VCExprLabelOp)node.Op;
- Contract.Assert(op != null);
- return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options));
- }
-
- public Term VisitSelectOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != 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);
-
- Term selectTerm = args[0];
- for (int i = 1; i < args.Count; i++) {
- selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]);
- }
- return selectTerm;
- }
-
- private Term ConstructStoreTerm(Term mapTerm, List<Term> args, int index) {
- System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1);
- if (index == args.Count - 2) {
- return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]);
- }
- else {
- Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1);
- return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t);
- }
- }
-
- public Term VisitStoreOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- List<Term> args = new List<Term>();
- foreach (VCExpr e in node)
- {
- Contract.Assert(e != null);
- args.Add(ExprLineariser.Linearise(e, options));
- }
- return ConstructStoreTerm(args[0], args, 1);
- }
-
- public Term VisitBvOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- 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 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 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 Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitCustomOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(node != null);
- Contract.Requires(options != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitAddOp(VCExprNAry node, LineariserOptions options) {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitSubOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitMulOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitDivOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitModOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitRealDivOp(VCExprNAry node, LineariserOptions options) {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitPowOp(VCExprNAry node, LineariserOptions options) {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitLtOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitLeOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitGtOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitGeOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitToIntOp(VCExprNAry node, LineariserOptions options) {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitToRealOp(VCExprNAry node, LineariserOptions options) {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
-
- public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
- {
- Contract.Requires(options != null);
- Contract.Requires(node != null);
- return WriteApplication(node.Op, node, options);
- }
- }
- }
-}
+//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// +//----------------------------------------------------------------------------- +using System; +using System.Text; +using System.IO; +using System.Collections; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using Microsoft.Basetypes; +using Microsoft.Boogie.VCExprAST; +using Microsoft.Z3; + +namespace Microsoft.Boogie.Z3 +{ + using System.Numerics.BigInteger; + + public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions> + { + private Z3apiOpLineariser opLineariser = null; + private IVCExprOpVisitor<Term, LineariserOptions> OpLineariser + { + get + { + Contract.Ensures(Contract.Result<IVCExprOpVisitor<bool, LineariserOptions>>() != null); + if (opLineariser == null) + opLineariser = new Z3apiOpLineariser(this); + return opLineariser; + } + } + + internal readonly UniqueNamer namer; + internal readonly Dictionary<VCExprVar, Term> letBindings; + protected Z3apiProverContext cm; + + public Z3apiExprLineariser(Z3apiProverContext cm, UniqueNamer namer) + { + this.cm = cm; + this.namer = namer; + this.letBindings = new Dictionary<VCExprVar, Term>(); + } + + public Term Linearise(VCExpr expr, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(expr != null); + return expr.Accept<Term, LineariserOptions>(this, options); + } + + ///////////////////////////////////////////////////////////////////////////////////// + + public Term Make(VCExprOp op, List<Term> children) { + Context z3 = cm.z3; + Term[] unwrapChildren = children.ToArray(); + VCExprBoogieFunctionOp boogieFunctionOp = op as VCExprBoogieFunctionOp; + if (boogieFunctionOp != null) { + FuncDecl f = cm.GetFunction(boogieFunctionOp.Func.Name); + return z3.MkApp(f, unwrapChildren); + } + VCExprDistinctOp distinctOp = op as VCExprDistinctOp; + if (distinctOp != null) { + return z3.MkDistinct(unwrapChildren); + } + + if (op == VCExpressionGenerator.AndOp) { + return z3.MkAnd(unwrapChildren); + } + + if (op == VCExpressionGenerator.OrOp) { + return z3.MkOr(unwrapChildren); + } + + if (op == VCExpressionGenerator.ImpliesOp) { + return z3.MkImplies(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.NotOp) { + return z3.MkNot(unwrapChildren[0]); + } + + if (op == VCExpressionGenerator.EqOp) { + return z3.MkEq(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.NeqOp) { + return z3.MkNot(z3.MkEq(unwrapChildren[0], unwrapChildren[1])); + } + + if (op == VCExpressionGenerator.LtOp) { + return z3.MkLt(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.LeOp) { + return z3.MkLe(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.GtOp) { + return z3.MkGt(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.GeOp) { + return z3.MkGe(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.AddOp) { + return z3.MkAdd(unwrapChildren); + } + + if (op == VCExpressionGenerator.SubOp) { + return z3.MkSub(unwrapChildren); + } + + if (op == VCExpressionGenerator.DivOp || op == VCExpressionGenerator.RealDivOp) { + return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.MulOp) { + return z3.MkMul(unwrapChildren); + } + + if (op == VCExpressionGenerator.ModOp) { + return z3.MkMod(unwrapChildren[0], unwrapChildren[1]); + } + + if (op == VCExpressionGenerator.IfThenElseOp) { + return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]); + } + + if (op == VCExpressionGenerator.ToIntOp) { + return z3.MkToInt(unwrapChildren[0]); + } + + if (op == VCExpressionGenerator.ToRealOp) { + return z3.MkToReal(unwrapChildren[0]); + } + + throw new Exception("unhandled boogie operator"); + } + + public Term Visit(VCExprLiteral node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + + if (node == VCExpressionGenerator.True) + return cm.z3.MkTrue(); + else if (node == VCExpressionGenerator.False) + return cm.z3.MkFalse(); + else if (node is VCExprIntLit) + return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort()); + else if (node is VCExprRealLit) { + string m = ((VCExprRealLit)node).Val.Mantissa.ToString(); + BigInteger e = ((VCExprRealLit)node).Val.Exponent; + string f = BigInteger.Pow(10, e.Abs); + + if (e == 0) { + return cm.z3.MkNumeral(m, cm.z3.MkRealSort()); + } + else if (((VCExprRealLit)node).Val.Exponent > 0) { + return cm.z3.MkMul(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort())); + } + else { + return cm.z3.MkDiv(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort())); + } + } + else { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + } + + public Term Visit(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + VCExprOp op = node.Op; + Contract.Assert(op != null); + + if (op.Equals(VCExpressionGenerator.AndOp) || op.Equals(VCExpressionGenerator.OrOp)) + { + // handle these operators without recursion + List<Term> asts = new List<Term>(); + string opString = op.Equals(VCExpressionGenerator.AndOp) ? "AND" : "OR"; + + IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node); + Contract.Assert(enumerator != null); + while (enumerator.MoveNext()) + { + VCExprNAry naryExpr = enumerator.Current as VCExprNAry; + if (naryExpr == null || !naryExpr.Op.Equals(op)) + { + asts.Add(Linearise(cce.NonNull((VCExpr)enumerator.Current), options)); + } + } + + return Make(op, asts); + } + + return node.Accept<Term, LineariserOptions>(OpLineariser, options); + } + + public Term Visit(VCExprVar node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + if (letBindings.ContainsKey(node)) + { + return letBindings[node]; + } + else + { + string varName = namer.GetName(node, node.Name); + return cm.GetConstant(varName, node.Type,node); + } + } + + public Term Visit(VCExprQuantifier node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + Contract.Assert(node.TypeParameters.Count == 0); + + namer.PushScope(); + try + { + List<string> varNames; + List<Type> varTypes; + VisitBounds(node.BoundVars, out varNames, out varTypes); + List<Pattern> patterns; + List<Term> no_patterns; + VisitTriggers(node.Triggers, options, out patterns, out no_patterns); + Term body = Linearise(node.Body, options); + Term result; + uint weight = 1; + string qid = ""; + int skolemid = 0; + + if (options.QuantifierIds) + { + VCQuantifierInfos infos = node.Infos; + Contract.Assert(infos != null); + if (infos.qid != null) + { + qid = infos.qid; + } + if (0 <= infos.uniqueId) + { + skolemid = infos.uniqueId; + } + } + + if (options.UseWeights) + { + weight = (uint) QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1); + } + + switch (node.Quan) + { + case Microsoft.Boogie.VCExprAST.Quantifier.ALL: + result = MakeQuantifier(true, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break; + case Microsoft.Boogie.VCExprAST.Quantifier.EX: + result = MakeQuantifier(false, weight, qid, skolemid, varNames, varTypes, patterns, no_patterns, body); break; + default: + throw new Exception("unknown quantifier kind " + node.Quan); + } + return result; + } + finally + { + namer.PopScope(); + } + } + + private 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 = cm.GetConstant(varNames[i], boogieTypes[i], null); + bound.Add(t); + } + + Term termAst = cm.z3.MkQuantifier(isForall, weight, cm.z3.MkSymbol(qid), cm.z3.MkSymbol(skolemid.ToString()), patterns.ToArray(), no_patterns.ToArray(), bound.ToArray(), body); + return termAst; + } + + private void VisitBounds(List<VCExprVar> boundVars, out List<string> varNames, out List<Type> varTypes) + { + varNames = new List<string>(); + varTypes = new List<Type>(); + foreach (VCExprVar var in boundVars) + { + string varName = namer.GetLocalName(var, var.Name); + varNames.Add(varName); + varTypes.Add(var.Type); + } + } + + private void VisitTriggers(List<VCTrigger> triggers, LineariserOptions options, out List<Pattern> patterns, out List<Term> no_patterns) + { + patterns = new List<Pattern>(); + no_patterns = new List<Term>(); + foreach (VCTrigger trigger in triggers) + { + List<Term> exprs = new List<Term>(); + foreach (VCExpr expr in trigger.Exprs) + { + System.Diagnostics.Debug.Assert(expr != null); + Term termAst = Linearise(expr, options); + exprs.Add(termAst); + } + if (exprs.Count > 0) + { + if (trigger.Pos) { + Pattern pattern = cm.z3.MkPattern(exprs.ToArray()); + patterns.Add(pattern); + } + else { + System.Diagnostics.Debug.Assert(false, "Z3api currently does not handle nopats"); + foreach (Term expr in exprs) + no_patterns.Add(expr); + } + } + } + } + + public Term Visit(VCExprLet node, LineariserOptions options) + { + foreach (VCExprLetBinding b in node) + { + Term defAst = Linearise(b.E, options); + letBindings.Add(b.V, defAst); + } + Term letAst = Linearise(node.Body, options); + foreach (VCExprLetBinding b in node) + { + letBindings.Remove(b.V); + } + return letAst; + } + + ///////////////////////////////////////////////////////////////////////////////////// + + internal class Z3apiOpLineariser : IVCExprOpVisitor<Term, LineariserOptions> + { + [ContractInvariantMethod] + void ObjectInvariant() + { + Contract.Invariant(ExprLineariser != null); + } + + private readonly Z3apiExprLineariser ExprLineariser; + + public Z3apiOpLineariser(Z3apiExprLineariser ExprLineariser) + { + Contract.Requires(ExprLineariser != null); + this.ExprLineariser = ExprLineariser; + } + + /////////////////////////////////////////////////////////////////////////////////// + + private Term WriteApplication(VCExprOp op, IEnumerable<VCExpr> terms, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(op != null); + Contract.Requires(cce.NonNullElements(terms)); + + List<Term> args = new List<Term>(); + foreach (VCExpr e in terms) + { + Contract.Assert(e != null); + args.Add(ExprLineariser.Linearise(e, options)); + } + return ExprLineariser.Make(op, args); + } + + /////////////////////////////////////////////////////////////////////////////////// + + public Term VisitNotOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitEqOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitNeqOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitAndOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitOrOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitImpliesOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitDistinctOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitLabelOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + VCExprLabelOp op = (VCExprLabelOp)node.Op; + Contract.Assert(op != null); + return ExprLineariser.cm.MakeLabel(op.label, op.pos, ExprLineariser.Linearise(node[0], options)); + } + + public Term VisitSelectOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != 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); + + Term selectTerm = args[0]; + for (int i = 1; i < args.Count; i++) { + selectTerm = ExprLineariser.cm.z3.MkArraySelect(selectTerm, args[i]); + } + return selectTerm; + } + + private Term ConstructStoreTerm(Term mapTerm, List<Term> args, int index) { + System.Diagnostics.Debug.Assert(0 < index && index < args.Count - 1); + if (index == args.Count - 2) { + return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], args[index + 1]); + } + else { + Term t = ConstructStoreTerm(ExprLineariser.cm.z3.MkArraySelect(mapTerm, args[index]), args, index + 1); + return ExprLineariser.cm.z3.MkArrayStore(mapTerm, args[index], t); + } + } + + public Term VisitStoreOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + List<Term> args = new List<Term>(); + foreach (VCExpr e in node) + { + Contract.Assert(e != null); + args.Add(ExprLineariser.Linearise(e, options)); + } + return ConstructStoreTerm(args[0], args, 1); + } + + public Term VisitBvOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + 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 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 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 Term VisitIfThenElseOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitCustomOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(node != null); + Contract.Requires(options != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitAddOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitSubOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitMulOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitDivOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitModOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitRealDivOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitPowOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitLtOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitLeOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitGtOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitGeOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitSubtypeOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitSubtype3Op(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitToIntOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitToRealOp(VCExprNAry node, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + + public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) + { + Contract.Requires(options != null); + Contract.Requires(node != null); + return WriteApplication(node.Op, node, options); + } + } + } +} diff --git a/Source/Provers/Z3api/Z3api.csproj b/Source/Provers/Z3api/Z3api.csproj index 1627536d..3fb2fe48 100644 --- a/Source/Provers/Z3api/Z3api.csproj +++ b/Source/Provers/Z3api/Z3api.csproj @@ -1,189 +1,189 @@ -<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
- <PropertyGroup>
- <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
- <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
- <ProductVersion>9.0.21022</ProductVersion>
- <SchemaVersion>2.0</SchemaVersion>
- <ProjectGuid>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid>
- <OutputType>Library</OutputType>
- <AppDesignerFolder>Properties</AppDesignerFolder>
- <RootNamespace>Microsoft.Boogie.Z3api</RootNamespace>
- <AssemblyName>Provers.Z3api</AssemblyName>
- <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
- <FileAlignment>512</FileAlignment>
- <StartupObject>
- </StartupObject>
- <FileUpgradeFlags>
- </FileUpgradeFlags>
- <OldToolsVersion>3.5</OldToolsVersion>
- <UpgradeBackupLocation />
- <PublishUrl>publish\</PublishUrl>
- <Install>true</Install>
- <InstallFrom>Disk</InstallFrom>
- <UpdateEnabled>false</UpdateEnabled>
- <UpdateMode>Foreground</UpdateMode>
- <UpdateInterval>7</UpdateInterval>
- <UpdateIntervalUnits>Days</UpdateIntervalUnits>
- <UpdatePeriodically>false</UpdatePeriodically>
- <UpdateRequired>false</UpdateRequired>
- <MapFileExtensions>true</MapFileExtensions>
- <ApplicationRevision>0</ApplicationRevision>
- <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
- <IsWebBootstrapper>false</IsWebBootstrapper>
- <UseApplicationTrust>false</UseApplicationTrust>
- <BootstrapperEnabled>true</BootstrapperEnabled>
- <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile>
- <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <DebugType>full</DebugType>
- <Optimize>false</Optimize>
- <OutputPath>bin\Debug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
- <DebugType>pdbonly</DebugType>
- <Optimize>true</Optimize>
- <OutputPath>bin\Release\</OutputPath>
- <DefineConstants>TRACE</DefineConstants>
- <ErrorReport>prompt</ErrorReport>
- <WarningLevel>4</WarningLevel>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- </PropertyGroup>
- <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\z3apidebug\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisRuleAssemblies>
- </CodeAnalysisRuleAssemblies>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>Migrated rules for Z3api.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
- </PropertyGroup>
- <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
- <DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\Checked\</OutputPath>
- <DefineConstants>DEBUG;TRACE</DefineConstants>
- <DebugType>full</DebugType>
- <PlatformTarget>AnyCPU</PlatformTarget>
- <CodeAnalysisLogFile>bin\Debug\Provers.Z3api.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
- <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
- <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
- <ErrorReport>prompt</ErrorReport>
- <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
- <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
- <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
- <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
- <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
- <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
- <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
- <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
- <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
- <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
- <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
- <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
- <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
- <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
- <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
- <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
- <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
- <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
- <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
- <CodeContractsCustomRewriterAssembly />
- <CodeContractsCustomRewriterClass />
- <CodeContractsLibPaths />
- <CodeContractsExtraRewriteOptions />
- <CodeContractsExtraAnalysisOptions />
- <CodeContractsBaseLineFile />
- <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
- <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
- <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
- <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
- </PropertyGroup>
- <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
- <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
- Other similar extension points exist, see Microsoft.Common.targets.
- <Target Name="BeforeBuild">
- </Target>
- <Target Name="AfterBuild">
- </Target>
- -->
- <ItemGroup>
- <Reference Include="ManagedAPI">
- <HintPath>..\..\..\..\..\iZ3\win\iZ3\Debug\ManagedAPI.dll</HintPath>
- </Reference>
- <Reference Include="System" />
- <Reference Include="System.Core">
- <RequiredTargetFramework>3.5</RequiredTargetFramework>
- </Reference>
- <Reference Include="System.Data" />
- <Reference Include="System.XML" />
- </ItemGroup>
- <ItemGroup>
- <ProjectReference Include="..\..\Basetypes\Basetypes.csproj">
- <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project>
- <Name>Basetypes</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj">
- <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
- <Name>CodeContractsExtender</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\Core\Core.csproj">
- <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>
- <Name>Core</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\Model\Model.csproj">
- <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>
- <Name>Model</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">
- <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>
- <Name>ParserHelper</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">
- <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>
- <Name>VCExpr</Name>
- </ProjectReference>
- <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj">
- <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>
- <Name>VCGeneration</Name>
- </ProjectReference>
- </ItemGroup>
- <ItemGroup>
- <Compile Include="..\..\version.cs">
- <Link>version.cs</Link>
- </Compile>
- <Compile Include="ContextLayer.cs" />
- <Compile Include="ProverLayer.cs" />
- <Compile Include="TypeAdapter.cs">
- <SubType>Code</SubType>
- </Compile>
- <Compile Include="VCExprVisitor.cs" />
- </ItemGroup>
- <ItemGroup>
- <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
- <Install>false</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
- <Visible>False</Visible>
- <ProductName>.NET Framework 3.5 SP1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
- <Visible>False</Visible>
- <ProductName>Windows Installer 3.1</ProductName>
- <Install>true</Install>
- </BootstrapperPackage>
- </ItemGroup>
+<?xml version="1.0" encoding="utf-8"?> +<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003"> + <PropertyGroup> + <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration> + <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform> + <ProductVersion>9.0.21022</ProductVersion> + <SchemaVersion>2.0</SchemaVersion> + <ProjectGuid>{966DD87B-A29D-4F3C-9406-F680A61DC0E0}</ProjectGuid> + <OutputType>Library</OutputType> + <AppDesignerFolder>Properties</AppDesignerFolder> + <RootNamespace>Microsoft.Boogie.Z3api</RootNamespace> + <AssemblyName>Provers.Z3api</AssemblyName> + <TargetFrameworkVersion>v4.0</TargetFrameworkVersion> + <FileAlignment>512</FileAlignment> + <StartupObject> + </StartupObject> + <FileUpgradeFlags> + </FileUpgradeFlags> + <OldToolsVersion>3.5</OldToolsVersion> + <UpgradeBackupLocation /> + <PublishUrl>publish\</PublishUrl> + <Install>true</Install> + <InstallFrom>Disk</InstallFrom> + <UpdateEnabled>false</UpdateEnabled> + <UpdateMode>Foreground</UpdateMode> + <UpdateInterval>7</UpdateInterval> + <UpdateIntervalUnits>Days</UpdateIntervalUnits> + <UpdatePeriodically>false</UpdatePeriodically> + <UpdateRequired>false</UpdateRequired> + <MapFileExtensions>true</MapFileExtensions> + <ApplicationRevision>0</ApplicationRevision> + <ApplicationVersion>1.0.0.%2a</ApplicationVersion> + <IsWebBootstrapper>false</IsWebBootstrapper> + <UseApplicationTrust>false</UseApplicationTrust> + <BootstrapperEnabled>true</BootstrapperEnabled> + <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'" >Client</TargetFrameworkProfile> + <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' "> + <DebugSymbols>true</DebugSymbols> + <DebugType>full</DebugType> + <Optimize>false</Optimize> + <OutputPath>bin\Debug\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' "> + <DebugType>pdbonly</DebugType> + <Optimize>true</Optimize> + <OutputPath>bin\Release\</OutputPath> + <DefineConstants>TRACE</DefineConstants> + <ErrorReport>prompt</ErrorReport> + <WarningLevel>4</WarningLevel> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + </PropertyGroup> + <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' "> + <DebugSymbols>true</DebugSymbols> + <OutputPath>bin\z3apidebug\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>AnyCPU</PlatformTarget> + <CodeAnalysisRuleAssemblies> + </CodeAnalysisRuleAssemblies> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>Migrated rules for Z3api.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules> + </PropertyGroup> + <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'"> + <DebugSymbols>true</DebugSymbols> + <OutputPath>bin\Checked\</OutputPath> + <DefineConstants>DEBUG;TRACE</DefineConstants> + <DebugType>full</DebugType> + <PlatformTarget>AnyCPU</PlatformTarget> + <CodeAnalysisLogFile>bin\Debug\Provers.Z3api.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile> + <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression> + <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile> + <ErrorReport>prompt</ErrorReport> + <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet> + <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories> + <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories> + <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking> + <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface> + <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure> + <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires> + <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers> + <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis> + <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations> + <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations> + <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations> + <CodeContractsEnumObligations>False</CodeContractsEnumObligations> + <CodeContractsPointerObligations>False</CodeContractsPointerObligations> + <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions> + <CodeContractsRunInBackground>True</CodeContractsRunInBackground> + <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies> + <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine> + <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs> + <CodeContractsCustomRewriterAssembly /> + <CodeContractsCustomRewriterClass /> + <CodeContractsLibPaths /> + <CodeContractsExtraRewriteOptions /> + <CodeContractsExtraAnalysisOptions /> + <CodeContractsBaseLineFile /> + <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults> + <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel> + <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly> + <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel> + </PropertyGroup> + <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" /> + <!-- To modify your build process, add your task inside one of the targets below and uncomment it. + Other similar extension points exist, see Microsoft.Common.targets. + <Target Name="BeforeBuild"> + </Target> + <Target Name="AfterBuild"> + </Target> + --> + <ItemGroup> + <Reference Include="ManagedAPI"> + <HintPath>..\..\..\..\..\iZ3\win\iZ3\Debug\ManagedAPI.dll</HintPath> + </Reference> + <Reference Include="System" /> + <Reference Include="System.Core"> + <RequiredTargetFramework>3.5</RequiredTargetFramework> + </Reference> + <Reference Include="System.Data" /> + <Reference Include="System.XML" /> + </ItemGroup> + <ItemGroup> + <ProjectReference Include="..\..\Basetypes\Basetypes.csproj"> + <Project>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</Project> + <Name>Basetypes</Name> + </ProjectReference> + <ProjectReference Include="..\..\CodeContractsExtender\CodeContractsExtender.csproj"> + <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project> + <Name>CodeContractsExtender</Name> + </ProjectReference> + <ProjectReference Include="..\..\Core\Core.csproj"> + <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project> + <Name>Core</Name> + </ProjectReference> + <ProjectReference Include="..\..\Model\Model.csproj"> + <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project> + <Name>Model</Name> + </ProjectReference> + <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj"> + <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project> + <Name>ParserHelper</Name> + </ProjectReference> + <ProjectReference Include="..\..\VCExpr\VCExpr.csproj"> + <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project> + <Name>VCExpr</Name> + </ProjectReference> + <ProjectReference Include="..\..\VCGeneration\VCGeneration.csproj"> + <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project> + <Name>VCGeneration</Name> + </ProjectReference> + </ItemGroup> + <ItemGroup> + <Compile Include="..\..\version.cs"> + <Link>version.cs</Link> + </Compile> + <Compile Include="ContextLayer.cs" /> + <Compile Include="ProverLayer.cs" /> + <Compile Include="TypeAdapter.cs"> + <SubType>Code</SubType> + </Compile> + <Compile Include="VCExprVisitor.cs" /> + </ItemGroup> + <ItemGroup> + <BootstrapperPackage Include="Microsoft.Net.Client.3.5"> + <Visible>False</Visible> + <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName> + <Install>false</Install> + </BootstrapperPackage> + <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1"> + <Visible>False</Visible> + <ProductName>.NET Framework 3.5 SP1</ProductName> + <Install>true</Install> + </BootstrapperPackage> + <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1"> + <Visible>False</Visible> + <ProductName>Windows Installer 3.1</ProductName> + <Install>true</Install> + </BootstrapperPackage> + </ItemGroup> </Project>
\ No newline at end of file diff --git a/Source/Provers/Z3api/cce.cs b/Source/Provers/Z3api/cce.cs index ef594484..1e0b12a5 100644 --- a/Source/Provers/Z3api/cce.cs +++ b/Source/Provers/Z3api/cce.cs @@ -1,193 +1,193 @@ -using System;
-using SA=System.Attribute;
-using System.Collections.Generic;
-using System.Diagnostics.Contracts;
-using System.Text;
-//using Microsoft.Boogie;
-
-/// <summary>
-/// A class containing static methods to extend the functionality of Code Contracts
-/// </summary>
-
-public static class cce {
- //[Pure]
- //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
- // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
- //}
- [Pure]
- public static T NonNull<T>(T t) {
- Contract.Assert(t != null);
- return t;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection) {
- return collection != null && Contract.ForAll(collection, c => c != null);
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
- return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
- }
- //[Pure]
- //public static bool NonNullElements(VariableSeq collection) {
- // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
- //}
- /// <summary>
- /// For possibly-null lists of non-null elements
- /// </summary>
- /// <typeparam name="T"></typeparam>
- /// <param name="collection"></param>
- /// <param name="nullability">If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>!</param>
- /// <returns></returns>
- [Pure]
- public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
- return (nullability && collection == null) || cce.NonNullElements(collection);
- //Should be the same as:
- /*if(nullability&&collection==null)
- * return true;
- * return cce.NonNullElements(collection)
- */
-
- }
- [Pure]
- public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
- return kvp.Key != null && kvp.Value != null;
- }
- [Pure]
- public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
- return iEnumerator != null;
- }
- //[Pure]
- //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
- // return cce.NonNullElements(graph.TopologicalSort());
- //}
- [Pure]
- public static void BeginExpose(object o) {
- }
- [Pure]
- public static void EndExpose() {
- }
- [Pure]
- public static bool IsPeerConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsConsistent(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposable(object o) {
- return true;
- }
- [Pure]
- public static bool IsExposed(object o) {
- return true;
- }
- [Pure]
- public static bool IsNew(object o) {
- return true;
- }
- public static class Owner {
- [Pure]
- public static bool Same(object o, object p) {
- return true;
- }
- [Pure]
- public static void AssignSame(object o, object p) {
- }
- [Pure]
- public static object ElementProxy(object o) {
- return o;
- }
- [Pure]
- public static bool None(object o) {
- return true;
- }
- [Pure]
- public static bool Different(object o, object p) {
- return true;
- }
- [Pure]
- public static bool New(object o) {
- return true;
- }
- }
- [Pure]
- public static void LoopInvariant(bool p) {
- Contract.Assert(p);
- }
- public class UnreachableException : Exception {
- public UnreachableException() {
- }
- }
- //[Pure]
- //public static bool IsValid(Microsoft.Dafny.Expression expression) {
- // return true;
- //}
- //public static List<T> toList<T>(PureCollections.Sequence s) {
- // List<T> toRet = new List<T>();
- // foreach (T t in s.elems)
- // if(t!=null)
- // toRet.Add(t);
- // return toRet;
- //}
-
- //internal static bool NonNullElements(Set set) {
- // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
- //}
-}
-
-public class PeerAttribute : SA {
-}
-public class RepAttribute : SA {
-}
-public class CapturedAttribute : SA {
-}
-public class NotDelayedAttribute : SA {
-}
-public class NoDefaultContractAttribute : SA {
-}
-public class VerifyAttribute : SA {
- public VerifyAttribute(bool b) {
-
- }
-}
-public class StrictReadonlyAttribute : SA {
-}
-public class AdditiveAttribute : SA {
-}
-public class ReadsAttribute : SA {
- public enum Reads {
- Nothing,
- Everything,
- };
- public ReadsAttribute(object o) {
- }
-}
-public class GlobalAccessAttribute : SA {
- public GlobalAccessAttribute(bool b) {
- }
-}
-public class EscapesAttribute : SA {
- public EscapesAttribute(bool b, bool b_2) {
- }
-}
-public class NeedsContractsAttribute : SA {
- public NeedsContractsAttribute() {
- }
- public NeedsContractsAttribute(bool ret, bool parameters) {
- }
- public NeedsContractsAttribute(bool ret, int[] parameters) {
- }
-}
-public class ImmutableAttribute : SA {
-}
-public class InsideAttribute : SA {
-}
-public class SpecPublicAttribute : SA {
-}
-public class ElementsPeerAttribute : SA {
-}
-public class ResultNotNewlyAllocatedAttribute : SA {
-}
-public class OnceAttribute : SA {
+using System; +using SA=System.Attribute; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Text; +//using Microsoft.Boogie; + +/// <summary> +/// A class containing static methods to extend the functionality of Code Contracts +/// </summary> + +public static class cce { + //[Pure] + //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) { + // return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents()); + //} + [Pure] + public static T NonNull<T>(T t) { + Contract.Assert(t != null); + return t; + } + [Pure] + public static bool NonNullElements<T>(IEnumerable<T> collection) { + return collection != null && Contract.ForAll(collection, c => c != null); + } + [Pure] + public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) { + return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair)); + } + //[Pure] + //public static bool NonNullElements(VariableSeq collection) { + // return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null); + //} + /// <summary> + /// For possibly-null lists of non-null elements + /// </summary> + /// <typeparam name="T"></typeparam> + /// <param name="collection"></param> + /// <param name="nullability">If true, the collection is treated as an IEnumerable<T!>?, rather than an IEnumerable<T!>!</param> + /// <returns></returns> + [Pure] + public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) { + return (nullability && collection == null) || cce.NonNullElements(collection); + //Should be the same as: + /*if(nullability&&collection==null) + * return true; + * return cce.NonNullElements(collection) + */ + + } + [Pure] + public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) { + return kvp.Key != null && kvp.Value != null; + } + [Pure] + public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) { + return iEnumerator != null; + } + //[Pure] + //public static bool NonNullElements<T>(Graphing.Graph<T> graph) { + // return cce.NonNullElements(graph.TopologicalSort()); + //} + [Pure] + public static void BeginExpose(object o) { + } + [Pure] + public static void EndExpose() { + } + [Pure] + public static bool IsPeerConsistent(object o) { + return true; + } + [Pure] + public static bool IsConsistent(object o) { + return true; + } + [Pure] + public static bool IsExposable(object o) { + return true; + } + [Pure] + public static bool IsExposed(object o) { + return true; + } + [Pure] + public static bool IsNew(object o) { + return true; + } + public static class Owner { + [Pure] + public static bool Same(object o, object p) { + return true; + } + [Pure] + public static void AssignSame(object o, object p) { + } + [Pure] + public static object ElementProxy(object o) { + return o; + } + [Pure] + public static bool None(object o) { + return true; + } + [Pure] + public static bool Different(object o, object p) { + return true; + } + [Pure] + public static bool New(object o) { + return true; + } + } + [Pure] + public static void LoopInvariant(bool p) { + Contract.Assert(p); + } + public class UnreachableException : Exception { + public UnreachableException() { + } + } + //[Pure] + //public static bool IsValid(Microsoft.Dafny.Expression expression) { + // return true; + //} + //public static List<T> toList<T>(PureCollections.Sequence s) { + // List<T> toRet = new List<T>(); + // foreach (T t in s.elems) + // if(t!=null) + // toRet.Add(t); + // return toRet; + //} + + //internal static bool NonNullElements(Set set) { + // return set != null && Contract.ForAll(0,set.Count, i => set[i] != null); + //} +} + +public class PeerAttribute : SA { +} +public class RepAttribute : SA { +} +public class CapturedAttribute : SA { +} +public class NotDelayedAttribute : SA { +} +public class NoDefaultContractAttribute : SA { +} +public class VerifyAttribute : SA { + public VerifyAttribute(bool b) { + + } +} +public class StrictReadonlyAttribute : SA { +} +public class AdditiveAttribute : SA { +} +public class ReadsAttribute : SA { + public enum Reads { + Nothing, + Everything, + }; + public ReadsAttribute(object o) { + } +} +public class GlobalAccessAttribute : SA { + public GlobalAccessAttribute(bool b) { + } +} +public class EscapesAttribute : SA { + public EscapesAttribute(bool b, bool b_2) { + } +} +public class NeedsContractsAttribute : SA { + public NeedsContractsAttribute() { + } + public NeedsContractsAttribute(bool ret, bool parameters) { + } + public NeedsContractsAttribute(bool ret, int[] parameters) { + } +} +public class ImmutableAttribute : SA { +} +public class InsideAttribute : SA { +} +public class SpecPublicAttribute : SA { +} +public class ElementsPeerAttribute : SA { +} +public class ResultNotNewlyAllocatedAttribute : SA { +} +public class OnceAttribute : SA { }
\ No newline at end of file |