Handle solution after returning SAT

kperun / SATPrakPDW

Interval Constraint Propagation strategy implementation for SMTRAT

MIT License

2 stars 0 forks source link

Handle solution after returning SAT #15

Closed Verdict7 closed 7 years ago

Verdict7 commented 7 years ago

The model created in checkCore is simply ignored after it was checked. It should probably be saved and updated according to the updateModel function.

kperun commented 7 years ago

@DavidWz implemented. Now in ICPPDWModel the mFoundModel variable stores an optional model, whenever such a model has been found in checkCore(). Whenever updateModel() is called and the satsolver() has the status SAT, this model is handed over as a satisfying assignment.