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/nonlinear_extension.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/nonlinear_extension.h')
-rw-r--r-- | src/theory/arith/nl/nonlinear_extension.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 4e029be7c..aae19df6e 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -33,6 +33,7 @@ #include "theory/arith/nl/iand_solver.h" #include "theory/arith/nl/icp/icp_solver.h" #include "theory/arith/nl/nl_model.h" +#include "theory/arith/nl/pow2_solver.h" #include "theory/arith/nl/stats.h" #include "theory/arith/nl/strategy.h" #include "theory/arith/nl/transcendental/transcendental_solver.h" @@ -277,6 +278,13 @@ class NonlinearExtension */ IAndSolver d_iandSlv; + /** The pow2 solver + * + * This is the subsolver responsible for running the procedure for + * constraints involving powers of 2. + */ + Pow2Solver d_pow2Slv; + /** The strategy for the nonlinear extension. */ Strategy d_strategy; |