diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-11 17:08:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-11 17:08:07 -0500 |
| commit | 81cd457d729f845f1b76d457359a0ae9963c0f88 (patch) | |
| tree | c521ed630f3514b26bfbce227a1e1e41b8dac01a /src/theory/quantifiers_engine.h | |
| parent | 3e6de62d11dcb3cf266f58e68def2f2c2ce728c3 (diff) | |
Infrastructure for instantiation rewriter (#3262)
Diffstat (limited to 'src/theory/quantifiers_engine.h')
| -rw-r--r-- | src/theory/quantifiers_engine.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 1f8c13f7b..458ba07bc 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -24,7 +24,6 @@ #include "context/cdlist.h" #include "expr/attribute.h" #include "expr/term_canonize.h" -#include "theory/quantifiers/cegqi/inst_strategy_cegqi.h" #include "theory/quantifiers/ematching/trigger.h" #include "theory/quantifiers/equality_infer.h" #include "theory/quantifiers/equality_query.h" @@ -119,8 +118,6 @@ public: quantifiers::BoundedIntegers* getBoundedIntegers() const; /** ceg instantiation */ quantifiers::SynthEngine* getSynthEngine() const; - /** get inst strategy cbqi */ - quantifiers::InstStrategyCegqi* getInstStrategyCegqi() const; //---------------------- end modules private: /** |