diff options
Diffstat (limited to 'src/theory/uf/cardinality_extension.cpp')
-rw-r--r-- | src/theory/uf/cardinality_extension.cpp | 29 |
1 files changed, 19 insertions, 10 deletions
diff --git a/src/theory/uf/cardinality_extension.cpp b/src/theory/uf/cardinality_extension.cpp index 98e330df4..34952084b 100644 --- a/src/theory/uf/cardinality_extension.cpp +++ b/src/theory/uf/cardinality_extension.cpp @@ -480,7 +480,7 @@ SortModel::SortModel(Node n, { d_cardinality_term = n; - if (options::ufssMode() == UF_SS_FULL) + if (options::ufssMode() == options::UfssMode::FULL) { // Register the strategy with the decision manager of the theory. // We are guaranteed that the decision manager is ready since we @@ -671,7 +671,7 @@ bool SortModel::areDisequal( Node a, Node b ) { /** check */ void SortModel::check( Theory::Effort level, OutputChannel* out ){ - Assert(options::ufssMode() == UF_SS_FULL); + Assert(options::ufssMode() == options::UfssMode::FULL); if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){ Debug("uf-ss") << "CardinalityExtension: Check " << level << " " << d_type << std::endl; @@ -1314,7 +1314,7 @@ CardinalityExtension::CardinalityExtension(context::Context* c, d_min_pos_tn_master_card(c, -1), d_rel_eqc(c) { - if (options::ufssMode() == UF_SS_FULL && options::ufssFairness()) + if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness()) { // Register the strategy with the decision manager of the theory. // We are guaranteed that the decision manager is ready since we @@ -1451,7 +1451,8 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) #endif bool polarity = n.getKind() != kind::NOT; TNode lit = polarity ? n : n[0]; - if( options::ufssMode()==UF_SS_FULL ){ + if (options::ufssMode() == options::UfssMode::FULL) + { if( lit.getKind()==CARDINALITY_CONSTRAINT ){ TypeNode tn = lit[0].getType(); Assert(tn.isSort()); @@ -1532,7 +1533,9 @@ void CardinalityExtension::assertNode(Node n, bool isDecision) } } } - }else{ + } + else + { if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){ // cardinality constraint from user input, set incomplete Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl; @@ -1566,7 +1569,8 @@ bool CardinalityExtension::areDisequal(Node a, Node b) void CardinalityExtension::check(Theory::Effort level) { if( !d_conflict ){ - if( options::ufssMode()==UF_SS_FULL ){ + if (options::ufssMode() == options::UfssMode::FULL) + { Trace("uf-ss-solver") << "CardinalityExtension: check " << level << std::endl; if (level == Theory::EFFORT_FULL) @@ -1593,7 +1597,9 @@ void CardinalityExtension::check(Theory::Effort level) break; } } - }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){ + } + else if (options::ufssMode() == options::UfssMode::NO_MINIMAL) + { if( level==Theory::EFFORT_FULL ){ // split on an equality between two equivalence classes (at most one per type) std::map< TypeNode, std::vector< Node > > eqc_list; @@ -1625,7 +1631,9 @@ void CardinalityExtension::check(Theory::Effort level) ++eqcs_i; } } - }else{ + } + else + { // unhandled uf ss mode Assert(false); } @@ -1664,7 +1672,8 @@ CardinalityExtension::CombinedCardinalityDecisionStrategy::identify() const void CardinalityExtension::preRegisterTerm(TNode n) { - if( options::ufssMode()==UF_SS_FULL ){ + if (options::ufssMode() == options::UfssMode::FULL) + { //initialize combined cardinality initializeCombinedCardinality(); @@ -1776,7 +1785,7 @@ void CardinalityExtension::initializeCombinedCardinality() /** check */ void CardinalityExtension::checkCombinedCardinality() { - Assert(options::ufssMode() == UF_SS_FULL); + Assert(options::ufssMode() == options::UfssMode::FULL); if( options::ufssFairness() ){ Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl; int totalCombinedCard = 0; |