diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 18:09:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-20 18:09:27 -0500 |
| commit | 0e62e42f739e467f61f5c3d10e7b1c7356db6406 (patch) | |
| tree | a4281c5b2c0881c2d622da68322e213f7168801b /src/theory/strings/base_solver.cpp | |
| parent | 0a0cee14c38cac0f87772c192ef387dcd36b6977 (diff) | |
Generalize mkConcat for types (#4123)
Towards theory of sequences.
The utility function mkConcat needs a type to know what to construct in the empty string case.
Diffstat (limited to 'src/theory/strings/base_solver.cpp')
| -rw-r--r-- | src/theory/strings/base_solver.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp index 6958d2528..128893cf0 100644 --- a/src/theory/strings/base_solver.cpp +++ b/src/theory/strings/base_solver.cpp @@ -35,6 +35,7 @@ BaseSolver::BaseSolver(context::Context* c, d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String("")); d_false = NodeManager::currentNM()->mkConst(false); d_cardSize = utils::getAlphabetCardinality(); + d_type = NodeManager::currentNM()->stringType(); } BaseSolver::~BaseSolver() {} @@ -253,7 +254,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti, if (!n.isNull()) { // construct the constant - Node c = utils::mkNConcat(vecc); + Node c = utils::mkNConcat(vecc, d_type); if (!d_state.areEqual(n, c)) { if (Trace.isOn("strings-debug")) |