This PR implements the first versions of MaxSMT solvers. It supports PMRes core-based algorithm implemented in z3 solver. Implementation is based on the article. Also this solution implements PDMRes solver implemented in z3.
Current solution is in progress. MaxSMT solvers do not provide subotimal solving yet.
Description
This PR implements the first versions of MaxSMT solvers. It supports PMRes core-based algorithm implemented in z3 solver. Implementation is based on the article. Also this solution implements PDMRes solver implemented in z3.
Current solution is in progress. MaxSMT solvers do not provide subotimal solving yet.