Problem in ConstrainedTerm.evaluateConstraints
kheradmand opened this issue · 1 comments
I can not give a small example here, but sometimes when I use krun, a rule that I expect to apply, does not get normally applied, but when I use a debugger and go step by step, the rule gets applied.
I tried to narrow the scope of the problem, the problem seems to be in the function ConstrainedTerm.evaluateConstraints
:
public static List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> evaluateConstraints(
ConjunctiveFormula constraint,
ConjunctiveFormula subjectConstraint,
ConjunctiveFormula patternConstraint,
Set<Variable> variables,
TermContext context) {
context.setTopConstraint(subjectConstraint);
List<ConjunctiveFormula> candidates = constraint.getDisjunctiveNormalForm().conjunctions().stream()
.map(c -> c.addAndSimplify(patternConstraint, context))
.filter(c -> !c.isFalse())
.map(ConjunctiveFormula::resolveNonDeterministicLookups)
.map(ConjunctiveFormula::getDisjunctiveNormalForm)
.map(DisjunctiveFormula::conjunctions)
.flatMap(List::stream)
.map(c -> c.simplify(context))
.filter(c -> !c.isFalse())
.collect(Collectors.toList());
int x = candidates.size(); //added by me
List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> solutions = Lists.newArrayList();
for (ConjunctiveFormula candidate : candidates) {
...
}
....
If I set a breakpoint after int x = candidates.size();
, the value of x
is 0
but if I put a break point right before that line and then evaluate one step, the value of x
becomes 1
.
I am not familiar with the code base (or Java 8 streams) but this phenomenon makes me suspect that this is a concurrency bug. Possibily
List<ConjunctiveFormula> candidates = ...
is being evaluated is being evaluated in a separate thread that has data race with the thread executing the rest of the function.
It is most probably not a concurrency problem because first of all I don't think there are multiple threads involved here, and second, even adding a long delay does not solve the problem:
public static List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> evaluateConstraints(
ConjunctiveFormula constraint,
ConjunctiveFormula subjectConstraint,
ConjunctiveFormula patternConstraint,
Set<Variable> variables,
TermContext context) {
context.setTopConstraint(subjectConstraint);
List<ConjunctiveFormula> candidates = constraint.getDisjunctiveNormalForm().conjunctions().stream()
.map(c -> c.addAndSimplify(patternConstraint, context))
.filter(c -> !c.isFalse())
.map(ConjunctiveFormula::resolveNonDeterministicLookups)
.map(ConjunctiveFormula::getDisjunctiveNormalForm)
.map(DisjunctiveFormula::conjunctions)
.flatMap(List::stream)
.map(c -> c.simplify(context))
.filter(c -> !c.isFalse())
.collect(Collectors.toList());
try {
Thread.sleep(1000);
} catch (InterruptedException e) {
e.printStackTrace();
}
int x = candidates.size();
List<Triple<ConjunctiveFormula, Boolean, Map<scala.collection.immutable.List<Pair<Integer, Integer>>, Term>>> solutions = Lists.newArrayList();
for (ConjunctiveFormula candidate : candidates) {
...
I really don't know what the problem may be.