summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/strings/theory_strings.cpp19
-rw-r--r--src/theory/strings/theory_strings_utils.cpp5
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress2/strings/cmi-split-cm-fail.smt212
4 files changed, 35 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9e14d6a3f..5b7c38361 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -264,6 +264,9 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m)
// assert the (relevant) portion of the equality engine to the model
if (!m->assertEqualityEngine(&d_equalityEngine, &termSet))
{
+ Unreachable()
+ << "TheoryStrings::collectModelInfo: failed to assert equality engine"
+ << std::endl;
return false;
}
@@ -423,6 +426,8 @@ bool TheoryStrings::collectModelInfoType(
uint32_t currLen =
lts_values[i].getConst<Rational>().getNumerator().toUnsignedInt();
std::unique_ptr<SEnumLen> sel;
+ Trace("strings-model") << "Cardinality of alphabet is "
+ << utils::getAlphabetCardinality() << std::endl;
if (tn.isString())
{
sel.reset(new StringEnumLen(
@@ -474,7 +479,10 @@ bool TheoryStrings::collectModelInfoType(
Node spl = nm->mkNode(OR, sl, sl.negate());
++(d_statistics.d_lemmasCmiSplit);
d_out->lemma(spl);
+ Trace("strings-lemma")
+ << "Strings::CollectModelInfoSplit: " << spl << std::endl;
}
+ // we added a lemma, so can return here
return false;
}
c = sel->getCurrent();
@@ -491,6 +499,11 @@ bool TheoryStrings::collectModelInfoType(
processed[eqc] = c;
if (!m->assertEquality(eqc, c, true))
{
+ // this should never happen due to the model soundness argument
+ // for strings
+ Unreachable()
+ << "TheoryStrings::collectModelInfoType: Inconsistent equality"
+ << std::endl;
return false;
}
}
@@ -534,6 +547,12 @@ bool TheoryStrings::collectModelInfoType(
processed[nodes[i]] = cc;
if (!m->assertEquality(nodes[i], cc, true))
{
+ // this should never happen due to the model soundness argument
+ // for strings
+
+ Unreachable() << "TheoryStrings::collectModelInfoType: "
+ "Inconsistent equality (unprocessed eqc)"
+ << std::endl;
return false;
}
}
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index b2a62cc62..b64a0df01 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -36,8 +36,9 @@ uint32_t getAlphabetCardinality()
Assert(128 <= String::num_codes());
return 128;
}
- Assert(256 <= String::num_codes());
- return 256;
+ // 3*16^4 = 196608 values in the SMT-LIB standard for Unicode strings
+ Assert(196608 <= String::num_codes());
+ return 196608;
}
Node mkAnd(const std::vector<Node>& a)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 935a4694f..656bb5880 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2050,6 +2050,7 @@ set(regress_2_tests
regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
regress2/quantifiers/syn874-1.smt2
regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
+ regress2/strings/cmi-split-cm-fail.smt2
regress2/strings/cmu-dis-0707-3.smt2
regress2/strings/cmu-disagree-0707-dd.smt2
regress2/strings/cmu-prereg-fmf.smt2
diff --git a/test/regress/regress2/strings/cmi-split-cm-fail.smt2 b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
new file mode 100644
index 000000000..e2ae94a27
--- /dev/null
+++ b/test/regress/regress2/strings/cmi-split-cm-fail.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --strings-exp --rewrite-divk
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_SLIA)
+(set-info :status sat)
+
+(declare-fun s () String)
+
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (not (= (str.at s 0) (str.at s 1))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 2) (str.at s 6))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 7))) 1 0) 0)))) (not (= (ite (not (= (str.at s 2) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 1) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 1) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 1) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 3))) 1 0) 0)))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 3) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 3) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 1) (str.at s 2))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 2) (str.at s 7))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 2) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 2) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 2) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 2) (str.at s 3))) 1 0) 0)))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (not (= (ite (not (= (str.at s 3) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 3) (str.at s 6))) 1 0) 0)))) (not (= (ite (not (= (str.at s 3) (str.at s 5))) 1 0) 0))) (not (= (ite (not (= (str.at s 3) (str.at s 4))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 4) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (not (= (str.at s 4) (str.at s 5))) 1 0) 0)))) (not (= (ite (not (= (str.at s 5) (str.at s 7))) 1 0) 0))) (not (= (ite (not (= (str.at s 5) (str.at s 6))) 1 0) 0))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (not (= (str.at s 6) (str.at s 7))) 1 0) 0)))) (not (= (ite (<= (str.len s) 8) 1 0) 0))) (not (= (ite (= (str.len s) 8) 1 0) 0))) (not (not (= (ite (<= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (= (str.len s) 7) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (= (str.len s) 6) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (= (str.len s) 5) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (= (str.len s) 4) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (= (str.len s) 3) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 2) 1 0) 0)))) (not (not (= (ite (= (str.len s) 2) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 1) 1 0) 0)))) (not (not (= (ite (= (str.len s) 1) 1 0) 0)))) (not (not (= (ite (<= (str.len s) 0) 1 0) 0)))) (not (not (= (ite (= (str.len s) 0) 1 0) 0)))))
+
+(check-sat)
+(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback