diff options
Diffstat (limited to 'Source/Provers/Z3api/ContextLayer.cs')
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 699 |
1 files changed, 410 insertions, 289 deletions
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index 3a9c74ae..f0aa3906 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -11,330 +11,451 @@ using Microsoft.Z3; using Microsoft.Boogie.VCExprAST;
using Microsoft.Basetypes;
-namespace Microsoft.Boogie.Z3
-{
- public class Z3Config
- {
- private Config config = new Config();
- private int counterexamples;
- private string logFilename;
- private List<string> debugTraces = new List<string>();
-
- public void SetModelCompletion(bool enabled)
- {
- config.SetParamValue("MODEL_VALUE_COMPLETION", (enabled ? "true" : "false"));
- }
+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>();
+
+ 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)
+ z3.OpenLog(logFilename);
+ foreach (string tag in debugTraces)
+ z3.EnableDebugTrace(tag);
+
+ this.z3log = null;
+ this.tm = new Z3TypeCachedBuilder(this);
+ this.namer = new UniqueNamer();
+ }
- public void SetModel(bool enabled)
- {
- config.SetParamValue("MODEL", (enabled ? "true" : "false"));
- }
+ public override void DeclareType(TypeCtorDecl t, string attributes) {
+ base.DeclareType(t, attributes);
+ log("(declare-sort {0})", t.Name);
+ }
- public void SetSoftTimeout(string timeout)
- {
- config.SetParamValue("SOFT_TIMEOUT", timeout);
- }
+ public override void DeclareConstant(Constant c, bool uniq, string attributes) {
+ base.DeclareConstant(c, uniq, attributes);
+ DeclareConstant(c.Name, c.TypedIdent.Type);
+ }
- public void SetTypeCheck(bool enabled)
- {
- config.SetParamValue("TYPE_CHECK", (enabled ? "true" : "false"));
- }
+ 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);
+ log("(declare-funs (({0} {1} {2})))", functionName, domainStr, rangeAst);
+ }
- public void SetCounterExample(int counterexample)
- {
- this.counterexamples = counterexample;
- }
+ public override void DeclareGlobalVariable(GlobalVariable v, string attributes) {
+ base.DeclareGlobalVariable(v, attributes);
+ DeclareConstant(v.Name, v.TypedIdent.Type);
+ }
- public void SetLogFilename(string filename)
- {
- this.logFilename = filename;
- }
+ public override string Lookup(VCExprVar var) {
+ return namer.Lookup(var);
+ }
- public Config Config
- {
- get { return this.config; }
- }
- public int Counterexamples
- {
- get { return this.counterexamples; }
- }
- public string LogFilename
- {
- get { return this.logFilename; }
- }
+ 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 EnableDebugTrace(string debugTrace)
- {
- this.debugTraces.Add(debugTrace);
- }
+ public void CloseLog() {
+ z3.CloseLog();
+ if (z3log != null) {
+ z3log.Close();
+ }
+ z3log = null;
+ }
- public List<string> DebugTraces
- {
- get { return this.debugTraces; }
- }
+ public void CreateBacktrackPoint() {
+ symbols.CreateBacktrackPoint();
+ constants.CreateBacktrackPoint();
+ functions.CreateBacktrackPoint();
+ labels.CreateBacktrackPoint();
+ z3.Push();
+ log("(push)");
}
- public abstract class Z3TermAst { }
- public abstract class Z3PatternAst { }
- public abstract class Z3ConstDeclAst { }
- public abstract class Z3LabeledLiterals { }
-
- public interface Z3Context
- {
- void CreateBacktrackPoint();
- void Backtrack();
- void AddAxiom(VCExpr axiom, LineariserOptions linOptions);
- void AddConjecture(VCExpr vc, LineariserOptions linOptions);
- void AddSmtlibString(string smtlibString);
- string GetDeclName(Z3ConstDeclAst constDeclAst);
- Z3PatternAst MakePattern(List<Z3TermAst> exprs);
- Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body);
- ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors);
- void TypeCheckBool(Z3TermAst t);
- void TypeCheckInt(Z3TermAst t);
- void DeclareType(string typeName);
- void DeclareConstant(string constantName, Type boogieType);
- void DeclareFunction(string functionName, List<Type> domain, Type range);
- Z3TermAst GetConstant(string constantName, Type constantType);
- Z3TermAst MakeIntLiteral(string numeral);
- Z3TermAst MakeTrue();
- Z3TermAst MakeFalse();
- Z3TermAst MakeLabel(string labelName, bool pos, Z3TermAst child);
- Z3LabeledLiterals GetRelevantLabels();
- Z3TermAst Make(string op, List<Z3TermAst> children);
- Z3TermAst MakeArraySelect(List<Z3TermAst> args);
- Z3TermAst MakeArrayStore(List<Z3TermAst> args);
- }
-
- internal class PartitionMap
- {
- private Context ctx;
- private Dictionary<Term, int> termToPartition = new Dictionary<Term, int>();
- private Dictionary<object, int> valueToPartition = new Dictionary<object, int>();
- private List<Object> partitionToValue = new List<Object>();
- private int partitionCounter = 0;
- public int PartitionCounter { get { return partitionCounter; } }
-
- public PartitionMap(Context ctx)
- {
- this.ctx = ctx;
- }
+ public void Backtrack() {
+ z3.Pop();
+ labels.Backtrack();
+ functions.Backtrack();
+ constants.Backtrack();
+ symbols.Backtrack();
+ log("(pop)");
+ }
- public int GetPartition(Term value)
- {
- int result;
- if (!termToPartition.TryGetValue(value, out result))
- {
- result = partitionCounter++;
- termToPartition.Add(value, result);
- partitionToValue.Add(null);
- object constant = Evaluate(value);
- valueToPartition.Add(constant, result);
- partitionToValue[result] = constant;
- }
- return result;
- }
+ 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);
+ }
- private object Evaluate(Term v)
- {
- Sort s = v.GetSort();
- Sort boolSort = ctx.MkBoolSort();
- Sort intSort = ctx.MkIntSort();
- ArrayValue av;
-
- if (s.Equals(boolSort))
- {
- return ctx.GetBoolValue(v);
- }
- else if (s.Equals(intSort))
- {
- int i;
- if (ctx.TryGetNumeralInt(v, out i))
- {
- return BigNum.FromInt(i);
- }
- else
- {
- return BigNum.FromString(ctx.GetNumeralString(v));
- }
- }
- else if (ctx.TryGetArrayValue(v, out av))
- {
- List<List<int>> arrayValue = new List<List<int>>();
- List<int> tuple;
- for (int i = 0; i < av.Domain.Length; i++)
- {
- tuple = new List<int>();
- tuple.Add(GetPartition(av.Domain[i]));
- tuple.Add(GetPartition(av.Range[i]));
- arrayValue.Add(tuple);
- }
- tuple = new List<int>();
- tuple.Add(GetPartition(av.ElseCase));
- arrayValue.Add(tuple);
- return arrayValue;
- }
- else
- {
- // The term is uninterpreted; just return the partition id.
- return GetPartition(v);
- }
- }
+ 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 List<Object> PartitionToValue(Context ctx)
- {
- return partitionToValue;
- }
+ public void AddSmtlibString(string smtlibString) {
+ FuncDecl[] decls;
+ Term[] assumptions;
+ Term[] terms;
+ Sort[] sorts;
+ string tmp;
+
+ z3.ParseSmtlibString(smtlibString, new Sort[] { }, new FuncDecl[] { },
+ out assumptions, out terms, out decls, out sorts, out tmp);
+ // TBD: check with Nikolaj about the correct position of assumptions
+ foreach (FuncDecl decl in decls) {
+ Symbol symbol = z3.GetDeclName(decl);
+ string functionName = z3.GetSymbolString(symbol);
+ functions.Add(functionName, decl);
+ }
+ foreach (Term assumption in assumptions) {
+ log("(assert {0})", assumption);
+ z3.AssertCnstr(assumption);
+ }
+ }
- public Dictionary<object, int> ValueToPartition(Context ctx)
- {
- return valueToPartition;
- }
+ 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;
}
- internal class BacktrackDictionary<K, V>
- {
- private Dictionary<K, V> dictionary = new Dictionary<K, V>();
- private Stack<List<K>> keyStack = new Stack<List<K>>();
+ private static bool Equals(List<string> l, List<string> r) {
+ Debug.Assert(l != null);
+ if (r == null)
+ return false;
- public BacktrackDictionary()
- {
- CreateBacktrackPoint();
- }
+ if (l.Count != r.Count)
+ return false;
- public bool TryGetValue(K key, out V val)
- {
- return dictionary.TryGetValue(key, out val);
- }
+ 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 void Add(K key, V v)
- {
- if (dictionary.ContainsKey(key))
- {
- dictionary.Remove(key);
- }
- dictionary.Add(key, v);
- keyStack.Peek().Add(key);
+ 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;
}
- public bool ContainsKey(K k)
- {
- return dictionary.ContainsKey(k);
+ 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);
}
- public void CreateBacktrackPoint()
- {
- keyStack.Push(new List<K>());
+ 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(new ErrorModel(models[0]), new List<string>(labelStrings));
+ boogieErrors.Add(e);
+
+ if (boogieErrors.Count < this.counterexamples) {
+ z3.BlockLiterals(labels);
+ log("block-literals {0}", labels);
}
- public void Backtrack()
- {
- List<K> keysToErase = keyStack.Pop();
- foreach (K key in keysToErase)
- {
- dictionary.Remove(key);
- }
- if (keyStack.Count == 0)
- this.CreateBacktrackPoint();
+ 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);
}
- public IEnumerator GetEnumerator()
- {
- return dictionary.Keys.GetEnumerator();
+ 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(new ErrorModel(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;
+ }
}
- internal class BoogieErrorModelBuilder
- {
- private Z3Context container;
- private PartitionMap partitionMap;
+ 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 BoogieErrorModelBuilder(Z3Context container)
- {
- this.container = container;
- this.partitionMap = new PartitionMap(((Z3SafeContext)container).z3);
- }
-
- private Dictionary<string, int> CreateConstantToPartition(Model z3Model)
- {
- Dictionary<string, int> constantToPartition = new Dictionary<string, int>();
- foreach (FuncDecl c in z3Model.GetModelConstants())
- {
- string name = container.GetDeclName(new Z3TypeSafeConstDecl(c));
- int pid = partitionMap.GetPartition(z3Model.Eval(c, new Term[0]));
- constantToPartition.Add(name, pid);
- }
- return constantToPartition;
- }
+ public Term GetConstant(string constantName, Type constantType) {
+ Term typeSafeTerm;
+ if (!constants.ContainsKey(constantName))
+ this.DeclareConstant(constantName, constantType);
- private List<List<string>> CreatePartitionToConstant(Dictionary<string, int> constantToPartition)
- {
- List<List<string>> partitionToConstant = new List<List<string>>();
- for (int i = 0; i < partitionMap.PartitionCounter; i++)
- {
- partitionToConstant.Add(new List<string>());
- }
- foreach (string s in constantToPartition.Keys)
- {
- partitionToConstant[constantToPartition[s]].Add(s);
- }
- return partitionToConstant;
- }
+ if (!constants.TryGetValue(constantName, out typeSafeTerm))
+ throw new Exception("constant " + constantName + " is not defined");
+ return typeSafeTerm;
+ }
- private Dictionary<string, List<List<int>>> CreateFunctionToPartition(Model z3Model)
- {
- Dictionary<string, List<List<int>>> functionToPartition = new Dictionary<string, List<List<int>>>();
-
- foreach (KeyValuePair<FuncDecl, FunctionGraph> kv in z3Model.GetFunctionGraphs())
- {
- List<List<int>> f_tuples = new List<List<int>>();
- string f_name = container.GetDeclName(new Z3TypeSafeConstDecl(kv.Key));
- FunctionGraph graph = kv.Value;
- foreach (FunctionEntry entry in graph.Entries)
- {
- List<int> tuple = new List<int>();
- foreach (Term v in entry.Arguments)
- {
- tuple.Add(partitionMap.GetPartition(z3Model.Eval(v)));
- }
- tuple.Add(partitionMap.GetPartition(z3Model.Eval(entry.Result)));
- f_tuples.Add(tuple);
- }
- List<int> else_tuple = new List<int>();
- else_tuple.Add(partitionMap.GetPartition(z3Model.Eval(graph.Else)));
- f_tuples.Add(else_tuple);
- functionToPartition.Add(f_name, f_tuples);
- }
- return functionToPartition;
- }
+ public FuncDecl GetFunction(string functionName) {
+ FuncDecl f;
+ if (!functions.TryGetValue(functionName, out f))
+ throw new Exception("function " + functionName + " is undefined");
+ return f;
+ }
- public Z3ErrorModel BuildBoogieModel(Model z3Model)
- {
- Dictionary<string, int> constantToPartition = CreateConstantToPartition(z3Model);
- Dictionary<string, List<List<int>>> functionToPartition = CreateFunctionToPartition(z3Model);
- List<List<string>> partitionToConstant = CreatePartitionToConstant(constantToPartition);
- List<Object> partitionToValue = partitionMap.PartitionToValue(((Z3SafeContext)container).z3);
- Dictionary<object, int> valueToPartition = partitionMap.ValueToPartition(((Z3SafeContext)container).z3);
- return new Z3ErrorModel(constantToPartition, partitionToConstant, partitionToValue, valueToPartition, functionToPartition);
- }
+ 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 class Z3ErrorModelAndLabels
- {
- private Z3ErrorModel _errorModel;
- private List<string> _relevantLabels;
- public Z3ErrorModel ErrorModel
- {
- get { return this._errorModel; }
- }
- public List<string> RelevantLabels
- {
- get { return this._relevantLabels; }
- }
- public Z3ErrorModelAndLabels(Z3ErrorModel errorModel, List<string> relevantLabels)
- {
- this._errorModel = errorModel;
- this._relevantLabels = relevantLabels;
- }
+ 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 ErrorModel _errorModel;
+ private List<string> _relevantLabels;
+ public ErrorModel ErrorModel {
+ get { return this._errorModel; }
+ }
+ public List<string> RelevantLabels {
+ get { return this._relevantLabels; }
+ }
+ public Z3ErrorModelAndLabels(ErrorModel errorModel, List<string> relevantLabels) {
+ this._errorModel = errorModel;
+ this._relevantLabels = relevantLabels;
+ }
+ }
+
+
+
}
\ No newline at end of file |