package org.eclipse.emf.henshin.sam.invcheck.algorithm;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.Map;
import java.util.Set;

import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.henshin.sam.invcheck.InvariantCheckerUtil;
import org.eclipse.emf.henshin.sam.invcheck.SubgraphIterator;
import org.eclipse.emf.henshin.sam.invcheck.adapter.GCNACAdapter;
import org.eclipse.emf.henshin.sam.invcheck.adapter.SamGraphInvCheckGraphAdapter;
import org.eclipse.emf.henshin.sam.invcheck.nac.NacFactory;
import org.eclipse.emf.henshin.sam.invcheck.nac.NegativeApplicationCondition;
import org.eclipse.emf.henshin.sam.model.samgraph.Edge;
import org.eclipse.emf.henshin.sam.model.samgraph.Graph;
import org.eclipse.emf.henshin.sam.model.samgraph.Node;
import org.eclipse.emf.henshin.sam.model.samgraphcondition.GraphCondition;
import org.eclipse.emf.henshin.sam.model.samgraphcondition.LogicalGCCoupling;
import org.eclipse.emf.henshin.sam.model.samgraphcondition.NegatedCondition;
import org.eclipse.emf.henshin.sam.model.samgraphcondition.Quantification;
import org.eclipse.emf.henshin.sam.model.samgraphcondition.SamgraphconditionPackage;
import org.eclipse.emf.henshin.sam.model.samrules.RuleGraph;
import org.eclipse.emf.henshin.sam.model.samtrace.Match;
import org.eclipse.emf.henshin.sam.model.samtrace.SamtraceFactory;

/**
 * Create all possible context for one match, disjunctively combined. Try to
 * eliminate disjunctive combinations to reduce NACs to one possibility. If
 * there is more than one possibility, discard match and generated context. Take
 * the next match, repeat. Take the next pattern, repeat.
 *
 * Problem: Translation of big NACs takes much time. Could order constraints by
 * NAC size to alleviate this.
 * 
 * When creating subgraphs from NACs to be matched to the target graph, we could
 * check whether the rest of the NAC (connected to the positive part) contains a
 * forbidden pattern. Thus, we could discard subgraphs without checking each and
 * every match. Unfortunately, this has to be implemented directly in the
 * NACTranslator.
 * 
 * @author Pro
 */
public class ContextGenerator {

	private Set<RuleGraph> generationConstraints;

	private Set<Graph> restrictingConstraints;

	private RuleGraph proofGoal;

	private RuleGraph currentConstraint;

	private NACTranslator nacT;

	private IsomorphicPartMatcher ipm;

	private Map<RuleGraph, Set<Match>> discardedMatches;

	private Map<RuleGraph, Set<Match>> discardedMatchesRevertible;

	public Set<RuleGraph> getGenerationConstraints() {
		return this.generationConstraints;
	}

	public void setGenerationConstraints(Set<RuleGraph> generationConstraints) {
		this.generationConstraints = generationConstraints;
	}

	public Set<Graph> getRestrictingConstraints() {
		return this.restrictingConstraints;
	}

	public void setRestrictingConstraints(Set<Graph> restrictingConstraints) {
		this.restrictingConstraints = restrictingConstraints;
	}

	public RuleGraph getProofGoal() {
		return this.proofGoal;
	}

	public void setProofGoal(RuleGraph proofGoal) {
		this.proofGoal = proofGoal;
	}

	/*
	 * public Set<RuleGraph> getCurrentConstraints() { return
	 * this.currentConstraints; }
	 * 
	 * public void setCurrentConstraints(Set<RuleGraph> currentConstraints) {
	 * this.currentConstraints = currentConstraints; }
	 */

	public ContextGenerator() {
		this.ipm = new IsomorphicPartMatcher();
		this.nacT = new NACTranslator();
		this.discardedMatches = new HashMap<RuleGraph, Set<Match>>();
		this.discardedMatchesRevertible = new HashMap<RuleGraph, Set<Match>>();
	}

