From b7bbe9a3bc30f41d1775a187ccc732aaeb41eaa1 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 11 Sep 2020 16:01:11 -0500 Subject: [PATCH] Move finite model minimization to UF last call effort (#5050) This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints). Fixes #4850. --- src/theory/quantifiers/fmf/model_engine.cpp | 33 +++++-------------- src/theory/theory_state.cpp | 2 ++ src/theory/theory_state.h | 5 +++ src/theory/uf/cardinality_extension.cpp | 26 ++++++++------- src/theory/uf/cardinality_extension.h | 13 +++++--- src/theory/uf/theory_uf.cpp | 8 ++++- src/theory/uf/theory_uf.h | 6 ++-- src/theory/valuation.h | 3 +- .../regress0/fmf/issue4850-force-card.smt2 | 6 ++++ 9 files changed, 57 insertions(+), 45 deletions(-) create mode 100644 test/regress/regress0/fmf/issue4850-force-card.smt2 diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 879bfd1c1..3cf90069f 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -24,9 +24,7 @@ #include "theory/quantifiers/term_util.h" #include "theory/quantifiers_engine.h" #include "theory/theory_engine.h" -#include "theory/uf/cardinality_extension.h" #include "theory/uf/equality_engine.h" -#include "theory/uf/theory_uf.h" using namespace std; using namespace CVC4; @@ -79,7 +77,6 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) if( doCheck ){ Assert(!d_quantEngine->inConflict()); int addedLemmas = 0; - FirstOrderModel* fm = d_quantEngine->getModel(); //the following will test that the model satisfies all asserted universal quantifiers by // (model-based) exhaustive instantiation. @@ -88,28 +85,16 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) Trace("model-engine") << "---Model Engine Round---" << std::endl; clSet = double(clock())/double(CLOCKS_PER_SEC); } - - Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; - // Let the cardinality extension verify that the model is minimal. - // This will if there are terms in the model that the cardinality extension - // was not notified of. - uf::CardinalityExtension* ufss = - static_cast( - d_quantEngine->getTheoryEngine()->theoryOf(THEORY_UF)) - ->getCardinalityExtension(); - if( !ufss || ufss->debugModel( fm ) ){ - Trace("model-engine-debug") << "Check model..." << std::endl; - d_incomplete_check = false; - //print debug - if( Trace.isOn("fmf-model-complete") ){ - Trace("fmf-model-complete") << std::endl; - debugPrint("fmf-model-complete"); - } - //successfully built an acceptable model, now check it - addedLemmas += checkModel(); - }else{ - addedLemmas++; + Trace("model-engine-debug") << "Check model..." << std::endl; + d_incomplete_check = false; + // print debug + if (Trace.isOn("fmf-model-complete")) + { + Trace("fmf-model-complete") << std::endl; + debugPrint("fmf-model-complete"); } + // successfully built an acceptable model, now check it + addedLemmas += checkModel(); if( Trace.isOn("model-engine") ){ double clSet2 = double(clock())/double(CLOCKS_PER_SEC); diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index f22a652c0..d5f9f4d0b 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -130,5 +130,7 @@ bool TheoryState::isSatLiteral(TNode lit) const return d_valuation.isSatLiteral(lit); } +TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); } + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 4ae381e78..633937991 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -74,6 +74,11 @@ class TheoryState /** Returns true if lit is a SAT literal. */ virtual bool isSatLiteral(TNode lit) const; + /** + * Returns pointer to model. This model is only valid during last call effort + * check. + */ + TheoryModel* getModel(); protected: /** Pointer to the SAT context object used by the theory. */ diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index b35efc23a..4f9483667 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1182,7 +1182,9 @@ void SortModel::debugPrint( const char* c ){ } } -bool SortModel::debugModel( TheoryModel* m ){ +bool SortModel::checkLastCall() +{ + TheoryModel* m = d_state.getModel(); if( Trace.isOn("uf-ss-warn") ){ std::vector< Node > eqcs; eq::EqClassesIterator eqcs_i = @@ -1572,6 +1574,18 @@ bool CardinalityExtension::areDisequal(Node a, Node b) /** check */ void CardinalityExtension::check(Theory::Effort level) { + if (level == Theory::EFFORT_LAST_CALL) + { + // if last call, call last call check for each sort + for (std::pair& r : d_rep_model) + { + if (!r.second->checkLastCall()) + { + break; + } + } + return; + } if (!d_state.isInConflict()) { if (options::ufssMode() == options::UfssMode::FULL) @@ -1750,16 +1764,6 @@ void CardinalityExtension::debugPrint(const char* c) } } -bool CardinalityExtension::debugModel(TheoryModel* m) -{ - for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - if( !it->second->debugModel( m ) ){ - return false; - } - } - return true; -} - /** initialize */ void CardinalityExtension::initializeCombinedCardinality() { diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index 4c2707c17..d75b6d62d 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -327,8 +327,15 @@ class CardinalityExtension int getMaximumNegativeCardinality() { return d_maxNegCard.get(); } //print debug void debugPrint( const char* c ); - /** debug a model */ - bool debugModel( TheoryModel* m ); + /** + * Check at last call effort. This will verify that the model is minimal. + * This return lemmas if there are terms in the model that the cardinality + * extension was not notified of. + * + * @return false if current model is not minimal. In this case, lemmas are + * sent on the output channel of the UF theory. + */ + bool checkLastCall(); /** get number of regions (for debugging) */ int getNumRegions(); @@ -387,8 +394,6 @@ class CardinalityExtension std::string identify() const { return std::string("CardinalityExtension"); } //print debug void debugPrint( const char* c ); - /** debug a model */ - bool debugModel( TheoryModel* m ); /** get cardinality for node */ int getCardinality( Node n ); /** get cardinality for type */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0a48d4c71..18ab70d46 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -125,6 +125,12 @@ static Node mkAnd(const std::vector& conjunctions) { //--------------------------------- standard check +bool TheoryUF::needsCheckLastEffort() +{ + // last call effort needed if using finite model finding + return d_thss != nullptr; +} + void TheoryUF::postCheck(Effort level) { if (d_state.isInConflict()) @@ -136,7 +142,7 @@ void TheoryUF::postCheck(Effort level) { d_thss->check(level); } - // check with the higher-order extension + // check with the higher-order extension at full effort if (!d_state.isInConflict() && fullEffort(level)) { if (options::ufHo()) diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 4a8369483..86c1b62c8 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -158,6 +158,8 @@ private: //--------------------------------- end initialization //--------------------------------- standard check + /** Do we need a check call at last call effort? */ + 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. */ @@ -187,10 +189,6 @@ private: EqualityStatus getEqualityStatus(TNode a, TNode b) override; std::string identify() const override { return "THEORY_UF"; } - - /** get a pointer to the uf with cardinality */ - CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); } - private: /** Explain why this literal is true by building an explanation */ void explain(TNode literal, Node& exp); diff --git a/src/theory/valuation.h b/src/theory/valuation.h index dc12d030d..d7d711b65 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -107,7 +107,8 @@ public: Node getModelValue(TNode var); /** - * Returns pointer to model. + * Returns pointer to model. This model is only valid during last call effort + * check. */ TheoryModel* getModel(); diff --git a/test/regress/regress0/fmf/issue4850-force-card.smt2 b/test/regress/regress0/fmf/issue4850-force-card.smt2 new file mode 100644 index 000000000..5aa7fc894 --- /dev/null +++ b/test/regress/regress0/fmf/issue4850-force-card.smt2 @@ -0,0 +1,6 @@ +(set-logic UFC) +(set-info :status sat) +(declare-sort a 0) +(declare-fun b () a) +(assert (not (fmf.card b 1))) +(check-sat) -- 2.30.2