Update theory of arithmetic to standard check (#5178)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 1 Oct 2020 19:12:08 +0000 (14:12 -0500)
committerGitHub <noreply@github.com>
Thu, 1 Oct 2020 19:12:08 +0000 (14:12 -0500)
commitcd91768f52349bd14399e49b2fbc4e59bb659ded
tree5f87c700390b04072700d7d870531a4111a13d25
parent4c2c2de951c52ef48704dbffe7ec5848917f1398
Update theory of arithmetic to standard check (#5178)

This updates the theory of arithmetic to use the standard check callbacks (preCheck, postCheck, preNotifyFact, notifyFact). It also refactors some use of the non-linear solver which will solely live in TheoryArith.

The longer term goal is to have TheoryArithPrivate be responsible for linear arithmetic solving only, and to be treated as a black box. Eventually, the non-linear solver will be removed from this class.

This PR is required for several things, including refactoring of preprocessing and expand definitions for arithmetic (div/mod will not be eliminated eagerly). It is also required for fixing issues related to div/mod appearing in instantiations.

This is the last class to have a custom check method. Followup PR will make Theory::check non-virtual.
src/theory/arith/nl/nl_solver.h
src/theory/arith/nl/nonlinear_extension.h
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
src/theory/arith/theory_arith_private.h