diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:27:08 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-12 18:27:08 -0700 |
| commit | 837a765cc49b0d36025ce9f2366c3f23fd2861e8 (patch) | |
| tree | db5de920e2c72daf5e21b5bce6a8e1cfe4026a76 | |
| parent | a89a37157195e4475ad0d608f283c6faccaa5d84 (diff) | |
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index d94e36d3c..b8dae3086 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -389,13 +389,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // y = "" Node cond1 = nm->mkNode(kind::STRING_PREFIX, y, x); - cond1 = y.eqNode(nm->mkConst(CVC4::String(""))); + // cond1 = y.eqNode(nm->mkConst(CVC4::String(""))); // rpw = str.++( z, x ) Node c1 = nm->mkNode(kind::AND, nm->mkNode(kind::EQUAL, x, nm->mkNode(kind::STRING_CONCAT, y,rp2)), nm->mkNode(kind::EQUAL, rpw, nm->mkNode(kind::STRING_CONCAT, z, rp2))); - c1 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, z, x)); + //c1 = rpw.eqNode(nm->mkNode(kind::STRING_CONCAT, z, x)); // contains( x, y ) Node cond2 = nm->mkNode(kind::STRING_STRCTN, x, y); @@ -433,7 +433,6 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { d_one))), y) .negate()); - */ c23 = nm->mkNode(kind::STRING_STRCTN, nm->mkNode( @@ -447,6 +446,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { d_one))), y) .negate(); + */ // assert: // IF y="" |