diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-09-12 18:35:57 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-09-12 18:35:57 -0500 |
| commit | f62cb035e728c77facc94c5dfe3a8a2df65aa3a7 (patch) | |
| tree | 20e8c8bdb3d89951596290c437266175bb30852b /src/theory/uf/theory_uf.cpp | |
| parent | a117e2b45539a822aa480b90558c2c0da6031dd9 (diff) | |
Rename UF with cardinality extension (#3241)
Diffstat (limited to 'src/theory/uf/theory_uf.cpp')
| -rw-r--r-- | src/theory/uf/theory_uf.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 7ea3f8370..6284ae31e 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -29,9 +29,9 @@ #include "proof/uf_proof.h" #include "theory/theory_model.h" #include "theory/type_enumerator.h" +#include "theory/uf/cardinality_extension.h" #include "theory/uf/ho_extension.h" #include "theory/uf/theory_uf_rewriter.h" -#include "theory/uf/theory_uf_strong_solver.h" using namespace std; @@ -81,7 +81,7 @@ void TheoryUF::finishInit() { if (getLogicInfo().isTheoryEnabled(THEORY_UF) && options::finiteModelFind() && options::ufssMode() != UF_SS_NONE) { - d_thss.reset(new StrongSolverTheoryUF( + d_thss.reset(new CardinalityExtension( getSatContext(), getUserContext(), *d_out, this)); } if (options::ufHo()) |