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.cpp | |
| 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.cpp')
| -rw-r--r-- | src/theory/arith/nl/strategy.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp index ffe925830..f20cf4221 100644 --- a/src/theory/arith/nl/strategy.cpp +++ b/src/theory/arith/nl/strategy.cpp @@ -37,6 +37,9 @@ std::ostream& operator<<(std::ostream& os, InferStep step) case InferStep::IAND_INIT: return os << "IAND_INIT"; case InferStep::IAND_FULL: return os << "IAND_FULL"; case InferStep::IAND_INITIAL: return os << "IAND_INITIAL"; + case InferStep::POW2_INIT: return os << "POW2_INIT"; + case InferStep::POW2_FULL: return os << "POW2_FULL"; + case InferStep::POW2_INITIAL: return os << "POW2_INITIAL"; case InferStep::ICP: return os << "ICP"; case InferStep::NL_INIT: return os << "NL_INIT"; case InferStep::NL_MONOMIAL_INFER_BOUNDS: @@ -125,6 +128,8 @@ void Strategy::initializeStrategy() } one << InferStep::IAND_INIT; one << InferStep::IAND_INITIAL << InferStep::BREAK; + one << InferStep::POW2_INIT; + one << InferStep::POW2_INITIAL << InferStep::BREAK; if (options::nlExt() == options::NlExtMode::FULL || options::nlExt() == options::NlExtMode::LIGHT) { @@ -164,6 +169,7 @@ void Strategy::initializeStrategy() one << InferStep::BREAK; } one << InferStep::IAND_FULL << InferStep::BREAK; + one << InferStep::POW2_FULL << InferStep::BREAK; if (options::nlCad()) { one << InferStep::CAD_INIT; |