diff options
| author | lianah <lianahady@gmail.com> | 2013-04-12 16:15:30 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
| commit | 6a86536bd25fc7ffa305f25990cf37b8c6566c52 (patch) | |
| tree | 197b931f8f391a21eebbf097fd0f4b5adeb53c09 /src/theory/theory_engine.h | |
| parent | e4f5359675972341858fe167f454ed5da4d8c115 (diff) | |
finished implementing bv to bool lifting and added --bv-to-bool option
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9abdaa034..324b952b0 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -45,6 +45,7 @@ #include "theory/ite_simplifier.h" #include "theory/unconstrained_simplifier.h" #include "theory/uf/equality_engine.h" +#include "theory/bv/bv_to_bool.h" namespace CVC4 { @@ -748,8 +749,11 @@ private: /** For preprocessing pass simplifying unconstrained expressions */ UnconstrainedSimplifier d_unconstrainedSimp; + /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ + theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: + Node ppBvToBool(TNode assertion); Node ppSimpITE(TNode assertion); void ppUnconstrainedSimp(std::vector<Node>& assertions); |