diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-09 15:21:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-09 15:21:08 -0500 |
| commit | 68df2d8d6c9218fe6a9bf01d22c7dfe2abdf684d (patch) | |
| tree | 672f3d0953e7de0f50ccbaa173afc360e4b19bfe /test | |
| parent | c64575b7c65a9822955efbf7711736068394899a (diff) | |
Associate all lemmas in non-linear arithmetic with an inference identifier (#4712)
This marks all lemmas in non-linear arithmetic with an identifier, which indicates informally the kind of justification that was used for them. The main motivation for this is for debugging the behavior of the non-linear solver.
The number of inferences can then be seen with --stats:
nl::inferences, [(SPLIT_ZERO : 19), (SIGN : 4), (COMPARISON : 29)]
The same design was used in strings and has been quite helpful.
This also adds a few high level stats to the new statistics class for non-linear.
Diffstat (limited to 'test')
0 files changed, 0 insertions, 0 deletions