diff options
| -rw-r--r-- | src/theory/strings/inference_manager.cpp | 1 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | test/regress/regress0/strings/code-perf.smt2 | 48 | ||||
| -rw-r--r-- | test/regress/regress2/strings/range-perf.smt2 | 7 |
5 files changed, 59 insertions, 0 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 6cc1e7b44..97f9666bd 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -274,6 +274,7 @@ bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq) void InferenceManager::sendPhaseRequirement(Node lit, bool pol) { + lit = Rewriter::rewrite(lit); d_pendingReqPhase[lit] = pol; } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2f51000ab..65f06c008 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2800,6 +2800,7 @@ void TheoryStrings::checkCodes() Node eqn = c1[0].eqNode(c2[0]); // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); + d_im.sendPhaseRequirement(deq, false); d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj"); } } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 444a740ea..fa7c854ea 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -844,6 +844,7 @@ set(regress_0_tests regress0/strings/bug002.smt2 regress0/strings/bug612.smt2 regress0/strings/bug613.smt2 + regress0/strings/code-perf.smt2 regress0/strings/code-sat-neg-one.smt2 regress0/strings/escchar.smt2 regress0/strings/escchar_25.smt2 @@ -1824,6 +1825,7 @@ set(regress_2_tests regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/norn-dis-0707-3.smt2 + regress2/strings/range-perf.smt2 regress2/strings/repl-repl.smt2 regress2/strings/replaceall-diffrange.smt2 regress2/strings/replaceall-len-c.smt2 diff --git a/test/regress/regress0/strings/code-perf.smt2 b/test/regress/regress0/strings/code-perf.smt2 new file mode 100644 index 000000000..39cab48ce --- /dev/null +++ b/test/regress/regress0/strings/code-perf.smt2 @@ -0,0 +1,48 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(declare-const x0 String) +(declare-const x1 String) +(declare-const x2 String) +(declare-const x3 String) +(declare-const x4 String) +(declare-const x5 String) +(declare-const x6 String) +(declare-const x7 String) +(declare-const x8 String) +(declare-const x9 String) +(declare-const x10 String) +(declare-const y0 Int) +(declare-const y1 Int) +(declare-const y2 Int) +(declare-const y3 Int) +(declare-const y4 Int) +(declare-const y5 Int) +(declare-const y6 Int) +(declare-const y7 Int) +(declare-const y8 Int) +(declare-const y9 Int) +(declare-const y10 Int) +(assert (and (= y0 (str.code x0)) (>= y0 (str.code "0")) (<= y0 (str.code "9")))) +(assert (and (= y1 (str.code x1)) (>= y1 (str.code "0")) (<= y1 (str.code "9")))) +(assert (and (= y2 (str.code x2)) (>= y2 (str.code "0")) (<= y2 (str.code "9")))) +(assert (and (= y3 (str.code x3)) (>= y3 (str.code "0")) (<= y3 (str.code "9")))) +(assert (and (= y4 (str.code x4)) (>= y4 (str.code "0")) (<= y4 (str.code "9")))) +(assert (and (= y5 (str.code x5)) (>= y5 (str.code "0")) (<= y5 (str.code "9")))) +(assert (and (= y6 (str.code x6)) (>= y6 (str.code "0")) (<= y6 (str.code "9")))) +(assert (and (= y7 (str.code x7)) (>= y7 (str.code "0")) (<= y7 (str.code "9")))) +(assert (and (= y8 (str.code x8)) (>= y8 (str.code "0")) (<= y8 (str.code "9")))) +(assert (and (= y9 (str.code x9)) (>= y9 (str.code "0")) (<= y9 (str.code "9")))) +(assert (and (= y10 (str.code x10)) (>= y10 (str.code "0")) (<= y10 (str.code "9")))) +(assert (= (str.len x0) 1)) +(assert (= (str.len x1) 1)) +(assert (= (str.len x2) 1)) +(assert (= (str.len x3) 1)) +(assert (= (str.len x4) 1)) +(assert (= (str.len x5) 1)) +(assert (= (str.len x6) 1)) +(assert (= (str.len x7) 1)) +(assert (= (str.len x8) 1)) +(assert (= (str.len x9) 1)) +(assert (= (str.len x10) 1)) +(check-sat) diff --git a/test/regress/regress2/strings/range-perf.smt2 b/test/regress/regress2/strings/range-perf.smt2 new file mode 100644 index 000000000..62ec10711 --- /dev/null +++ b/test/regress/regress2/strings/range-perf.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(declare-const x String) +(assert (str.in.re x (re.loop (re.range "0" "9") 12 12))) +(assert (str.in.re x (re.++ (re.* re.allchar) (str.to.re "01") (re.* re.allchar)))) +(check-sat) |