	public boolean proof() {
		Match match = InvariantCheckerUtil.copyAsRuleGraph(this.proofGoal);
		RuleGraph precondition = null;
		for (Node n : match.getNodeMatching().values()) {
			precondition = (RuleGraph) n.eContainer();
			break;
		}
		nacT.setRestrictingConstraints(this.restrictingConstraints);

		// int cnt = 0;
		this.currentConstraint = precondition;
		Iterator<RuleGraph> iter = this.generationConstraints.iterator();
		while (iter.hasNext()) {
			RuleGraph constraint = iter.next();
			if (generateContext(constraint)) {
				// cnt++;
				if (checkProofGoal()) {
					return true;
				} else {
					// reset iterator
					iter = this.generationConstraints.iterator();
					// delete revertible discarded matches
					this.discardedMatchesRevertible.clear();
				}
			} else {
				// do nothing, continue loop with next pattern
			}
		}
		// System.out.println(cnt);
		// iterated through all patterns without being able to generate new
		// context
		return false;
	}

	public boolean generateContext(RuleGraph pattern) {
		// System.out.println("gc: " + ((NegatedCondition)
		// pattern.eContainer().eContainer()).getName());
		// so actually we may allow multiple NACs. Should then change this
		// check.
		if (pattern.getCondition() == null) {
			throw new UnsupportedOperationException(
					"Patterns that are used to generate context must have one or more NACs.");
		}
		if (pattern.getCondition().eClass() == SamgraphconditionPackage.eINSTANCE.getLogicalGCCoupling()
				&& ((LogicalGCCoupling) pattern.getCondition()).getOperands().size() != 1) {
			// have to see whether this will work
			// throw new UnsupportedOperationException("Patterns that are used
			// to generate context must have exactly one NAC.");
		}

		if (this.discardedMatches.get(pattern) == null) {
			this.discardedMatches.put(pattern, new HashSet<Match>());
		}
		if (this.discardedMatchesRevertible.get(pattern) == null) {
			this.discardedMatchesRevertible.put(pattern, new HashSet<Match>());
		}

		boolean generatedContext = false;

		RuleGraph g = null;
		Match tmpMatch = null;
		ipm.reset();

		// old version
		/*
		 * if (this.currentConstraint.getCondition() != null) {
		 * 
		 * // at this point we take one and only one NAC from the current
		 * constraint to match the current generating constraint in it // in
		 * order to also generate context for other NACs
		 * NegativeApplicationCondition nac =
		 * SamGraphInvCheckGraphAdapter.getInstance(this.currentConstraint).
		 * getNacs().get(0); tmpMatch = SubgraphIterator.fullNacToRuleGraph(nac,
		 * false); for (Node n : tmpMatch.getNodeMatching().values()) { g =
		 * (RuleGraph) n.eContainer(); break; } } else { tmpMatch =
		 * InvariantCheckingUtil.copyAsRuleGraph(this.currentConstraint); for
		 * (Node n : tmpMatch.getNodeMatching().values()) { g = (RuleGraph)
		 * n.eContainer(); break; } }
		 */

		Iterator<NegativeApplicationCondition> nacIter = null;
		boolean first = false;
		if (this.currentConstraint.getCondition() == null) {
			first = true;
		} else {
			// remember to delete condition if we reach a point where we remove
			// all conditions from current constraint. Cannot happen right now
			nacIter = SamGraphInvCheckGraphAdapter.getInstance(this.currentConstraint).getNacs().iterator();
		}
		while (first || (nacIter != null && nacIter.hasNext())) {
			NegativeApplicationCondition targetNac = null;
			if (first) {
				tmpMatch = InvariantCheckerUtil.copyAsRuleGraph(this.currentConstraint);
				for (Node n : tmpMatch.getNodeMatching().values()) {
					g = (RuleGraph) n.eContainer();
					break;
				}
			} else {
				targetNac = nacIter.next();
				tmpMatch = SubgraphIterator.fullNacToRuleGraph(targetNac, false);
				for (Node n : tmpMatch.getNodeMatching().values()) {
					g = (RuleGraph) n.eContainer();
					break;
				}
			}
			first = false;

			// old

			ipm.setHostGraph(g);
			ipm.setPattern(pattern);
			ipm.setCurrentSubGraph(SubgraphIterator.graphToPosSubGraph(pattern));
			ipm.reset();

			Match nextMatch = null;

			// here we could integrate a check for not only a match with the
			// graph and one NAC
			// but for matches with other NACs if there is more than one.
			// however, we need to take care, that a match targets only the
			// graph and exactly one NAC
			// could just iterate over NACs and then over matches for the
			// current NAC. Would just need
			// to ensure that the same match in the graph will not be considered
			// multiple times.
			while (nextMatch == null) {
				nextMatch = ipm.getNextMatching();
				if (nextMatch == null) {
					// System.out.println("no match: " + ((NegatedCondition)
					// pattern.eContainer().eContainer()).getName());
					// return false;
					break;
				} else {
					// if (!checkMatch(nextMatch, tmpMatch, pattern) && false) {
					// //System.out.println("match was discarded: " +
					// ((NegatedCondition)
					// pattern.eContainer().eContainer()).getName());
					// nextMatch = null;
					// } else
					{
						// match is valid, use it to generate context
						nacT.reset();
						nacT.setPattern(pattern);
						nacT.setMergedGraph(g);
						nacT.setInitialMatching(nextMatch);

						RuleGraph result = null;
						if (nacT.checkFullNacExistence()) {
							result = null;
						} else {
							result = nacT.translateContext();
						}
						if (result == null) {
							// System.out.println("translate null: " +
							// ((NegatedCondition)
							// pattern.eContainer().eContainer()).getName());
							Match match = SamtraceFactory.eINSTANCE.createMatch();
							for (Map.Entry<Node, Node> entry : nextMatch.getNodeMatching()) {
								Node newValue = null;
								for (Map.Entry<Node, Node> e : tmpMatch.getNodeMatching()) {
									if (entry.getValue() == e.getValue()) {
										newValue = e.getKey();
										break;
									}
								}
								match.getNodeMatching().put(entry.getKey(), newValue);
							}
							for (Map.Entry<Edge, Edge> entry : nextMatch.getEdgeMatching()) {
								Edge newValue = null;
								for (Map.Entry<Edge, Edge> e : tmpMatch.getEdgeMatching()) {
									if (entry.getValue() == e.getValue()) {
										newValue = e.getKey();
										break;
									}
								}
								match.getEdgeMatching().put(entry.getKey(), newValue);
							}
							this.discardedMatches.get(pattern).add(match);
							nextMatch = null;
						} else {
							// System.out.println("translate not null: " +
							// ((NegatedCondition)
							// pattern.eContainer().eContainer()).getName());
							if (removeInvalidNacs(result)) {
								generatedContext = true;
								// probably a good idea to exclude match here.
								// If not, it will result in an empty
								// translation the next time it is chosen and
								// will then be discarded

								// now we have to transform the generated NACs
								// to the current NAC
								if (this.currentConstraint.getCondition() == null) {
									/*
									 * NegativeApplicationCondition newNac =
									 * NacFactory.eINSTANCE.
									 * createNegativeApplicationCondition();
									 * Set<NegativeApplicationCondition> nacs =
									 * new
									 * HashSet<NegativeApplicationCondition>();
									 * nacs.add(newNac);
									 * newNac.setGraph(this.currentConstraint);
									 * this.currentConstraint.setCondition(
									 * InvariantCheckingUtil.
									 * createNegatedConditions(nacs));
									 */
									targetNac = NacFactory.eINSTANCE.createNegativeApplicationCondition();
									// Set<NegativeApplicationCondition> nacs =
									// new
									// HashSet<NegativeApplicationCondition>();
									// nacs.add(targetNac);
									targetNac.setGraph(this.currentConstraint);
									// this.currentConstraint.setCondition(InvariantCheckingUtil.createNegatedConditions(nacs));
								}
								// in prior versions, we translated the result
								// to the only nac in the current constraint
								// now, we translate it to the nac that was used
								// as a target to generate context
								// NegativeApplicationCondition nac =
								// GCNACAdapter.getInstance(((LogicalGCCoupling)
								// this.currentConstraint.getCondition()).getOperands().get(0));
								// iterate over all generated nacs
								Set<NegativeApplicationCondition> newNacs = new HashSet<NegativeApplicationCondition>();
								for (NegativeApplicationCondition generatedNac : SamGraphInvCheckGraphAdapter
										.getInstance(result).getNacs()) {
									// have to copy existing nac. Problem:
									// cannot insert new nacs just yet because
									// we are currently iterating over them -
									// or maybe we can, because the adapter will
									// not be updated when we add nacs?
									NegativeApplicationCondition copyOfTargetNac = NacFactory.eINSTANCE
											.createNegativeApplicationCondition();
									copyOfTargetNac.setGraph(targetNac.getGraph());
									Match copyOfTargetNacMatch = copyNacWithoutInterface(targetNac, copyOfTargetNac);

									copyOfTargetNac.getNodes().addAll(generatedNac.getNodes());
									copyOfTargetNac.getEdges().addAll(generatedNac.getEdges());

									for (Edge e : copyOfTargetNac.getEdges()) {
										if (!copyOfTargetNac.getNodes().contains(e.getSource())) {
											for (Map.Entry<Node, Node> entry : tmpMatch.getNodeMatching()) {
												if (entry.getValue() == e.getSource()) {
													if (copyOfTargetNacMatch.getNodeMatching()
															.containsKey(entry.getKey())) {
														e.setSource(copyOfTargetNacMatch.getNodeMatching()
																.get(entry.getKey()));
													} else {
														e.setSource(entry.getKey());
													}
													break;
												}
											}
										}
										if (!copyOfTargetNac.getNodes().contains(e.getTarget())) {
											for (Map.Entry<Node, Node> entry : tmpMatch.getNodeMatching()) {
												if (entry.getValue() == e.getTarget()) {
													if (copyOfTargetNacMatch.getNodeMatching()
															.containsKey(entry.getKey())) {
														e.setTarget(copyOfTargetNacMatch.getNodeMatching()
																.get(entry.getKey()));
													} else {
														e.setTarget(entry.getKey());
													}
													break;
												}
											}
										}
										/*
										 * if (e.getSource().eContainer() !=
										 * this.currentConstraint &&
										 * !copyOfTargetNac.getNodes().contains(
										 * e.getSource())) {
										 * //System.out.println(
										 * "nac error src/cr " + e.getName() +
										 * ":" + e.getInstanceOf().getName()); }
										 * if (e.getTarget().eContainer() !=
										 * this.currentConstraint &&
										 * !copyOfTargetNac.getNodes().contains(
										 * e.getTarget())) {
										 * //System.out.println(
										 * "nac error tar/cr " + e.getName() +
										 * ":" + e.getInstanceOf().getName()); }
										 */
									}
									newNacs.add(copyOfTargetNac);
								}

								// nac.getNodes().addAll(SamGraphInvCheckGraphAdapter.getInstance(result).getNacs().get(0).getNodes());
								// nac.getEdges().addAll(SamGraphInvCheckGraphAdapter.getInstance(result).getNacs().get(0).getEdges());
								/*
								 * old for (Edge e : nac.getEdges()) { if
								 * (!nac.getNodes().contains(e.getSource())) {
								 * for (Map.Entry<Node, Node> entry :
								 * tmpMatch.getNodeMatching()) { if
								 * (entry.getValue() == e.getSource()) {
								 * e.setSource(entry.getKey()); break; } } } if
								 * (!nac.getNodes().contains(e.getTarget())) {
								 * for (Map.Entry<Node, Node> entry :
								 * tmpMatch.getNodeMatching()) { if
								 * (entry.getValue() == e.getTarget()) {
								 * e.setTarget(entry.getKey()); break; } } } }
								 */

								// exclude match
								Match match = SamtraceFactory.eINSTANCE.createMatch();
								for (Map.Entry<Node, Node> entry : nextMatch.getNodeMatching()) {
									Node newValue = null;
									for (Map.Entry<Node, Node> e : tmpMatch.getNodeMatching()) {
										if (entry.getValue() == e.getValue()) {
											newValue = e.getKey();
											break;
										}
									}
									match.getNodeMatching().put(entry.getKey(), newValue);
								}
								for (Map.Entry<Edge, Edge> entry : nextMatch.getEdgeMatching()) {
									Edge newValue = null;
									for (Map.Entry<Edge, Edge> e : tmpMatch.getEdgeMatching()) {
										if (entry.getValue() == e.getValue()) {
											newValue = e.getKey();
											break;
										}
									}
									match.getEdgeMatching().put(entry.getKey(), newValue);
								}
								this.discardedMatches.get(pattern).add(match);

								// remove old NACs, add expanded NACs
								EObject gcToRemove = null;
								for (Edge e : targetNac.getEdges()) {
									if (gcToRemove == null) {
										gcToRemove = e.eContainer();
										while (SamgraphconditionPackage.eINSTANCE.getNegatedCondition() != gcToRemove
												.eClass()) {
											gcToRemove = gcToRemove.eContainer();
										}
									}
									e.setSource(null);
									e.setTarget(null);
								}
								if (gcToRemove == null) {
									for (Node n : targetNac.getNodes()) {
										gcToRemove = n.eContainer();
										while (SamgraphconditionPackage.eINSTANCE.getNegatedCondition() != gcToRemove
												.eClass()) {
											gcToRemove = gcToRemove.eContainer();
										}
										break;
									}
								}
								this.currentConstraint.setCondition(InvariantCheckerUtil
										.addNegatedConditions(this.currentConstraint.getCondition(), newNacs));
								((LogicalGCCoupling) this.currentConstraint.getCondition()).getOperands()
										.remove(gcToRemove);
								/*
								 * for (Edge e :
								 * this.currentConstraint.getEdges()) { if
								 * (e.eContainer() != this.currentConstraint) {
								 * //System.out.println("cont error"); } if
								 * (e.getSource().eContainer() !=
								 * this.currentConstraint) {
								 * //System.out.println("cc error src"); } if
								 * (e.getTarget().eContainer() !=
								 * this.currentConstraint) {
								 * //System.out.println("cc error tar"); } } for
								 * (NegativeApplicationCondition nac :
								 * SamGraphInvCheckGraphAdapter.getInstance(this
								 * .currentConstraint).getNacs()) { for (Edge e
								 * : nac.getEdges()) { if
								 * (e.getSource().eContainer() !=
								 * this.currentConstraint &&
								 * !nac.getNodes().contains(e.getSource())) {
								 * System.out.println("nac error src"); } if
								 * (e.getTarget().eContainer() !=
								 * this.currentConstraint &&
								 * !nac.getNodes().contains(e.getTarget())) {
								 * System.out.println("nac error tar"); } } }
								 */

								return true;
							} else {
								generatedContext = true;
								// there is no condition left. This means we
								// have to discard the current NAC from which
								// context was generated
								// if there is no nac left after that, the
								// positive part of the proof goal is a
								// forbidden pattern
								// this also means that we can prove forbidden
								// patterns without nacs - however, the chance
								// of failure to proof that is quite high

								// we must not add this match to the discarded
								// matches
								/*
								 * Match match =
								 * SamtraceFactory.eINSTANCE.createMatch(); for
								 * (Map.Entry<Node, Node> entry :
								 * nextMatch.getNodeMatching()) { Node newValue
								 * = null; for (Map.Entry<Node, Node> e :
								 * tmpMatch.getNodeMatching()){ if
								 * (entry.getValue() == e.getValue()) { newValue
								 * = e.getKey(); break; } }
								 * match.getNodeMatching().put(entry.getKey(),
								 * newValue); } for (Map.Entry<Edge, Edge> entry
								 * : nextMatch.getEdgeMatching()) { Edge
								 * newValue = null; for (Map.Entry<Edge, Edge> e
								 * : tmpMatch.getEdgeMatching()){ if
								 * (entry.getValue() == e.getValue()) { newValue
								 * = e.getKey(); break; } }
								 * match.getEdgeMatching().put(entry.getKey(),
								 * newValue); }
								 * this.discardedMatchesRevertible.get(pattern).
								 * add(match);
								 */

								// need to remove the nac from which this
								// context was generated
								if (targetNac != null) {
									for (Edge e : targetNac.getEdges()) {
										e.setSource(null);
										e.setTarget(null);
									}
								}
								if (this.currentConstraint.getCondition() == null) {
									// do not add a condition
								} else if (SamgraphconditionPackage.eINSTANCE
										.getNegatedCondition() == this.currentConstraint.getCondition().eClass()) {
									// single condition, remove that. If this
									// happens, we should be done with the proof
									this.currentConstraint.setCondition(null);
								} else if (SamgraphconditionPackage.eINSTANCE
										.getLogicalGCCoupling() == this.currentConstraint.getCondition().eClass()) {
									if (((LogicalGCCoupling) this.currentConstraint.getCondition()).getOperands()
											.size() <= 1) {
										// no or just the one condition in
										// coupling. If this happens, we should
										// be done with the proof
										this.currentConstraint.setCondition(null);
									} else {
										// more than one condition in coupling
										// of current constraint. have to
										// continue context generation
										GraphCondition gc = null;
										for (GraphCondition cond : ((LogicalGCCoupling) this.currentConstraint
												.getCondition()).getOperands()) {
											if (GCNACAdapter.getInstance(cond).equals(targetNac)) {
												gc = cond;
												break;
											}
										}
										if (gc != null) {
											((LogicalGCCoupling) this.currentConstraint.getCondition()).getOperands()
													.remove(gc);
										} else {
											throw new RuntimeException("strange error");
										}
									}
								} else {
									throw new RuntimeException("strange error");
								}
								return true;
							}
						}
					}
				}
			}
		}
		return generatedContext;
	}

