search

kperun / SATPrakPDW

Interval Constraint Propagation strategy implementation for SMTRAT
MIT License
2 stars 0 forks source link

No distinction between active and non-active variables #50

Closed kperun closed 7 years ago

kperun commented 7 years ago

Currently, we see all variables which have been extracted during the informCore() call as the variables of our current problem. However, when certain variables only occur in a subset of constraint which is currently not active, it does not make sense to check if the boundaries of these variables are fulfilled. Here, we probably should also store the current active variables.

DavidWz commented 7 years ago

There are always constraints of the form -1000 < x < 1000 so every variable is always active.