Disjunctive Invariants

[danbryce]

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.

[soonhokong]

Hi @danbryce,

I'm sorry that I couldn't find time to process your pull-request. I'll do it soon.

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'm not sure that you've noticed this, but I'm actually working on a new implementation of dReal. The repository is at https://github.com/dreal/dreal3. I believe that in the new version, it's easier to understand and extend the codebase. I started this version almost from scratch, I mean from OpenSMT2 codebase. Please understand that I couldn't port your contributions to dReal to this version yet. When things are more stable, I'll ask you to do that.

Here are some main changes:

• We have our own datastructures -- box, constraint, contractors, etc.
• We've replaced Realpaver with the new constraint solver IBEX that we discussed last summer.
• We control the main ICP loop which we asked Realpaver to do.
• In design, it's easier to wrap a constraint solver into a pruning operator. We plan to add more, for example, SpaceEx and Flow* for ODE solving.

In terms of progress in ODE solving, I started migrating the CAPD pruning operators to this version but couldn't finish it yet. There are some steps for that:

• CAPD forward full pruning is already there.
• CAPD backward full pruning is not there yet. But it only requires copy-paste. Well.. I actually want to refactor the forward one, extract the core CAPD routines, and use them to implement both of forward and backward pruning operators.
• The invariant checking part is missing for now. It's not difficult to add the previous invariant checking which only checks a conjunction of simple inequalities. I don't think it's difficult either to extend it and support a conjunction/disjunction of simple ineqs. The hard part is to support a general logic formula as an invariant, which requires recursive calls to dReal.

I'll finish some refactoring and implementing full CAPD backward pruning + the previous invariant checking. Please subscribe dreal/dreal3#21. After that, I can extend it to support disjunction or ask you to do it. What do you think?

[soonhokong]

Of course, if you're in hurry, please feel free to extend the current version of dReal.

[danbryce]

Thanks. I knew you were doing this, but didn't know where to look.