summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers_engine.h
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-03-23 14:13:38 -0500
committerGitHub <noreply@github.com>2018-03-23 14:13:38 -0500
commitf3d010e07f30dd658d4532a43b3813654376162d (patch)
tree1080a71e07f906f6af5b5144c0a83207c40c1b2a /src/theory/quantifiers_engine.h
parent4f506ac50e43a71a92094a478deeaa2c2cd1df4a (diff)
Remove unused code (#1700)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r--src/theory/quantifiers_engine.h10
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback