diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-26 14:35:40 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-26 14:35:40 +0200 |
commit | 51aa945e59ecf3354192f40c3f645d8b221e34a9 (patch) | |
tree | efd08ada86eaaefe42f371a6744dcf681266e6a6 /src/theory | |
parent | e61a79df77924c66e8f6ff3141172bda49301475 (diff) |
Lazy preprocessing of extended operators in strings. Add regressions. Fixes bug 613.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/options | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 42 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 3 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 53 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 2 |
5 files changed, 76 insertions, 27 deletions
diff --git a/src/theory/strings/options b/src/theory/strings/options index 596d46c54..8a839a118 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -32,4 +32,7 @@ option stringIgnNegMembership strings-inm --strings-inm bool :default false #expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 128 :read-write # the cardinality of the characters used by the theory of strings, default 128 (for standard ASCII) or 256 (for extended ASCII) +option stringLazyPreproc strings-lazy-pp --strings-lazy-pp bool :default true + perform string preprocessing lazily + endmodule diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4ac178cbd..507c74c53 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -74,10 +74,14 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu d_equalityEngine.addFunctionKind(kind::STRING_SUBSTR_TOTAL); d_equalityEngine.addFunctionKind(kind::STRING_ITOS); d_equalityEngine.addFunctionKind(kind::STRING_STOI); - //d_equalityEngine.addFunctionKind(kind::STRING_U16TOS); - //d_equalityEngine.addFunctionKind(kind::STRING_STOU16); - //d_equalityEngine.addFunctionKind(kind::STRING_U32TOS); - //d_equalityEngine.addFunctionKind(kind::STRING_STOU32); + if( options::stringLazyPreproc() ){ + d_equalityEngine.addFunctionKind(kind::STRING_U16TOS); + d_equalityEngine.addFunctionKind(kind::STRING_STOU16); + d_equalityEngine.addFunctionKind(kind::STRING_U32TOS); + d_equalityEngine.addFunctionKind(kind::STRING_STOU32); + d_equalityEngine.addFunctionKind(kind::STRING_STRIDOF); + d_equalityEngine.addFunctionKind(kind::STRING_STRREPL); + } d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); @@ -593,9 +597,37 @@ void TheoryStrings::check(Effort e) { TNode fact = assertion.assertion; Trace("strings-assertion") << "get assertion: " << fact << endl; - polarity = fact.getKind() != kind::NOT; atom = polarity ? fact : fact[0]; + + //run preprocess + if( options::stringLazyPreproc() ){ + std::map< Node, Node >::iterator itp = d_preproc_cache.find( atom ); + if( itp==d_preproc_cache.end() ){ + std::vector< Node > new_nodes; + Node res = d_preproc.decompose( atom, new_nodes ); + d_preproc_cache[atom] = res; + if( atom!=res ){ + Trace("strings-assertion-debug") << "...preprocessed to : " << res << std::endl; + Node plem = NodeManager::currentNM()->mkNode( kind::IFF, atom, res ); + plem = Rewriter::rewrite( plem ); + d_out->lemma( plem ); + Trace("strings-pp-lemma") << "Preprocess eq lemma : " << plem << std::endl; + Trace("strings-pp-lemma") << "...from " << fact << std::endl; + }else{ + Trace("strings-assertion-debug") << "...preprocess ok." << std::endl; + } + if( !new_nodes.empty() ){ + Node nnlem = new_nodes.size()==1 ? new_nodes[0] : NodeManager::currentNM()->mkNode( kind::AND, new_nodes ); + nnlem = Rewriter::rewrite( nnlem ); + Trace("strings-assertion-debug") << "...new nodes : " << nnlem << std::endl; + Trace("strings-pp-lemma") << "Preprocess lemma : " << nnlem << std::endl; + Trace("strings-pp-lemma") << "...from " << fact << std::endl; + d_out->lemma( nnlem ); + } + } + } + //must record string in regular expressions if ( atom.getKind() == kind::STRING_IN_REGEXP ) { addMembership(assertion); diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index d83df2a31..7eda63f37 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -173,6 +173,9 @@ private: std::vector< Node > d_terms_cache; void collectTerm( Node n ); void appendTermLemma(); + // preprocess cache + StringsPreprocess d_preproc; + std::map< Node, Node > d_preproc_cache; ///////////////////////////////////////////////////////////////////////////// // MODEL GENERATION diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 8978372e3..581e2be0a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -244,7 +244,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { //t3 = s2 Node c4 = t[1].eqNode( sk3 ); //~contain(t2, s2) - Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, + Node c5 = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk2, NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[1], d_zero, NodeManager::currentNM()->mkNode(kind::MINUS, @@ -259,8 +259,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node cond = skk.eqNode( negone ); Node rr = NodeManager::currentNM()->mkNode( kind::ITE, cond, left, right ); new_nodes.push_back( rr ); - d_cache[t] = skk; - retNode = skk; + if( options::stringLazyPreproc() ){ + new_nodes.push_back( t.eqNode( skk ) ); + d_cache[t] = Node::null(); + }else{ + d_cache[t] = skk; + retNode = skk; + } } else { throw LogicException("string indexof not supported in default mode, try --strings-exp"); } @@ -373,12 +378,17 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { t.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, NodeManager::currentNM()->mkConst(::CVC4::String("-")), pret)))); new_nodes.push_back( conc );*/ - - d_cache[t] = pret; + if( options::stringLazyPreproc() && t!=pret ){ + new_nodes.push_back( t.eqNode( pret ) ); + d_cache[t] = Node::null(); + }else{ + d_cache[t] = pret; + retNode = pret; + } + //don't rewrite processed if(t != pret) { d_cache[pret] = pret; } - retNode = pret; } else { throw LogicException("string int.to.str not supported in default mode, try --strings-exp"); } @@ -488,12 +498,16 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { Node conc = NodeManager::currentNM()->mkNode(kind::ITE, pret.eqNode(negone), NodeManager::currentNM()->mkNode(kind::OR, cc1, cc2), cc3); new_nodes.push_back( conc ); - - d_cache[t] = pret; + if( options::stringLazyPreproc() && t!=pret ){ + new_nodes.push_back( t.eqNode( pret ) ); + d_cache[t] = Node::null(); + }else{ + d_cache[t] = pret; + retNode = pret; + } if(t != pret) { d_cache[pret] = pret; } - retNode = pret; } else { throw LogicException("string int.to.str not supported in default mode, try --strings-exp"); } @@ -511,8 +525,8 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { 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()->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), @@ -520,9 +534,13 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { new_nodes.push_back( rr ); rr = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, y), d_zero) ); new_nodes.push_back( rr ); - - d_cache[t] = skw; - retNode = skw; + if( options::stringLazyPreproc() ){ + new_nodes.push_back( t.eqNode( skw ) ); + d_cache[t] = Node::null(); + }else{ + d_cache[t] = skw; + retNode = skw; + } } else { throw LogicException("string replace not supported in default mode, try --strings-exp"); } @@ -609,13 +627,6 @@ void StringsPreprocess::simplify(std::vector< Node > &vec_node) { } } } -/* -void StringsPreprocess::simplify(std::vector< Node > &vec_node) { - std::vector< Node > new_nodes; - simplify(vec_node, new_nodes); - vec_node.insert( vec_node.end(), new_nodes.begin(), new_nodes.end() ); -} -*/ }/* CVC4::theory::strings namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 155b7b236..d96644bee 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -38,8 +38,8 @@ private: int checkFixLenVar( Node t ); void processRegExp( Node s, Node r, std::vector< Node > &ret ); Node simplify( Node t, std::vector< Node > &new_nodes ); - Node decompose( Node t, std::vector< Node > &new_nodes ); public: + Node decompose( Node t, std::vector< Node > &new_nodes ); void simplify(std::vector< Node > &vec_node); StringsPreprocess(); }; |