Improve integration of nonlinear arithmetic into the arithmetic theory. (#6956)
authorGereon Kremer <nafur42@gmail.com>
Thu, 26 Aug 2021 14:19:56 +0000 (07:19 -0700)
committerGitHub <noreply@github.com>
Thu, 26 Aug 2021 14:19:56 +0000 (14:19 +0000)
commitdaee9d4ec0c9e7c5054345c4156c4debe815e045
tree0592cd34886c85af2dcf7e962c6f8a68006f748b
parenta81064b538382670f25c87f138961f12def7880a
Improve integration of nonlinear arithmetic into the arithmetic theory. (#6956)

The nonlinear extension used to be called only during model construction, a rather atypical place which lead to a series of subtle issues. This PR moves it into the postCheck method. To do that, a few other changes are necessary, most notably collectAssertedTerms and collectTerms are moved back from the model manager into the theory class.
src/theory/arith/nl/nonlinear_extension.cpp
src/theory/arith/theory_arith.cpp
src/theory/arith/theory_arith.h
src/theory/arith/theory_arith_private.cpp
test/regress/regress2/bv_to_int_mask_array_1.smt2