	private boolean removeInvalidNacs(RuleGraph result) {
		Set<NegatedCondition> toRemove = new HashSet<NegatedCondition>();
		// translate returns a coupling - if there is just one condition and
		// translate ever
		// returns just a negated condition, this should be changed
		for (GraphCondition gc : ((LogicalGCCoupling) result.getCondition()).getOperands()) {
			NegatedCondition nac = (NegatedCondition) gc;
			IsomorphicPartMatcher subIpm = new IsomorphicPartMatcher();
			Match match = SubgraphIterator.fullNacToGraph(GCNACAdapter.getInstance(nac), false);
			Graph host = null;
			for (Node n : match.getNodeMatching().values()) {
				host = (Graph) n.eContainer();
				break;
			}
			subIpm.setHostGraph(host);
			for (Graph rg : this.restrictingConstraints) {
				subIpm.reset();
				subIpm.setPattern(rg);
				subIpm.setCurrentSubGraph(SubgraphIterator.graphToSubGraph(rg));
				if (subIpm.getNextMatching() != null) {
					toRemove.add(nac);
					break;
				}
			}
		}
		for (NegatedCondition nac : toRemove) {
			Quantification quant = (Quantification) nac.getOperand();
			Graph graph = quant.getContext();
			for (Edge e : graph.getEdges()) {
				e.setSource(null);
				e.setTarget(null);
			}
		}
		((LogicalGCCoupling) result.getCondition()).getOperands().removeAll(toRemove);
		if (((LogicalGCCoupling) result.getCondition()).getOperands().size() < 1) {
			// System.out.println("0 nacs left");
			return false;
		} else if (((LogicalGCCoupling) result.getCondition()).getOperands().size() > 1) {
			// we will still return true here. Note that the generator should
			// still give the correct result, as
			// there will just be more nacs in the current constraint (the one
			// trying to reach the proof goal.
			// However, generating new nacs with generating constraints will
			// just happen in the first nac in the condition.
			// This is not wrong, but it is not complete either, as the
			// generating constraint should be matches to all possible nacs,
			// not just the first.
			// System.out.println("not one nac left: " + ((LogicalGCCoupling)
			// result.getCondition()).getOperands().size());
			// return false;
			return true;
		} else {
			// System.out.println("one nac left: ");
			return true;
		}
	}
/*
	private boolean checkMatch(Match chMatch, Match tmpMatch, RuleGraph pattern) {
		for (Match m : this.discardedMatches.get(pattern)) {
			boolean equal = true;
			for (Map.Entry<Node, Node> entry : chMatch.getNodeMatching()) {
				if (tmpMatch.getNodeMatching().get(m.getNodeMatching().get(entry.getKey())) != entry.getValue()) {
					equal = false;
					break;
				}
			}
			if (equal) {
				for (Map.Entry<Edge, Edge> entry : chMatch.getEdgeMatching()) {
					if (tmpMatch.getEdgeMatching().get(m.getEdgeMatching().get(entry.getKey())) != entry.getValue()) {
						equal = false;
						break;
					}
				}
			}
			if (equal) {
				return false;
			}
			// m: pattern -> host
			// chMatch: pattern ->chost
			// tmpMatch: host -> chost
		}
		for (Match m : this.discardedMatchesRevertible.get(pattern)) {
			boolean equal = true;
			for (Map.Entry<Node, Node> entry : chMatch.getNodeMatching()) {
				if (tmpMatch.getNodeMatching().get(m.getNodeMatching().get(entry.getKey())) != entry.getValue()) {
					equal = false;
					break;
				}
			}
			if (equal) {
				for (Map.Entry<Edge, Edge> entry : chMatch.getEdgeMatching()) {
					if (tmpMatch.getEdgeMatching().get(m.getEdgeMatching().get(entry.getKey())) != entry.getValue()) {
						equal = false;
						break;
					}
				}
			}
			if (equal) {
				return false;
			}
			// m: pattern -> host
			// chMatch: pattern ->chost
			// tmpMatch: host -> chost
		}
		return true;
	}
*/
	public Match copyNacWithoutInterface(NegativeApplicationCondition nac, NegativeApplicationCondition newNac) {
		Match match = SamtraceFactory.eINSTANCE.createMatch();

		for (Node n : nac.getNodes()) {
			Node newNode = InvariantCheckerUtil.copyAsPattern(n);
			match.getNodeMatching().put(n, newNode);
			newNac.getNodes().add(newNode);
		}
		for (Edge e : nac.getEdges()) {
			Edge newEdge = InvariantCheckerUtil.copyAsPattern(e);
			match.getEdgeMatching().put(e, newEdge);
			newNac.getEdges().add(newEdge);
			if (match.getNodeMatching().get(e.getSource()) != null) {
				newEdge.setSource(match.getNodeMatching().get(e.getSource()));
			} else {
				newEdge.setSource(e.getSource());
			}
			if (match.getNodeMatching().get(e.getTarget()) != null) {
				newEdge.setTarget(match.getNodeMatching().get(e.getTarget()));
			} else {
				newEdge.setTarget(e.getTarget());
			}

		}
		return match;
	}

