diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-19 17:09:19 -0600 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-11-19 17:09:19 -0600 |
commit | f806a8eedf01753116c225b4c1a5e29543fda370 (patch) | |
tree | d432b4fb11c8a212fd6090687561f581c29fbefc | |
parent | 09a2f1a01f5cf807112bc31d5f79f5f73e026b03 (diff) |
Bug fix for previous commit
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 5f63fa8df..dab105d20 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1648,16 +1648,18 @@ void StrongSolverTheoryUF::propagate( Theory::Effort level ){ /** get next decision request */ Node StrongSolverTheoryUF::getNextDecisionRequest(){ //request the combined cardinality as a decision literal, if not already asserted - int comCard = 0; - Node com_lit; - do { - com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null(); - if( d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){ - Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl; - return com_lit; - } - comCard++; - }while( !com_lit.isNull() ); + if( options::ufssFairness() ){ + int comCard = 0; + Node com_lit; + do { + com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null(); + if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){ + Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl; + return com_lit; + } + comCard++; + }while( !com_lit.isNull() ); + } //otherwise, check each individual sort for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ Node n = it->second->getNextDecisionRequest(); |