Skip to content

Commit

Permalink
Fixing ConflictCause construction in ArrayAssignment, adding related …
Browse files Browse the repository at this point in the history
…solver test.
  • Loading branch information
AntoniusW committed Jun 23, 2017
1 parent cc2d766 commit a65421f
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -225,14 +225,16 @@ private ConflictCause assignWithDecisionLevel(int atom, ThriceTruth value, NoGoo

// Check consistency.
if (!assignmentsConsistent(current, value)) {
ConflictCause conflictCause = null;
ConflictCause conflictCause = new ConflictCause(impliedBy);
// Assignments are inconsistent, prepare the reason.
NoGood violated = impliedBy;
if (decisionLevel < current.getWeakDecisionLevel()) {
// New assignment is lower than the current one, hence cause is the reason for the (higher) current one.
violated = current.getPrevious() == null ? current.getImpliedBy() : current.getPrevious().getImpliedBy(); // take MBT reason if it exists.
if (violated == null) {
conflictCause = new ConflictCause(current);
} else {
conflictCause = new ConflictCause(violated);
}
// The lower assignment takes precedence over the current value, overwrite it and adjust mbtCounter.
if (current.getTruth() == MBT) {
Expand All @@ -244,7 +246,6 @@ private ConflictCause assignWithDecisionLevel(int atom, ThriceTruth value, NoGoo
}

}
conflictCause = new ConflictCause(impliedBy);
return conflictCause;
}

Expand Down
26 changes: 26 additions & 0 deletions src/test/java/at/ac/tuwien/kr/alpha/solver/SolverTests.java
Original file line number Diff line number Diff line change
Expand Up @@ -862,4 +862,30 @@ public void noPositiveCycleSelfFoundingGuess() throws IOException {
Set<AnswerSet> answerSets = solver.collectSet();
assertTrue(answerSets.isEmpty());
}

@Test
public void conflictFromUnaryNoGood() throws IOException {
String program =
"d(b).\n" +
"sel(X) :- not nsel(X), d(X).\n" +
"nsel(X) :- not sel(X), d(X).\n" +
"t(a) :- sel(b).\n" +
":- t(X).\n";

ParsedProgram parsedProgram = parseVisit(program);
NaiveGrounder grounder = new NaiveGrounder(parsedProgram);
Solver solver = getInstance(grounder);

Set<AnswerSet> expected = new HashSet<>(Collections.singletonList(
new BasicAnswerSet.Builder()
.predicate("d")
.instance("b")
.predicate("nsel")
.instance("b")
.build()
));

Set<AnswerSet> answerSets = solver.collectSet();
assertEquals(expected, answerSets);
}
}

0 comments on commit a65421f

Please sign in to comment.