karmaresearch / vlog

Apache License 2.0
55 stars 9 forks source link

Incomplete query answering for rules with partially grounded atoms in the body #95

Closed alloka closed 2 years ago

alloka commented 2 years ago

Using Rulewerk Syntax, consider the following example:

We have the following edb facts: cont(d12).
cont(d6). cont(d13). cont(d7). cont(d3). cont(d2). fetch(d11,b11). fetch(d3,b5). fetch(d1,b2). fetch(d11,b12). fetch(d3,b6). fetch(d3,b4). fetch(d1,b1). fetch(d3,b3). fetch(d8,b7). offset(d12). offset(d15). offset(d6). offset(d8). offset(d2). putOn(b11,d13). putOn(b1,d3). putOn(b5,d8). putOn(b4,d7). putOn(b3,d6). putOn(b11,d12). putOn(b1,d2). putOn(b1,d4). putOn(b11,d14). putOn(b6,d9).

and the following rules: buildWall_p(?x1, ?x0,!p) :- inv(?x1, ?x0), offset(?x0). inv(?x2, ?x1) :- inv(?x2, ?x0), buildWall_p(?x0, ?x1,?p). inv(?x2, ?x1) :- fetch(?x2, ?x0), putOn(?x0, ?x1), cont(?x1). iterate(?p) :- buildWall_p(d1,d2,?p).

where any variable with a ? before is a universal variable and the variable with a ! before is an existential variable, d1 and d2 are constants.

Querying buildWallp we get the following answers: ?x0 -> d11, ?x1 -> d12, ?p -> :null1_30 ?x0 -> d3, ?x1 -> d6, ?p -> :null1_31 ?x0 -> d1, ?x1 -> d2, ?p -> :null1_32 ?x0 -> d1, ?x1 -> d6, ?p -> :null1_3_3

which means that we have an idb buildWallp(d1,d2,:null1_3_2), and that means that the rule with iterate(?p) in the head should fire, but that is not the case as if we query iterate(?p) we don't get an answer.