diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-01 14:12:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-01 14:12:08 -0500 |
| commit | cd91768f52349bd14399e49b2fbc4e59bb659ded (patch) | |
| tree | 5f87c700390b04072700d7d870531a4111a13d25 /src/prop | |
| parent | 4c2c2de951c52ef48704dbffe7ec5848917f1398 (diff) | |
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.
Diffstat (limited to 'src/prop')
0 files changed, 0 insertions, 0 deletions