diff options
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 16 |
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; |