From 86094a88045847c76f54535b34730f8b9895e842 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 29 Jan 2014 12:05:02 -0600 Subject: [PATCH] roll back to uf implementation for substr and charat --- src/theory/strings/theory_strings.cpp | 23 ++++++++++++++++--- src/theory/strings/theory_strings.h | 1 + .../strings/theory_strings_rewriter.cpp | 5 +++- 3 files changed, 25 insertions(+), 4 deletions(-) diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3209a92ec..2b1bb2b63 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -62,7 +62,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); - + d_all_warning = true; d_regexp_incomplete = false; d_opt_regexp_gcd = true; @@ -1709,6 +1709,21 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { bool TheoryStrings::checkSimple() { bool addedLemma = false; + + //Initialize UF + if(d_undefSubstr.isNull()) { + std::vector< TypeNode > argTypes; + argTypes.push_back(NodeManager::currentNM()->stringType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + argTypes.push_back(NodeManager::currentNM()->integerType()); + d_undefSubstr = NodeManager::currentNM()->mkSkolem("__undefSS", + NodeManager::currentNM()->mkFunctionType( + argTypes, NodeManager::currentNM()->stringType()), + "undefined substr", + NodeManager::SKOLEM_EXACT_NAME); + } + + eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ) { Node eqc = (*eqcs_i); @@ -1760,7 +1775,8 @@ bool TheoryStrings::checkSimple() { Node len_sk1_eq_i = n[1].eqNode( NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1greq0 )); Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); - lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) ); + Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], d_one)); + lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf) ); Trace("strings-lemma") << "Strings::Lemma CHARAT : " << lemma << std::endl; d_out->lemma(lemma); } else if( n.getKind() == kind::STRING_SUBSTR ) { @@ -1778,7 +1794,8 @@ bool TheoryStrings::checkSimple() { Node lemma = NodeManager::currentNM()->mkNode( kind::AND, x_eq_123, len_sk1_eq_i ); Node cond = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, lenxgti, t1geq0, t2geq0 )); - lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::IMPLIES, cond, lemma ) ); + Node uf = sk.eqNode( NodeManager::currentNM()->mkNode(kind::APPLY_UF, d_undefSubstr, n[0], n[1], n[2])); + lemma = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::ITE, cond, lemma, uf ) ); Trace("strings-lemma") << "Strings::Lemma SUBSTR : " << lemma << std::endl; d_out->lemma(lemma); } diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d15a76aad..81748d607 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -115,6 +115,7 @@ private: Node d_false; Node d_zero; Node d_one; + Node d_undefSubstr; // Options bool d_all_warning; bool d_opt_fmf; diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7bf016d29..1dc9cbe85 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -353,7 +353,10 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } else if(node.getKind() == kind::STRING_SUBSTR) { - if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { + Node zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); + if(node[2] == zero) { + retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") ); + } else if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { int i = node[1].getConst().getNumerator().toUnsignedInt(); int j = node[2].getConst().getNumerator().toUnsignedInt(); if( node[0].getConst().size() >= (unsigned) (i + j) ) { -- 2.30.2