diff options
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 66 | ||||
| -rw-r--r-- | src/theory/uf/theory_uf.h | 6 |
2 files changed, 32 insertions, 40 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 1afb8cc31..36b05b145 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -148,56 +148,54 @@ void TheoryUF::postCheck(Effort level) } } -bool TheoryUF::preNotifyFact( - TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) +void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) { + if (d_state.isInConflict()) + { + return; + } if (d_thss != nullptr) { bool isDecision = d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact); d_thss->assertNode(fact, isDecision); - if (d_state.isInConflict()) - { - return true; - } } - if (atom.getKind() == kind::CARDINALITY_CONSTRAINT - || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT) + switch (atom.getKind()) { - if (d_thss == nullptr) + case kind::EQUAL: { - if (!getLogicInfo().hasCardinalityConstraints()) + if (options::ufHo() && options::ufHoExt()) { - std::stringstream ss; - ss << "Cardinality constraint " << atom - << " was asserted, but the logic does not allow it." << std::endl; - ss << "Try using a logic containing \"UFC\"." << std::endl; - throw Exception(ss.str()); - } - else - { - // support for cardinality constraints is not enabled, set incomplete - d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED); + if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction()) + { + // apply extensionality eagerly using the ho extension + d_ho->applyExtensionality(fact); + } } } - // don't need to assert cardinality constraints if not producing models - return !options::produceModels(); - } - return false; -} - -void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) -{ - if (!d_state.isInConflict() && atom.getKind() == kind::EQUAL) - { - if (options::ufHo() && options::ufHoExt()) + break; + case kind::CARDINALITY_CONSTRAINT: + case kind::COMBINED_CARDINALITY_CONSTRAINT: { - if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction()) + if (d_thss == nullptr) { - // apply extensionality eagerly using the ho extension - d_ho->applyExtensionality(fact); + if (!getLogicInfo().hasCardinalityConstraints()) + { + std::stringstream ss; + ss << "Cardinality constraint " << atom + << " was asserted, but the logic does not allow it." << std::endl; + ss << "Try using a logic containing \"UFC\"." << std::endl; + throw Exception(ss.str()); + } + else + { + // support for cardinality constraints is not enabled, set incomplete + d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED); + } } } + break; + default: break; } } //--------------------------------- end standard check diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index c811e08e8..c953cfe5c 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -128,12 +128,6 @@ private: bool needsCheckLastEffort() override; /** Post-check, called after the fact queue of the theory is processed. */ void postCheck(Effort level) override; - /** Pre-notify fact, return true if processed. */ - bool preNotifyFact(TNode atom, - bool pol, - TNode fact, - bool isPrereg, - bool isInternal) override; /** Notify fact */ void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; //--------------------------------- end standard check |