diff options
Diffstat (limited to 'src/theory/quantifiers/relevant_domain.cpp')
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 7b4440c31..ad6c241e7 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -83,6 +83,20 @@ void RelevantDomain::compute(){ } }while( !success ); Trace("rel-dom") << "done compute relevant domain" << std::endl; + /* + //debug printing + Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl; + if( useRelInstDomain ){ + Trace("rel-dom") << "Relevant domain : " << std::endl; + for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){ + Trace("rel-dom") << " " << i << " : "; + for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){ + Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " "; + } + Trace("rel-dom") << std::endl; + } + } + */ } bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){ |