diff options
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index dd34ae16b..5506b0120 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -23,14 +23,15 @@ #include <memory> #include <set> #include <unordered_map> -#include <vector> #include <utility> +#include <vector> #include "base/check.h" #include "context/cdhashset.h" #include "expr/node.h" #include "options/options.h" #include "options/smt_options.h" +#include "options/theory_options.h" #include "prop/prop_engine.h" #include "smt/command.h" #include "smt_util/lemma_channels.h" @@ -864,10 +865,13 @@ public: * Forwards an entailment check according to the given theoryOfMode. * See theory.h for documentation on entailmentCheck(). */ - std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL); - -private: + std::pair<bool, Node> entailmentCheck( + options::TheoryOfMode mode, + TNode lit, + const theory::EntailmentCheckParameters* params = NULL, + theory::EntailmentCheckSideEffects* out = NULL); + private: /** Default visitor for pre-registration */ PreRegisterVisitor d_preRegistrationVisitor; |