5 // Alexander Chebaturkin (chebaturkin@gmail.com)
7 // Copyright (C) 2011 Alexander Chebaturkin
9 // Permission is hereby granted, free of charge, to any person obtaining
10 // a copy of this software and associated documentation files (the
11 // "Software"), to deal in the Software without restriction, including
12 // without limitation the rights to use, copy, modify, merge, publish,
13 // distribute, sublicense, and/or sell copies of the Software, and to
14 // permit persons to whom the Software is furnished to do so, subject to
15 // the following conditions:
17 // The above copyright notice and this permission notice shall be
18 // included in all copies or substantial portions of the Software.
20 // THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
21 // EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
22 // MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
23 // NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
24 // LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
25 // OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
26 // WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
30 using System.Collections.Generic;
33 using Mono.CodeContracts.Static.DataStructures;
34 using Mono.CodeContracts.Static.Extensions;
36 namespace Mono.CodeContracts.Static.Analysis.HeapAnalysis.SymbolicGraph {
37 class SymGraph<TFunc, TADomain> : ISymGraph<TFunc, TADomain, SymGraph<TFunc, TADomain>>
38 where TFunc : IEquatable<TFunc>, IConstantInfo
39 where TADomain : IAbstractDomainForEGraph<TADomain>, IEquatable<TADomain> {
40 public const bool DoIncrementalJoin = false;
41 private static int egraphIdGenerator;
42 private static SymGraph<TFunc, TADomain> BottomValue;
43 public readonly SymValue BottomPlaceHolder;
44 public readonly SymGraph<TFunc, TADomain> Parent;
45 public readonly TADomain UnderlyingTopValue;
47 private readonly SymValue const_root;
48 private readonly int egraph_id;
49 private readonly int history_size;
51 private readonly SymGraph<TFunc, TADomain> root_graph;
53 private readonly TADomain underlying_bottom_value;
54 private IImmutableMap<SymValue, TADomain> abs_map;
55 private IImmutableMap<SymValue, SymValue> forw_map;
56 private bool is_immutable;
58 public SymGraph (TADomain topValue, TADomain bottomValue)
59 : this (topValue, bottomValue, false)
61 if (BottomValue != null)
63 BottomValue = new SymGraph<TFunc, TADomain> (topValue, bottomValue, false);
66 private SymGraph (TADomain topValue, TADomain bottomValue, bool _)
68 this.egraph_id = egraphIdGenerator++;
69 this.const_root = FreshSymbol ();
71 TermMap = DoubleImmutableMap<SymValue, TFunc, SymValue>.Empty (SymValue.GetUniqueKey);
72 MultiEdgeMap = DoubleImmutableMap<SymValue, MultiEdge<TFunc, TADomain>, Sequence<SymValue>>.Empty (SymValue.GetUniqueKey);
73 this.abs_map = ImmutableIntKeyMap<SymValue, TADomain>.Empty (SymValue.GetUniqueKey);
74 this.forw_map = ImmutableIntKeyMap<SymValue, SymValue>.Empty (SymValue.GetUniqueKey);
75 EqualTermsMap = ImmutableIntKeyMap<SymValue, Sequence<SymGraphTerm<TFunc>>>.Empty (SymValue.GetUniqueKey);
76 EqualMultiTermsMap = ImmutableIntKeyMap<SymValue, SymGraphTerm<TFunc>>.Empty (SymValue.GetUniqueKey);
78 this.BottomPlaceHolder = FreshSymbol ();
79 this.abs_map = this.abs_map.Add (this.BottomPlaceHolder, bottomValue);
80 this.is_immutable = false;
81 this.history_size = 1;
83 this.root_graph = this;
85 this.UnderlyingTopValue = topValue;
86 this.underlying_bottom_value = bottomValue;
89 private SymGraph (SymGraph<TFunc, TADomain> from)
91 this.egraph_id = egraphIdGenerator++;
92 this.const_root = from.const_root;
93 this.BottomPlaceHolder = from.BottomPlaceHolder;
94 TermMap = from.TermMap;
95 MultiEdgeMap = from.MultiEdgeMap;
96 IdGenerator = from.IdGenerator;
97 this.abs_map = from.abs_map;
98 this.forw_map = from.forw_map;
99 EqualTermsMap = from.EqualTermsMap;
100 EqualMultiTermsMap = from.EqualMultiTermsMap;
101 this.UnderlyingTopValue = from.UnderlyingTopValue;
102 this.underlying_bottom_value = from.underlying_bottom_value;
103 Updates = from.Updates;
105 this.root_graph = from.root_graph;
106 this.history_size = from.history_size + 1;
108 from.MarkAsImmutable ();
111 public IImmutableMap<SymValue, SymGraphTerm<TFunc>> EqualMultiTermsMap { get; private set; }
112 public IImmutableMap<SymValue, Sequence<SymGraphTerm<TFunc>>> EqualTermsMap { get; private set; }
113 public DoubleImmutableMap<SymValue, MultiEdge<TFunc, TADomain>, Sequence<SymValue>> MultiEdgeMap { get; private set; }
114 public DoubleImmutableMap<SymValue, TFunc, SymValue> TermMap { get; private set; }
115 public int IdGenerator { get; private set; }
116 public Sequence<Update<TFunc, TADomain>> Updates { get; private set; }
118 public bool IsImmutable
120 get { return this.is_immutable; }
123 private int LastSymbolId
125 get { return IdGenerator; }
128 public SymValue this [SymValue[] args, TFunc function]
132 int len = args.Length;
133 for (int i = 0; i < len; i++)
134 args [i] = Find (args [i]);
136 SymValue candidate = FindCandidate (args, function);
137 if (candidate != null)
139 candidate = FreshSymbol ();
140 for (int i = 0; i < len; i++) {
141 var edge = new MultiEdge<TFunc, TADomain> (function, i, len);
142 MultiEdgeMap = MultiEdgeMap.Add (args [i], edge, MultiEdgeMap [args [i], edge].Cons (candidate));
144 EqualMultiTermsMap = EqualMultiTermsMap.Add (candidate, new SymGraphTerm<TFunc> (function, args));
145 AddMultiEdgeUpdate (args, function);
150 int len = args.Length;
151 for (int i = 0; i < len; i++)
152 args [i] = Find (args [i]);
154 bool isTermEqual = true;
155 SymGraphTerm<TFunc> term = EqualMultiTermsMap [value];
156 if (term.Args != null) {
157 for (int i = 0; i < len; i++) {
158 if (term.Args [i] != args [i]) {
165 for (int i = 0; i < len; i++) {
166 var edge = new MultiEdge<TFunc, TADomain> (function, i, len);
167 Sequence<SymValue> list = MultiEdgeMap [args [i], edge];
168 if (isTermEqual && !Sequence<SymValue>.Contains (list, value))
171 MultiEdgeMap = MultiEdgeMap.Add (args [i], edge, list.Cons (value));
175 EqualMultiTermsMap = EqualMultiTermsMap.Add (value, new SymGraphTerm<TFunc> (function, args));
176 AddMultiEdgeUpdate (args, function);
180 public SymValue this [TFunc function, params SymValue[] args]
182 get { return this [args, function]; }
185 private SymValue this [SymValue source, TFunc function]
189 source = Find (source);
190 SymValue sv = TermMap [source, function];
193 key = FreshSymbol ();
194 TermMap = TermMap.Add (source, function, key);
195 EqualTermsMap = EqualTermsMap.Add (key, Sequence<SymGraphTerm<TFunc>>.Cons (new SymGraphTerm<TFunc> (function, source), null));
196 AddEdgeUpdate (source, function);
204 source = Find (source);
205 value = Find (value);
207 TermMap = TermMap.Add (source, function, value);
208 Sequence<SymGraphTerm<TFunc>> rest = EqualTermsMap [value];
209 if (rest.IsEmpty () || (!rest.Head.Function.Equals (function) || rest.Head.Args [0] != source))
210 EqualTermsMap = EqualTermsMap.Add (value, rest.Cons (new SymGraphTerm<TFunc> (function, source)));
212 AddEdgeUpdate (source, function);
216 public IEnumerable<Pair<SymValue, SymGraphTerm<TFunc>>> ValidMultiTerms {
219 foreach (SymValue sv in EqualMultiTermsMap.Keys) {
220 SymGraphTerm<TFunc> term = EqualMultiTermsMap [sv];
221 if (IsValidMultiTerm (term))
222 yield return new Pair<SymValue, SymGraphTerm<TFunc>> (sv, term);
227 public SymValue ConstRoot
229 get { return this.const_root; }
232 #region ISymGraph<TFunc,TADomain,SymGraph<TFunc,TADomain>> Members
233 public TADomain this [SymValue symbol]
237 symbol = Find (symbol);
238 if (this.abs_map.ContainsKey (symbol))
239 return this.abs_map [symbol];
241 return this.UnderlyingTopValue;
245 SymValue newSym = Find (symbol);
246 if (this [symbol].Equals (value))
248 AddAbstractValueUpdate (newSym);
250 this.abs_map = this.abs_map.Remove (newSym);
252 this.abs_map = this.abs_map.Add (newSym, value);
256 public SymValue this [TFunc function]
258 get { return this [this.const_root, function]; }
259 set { this [this.const_root, function] = value; }
262 public SymValue this [TFunc function, SymValue arg]
264 get { return this [arg, function]; }
265 set { this [arg, function] = value; }
268 public IEnumerable<TFunc> Constants
270 get { return TermMap.Keys2 (this.const_root); }
273 public IEnumerable<SymValue> Variables
275 get { return TermMap.Keys1; }
278 public SymGraph<TFunc, TADomain> Top
280 get { return new SymGraph<TFunc, TADomain> (this.UnderlyingTopValue, this.underlying_bottom_value); }
283 public SymGraph<TFunc, TADomain> Bottom
287 if (BottomValue == null) {
288 BottomValue = new SymGraph<TFunc, TADomain> (this.UnderlyingTopValue, this.underlying_bottom_value);
289 BottomValue.MarkAsImmutable ();
297 get { return TermMap.Keys2Count (this.const_root) == 0; }
302 get { return this == BottomValue; }
305 public SymValue FreshSymbol ()
307 return new SymValue (++IdGenerator);
310 public SymValue TryLookup (TFunc function)
312 return LookupWithoutManifesting (this.const_root, function);
315 public SymValue TryLookup (TFunc function, SymValue arg)
317 return LookupWithoutManifesting (arg, function);
320 public void Eliminate (TFunc function, SymValue arg)
322 SymValue value = Find (arg);
323 DoubleImmutableMap<SymValue, TFunc, SymValue> newTermMap = TermMap.Remove (value, function);
324 if (newTermMap == TermMap)
326 TermMap = newTermMap;
327 AddEliminateEdgeUpdate (value, function);
330 public void Eliminate (TFunc function)
332 TermMap = TermMap.Remove (this.const_root, function);
333 AddEliminateEdgeUpdate (this.const_root, function);
336 public void EliminateAll (SymValue arg)
338 SymValue value = Find (arg);
339 AddEliminateAllUpdate (value);
340 TermMap = TermMap.RemoveAll (value);
341 this [arg] = this.UnderlyingTopValue;
344 public void AssumeEqual (SymValue v1, SymValue v2)
346 var workList = new WorkList<EqualityPair<TFunc, TADomain>> ();
347 SymValue sv1 = Find (v1);
348 SymValue sv2 = Find (v2);
350 if (TryPushEquality (workList, sv1, sv2))
351 AddEqualityUpdate (sv1, sv2);
353 DrainEqualityWorkList (workList);
356 public bool IsEqual (SymValue v1, SymValue v2)
358 return Find (v1) == Find (v2);
361 public IEnumerable<TFunc> Functions (SymValue sv)
363 return TermMap.Keys2 (Find (sv));
366 public IEnumerable<SymGraphTerm<TFunc>> EqTerms (SymValue sv)
368 foreach (var term in EqualTermsMap [Find (sv)].AsEnumerable ()) {
369 if (TryLookup (term.Function, term.Args) == sv)
374 public SymGraph<TFunc, TADomain> Clone ()
376 return new SymGraph<TFunc, TADomain> (this);
379 public SymGraph<TFunc, TADomain> Join(SymGraph<TFunc, TADomain> that)
381 throw new NotImplementedException();
384 public SymGraph<TFunc, TADomain> Join (SymGraph<TFunc, TADomain> that, bool widening, out bool weaker)
387 SymGraph<TFunc, TADomain> join = Join (that, out info, widening);
388 weaker = info.Changed;
392 public SymGraph<TFunc, TADomain> Widen(SymGraph<TFunc, TADomain> that)
394 throw new NotImplementedException();
397 public SymGraph<TFunc, TADomain> Join (SymGraph<TFunc, TADomain> that, out IMergeInfo mergeInfo, bool widen)
399 SymGraph<TFunc, TADomain> egraph = this;
401 SymGraph<TFunc, TADomain> commonTail = ComputeCommonTail (egraph, that, out updateSize);
402 bool hasCommonTail = commonTail != null;
404 bool doingIncrementalJoin = hasCommonTail & commonTail != egraph.root_graph & !widen & DoIncrementalJoin;
408 if (DebugOptions.Debug)
410 Console.WriteLine ("SymGraph {0}", widen ? "widen" : "join");
411 if (commonTail != null)
412 Console.WriteLine ("Last common symbol: {0}", commonTail.LastSymbolId);
414 Console.WriteLine (" Doing {0}", doingIncrementalJoin ? "incremental join" : "full join");
417 SymGraph<TFunc, TADomain> result;
418 MergeInfo<TFunc, TADomain> mergeState;
419 if (doingIncrementalJoin) {
420 result = new SymGraph<TFunc, TADomain> (commonTail);
421 mergeState = new MergeInfo<TFunc, TADomain> (result, egraph, that, widen);
422 mergeState.Replay (commonTail);
423 mergeState.Commit ();
425 result = new SymGraph<TFunc, TADomain> (commonTail);
426 mergeState = new MergeInfo<TFunc, TADomain> (result, egraph, that, widen);
427 mergeState.ReplayEliminations (commonTail);
428 mergeState.AddMapping (egraph.const_root, that.const_root, result.const_root);
429 mergeState.JoinSymbolicValue (egraph.const_root, that.const_root, result.const_root);
430 mergeState.Commit ();
432 mergeInfo = mergeState;
434 if (DebugOptions.Debug)
436 Console.WriteLine (" Result update size {0}", result.Updates.Length ());
437 Console.WriteLine ("Done with Egraph join: changed = {0}", mergeInfo.Changed ? 1 : 0);
443 public void Dump (TextWriter tw)
445 var set = new HashSet<SymValue> ();
446 var workList = new WorkList<SymValue> ();
447 IImmutableMap<SymValue, int> triggers = ImmutableIntKeyMap<SymValue, int>.Empty (SymValue.GetUniqueKey);
448 tw.WriteLine ("EGraphId: {0}", this.egraph_id);
449 tw.WriteLine ("LastSymbolId: {0}", LastSymbolId);
451 foreach (TFunc function in TermMap.Keys2 (this.const_root)) {
452 SymValue sv = this [this.const_root, function];
453 tw.WriteLine ("{0} = {1}", function, sv);
457 while (!workList.IsEmpty ()) {
458 SymValue sv = workList.Pull ();
462 foreach (TFunc function in TermMap.Keys2 (sv)) {
463 SymValue target = this [sv, function];
465 tw.WriteLine ("{0}({2}) = {1})", function, target, sv);
466 workList.Add (target);
468 foreach (var edge in MultiEdgeMap.Keys2 (sv)) {
469 foreach (SymValue target in MultiEdgeMap [sv, edge].AsEnumerable ()) {
470 if (!UpdateTrigger (target, edge, ref triggers))
472 SymGraphTerm<TFunc> term = EqualMultiTermsMap [target];
473 if (term.Args != null) {
474 tw.WriteLine ("{0}({1}) = {2}",
476 term.Args.ToString (", "), target);
477 workList.Add (target);
483 tw.WriteLine ("**Abstract value map");
484 foreach (SymValue sv in set) {
485 TADomain abstractValue = this [sv];
486 if (!abstractValue.IsTop)
487 tw.WriteLine ("{0} -> {1}", sv, abstractValue);
492 #region Implementation of IAbstractDomain<SymGraph<Constant,AbstractValue>>
493 public SymGraph<TFunc, TADomain> Meet (SymGraph<TFunc, TADomain> that)
495 if (this == that || IsBottom || that.IsTop)
497 if (that.IsBottom || IsTop)
503 public bool LessEqual (SymGraph<TFunc, TADomain> that)
505 IImmutableMap<SymValue, Sequence<SymValue>> forwardMap;
506 IImmutableMap<SymValue, SymValue> backwardMap;
508 return LessEqual (that, out forwardMap, out backwardMap);
511 public SymGraph<TFunc, TADomain> ImmutableVersion ()
517 public bool LessEqual (SymGraph<TFunc, TADomain> that,
518 out IImmutableMap<SymValue, Sequence<SymValue>> forward,
519 out IImmutableMap<SymValue, SymValue> backward)
521 if (!IsSameEGraph (that))
522 return InternalLessEqual (this, that, out forward, out backward);
530 public bool HasAllBottomFields (SymValue sv)
535 return this [sv].HasAllBottomFields;
538 public SymValue LookupOrManifest (TFunc function, SymValue arg, out bool fresh)
540 int oldCnt = IdGenerator;
541 SymValue result = this [function, arg];
543 fresh = oldCnt < IdGenerator;
547 public SymValue TryLookup (TFunc function, params SymValue[] args)
549 if (args.Length == 0 || args.Length == 1)
550 return LookupWithoutManifesting (this.const_root, function);
551 return LookupWithoutManifesting (args, function);
554 public SymValue LookupWithoutManifesting (SymValue sv, TFunc function)
559 SymValue result = TermMap [sv, function];
563 return Find (result);
566 public SymValue LookupWithoutManifesting (SymValue[] args, TFunc function)
568 int length = args.Length;
569 for (int i = 0; i < length; i++)
570 args [i] = Find (args [i]);
571 return FindCandidate (args, function);
574 public SymValue LookupOrBottomPlaceHolder (SymValue arg, TFunc function, out bool isPlaceHolder)
576 SymValue result = LookupWithoutManifesting (arg, function);
578 isPlaceHolder = result == null;
579 return isPlaceHolder ? this.BottomPlaceHolder : result;
582 private SymValue Find (SymValue v)
584 SymValue forw = this.forw_map [v];
591 private bool IsOldSymbol (SymValue sv)
593 if (this.Parent == null)
595 return sv.UniqueId <= this.Parent.LastSymbolId;
598 private SymValue FindCandidate (SymValue[] args, TFunc function)
600 int length = args.Length;
601 var multiEdge = new MultiEdge<TFunc, TADomain> (function, 0, length);
602 for (Sequence<SymValue> list = MultiEdgeMap [args [0], multiEdge]; list != null; list = list.Tail) {
603 SymGraphTerm<TFunc> term = EqualMultiTermsMap [list.Head];
604 if (term.Args.Length == length) {
607 for (int i = 0; i < length; ++i) {
608 if (Find (term.Args [i]) != args [i]) {
621 private bool TryPushEquality (WorkList<EqualityPair<TFunc, TADomain>> workList, SymValue sv1, SymValue sv2)
624 workList.Add (new EqualityPair<TFunc, TADomain> (sv1, sv2));
631 private void DrainEqualityWorkList (WorkList<EqualityPair<TFunc, TADomain>> workList)
633 while (!workList.IsEmpty ()) {
634 EqualityPair<TFunc, TADomain> equalityPair = workList.Pull ();
635 SymValue sv1 = Find (equalityPair.Sv1);
636 SymValue sv2 = Find (equalityPair.Sv2);
638 if (sv1.UniqueId < sv2.UniqueId) {
644 foreach (TFunc function in Functions (sv1)) {
645 SymValue v2 = LookupWithoutManifesting (sv2, function);
647 this [sv2, function] = this [sv1, function];
649 TryPushEquality (workList, this [sv1, function], v2);
651 TADomain thisValue = this [sv1];
652 TADomain thatValue = this [sv2];
653 foreach (var elem in EqualTermsMap [sv1].AsEnumerable ())
654 EqualTermsMap = EqualTermsMap.Add (sv2, EqualTermsMap [sv2].Cons (elem));
656 this.forw_map = this.forw_map.Add (sv1, sv2);
657 this [sv2] = thisValue.Meet (thatValue);
662 private IEnumerable<MultiEdge<TFunc, TADomain>> MultiEdges (SymValue sv)
664 return MultiEdgeMap.Keys2 (Find (sv));
667 public IEnumerable<SymGraphTerm<TFunc>> EqMultiTerms (SymValue sv)
669 SymGraphTerm<TFunc> term = EqualMultiTermsMap [sv];
670 if (term.Args != null && IsValidMultiTerm (term))
674 public bool IsValidSymbol (SymValue sv)
676 return EqualTermsMap.ContainsKey (sv);
679 private bool IsValidMultiTerm (SymGraphTerm<TFunc> term)
681 return LookupWithoutManifesting (term.Args, term.Function) != null;
684 private static SymGraph<TFunc, TADomain> ComputeCommonTail (SymGraph<TFunc, TADomain> g1, SymGraph<TFunc, TADomain> g2, out int updateSize)
686 SymGraph<TFunc, TADomain> graph1 = g1;
687 SymGraph<TFunc, TADomain> graph2 = g2;
688 while (graph1 != graph2) {
691 if (graph2 == null) {
695 if (graph1.history_size > graph2.history_size)
696 graph1 = graph1.Parent;
697 else if (graph2.history_size > graph1.history_size)
698 graph2 = graph2.Parent;
700 graph1 = graph1.Parent;
701 graph2 = graph2.Parent;
704 SymGraph<TFunc, TADomain> tail = graph1;
705 int historySize = tail != null ? tail.history_size : 0;
706 updateSize = g1.history_size + g2.history_size - 2*historySize;
710 private static bool InternalLessEqual (SymGraph<TFunc, TADomain> thisG, SymGraph<TFunc, TADomain> thatG,
711 out IImmutableMap<SymValue, Sequence<SymValue>> forward,
712 out IImmutableMap<SymValue, SymValue> backward)
715 SymGraph<TFunc, TADomain> commonTail = ComputeCommonTail (thisG, thatG, out updateSize);
716 if (thisG.IsImmutable)
717 thisG = thisG.Clone ();
719 var workList = new WorkList<EqualityPair<TFunc, TADomain>> ();
720 workList.Add (new EqualityPair<TFunc, TADomain> (thisG.const_root, thatG.const_root));
721 IImmutableSet<SymValue> backwardManifested = ImmutableSet<SymValue>.Empty (SymValue.GetUniqueKey);
722 IImmutableMap<SymValue, SymValue> backwardMap = ImmutableIntKeyMap<SymValue, SymValue>.Empty (SymValue.GetUniqueKey);
723 IImmutableMap<SymValue, Sequence<SymValue>> forwardMap = ImmutableIntKeyMap<SymValue, Sequence<SymValue>>.Empty (SymValue.GetUniqueKey);
724 IImmutableMap<SymValue, int> triggers = ImmutableIntKeyMap<SymValue, int>.Empty (SymValue.GetUniqueKey);
726 while (!workList.IsEmpty ()) {
727 EqualityPair<TFunc, TADomain> equalityPair = workList.Pull ();
728 SymValue sv1 = equalityPair.Sv1;
729 SymValue sv2 = equalityPair.Sv2;
732 if (VisitedBefore (sv2, backwardManifested, backwardMap, out s)) {
733 if (s != null && s == sv1)
736 if (DebugOptions.Debug)
737 Console.WriteLine ("---LessEqual fails due to pre-existing relation: {0} <- {1}", s, sv2);
743 TADomain val1 = sv1 == null ? thisG.UnderlyingTopValue.ForManifestedField () : thisG [sv1];
744 TADomain val2 = thatG [sv2];
745 if (!val1.LessEqual (val2)) {
746 if (DebugOptions.Debug)
747 Console.WriteLine ("---LessEqual fails due to abstract values: !({0} <= {1})", val1, val2);
753 backwardMap = backwardMap.Add (sv2, sv1);
754 forwardMap = forwardMap.Add (sv1, forwardMap [sv1].Cons (sv2));
756 backwardManifested = backwardManifested.Add (sv2);
757 if (thisG.HasAllBottomFields (sv1))
759 if (thatG.HasAllBottomFields (sv2)) {
760 if (DebugOptions.Debug)
762 Console.WriteLine ("---LessEqual fails due to bottom field difference");
769 foreach (TFunc function in thatG.Functions (sv2)) {
770 SymValue v1 = thisG [function, sv1];
771 SymValue v2 = thatG [function, sv2];
772 if (DebugOptions.Debug)
773 Console.WriteLine (" {0}-{1}->{2} <=? {3}-{4}->{5}", sv1, function, v1, sv2, function, v2);
774 workList.Add (new EqualityPair<TFunc, TADomain> (v1, v2));
777 foreach (var e in thatG.MultiEdges (sv2)) {
778 foreach (SymValue sv in thatG.MultiEdgeMap [sv2, e].AsEnumerable ()) {
779 if (!UpdateTrigger (sv, e, ref triggers))
782 SymGraphTerm<TFunc> term = thatG.EqualMultiTermsMap [sv];
783 var args = new SymValue[term.Args.Length];
784 for (int i = 0; i < args.Length; i++)
785 args [i] = backwardMap [term.Args [i]];
787 SymValue v1 = thisG.LookupWithoutManifesting (args, e.Function);
789 if (DebugOptions.Debug)
790 Console.WriteLine ("---LessEqual fails due to missing multi term {0}({1})",
792 string.Join (", ", term.Args.Select (it => it.ToString ())));
798 workList.Add (new EqualityPair<TFunc, TADomain> (v1, sv));
802 forward = forwardMap;
803 backward = CompleteWithCommon (backwardMap, thisG, commonTail.IdGenerator);
807 private static IImmutableMap<SymValue, SymValue> CompleteWithCommon (IImmutableMap<SymValue, SymValue> map,
808 SymGraph<TFunc, TADomain> thisGraph, int lastCommonId)
810 IEnumerable<SymValue> symValues = thisGraph.EqualTermsMap.Keys.Concat (thisGraph.EqualMultiTermsMap.Keys);
811 foreach (SymValue sv in symValues) {
812 if (IsCommon (sv, lastCommonId) && !map.ContainsKey (sv))
813 map = map.Add (sv, sv);
818 private static bool IsCommon (SymValue sv, int lastCommonId)
820 return sv.UniqueId <= lastCommonId;
823 private static bool UpdateTrigger (SymValue sv, MultiEdge<TFunc, TADomain> edge, ref IImmutableMap<SymValue, int> triggers)
825 int val = triggers [sv] + 1;
826 triggers = triggers.Add (sv, val);
827 return (val == edge.Arity);
830 private static bool VisitedBefore (SymValue sv2,
831 IImmutableSet<SymValue> backwardManifested,
832 IImmutableMap<SymValue, SymValue> backward,
835 sv1 = backward [sv2];
836 return sv1 != null || backwardManifested.Contains (sv2);
839 private bool IsSameEGraph (SymGraph<TFunc, TADomain> that)
843 if (that.Parent == this)
844 return that.Updates == Updates;
849 private void MarkAsImmutable ()
851 this.is_immutable = true;
854 #region Merge updates
855 private void AddUpdate (Update<TFunc, TADomain> update)
857 Updates = Updates.Cons (update);
860 private void AddAbstractValueUpdate (SymValue sv)
862 if (!IsOldSymbol (sv))
864 AddUpdate (new AbstractDomainUpdate<TFunc, TADomain> (sv));
867 private void AddEqualityUpdate (SymValue sv1, SymValue sv2)
869 if (!IsOldSymbol (sv1) || !IsOldSymbol (sv2))
871 AddUpdate (new EqualityUpdate<TFunc, TADomain> (sv1, sv2));
874 private void AddEdgeUpdate (SymValue from, TFunc function)
876 if (!IsOldSymbol (from))
878 AddUpdate (new EdgeUpdate<TFunc, TADomain> (from, function));
881 private void AddEliminateAllUpdate (SymValue from)
883 if (!IsOldSymbol (from))
885 foreach (TFunc function in TermMap.Keys2 (from))
886 AddUpdate (new EliminateEdgeUpdate<TFunc, TADomain> (from, function));
889 private void AddEliminateEdgeUpdate (SymValue from, TFunc function)
891 if (!IsOldSymbol (from))
893 AddUpdate (new EliminateEdgeUpdate<TFunc, TADomain> (from, function));
896 private void AddMultiEdgeUpdate (SymValue[] from, TFunc function)
898 for (int i = 0; i < from.Length; i++) {
899 if (!IsOldSymbol (from [i]))
903 AddUpdate (new MultiEdgeUpdate<TFunc, TADomain> (from, function));
907 public IImmutableMap<SymValue, Sequence<SymValue>> GetForwardIdentityMap ()
909 var res = ImmutableIntKeyMap<SymValue, Sequence<SymValue>>.Empty (SymValue.GetUniqueKey);
910 foreach (var sv in this.EqualTermsMap.Keys.Union (this.EqualMultiTermsMap.Keys)) {
911 res = res.Add (sv, Sequence<SymValue>.Cons (sv, null));