diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-08 17:16:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-07-08 17:16:50 -0500 |
commit | 77db9e59b783667149c2a71b730e26fe74084073 (patch) | |
tree | 21b2f657b747004a27aa66165a555f72a128f40e /src/theory/uf | |
parent | 1e71ddfb9ac9e368c9f99d351ae7954fb502663e (diff) |
Towards refactoring relations (#3078)
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 18 |
1 files changed, 16 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index a21edd8eb..1bd8bb247 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1566,8 +1566,22 @@ void StrongSolverTheoryUF::check( Theory::Effort level ){ if( !d_conflict ){ if( options::ufssMode()==UF_SS_FULL ){ Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl; - if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){ - debugPrint( "uf-ss-debug" ); + if (level == Theory::EFFORT_FULL) + { + if (Debug.isOn("uf-ss-debug")) + { + debugPrint("uf-ss-debug"); + } + if (Trace.isOn("uf-ss-state")) + { + Trace("uf-ss-state") + << "StrongSolverTheoryUF::check " << level << std::endl; + for (std::pair<const TypeNode, SortModel*>& rm : d_rep_model) + { + Trace("uf-ss-state") << " " << rm.first << " has cardinality " + << rm.second->getCardinality() << std::endl; + } + } } for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ it->second->check( level, d_out ); |