content: /**
   * Copyright (c) 2018-2019, 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.grounder.structure;
  
  import static org.junit.jupiter.api.Assertions.assertFalse;
  import static org.junit.jupiter.api.Assertions.assertNotEquals;
  
  import java.util.Arrays;
  import java.util.Collections;
  import java.util.Set;
  import java.util.function.Function;
  
  import org.junit.jupiter.api.Test;
  
  import at.ac.tuwien.kr.alpha.api.config.SystemConfig;
  import at.ac.tuwien.kr.alpha.api.programs.Predicate;
  import at.ac.tuwien.kr.alpha.api.programs.ProgramParser;
  import at.ac.tuwien.kr.alpha.api.programs.atoms.Atom;
  import at.ac.tuwien.kr.alpha.api.programs.atoms.BasicAtom;
  import at.ac.tuwien.kr.alpha.api.programs.literals.Literal;
  import at.ac.tuwien.kr.alpha.commons.Predicates;
  import at.ac.tuwien.kr.alpha.commons.programs.atoms.Atoms;
  import at.ac.tuwien.kr.alpha.commons.programs.terms.Terms;
  import at.ac.tuwien.kr.alpha.core.common.AtomStore;
  import at.ac.tuwien.kr.alpha.core.common.AtomStoreImpl;
  import at.ac.tuwien.kr.alpha.core.grounder.NaiveGrounder;
  import at.ac.tuwien.kr.alpha.core.parser.ProgramParserImpl;
  import at.ac.tuwien.kr.alpha.core.programs.CompiledProgram;
  import at.ac.tuwien.kr.alpha.core.programs.InternalProgram;
  import at.ac.tuwien.kr.alpha.core.programs.transformation.NormalizeProgramTransformation;
  import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth;
  import at.ac.tuwien.kr.alpha.core.solver.TrailAssignment;
  
  /**
   * Copyright (c) 2018-2020, the Alpha Team.
   */
  public class AnalyzeUnjustifiedTest {
  
  	private final ProgramParser parser = new ProgramParserImpl();
  	private final NormalizeProgramTransformation normalize = new NormalizeProgramTransformation(SystemConfig.DEFAULT_AGGREGATE_REWRITING_CONFIG);
  	private final Function<String, CompiledProgram> parseAndPreprocess = (str) -> {
  		return InternalProgram.fromNormalProgram(normalize.apply(parser.parse(str)));
  	};
  
  	@Test
  	public void justifySimpleRules() {
  		String program = "p(X) :- q(X)." +
  			"q(X) :- p(X)." +
  			"q(5) :- r." +
  			"r :- not nr." +
  			"nr :- not r." +
  			":- not p(5).";
  		CompiledProgram internalProgram = parseAndPreprocess.apply(program);
  		AtomStore atomStore = new AtomStoreImpl();
  		NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true);
  		grounder.getNoGoods(null);
  		TrailAssignment assignment = new TrailAssignment(atomStore);
  		int rId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("r", 0)));
  		int nrId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("nr", 0)));
  		assignment.growForMaxAtomId();
  		assignment.assign(rId, ThriceTruth.FALSE);
  		assignment.assign(nrId, ThriceTruth.TRUE);
  		BasicAtom p5 = Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Collections.singletonList(Terms.newConstant(5)));
  		assignment.assign(atomStore.get(p5), ThriceTruth.MBT);
  		Set<Literal> reasons = grounder.justifyAtom(atomStore.get(p5), assignment);
  		assertFalse(reasons.isEmpty());
  	}
  
  	@Test
  	public void justifyLargerRules() {
  		String program = "p(X) :- q(X,Y), r(Y), not s(X,Y)." +
  			"{ q(1,X)} :- dom(X)." +
  			"dom(1..3)." +
  			"{r(X)} :- p(X)." +
  			"{r(2)}." +
  			"{s(1,2)}." +
  			":- not p(1).";
  		CompiledProgram internalProgram = parseAndPreprocess.apply(program);
  		AtomStore atomStore = new AtomStoreImpl();
  		NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true);
  		grounder.getNoGoods(null);
  		TrailAssignment assignment = new TrailAssignment(atomStore);
  		Atom p1 = parser.parse("p(1).").getFacts().get(0);
  		Atom r2 = parser.parse("r(2).").getFacts().get(0);
  		Atom s12 = parser.parse("s(1,2).").getFacts().get(0);
  		Atom q11 = parser.parse("q(1,1).").getFacts().get(0);
  		Atom q12 = parser.parse("q(1,2).").getFacts().get(0);
  		Atom q13 = parser.parse("q(1,3).").getFacts().get(0);
  		int p1Id = atomStore.get(p1);
  		int r2Id = atomStore.get(r2);
  		int s12Id = atomStore.get(s12);
  		int q11Id = atomStore.get(q11);
  		int q12Id = atomStore.get(q12);
  		int q13Id = atomStore.get(q13);
  		assignment.growForMaxAtomId();
  		assignment.assign(p1Id, ThriceTruth.MBT);
  		assignment.assign(r2Id, ThriceTruth.TRUE);
  		assignment.assign(s12Id, ThriceTruth.TRUE);
  		assignment.assign(q11Id, ThriceTruth.TRUE);
  		assignment.assign(q12Id, ThriceTruth.TRUE);
  		assignment.assign(q13Id, ThriceTruth.FALSE);
  
  		Set<Literal> reasons = grounder.justifyAtom(p1Id, assignment);
  		assertFalse(reasons.isEmpty());
  	}
  
  	@Test
  	public void justifyMultipleReasons() {
  		String program = "n(a). n(b). n(c). n(d). n(e)." +
  			"s(a,b). s(b,c). s(c,d). s(d,e)." +
  			"{ q(X) } :- n(X)." +
  			"p(X) :- q(X)." +
  			"p(X) :- p(Y), s(Y,X)." +
  			":- not p(c).";
  		CompiledProgram internalProgram = parseAndPreprocess.apply(program);
  		AtomStore atomStore = new AtomStoreImpl();
  		NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true);
  		grounder.getNoGoods(null);
  		TrailAssignment assignment = new TrailAssignment(atomStore);
  		Atom qa = parser.parse("q(a).").getFacts().get(0);
  		Atom qb = parser.parse("q(b).").getFacts().get(0);
  		Atom qc = parser.parse("q(c).").getFacts().get(0);
  		Atom qd = parser.parse("q(d).").getFacts().get(0);
  		Atom qe = parser.parse("q(e).").getFacts().get(0);
  		int qaId = atomStore.get(qa);
  		int qbId = atomStore.get(qb);
  		int qcId = atomStore.get(qc);
  		int qdId = atomStore.get(qd);
  		int qeId = atomStore.get(qe);
  
  		assignment.growForMaxAtomId();
  		assignment.assign(qaId, ThriceTruth.FALSE);
  		assignment.assign(qbId, ThriceTruth.FALSE);
  		assignment.assign(qcId, ThriceTruth.FALSE);
  		assignment.assign(qdId, ThriceTruth.FALSE);
  		assignment.assign(qeId, ThriceTruth.FALSE);
  
  		Predicate nq = Predicates.getPredicate("_nq", 2, true);
  		Atom nqa = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("a")));
  		Atom nqb = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("b")));
  		Atom nqc = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("c")));
  		Atom nqd = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("d")));
  		Atom nqe = Atoms.newBasicAtom(nq, Arrays.asList(Terms.newConstant("1"), Terms.newSymbolicConstant("e")));
  		int nqaId = atomStore.get(nqa);
  		int nqbId = atomStore.get(nqb);
  		int nqcId = atomStore.get(nqc);
  		int nqdId = atomStore.get(nqd);
  		int nqeId = atomStore.get(nqe);
  
  		assignment.growForMaxAtomId();
  		assignment.assign(nqaId, ThriceTruth.TRUE);
  		assignment.assign(nqbId, ThriceTruth.TRUE);
  		assignment.assign(nqcId, ThriceTruth.TRUE);
  		assignment.assign(nqdId, ThriceTruth.TRUE);
  		assignment.assign(nqeId, ThriceTruth.TRUE);
  
  		Atom pc = parser.parse("p(c).").getFacts().get(0);
  		Set<Literal> reasons = grounder.justifyAtom(atomStore.get(pc), assignment);
  		assertFalse(reasons.isEmpty());
  	}
  
  	@Test
  	public void justifyNegatedFactsRemovedFromReasons() {
  		String program = "forbidden(2,9). forbidden(1,9)." +
  			"p(X) :- q(X)." +
  			"q(X) :- p(X)." +
  			"q(5) :- r." +
  			"r :- not nr, not forbidden(2,9), not forbidden(1,9)." +
  			"nr :- not r." +
  			":- not p(5).";
  		CompiledProgram internalProgram = parseAndPreprocess.apply(program);
  		AtomStore atomStore = new AtomStoreImpl();
  		NaiveGrounder grounder = new NaiveGrounder(internalProgram, atomStore, true);
  		grounder.getNoGoods(null);
  		TrailAssignment assignment = new TrailAssignment(atomStore);
  		int rId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("r", 0)));
  		int nrId = atomStore.get(Atoms.newBasicAtom(Predicates.getPredicate("nr", 0)));
  		assignment.growForMaxAtomId();
  		assignment.assign(rId, ThriceTruth.FALSE);
  		assignment.assign(nrId, ThriceTruth.TRUE);
  		BasicAtom p5 = Atoms.newBasicAtom(Predicates.getPredicate("p", 1), Collections.singletonList(Terms.newConstant(5)));
  		assignment.assign(atomStore.get(p5), ThriceTruth.MBT);
  		Set<Literal> reasons = grounder.justifyAtom(atomStore.get(p5), assignment);
  		assertFalse(reasons.isEmpty());
  		for (Literal literal : reasons) {
  			// Check that facts are not present in justification.
  			assertNotEquals(literal.getPredicate(), Predicates.getPredicate("forbidden", 2));
  		}
  	}
  }
  