diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2018-04-25 11:54:23 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-25 11:54:23 -0700 |
| commit | a2df47ad560843301ba98c79f1f0fe5d6091c0ae (patch) | |
| tree | 8c2683dab7f7f856aebdf05fe439481358fd5f98 /src/theory/theory_engine.h | |
| parent | 6445c3dbf5fed9fa32426f041061234b5ac407f7 (diff) | |
Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 04e3c5697..80853bb6f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -35,7 +35,6 @@ #include "smt/command.h" #include "smt_util/lemma_channels.h" #include "theory/atom_requests.h" -#include "theory/bv/bv_to_bool.h" #include "theory/interrupted.h" #include "theory/rewriter.h" #include "theory/shared_terms_database.h" @@ -851,11 +850,8 @@ private: UnconstrainedSimplifier* d_unconstrainedSimp; /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ - theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: void staticInitializeBVOptions(const std::vector<Node>& assertions); - void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); - void ppBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); bool ppBvAbstraction(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); void mkAckermanizationAssertions(std::vector<Node>& assertions); |