Apologies: I couldn't find an existing issue for this.
We have discussed the need for disjunctive invariants before, and I am at the point where it would be nice to have. I realize that it involves some re-arhcitecting of the nra_solver, but just wanted to see the status, and if its on anyone's todo list currently. I may have the availability, but don't want to jump into anything w/o discussing a bit.
I need to state constraints of the form:
(not (exists_t 0 [0 time_0] (and (<= x_0_t 10) (<= 0 x_0_t))))
0 <= x <= 10 is the condition of a PDDL+ process, and I need to check that it is not satisfied over a time interval.
Converting the constraint gives:
(forall_t 0 [0 time_0] (or (> x_0_t 10) (> 0 x_0_t)))
I am open to suggestions, but the most straight-forward solution is to directly handle disjunction.
Apologies: I couldn't find an existing issue for this.
We have discussed the need for disjunctive invariants before, and I am at the point where it would be nice to have. I realize that it involves some re-arhcitecting of the nra_solver, but just wanted to see the status, and if its on anyone's todo list currently. I may have the availability, but don't want to jump into anything w/o discussing a bit.
I need to state constraints of the form:
(not (exists_t 0 [0 time_0] (and (<= x_0_t 10) (<= 0 x_0_t))))
0 <= x <= 10 is the condition of a PDDL+ process, and I need to check that it is not satisfied over a time interval.
Converting the constraint gives:
(forall_t 0 [0 time_0] (or (> x_0_t 10) (> 0 x_0_t)))
I am open to suggestions, but the most straight-forward solution is to directly handle disjunction.