From c5d7d5b40e79041638d7b26cc63b3c0953411152 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 20 Dec 2018 06:08:49 +0000 Subject: indexof splitting --- src/theory/quantifiers/fmf/bounded_integers.cpp | 2 +- src/theory/strings/theory_strings.cpp | 7 +++++++ 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index ef6926bcb..cafa4a749 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -275,7 +275,7 @@ void BoundedIntegers::process( Node q, Node n, bool pol, bool BoundedIntegers::needsCheck(Theory::Effort e) { - return e == Theory::EFFORT_FULL; + return e == Theory::EFFORT_LAST_CALL; } void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 71a0ef63a..d6d137eb7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -3891,6 +3891,13 @@ 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 lem = nm->mkNode(OR, nm->mkNode(EQUAL, n, d_neg_one), nm->mkNode(GEQ, n, n[2])); + Trace("strings-lemma") << "Strings::Lemma STRIDOF : " << lem << std::endl; + Trace("strings-assert") << "(assert " << lem << ")" << std::endl; + d_out->lemma(lem); + } } void TheoryStrings::sendInternalInference(std::vector& exp, -- cgit v1.2.3