diff options
| -rw-r--r-- | src/theory/strings/options | 3 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 36 | ||||
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 22 | ||||
| -rw-r--r-- | test/regress/regress0/strings/substr001.smt2 | 1 |
4 files changed, 39 insertions, 23 deletions
diff --git a/src/theory/strings/options b/src/theory/strings/options index 8bede6cae..6f4355fb6 100644 --- a/src/theory/strings/options +++ b/src/theory/strings/options @@ -17,4 +17,7 @@ option stringFMF strings-fmf --strings-fmf bool :default false :predicate CVC4:: option stringLB strings-lb --strings-lb=N unsigned :default 0 :predicate less_equal(2) :predicate-include "smt/smt_engine.h" the strategy of LB rule application: 0-lazy, 1-eager, 2-no +option stringExp strings-exp --strings-exp bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h" + experimental features in the theory of strings + endmodule diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index 9da0e343d..ff01b1887 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -16,6 +16,8 @@ #include "theory/strings/theory_strings_preprocess.h" #include "expr/kind.h" +#include "theory/strings/options.h" +#include "smt/logic_exception.h" namespace CVC4 { namespace theory { @@ -114,22 +116,26 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) { // return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] ); //} } else if( t.getKind() == kind::STRING_SUBSTR ){ - Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); - Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); - Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" ); - Node x = simplify( t[0], new_nodes ); - Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, - NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); - new_nodes.push_back( x_eq_123 ); - Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); - new_nodes.push_back( len_sk1_eq_i ); - Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2], - NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); - new_nodes.push_back( len_sk2_eq_j ); + if(options::stringExp()) { + Node sk1 = NodeManager::currentNM()->mkSkolem( "st1sym_$$", t.getType(), "created for substr" ); + Node sk2 = NodeManager::currentNM()->mkSkolem( "st2sym_$$", t.getType(), "created for substr" ); + Node sk3 = NodeManager::currentNM()->mkSkolem( "st3sym_$$", t.getType(), "created for substr" ); + Node x = simplify( t[0], new_nodes ); + Node x_eq_123 = NodeManager::currentNM()->mkNode( kind::EQUAL, + NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, sk2, sk3 ), x ); + new_nodes.push_back( x_eq_123 ); + Node len_sk1_eq_i = NodeManager::currentNM()->mkNode( kind::EQUAL, t[1], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk1 ) ); + new_nodes.push_back( len_sk1_eq_i ); + Node len_sk2_eq_j = NodeManager::currentNM()->mkNode( kind::EQUAL, t[2], + NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk2 ) ); + new_nodes.push_back( len_sk2_eq_j ); - d_cache[t] = sk2; - retNode = sk2; + d_cache[t] = sk2; + retNode = sk2; + } else { + throw LogicException("substring not supported in this release"); + } } else if( t.getNumChildren()>0 ){ std::vector< Node > cc; if (t.getMetaKind() == kind::metakind::PARAMETERIZED) { diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index cd9db85c7..0e37367bf 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -14,6 +14,8 @@ ** Implementation of the theory of strings. **/ #include "theory/strings/theory_strings_rewriter.h" +#include "theory/strings/options.h" +#include "smt/logic_exception.h" using namespace std; using namespace CVC4; @@ -339,17 +341,21 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { } } } else if(node.getKind() == kind::STRING_SUBSTR) { - if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { - int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); - int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); - if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) { - retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); + if(options::stringExp()) { + if( node[0].isConst() && node[1].isConst() && node[2].isConst() ) { + int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt(); + int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt(); + if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) { + retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) ); + } else { + // TODO: some issues, must be guarded by users + retNode = NodeManager::currentNM()->mkConst( false ); + } } else { - // TODO: some issues, must be guarded by users - retNode = NodeManager::currentNM()->mkConst( false ); + //handled by preprocess } } else { - //handled by preprocess + throw LogicException("substring not supported in this release"); } } else if(node.getKind() == kind::STRING_IN_REGEXP) { retNode = rewriteMembership(node); diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 index b5ff587b2..2b2ae9820 100644 --- a/test/regress/regress0/strings/substr001.smt2 +++ b/test/regress/regress0/strings/substr001.smt2 @@ -1,4 +1,5 @@ (set-logic QF_S)
+(set-option :strings-exp true)
(set-info :status sat)
(declare-fun x () String)
|