diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-30 13:54:07 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-30 11:54:07 -0700 |
commit | a6ef5fbd9ac3a6a247c6ecbcac2fc9e518be6f1c (patch) | |
tree | 43f517dbba414dd037edcf4786643e86203047a4 /src/theory/uf | |
parent | 5418990bd91dc0bdae24c10ddd1bc7ccf1c2dce2 (diff) |
Remove subsort symmetry breaking (#1807)
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 42 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 6 |
2 files changed, 4 insertions, 44 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 76cb95867..0e3f9c7a2 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -21,7 +21,6 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/theory_model.h" -#include "theory/quantifiers/symmetry_breaking.h" //#define ONE_SPLIT_REGION //#define DISABLE_QUICK_CLIQUE_CHECKS @@ -144,9 +143,6 @@ void Region::setEqual( Node a, Node b ){ if( !isDisequal( a, n, t ) ){ setDisequal( a, n, t, true ); nr->setDisequal( n, a, t, true ); - if( options::ufssSymBreak() ){ - d_cf->d_thss->getSymmetryBreaker()->assertDisequal( a, n ); - } } setDisequal( b, n, t, false ); nr->setDisequal( n, b, t, false ); @@ -608,12 +604,6 @@ void SortModel::merge( Node a, Node b ){ d_regions_map[b] = -1; } d_reps = d_reps - 1; - - if( !d_conflict ){ - if( options::ufssSymBreak() ){ - d_thss->getSymmetryBreaker()->merge(a, b); - } - } } } } @@ -659,12 +649,6 @@ void SortModel::assertDisequal( Node a, Node b, Node reason ){ checkRegion( ai ); checkRegion( bi ); } - - if( !d_conflict ){ - if( options::ufssSymBreak() ){ - d_thss->getSymmetryBreaker()->assertDisequal(a, b); - } - } } } } @@ -1508,7 +1492,8 @@ Node SortModel::getCardinalityLiteral( int c ) { StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, context::UserContext* u, - OutputChannel& out, TheoryUF* th) + OutputChannel& out, + TheoryUF* th) : d_out(&out), d_th(th), d_conflict(c, false), @@ -1518,11 +1503,8 @@ StrongSolverTheoryUF::StrongSolverTheoryUF(context::Context* c, d_min_pos_com_card(c, -1), d_card_assertions_eqv_lemma(u), d_min_pos_tn_master_card(c, -1), - d_rel_eqc(c), - d_sym_break(NULL) { - if (options::ufssSymBreak()) { - d_sym_break = new SubsortSymmetryBreaker(th->getQuantifiersEngine(), c); - } + d_rel_eqc(c) +{ } StrongSolverTheoryUF::~StrongSolverTheoryUF() { @@ -1530,9 +1512,6 @@ StrongSolverTheoryUF::~StrongSolverTheoryUF() { it != d_rep_model.end(); ++it) { delete it->second; } - if (d_sym_break) { - delete d_sym_break; - } } SortInference* StrongSolverTheoryUF::getSortInference() { @@ -1555,9 +1534,6 @@ void StrongSolverTheoryUF::ensureEqc( SortModel* c, Node a ) { d_rel_eqc[a] = true; Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; c->newEqClass( a ); - if( options::ufssSymBreak() ){ - d_sym_break->newEqClass( a ); - } Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; } } @@ -1589,9 +1565,6 @@ void StrongSolverTheoryUF::newEqClass( Node a ){ #else Trace("uf-ss-solver") << "StrongSolverTheoryUF: New eq class " << a << " : " << a.getType() << std::endl; c->newEqClass( a ); - if( options::ufssSymBreak() ){ - d_sym_break->newEqClass( a ); - } Trace("uf-ss-solver") << "StrongSolverTheoryUF: Done New eq class." << std::endl; #endif } @@ -1790,10 +1763,6 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ break; } } - //check symmetry breaker - if( !d_conflict && options::ufssSymBreak() ){ - d_sym_break->check( level ); - } }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){ if( level==Theory::EFFORT_FULL ){ // split on an equality between two equivalence classes (at most one per type) @@ -2125,7 +2094,6 @@ StrongSolverTheoryUF::Statistics::Statistics(): d_clique_lemmas("StrongSolverTheoryUF::Clique_Lemmas", 0), d_split_lemmas("StrongSolverTheoryUF::Split_Lemmas", 0), d_disamb_term_lemmas("StrongSolverTheoryUF::Disambiguate_Term_Lemmas", 0), - d_sym_break_lemmas("StrongSolverTheoryUF::Symmetry_Breaking_Lemmas", 0), d_totality_lemmas("StrongSolverTheoryUF::Totality_Lemmas", 0), d_max_model_size("StrongSolverTheoryUF::Max_Model_Size", 1) { @@ -2133,7 +2101,6 @@ StrongSolverTheoryUF::Statistics::Statistics(): smtStatisticsRegistry()->registerStat(&d_clique_lemmas); smtStatisticsRegistry()->registerStat(&d_split_lemmas); smtStatisticsRegistry()->registerStat(&d_disamb_term_lemmas); - smtStatisticsRegistry()->registerStat(&d_sym_break_lemmas); smtStatisticsRegistry()->registerStat(&d_totality_lemmas); smtStatisticsRegistry()->registerStat(&d_max_model_size); } @@ -2143,7 +2110,6 @@ StrongSolverTheoryUF::Statistics::~Statistics(){ smtStatisticsRegistry()->unregisterStat(&d_clique_lemmas); smtStatisticsRegistry()->unregisterStat(&d_split_lemmas); smtStatisticsRegistry()->unregisterStat(&d_disamb_term_lemmas); - smtStatisticsRegistry()->unregisterStat(&d_sym_break_lemmas); smtStatisticsRegistry()->unregisterStat(&d_totality_lemmas); smtStatisticsRegistry()->unregisterStat(&d_max_model_size); } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index f634a493c..ecbfd9a87 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -26,7 +26,6 @@ namespace CVC4 { class SortInference; namespace theory { -class SubsortSymmetryBreaker; namespace uf { class TheoryUF; } /* namespace CVC4::theory::uf */ @@ -370,8 +369,6 @@ public: ~StrongSolverTheoryUF(); /** get theory */ TheoryUF* getTheory() { return d_th; } - /** symmetry breaker */ - SubsortSymmetryBreaker* getSymmetryBreaker() { return d_sym_break; } /** get sort inference module */ SortInference* getSortInference(); /** get default sat context */ @@ -421,7 +418,6 @@ public: IntStat d_clique_lemmas; IntStat d_split_lemmas; IntStat d_disamb_term_lemmas; - IntStat d_sym_break_lemmas; IntStat d_totality_lemmas; IntStat d_max_model_size; Statistics(); @@ -468,8 +464,6 @@ public: context::CDO<int> d_min_pos_tn_master_card; /** relevant eqc */ NodeBoolMap d_rel_eqc; - /** symmetry breaking techniques */ - SubsortSymmetryBreaker* d_sym_break; }; /* class StrongSolverTheoryUF */ |