diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-10-02 14:22:36 -0500 |
---|---|---|
committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-10-03 10:55:14 -0500 |
commit | b663c658c80cee918afe37222e62dd1e5db33f5c (patch) | |
tree | 0d440c65b6454b03a4e1f4820ed3e34623edc870 /src/theory | |
parent | 8f29e55e2d508872234fe811bccf68ffc235d5a4 (diff) |
Added support for converting unsorted problems to multi-sorted problems via sort inference and monotonicity. Minor cleanup.
Diffstat (limited to 'src/theory')
-rwxr-xr-x | src/theory/quantifiers_engine.cpp | 26 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 2 |
2 files changed, 18 insertions, 10 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 0fe50aad6..2ae5edb39 100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -632,8 +632,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, return r; }else{ int sortId = 0; - if( optInternalRepSortInference() ){ - //if( options::ufssSymBreak() ){ + if( optInternalRepSortInference() && !f.isNull() ){ sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( f, f[0][index] ); } if( d_int_rep[sortId].find( r )==d_int_rep[sortId].end() ){ @@ -646,12 +645,20 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, }else{ std::vector< Node > eqc; getEquivalenceClass( r, eqc ); + Trace("internal-rep-select") << "Choose representative for equivalence class : { "; + for( unsigned i=0; i<eqc.size(); i++ ){ + if( i>0 ) Trace("internal-rep-select") << ", "; + Trace("internal-rep-select") << eqc[i]; + } + Trace("internal-rep-select") << " } " << std::endl; int r_best_score = -1; for( size_t i=0; i<eqc.size(); i++ ){ - int score = getRepScore( eqc[i], f, index ); + //if cbqi is active, do not choose instantiation constant terms if( !options::cbqi() || !quantifiers::TermDb::hasInstConstAttr(eqc[i]) ){ - if( optInternalRepSortInference() ){ - int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i]); + int score = getRepScore( eqc[i], f, index ); + //base it on sort information as well + if( sortId!=0 ){ + int e_sortId = d_qe->getTheoryEngine()->getSortInference()->getSortId( eqc[i] ); if( score>=0 && e_sortId!=sortId ){ score += 100; } @@ -661,12 +668,12 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, r_best = eqc[i]; r_best_score = score; } - } + } } if( r_best.isNull() ){ - Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); - r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); - } + Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, index ); + r_best = d_qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); + } //now, make sure that no other member of the class is an instance if( !optInternalRepSortInference() ){ r_best = getInstance( r_best, eqc ); @@ -675,6 +682,7 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f, if( d_rep_score.find( r_best )==d_rep_score.end() ){ d_rep_score[ r_best ] = d_reset_count; } + Trace("internal-rep-select") << "...Choose " << r_best << std::endl; } d_int_rep[sortId][r] = r_best; if( r_best!=a ){ diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 163dd3c1f..8c85e4dd2 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1152,7 +1152,7 @@ void StrongSolverTheoryUF::SortModel::addCliqueLemma( std::vector< Node >& cliqu clique.pop_back(); } //debugging information - if( options::ufssSymBreak() ){ + if( Trace.isOn("uf-ss-cliques") ){ std::vector< Node > clique_vec; clique_vec.insert( clique_vec.begin(), clique.begin(), clique.end() ); addClique( d_cardinality, clique_vec ); |