From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Feb 2018 17:18:40 +0000 (-0600)
Subject: Fix cd-simplification for strings (#1624)
X-Git-Tag: cvc5-1.0.0~5271
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86ce6eefaafe0f301feea38276bb364c072c71f0;p=cvc5.git

Fix cd-simplification for strings (#1624)
---

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6df2a1fdf..17551b528 100644
--- 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 400ee7cff..493cd5b6d 100644
--- 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
index 000000000..0800592d6
--- /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