We report on work-in-progress to create an SMT-solver inside Maple for non-linear real arithmetic (NRA). We give background information on the algorithm being implemented: cylindrical algebraic coverings as a theory solver in the lazy SMT paradigm. We then present some new work on the identification of minimal conflicting cores from the coverings.
Bibliographical note© ACM, 2022. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ACM Communications in Computer Algebra, vol. 56, no. 2, pp. 76-79.http://doi.acm.org/10.1145/3572867.3572880
- Computer Algebra
- Symbolic computation
- satisfiability modulo theories
- cylindrical algebraic coverings
- Set covering problem