diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-23 14:13:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-23 14:13:38 -0500 |
commit | f3d010e07f30dd658d4532a43b3813654376162d (patch) | |
tree | 1080a71e07f906f6af5b5144c0a83207c40c1b2a /src/theory/quantifiers_engine.h | |
parent | 4f506ac50e43a71a92094a478deeaa2c2cd1df4a (diff) |
Remove unused code (#1700)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 3fb250d4a..e031bb64b 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -70,8 +70,6 @@ namespace quantifiers { class CegInstantiation; class LtePartialInst; class AlphaEquivalence; - class FunDefEngine; - class QuantEqualityEngine; class InstStrategyEnum; class InstStrategyCbqi; class InstStrategyCegqi; @@ -151,10 +149,6 @@ private: quantifiers::CegInstantiation * d_ceg_inst; /** lte partial instantiation */ quantifiers::LtePartialInst * d_lte_part_inst; - /** function definitions engine */ - quantifiers::FunDefEngine * d_fun_def_engine; - /** quantifiers equality engine */ - quantifiers::QuantEqualityEngine * d_uee; /** full saturation */ quantifiers::InstStrategyEnum* d_fs; /** counterexample-based quantifier instantiation */ @@ -251,10 +245,6 @@ public: quantifiers::CegInstantiation * getCegInstantiation() { return d_ceg_inst; } /** local theory ext partial inst */ quantifiers::LtePartialInst * getLtePartialInst() { return d_lte_part_inst; } - /** function definition engine */ - quantifiers::FunDefEngine * getFunDefEngine() { return d_fun_def_engine; } - /** quantifiers equality engine */ - quantifiers::QuantEqualityEngine * getQuantEqualityEngine() { return d_uee; } /** get full saturation */ quantifiers::InstStrategyEnum* getInstStrategyEnum() { return d_fs; } /** get inst strategy cbqi */ |