Conflict generalisation

src/main/java/at/ac/tuwien/kr/alpha/Util.java

@@ -1,5 +1,5 @@
-/**
- * Copyright (c) 2016, the Alpha Team.
+/*
+ * Copyright (c) 2016-2020, the Alpha Team.
  * All rights reserved.
  *
  * Additional changes made by Siemens.
@@ -33,8 +33,13 @@
 import java.nio.channels.ReadableByteChannel;
 import java.nio.charset.StandardCharsets;
 import java.util.AbstractMap;
+import java.util.Collection;
+import java.util.Collections;
+import java.util.Comparator;
 import java.util.Iterator;
+import java.util.LinkedHashSet;
 import java.util.Map;
+import java.util.Set;
 import java.util.SortedSet;
 import java.util.StringJoiner;
 import java.util.stream.Collector;
@@ -52,6 +57,13 @@ public static <K, V> Map.Entry<K, V> entry(K key, V value) {
 		return Collectors.toMap(Map.Entry::getKey, Map.Entry::getValue);
 	}
 
+	public static <K, V extends Integer> K getKeyWithMaximumValue(Map<K, V> map) {
+		if (map.isEmpty()) {
+			return null;
+		}
+		return Collections.max(map.entrySet(), Comparator.comparingInt(Map.Entry::getValue)).getKey();
+	}
+
 	public static <E> String join(String prefix, Iterable<E> iterable, String suffix) {
 		return join(prefix, iterable, ", ", suffix);
 	}
@@ -117,4 +129,22 @@ public static int arrayGrowthSize(int oldSize) {
 		// Growth factor is 1.5.
 		return oldSize + (oldSize >> 1);
 	}
+
+	public static Set<Integer> intArrayToLinkedHashSet(int[] array) {
+		final Set<Integer> set = new LinkedHashSet<>(array.length);
+		for (int element : array) {
+			set.add(element);
+		}
+		return set;
+	}
+
+	public static int[] collectionToIntArray(Collection<? extends Integer> collection) {
+		final int[] array = new int[collection.size()];
+		int i = 0;
+		for (Integer element : collection) {
+			array[i++] = element;
+		}
+		return array;
+	}
+
 }

src/main/java/at/ac/tuwien/kr/alpha/common/AtomStore.java

@@ -94,7 +94,7 @@ default String literalToString(int literal) {
 	 * @param noGood the nogood to translate
 	 * @return the string representation of the NoGood.
 	 */
