From f62cb035e728c77facc94c5dfe3a8a2df65aa3a7 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 12 Sep 2019 18:35:57 -0500 Subject: [PATCH] Rename UF with cardinality extension (#3241) --- src/CMakeLists.txt | 4 +- src/options/options_handler.cpp | 10 +- src/options/uf_options.toml | 22 +- src/options/ufss_mode.h | 19 +- src/theory/quantifiers/fmf/model_builder.cpp | 1 - src/theory/quantifiers/fmf/model_engine.cpp | 12 +- ...g_solver.cpp => cardinality_extension.cpp} | 249 +++++++++--------- ...trong_solver.h => cardinality_extension.h} | 80 +++--- src/theory/uf/equality_engine.cpp | 2 +- src/theory/uf/theory_uf.cpp | 4 +- src/theory/uf/theory_uf.h | 12 +- 11 files changed, 203 insertions(+), 212 deletions(-) rename src/theory/uf/{theory_uf_strong_solver.cpp => cardinality_extension.cpp} (90%) rename src/theory/uf/{theory_uf_strong_solver.h => cardinality_extension.h} (93%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index d6376fb8d..4f56be8a9 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -679,6 +679,8 @@ libcvc4_add_sources( theory/type_enumerator.h theory/type_set.cpp theory/type_set.h + theory/uf/cardinality_extension.cpp + theory/uf/cardinality_extension.h theory/uf/equality_engine.cpp theory/uf/equality_engine.h theory/uf/equality_engine_types.h @@ -691,8 +693,6 @@ libcvc4_add_sources( theory/uf/theory_uf_model.cpp theory/uf/theory_uf_model.h theory/uf/theory_uf_rewriter.h - theory/uf/theory_uf_strong_solver.cpp - theory/uf/theory_uf_strong_solver.h theory/uf/theory_uf_type_rules.h theory/valuation.cpp theory/valuation.h diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 874c57629..e838988c9 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -1587,16 +1587,18 @@ void OptionsHandler::setBitblastAig(std::string option, bool arg) // theory/uf/options_handlers.h const std::string OptionsHandler::s_ufssModeHelp = "\ -UF strong solver options currently supported by the --uf-ss option:\n\ +UF with cardinality options currently supported by the --uf-ss option when\n\ +combined with finite model finding:\n\ \n\ full \n\ -+ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\ ++ Default, use UF with cardinality to find minimal models for uninterpreted\n\ +sorts.\n\ \n\ no-minimal \n\ -+ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\ ++ Use UF with cardinality to shrink models, but do no enforce minimality.\n\ \n\ none \n\ -+ Do not use uf strong solver to shrink model sizes. \n\ ++ Do not use UF with cardinality to shrink model sizes. \n\ \n\ "; diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml index e0c34127a..8790e4ec3 100644 --- a/src/options/uf_options.toml +++ b/src/options/uf_options.toml @@ -11,24 +11,6 @@ header = "options/uf_options.h" default = "true" help = "use UF symmetry breaker (Deharbe et al., CADE 2011)" -[[option]] - name = "ufssRegions" - category = "regular" - long = "uf-ss-regions" - type = "bool" - default = "true" - read_only = true - help = "disable region-based method for discovering cliques and splits in uf strong solver" - -[[option]] - name = "ufssEagerSplits" - category = "regular" - long = "uf-ss-eager-split" - type = "bool" - default = "false" - read_only = true - help = "add splits eagerly for uf strong solver" - [[option]] name = "ufssTotality" category = "regular" @@ -63,7 +45,7 @@ header = "options/uf_options.h" type = "int" default = "-1" read_only = true - help = "tells the uf strong solver to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)" + help = "tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)" [[option]] name = "ufssMode" @@ -74,7 +56,7 @@ header = "options/uf_options.h" handler = "stringToUfssMode" includes = ["options/ufss_mode.h"] read_only = true - help = "mode of operation for uf strong solver." + help = "mode of operation for uf with cardinality solver." [[option]] name = "ufssFairness" diff --git a/src/options/ufss_mode.h b/src/options/ufss_mode.h index d6a106ecf..452317b8f 100644 --- a/src/options/ufss_mode.h +++ b/src/options/ufss_mode.h @@ -23,12 +23,23 @@ namespace CVC4 { namespace theory { namespace uf { -enum UfssMode{ - /** default, use uf strong solver to find minimal models for uninterpreted sorts */ +/** + * These modes determine the role of UF with cardinality when using finite model + * finding (--finite-model-find). + */ +enum UfssMode +{ + /** + * Default, use UF with cardinality to find minimal models for uninterpreted + * sorts. + */ UF_SS_FULL, - /** use uf strong solver to shrink model sizes, but do no enforce minimality */ + /** + * Use UF with cardinality to shrink model sizes, but do no enforce + * minimality. + */ UF_SS_NO_MINIMAL, - /** do not use uf strong solver */ + /** do not use UF with cardinality */ UF_SS_NONE, }; diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 63f004448..f3eb88a90 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -28,7 +28,6 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_model.h" -#include "theory/uf/theory_uf_strong_solver.h" using namespace std; using namespace CVC4; diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index 35d1f82fd..3ab52a63b 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -24,9 +24,9 @@ #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" -#include "theory/uf/theory_uf_strong_solver.h" using namespace std; using namespace CVC4; @@ -90,9 +90,13 @@ void ModelEngine::check(Theory::Effort e, QEffort quant_e) } Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl; - //let the strong solver verify that the model is minimal - //for debugging, this will if there are terms in the model that the strong solver was not notified of - uf::StrongSolverTheoryUF * ufss = ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver(); + // 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; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/cardinality_extension.cpp similarity index 90% rename from src/theory/uf/theory_uf_strong_solver.cpp rename to src/theory/uf/cardinality_extension.cpp index 1bd8bb247..94e5f67c1 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_uf_strong_solver.cpp +/*! \file cardinality_extension.cpp ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King @@ -9,10 +9,10 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Implementation of theory uf strong solver class + ** \brief Implementation of theory of UF with cardinality. **/ -#include "theory/uf/theory_uf_strong_solver.h" +#include "theory/uf/cardinality_extension.h" #include "options/uf_options.h" #include "theory/uf/theory_uf.h" @@ -36,7 +36,7 @@ namespace theory { namespace uf { /* These are names are unambigious are we use abbreviations. */ -typedef StrongSolverTheoryUF::SortModel SortModel; +typedef CardinalityExtension::SortModel SortModel; typedef SortModel::Region Region; typedef Region::RegionNodeInfo RegionNodeInfo; typedef RegionNodeInfo::DiseqList DiseqList; @@ -228,7 +228,8 @@ struct sortExternalDegree { int gmcCount = 0; bool Region::getMustCombine( int cardinality ){ - if( options::ufssRegions() && d_total_diseq_external>=unsigned(cardinality) ){ + if (d_total_diseq_external >= static_cast(cardinality)) + { //The number of external disequalities is greater than or equal to //cardinality. Thus, a clique of size cardinality+1 may exist //between nodes in d_regions[i] and other regions Check if this is @@ -285,8 +286,9 @@ bool Region::check( Theory::Effort level, int cardinality, }else{ return false; } - }else if( options::ufssRegions() || options::ufssEagerSplits() || - level==Theory::EFFORT_FULL ) { + } + else if (level==Theory::EFFORT_FULL) + { //build test clique, up to size cardinality+1 if( d_testCliqueSize<=unsigned(cardinality) ){ std::vector< Node > newClique; @@ -460,7 +462,7 @@ std::string SortModel::CardinalityDecisionStrategy::identify() const SortModel::SortModel(Node n, context::Context* c, context::UserContext* u, - StrongSolverTheoryUF* thss) + CardinalityExtension* thss) : d_type(n.getType()), d_thss(thss), d_regions_index(c, 0), @@ -528,21 +530,15 @@ void SortModel::newEqClass( Node n ){ d_regions_map[n] = -1; } }else{ - if( !options::ufssRegions() ){ - // If not using regions, always add new equivalence classes - // to region index = 0. - d_regions_index = 0; - } d_regions_map[n] = d_regions_index; - Debug("uf-ss") << "StrongSolverTheoryUF: New Eq Class " << n + 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( !options::ufssRegions() || - d_regions[ d_regions_index ]->getNumReps()==0 ); + Assert(d_regions[d_regions_index]->getNumReps()==0); }else{ d_regions.push_back( new Region( this, d_thss->getSatContext() ) ); } @@ -563,10 +559,8 @@ void SortModel::merge( Node a, Node b ){ } d_regions_map[b] = -1; }else{ - //Assert( a==d_th->d_equalityEngine.getRepresentative( a ) ); - //Assert( b==d_th->d_equalityEngine.getRepresentative( b ) ); - Debug("uf-ss") << "StrongSolverTheoryUF: Merging " - << a << " = " << b << "..." << std::endl; + 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() ); @@ -620,8 +614,9 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ //do nothing }else{ //if they are not already disequal - a = d_thss->getTheory()->d_equalityEngine.getRepresentative( a ); - b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b ); + 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 ) ){ @@ -660,8 +655,8 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ } bool SortModel::areDisequal( Node a, Node b ) { - Assert( a == d_thss->getTheory()->d_equalityEngine.getRepresentative( a ) ); - Assert( b == d_thss->getTheory()->d_equalityEngine.getRepresentative( b ) ); + Assert(a == d_thss->getTheory()->getEqualityEngine()->getRepresentative(a)); + Assert(b == d_thss->getTheory()->getEqualityEngine()->getRepresentative(b)); if( d_regions_map.find( a )!=d_regions_map.end() && d_regions_map.find( b )!=d_regions_map.end() ){ int ai = d_regions_map[a]; @@ -676,14 +671,14 @@ bool SortModel::areDisequal( Node a, Node b ) { void SortModel::check( Theory::Effort level, OutputChannel* out ){ Assert( options::ufssMode()==UF_SS_FULL ); if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){ - Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl; + 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; } - //Notice() << "StrongSolverTheoryUF: Check " << level << 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 ){ @@ -713,7 +708,8 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){ if( !applyTotality( d_cardinality ) ){ //do splitting on demand bool addedLemma = false; - if( level==Theory::EFFORT_FULL || options::ufssEagerSplits() ){ + if (level==Theory::EFFORT_FULL) + { 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++ ){ @@ -835,8 +831,9 @@ void SortModel::setSplitScore( Node n, int s ){ void SortModel::assertCardinality( OutputChannel* out, int c, bool val ){ if( !d_conflict ){ Trace("uf-ss-assert") - << "Assert cardinality "<< d_type << " " << c << " " << val << " level = " - << d_thss->getTheory()->d_valuation.getAssertionLevel() << std::endl; + << "Assert cardinality " << d_type << " " << c << " " << val + << " level = " + << d_thss->getTheory()->getValuation().getAssertionLevel() << std::endl; Assert( c>0 ); Node cl = getCardinalityLiteral( c ); if( val ){ @@ -1205,22 +1202,6 @@ bool SortModel::debugModel( TheoryModel* m ){ Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard << std::endl; Trace("uf-ss-warn") << " # Reps : " << nReps << std::endl; if( d_maxNegCard>=nReps ){ - /* - for( unsigned i=0; i0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){ - rs->d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] ); - add--; - } - } - for( int i=0; imkSkolem( ss.str(), d_type, - "enumeration to meet negative card constraint" ); - d_fresh_aloc_reps.push_back( nn ); - rs->d_type_reps[d_type].push_back( nn ); - } - */ while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){ std::stringstream ss; ss << "r_" << d_type << "_"; @@ -1316,7 +1297,7 @@ Node SortModel::getCardinalityLiteral(unsigned c) return lit; } -StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, +CardinalityExtension::CardinalityExtension(context::Context* c, context::UserContext* u, OutputChannel& out, TheoryUF* th) @@ -1341,38 +1322,46 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, } } -StrongSolverTheoryUF::~StrongSolverTheoryUF() { +CardinalityExtension::~CardinalityExtension() +{ for (std::map::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it) { delete it->second; } } -SortInference* StrongSolverTheoryUF::getSortInference() { +SortInference* CardinalityExtension::getSortInference() +{ return d_th->getQuantifiersEngine()->getTheoryEngine()->getSortInference(); } /** get default sat context */ -context::Context* StrongSolverTheoryUF::getSatContext() { +context::Context* CardinalityExtension::getSatContext() +{ return d_th->getSatContext(); } /** get default output channel */ -OutputChannel& StrongSolverTheoryUF::getOutputChannel() { +OutputChannel& CardinalityExtension::getOutputChannel() +{ return d_th->getOutputChannel(); } /** ensure eqc */ -void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) { +void CardinalityExtension::ensureEqc(SortModel* c, Node a) +{ if( !hasEqc( a ) ){ d_rel_eqc[a] = true; - Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : " + << a.getType() << std::endl; c->newEqClass( a ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class." + << std::endl; } } -void StrongSolverTheoryUF::ensureEqcRec( Node n ) { +void CardinalityExtension::ensureEqcRec(Node n) +{ if( !hasEqc( n ) ){ SortModel* c = getSortModel( n ); if( c ){ @@ -1385,66 +1374,75 @@ void StrongSolverTheoryUF::ensureEqcRec( Node n ) { } /** has eqc */ -bool StrongSolverTheoryUF::hasEqc( Node a ) { +bool CardinalityExtension::hasEqc(Node a) +{ NodeBoolMap::iterator it = d_rel_eqc.find( a ); return it!=d_rel_eqc.end() && (*it).second; } /** new node */ -void StrongSolverTheoryUF::newEqClass( Node a ){ +void CardinalityExtension::newEqClass(Node a) +{ SortModel* c = getSortModel( a ); if( c ){ #ifdef LAZY_REL_EQC //do nothing #else - Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: New eq class " << a << " : " + << a.getType() << std::endl; c->newEqClass( a ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done New eq class." + << std::endl; #endif } } /** merge */ -void StrongSolverTheoryUF::merge( Node a, Node b ){ +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") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b + << " : " << a.getType() << std::endl; c->merge( a, b ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl; }else{ //c->assignEqClass( b, a ); d_rel_eqc[b] = true; } #else - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Merge " << a << " " << b << " : " << a.getType() << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Merge " << a << " " << b + << " : " << a.getType() << std::endl; c->merge( a, b ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Merge." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done Merge." << std::endl; #endif } } /** assert terms are disequal */ -void StrongSolverTheoryUF::assertDisequal( Node a, Node b, Node reason ){ +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") << "StrongSolverTheoryUF: Assert disequal " << a << " " << b << " : " << a.getType() << std::endl; - //Assert( d_th->d_equalityEngine.getRepresentative( a )==a ); - //Assert( d_th->d_equalityEngine.getRepresentative( b )==b ); + Trace("uf-ss-solver") << "CardinalityExtension: Assert disequal " << a + << " " << b << " : " << a.getType() << std::endl; c->assertDisequal( a, b, reason ); - Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done Assert disequal." << std::endl; + Trace("uf-ss-solver") << "CardinalityExtension: Done Assert disequal." + << std::endl; } } /** assert a node */ -void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ +void CardinalityExtension::assertNode(Node n, bool isDecision) +{ Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl; #ifdef LAZY_REL_EQC ensureEqcRec( n ); @@ -1542,30 +1540,33 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){ Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl; } -bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) { +bool CardinalityExtension::areDisequal(Node a, Node b) +{ if( a==b ){ return false; - }else{ - a = d_th->d_equalityEngine.getRepresentative( a ); - b = d_th->d_equalityEngine.getRepresentative( b ); - if( d_th->d_equalityEngine.areDisequal( a, b, false ) ){ - return true; - }else{ - SortModel* c = getSortModel( a ); - if( c ){ - return c->areDisequal( a, b ); - }else{ - return false; - } - } } + eq::EqualityEngine* ee = d_th->getEqualityEngine(); + a = ee->getRepresentative(a); + b = ee->getRepresentative(b); + if (ee->areDisequal(a, b, false)) + { + return true; + } + SortModel* c = getSortModel(a); + if (c) + { + return c->areDisequal(a, b); + } + return false; } /** check */ -void StrongSolverTheoryUF::check( Theory::Effort level ){ +void CardinalityExtension::check(Theory::Effort level) +{ if( !d_conflict ){ if( options::ufssMode()==UF_SS_FULL ){ - Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl; + Trace("uf-ss-solver") + << "CardinalityExtension: check " << level << std::endl; if (level == Theory::EFFORT_FULL) { if (Debug.isOn("uf-ss-debug")) @@ -1575,7 +1576,7 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ if (Trace.isOn("uf-ss-state")) { Trace("uf-ss-state") - << "StrongSolverTheoryUF::check " << level << std::endl; + << "CardinalityExtension::check " << level << std::endl; for (std::pair& rm : d_rep_model) { Trace("uf-ss-state") << " " << rm.first << " has cardinality " @@ -1626,11 +1627,13 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ // unhandled uf ss mode Assert( false ); } - Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl; + Trace("uf-ss-solver") << "Done CardinalityExtension: check " << level + << std::endl; } } -void StrongSolverTheoryUF::presolve() { +void CardinalityExtension::presolve() +{ d_initializedCombinedCardinality = false; for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->presolve(); @@ -1638,13 +1641,13 @@ void StrongSolverTheoryUF::presolve() { } } -StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy:: +CardinalityExtension::CombinedCardinalityDecisionStrategy:: CombinedCardinalityDecisionStrategy(context::Context* satContext, Valuation valuation) : DecisionStrategyFmf(satContext, valuation) { } -Node StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::mkLiteral( +Node CardinalityExtension::CombinedCardinalityDecisionStrategy::mkLiteral( unsigned i) { NodeManager* nm = NodeManager::currentNM(); @@ -1652,12 +1655,13 @@ Node StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::mkLiteral( } std::string -StrongSolverTheoryUF::CombinedCardinalityDecisionStrategy::identify() const +CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const { return std::string("uf_combined_card"); } -void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ +void CardinalityExtension::preRegisterTerm(TNode n) +{ if( options::ufssMode()==UF_SS_FULL ){ //initialize combined cardinality initializeCombinedCardinality(); @@ -1699,17 +1703,8 @@ void StrongSolverTheoryUF::preRegisterTerm( TNode n ){ } } -//void StrongSolverTheoryUF::registerQuantifier( Node f ){ -// Debug("uf-ss-register") << "Register quantifier " << f << std::endl; - //must ensure the quantifier does not quantify over arithmetic - //for( int i=0; i<(int)f[0].getNumChildren(); i++ ){ - // TypeNode tn = f[0][i].getType(); - // preRegisterType( tn, true ); - //} -//} - - -SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ +SortModel* CardinalityExtension::getSortModel(Node n) +{ TypeNode tn = n.getType(); std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn ); //pre-register the type if not done already @@ -1725,7 +1720,8 @@ SortModel* StrongSolverTheoryUF::getSortModel( Node n ){ } /** get cardinality for sort */ -int StrongSolverTheoryUF::getCardinality( Node n ) { +int CardinalityExtension::getCardinality(Node n) +{ SortModel* c = getSortModel( n ); if( c ){ return c->getCardinality(); @@ -1734,7 +1730,8 @@ int StrongSolverTheoryUF::getCardinality( Node n ) { } } -int StrongSolverTheoryUF::getCardinality( TypeNode tn ) { +int CardinalityExtension::getCardinality(TypeNode tn) +{ std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn ); if( it!=d_rep_model.end() && it->second ){ return it->second->getCardinality(); @@ -1743,20 +1740,8 @@ int StrongSolverTheoryUF::getCardinality( TypeNode tn ) { } //print debug -void StrongSolverTheoryUF::debugPrint( const char* c ){ - //EqClassesIterator< TheoryUF::NotifyClass > eqc_iter( &((TheoryUF*)d_th)->d_equalityEngine ); - //while( !eqc_iter.isFinished() ){ - // Debug( c ) << "Eq class [[" << (*eqc_iter) << "]]" << std::endl; - // EqClassIterator< TheoryUF::NotifyClass > eqc_iter2( *eqc_iter, &((TheoryUF*)d_th)->d_equalityEngine ); - // Debug( c ) << " "; - // while( !eqc_iter2.isFinished() ){ - // Debug( c ) << "[" << (*eqc_iter2) << "] "; - // eqc_iter2++; - // } - // Debug( c ) << std::endl; - // eqc_iter++; - //} - +void CardinalityExtension::debugPrint(const char* c) +{ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ Debug( c ) << "Conflict find structure for " << it->first << ": " << std::endl; it->second->debugPrint( c ); @@ -1764,7 +1749,8 @@ void StrongSolverTheoryUF::debugPrint( const char* c ){ } } -bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){ +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; @@ -1774,7 +1760,8 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){ } /** initialize */ -void StrongSolverTheoryUF::initializeCombinedCardinality() { +void CardinalityExtension::initializeCombinedCardinality() +{ if (d_cc_dec_strat.get() != nullptr && !d_initializedCombinedCardinality.get()) { @@ -1785,7 +1772,8 @@ void StrongSolverTheoryUF::initializeCombinedCardinality() { } /** check */ -void StrongSolverTheoryUF::checkCombinedCardinality() { +void CardinalityExtension::checkCombinedCardinality() +{ Assert( options::ufssMode()==UF_SS_FULL ); if( options::ufssFairness() ){ Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl; @@ -1865,13 +1853,13 @@ void StrongSolverTheoryUF::checkCombinedCardinality() { } } -StrongSolverTheoryUF::Statistics::Statistics(): - d_clique_conflicts("StrongSolverTheoryUF::Clique_Conflicts", 0), - d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0), - d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0), - d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0), - d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0), - d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1) +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); @@ -1881,7 +1869,8 @@ StrongSolverTheoryUF::Statistics::Statistics(): smtStatisticsRegistry()->registerStat(&d_max_model_size); } -StrongSolverTheoryUF::Statistics::~Statistics(){ +CardinalityExtension::Statistics::~Statistics() +{ smtStatisticsRegistry()->unregisterStat(&d_clique_conflicts); smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/cardinality_extension.h similarity index 93% rename from src/theory/uf/theory_uf_strong_solver.h rename to src/theory/uf/cardinality_extension.h index 5dac994aa..3e3d90be5 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/cardinality_extension.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_uf_strong_solver.h +/*! \file cardinality_extension.h ** \verbatim ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King @@ -9,7 +9,7 @@ ** All rights reserved. See the file COPYING in the top-level source ** directory for licensing information.\endverbatim ** - ** \brief Theory uf strong solver + ** \brief Theory of UF with cardinality. **/ #include "cvc4_private.h" @@ -19,49 +19,52 @@ #include "context/cdhashmap.h" #include "context/context.h" -#include "context/context_mm.h" #include "theory/theory.h" #include "util/statistics_registry.h" #include "theory/decision_manager.h" namespace CVC4 { + class SortInference; -namespace theory { -namespace uf { -class TheoryUF; -} /* namespace CVC4::theory::uf */ -} /* namespace CVC4::theory */ -} /* namespace CVC4 */ -namespace CVC4 { namespace theory { namespace uf { -class StrongSolverTheoryUF{ -protected: +class TheoryUF; + +/** + * This module implements a theory solver for UF with cardinality constraints. + * For high level details, see Reynolds et al "Finite Model Finding in SMT", + * CAV 2013, or Reynolds dissertation "Finite Model Finding in Satisfiability + * Modulo Theories". + */ +class CardinalityExtension +{ + protected: typedef context::CDHashMap NodeBoolMap; typedef context::CDHashMap NodeIntMap; - typedef context::CDHashMap NodeNodeMap; - typedef context::CDHashMap TypeNodeBoolMap; -public: + + public: /** * Information for incremental conflict/clique finding for a * particular sort. */ - class SortModel { - private: + class SortModel + { + private: std::map< Node, std::vector< int > > d_totality_lems; std::map< TypeNode, std::map< int, std::vector< Node > > > d_sym_break_terms; std::map< Node, int > d_sym_break_index; - public: + public: /** * A partition of the current equality graph for which cliques * can occur internally. */ - class Region { - public: + class Region + { + public: /** information stored about each node in region */ class RegionNodeInfo { public: @@ -95,7 +98,7 @@ public: context::CDO< int > d_size; NodeBoolMap d_disequalities; }; /* class DiseqList */ - public: + public: /** constructor */ RegionNodeInfo( context::Context* c ) : d_internal(c), d_external(c), d_valid(c, true) { @@ -119,7 +122,7 @@ public: DiseqList* get(unsigned i) { return d_disequalities[i]; } - private: + private: DiseqList d_internal; DiseqList d_external; context::CDO< bool > d_valid; @@ -149,7 +152,7 @@ public: //whether region is valid context::CDO< bool > d_valid; - public: + public: //constructor Region( SortModel* cf, context::Context* c ); virtual ~Region(); @@ -209,11 +212,11 @@ public: Node frontKey() const { return d_nodes.begin()->first; } }; /* class Region */ - private: + private: /** the type this model is for */ TypeNode d_type; - /** strong solver pointer */ - StrongSolverTheoryUF* d_thss; + /** Pointer to the cardinality extension that owns this. */ + CardinalityExtension* d_thss; /** regions used to d_region_index */ context::CDO< unsigned > d_regions_index; /** vector of regions */ @@ -292,9 +295,11 @@ public: bool doSendLemma( Node lem ); - public: - SortModel( Node n, context::Context* c, context::UserContext* u, - StrongSolverTheoryUF* thss ); + public: + SortModel(Node n, + context::Context* c, + context::UserContext* u, + CardinalityExtension* thss); virtual ~SortModel(); /** initialize */ void initialize( OutputChannel* out ); @@ -359,10 +364,12 @@ public: std::unique_ptr d_c_dec_strat; }; /** class SortModel */ -public: - StrongSolverTheoryUF(context::Context* c, context::UserContext* u, - OutputChannel& out, TheoryUF* th); - ~StrongSolverTheoryUF(); + public: + CardinalityExtension(context::Context* c, + context::UserContext* u, + OutputChannel& out, + TheoryUF* th); + ~CardinalityExtension(); /** get theory */ TheoryUF* getTheory() { return d_th; } /** get sort inference module */ @@ -388,7 +395,7 @@ public: /** preregister a term */ void preRegisterTerm( TNode n ); /** identify */ - std::string identify() const { return std::string("StrongSolverTheoryUF"); } + std::string identify() const { return std::string("CardinalityExtension"); } //print debug void debugPrint( const char* c ); /** debug a model */ @@ -428,7 +435,7 @@ public: /** ensure eqc for all subterms of n */ void ensureEqcRec(Node n); - /** The output channel for the strong solver. */ + /** The output channel used by this class. */ OutputChannel* d_out; /** theory uf pointer */ TheoryUF* d_th; @@ -469,8 +476,7 @@ public: context::CDO d_min_pos_tn_master_card; /** relevant eqc */ NodeBoolMap d_rel_eqc; -}; /* class StrongSolverTheoryUF */ - +}; /* class CardinalityExtension */ }/* CVC4::theory namespace::uf */ }/* CVC4::theory namespace */ diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index 3e321bf29..32d32b479 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -242,7 +242,7 @@ EqualityNodeId EqualityEngine::newNode(TNode node) { Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl; - // notify e.g. the UF theory strong solver + // notify e.g. the theory that owns this equality engine. if (d_performNotify) { d_notify.eqNotifyNewClass(node); } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7ea3f8370..6284ae31e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -29,9 +29,9 @@ #include "proof/uf_proof.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" +#include "theory/uf/cardinality_extension.h" #include "theory/uf/ho_extension.h" #include "theory/uf/theory_uf_rewriter.h" -#include "theory/uf/theory_uf_strong_solver.h" using namespace std; @@ -81,7 +81,7 @@ void TheoryUF::finishInit() { if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind() && options::ufssMode() != UF_SS_NONE) { - d_thss.reset(new StrongSolverTheoryUF( + d_thss.reset(new CardinalityExtension( getSatContext(), getUserContext(), *d_out, this)); } if (options::ufHo()) diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 248f46900..dd69b2ee2 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -33,13 +33,11 @@ namespace CVC4 { namespace theory { namespace uf { -class UfTermDb; -class StrongSolverTheoryUF; +class CardinalityExtension; class HoExtension; class TheoryUF : public Theory { - friend class StrongSolverTheoryUF; typedef context::CDHashSet NodeSet; typedef context::CDHashMap NodeNodeMap; public: @@ -120,8 +118,8 @@ private: /** The notify class */ NotifyClass d_notify; - /** The associated theory strong solver (or nullptr if it does not exist) */ - std::unique_ptr d_thss; + /** The associated cardinality extension (or nullptr if it does not exist) */ + std::unique_ptr d_thss; /** the higher-order solver extension (or nullptr if it does not exist) */ std::unique_ptr d_ho; @@ -218,8 +216,8 @@ private: eq::EqualityEngine* getEqualityEngine() override { return &d_equalityEngine; } - /** get a pointer to the strong solver (uf with cardinality) */ - StrongSolverTheoryUF* getStrongSolver() const { return d_thss.get(); } + /** get a pointer to the uf with cardinality */ + CardinalityExtension* getCardinalityExtension() const { return d_thss.get(); } /** are we in conflict? */ bool inConflict() const { return d_conflict; } -- 2.30.2