[LOGIC-100] pruning of unsatisfiable non-ground disequalities Created: 07/Jan/13 Updated: 28/Jul/13 Resolved: 07/Jan/13
|Reporter:||Nada Amin||Assignee:||David Nolen|
Not sure whether we actually want to do anything about this.
When running this snippet,
we get the result:
The reified != constraint is arguably spurious, because of the occurs-check.
Even if we instantiate the a:
we get the result:
while there is no way the != constraint can be satisfied.
|Comment by Nada Amin [ 07/Jan/13 7:25 AM ]|
logic-100.diff contains a hackish fix: use unify instead of not= to deal with non-ground terms. Also, don't add the constraint if you know that some pairs cannot be unified upfront (this is needed b/c disunify and unify are not consistent wrt occurs-check).
|Comment by David Nolen [ 07/Jan/13 8:37 AM ]|
Well it is possible to disable occurs-check. Why can't we just use the existing occurs-check fn to do this work?
|Comment by Nada Amin [ 07/Jan/13 9:35 AM ]|
There are two issues. The first one is that it's too conservative to just prune != constraints by checking that ground term pairs are not=, because [1 w] and [2 z] should also be pruned. Here is an extra test case illustrating this:
On master, the second one fails b/c it has the extra constraint
which we ought to prune.
The second issue is that disunify does not take the occurs-check into account, so it can create a !=c that is not considered runnable, but if run, would be rightly pruned by the new unify clause (if the occurs-check is enabled).
|Comment by David Nolen [ 07/Jan/13 10:39 AM ]|
Ok, makes sense. Can we get a new patch using master. This one doesn't apply anymore. Thanks!
|Comment by Nada Amin [ 07/Jan/13 10:50 AM ]|
logic-100-rebase.diff is a new patch against master. I also added the extra tests discussed above.
|Comment by David Nolen [ 07/Jan/13 11:00 AM ]|