-	default <T extends NoGoodInterface> String noGoodToString(T noGood) {
+	default <T extends NoGoodInterface<Integer>> String noGoodToString(T noGood) {
 		StringBuilder sb = new StringBuilder();
 
 		if (noGood.hasHead()) {

src/main/java/at/ac/tuwien/kr/alpha/common/Literals.java

@@ -1,5 +1,5 @@
-/**
- * Copyright (c) 2016-2019, the Alpha Team.
+/*
+ * Copyright (c) 2016-2020, the Alpha Team.
  * All rights reserved.
  *
  * Additional changes made by Siemens.
@@ -80,4 +80,19 @@ public static int positiveLiteral(int literal) {
 	public static String literalToString(int literal) {
 		return (isPositive(literal) ? "+" : "-") + atomOf(literal);
 	}
+
+	/**
+	 * Returns the index of the first position at which a literal of the given atom occurs in the given array of literals.
+	 * @param atom the atom to look for
+	 * @param literals an array of literals
+	 * @return the first index where the atom occurs, or -1 if it does not occur
+	 */
+	public static int findAtomInLiterals(int atom, int[] literals) {
+		for (int i = 0; i < literals.length; i++) {
+			if (atomOf(literals[i]) == atom) {
+				return i;
+			}
+		}
+		return -1;
+	}
 }

src/main/java/at/ac/tuwien/kr/alpha/common/NoGood.java

@@ -35,29 +35,36 @@
 import java.util.stream.IntStream;
 
 import static at.ac.tuwien.kr.alpha.Util.oops;
-import static at.ac.tuwien.kr.alpha.common.Literals.*;
-import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.*;
-
-public class NoGood implements NoGoodInterface, Comparable<NoGood> {
-	public static final int HEAD = 0;
+import static at.ac.tuwien.kr.alpha.common.Literals.atomOf;
+import static at.ac.tuwien.kr.alpha.common.Literals.isNegated;
+import static at.ac.tuwien.kr.alpha.common.Literals.isPositive;
+import static at.ac.tuwien.kr.alpha.common.Literals.negateLiteral;
+import static at.ac.tuwien.kr.alpha.common.Literals.positiveLiteral;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.INTERNAL;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.LEARNT;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.STATIC;
+import static at.ac.tuwien.kr.alpha.common.NoGoodInterface.Type.SUPPORT;
+
+public class NoGood implements NoGoodInterface<Integer>, Comparable<NoGood> {
 	public static final NoGood UNSAT = new NoGood();
 
 	protected final int[] literals;
 	private final boolean head;
 	private final Type type;
+	private NonGroundNoGood nonGroundNoGood;
 
 	public NoGood(int... literals) {
 		this(STATIC, literals, false);
 	}
-	
+
 	public NoGood(Type type, int... literals) {
 		this(type, literals, false);
 	}
-	
+
 	private NoGood(Type type, int[] literals, boolean head) {
 		this.type = type;
 		this.head = head;
-		if (head && !isNegated(literals[0])) {
+		if (head && !isNegated(literals[HEAD])) {
 			throw oops("Head is not negative");
 		}
 
@@ -80,8 +87,9 @@ protected NoGood(NoGood noGood) {
 		this.literals = noGood.literals.clone();
 		this.head = noGood.head;
 		this.type = noGood.type;
+		this.nonGroundNoGood = noGood.nonGroundNoGood;
 	}
-	
+
 	public static NoGood learnt(int... literals) {
 		return new NoGood(LEARNT, literals);
 	}
@@ -93,7 +101,7 @@ public static NoGood headFirst(int... literals) {
 	public static NoGood headFirstInternal(int... literals) {
 		return headFirst(INTERNAL, literals);
 	}
-	
+
 	public static NoGood headFirst(Type type, int... literals) {
 		return new NoGood(type, literals, true);
 	}
@@ -109,11 +117,11 @@ public static NoGood support(int headLiteral, int bodyRepresentingLiteral) {
 	public static NoGood fromConstraint(List<Integer> posLiterals, List<Integer> negLiterals) {
 		return new NoGood(addPosNeg(new int[posLiterals.size() + negLiterals.size()], posLiterals, negLiterals, 0));
 	}
-	
+
 	public static NoGood fromBody(List<Integer> posLiterals, List<Integer> negLiterals, int bodyRepresentingLiteral) {
 		return fromBody(STATIC, posLiterals, negLiterals, bodyRepresentingLiteral);
 	}
-	
+
 	public static NoGood fromBodyInternal(List<Integer> posLiterals, List<Integer> negLiterals, int bodyRepresentingLiteral) {
 		return fromBody(INTERNAL, posLiterals, negLiterals, bodyRepresentingLiteral);
 	}
@@ -144,6 +152,8 @@ public int size() {
 	public Antecedent asAntecedent() {
 		return new Antecedent() {
 
+			private final NoGood originalNoGood = NoGood.this;
+
 			@Override
 			public int[] getReasonLiterals() {
 				return NoGood.this.literals; // Beware: returned array must not be modified!
@@ -156,6 +166,11 @@ public void bumpActivity() {
 			@Override
 			public void decreaseActivity() {
 			}
+
+			@Override
+			public NoGood getOriginalNoGood() {
+				return originalNoGood;
+			}
 		};
 	}
 
@@ -171,7 +186,7 @@ public int getPositiveLiteral(int index) {
 	}
 
 	@Override
-	public int getLiteral(int index) {
+	public Integer getLiteral(int index) {
 		return literals[index];
 	}
 
@@ -180,16 +195,19 @@ public boolean hasHead() {
 		return head;
 	}
 
-	@Override
-	public int getHead() {
-		return getLiteral(HEAD);
-	}
-
 	@Override
 	public Type getType() {
 		return type;
 	}
 
+	public NonGroundNoGood getNonGroundNoGood() {
+		return nonGroundNoGood;
+	}
+
+	public void setNonGroundNoGood(NonGroundNoGood nonGroundNoGood) {
+		this.nonGroundNoGood = nonGroundNoGood;
+	}
+
 	@Override
 	public Iterator<Integer> iterator() {
 		return new Iterator<Integer>() {
@@ -211,6 +229,15 @@ public IntStream stream() {
 		return Arrays.stream(literals);
 	}
 
+	public int indexOf(int literal) {
+		for (int i = 0; i < literals.length; i++) {
+			if (literals[i] == literal) {
+				return i;
+			}
+		}
+		return -1;
+	}
+
 	@Override
 	public int compareTo(NoGood o) {
 		if (o == null) {

src/main/java/at/ac/tuwien/kr/alpha/common/NoGoodInterface.java

@@ -29,14 +29,16 @@
 
 import at.ac.tuwien.kr.alpha.solver.Antecedent;
 
-public interface NoGoodInterface extends Iterable<Integer> {
+public interface NoGoodInterface<T> extends Iterable<T> {
+
+	int HEAD = 0;
 
 	/**
 	 * Returns the literal at the given index.
 	 * @param index the index position within the NoGood.
 	 * @return the literal at the index.
 	 */
-	int getLiteral(int index);
+	T getLiteral(int index);
 
 	/**
 	 * Returns whether the NoGood has a head.
@@ -46,9 +48,11 @@ public interface NoGoodInterface extends Iterable<Integer> {
 
 	/**
 	 * Returns the head literal of the NoGood, if present.
-	 * @return the head literal if the NoGood has a head, otherwise an arbitrary integer.
+	 * @return the head literal if the NoGood has a head, otherwise an arbitrary literal.
 	 */
-	int getHead();
+	default T getHead() {
+		return getLiteral(HEAD);
+	}
 
 	/**
 	 * Returns the size, i.e., number of literals, in the NoGood.