diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-24 15:54:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-24 17:54:31 -0300 |
| commit | 9a4deadddfd3d4489ba15f65f0e3dab72b2fcccc (patch) | |
| tree | c86ed005257bc1d951bfa30141b8dcde1039324f /src/theory/quantifiers/ematching/ho_trigger.cpp | |
| parent | ba34ba8fc1edc62702f6b6ffcd247d13ba7f8271 (diff) | |
Split higher-order term database (#7045)
This splits higher-order term database as a derived class of term database, thus separating higher-order specific things out of our core term database.
This eliminates many of the references to the deprecated option uf-ho.
This is work towards eliminating that option.
Diffstat (limited to 'src/theory/quantifiers/ematching/ho_trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/ematching/ho_trigger.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 73a894081..cb4bac254 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -13,14 +13,15 @@ * Implementation of higher-order trigger class. */ +#include "theory/quantifiers/ematching/ho_trigger.h" + #include <stack> -#include "theory/quantifiers/ematching/ho_trigger.h" +#include "theory/quantifiers/ho_term_database.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_inference_manager.h" #include "theory/quantifiers/quantifiers_registry.h" #include "theory/quantifiers/quantifiers_state.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_registry.h" #include "theory/quantifiers/term_util.h" #include "theory/uf/theory_uf_rewriter.h" @@ -503,7 +504,7 @@ uint64_t HigherOrderTrigger::addHoTypeMatchPredicateLemmas() // if a variable of this type occurs in this trigger if (d_ho_var_types.find(stn) != d_ho_var_types.end()) { - Node u = tdb->getHoTypeMatchPredicate(tn); + Node u = HoTermDb::getHoTypeMatchPredicate(tn); Node au = nm->mkNode(kind::APPLY_UF, u, f); if (d_qim.addPendingLemma(au, InferenceId::QUANTIFIERS_HO_MATCH_PRED)) |