From 571712dbd11b42ef4586c6adff397bae8ee35397 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Sep 2018 11:40:16 -0500 Subject: [PATCH] Decision strategy: incorporate UF with cardinality constraints (#2476) --- src/theory/uf/kinds | 2 +- src/theory/uf/theory_uf.cpp | 16 +- src/theory/uf/theory_uf.h | 1 - src/theory/uf/theory_uf_strong_solver.cpp | 397 ++++++++-------------- src/theory/uf/theory_uf_strong_solver.h | 69 +++- 5 files changed, 205 insertions(+), 280 deletions(-) diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 500295a0c..109e6d0a1 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -8,7 +8,7 @@ theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" typechecker "theory/uf/theory_uf_type_rules.h" properties stable-infinite parametric -properties check propagate ppStaticLearn presolve getNextDecisionRequest +properties check propagate ppStaticLearn presolve rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; first parameter is the function, remaining ones are parameters to that function" diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 653b89d7b..3e9e2354d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -79,8 +79,12 @@ void TheoryUF::finishInit() { TheoryModel* tm = d_valuation.getModel(); Assert(tm != nullptr); tm->setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT); - // initialize the strong solver - if (options::finiteModelFind() && options::ufssMode()!=UF_SS_NONE) { + // Initialize the cardinality constraints solver if the logic includes UF, + // finite model finding is enabled, and it is not disabled by + // options::ufssMode(). + if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind() + && options::ufssMode() != UF_SS_NONE) + { d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this); } } @@ -296,14 +300,6 @@ void TheoryUF::propagate(Effort effort) { //} } -Node TheoryUF::getNextDecisionRequest( unsigned& priority ){ - if (d_thss != NULL && !d_conflict) { - return d_thss->getNextDecisionRequest( priority ); - }else{ - return Node::null(); - } -} - void TheoryUF::explain(TNode literal, std::vector& assumptions, eq::EqProof* pf) { // Do the work bool polarity = literal.getKind() != kind::NOT; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 9221f64ac..2fd23a657 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -301,7 +301,6 @@ private: void computeCareGraph() override; void propagate(Effort effort) override; - Node getNextDecisionRequest(unsigned& priority) override; EqualityStatus getEqualityStatus(TNode a, TNode b) override; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 4efa6c2ce..a19298b64 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -441,32 +441,51 @@ void Region::debugPrint( const char* c, bool incClique ) { } } -SortModel::SortModel( Node n, - context::Context* c, - context::UserContext* u, - StrongSolverTheoryUF* thss ) - : d_type( n.getType() ) - , d_thss( thss ) - , d_regions_index( c, 0 ) - , d_regions_map( c ) - , d_split_score( c ) - , d_disequalities_index( c, 0 ) - , d_reps( c, 0 ) - , d_conflict( c, false ) - , d_cardinality( c, 1 ) - , d_aloc_cardinality( u, 0 ) - , d_hasCard( c, false ) - , d_maxNegCard( c, 0 ) - , d_initialized( u, false ) - , d_lemma_cache( u ) +SortModel::CardinalityDecisionStrategy::CardinalityDecisionStrategy( + Node t, context::Context* satContext, Valuation valuation) + : DecisionStrategyFmf(satContext, valuation), d_cardinality_term(t) +{ +} +Node SortModel::CardinalityDecisionStrategy::mkLiteral(unsigned i) +{ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode( + CARDINALITY_CONSTRAINT, d_cardinality_term, nm->mkConst(Rational(i + 1))); +} +std::string SortModel::CardinalityDecisionStrategy::identify() const +{ + return std::string("uf_card"); +} + +SortModel::SortModel(Node n, + context::Context* c, + context::UserContext* u, + StrongSolverTheoryUF* thss) + : d_type(n.getType()), + d_thss(thss), + d_regions_index(c, 0), + d_regions_map(c), + d_split_score(c), + d_disequalities_index(c, 0), + d_reps(c, 0), + d_conflict(c, false), + d_cardinality(c, 1), + d_hasCard(c, false), + d_maxNegCard(c, 0), + d_initialized(u, false), + d_lemma_cache(u), + d_c_dec_strat(nullptr) { d_cardinality_term = n; - //if( d_type.isSort() ){ - // TypeEnumerator te(tn); - // d_cardinality_term = *te; - //}else{ - // d_cardinality_term = tn.mkGroundTerm(); - //} + + if (options::ufssMode() == UF_SS_FULL) + { + // Register the strategy with the decision manager of the theory. + // We are guaranteed that the decision manager is ready since we + // construct this module during TheoryUF::finishInit. + d_c_dec_strat.reset(new CardinalityDecisionStrategy( + n, c, thss->getTheory()->getValuation())); + } } SortModel::~SortModel() { @@ -480,9 +499,11 @@ SortModel::~SortModel() { /** initialize */ void SortModel::initialize( OutputChannel* out ){ - if( !d_initialized ){ + if (d_c_dec_strat.get() != nullptr && !d_initialized) + { d_initialized = true; - allocateCardinality( out ); + d_thss->getTheory()->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_UF_CARD, d_c_dec_strat.get()); } } @@ -761,35 +782,12 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ void SortModel::presolve() { d_initialized = false; - d_aloc_cardinality = 0; } void SortModel::propagate( Theory::Effort level, OutputChannel* out ){ } -Node SortModel::getNextDecisionRequest(){ - //request the current cardinality as a decision literal, if not already asserted - for( int i=1; i<=d_aloc_cardinality; i++ ){ - if( !d_hasCard || igetTheory()->d_valuation.hasSatValue( cn, value ) ){ - Trace("uf-ss-dec") << "UFSS : Get next decision " << d_type << " " << i << std::endl; - return cn; - }else{ - Trace("uf-ss-dec-debug") << " dec : " << cn << " already asserted " << value << std::endl; - Assert( !value ); - } - } - } - Trace("uf-ss-dec") << "UFSS : no decisions for " << d_type << "." << std::endl; - Trace("uf-ss-dec-debug") << " aloc_cardinality = " << d_aloc_cardinality << ", cardinality = " << d_cardinality << ", hasCard = " << d_hasCard << std::endl; - Assert( d_hasCard ); - return Node::null(); -} - int SortModel::getNumDisequalitiesToRegion( Node n, int ri ){ int ni = d_regions_map[n]; int counter = 0; @@ -863,26 +861,18 @@ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ } } } - }else{ - //see if we need to request a new cardinality - if( !d_hasCard ){ - bool needsCard = true; - for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); it!=d_cardinality_literal.end(); ++it ){ - if( it->first<=d_aloc_cardinality.get() ){ - bool value; - if( !d_thss->getTheory()->d_valuation.hasSatValue( it->second, value ) ){ - Debug("fmf-card-debug") << "..does not need allocate because we are waiting for " << it->second << std::endl; - needsCard = false; - break; - } - } - } - if( needsCard ){ - allocateCardinality( out ); - } - }else{ - Debug("fmf-card-debug") << "..already has card = " << d_cardinality << std::endl; + // we assert it positively, if its beyond the bound, abort + if (options::ufssAbortCardinality() != -1 + && c >= options::ufssAbortCardinality()) + { + std::stringstream ss; + ss << "Maximum cardinality (" << options::ufssAbortCardinality() + << ") for finite model finding exceeded." << std::endl; + throw LogicException(ss.str()); } + } + else + { if( c>d_maxNegCard.get() ){ Trace("uf-ss-com-card-debug") << "Maximum negative cardinality for " << d_type << " is now " << c << std::endl; d_maxNegCard.set( c ); @@ -993,95 +983,6 @@ void SortModel::moveNode( Node n, int ri ){ d_regions_map[n] = ri; } -void SortModel::allocateCardinality( OutputChannel* out ){ - if( d_aloc_cardinality>0 ){ - Trace("uf-ss-fmf") << "No model of size " << d_aloc_cardinality << " exists for type " << d_type << " in this branch" << std::endl; - } - Trace("uf-ss-debug") << "Allocate cardinality " << d_aloc_cardinality << " for type " << d_type << std::endl; - if( Trace.isOn("uf-ss-cliques") ){ - Trace("uf-ss-cliques") << "Cliques of size " << (d_aloc_cardinality+1) << " for " << d_type << " : " << std::endl; - for( size_t i=0; igetTheory()->d_valuation.hasSatValue( cl, value ) ){ - if( value ){ - //if one is already asserted postively, abort - return; - }else{ - increment = true; - } - } - }while( increment ); - - //check for abort case - if (options::ufssAbortCardinality() != -1 && - d_aloc_cardinality >= options::ufssAbortCardinality()) { - std::stringstream ss; - ss << "Maximum cardinality (" << options::ufssAbortCardinality() - << ") for finite model finding exceeded." << std::endl; - throw LogicException(ss.str()); - }else{ - if( applyTotality( d_aloc_cardinality ) ){ - //must generate new cardinality lemma term - Node var; - if( d_aloc_cardinality==1 && !options::ufssTotalitySymBreak() ){ - //get arbitrary ground term - var = d_cardinality_term; - }else{ - std::stringstream ss; - ss << "_c_" << d_aloc_cardinality; - var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" ); - } - if( d_aloc_cardinality-1<(int)d_totality_terms[0].size() ){ - d_totality_terms[0][d_aloc_cardinality-1] = var; - }else{ - d_totality_terms[0].push_back( var ); - } - Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl; - //must be distinct from all other cardinality terms - for( int i=0; i<(int)(d_totality_terms[0].size()-1); i++ ){ - Node lem = NodeManager::currentNM()->mkNode( NOT, var.eqNode( d_totality_terms[0][i] ) ); - Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem << std::endl; - d_thss->getOutputChannel().lemma( lem ); - } - } - - //add splitting lemma for cardinality constraint - Assert( !d_cardinality_term.isNull() ); - Node lem = getCardinalityLiteral( d_aloc_cardinality ); - lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); - d_cardinality_lemma[ d_aloc_cardinality ] = lem; - //add as lemma to output channel - if( doSendLemma( lem ) ){ - Trace("uf-ss-lemma") << "*** Cardinality split on : " << lem << std::endl; - } - //require phase - out->requirePhase( d_cardinality_literal[ d_aloc_cardinality ], true ); - d_thss->d_statistics.d_max_model_size.maxAssign( d_aloc_cardinality ); - - if( applyTotality( d_aloc_cardinality ) ){ - //must send totality axioms for each existing term - for( NodeIntMap::iterator it = d_regions_map.begin(); it != d_regions_map.end(); ++it ){ - addTotalityAxiom( (*it).first, d_aloc_cardinality, &d_thss->getOutputChannel() ); - } - } - } -} - int SortModel::addSplit( Region* r, OutputChannel* out ){ Node s; if( r->hasSplits() ){ @@ -1357,16 +1258,62 @@ int SortModel::getNumRegions(){ return count; } -Node SortModel::getCardinalityLiteral( int c ) { - if( d_cardinality_literal.find(c) == d_cardinality_literal.end() ){ - Node c_as_rational = NodeManager::currentNM()->mkConst(Rational(c)); - d_cardinality_literal[c] = - NodeManager::currentNM()->mkNode(CARDINALITY_CONSTRAINT, - d_cardinality_term, - c_as_rational); +Node SortModel::getCardinalityLiteral(unsigned c) +{ + Assert(c > 0); + std::map::iterator itcl = d_cardinality_literal.find(c); + if (itcl != d_cardinality_literal.end()) + { + return itcl->second; + } + // get the literal from the decision strategy + Node lit = d_c_dec_strat->getLiteral(c - 1); + d_cardinality_literal[c] = lit; + // Since we are reasoning about cardinality c, we invoke a totality axiom + if (!applyTotality(c)) + { + // return if we are not using totality axioms + return lit; + } + + NodeManager* nm = NodeManager::currentNM(); + Node var; + if (c == 1 && !options::ufssTotalitySymBreak()) + { + // get arbitrary ground term + var = d_cardinality_term; + } + else + { + std::stringstream ss; + ss << "_c_" << c; + var = nm->mkSkolem(ss.str(), d_type, "is a cardinality lemma term"); } - return d_cardinality_literal[c]; + if ((c - 1) < d_totality_terms[0].size()) + { + d_totality_terms[0][c - 1] = var; + } + else + { + d_totality_terms[0].push_back(var); + } + // must be distinct from all other cardinality terms + for (unsigned i = 1, size = d_totality_terms[0].size(); i < size; i++) + { + Node lem = var.eqNode(d_totality_terms[0][i - 1]).notNode(); + Trace("uf-ss-lemma") << "Totality distinctness lemma : " << lem + << std::endl; + d_thss->getOutputChannel().lemma(lem); + } + // must send totality axioms for each existing term + for (NodeIntMap::iterator it = d_regions_map.begin(); + it != d_regions_map.end(); + ++it) + { + addTotalityAxiom((*it).first, c, &d_thss->getOutputChannel()); + } + return lit; } StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, @@ -1377,13 +1324,21 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, d_th(th), d_conflict(c, false), d_rep_model(), - d_aloc_com_card(u, 0), - d_com_card_assertions(c), d_min_pos_com_card(c, -1), + d_cc_dec_strat(nullptr), + d_initializedCombinedCardinality(u, false), d_card_assertions_eqv_lemma(u), d_min_pos_tn_master_card(c, -1), d_rel_eqc(c) { + if (options::ufssMode() == UF_SS_FULL && options::ufssFairness()) + { + // Register the strategy with the decision manager of the theory. + // We are guaranteed that the decision manager is ready since we + // construct this module during TheoryUF::finishInit. + d_cc_dec_strat.reset( + new CombinedCardinalityDecisionStrategy(c, th->getValuation())); + } } StrongSolverTheoryUF::~StrongSolverTheoryUF() { @@ -1554,7 +1509,6 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ } } }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ - d_com_card_assertions[lit] = polarity; if( polarity ){ //safe to assume int here int nCard = lit[0].getConst().getNumerator().getSignedInt(); @@ -1562,26 +1516,6 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ d_min_pos_com_card.set( nCard ); checkCombinedCardinality(); } - }else{ - bool needsCard = true; - if( d_min_pos_com_card.get()==-1 ){ - //check if all current combined cardinality constraints are asserted negatively - for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){ - if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){ - Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl; - needsCard = false; - break; - }else{ - Assert( !d_com_card_assertions[it->second] ); - } - } - }else{ - Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : positive assertion : " << d_min_pos_com_card.get() << std::endl; - needsCard = false; - } - if( needsCard ){ - allocateCombinedCardinality(); - } } }else{ if( Trace.isOn("uf-ss-warn") ){ @@ -1683,45 +1617,30 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ } void StrongSolverTheoryUF::presolve() { - d_aloc_com_card.set( 0 ); + d_initializedCombinedCardinality = false; for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->presolve(); it->second->initialize( d_out ); } } -/** get next decision request */ -Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){ - //request the combined cardinality as a decision literal, if not already asserted - if( options::ufssMode()==UF_SS_FULL ){ - if( options::ufssFairness() ){ - int comCard = 0; - Node com_lit; - do { - if( comCard::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ - Node n = it->second->getNextDecisionRequest(); - if( !n.isNull() ){ - priority = 1; - return n; - } - } - } - Trace("uf-ss-dec") << "...no UF SS decisions." << std::endl; - return Node::null(); +StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy:: + CombinedCardinalityDecisionStrategy(context::Context* satContext, + Valuation valuation) + : DecisionStrategyFmf(satContext, valuation) +{ +} +Node StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::mkLiteral( + unsigned i) +{ + NodeManager* nm = NodeManager::currentNM(); + return nm->mkNode(COMBINED_CARDINALITY_CONSTRAINT, nm->mkConst(Rational(i))); +} + +std::string +StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::identify() const +{ + return std::string("uf_combined_card"); } void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ @@ -1842,12 +1761,12 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){ /** initialize */ void StrongSolverTheoryUF::initializeCombinedCardinality() { - Assert( options::ufssMode()==UF_SS_FULL ); - if( options::ufssFairness() ){ - if( d_aloc_com_card.get()==0 ){ - Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl; - allocateCombinedCardinality(); - } + if (d_cc_dec_strat.get() != nullptr + && !d_initializedCombinedCardinality.get()) + { + d_initializedCombinedCardinality = true; + d_th->getDecisionManager()->registerStrategy( + DecisionManager::STRAT_UF_COMBINED_CARD, d_cc_dec_strat.get()); } } @@ -1896,10 +1815,7 @@ void StrongSolverTheoryUF::checkCombinedCardinality() { int cc = d_min_pos_com_card.get(); if( cc !=-1 && totalCombinedCard > cc ){ //conflict - Assert( d_com_card_literal.find( cc ) != d_com_card_literal.end() ); - Node com_lit = d_com_card_literal[cc]; - Assert(d_com_card_assertions.find(com_lit)!=d_com_card_assertions.end()); - Assert( d_com_card_assertions[com_lit] ); + Node com_lit = d_cc_dec_strat->getLiteral(cc); std::vector< Node > conf; conf.push_back( com_lit ); int totalAdded = 0; @@ -1935,25 +1851,6 @@ void StrongSolverTheoryUF::checkCombinedCardinality() { } } -void StrongSolverTheoryUF::allocateCombinedCardinality() { - Assert( options::ufssMode()==UF_SS_FULL ); - Trace("uf-ss-com-card") << "Allocate combined cardinality (" << d_aloc_com_card.get() << ")" << std::endl; - //make node - Node lem = NodeManager::currentNM()->mkNode( COMBINED_CARDINALITY_CONSTRAINT, - NodeManager::currentNM()->mkConst( Rational( d_aloc_com_card.get() ) ) ); - Trace("uf-ss-com-card") << "Split on " << lem << std::endl; - lem = Rewriter::rewrite(lem); - d_com_card_literal[ d_aloc_com_card.get() ] = lem; - lem = NodeManager::currentNM()->mkNode( OR, lem, lem.notNode() ); - //add as lemma to output channel - Trace("uf-ss-lemma") << "*** Combined cardinality split : " << lem << std::endl; - getOutputChannel().lemma( lem ); - //require phase - getOutputChannel().requirePhase( d_com_card_literal[ d_aloc_com_card.get() ], true ); - //increment cardinality - d_aloc_com_card.set( d_aloc_com_card.get() + 1 ); -} - StrongSolverTheoryUF::Statistics::Statistics(): d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0), d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0), diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 2e219da04..286c7391a 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -23,6 +23,8 @@ #include "theory/theory.h" #include "util/statistics_registry.h" +#include "theory/decision_manager.h" + namespace CVC4 { class SortInference; namespace theory { @@ -262,16 +264,12 @@ public: context::CDO d_conflict; /** cardinality */ context::CDO< int > d_cardinality; - /** maximum allocated cardinality */ - context::CDO< int > d_aloc_cardinality; /** cardinality lemma term */ Node d_cardinality_term; /** cardinality totality terms */ std::map< int, std::vector< Node > > d_totality_terms; /** cardinality literals */ std::map< int, Node > d_cardinality_literal; - /** cardinality lemmas */ - std::map< int, Node > d_cardinality_lemma; /** whether a positive cardinality constraint has been asserted */ context::CDO< bool > d_hasCard; /** clique lemmas that have been asserted */ @@ -314,8 +312,6 @@ public: void presolve(); /** propagate */ void propagate( Theory::Effort level, OutputChannel* out ); - /** get next decision request */ - Node getNextDecisionRequest(); /** assert cardinality */ void assertCardinality( OutputChannel* out, int c, bool val ); /** is in conflict */ @@ -327,16 +323,40 @@ public: /** get cardinality term */ Node getCardinalityTerm() { return d_cardinality_term; } /** get cardinality literal */ - Node getCardinalityLiteral( int c ); + Node getCardinalityLiteral(unsigned c); /** get maximum negative cardinality */ int getMaximumNegativeCardinality() { return d_maxNegCard.get(); } //print debug void debugPrint( const char* c ); /** debug a model */ bool debugModel( TheoryModel* m ); - public: /** get number of regions (for debugging) */ int getNumRegions(); + + private: + /** + * Decision strategy for cardinality constraints. This asserts + * the minimal constraint positively in the SAT context. For details, see + * Section 6.3 of Reynolds et al, "Constraint Solving for Finite Model + * Finding in SMT Solvers", TPLP 2017. + */ + class CardinalityDecisionStrategy : public DecisionStrategyFmf + { + public: + CardinalityDecisionStrategy(Node t, + context::Context* satContext, + Valuation valuation); + /** make literal (the i^th combined cardinality literal) */ + Node mkLiteral(unsigned i) override; + /** identify */ + std::string identify() const override; + + private: + /** the cardinality term */ + Node d_cardinality_term; + }; + /** cardinality decision strategy */ + std::unique_ptr d_c_dec_strat; }; /** class SortModel */ public: @@ -365,8 +385,6 @@ public: void check( Theory::Effort level ); /** presolve */ void presolve(); - /** get next decision request */ - Node getNextDecisionRequest( unsigned& priority ); /** preregister a term */ void preRegisterTerm( TNode n ); /** identify */ @@ -403,8 +421,6 @@ public: SortModel* getSortModel(Node n); /** initialize */ void initializeCombinedCardinality(); - /** allocateCombinedCardinality */ - void allocateCombinedCardinality(); /** check */ void checkCombinedCardinality(); /** ensure eqc */ @@ -420,14 +436,31 @@ public: context::CDO d_conflict; /** rep model structure, one for each type */ std::map d_rep_model; - /** allocated combined cardinality */ - context::CDO d_aloc_com_card; - /** combined cardinality constraints */ - std::map d_com_card_literal; - /** combined cardinality assertions (indexed by cardinality literals ) */ - NodeBoolMap d_com_card_assertions; + /** minimum positive combined cardinality */ context::CDO d_min_pos_com_card; + /** + * Decision strategy for combined cardinality constraints. This asserts + * the minimal combined cardinality constraint positively in the SAT + * context. It is enabled by options::ufssFairness(). For details, see + * the extension to multiple sorts in Section 6.3 of Reynolds et al, + * "Constraint Solving for Finite Model Finding in SMT Solvers", TPLP 2017. + */ + class CombinedCardinalityDecisionStrategy : public DecisionStrategyFmf + { + public: + CombinedCardinalityDecisionStrategy(context::Context* satContext, + Valuation valuation); + /** make literal (the i^th combined cardinality literal) */ + Node mkLiteral(unsigned i) override; + /** identify */ + std::string identify() const override; + }; + /** combined cardinality decision strategy */ + std::unique_ptr d_cc_dec_strat; + /** Have we initialized combined cardinality? */ + context::CDO d_initializedCombinedCardinality; + /** cardinality literals for which we have added */ NodeBoolMap d_card_assertions_eqv_lemma; /** the master monotone type (if ufssFairnessMonotone enabled) */ -- 2.30.2