Bugs in XSB with outputvoc
Issue #935
new
See, e.g.,
vocabulary V{
type LTL constructed from {B, X(LTL)}
True(LTL)
ToCheck:LTL
IsTrue
}
theory T:V{
{
IsTrue <- True(X(X(B))).
True(B).
True(X(x)) <- True(x).
}
}
structure S:V{
ToCheck = X(X(B))
}
vocabulary interesting{
extern V::IsTrue/0
}
vocabulary V2{
True(nat)
IsTrue
}
theory T2:V2{
{
IsTrue <- True(2).
True(0).
True(x+1) <- True(x).
}
}
structure S2:V2{
}
vocabulary interesting2{
extern V2::IsTrue/0
}
procedure main(){
print(calculatedefinitions(T2,S2,interesting2))
print(calculatedefinitions(T,S,interesting))
}
The firs call gives a wrong result.
The second (though for XSB this should have the same complexity) does not end.
Comments (8)
-
-
reporter
For T2S2, due to the outputvocabulary, XSB can do this in finite time
-
Correction, T2 and S2 should be T and S (and vice versa) in the previous 2 comments.
-
T,S (the constructed type ones) work, if you turn of definition splitting. * edit: I see this as something that should be solved in splitdefs, not in XSB. For IDP to split definitions, to only have the calcdef inference join them again afterwards seems wrong.
-
T2,S2 will require quite some work to fix. They require a rewrite of the built-in arithmatic operator translations to a version that is equally flexible as IDP is. (e.g. look at the example for ixdivision/3 in the XSB built-in code in PrologProgram.cpp).
However, after this, also a more intelligent reordering of the clause must be done. Right now, the reordering algorithm causes a general call to True/1, whilst we only want to call it for specific instances. This call True(X) (with X not bound) causes an infinite running time.
-
reporter
Some fishy output with verbosity high enough for calcdef:
Evaluating the following symbols: IsTrue CalculateDefinitions is NOT able to calculate the following symbols, even though it was (implicitly) asked: IsTrue Calculating known definitions of (at most) the following symbols: True, IsTrue... -
reporter
Do I get it right that the fix for this is: depending on the context, we should write X=Y+1 either like this or like Y=X-1 in order to optimize call patterns?
And then the issue should be fixed, right?
-
@fishy output That is fixed in my current branch.
This fix consists of 2 parts
1) the fix you mentioned in the comment above this
2) making sure that a recursive call to a predicate is done later than it is now (if it is possible that there is a generator for some of the arguments, use those first)
- Log in to comment
There are two different issues here.
T2,S2 do not work (and run infinitely) because the model has infinite size. The relation True(x) contains B, X(B), X(X(B)), X(X(X(B))) ... Because there is no specific query, the entire interpretation for True(x) is calculated. This takes an infinite amount of time. I would not call this a bug. This is unsupported behaviour.
T,S do not work because of a lack of proper reordering (the set of natural numbers is used as a generator). Because an error is thrown, the result is empty (error throwing in XSB is buggy, and this is not IDP's fault). This can be fixed through a refactor of the body reordering algorithm. However, it seems that this happens in several places at the moment, so this would come at a developing cost of at least 2 days I estimate.