diff options
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 2 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.cpp | 4 | ||||
-rw-r--r-- | src/theory/uf/theory_uf_strong_solver.h | 2 |
4 files changed, 7 insertions, 5 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index ae935798e..4cdc5e240 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -205,9 +205,9 @@ void TheoryUF::propagate(Effort effort) { //} } -Node TheoryUF::getNextDecisionRequest(){ +Node TheoryUF::getNextDecisionRequest( unsigned& priority ){ if (d_thss != NULL && !d_conflict) { - return d_thss->getNextDecisionRequest(); + return d_thss->getNextDecisionRequest( priority ); }else{ return Node::null(); } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 3a83decec..0900b4c90 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -194,7 +194,7 @@ public: void computeCareGraph(); void propagate(Effort effort); - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); EqualityStatus getEqualityStatus(TNode a, TNode b); diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp index 4713c7dcf..edb92bb1b 100644 --- a/src/theory/uf/theory_uf_strong_solver.cpp +++ b/src/theory/uf/theory_uf_strong_solver.cpp @@ -1962,7 +1962,7 @@ void StrongSolverTheoryUF::propagate( Theory::Effort level ){ } /** get next decision request */ -Node StrongSolverTheoryUF::getNextDecisionRequest(){ +Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){ //request the combined cardinality as a decision literal, if not already asserted if( options::ufssFairness() ){ int comCard = 0; @@ -1972,6 +1972,7 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){ 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; + priority = 1; return com_lit; } comCard++; @@ -1984,6 +1985,7 @@ Node StrongSolverTheoryUF::getNextDecisionRequest(){ for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){ Node n = it->second->getNextDecisionRequest(); if( !n.isNull() ){ + priority = 1; return n; } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 40026522d..4130a7d41 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -399,7 +399,7 @@ public: /** propagate */ void propagate( Theory::Effort level ); /** get next decision request */ - Node getNextDecisionRequest(); + Node getNextDecisionRequest( unsigned& priority ); /** preregister a term */ void preRegisterTerm( TNode n ); /** notify restart */ |