From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 28 Apr 2020 20:10:16 +0000 (-0700)
Subject: Register lower bound for str.to_int (#4408)
X-Git-Tag: cvc5-1.0.0~3332
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ad0b69e6a6242c2c7a2d060ff70ddd78861ca50a;p=cvc5.git

Register lower bound for str.to_int (#4408)

This commit changes the term registration for str.to_int terms. Before, we were not sending out any lemmas when registering str.to_int terms. Now, we send a simple lemma that asserts that the value is greater or equal to negative one.
---

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 4f1e41ebb..3d898b40b 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -225,6 +225,10 @@ void TermRegistry::registerTerm(Node n, int effort)
                             nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
                             nm->mkNode(LEQ, n, len));
   }
+  else if (n.getKind() == STRING_STOI)
+  {
+    regTermLem = nm->mkNode(GEQ, n, nm->mkConst(Rational(-1)));
+  }
   if (!regTermLem.isNull())
   {
     Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem