Fixes #8918.
{
NodeManager* nm = NodeManager::currentNM();
theory::strings::SkolemCache skc(nullptr);
- theory::strings::StringsPreprocess pp(&skc);
+ theory::strings::StringsPreprocess pp(d_env, &skc);
for (size_t i = 0, nasserts = assertionsToPreprocess->size(); i < nasserts;
++i)
{
d_csolver(cs),
d_extt(et),
d_statistics(statistics),
- d_preproc(d_termReg.getSkolemCache(), &statistics.d_reductions),
+ d_preproc(env, d_termReg.getSkolemCache(), &statistics.d_reductions),
d_hasExtf(context(), false),
d_extfInferCache(context()),
d_reduced(userContext())
// we do not use optimizations
SkolemCache skc(nullptr);
std::vector<Node> conj;
- ret = StringsPreprocess::reduce(t, conj, &skc);
+ ret = StringsPreprocess::reduce(t, conj, &skc, d_alphaCard);
conj.push_back(t.eqNode(ret));
ret = nm->mkAnd(conj);
}
namespace theory {
namespace strings {
-StringsPreprocess::StringsPreprocess(SkolemCache* sc,
+StringsPreprocess::StringsPreprocess(Env& env,
+ SkolemCache* sc,
HistogramStat<Kind>* statReductions)
- : d_sc(sc), d_statReductions(statReductions)
+ : EnvObj(env), d_sc(sc), d_statReductions(statReductions)
{
}
Node StringsPreprocess::reduce(Node t,
std::vector<Node>& asserts,
- SkolemCache* sc)
+ SkolemCache* sc,
+ size_t alphaCard)
{
Trace("strings-preprocess-debug")
<< "StringsPreprocess::reduce: " << t << std::endl;
Node b12 = nm->mkNode(STRING_LENGTH, sk1).eqNode(n);
Node lsk2 = nm->mkNode(STRING_LENGTH, sk2);
Node b13 = nm->mkNode(EQUAL, lsk2, nm->mkNode(SUB, lt0, t12));
- Node b1 = nm->mkNode(AND, b11, b12, b13);
+ std::vector<Node> bchildren { b11, b12, b13 };
+ if (s.getType().isString())
+ {
+ Node crange = utils::mkCodeRange(skt, alphaCard);
+ bchildren.push_back(crange);
+ }
+ Node b1 = nm->mkNode(AND, bchildren);
// the lemma for `seq.nth`
Node lemma = nm->mkNode(IMPLIES, cond, b1);
// IMPLIES: s = sk1 ++ unit(skt) ++ sk2 AND
// len( sk1 ) = n AND
// len( sk2 ) = len( s )- (n+1)
+ // We also ensure skt is a valid code point if s is of type String
asserts.push_back(lemma);
retNode = skt;
}
{
size_t prev_asserts = asserts.size();
// call the static reduce routine
- Node retNode = reduce(t, asserts, d_sc);
+ Node retNode = reduce(t, asserts, d_sc, options().strings.stringsAlphaCard);
if( t!=retNode ){
Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << " -> " << retNode << std::endl;
if (!asserts.empty())
#define CVC5__THEORY__STRINGS__PREPROCESS_H
#include <vector>
+
#include "context/cdhashmap.h"
+#include "smt/env_obj.h"
#include "theory/rewriter.h"
#include "theory/strings/sequences_stats.h"
#include "theory/strings/skolem_cache.h"
* used for reducing extended functions on-demand during the "extended function
* reductions" inference schema of TheoryStrings.
*/
-class StringsPreprocess {
+class StringsPreprocess : protected EnvObj
+{
public:
- StringsPreprocess(SkolemCache* sc,
+ StringsPreprocess(Env& env,
+ SkolemCache* sc,
HistogramStat<Kind>* statReductions = nullptr);
~StringsPreprocess();
/** The reduce routine
* @param asserts The vector for storing the assertions that correspond to
* the reduction of t,
* @param sc The skolem cache for generating new variables,
+ * @param alphaCard The cardinality of the alphabet
* @return The reduced form of t.
*/
- static Node reduce(Node t, std::vector<Node>& asserts, SkolemCache* sc);
+ static Node reduce(Node t,
+ std::vector<Node>& asserts,
+ SkolemCache* sc,
+ size_t alphaCard);
/**
* Calls the above method for the skolem cache owned by this class, and
* records statistics.
regress1/strings/issue8890-inj-oob.smt2
regress1/strings/issue8906-oob-exp.smt2
regress1/strings/issue8915-str-unit-model.smt2
+ regress1/strings/issue8918-str-nth-crange-red.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
regress1/strings/loop003.smt2
--- /dev/null
+; COMMAND-LINE: --strings-exp --no-strings-lazy-pp
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (<= (str.to_int (str.++ "0" (str.from_int (ite (str.prefixof "-" (str.at a 2)) 0 (str.to_int (str.at a 2)))))) (- 1)))
+(check-sat)