Add priorities to getNextDecision. Properly handle case for finite types + unbounded heaps in sep logic. Fix another simple memory leak in sygus.

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 */