diff options
Diffstat (limited to 'Source/Provers/Z3api/ContextLayer.cs')
-rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 1454 |
1 files changed, 727 insertions, 727 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 |