3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-12 02:04:43 +00:00
Commit graph

1 commit

Author SHA1 Message Date
Jakob Rath
f83705bf9f
Polysat: first pass at forbidden intervals (not yet fully integrated into solver) (#5227)
* Add interval class

* Take dependency as const reference

* Compute forbidden intervals for ule-constraints

* Add class for evaluated interval

* We need the evaluated bounds as well

* Don't add constraint to cjust multiple times (hack, to be improved later)

* typo

* More interval helpers

* Add constraint::ult factory function

* Fix forbidden interval condition

* Add solver::has_viable

* Add conflict explanation using forbidden intervals (not yet fully integrated into solver)
2021-04-29 10:12:54 -07:00