diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/theory/theory_engine.h | |
parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 8 |
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; } |