diff options
Diffstat (limited to 'src/theory/theory_engine.h')
| -rw-r--r-- | src/theory/theory_engine.h | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 92469aa31..8f292e008 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -39,6 +39,7 @@ #include "util/statistics_registry.h" #include "util/cvc4_assert.h" #include "util/sort_inference.h" +#include "theory/quantifiers/quant_conflict_find.h" #include "theory/uf/equality_engine.h" #include "theory/bv/bv_to_bool.h" #include "theory/atom_requests.h" @@ -778,10 +779,10 @@ private: UnconstrainedSimplifier* d_unconstrainedSimp; /** For preprocessing pass lifting bit-vectors of size 1 to booleans */ - theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; + theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor; public: - void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); + void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions); Node ppSimpITE(TNode assertion); /** Returns false if an assertion simplified to false. */ bool donePPSimpITE(std::vector<Node>& assertions); @@ -790,6 +791,8 @@ public: SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; } + theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } + SortInference* getSortInference() { return &d_sortInfer; } private: std::map< std::string, std::vector< theory::Theory* > > d_attr_handle; |