search

kperun / SATPrakPDW

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

Add support for iterative calls to the backend #57

Closed DavidWz closed 7 years ago

DavidWz commented 7 years ago

After issue #56 is resolved, we need to handle the infeasable subset returned by the backend. To this end, create a method handleBackendUnsat(...)to ICPTree with parameters containing the conflict reasons (maybe mInfeasableSubset?, but from the backend). During the handleBackendUnsat method, initialize mConflictingConstraints and mConflictingVariables, then call handleUnsat as usual.

kperun commented 7 years ago

@DavidWz in order to retrieve the infeasible set from the backends, take a look at Module.cpp (lines 644-657). There, this behavior is already implemented and illustrates the overall procedure quite good.

DavidWz commented 7 years ago

@kperun Thanks, I had to copy that code and tweak it a little bit so that we don't use origins (that's where the segfault came from). Backend call is fully implemented now.