summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3273b3d19..7ce8345f7 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -97,7 +97,7 @@ namespace theory {
}/* CVC4::theory namespace */
class DecisionEngine;
-class RemoveITE;
+class RemoveTermFormulas;
class UnconstrainedSimplifier;
/**
@@ -439,7 +439,7 @@ class TheoryEngine {
/** Enusre that the given atoms are send to the given theory */
void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory);
- RemoveITE& d_iteRemover;
+ RemoveTermFormulas& d_tform_remover;
/** sort inference module */
SortInference d_sortInfer;
@@ -461,7 +461,7 @@ public:
/** Constructs a theory engine */
TheoryEngine(context::Context* context, context::UserContext* userContext,
- RemoveITE& iteRemover, const LogicInfo& logic,
+ RemoveTermFormulas& iteRemover, const LogicInfo& logic,
LemmaChannels* channels);
/** Destroys a theory engine */
@@ -850,7 +850,7 @@ public:
theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
- RemoveITE* getIteRemover() { return &d_iteRemover; }
+ RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; }
SortInference* getSortInference() { return &d_sortInfer; }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback