Fix cd-simplification for strings (#1624)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6df2a1fdfb6db3b4f13be74df7090280e3820433..17551b52839654c648fa150d54f60847dfb6374c 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -1340,13 +1340,28 @@ void TheoryStrings::checkExtfEval( int effort ) {
           getExtTheory()->markReduced( n );
           Trace("strings-extf-debug") << "  resolvable by evaluation..." << std::endl;
           std::vector< Node > exps;
+          // The following optimization gets the "symbolic definition" of
+          // an extended term. The symbolic definition of a term t is a term
+          // t' where constants are replaced by their corresponding proxy
+          // variables.
+          // For example, if lsym is a proxy variable for "", then
+          // str.replace( lsym, lsym, lsym ) is the symbolic definition for
+          // str.replace( "", "", "" ). It is generally better to use symbolic
+          // definitions when doing cd-rewriting for the purpose of minimizing
+          // clauses, e.g. we infer the unit equality:
+          //    str.replace( lsym, lsym, lsym ) == ""
+          // instead of making this inference multiple times:
+          //    x = "" => str.replace( x, x, x ) == ""
+          //    y = "" => str.replace( y, y, y ) == ""
           Trace("strings-extf-debug") << "  get symbolic definition..." << std::endl;
           Node nrs = getSymbolicDefinition( sn, exps );
           if( !nrs.isNull() ){
             Trace("strings-extf-debug") << "  rewrite " << nrs << "..." << std::endl;
-            nrs = Rewriter::rewrite( nrs );
-            //ensure the symbolic form is non-trivial
-            if( nrs.isConst() ){
+            Node nrsr = Rewriter::rewrite(nrs);
+            // ensure the symbolic form is not rewritable
+            if (nrsr != nrs)
+            {
+              // we cannot use the symbolic definition if it rewrites
               Trace("strings-extf-debug") << "  symbolic definition is trivial..." << std::endl;
               nrs = Node::null();
             }

diff --git a/test/regress/regress1/strings/Makefile.am b/test/regress/regress1/strings/Makefile.am
index 400ee7cffc07679ffb1d7e8b7ee50f0fa9e8150b..493cd5b6dd91ea709c64509881f3b7c41aac83cc 100644 (file)
--- a/test/regress/regress1/strings/Makefile.am
+++ b/test/regress/regress1/strings/Makefile.am
@@ -72,7 +72,8 @@ TESTS =       \
        str001.smt2 \
        str002.smt2 \
        str007.smt2 \
-       rew-020618.smt2
+       rew-020618.smt2 \
+       double-replace.smt2
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress1/strings/double-replace.smt2 b/test/regress/regress1/strings/double-replace.smt2
new file mode 100644 (file)
index 0000000..0800592
--- /dev/null
+++ b/test/regress/regress1/strings/double-replace.smt2
@@ -0,0 +1,7 @@
+(set-logic SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (not (= (str.replace (str.replace x y x) x y) x)))
+(check-sat)
\ No newline at end of file