pstlab / oRatio

oRatio is an Integrated Logic and Constraint based solver
Apache License 2.0
6 stars 1 forks source link

Declaration order #20

Closed Raffarti closed 4 years ago

Raffarti commented 4 years ago
class Rover : StateVariable {
    real id;

    Rover(real id) :
        id(id) {}

    predicate Equipped() {false;}
}

Rover r0;
Rover r1 = new Rover(1.0);

fact e = new r1.Equipped();
goal t = new r0.Equipped();

No solution is found for this, unless r1 is initialized before declaring r0. When Rover is not a state varaible, a solution is always found, perhaps linked to #19.

riccardodebenedictis commented 4 years ago

This behaviour is, somehow, correct (as stated, in 'unfair terms', in the wiki)!

Statements are executed sequentially, so you are actually creating a variable (i.e., r0) with an empty domain (there is no instance yet of Rover when creating r0). The solver cannot assign a value to that variable and backtracks. Since the variable is created at root-level, it just returns false (i.e., unsolvable).

It is, in principle, possible to postpone the creation of existentially scoped variables (I know some languages, like JavaScript, allow this), but it probably makes parsing too much more complex..

So, the wrong behaviour was actually related to the fact that

when Rover is not a state varaible, a solution is always found

thanks, again!