content: /*
   * Copyright (c) 2016-2020, the Alpha Team.
   * All rights reserved.
   *
   * Additional changes made by Siemens.
   *
   * Redistribution and use in source and binary forms, with or without
   * modification, are permitted provided that the following conditions are met:
   *
   * 1) Redistributions of source code must retain the above copyright notice, this
   *    list of conditions and the following disclaimer.
   *
   * 2) Redistributions in binary form must reproduce the above copyright notice,
   *    this list of conditions and the following disclaimer in the documentation
   *    and/or other materials provided with the distribution.
   *
   * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
   * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
   * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
   * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
   * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
   * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
   * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
   * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
   * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
   * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
   */
  package at.ac.tuwien.kr.alpha.core.common;
  
  import at.ac.tuwien.kr.alpha.commons.util.Util;
  import at.ac.tuwien.kr.alpha.core.solver.Antecedent;
  
  import java.util.Arrays;
  import java.util.Iterator;
  import java.util.List;
  import java.util.stream.IntStream;
  
  import static at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type.INTERNAL;
  import static at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type.LEARNT;
  import static at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type.STATIC;
  import static at.ac.tuwien.kr.alpha.core.common.NoGoodInterface.Type.SUPPORT;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.atomOf;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isNegated;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.isPositive;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.negateLiteral;
  import static at.ac.tuwien.kr.alpha.core.programs.atoms.Literals.positiveLiteral;
  
  public class NoGood implements NoGoodInterface, Comparable<NoGood> {
  	public static final int HEAD = 0;
  	public static final NoGood UNSAT = new NoGood();
  
  	protected final int[] literals;
  	private final boolean head;
  	private final Type type;
  
  	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])) {
  			throw Util.oops("Head is not negative");
  		}
  
  		// HINT: this might decrease performance if NoGoods are mostly small.
  		Arrays.sort(literals, head ? 1 : 0, literals.length);
  
  		int shift = 0;
  		for (int i = 1; i < literals.length; i++) {
  			if (literals[i - 1] == literals[i]) { // check for duplicate
  				shift++;
  			}
  			literals[i - shift] = literals[i]; // Remove duplicates in place by shifting remaining literals.
  		}
  
  		// copy-shrink array if needed.
  		this.literals = shift <= 0 ? literals : Arrays.copyOf(literals, literals.length - shift);
  	}
  
  	protected NoGood(NoGood noGood) {
  		this.literals = noGood.literals.clone();
  		this.head = noGood.head;
  		this.type = noGood.type;
  	}
  	
  	public static NoGood learnt(int... literals) {
  		return new NoGood(LEARNT, literals);
  	}
  
  	public static NoGood headFirst(int... literals) {
  		return headFirst(STATIC, 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);
  	}
  
  	public static NoGood fact(int literal) {
  		return headFirst(literal);
  	}
  
  	public static NoGood support(int headLiteral, int bodyRepresentingLiteral) {
  		return new NoGood(SUPPORT, headLiteral, negateLiteral(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);
  	}
  
  	public static NoGood fromBody(Type type, List<Integer> posLiterals, List<Integer> negLiterals, int bodyRepresentingLiteral) {
  		int[] bodyLiterals = new int[posLiterals.size() + negLiterals.size() + 1];
  		bodyLiterals[0] = negateLiteral(bodyRepresentingLiteral);
  		return NoGood.headFirst(type, addPosNeg(bodyLiterals, posLiterals, negLiterals, 1));
  	}
  
  	private static int[] addPosNeg(int[] literals, List<Integer> posLiterals, List<Integer> negLiterals, int offset) {
  		int i = offset;
  		for (Integer literal : posLiterals) {
  			literals[i++] = literal;
  		}
  		for (Integer literal : negLiterals) {
  			literals[i++] = negateLiteral(literal);
  		}
  		return literals;
  	}
  
  	@Override
  	public int size() {
  		return literals.length;
  	}
  
  	@Override
  	public Antecedent asAntecedent() {
  		return new Antecedent() {
  
  			@Override
  			public int[] getReasonLiterals() {
  				return NoGood.this.literals; // Beware: returned array must not be modified!
  			}
  
  			@Override
  			public void bumpActivity() {
  			}
  
  			@Override
  			public void decreaseActivity() {
  			}
  
  			@Override
  			public String toString() {
  				return NoGood.this + "(unwatched)";
  			}
  		};
  	}
  
  	public NoGood withoutHead() {
  		return new NoGood(type, literals.clone());
  	}
  
  	/**
  	 * A shorthand for <code>Literals.positiveLiteral(getLiteral(...))</code>
  	 */
  	public int getPositiveLiteral(int index) {
  		return positiveLiteral(getLiteral(index));
  	}
  
  	@Override
  	public int getLiteral(int index) {
  		return literals[index];
  	}
  
  	@Override
  	public boolean hasHead() {
  		return head;
  	}
  
  	@Override
  	public int getHead() {
  		return getLiteral(HEAD);
  	}
  
  	@Override
  	public Type getType() {
  		return type;
  	}
  
  	@Override
  	public Iterator<Integer> iterator() {
  		return new Iterator<Integer>() {
  			private int i;
  
  			@Override
  			public boolean hasNext() {
  				return literals.length > i;
  			}
  
  			@Override
  			public Integer next() {
  				return literals[i++];
  			}
  		};
  	}
  
  	public IntStream stream() {
  		return Arrays.stream(literals);
  	}
  
  	@Override
  	public int compareTo(NoGood o) {
  		if (o == null) {
  			throw new NullPointerException("Cannot compare against null.");
  		}
  
  		if (o.head && !head) {
  			return -1;
  		}
  
  		if (!o.head && head) {
  			return +1;
  		}
  
  		if (o.literals.length > literals.length) {
  			return -1;
  		}
  
  		if (o.literals.length < literals.length) {
  			return +1;
  		}
  
  		for (int i = 0; i < literals.length; i++) {
  			if (o.literals[i] > literals[i]) {
  				return -1;
  			}
  			if (o.literals[i] < literals[i]) {
  				return +1;
  			}
  		}
  
  		return 0;
  	}
  
  	@Override
  	public boolean equals(Object o) {
  		if (this == o) {
  			return true;
  		}
  		if (o == null || getClass() != o.getClass()) {
  			return false;
  		}
  
  		NoGood noGood = (NoGood) o;
  
  		return head == noGood.head && Arrays.equals(literals, noGood.literals);
  	}
  
  	@Override
  	public int hashCode() {
  		return 31 * Arrays.hashCode(literals) * (head ? +1 : -1);
  	}
  
  	@Override
  	public String toString() {
  		StringBuilder sb = new StringBuilder();
  
  		if (head) {
  			sb.append("*");
  		}
  
  		sb.append("{ ");
  
  		for (int literal : literals) {
  			sb.append(isPositive(literal) ? "+" : "-");
  			sb.append(atomOf(literal));
  			sb.append(" ");
  		}
  
  		sb.append("}");
  
  		return sb.toString();
  	}
  
  }
  