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/congruence_manager.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/congruence_manager.cpp')
| -rw-r--r-- | src/theory/arith/congruence_manager.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp index 96272f939..9e7202f1d 100644 --- a/src/theory/arith/congruence_manager.cpp +++ b/src/theory/arith/congruence_manager.cpp @@ -85,6 +85,7 @@ void ArithCongruenceManager::finishInit(eq::EqualityEngine* ee, d_ee->addFunctionKind(kind::EXPONENTIAL); d_ee->addFunctionKind(kind::SINE); d_ee->addFunctionKind(kind::IAND); + d_ee->addFunctionKind(kind::POW2); // have proof equality engine only if proofs are enabled Assert(isProofEnabled() == (pfee != nullptr)); d_pfee = pfee; |