diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-25 19:42:43 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-25 19:42:43 -0700 |
| commit | eefd31d2fe256bdee9a5c33105eced1a358bb378 (patch) | |
| tree | 5b8d52bdfc288557bf6456ca315ad2862ab4669b /src/theory/arith/nl/strategy.h | |
| parent | abd18eeb854047e13e38518c536afd16a1be448d (diff) | |
pow2 -- final changes (#6800)
This commit adds the remaining changes for a working and integrated `pow2` solver.
In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.
The next steps are new rewrites and and more lemma schemas.
Diffstat (limited to 'src/theory/arith/nl/strategy.h')
| -rw-r--r-- | src/theory/arith/nl/strategy.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h index ba0d3370e..e2fc6c1c6 100644 --- a/src/theory/arith/nl/strategy.h +++ b/src/theory/arith/nl/strategy.h @@ -44,7 +44,15 @@ enum class InferStep /** An initial IAND check */ IAND_INITIAL, + /** Initialize the POW2 solver */ + POW2_INIT, + /** A full POW2 check */ + POW2_FULL, + /** An initial POW2 check */ + POW2_INITIAL, + /** An ICP check */ + ICP, /** Initialize the NL solver */ |