diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 11:20:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 11:20:50 -0500 |
commit | 079ed9540d498bcbb58f2f0fbe87bdae28101d1e (patch) | |
tree | 8c3ba1818dc515c1714b23555460a3a39192acc5 /src/theory/uf | |
parent | 03cc40cc070df0bc11c1556cef3016f784a95d23 (diff) |
Refactor theory model (#1236)
* Refactor theory model, working on making RepSet references const.
* Encapsulation of members of rep set.
* More documentation on rep set.
* Swap names
* Reference issues.
* Minor
* Minor
* New clang format.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 19 |
2 files changed, 12 insertions, 9 deletions
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 1b7437a7e..54e99cdba 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -437,7 +437,7 @@ Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* //consider finding another value, if possible Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl; TypeNode tn = defaultTerm.getType(); - Node newDefaultVal = m->getDomainValue( tn, d_values ); + Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values); if( !newDefaultVal.isNull() ){ defaultVal = newDefaultVal; Debug("fmf-model-cons-debug") << "-> Change default value to "; diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 4b6a326cf..eb9e5e987 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -851,8 +851,8 @@ bool SortModel::minimize( OutputChannel* out, TheoryModel* m ){ #if 0 // ensure that the constructed model is minimal // if the model has terms that the strong solver does not know about - if( (int)m->d_rep_set.d_type_reps[ d_type ].size()>d_cardinality ){ - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->d_equalityEngine ); + if( (int)rs->d_type_reps[ d_type ].size()>d_cardinality ){ + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &m->getEqualityEngine() ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( eqc.getType()==d_type ){ @@ -1550,7 +1550,8 @@ void SortModel::debugPrint( const char* c ){ bool SortModel::debugModel( TheoryModel* m ){ if( Trace.isOn("uf-ss-warn") ){ std::vector< Node > eqcs; - eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( m->d_equalityEngine ); + eq::EqClassesIterator eqcs_i = + eq::EqClassesIterator(m->getEqualityEngine()); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); if( eqc.getType()==d_type ){ @@ -1567,7 +1568,8 @@ bool SortModel::debugModel( TheoryModel* m ){ ++eqcs_i; } } - int nReps = m->d_rep_set.d_type_reps.find( d_type )==m->d_rep_set.d_type_reps.end() ? 0 : (int)m->d_rep_set.d_type_reps[d_type].size(); + RepSet* rs = m->getRepSetPtr(); + int nReps = (int)rs->getNumRepresentatives(d_type); if( nReps!=(d_maxNegCard+1) ){ Trace("uf-ss-warn") << "WARNING : Model does not have same # representatives as cardinality for " << d_type << "." << std::endl; Trace("uf-ss-warn") << " Max neg cardinality : " << d_maxNegCard << std::endl; @@ -1576,16 +1578,17 @@ bool SortModel::debugModel( TheoryModel* m ){ /* for( unsigned i=0; i<d_fresh_aloc_reps.size(); i++ ){ if( add>0 && !m->d_equalityEngine->hasTerm( d_fresh_aloc_reps[i] ) ){ - m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] ); + rs->d_type_reps[d_type].push_back( d_fresh_aloc_reps[i] ); add--; } } for( int i=0; i<add; i++ ){ std::stringstream ss; ss << "r_" << d_type << "_"; - Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "enumeration to meet negative card constraint" ); + Node nn = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, + "enumeration to meet negative card constraint" ); d_fresh_aloc_reps.push_back( nn ); - m->d_rep_set.d_type_reps[d_type].push_back( nn ); + rs->d_type_reps[d_type].push_back( nn ); } */ while( (int)d_fresh_aloc_reps.size()<=d_maxNegCard ){ @@ -1595,7 +1598,7 @@ bool SortModel::debugModel( TheoryModel* m ){ d_fresh_aloc_reps.push_back( nn ); } if( d_maxNegCard==0 ){ - m->d_rep_set.d_type_reps[d_type].push_back( d_fresh_aloc_reps[0] ); + rs->d_type_reps[d_type].push_back(d_fresh_aloc_reps[0]); }else{ //must add lemma std::vector< Node > force_cl; |