Use NlLemma utility for all lemmas in non-linear. (#4573)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 6 Jun 2020 17:25:50 +0000 (12:25 -0500)
committerGitHub <noreply@github.com>
Sat, 6 Jun 2020 17:25:50 +0000 (12:25 -0500)
commit79d0e47c14a9e8213d6c6e112835142cf2417943
treee6b4e0a20fbb5f8613180f85fa0ace45f6e35b04
parent2507dbb96587b8a1a23fb36d8e201e8ac77350de
Use NlLemma utility for all lemmas in non-linear. (#4573)

This makes it much easier to set custom properties of lemmas (e.g. preprocess) and also will allow proof tracking and debugging in the future.

This also enables a fix on the IAND branch related to preprocessing lemmas.
src/theory/arith/nl/nl_lemma_utils.cpp
src/theory/arith/nl/nl_lemma_utils.h
src/theory/arith/nl/nl_model.cpp
src/theory/arith/nl/nl_model.h
src/theory/arith/nl/nl_solver.cpp
src/theory/arith/nl/nl_solver.h
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/nl/nonlinear_extension.h
src/theory/arith/nl/transcendental_solver.cpp
src/theory/arith/nl/transcendental_solver.h