From: Andrew Reynolds Date: Fri, 6 Mar 2020 23:01:45 +0000 (-0600) Subject: Minor refactor for theory of sets (#3924) X-Git-Tag: cvc5-1.0.0~3552 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76c1710e99f2e9ca2109762394eaefcbc4a5557c;p=cvc5.git Minor refactor for theory of sets (#3924) Flattens a block of code and refactors the main check loop, will make it easier to incorporate new extensions. It also avoids a needless call to check() for Relations when there are no relations constraints. --- diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 866c80863..b949be76c 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -373,6 +373,8 @@ void TheorySetsPrivate::fullEffortCheck() Trace("sets") << "----- Full effort check ------" << std::endl; do { + Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed()); + Trace("sets") << "...iterate full effort check..." << std::endl; fullEffortReset(); @@ -476,71 +478,88 @@ void TheorySetsPrivate::fullEffortCheck() // We may have sent lemmas while registering the terms in the loop above, // e.g. the cardinality solver. - if (!d_im.hasProcessed()) + if (d_im.hasProcessed()) { - if (Trace.isOn("sets-mem")) + continue; + } + if (Trace.isOn("sets-mem")) + { + const std::vector& sec = d_state.getSetsEqClasses(); + for (const Node& s : sec) { - const std::vector& sec = d_state.getSetsEqClasses(); - for (const Node& s : sec) + Trace("sets-mem") << "Eqc " << s << " : "; + const std::map& smem = d_state.getMembers(s); + if (!smem.empty()) { - Trace("sets-mem") << "Eqc " << s << " : "; - const std::map& smem = d_state.getMembers(s); - if (!smem.empty()) - { - Trace("sets-mem") << "Memberships : "; - for (const std::pair& it2 : smem) - { - Trace("sets-mem") << it2.first << " "; - } - } - Node ss = d_state.getSingletonEqClass(s); - if (!ss.isNull()) + Trace("sets-mem") << "Memberships : "; + for (const std::pair& it2 : smem) { - Trace("sets-mem") << " : Singleton : " << ss; + Trace("sets-mem") << it2.first << " "; } - Trace("sets-mem") << std::endl; } - } - checkSubtypes(); - d_im.flushPendingLemmas(true); - if (!d_im.hasProcessed()) - { - checkDownwardsClosure(); - if (options::setsInferAsLemmas()) + Node ss = d_state.getSingletonEqClass(s); + if (!ss.isNull()) { - d_im.flushPendingLemmas(); - } - if (!d_im.hasProcessed()) - { - checkUpwardsClosure(); - d_im.flushPendingLemmas(); - if (!d_im.hasProcessed()) - { - checkDisequalities(); - d_im.flushPendingLemmas(); - if (!d_im.hasProcessed()) - { - checkReduceComprehensions(); - d_im.flushPendingLemmas(); - - if (!d_im.hasProcessed() && d_card_enabled) - { - // call the check method of the cardinality solver - d_cardSolver->check(); - } - } - } + Trace("sets-mem") << " : Singleton : " << ss; } + Trace("sets-mem") << std::endl; + } + } + // check subtypes + checkSubtypes(); + d_im.flushPendingLemmas(true); + if (d_im.hasProcessed()) + { + continue; + } + // check downwards closure + checkDownwardsClosure(); + if (options::setsInferAsLemmas()) + { + d_im.flushPendingLemmas(); + } + if (d_im.hasProcessed()) + { + continue; + } + // check upwards closure + checkUpwardsClosure(); + d_im.flushPendingLemmas(); + if (d_im.hasProcessed()) + { + continue; + } + // check disequalities + checkDisequalities(); + d_im.flushPendingLemmas(); + if (d_im.hasProcessed()) + { + continue; + } + // check reduce comprehensions + checkReduceComprehensions(); + d_im.flushPendingLemmas(); + if (d_im.hasProcessed()) + { + continue; + } + if (d_card_enabled) + { + // call the check method of the cardinality solver + d_cardSolver->check(); + if (d_im.hasProcessed()) + { + continue; } } - if (!d_im.hasProcessed()) + if (d_rels_enabled) { - // invoke relations solver + // call the check method of the relations solver d_rels->check(Theory::EFFORT_FULL); } - Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed()); } while (!d_im.hasSentLemma() && !d_state.isInConflict() && d_im.hasAddedFact()); + Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed()); Trace("sets") << "----- End full effort check, conflict=" << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma() << std::endl;