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.

AmirHosein Sadeghimanesh

An SMT solver for non-linear real arithmetic inside maple

ivySCI AI Smartly Parses PDF, Answers Researchers' Questions, and Helps You Understand Papers in Seconds

Journal Info

Category	Quartile
MATHEMATICS, APPLIED	4