	public boolean checkProofGoal() {
		// alle Graphen, die proof goal erf�llen, m�ssen auch current constraint
		// erf�llen
		this.ipm.reset();
		this.ipm.setHostGraph(this.proofGoal);
		this.ipm.setPattern(this.currentConstraint);
		this.ipm.setCurrentSubGraph(SubgraphIterator.graphToSubGraph(this.currentConstraint));
		return this.ipm.getNextMatching() != null;
	}

	/*
	 * @deprecated
	 */
/*	public void discardPatterns() {
		Set<RuleGraph> toDiscard = new HashSet<RuleGraph>();
		for (Graph rg : restrictingConstraints) {
			ipm.reset();
		}
	}
*/
	public Set<RuleGraph> separateContext(RuleGraph targetGraph) {
		Set<RuleGraph> result = new HashSet<RuleGraph>();
		for (NegativeApplicationCondition nac : SamGraphInvCheckGraphAdapter.getInstance(targetGraph).getNacs()) {
			RuleGraph newGraph = null;
			Match match = InvariantCheckerUtil.copyAsRuleGraph(targetGraph);
			for (Node n : match.getNodeMatching().values()) {
				if (n != null) {
					newGraph = (RuleGraph) n.eContainer();
					break;
				}
			}
			for (Node n : nac.getNodes()) {
				newGraph.getNodes().add(n);
			}
			for (Edge e : nac.getEdges()) {
				newGraph.getEdges().add(e);
				if (!newGraph.getNodes().contains(e.getSource())) {
					e.setSource(match.getNodeMatching().get(e.getSource()));
				}
				if (!newGraph.getNodes().contains(e.getTarget())) {
					e.setTarget(match.getNodeMatching().get(e.getTarget()));
				}
			}
			result.add(newGraph);
		}
		return result;
	}

