Skip to content
This repository was archived by the owner on Feb 1, 2020. It is now read-only.
This repository was archived by the owner on Feb 1, 2020. It is now read-only.

Problem in ConstrainedTerm.evaluateConstraints  #2408

@kheradmand

Description

@kheradmand

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions