Better heuristic for str.code/re.range (#3220)

To make sure that our `str.code` function is injectve (except for -1 in
the codomain), we send the inference that `str.code(x) == -1 v
str.code(x) != str.code(y) v x == y` for each pair of `str.code` terms.
Because of the order of disjuncts, `str.code(x) != str.code(y)` was
usually assigned true. This in turn lead to a difficult problem for the
arithmetic engine if there were more `str.code` applications than the
size of the domain. E.g. if we had `0 <= str.code(xi) < 10` for 0 <= i
<= 10, then the arithmetic engine had a difficult time finding a
conflict. This PR improves the heuristic by setting the phase of
`str.code(x) != str.code(y)` to false, so we prefer to keep the
`str.code` values equal instead of trying to make them different.

This change is also reflected in the models produced for inputs
involving `str.code`: Previously, we were producing models with
different values for the `str.code` whereas now the models are much more
uniform.

The PR adds two regressions, one testing `str.code` performance directly
and one testing it for `str.code` terms generated by `re.range`.

Signed-off-by: Andres Noetzli <anoetzli@amazon.com>

diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 6cc1e7b44abcfa0ad33640187f2105d213b21c3c..97f9666bd395a6663651cbdce24f3034f06419b9 100644 (file)
--- 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 2f51000abc6f2ffde6c89dbb10a5ee0d003f9c87..65f06c0083cde35f518c430dae5c3e2970081b3c 100644 (file)
--- 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 444a740eae2862f9184f496790736e8f6e7cd76c..fa7c854ea2b15716cf10f740805ce9078b843ec1 100644 (file)
--- 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 (file)
index 0000000..39cab48
--- /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 (file)
index 0000000..62ec107
--- /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)