diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-07-20 19:46:21 +0200 |
commit | f62d9456b41bf17df1d339e46776c9213cb3705a (patch) | |
tree | 01d3448b3c9fe89ead56c72b18f8516292092e13 /src/theory/quantifiers_engine.h | |
parent | 7943953741c67d8246f983e193d26812d959b4cd (diff) |
Squashed merge of SygusComp 2015 branch.
Diffstat (limited to 'src/theory/quantifiers_engine.h')
-rw-r--r-- | src/theory/quantifiers_engine.h | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 3040a35c7..54f63bfe0 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -93,6 +93,7 @@ namespace quantifiers { class CegInstantiation; class LtePartialInst; class AlphaEquivalence; + class FunDefEngine; }/* CVC4::theory::quantifiers */ namespace inst { @@ -142,6 +143,8 @@ private: quantifiers::CegInstantiation * d_ceg_inst; /** lte partial instantiation */ quantifiers::LtePartialInst * d_lte_part_inst; + /** function definitions engine */ + quantifiers::FunDefEngine * d_fun_def_engine; public: //effort levels enum { QEFFORT_CONFLICT, @@ -228,6 +231,8 @@ public: //modules 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; } private: /** owner of quantified formulas */ std::map< Node, QuantifiersModule * > d_owner; |