	/**
	 * @deprecated
	 * @param targetGraph
	 * @return
	 */
	public Set<RuleGraph> separateContextPositive(RuleGraph targetGraph) {
		Set<RuleGraph> result = new HashSet<RuleGraph>();
		for (NegativeApplicationCondition nac : SamGraphInvCheckGraphAdapter.getInstance(targetGraph).getNacs()) {
			RuleGraph newGraph = null;
			Match match = InvariantCheckerUtil.copyAsRuleGraph(targetGraph);
			for (Node n : match.getNodeMatching().values()) {
				if (n != null) {
					newGraph = (RuleGraph) n.eContainer();
					break;
				}
			}
			for (Node n : nac.getNodes()) {
				newGraph.getNodes().add(n);
			}
			for (Edge e : nac.getEdges()) {
				newGraph.getEdges().add(e);
				if (!newGraph.getNodes().contains(e.getSource())) {
					e.setSource(match.getNodeMatching().get(e.getSource()));
				}
				if (!newGraph.getNodes().contains(e.getTarget())) {
					e.setTarget(match.getNodeMatching().get(e.getTarget()));
				}
			}
			result.add(newGraph);
		}
		return result;
	}

	public RuleGraph addContext(RuleGraph pattern, RuleGraph targetGraph) {
		if (pattern.getCondition() == null) {
			return null;
		}
		if (pattern.getCondition().eClass() == SamgraphconditionPackage.eINSTANCE.getLogicalGCCoupling()
				&& ((LogicalGCCoupling) pattern.getCondition()).getOperands().size() != 1) {
			throw new UnsupportedOperationException();
		}

		Graph g = null;
		Match tmpMatch = null;
		ipm.reset();
		if (targetGraph.getCondition() != null) {
			NegativeApplicationCondition nac = SamGraphInvCheckGraphAdapter.getInstance(targetGraph).getNacs().get(0);
			tmpMatch = SubgraphIterator.fullNacToGraph(nac, false);
			for (Node n : tmpMatch.getNodeMatching().values()) {
				g = (Graph) n.eContainer();
				break;
			}
		} else {
			tmpMatch = InvariantCheckerUtil.copyAsRuleGraph(targetGraph);
			for (Node n : tmpMatch.getNodeMatching().values()) {
				g = (Graph) n.eContainer();
				break;
			}
		}
		ipm.setHostGraph(g);
		ipm.setPattern(pattern);
		ipm.setCurrentSubGraph(SubgraphIterator.graphToPosSubGraph(pattern));

		Match nextMatch = ipm.getNextMatching();
		if (nextMatch == null) {
			return null;
		}
		nacT.reset();
		nacT.setPattern(pattern);
		nacT.setMergedGraph(targetGraph);
		nacT.setInitialMatching(nextMatch);
		RuleGraph result = nacT.translate();

		// reform NACs in result
		// for (NegativeApplicationCondition nac : )

		return result;
	}

	/**
	 * @deprecated
	 * @param pattern
	 * @param targetGraph
	 * @return
	 */
	public RuleGraph addContextPositive(RuleGraph pattern, RuleGraph targetGraph) {
		if (pattern.getCondition() == null) {
			return null;
		}
		if (pattern.getCondition().eClass() == SamgraphconditionPackage.eINSTANCE.getLogicalGCCoupling()
				&& ((LogicalGCCoupling) pattern.getCondition()).getOperands().size() != 1) {
			throw new UnsupportedOperationException();
		}

		ipm.setHostGraph(targetGraph);

		// have to transfer nacs to original graph

		ipm.setPattern(pattern);
		ipm.setCurrentSubGraph(SubgraphIterator.graphToPosSubGraph(pattern));

		Match nextMatch = ipm.getNextMatching();
		if (nextMatch == null) {
			return null;
		}
		nacT.reset();
		nacT.setPattern(pattern);
		nacT.setMergedGraph(targetGraph);
		nacT.setInitialMatching(nextMatch);
		RuleGraph result = nacT.translate();

		return result;
	}

}