diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 9 |
2 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index e60e67ac1..e73cf5e9d 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2846,12 +2846,16 @@ bool TheoryStrings::checkNegContains() { } } else if(!areDisequal(lenx, lens)) { if(d_neg_ctn_ulen.find(atom) == d_neg_ctn_ulen.end()) { + lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); + lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); d_neg_ctn_ulen.insert( atom ); sendSplit(lenx, lens, "NEG-CTN-SP"); addedLemma = true; } } else { if(d_neg_ctn_cached.find(atom) == d_neg_ctn_cached.end()) { + lenx = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x); + lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s); Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType()); Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1); Node g1 = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode( kind::GEQ, b1, d_zero ), diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 0cccdf0ef..be419a36a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -482,9 +482,14 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node cond = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, x, y ); Node c1 = x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, y, sk2 ) ); Node c2 = skw.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, z, sk2 ) ); - //Node c3 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, sk1, y ).negate(); + Node c3 = NodeManager::currentNM()->mkNode(kind::STRING_STRCTN, + NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1, + NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, y, d_zero, + NodeManager::currentNM()->mkNode(kind::MINUS, + NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), + NodeManager::currentNM()->mkConst(::CVC4::Rational(1))))), y).negate(); Node rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, - NodeManager::currentNM()->mkNode( kind::AND, c1, c2), // c3 + NodeManager::currentNM()->mkNode( kind::AND, c1, c2, c3), skw.eqNode(x) ) ); new_nodes.push_back( rr ); rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) ); |