soonhokong
commented
9 years ago 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 https://github.com/dreal/dreal3/issues/21. After that, I can extend it to support disjunction or ask you to do it. What do you think?
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.