Decision strategy: incorporate UF with cardinality constraints (#2476)

1 files changed, 6 insertions, 10 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 653b89d7b..3e9e2354d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -79,8 +79,12 @@ void TheoryUF::finishInit() {
   TheoryModel* tm = d_valuation.getModel();
   Assert(tm != nullptr);
   tm->setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT);
-  // initialize the strong solver
-  if (options::finiteModelFind() && options::ufssMode()!=UF_SS_NONE) {
+  // Initialize the cardinality constraints solver if the logic includes UF,
+  // finite model finding is enabled, and it is not disabled by
+  // options::ufssMode().
+  if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind()
+      && options::ufssMode() != UF_SS_NONE)
+  {
     d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this);
   }
 }
@@ -296,14 +300,6 @@ void TheoryUF::propagate(Effort effort) {
   //}
 }
 
-Node TheoryUF::getNextDecisionRequest( unsigned& priority ){
-  if (d_thss != NULL && !d_conflict) {
-    return d_thss->getNextDecisionRequest( priority );
-  }else{
-    return Node::null();
-  }
-}
-
 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;