diff options
-rw-r--r-- | src/smt/smt_engine.cpp | 23 | ||||
-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 | ||||
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 6 | ||||
-rw-r--r-- | test/regress/regress0/strings/bug613.smt2 | 9 | ||||
-rwxr-xr-x | test/regress/regress0/strings/ilc-like.smt2 | 14 | ||||
-rwxr-xr-x | test/regress/regress0/strings/indexof-sym-simp.smt2 | 10 |
10 files changed, 125 insertions, 40 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 519f330df..ae93176b2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3294,17 +3294,18 @@ void SmtEnginePrivate::processAssertions() { dumpAssertions("post-bv-to-bool", d_assertions); Trace("smt") << "POST bvToBool" << endl; } - - if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; - dumpAssertions("pre-strings-pp", d_assertions); - CVC4::theory::strings::StringsPreprocess sp; - sp.simplify( d_assertions.ref() ); - //for (unsigned i = 0; i < d_assertions.size(); ++ i) { - // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); - //} - Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; - dumpAssertions("post-strings-pp", d_assertions); + if( !options::stringLazyPreproc() ){ + if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) { + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl; + dumpAssertions("pre-strings-pp", d_assertions); + CVC4::theory::strings::StringsPreprocess sp; + sp.simplify( d_assertions.ref() ); + //for (unsigned i = 0; i < d_assertions.size(); ++ i) { + // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) ); + //} + Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl; + dumpAssertions("post-strings-pp", d_assertions); + } } if( d_smt.d_logic.isQuantified() ){ Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl; 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(); }; diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index eb88df905..b796fc80b 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -50,8 +50,10 @@ TESTS = \ loop008.smt2 \ loop009.smt2 \ reloop.smt2 \ - unsound-0908.smt2 - + unsound-0908.smt2 \ + ilc-like.smt2 \ + indexof-sym-simp.smt2 \ + bug613.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/bug613.smt2 b/test/regress/regress0/strings/bug613.smt2 new file mode 100644 index 000000000..506076cd6 --- /dev/null +++ b/test/regress/regress0/strings/bug613.smt2 @@ -0,0 +1,9 @@ +(set-logic QF_S) +(set-info :status sat) +(set-option :strings-exp true) + +(declare-fun s () String) +(assert (= s "<a></a>")) +(assert (< (str.indexof s "<a>" 0) (str.indexof s "</a>" 0))) + +(check-sat) diff --git a/test/regress/regress0/strings/ilc-like.smt2 b/test/regress/regress0/strings/ilc-like.smt2 new file mode 100755 index 000000000..a711c215c --- /dev/null +++ b/test/regress/regress0/strings/ilc-like.smt2 @@ -0,0 +1,14 @@ +(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun s () String)
+(assert (= s "I like cookies."))
+
+(declare-fun target () String)
+(assert (= target "like"))
+
+(declare-fun location () Int)
+(assert (= location (str.indexof s target 0)))
+
+(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/indexof-sym-simp.smt2 b/test/regress/regress0/strings/indexof-sym-simp.smt2 new file mode 100755 index 000000000..7ae60f2db --- /dev/null +++ b/test/regress/regress0/strings/indexof-sym-simp.smt2 @@ -0,0 +1,10 @@ +(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+(declare-fun s () String)
+(declare-fun t () String)
+(declare-fun r () String)
+; solvable if we do equality reasoning over str.indexof
+(assert (= t s))
+(assert (not (= (str.indexof t r 0) (str.indexof s r 0))))
+(check-sat)
\ No newline at end of file |