Use inference manager for nl_solver (#5125)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Sat, 26 Sep 2020 17:11:13 +0000 (19:11 +0200)
committerGitHub <noreply@github.com>
Sat, 26 Sep 2020 17:11:13 +0000 (12:11 -0500)
commitb52dc978f2445c6765b806119d238ca81cb8fe90
tree30cd36ea1d3a864946a9f3869e2fdddfe0d3564e
parent1fe9c2efe36b126c70097b0f83db5654e0abcabe
Use inference manager for nl_solver (#5125)

This PR migrates the nl_solver part of the nonlinear extension to use the new inference manager as well.
It adds a new method clearWaitingLemmas to the inference manager and uses ArithLemma (though NlLemma exists) as we don't need the additional functionality of NlLemma.
src/theory/arith/inference_manager.cpp
src/theory/arith/inference_manager.h
src/theory/arith/nl/nl_solver.cpp
src/theory/arith/nl/nl_solver.h
src/theory/arith/nl/nonlinear_extension.cpp