diff options
| -rw-r--r-- | src/smt/set_defaults.cpp | 4 | ||||
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 13 | ||||
| -rw-r--r-- | src/theory/sep/theory_sep.cpp | 16 |
3 files changed, 20 insertions, 13 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 6f00998d2..236137bb2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -911,6 +911,10 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) { options::preSkolemQuant.set(true); } + // must have separation logic + logic = logic.getUnlockedCopy(); + logic.enableTheory(THEORY_SEP); + logic.lock(); } // now, have determined whether finite model find is on/off diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 59082b55f..3bfc4ac61 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -498,19 +498,6 @@ void QuantifiersEngine::ppNotifyAssertions( quantifiers::QuantAttributes::setInstantiationLevelAttr(a, 0); } } - if (d_qepr != NULL) - { - for (const Node& a : assertions) - { - d_qepr->registerAssertion(a); - } - // must handle sources of other new constants e.g. separation logic - // FIXME (as part of project 3) : cleanup - sep::TheorySep* theory_sep = - static_cast<sep::TheorySep*>(getTheoryEngine()->theoryOf(THEORY_SEP)); - theory_sep->initializeBounds(); - d_qepr->finishInit(); - } if (options::sygus()) { quantifiers::SynthEngine* sye = d_private->d_synth_e.get(); 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 |