From: Andrew Reynolds Date: Mon, 12 Oct 2020 22:56:32 +0000 (-0500) Subject: Remove uf-ss-totality option (#5251) X-Git-Tag: cvc5-1.0.0~2722 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b22b24ed70962fb9a5ce50d4cd202d70d7380bee;p=cvc5.git Remove uf-ss-totality option (#5251) This option has a number of subtle bugs, it should be reimplemented if/when finite-model-find is refactored. It is not high priority enough to maintain. This does some additional cleaning of the uf cardinality extension, some methods changed indentation. Fixes #5239, fixes #4872, fixes #4865. --- diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index 6916598ce..a098061f8 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -11,15 +11,6 @@ header = "options/uf_options.h" default = "true" help = "use UF symmetry breaker (Deharbe et al., CADE 2011)" -[[option]] - name = "ufssTotality" - category = "regular" - long = "uf-ss-totality" - type = "bool" - default = "false" - read_only = true - help = "always use totality axioms for enforcing cardinality constraints" - [[option]] name = "ufssTotalityLimited" category = "regular" diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 73c6b0a21..688a8b645 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -22,15 +22,10 @@ #include "theory/quantifiers/term_database.h" #include "theory/theory_model.h" -//#define ONE_SPLIT_REGION -//#define COMBINE_REGIONS_SMALL_INTO_LARGE -//#define LAZY_REL_EQC - using namespace std; using namespace CVC4::kind; using namespace CVC4::context; - namespace CVC4 { namespace theory { namespace uf { @@ -517,38 +512,21 @@ void SortModel::newEqClass( Node n ){ if (!d_state.isInConflict()) { if( d_regions_map.find( n )==d_regions_map.end() ){ - // Must generate totality axioms for every cardinality we have - // allocated thus far. - for( std::map< int, Node >::iterator it = d_cardinality_literal.begin(); - it != d_cardinality_literal.end(); ++it ){ - if( applyTotality( it->first ) ){ - addTotalityAxiom(n, it->first); - } - } - if( options::ufssTotality() ){ - // Regions map will store whether we need to equate this term - // with a constant equivalence class. - if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){ - d_regions_map[n] = 0; - }else{ - d_regions_map[n] = -1; - } + d_regions_map[n] = d_regions_index; + Debug("uf-ss") << "CardinalityExtension: New Eq Class " << n << std::endl; + Debug("uf-ss-debug") << d_regions_index << " " << (int)d_regions.size() + << std::endl; + if (d_regions_index < d_regions.size()) + { + d_regions[d_regions_index]->debugPrint("uf-ss-debug", true); + d_regions[d_regions_index]->setValid(true); + Assert(d_regions[d_regions_index]->getNumReps() == 0); }else{ - d_regions_map[n] = d_regions_index; - Debug("uf-ss") << "CardinalityExtension: New Eq Class " << n - << std::endl; - Debug("uf-ss-debug") << d_regions_index << " " - << (int)d_regions.size() << std::endl; - if( d_regions_indexdebugPrint("uf-ss-debug",true); - d_regions[ d_regions_index ]->setValid(true); - Assert(d_regions[d_regions_index]->getNumReps() == 0); - }else{ - d_regions.push_back(new Region(this, d_state.getSatContext())); - } - d_regions[ d_regions_index ]->addRep( n ); - d_regions_index = d_regions_index + 1; + d_regions.push_back(new Region(this, d_state.getSatContext())); } + d_regions[d_regions_index]->addRep(n); + d_regions_index = d_regions_index + 1; + d_reps = d_reps + 1; } } @@ -556,107 +534,116 @@ void SortModel::newEqClass( Node n ){ /** merge */ void SortModel::merge( Node a, Node b ){ - if (!d_state.isInConflict()) + if (d_state.isInConflict()) + { + return; + } + Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b << "..." + << std::endl; + if (a != b) { - if( options::ufssTotality() ){ - if( d_regions_map[b]==-1 ){ - d_regions_map[a] = -1; + Assert(d_regions_map.find(a) != d_regions_map.end()); + Assert(d_regions_map.find(b) != d_regions_map.end()); + int ai = d_regions_map[a]; + int bi = d_regions_map[b]; + Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; + if (ai != bi) + { + if (d_regions[ai]->getNumReps() == 1) + { + int ri = combineRegions(bi, ai); + d_regions[ri]->setEqual(a, b); + checkRegion(ri); } - d_regions_map[b] = -1; - }else{ - Debug("uf-ss") << "CardinalityExtension: Merging " << a << " = " << b - << "..." << std::endl; - if( a!=b ){ - Assert(d_regions_map.find(a) != d_regions_map.end()); - Assert(d_regions_map.find(b) != d_regions_map.end()); - int ai = d_regions_map[a]; - int bi = d_regions_map[b]; - Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; - if( ai!=bi ){ - if( d_regions[ai]->getNumReps()==1 ){ - int ri = combineRegions( bi, ai ); - d_regions[ri]->setEqual( a, b ); - checkRegion( ri ); - }else if( d_regions[bi]->getNumReps()==1 ){ - int ri = combineRegions( ai, bi ); - d_regions[ri]->setEqual( a, b ); - checkRegion( ri ); - }else{ - // Either move a to d_regions[bi], or b to d_regions[ai]. - RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a); - RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b); - int aex = ( a_region_info->getNumInternalDisequalities() - - getNumDisequalitiesToRegion( a, bi ) ); - int bex = ( b_region_info->getNumInternalDisequalities() - - getNumDisequalitiesToRegion( b, ai ) ); - // Based on which would produce the fewest number of - // external disequalities. - if( aexsetEqual( a, b ); - }else{ - moveNode( b, ai ); - d_regions[ai]->setEqual( a, b ); - } - checkRegion( ai ); - checkRegion( bi ); - } + else if (d_regions[bi]->getNumReps() == 1) + { + int ri = combineRegions(ai, bi); + d_regions[ri]->setEqual(a, b); + checkRegion(ri); + } + else + { + // Either move a to d_regions[bi], or b to d_regions[ai]. + RegionNodeInfo* a_region_info = d_regions[ai]->getRegionInfo(a); + RegionNodeInfo* b_region_info = d_regions[bi]->getRegionInfo(b); + int aex = (a_region_info->getNumInternalDisequalities() + - getNumDisequalitiesToRegion(a, bi)); + int bex = (b_region_info->getNumInternalDisequalities() + - getNumDisequalitiesToRegion(b, ai)); + // Based on which would produce the fewest number of + // external disequalities. + if (aex < bex) + { + moveNode(a, bi); + d_regions[bi]->setEqual(a, b); }else{ + moveNode(b, ai); d_regions[ai]->setEqual( a, b ); - checkRegion( ai ); } - d_regions_map[b] = -1; + checkRegion(ai); + checkRegion(bi); } - d_reps = d_reps - 1; } + else + { + d_regions[ai]->setEqual(a, b); + checkRegion(ai); + } + d_regions_map[b] = -1; } + d_reps = d_reps - 1; } /** assert terms are disequal */ void SortModel::assertDisequal( Node a, Node b, Node reason ){ - if (!d_state.isInConflict()) + if (d_state.isInConflict()) { - if( options::ufssTotality() ){ - //do nothing - }else{ - //if they are not already disequal - eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine(); - a = ee->getRepresentative(a); - b = ee->getRepresentative(b); - int ai = d_regions_map[a]; - int bi = d_regions_map[b]; - if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){ - Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl; - //if( reason.getKind()!=NOT || reason[0].getKind()!=EQUAL || - // a!=reason[0][0] || b!=reason[0][1] ){ - // Notice() << "Assert disequal " << a << " != " << b << ", reason = " << reason << "..." << std::endl; - //} - Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." << std::endl; - //add to list of disequalities - if( d_disequalities_indexsetDisequal( a, b, 1, true ); - d_regions[ai]->setDisequal( b, a, 1, true ); - checkRegion( ai, false ); //do not need to check if it needs to combine (no new ext. disequalities) - }else{ - //external disequality - d_regions[ai]->setDisequal( a, b, 0, true ); - d_regions[bi]->setDisequal( b, a, 0, true ); - checkRegion( ai ); - checkRegion( bi ); - } - } - } + return; + } + // if they are not already disequal + eq::EqualityEngine* ee = d_thss->getTheory()->getEqualityEngine(); + a = ee->getRepresentative(a); + b = ee->getRepresentative(b); + int ai = d_regions_map[a]; + int bi = d_regions_map[b]; + if (d_regions[ai]->isDisequal(a, b, ai == bi)) + { + // already disequal + return; + } + Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." + << std::endl; + Debug("uf-ss-disequal") << "Assert disequal " << a << " != " << b << "..." + << std::endl; + // add to list of disequalities + if (d_disequalities_index < d_disequalities.size()) + { + d_disequalities[d_disequalities_index] = reason; + } + else + { + d_disequalities.push_back(reason); + } + d_disequalities_index = d_disequalities_index + 1; + // now, add disequalities to regions + Assert(d_regions_map.find(a) != d_regions_map.end()); + Assert(d_regions_map.find(b) != d_regions_map.end()); + Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; + if (ai == bi) + { + // internal disequality + d_regions[ai]->setDisequal(a, b, 1, true); + d_regions[ai]->setDisequal(b, a, 1, true); + // do not need to check if it needs to combine (no new ext. disequalities) + checkRegion(ai, false); + } + else + { + // external disequality + d_regions[ai]->setDisequal(a, b, 0, true); + d_regions[bi]->setDisequal(b, a, 0, true); + checkRegion(ai); + checkRegion(bi); } } @@ -673,116 +660,134 @@ bool SortModel::areDisequal( Node a, Node b ) { } } -/** check */ void SortModel::check(Theory::Effort level) { Assert(options::ufssMode() == options::UfssMode::FULL); - if (level >= Theory::EFFORT_STANDARD && d_hasCard && !d_state.isInConflict()) + if (!d_hasCard && d_state.isInConflict()) { - Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type - << std::endl; + // not necessary to check + return; + } + Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type + << std::endl; + if (level == Theory::EFFORT_FULL) + { + Debug("fmf-full-check") << std::endl; + Debug("fmf-full-check") + << "Full check for SortModel " << d_type << ", status : " << std::endl; + debugPrint("fmf-full-check"); + Debug("fmf-full-check") << std::endl; + } + if (d_reps <= (unsigned)d_cardinality) + { + Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " + << d_type << ", <= " << d_cardinality << std::endl; if( level==Theory::EFFORT_FULL ){ - Debug("fmf-full-check") << std::endl; - Debug("fmf-full-check") << "Full check for SortModel " << d_type << ", status : " << std::endl; - debugPrint("fmf-full-check"); - Debug("fmf-full-check") << std::endl; + Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " + << d_type << ", <= " << d_cardinality << std::endl; } - if( d_reps<=(unsigned)d_cardinality ){ - Debug("uf-ss-debug") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl; - if( level==Theory::EFFORT_FULL ){ - Debug("uf-ss-sat") << "We have " << d_reps << " representatives for type " << d_type << ", <= " << d_cardinality << std::endl; - //Notice() << "We have " << d_reps << " representatives for type " << d_type << ", <= " << cardinality << std::endl; - //Notice() << "Model size for " << d_type << " is " << cardinality << std::endl; - //Notice() << cardinality << " "; + return; + } + // first check if we can generate a clique conflict + // do a check within each region + for (size_t i = 0; i < d_regions_index; i++) + { + if (d_regions[i]->valid()) + { + std::vector clique; + if (d_regions[i]->check(level, d_cardinality, clique)) + { + // add clique lemma + addCliqueLemma(clique); + return; } - return; - }else{ - //first check if we can generate a clique conflict - if( !options::ufssTotality() ){ - //do a check within each region - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->valid() ){ - std::vector< Node > clique; - if( d_regions[i]->check( level, d_cardinality, clique ) ){ - //add clique lemma - addCliqueLemma(clique); - return; - }else{ - Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl; - } - } + else + { + Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl; + } + } + } + // do splitting on demand + bool addedLemma = false; + if (level == Theory::EFFORT_FULL) + { + Trace("uf-ss-debug") << "Add splits?" << std::endl; + // see if we have any recommended splits from large regions + for (size_t i = 0; i < d_regions_index; i++) + { + if (d_regions[i]->valid() && d_regions[i]->getNumReps() > d_cardinality) + { + int sp = addSplit(d_regions[i]); + if (sp == 1) + { + addedLemma = true; + } + else if (sp == -1) + { + check(level); + return; } } - if( !applyTotality( d_cardinality ) ){ - //do splitting on demand - bool addedLemma = false; - if (level==Theory::EFFORT_FULL) + } + } + // If no added lemmas, force continuation via combination of regions. + if (level != Theory::EFFORT_FULL || addedLemma) + { + return; + } + // check at full effort + Trace("uf-ss-debug") << "No splits added. " << d_cardinality << std::endl; + Trace("uf-ss-si") << "Must combine region" << std::endl; + bool recheck = false; + SortInference* si = d_thss->getSortInference(); + if (si != nullptr) + { + // If sort inference is enabled, search for regions with same sort. + std::map sortsFound; + for (size_t i = 0; i < d_regions_index; i++) + { + if (d_regions[i]->valid()) + { + Node op = d_regions[i]->frontKey(); + int sort_id = si->getSortId(op); + if (sortsFound.find(sort_id) != sortsFound.end()) { - Trace("uf-ss-debug") << "Add splits?" << std::endl; - //see if we have any recommended splits from large regions - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->valid() && d_regions[i]->getNumReps()>d_cardinality ){ - int sp = addSplit(d_regions[i]); - if( sp==1 ){ - addedLemma = true; -#ifdef ONE_SPLIT_REGION - break; -#endif - }else if( sp==-1 ){ - check(level); - return; - } - } - } + Debug("fmf-full-check") << "Combined regions " << i << " " + << sortsFound[sort_id] << std::endl; + combineRegions(sortsFound[sort_id], i); + recheck = true; + break; } - //If no added lemmas, force continuation via combination of regions. - if( level==Theory::EFFORT_FULL ){ - if( !addedLemma ){ - Trace("uf-ss-debug") << "No splits added. " << d_cardinality - << std::endl; - Trace("uf-ss-si") << "Must combine region" << std::endl; - bool recheck = false; - SortInference* si = d_thss->getSortInference(); - if (si != nullptr) - { - //If sort inference is enabled, search for regions with same sort. - std::map< int, int > sortsFound; - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->valid() ){ - Node op = d_regions[i]->frontKey(); - int sort_id = si->getSortId(op); - if( sortsFound.find( sort_id )!=sortsFound.end() ){ - Debug("fmf-full-check") << "Combined regions " << i << " " << sortsFound[sort_id] << std::endl; - combineRegions( sortsFound[sort_id], i ); - recheck = true; - break; - }else{ - sortsFound[sort_id] = i; - } - } - } - } - if( !recheck ) { - //naive strategy, force region combination involving the first valid region - for( int i=0; i<(int)d_regions_index; i++ ){ - if( d_regions[i]->valid() ){ - int fcr = forceCombineRegion( i, false ); - Debug("fmf-full-check") << "Combined regions " << i << " " << fcr << std::endl; - Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl; - recheck = true; - break; - } - } - } - if( recheck ){ - Trace("uf-ss-debug") << "Must recheck." << std::endl; - check(level); - } - } + else + { + sortsFound[sort_id] = i; } } } } + if (!recheck) + { + // naive strategy, force region combination involving the first + // valid region + for (size_t i = 0; i < d_regions_index; i++) + { + if (d_regions[i]->valid()) + { + int fcr = forceCombineRegion(i, false); + Debug("fmf-full-check") + << "Combined regions " << i << " " << fcr << std::endl; + Trace("uf-ss-debug") + << "Combined regions " << i << " " << fcr << std::endl; + recheck = true; + break; + } + } + } + if (recheck) + { + Trace("uf-ss-debug") << "Must recheck." << std::endl; + check(level); + } } void SortModel::presolve() { @@ -960,11 +965,6 @@ int SortModel::forceCombineRegion( int ri, bool useDensity ){ int SortModel::combineRegions( int ai, int bi ){ -#ifdef COMBINE_REGIONS_SMALL_INTO_LARGE - if( d_regions[ai]->getNumReps()getNumReps() ){ - return combineRegions( bi, ai ); - } -#endif Debug("uf-ss-region") << "uf-ss: Combine Region #" << bi << " with Region #" << ai << std::endl; Assert(isValid(ai) && isValid(bi)); Region* region_bi = d_regions[bi]; @@ -1078,71 +1078,6 @@ void SortModel::addCliqueLemma(std::vector& clique) } } -void SortModel::addTotalityAxiom(Node n, int cardinality) -{ - if( std::find( d_totality_terms[0].begin(), d_totality_terms[0].end(), n )==d_totality_terms[0].end() ){ - if( std::find( d_totality_lems[n].begin(), d_totality_lems[n].end(), cardinality ) == d_totality_lems[n].end() ){ - NodeManager* nm = NodeManager::currentNM(); - d_totality_lems[n].push_back( cardinality ); - Node cardLit = d_cardinality_literal[ cardinality ]; - int sort_id = 0; - SortInference* si = d_thss->getSortInference(); - if (si != nullptr) - { - sort_id = si->getSortId(n); - } - Trace("uf-ss-totality") << "Add totality lemma for " << n << " " << cardinality << ", sort id is " << sort_id << std::endl; - int use_cardinality = cardinality; - if( options::ufssTotalitySymBreak() ){ - if( d_sym_break_index.find(n)!=d_sym_break_index.end() ){ - use_cardinality = d_sym_break_index[n]; - }else if( (int)d_sym_break_terms[n.getType()][sort_id].size() eqs; - for( int i=0; imkNode(OR, eqs); - Node lem = NodeManager::currentNM()->mkNode( IMPLIES, cardLit, ax ); - Trace("uf-ss-lemma") << "*** Add totality axiom " << lem << std::endl; - //send as lemma to the output channel - d_im.lemma(lem, LemmaProperty::NONE, false); - ++( d_thss->d_statistics.d_totality_lemmas ); - } - } -} - -/** apply totality */ -bool SortModel::applyTotality( int cardinality ){ - return options::ufssTotality() || cardinality<=options::ufssTotalityLimited(); -} - -/** get totality lemma terms */ -Node SortModel::getTotalityLemmaTerm( int cardinality, int i ){ - return d_totality_terms[0][i]; -} - void SortModel::simpleCheckCardinality() { if( d_maxNegCard.get()!=0 && d_hasCard.get() && d_cardinality.get()mkNode( AND, getCardinalityLiteral( d_cardinality.get() ), @@ -1249,10 +1184,10 @@ int SortModel::getNumRegions(){ return count; } -Node SortModel::getCardinalityLiteral(unsigned c) +Node SortModel::getCardinalityLiteral(size_t c) { Assert(c > 0); - std::map::iterator itcl = d_cardinality_literal.find(c); + std::map::iterator itcl = d_cardinality_literal.find(c); if (itcl != d_cardinality_literal.end()) { return itcl->second; @@ -1261,49 +1196,7 @@ Node SortModel::getCardinalityLiteral(unsigned c) 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"); - } - 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_im.lemma(lem, LemmaProperty::NONE, false); - } - // 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); - } + // return the literal return lit; } @@ -1391,15 +1284,11 @@ void CardinalityExtension::newEqClass(Node a) { SortModel* c = getSortModel( a ); if( c ){ -#ifdef LAZY_REL_EQC - //do nothing -#else Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : " << a.getType() << std::endl; c->newEqClass( a ); Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class." << std::endl; -#endif } } @@ -1409,23 +1298,10 @@ void CardinalityExtension::merge(Node a, Node b) //TODO: ensure they are relevant SortModel* c = getSortModel( a ); if( c ){ -#ifdef LAZY_REL_EQC - ensureEqc( c, a ); - if( hasEqc( b ) ){ - Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b - << " : " << a.getType() << std::endl; - c->merge( a, b ); - Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl; - }else{ - //c->assignEqClass( b, a ); - d_rel_eqc[b] = true; - } -#else Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b << " : " << a.getType() << std::endl; c->merge( a, b ); Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl; -#endif } } @@ -1434,10 +1310,6 @@ void CardinalityExtension::assertDisequal(Node a, Node b, Node reason) { SortModel* c = getSortModel( a ); if( c ){ -#ifdef LAZY_REL_EQC - ensureEqc( c, a ); - ensureEqc( c, b ); -#endif Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl; c->assertDisequal( a, b, reason ); @@ -1450,9 +1322,6 @@ void CardinalityExtension::assertDisequal(Node a, Node b, Node reason) void CardinalityExtension::assertNode(Node n, bool isDecision) { Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl; -#ifdef LAZY_REL_EQC - ensureEqcRec( n ); -#endif bool polarity = n.getKind() != kind::NOT; TNode lit = polarity ? n : n[0]; if (options::ufssMode() == options::UfssMode::FULL) @@ -1860,15 +1729,11 @@ CardinalityExtension::Statistics::Statistics() : d_clique_conflicts("CardinalityExtension::Clique_Conflicts", 0), d_clique_lemmas("CardinalityExtension::Clique_Lemmas", 0), d_split_lemmas("CardinalityExtension::Split_Lemmas", 0), - d_disamb_term_lemmas("CardinalityExtension::Disambiguate_Term_Lemmas", 0), - d_totality_lemmas("CardinalityExtension::Totality_Lemmas", 0), d_max_model_size("CardinalityExtension::Max_Model_Size", 1) { smtStatisticsRegistry()->registerStat(&d_clique_conflicts); smtStatisticsRegistry()->registerStat(&d_clique_lemmas); smtStatisticsRegistry()->registerStat(&d_split_lemmas); - smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas); - smtStatisticsRegistry()->registerStat(&d_totality_lemmas); smtStatisticsRegistry()->registerStat(&d_max_model_size); } @@ -1877,8 +1742,6 @@ CardinalityExtension::Statistics::~Statistics() smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts); smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas); smtStatisticsRegistry()->unregisterStat(&d_max_model_size); } diff --git a/src/theory/uf/cardinality_extension.h b/src/theory/uf/cardinality_extension.h index db27c98cd..cbef690b1 100644 --- a/src/theory/uf/cardinality_extension.h +++ b/src/theory/uf/cardinality_extension.h @@ -222,7 +222,7 @@ class CardinalityExtension /** Pointer to the cardinality extension that owns this. */ CardinalityExtension* d_thss; /** regions used to d_region_index */ - context::CDO< unsigned > d_regions_index; + context::CDO d_regions_index; /** vector of regions */ std::vector< Region* > d_regions; /** map from Nodes to index of d_regions they exist in, -1 means invalid */ @@ -265,31 +265,22 @@ class CardinalityExtension int addSplit(Region* r); /** add clique lemma */ void addCliqueLemma(std::vector& clique); - /** add totality axiom */ - void addTotalityAxiom(Node n, int cardinality); /** cardinality */ - context::CDO< int > d_cardinality; + context::CDO d_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; + std::map d_cardinality_literal; /** whether a positive cardinality constraint has been asserted */ context::CDO< bool > d_hasCard; /** clique lemmas that have been asserted */ std::map< int, std::vector< std::vector< Node > > > d_cliques; /** maximum negatively asserted cardinality */ - context::CDO< int > d_maxNegCard; + context::CDO d_maxNegCard; /** list of fresh representatives allocated */ std::vector< Node > d_fresh_aloc_reps; /** whether we are initialized */ context::CDO< bool > d_initialized; - - /** apply totality */ - bool applyTotality( int cardinality ); - /** get totality lemma terms */ - Node getTotalityLemmaTerm( int cardinality, int i ); /** simple check cardinality */ void simpleCheckCardinality(); @@ -322,7 +313,7 @@ class CardinalityExtension /** get cardinality term */ Node getCardinalityTerm() { return d_cardinality_term; } /** get cardinality literal */ - Node getCardinalityLiteral(unsigned c); + Node getCardinalityLiteral(size_t c); /** get maximum negative cardinality */ int getMaximumNegativeCardinality() { return d_maxNegCard.get(); } //print debug @@ -406,8 +397,6 @@ class CardinalityExtension IntStat d_clique_conflicts; IntStat d_clique_lemmas; IntStat d_split_lemmas; - IntStat d_disamb_term_lemmas; - IntStat d_totality_lemmas; IntStat d_max_model_size; Statistics(); ~Statistics(); diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 3a6c60fb0..f239492af 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -509,6 +509,8 @@ set(regress_0_tests regress0/fmf/fmf-strange-bounds-2.smt2 regress0/fmf/forall_unit_data2.smt2 regress0/fmf/issue3661-ccard-dec.smt2 + regress0/fmf/issue4872-qf_ufc.smt2 + regress0/fmf/issue5239-uf-ss-tot.smt2 regress0/fmf/krs-sat.smt2 regress0/fmf/no-minimal-sat.smt2 regress0/fmf/quant_real_univ.cvc diff --git a/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 new file mode 100644 index 000000000..c46bc1e28 --- /dev/null +++ b/test/regress/regress0/fmf/issue4872-qf_ufc.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_UFC) +(set-info :status sat) +(declare-sort S0 0) +(declare-const S0-0 S0) +(assert (fmf.card S0-0 1)) +(assert (fmf.card S0-0 4)) +(check-sat) diff --git a/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 new file mode 100644 index 000000000..a92f2f441 --- /dev/null +++ b/test/regress/regress0/fmf/issue5239-uf-ss-tot.smt2 @@ -0,0 +1,6 @@ +(set-logic UFC) +(set-info :status sat) +(declare-sort a 0) +(declare-fun b () a) +(assert (fmf.card b 2)) +(check-sat) diff --git a/test/regress/regress1/fmf/issue4068-si-qf.smt2 b/test/regress/regress1/fmf/issue4068-si-qf.smt2 index 792977260..de6da315f 100644 --- a/test/regress/regress1/fmf/issue4068-si-qf.smt2 +++ b/test/regress/regress1/fmf/issue4068-si-qf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --uf-ss-totality --fmf-fun --sort-inference --no-check-models +; COMMAND-LINE: --fmf-fun --sort-inference --no-check-models ; EXPECT: sat (set-logic QF_UFNIA) (set-info :status sat)