content: package at.ac.tuwien.kr.alpha.core.solver.learning;
  
  import static at.ac.tuwien.kr.alpha.core.common.NoGoodTest.fromOldLiterals;
  import static at.ac.tuwien.kr.alpha.core.solver.AntecedentTest.antecedentsEquals;
  import static org.junit.jupiter.api.Assertions.assertEquals;
  import static org.junit.jupiter.api.Assertions.assertFalse;
  import static org.junit.jupiter.api.Assertions.assertNotNull;
  import static org.junit.jupiter.api.Assertions.assertNull;
  import static org.junit.jupiter.api.Assertions.assertTrue;
  
  import org.junit.jupiter.api.Disabled;
  import org.junit.jupiter.api.Test;
  
  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.common.NoGood;
  import at.ac.tuwien.kr.alpha.core.solver.Antecedent;
  import at.ac.tuwien.kr.alpha.core.solver.ConflictCause;
  import at.ac.tuwien.kr.alpha.core.solver.NoGoodStore;
  import at.ac.tuwien.kr.alpha.core.solver.NoGoodStoreAlphaRoaming;
  import at.ac.tuwien.kr.alpha.core.solver.ThriceTruth;
  import at.ac.tuwien.kr.alpha.core.solver.TrailAssignment;
  import at.ac.tuwien.kr.alpha.core.solver.WritableAssignment;
  import at.ac.tuwien.kr.alpha.core.test.util.TestUtils;
  
  /**
   * Copyright (c) 2016-2019, the Alpha Team.
   */
  public class GroundConflictNoGoodLearnerTest {
  
  	private final WritableAssignment assignment;
  	private final NoGoodStore store;
  	private AtomStore atomStore;
  
  	public GroundConflictNoGoodLearnerTest() {
  		atomStore = new AtomStoreImpl();
  		TestUtils.fillAtomStore(atomStore, 20);
  		this.assignment = new TrailAssignment(atomStore);
  		this.assignment.growForMaxAtomId();
  		this.store = new NoGoodStoreAlphaRoaming(assignment);
  		this.store.growForMaxAtomId(20);
  	}
  
  	@Test
  	public void smallConflictNonTrivial1UIP() {
  		GroundConflictNoGoodLearner learner = new GroundConflictNoGoodLearner(assignment, atomStore);
  
  		NoGood n1 = new NoGood(fromOldLiterals(2, -8, 1));
  		NoGood n2 = new NoGood(fromOldLiterals(-1, -7));
  		NoGood n3 = new NoGood(fromOldLiterals(-3, 1));
  		NoGood n4 = new NoGood(fromOldLiterals(5, 3));
  		NoGood n5 = new NoGood(fromOldLiterals(6, -5));
  		NoGood n6 = new NoGood(fromOldLiterals(4, -2));
  		NoGood n7 = new NoGood(fromOldLiterals(-6, -4));
  		store.add(10, n1);
  		store.add(11, n2);
  		store.add(12, n3);
  		store.add(13, n4);
  		store.add(14, n5);
  		store.add(15, n6);
  		store.add(16, n7);
  
  		assignment.choose(9, ThriceTruth.TRUE);
  		assignment.choose(8, ThriceTruth.FALSE);
  		assertNull(store.propagate());
  		assertFalse(store.didPropagate());
  		assignment.choose(7, ThriceTruth.FALSE);
  		ConflictCause conflictCause = store.propagate();
  		assertTrue(store.didPropagate());
  
  		assertNotNull(conflictCause);
  		Antecedent violatedNoGood = conflictCause.getAntecedent();
  		assertNotNull(violatedNoGood);
  		assertTrue(antecedentsEquals(violatedNoGood, n5.asAntecedent()) || antecedentsEquals(violatedNoGood, n7.asAntecedent()));
  		GroundConflictNoGoodLearner.ConflictAnalysisResult analysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent());
  		NoGood learnedNoGood = analysisResult.learnedNoGood;
  		assertEquals(new NoGood(fromOldLiterals(1, -8)), learnedNoGood);
  		int backjumpingDecisionLevel = analysisResult.backjumpLevel;
  		assertEquals(backjumpingDecisionLevel, 2);
  	}
  
  	@Test
  	@Disabled("TrailAssignment no longer propagates at lower decision level.")
  	public void subCurrentDLPropagationWithChoiceCauseOfConflict() {
  		GroundConflictNoGoodLearner learner = new GroundConflictNoGoodLearner(assignment, atomStore);
  		NoGood n1 = new NoGood(fromOldLiterals(1, -2));
  		NoGood n2 = new NoGood(fromOldLiterals(2, 3));
  		store.add(10, n1);
  		assignment.choose(1, ThriceTruth.TRUE);
  		assignment.choose(3, ThriceTruth.TRUE);
  		store.propagate();
  		assertEquals(ThriceTruth.MBT, assignment.get(2).getTruth());
  		assertEquals(1, assignment.get(2).getDecisionLevel());
  		ConflictCause conflictCause = store.add(11, n2);
  		assertNotNull(conflictCause);
  		assertNotNull(conflictCause.getAntecedent());
  		GroundConflictNoGoodLearner.ConflictAnalysisResult conflictAnalysisResult = learner.analyzeConflictingNoGood(conflictCause.getAntecedent());
  		assertNull(conflictAnalysisResult.learnedNoGood);
  		assertEquals(2, conflictAnalysisResult.backjumpLevel);
  
  	}
  }
  