Fixed: too few split names were considered (again!).
The fix from f46b9745 was insufficient. One plus name for all splits is not sufficient. For two constants a, b, (a = b) is not valid. To see that on split level 2, at least two names must be considered. So the new fix is a combination of the pre-f46b9745 state and the f46b9745-fix. Another, simpler way to deal with split names is probably to assume that the query only mentions quasi-primitive literals. Any non-quasi-primitive clause could be brought into this normal form by replacing (f(t) = g(t)) by (g(t) != x v f(t) = x) and (f(t) = x) by (t != y v f(y) = x). The solution is simple because it makes - Grounder::Flatten (although we should recycle it in Formula::NF()), - Grounder::PlusSplitNames(), - Solver::ResolveDeterminedTerms() obsolete. As we then drop Solver::ResolveDeterminedTerms(), the reasoner would even preserve soundness (if we keep it, the reasoner would still fall into the (c = d) trap for k >= 2).
Loading
Please register or sign in to comment