diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 13:04:14 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2020-05-15 13:04:14 -0500 |
| commit | bf148a0efc2a14bed1cdd98248600dd1f896ee33 (patch) | |
| tree | 3889960c984565b9fe0b44a8840d37e40d6e6277 | |
| parent | 069066cff8b458f23a8b3472b2acff38664d76c7 (diff) | |
Do VSplit length conclusion
| -rw-r--r-- | src/theory/strings/core_solver.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp index a95c9b5f7..a97ca0edf 100644 --- a/src/theory/strings/core_solver.cpp +++ b/src/theory/strings/core_solver.cpp @@ -769,7 +769,6 @@ Node CoreSolver::getConclusion(Node x, // eq2 = nm->mkNode(AND, eq2, nm->mkNode(GEQ, sk2, d_one)); conc = nm->mkNode(OR, eq1, eq2); } - /* if (options::stringUnifiedVSpt()) { // we can assume its length is greater than zero @@ -777,7 +776,6 @@ Node CoreSolver::getConclusion(Node x, conc = nm->mkNode(AND, conc, sk1.eqNode(emp).negate(), nm->mkNode(GT,nm->mkNode(STRING_LENGTH,sk1), nm->mkConst(Rational(0)))); } - */ } else if (rule==PfRule::CONCAT_CSPLIT) { @@ -1640,7 +1638,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi, if (options::stringUnifiedVSpt()) { Assert(newSkolems.size() == 1); - iinfo.d_new_skolem[LENGTH_GEQ_ONE].push_back(newSkolems[0]); + iinfo.d_new_skolem[LENGTH_IGNORE].push_back(newSkolems[0]); } } else if (lentTestSuccess == 0) |