From 8a133e21e4b12538b39df7a2dc3c0bdc4eb7c847 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 30 Apr 2019 15:59:57 -0700 Subject: revert diff --- src/theory/strings/theory_strings.cpp | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 14216f8aa..1e50b2609 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3983,23 +3983,6 @@ void TheoryStrings::registerTerm( Node n, int effort ) { Trace("strings-assert") << "(assert " << lem << ")" << std::endl; d_out->lemma(lem); } - else if (n.getKind() == STRING_STRIDOF) - { - Node lower = n[2]; - if (!TheoryStringsRewriter::checkEntailArith(lower)) { - lower = d_zero; - } - Node neg = Rewriter::rewrite(nm->mkNode(EQUAL, n, d_neg_one)); - Node geq = Rewriter::rewrite(nm->mkNode(GEQ, n, lower)); - Node lem = nm->mkNode(OR, neg, geq); - Trace("strings-lemma") << "Strings::Lemma STRIDOF : " << lem << std::endl; - Trace("strings-assert") << "(assert " << lem << ")" << std::endl; - //d_out->lemma(lem); - //d_out->requirePhase(neg, true); - - lem = Rewriter::rewrite(nm->mkNode(GT, nm->mkNode(STRING_LENGTH, n[0]), n)); - d_out->lemma(lem); - } } bool TheoryStrings::sendInternalInference(std::vector& exp, -- cgit v1.2.3