diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-09-08 11:45:38 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-09-08 11:45:38 -0500 |
commit | be3543ef7e01eb32aab3161fa2778953fabc988d (patch) | |
tree | d821c034199aad91fddaa27d9baf3792c91463a6 /src/theory/sep | |
parent | 3f150596fe2186aea1c40b3210e8a0d59dc1ba94 (diff) |
Eliminate a custom use of TheorySep in quantifiers engine for EPR (#5039)
This moves the initialization of the connection between separation logic and EPR to the separation logic theory, which is a more logical place for this. This eliminates a backwards reference to theory engine from quantifiers engine.
Diffstat (limited to 'src/theory/sep')
-rw-r--r-- | src/theory/sep/theory_sep.cpp | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index dc8ec9203..c9b6a9d89 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -1001,6 +1001,22 @@ void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) { d_loc_to_data_type[d_type_ref] = d_type_data; } } + // initialize the EPR utility + QuantifiersEngine* qe = getQuantifiersEngine(); + if (qe != nullptr) + { + quantifiers::QuantEPR* qepr = qe->getQuantEPR(); + if (qepr != nullptr) + { + for (const Node& a : assertions) + { + qepr->registerAssertion(a); + } + // must handle sources of other new constants e.g. separation logic + initializeBounds(); + qepr->finishInit(); + } + } } //return cardinality |