| STRINRE_TOK { $kind = CVC4::kind::STRING_IN_REGEXP; }
| STRTORE_TOK { $kind = CVC4::kind::STRING_TO_REGEXP; }
| RECON_TOK { $kind = CVC4::kind::REGEXP_CONCAT; }
- | REOR_TOK { $kind = CVC4::kind::REGEXP_OR; }
+ | REUNION_TOK { $kind = CVC4::kind::REGEXP_UNION; }
| REINTER_TOK { $kind = CVC4::kind::REGEXP_INTER; }
| RESTAR_TOK { $kind = CVC4::kind::REGEXP_STAR; }
| REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; }
STRINRE_TOK : 'str.in.re';
STRTORE_TOK : 'str.to.re';
RECON_TOK : 're.++';
-REOR_TOK : 're.or';
-REINTER_TOK : 're.itr';
+REUNION_TOK : 're.union';
+REINTER_TOK : 're.inter';
RESTAR_TOK : 're.*';
REPLUS_TOK : 're.+';
REOPT_TOK : 're.opt';
case kind::STRING_STOI: out << "str.to.int "; break;
case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
case kind::REGEXP_CONCAT: out << "re.++ "; break;
- case kind::REGEXP_OR: out << "re.or "; break;
- case kind::REGEXP_INTER: out << "re.itr "; break;
+ case kind::REGEXP_UNION: out << "re.union "; break;
+ case kind::REGEXP_INTER: out << "re.inter "; break;
case kind::REGEXP_STAR: out << "re.* "; break;
case kind::REGEXP_PLUS: out << "re.+ "; break;
case kind::REGEXP_OPT: out << "re.opt "; break;
return;
}
+ // set strings-exp
+ /*
+ if(!d_logic.hasEverything() && d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
+ if(! options::stringExp.wasSetByUser()) {
+ options::stringExp.set( true );
+ Trace("smt") << "turning on strings-exp, for the theory of strings" << std::endl;
+ }
+ }*/
// for strings
if(options::stringExp()) {
if( !d_logic.isQuantified() ) {
options::fmfBoundInt.set( true );
Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
}
+ /*
if(! options::rewriteDivk.wasSetByUser()) {
options::rewriteDivk.set( true );
Trace("smt") << "turning on rewrite-divk, for strings-exp" << std::endl;
- }
-
+ }*/
/*
if(! options::stringFMF.wasSetByUser()) {
options::stringFMF.set( true );
# equal equal / less than / output
operator STRING_TO_REGEXP 1 "convert string to regexp"
operator REGEXP_CONCAT 2: "regexp concat"
-operator REGEXP_OR 2: "regexp or"
+operator REGEXP_UNION 2: "regexp union"
operator REGEXP_INTER 2: "regexp intersection"
operator REGEXP_STAR 1 "regexp *"
operator REGEXP_PLUS 1 "regexp +"
# "a regexp contains all strings"
typerule REGEXP_CONCAT ::CVC4::theory::strings::RegExpConcatTypeRule
-typerule REGEXP_OR ::CVC4::theory::strings::RegExpOrTypeRule
+typerule REGEXP_UNION ::CVC4::theory::strings::RegExpUnionTypeRule
typerule REGEXP_INTER ::CVC4::theory::strings::RegExpInterTypeRule
typerule REGEXP_STAR ::CVC4::theory::strings::RegExpStarTypeRule
typerule REGEXP_PLUS ::CVC4::theory::strings::RegExpPlusTypeRule
module STRINGS "theory/strings/options.h" Strings theory
-expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
- the cardinality of the characters used by the theory of strings, default 256
+option stringExp strings-exp --strings-exp bool :default false :read-write
+ experimental features in the theory of strings
-option stringRegExpUnrollDepth strings-regexp-depth --strings-regexp-depth=N int16_t :default 10 :read-write
- the depth of unrolloing regular expression used by the theory of strings, default 10
+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 stringFMF strings-fmf --strings-fmf bool :default false :read-write
the finite model finding used by the theory of strings
-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
+expert-option stringCharCardinality strings-alphabet-card --strings-alphabet-card=N int16_t :default 256 :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
+ the cardinality of the characters used by the theory of strings, default 256
-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
+option stringRegExpUnrollDepth strings-regexp-depth --strings-regexp-depth=N int16_t :default 10 :read-write
+ the depth of unrolloing regular expression used by the theory of strings, default 10 (deprecated)
endmodule
\r
RegExpOpr::RegExpOpr() {\r
d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );\r
+ d_true = NodeManager::currentNM()->mkConst( true );\r
+ d_false = NodeManager::currentNM()->mkConst( false );\r
+ d_emptyRegexp = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );\r
+ d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );\r
+ d_one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );\r
// All Charactors = all printable ones 32-126\r
d_char_start = 'a';//' ';\r
d_char_end = 'c';//'~';\r
d_sigma = mkAllExceptOne( '\0' );\r
+ //d_sigma = NodeManager::currentNM()->mkConst( kind::REGEXP_SIGMA );\r
d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma );\r
}\r
\r
} else {\r
int k = r.getKind();\r
switch( k ) {\r
- case kind::STRING_TO_REGEXP:\r
- {\r
+ case kind::REGEXP_EMPTY: {\r
+ ret = 2;\r
+ break;\r
+ }\r
+ case kind::REGEXP_SIGMA: {\r
+ ret = 2;\r
+ break;\r
+ }\r
+ case kind::STRING_TO_REGEXP: {\r
if(r[0].isConst()) {\r
if(r[0] == d_emptyString) {\r
ret = 1;\r
} else {\r
ret = 0;\r
}\r
- }\r
break;\r
- case kind::REGEXP_CONCAT:\r
- {\r
+ }\r
+ case kind::REGEXP_CONCAT: {\r
bool flag = false;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
int tmp = delta( r[i] );\r
if(!flag && ret != 2) {\r
ret = 1;\r
}\r
- }\r
break;\r
- case kind::REGEXP_OR:\r
- {\r
+ }\r
+ case kind::REGEXP_UNION: {\r
bool flag = false;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
int tmp = delta( r[i] );\r
if(!flag && ret != 1) {\r
ret = 2;\r
}\r
- }\r
break;\r
- case kind::REGEXP_INTER:\r
- {\r
+ }\r
+ case kind::REGEXP_INTER: {\r
bool flag = true;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
int tmp = delta( r[i] );\r
if(flag) {\r
ret = 1;\r
}\r
- }\r
break;\r
- case kind::REGEXP_STAR:\r
- {\r
- ret = 1;\r
}\r
+ case kind::REGEXP_STAR: {\r
+ ret = 1;\r
break;\r
- case kind::REGEXP_PLUS:\r
- {\r
- ret = delta( r[0] );\r
}\r
+ case kind::REGEXP_PLUS: {\r
+ ret = delta( r[0] );\r
break;\r
- case kind::REGEXP_OPT:\r
- {\r
- ret = 1;\r
}\r
+ case kind::REGEXP_OPT: {\r
+ ret = 1;\r
break;\r
- case kind::REGEXP_RANGE:\r
- {\r
- ret = 2;\r
}\r
+ case kind::REGEXP_RANGE: {\r
+ ret = 2;\r
break;\r
- default:\r
- //TODO: special sym: sigma, none, all\r
+ }\r
+ default: {\r
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in delta of RegExp." << std::endl;\r
- //AlwaysAssert( false );\r
+ AlwaysAssert( false );\r
//return Node::null();\r
+ }\r
}\r
d_delta_cache[r] = ret;\r
}\r
return ret;\r
}\r
\r
-//null - no solution\r
Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {\r
Assert( c.size() < 2 );\r
Trace("strings-regexp-derivative") << "RegExp-derivative starts with R{ " << mkString( r ) << " }, c=" << c << std::endl;\r
- Node retNode = Node::null();\r
+ Node retNode = d_emptyRegexp;\r
PairDvStr dv = std::make_pair( r, c );\r
if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {\r
retNode = d_dv_cache[dv];\r
} else if( c.isEmptyString() ){\r
int tmp = delta( r );\r
if(tmp == 0) {\r
- retNode = Node::null();\r
// TODO variable\r
+ retNode = d_emptyRegexp;\r
} else if(tmp == 1) {\r
retNode = r;\r
} else {\r
- retNode = Node::null();\r
+ retNode = d_emptyRegexp;\r
}\r
} else {\r
int k = r.getKind();\r
switch( k ) {\r
- case kind::STRING_TO_REGEXP:\r
- {\r
+ case kind::REGEXP_EMPTY: {\r
+ retNode = d_emptyRegexp;\r
+ break;\r
+ }\r
+ case kind::REGEXP_SIGMA: {\r
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );\r
+ break;\r
+ }\r
+ case kind::STRING_TO_REGEXP: {\r
if(r[0].isConst()) {\r
if(r[0] == d_emptyString) {\r
- retNode = Node::null();\r
+ retNode = d_emptyRegexp;\r
} else {\r
if(r[0].getConst< CVC4::String >().getFirstChar() == c.getFirstChar()) {\r
- retNode = r[0].getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, \r
- NodeManager::currentNM()->mkConst( r[0].getConst< CVC4::String >().substr(1) ) );\r
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, \r
+ r[0].getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( r[0].getConst< CVC4::String >().substr(1) ) );\r
} else {\r
- retNode = Node::null();\r
+ retNode = d_emptyRegexp;\r
}\r
}\r
} else {\r
- retNode = Node::null();\r
// TODO variable\r
+ retNode = d_emptyRegexp;\r
}\r
- }\r
break;\r
- case kind::REGEXP_CONCAT:\r
- {\r
+ }\r
+ case kind::REGEXP_CONCAT: {\r
+ Node rees = NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString );\r
std::vector< Node > vec_nodes;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
Node dc = derivativeSingle(r[i], c);\r
- if(!dc.isNull()) {\r
+ if(dc != d_emptyRegexp) {\r
std::vector< Node > vec_nodes2;\r
- if(dc != d_emptyString) {\r
+ if(dc != rees) {\r
vec_nodes2.push_back( dc );\r
}\r
for(unsigned j=i+1; j<r.getNumChildren(); ++j) {\r
- if(r[j] != d_emptyString) {\r
+ if(r[j] != rees) {\r
vec_nodes2.push_back( r[j] );\r
}\r
}\r
- Node tmp = vec_nodes2.size()==0 ? d_emptyString :\r
- ( vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 ) );\r
+ Node tmp = vec_nodes2.size()==0 ? rees : \r
+ vec_nodes2.size()==1 ? vec_nodes2[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, vec_nodes2 );\r
if(std::find(vec_nodes.begin(), vec_nodes.end(), tmp) == vec_nodes.end()) {\r
vec_nodes.push_back( tmp );\r
}\r
break;\r
}\r
}\r
- retNode = vec_nodes.size() == 0 ? Node::null() :\r
- ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );\r
- }\r
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :\r
+ ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );\r
break;\r
- case kind::REGEXP_OR:\r
- {\r
+ }\r
+ case kind::REGEXP_UNION: {\r
std::vector< Node > vec_nodes;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
Node dc = derivativeSingle(r[i], c);\r
- if(!dc.isNull()) {\r
+ if(dc != d_emptyRegexp) {\r
if(std::find(vec_nodes.begin(), vec_nodes.end(), dc) == vec_nodes.end()) {\r
vec_nodes.push_back( dc );\r
}\r
}\r
Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << mkString(dc) << std::endl;\r
}\r
- retNode = vec_nodes.size() == 0 ? Node::null() :\r
- ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) );\r
- }\r
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :\r
+ ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes ) );\r
break;\r
- case kind::REGEXP_INTER:\r
- {\r
+ }\r
+ case kind::REGEXP_INTER: {\r
bool flag = true;\r
bool flag_sg = false;\r
std::vector< Node > vec_nodes;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
Node dc = derivativeSingle(r[i], c);\r
- if(!dc.isNull()) {\r
+ if(dc != d_emptyRegexp) {\r
if(dc == d_sigma_star) {\r
flag_sg = true;\r
} else {\r
if(vec_nodes.size() == 0 && flag_sg) {\r
retNode = d_sigma_star;\r
} else {\r
- retNode = vec_nodes.size() == 0 ? Node::null() :\r
+ retNode = vec_nodes.size() == 0 ? d_emptyRegexp :\r
( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_INTER, vec_nodes ) );\r
}\r
} else {\r
- retNode = Node::null();\r
+ retNode = d_emptyRegexp;\r
}\r
- }\r
break;\r
- case kind::REGEXP_STAR:\r
- {\r
- Node dc = derivativeSingle(r[0], c);\r
- if(!dc.isNull()) {\r
- retNode = dc==d_emptyString ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );\r
- } else {\r
- retNode = Node::null();\r
- }\r
}\r
- break;\r
- case kind::REGEXP_PLUS:\r
- {\r
+ case kind::REGEXP_STAR: {\r
Node dc = derivativeSingle(r[0], c);\r
- if(!dc.isNull()) {\r
- retNode = dc==d_emptyString ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );\r
+ if(dc != d_emptyRegexp) {\r
+ retNode = dc==NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, d_emptyString ) ? r : NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, dc, r );\r
} else {\r
- retNode = Node::null();\r
+ retNode = d_emptyRegexp;\r
}\r
- }\r
- break;\r
- case kind::REGEXP_OPT:\r
- {\r
- retNode = derivativeSingle(r[0], c);\r
- }\r
break;\r
- case kind::REGEXP_RANGE:\r
- {\r
- char ch = c.getFirstChar();\r
- if (ch >= r[0].getConst< CVC4::String >().getFirstChar() && ch <= r[1].getConst< CVC4::String >().getFirstChar() ) {\r
- retNode = d_emptyString;\r
- } else {\r
- retNode = Node::null();\r
- }\r
}\r
- break;\r
- default:\r
+ default: {\r
//TODO: special sym: sigma, none, all\r
Trace("strings-error") << "Unsupported term: " << mkString( r ) << " in derivative of RegExp." << std::endl;\r
- //AlwaysAssert( false );\r
+ Assert( false, "Unsupported Term" );\r
//return Node::null();\r
+ }\r
}\r
- if(!retNode.isNull()) {\r
+ if(retNode != d_emptyRegexp) {\r
retNode = Rewriter::rewrite( retNode );\r
}\r
d_dv_cache[dv] = retNode;\r
return true;\r
}\r
break;\r
- case kind::REGEXP_OR:\r
+ case kind::REGEXP_UNION:\r
{\r
int g_co;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
return true;\r
}\r
break;\r
- case kind::REGEXP_OR:\r
+ case kind::REGEXP_UNION:\r
{\r
bool flag = false;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
vec_nodes.push_back( n );\r
}\r
}\r
- return NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );\r
+ return NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );\r
}\r
\r
Node RegExpOpr::complement( Node r ) {\r
}\r
Node tmp = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, r, d_sigma, d_sigma_star );\r
vec_nodes.push_back( tmp );\r
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );\r
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );\r
}\r
} else {\r
Trace("strings-error") << "Unsupported string variable: " << r[0] << " in complement of RegExp." << std::endl;\r
}\r
vec_nodes.push_back( tmp );\r
}\r
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );\r
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );\r
}\r
break;\r
- case kind::REGEXP_OR:\r
+ case kind::REGEXP_UNION:\r
{\r
std::vector< Node > vec_nodes;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
Node tmp = complement( r[i] );\r
vec_nodes.push_back( tmp );\r
}\r
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );\r
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );\r
}\r
break;\r
case kind::REGEXP_STAR:\r
}\r
\r
//simplify\r
-void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes) {\r
+void RegExpOpr::simplify(Node t, std::vector< Node > &new_nodes, bool polarity) {\r
+ Trace("strings-regexp-simpl") << "RegExp-Simpl starts with " << t << ", polarity=" << polarity << std::endl; \r
Assert(t.getKind() == kind::STRING_IN_REGEXP);\r
Node str = Rewriter::rewrite(t[0]);\r
Node re = Rewriter::rewrite(t[1]);\r
- simplifyRegExp( str, re, new_nodes );\r
+ if(polarity) {\r
+ simplifyPRegExp( str, re, new_nodes );\r
+ } else {\r
+ simplifyNRegExp( str, re, new_nodes );\r
+ }\r
+ Trace("strings-regexp-simpl") << "RegExp-Simpl returns (" << new_nodes.size() << "):\n";\r
+ for(unsigned i=0; i<new_nodes.size(); i++) {\r
+ Trace("strings-regexp-simpl") << "\t" << new_nodes[i] << std::endl;\r
+ }\r
}\r
-void RegExpOpr::simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {\r
+void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {\r
+ std::pair < Node, Node > p(s, r);\r
+ std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_simpl_neg_cache.find(p);\r
+ if(itr != d_simpl_neg_cache.end()) {\r
+ new_nodes.push_back( itr->second );\r
+ return;\r
+ } else {\r
+ int k = r.getKind();\r
+ Node conc;\r
+ switch( k ) {\r
+ case kind::REGEXP_EMPTY: {\r
+ conc = d_true;\r
+ break;\r
+ }\r
+ case kind::REGEXP_SIGMA: {\r
+ conc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s)).negate();\r
+ break;\r
+ }\r
+ case kind::STRING_TO_REGEXP: {\r
+ conc = s.eqNode(r[0]).negate();\r
+ break;\r
+ }\r
+ case kind::REGEXP_CONCAT: {\r
+ //TODO: rewrite empty\r
+ Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());\r
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);\r
+ Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero),\r
+ NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) );\r
+ Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());\r
+ Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());\r
+ Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);\r
+ Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));\r
+ Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));\r
+ Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();\r
+ if(r[0].getKind() == kind::STRING_TO_REGEXP) {\r
+ s1r1 = s1.eqNode(r[0][0]).negate();\r
+ } else if(r[0].getKind() == kind::REGEXP_EMPTY) {\r
+ s1r1 = d_true;\r
+ }\r
+ Node r2 = r[1];\r
+ if(r.getNumChildren() > 2) {\r
+ std::vector< Node > nvec;\r
+ for(unsigned i=1; i<r.getNumChildren(); i++) {\r
+ nvec.push_back( r[i] );\r
+ }\r
+ r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, nvec);\r
+ }\r
+ r2 = Rewriter::rewrite(r2);\r
+ Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r2).negate();\r
+ if(r2.getKind() == kind::STRING_TO_REGEXP) {\r
+ s2r2 = s2.eqNode(r2[0]).negate();\r
+ } else if(r2.getKind() == kind::REGEXP_EMPTY) {\r
+ s2r2 = d_true;\r
+ }\r
+\r
+ conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);\r
+ conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);\r
+ conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);\r
+ conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);\r
+ conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);\r
+ break;\r
+ }\r
+ case kind::REGEXP_UNION: {\r
+ std::vector< Node > c_and;\r
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {\r
+ c_and.push_back( r[i][0].eqNode(s).negate() );\r
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {\r
+ continue;\r
+ } else {\r
+ c_and.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]).negate());\r
+ }\r
+ }\r
+ conc = c_and.size() == 0 ? d_true :\r
+ c_and.size() == 1 ? c_and[0] : NodeManager::currentNM()->mkNode(kind::AND, c_and);\r
+ break;\r
+ }\r
+ case kind::REGEXP_INTER: {\r
+ bool emptyflag = false;\r
+ std::vector< Node > c_or;\r
+ for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {\r
+ c_or.push_back( r[i][0].eqNode(s).negate() );\r
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {\r
+ emptyflag = true;\r
+ break;\r
+ } else {\r
+ c_or.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]).negate());\r
+ }\r
+ }\r
+ if(emptyflag) {\r
+ conc = d_true;\r
+ } else {\r
+ conc = c_or.size() == 1 ? c_or[0] : NodeManager::currentNM()->mkNode(kind::OR, c_or);\r
+ }\r
+ break;\r
+ }\r
+ case kind::REGEXP_STAR: {\r
+ if(s == d_emptyString) {\r
+ conc = d_false;\r
+ } else if(r[0].getKind() == kind::REGEXP_EMPTY) {\r
+ conc = s.eqNode(d_emptyString).negate();\r
+ } else if(r[0].getKind() == kind::REGEXP_SIGMA) {\r
+ conc = d_false;\r
+ } else {\r
+ Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);\r
+ Node sne = s.eqNode(d_emptyString).negate();\r
+ Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());\r
+ Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);\r
+ Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_one),\r
+ NodeManager::currentNM()->mkNode( kind::GEQ, lens, b1 ) );\r
+ //internal\r
+ Node s1 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, d_zero, b1);\r
+ Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1));\r
+ //Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());\r
+ //Node s2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());\r
+ //Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, s1, s2);\r
+ //Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2));\r
+ //Node s1len = b1.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1));\r
+ Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();\r
+ Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r).negate();\r
+ \r
+ conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);\r
+ //conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1len, conc);\r
+ //conc = NodeManager::currentNM()->mkNode(kind::EXISTS, b2v, conc);\r
+ conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);\r
+ conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);\r
+ conc = NodeManager::currentNM()->mkNode(kind::AND, sne, conc);\r
+ }\r
+ break;\r
+ }\r
+ default: {\r
+ Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyNRegExp." << std::endl;\r
+ AlwaysAssert( false, "Unsupported Term" );\r
+ }\r
+ }\r
+ conc = Rewriter::rewrite( conc );\r
+ new_nodes.push_back( conc );\r
+ d_simpl_neg_cache[p] = conc;\r
+ }\r
+}\r
+void RegExpOpr::simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {\r
std::pair < Node, Node > p(s, r);\r
std::map < std::pair< Node, Node >, Node >::const_iterator itr = d_simpl_cache.find(p);\r
if(itr != d_simpl_cache.end()) {\r
return;\r
} else {\r
int k = r.getKind();\r
+ Node conc;\r
switch( k ) {\r
- case kind::REGEXP_EMPTY:\r
- {\r
- Node eq = NodeManager::currentNM()->mkConst( false );\r
- new_nodes.push_back( eq );\r
- d_simpl_cache[p] = eq;\r
- }\r
+ case kind::REGEXP_EMPTY: {\r
+ conc = d_false;\r
break;\r
- case kind::REGEXP_SIGMA:\r
- {\r
- Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );\r
- Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));\r
- new_nodes.push_back( eq );\r
- d_simpl_cache[p] = eq;\r
}\r
+ case kind::REGEXP_SIGMA: {\r
+ conc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));\r
break;\r
- case kind::STRING_TO_REGEXP:\r
- {\r
- Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );\r
- new_nodes.push_back( eq );\r
- d_simpl_cache[p] = eq;\r
}\r
+ case kind::STRING_TO_REGEXP: {\r
+ conc = s.eqNode(r[0]);\r
break;\r
- case kind::REGEXP_CONCAT:\r
- {\r
+ }\r
+ case kind::REGEXP_CONCAT: {\r
+ std::vector< Node > nvec;\r
std::vector< Node > cc;\r
bool emptyflag = false;\r
- Node ff = NodeManager::currentNM()->mkConst( false );\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
if(r[i].getKind() == kind::STRING_TO_REGEXP) {\r
cc.push_back( r[i][0] );\r
emptyflag = true;\r
break;\r
} else {\r
- Node sk = NodeManager::currentNM()->mkSkolem( "rcon_$$", s.getType(), "created for regular expression concat" );\r
- simplifyRegExp( sk, r[i], new_nodes );\r
- if(new_nodes.size() != 0) {\r
- if(new_nodes[new_nodes.size() - 1] == ff) {\r
- emptyflag = true;\r
- break;\r
- }\r
- }\r
- cc.push_back( sk );\r
+ Node sk = NodeManager::currentNM()->mkSkolem( "rc_$$", s.getType(), "created for regular expression concat" );\r
+ Node lem = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk, r[i]);\r
+ nvec.push_back(lem);\r
+ cc.push_back(sk);\r
}\r
}\r
if(emptyflag) {\r
- new_nodes.push_back( ff );\r
- d_simpl_cache[p] = ff;\r
+ conc = d_false;\r
} else {\r
- Node cc_eq = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) );\r
- new_nodes.push_back( cc_eq );\r
- d_simpl_cache[p] = cc_eq;\r
+ Node lem = s.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc) );\r
+ nvec.push_back(lem);\r
+ conc = nvec.size() == 1 ? nvec[0] : NodeManager::currentNM()->mkNode(kind::AND, nvec);\r
}\r
- }\r
break;\r
- case kind::REGEXP_OR:\r
- {\r
+ }\r
+ case kind::REGEXP_UNION: {\r
std::vector< Node > c_or;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
- simplifyRegExp( s, r[i], c_or );\r
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {\r
+ c_or.push_back( r[i][0].eqNode(s) );\r
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {\r
+ continue;\r
+ } else {\r
+ c_or.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]));\r
+ }\r
}\r
- Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );\r
- new_nodes.push_back( eq );\r
- d_simpl_cache[p] = eq;\r
- }\r
+ conc = c_or.size() == 0 ? d_false :\r
+ c_or.size() == 1 ? c_or[0] : NodeManager::currentNM()->mkNode(kind::OR, c_or);\r
break;\r
- case kind::REGEXP_INTER:\r
- {\r
- Node nfalse = NodeManager::currentNM()->mkConst( false );\r
+ }\r
+ case kind::REGEXP_INTER: {\r
+ std::vector< Node > c_and;\r
+ bool emptyflag = false;\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
- simplifyRegExp( s, r[i], new_nodes );\r
- if(new_nodes.size() != 0) {\r
- if(new_nodes[new_nodes.size() - 1] == nfalse) {\r
- break;\r
- }\r
+ if(r[i].getKind() == kind::STRING_TO_REGEXP) {\r
+ c_and.push_back( r[i][0].eqNode(s) );\r
+ } else if(r[i].getKind() == kind::REGEXP_EMPTY) {\r
+ emptyflag = true;\r
+ break;\r
+ } else {\r
+ c_and.push_back(NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[i]));\r
}\r
}\r
- }\r
+ if(emptyflag) {\r
+ conc = d_false;\r
+ } else {\r
+ conc = c_and.size() == 1 ? c_and[0] : NodeManager::currentNM()->mkNode(kind::AND, c_and);\r
+ }\r
break;\r
- case kind::REGEXP_STAR:\r
- {\r
- Node eq;\r
- if(r[0].getKind() == kind::REGEXP_EMPTY) {\r
- eq = NodeManager::currentNM()->mkConst( false );\r
+ }\r
+ case kind::REGEXP_STAR: {\r
+ if(s == d_emptyString) {\r
+ conc = d_true;\r
+ } else if(r[0].getKind() == kind::REGEXP_EMPTY) {\r
+ conc = s.eqNode(d_emptyString);\r
} else if(r[0].getKind() == kind::REGEXP_SIGMA) {\r
- eq = NodeManager::currentNM()->mkConst( true );\r
+ conc = d_true;\r
} else {\r
- eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );\r
+ Node se = s.eqNode(d_emptyString);\r
+ Node sinr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s, r[0]);\r
+ Node sk1 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );\r
+ Node sk2 = NodeManager::currentNM()->mkSkolem( "rs_$$", s.getType(), "created for regular expression star" );\r
+ Node s1nz = sk1.eqNode(d_emptyString).negate();\r
+ Node s2nz = sk2.eqNode(d_emptyString).negate();\r
+ Node s1inr = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk1, r[0]);\r
+ Node s2inrs = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, sk2, r);\r
+ Node s12 = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, sk1, sk2));\r
+\r
+ conc = NodeManager::currentNM()->mkNode(kind::AND, s12, s1nz, s2nz, s1inr, s2inrs);\r
+ conc = NodeManager::currentNM()->mkNode(kind::OR, se, sinr, conc);\r
}\r
- new_nodes.push_back( eq );\r
- d_simpl_cache[p] = eq;\r
- }\r
- break;\r
- default:\r
- //TODO: special sym: sigma, none, all\r
- Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;\r
- Assert( false );\r
break;\r
+ }\r
+ default: {\r
+ Trace("strings-regexp") << "Unsupported term: " << r << " in simplifyPRegExp." << std::endl;\r
+ AlwaysAssert( false, "Unsupported Term" );\r
+ }\r
}\r
+ conc = Rewriter::rewrite( conc );\r
+ new_nodes.push_back( conc );\r
+ d_simpl_cache[p] = conc;\r
}\r
}\r
\r
} else {\r
int k = r.getKind();\r
switch( k ) {\r
- case kind::REGEXP_EMPTY:\r
- {\r
+ case kind::REGEXP_EMPTY: {\r
retStr += "Empty";\r
- }\r
break;\r
- case kind::REGEXP_SIGMA:\r
- {\r
- retStr += "{W}";\r
}\r
+ case kind::REGEXP_SIGMA: {\r
+ retStr += "{W}";\r
break;\r
- case kind::STRING_TO_REGEXP:\r
- {\r
- retStr += niceChar( r[0] );\r
}\r
+ case kind::STRING_TO_REGEXP: {\r
+ retStr += niceChar( r[0] );\r
break;\r
- case kind::REGEXP_CONCAT:\r
- {\r
+ }\r
+ case kind::REGEXP_CONCAT: {\r
retStr += "(";\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
if(i != 0) retStr += ".";\r
retStr += mkString( r[i] );\r
}\r
retStr += ")";\r
- }\r
break;\r
- case kind::REGEXP_OR:\r
- {\r
+ }\r
+ case kind::REGEXP_UNION: {\r
if(r == d_sigma) {\r
retStr += "{A}";\r
} else {\r
}\r
retStr += ")";\r
}\r
- }\r
break;\r
- case kind::REGEXP_INTER:\r
- {\r
+ }\r
+ case kind::REGEXP_INTER: {\r
retStr += "(";\r
for(unsigned i=0; i<r.getNumChildren(); ++i) {\r
if(i != 0) retStr += "&";\r
retStr += mkString( r[i] );\r
}\r
retStr += ")";\r
- }\r
break;\r
- case kind::REGEXP_STAR:\r
- {\r
+ }\r
+ case kind::REGEXP_STAR: {\r
retStr += mkString( r[0] );\r
retStr += "*";\r
- }\r
break;\r
- case kind::REGEXP_PLUS:\r
- {\r
+ }\r
+ case kind::REGEXP_PLUS: {\r
retStr += mkString( r[0] );\r
retStr += "+";\r
- }\r
break;\r
- case kind::REGEXP_OPT:\r
- {\r
+ }\r
+ case kind::REGEXP_OPT: {\r
retStr += mkString( r[0] );\r
retStr += "?";\r
- }\r
break;\r
- case kind::REGEXP_RANGE:\r
- {\r
+ }\r
+ case kind::REGEXP_RANGE: {\r
retStr += "[";\r
retStr += niceChar( r[0] );\r
retStr += "-";\r
retStr += niceChar( r[1] );\r
retStr += "]";\r
- }\r
break;\r
+ }\r
default:\r
- //TODO: special sym: sigma, none, all\r
Trace("strings-error") << "Unsupported term: " << r << " in RegExp." << std::endl;\r
//AlwaysAssert( false );\r
//return Node::null();\r
typedef std::pair< Node, CVC4::String > PairDvStr;\r
private:\r
Node d_emptyString;\r
+ Node d_true;\r
+ Node d_false;\r
+ Node d_emptyRegexp;\r
+ Node d_zero;\r
+ Node d_one;\r
+\r
char d_char_start;\r
char d_char_end;\r
Node d_sigma;\r
Node d_sigma_star;\r
\r
std::map< std::pair< Node, Node >, Node > d_simpl_cache;\r
+ std::map< std::pair< Node, Node >, Node > d_simpl_neg_cache;\r
std::map< Node, Node > d_compl_cache;\r
std::map< Node, int > d_delta_cache;\r
std::map< PairDvStr, Node > d_dv_cache;\r
std::map< Node, bool > d_cstre_cache;\r
//bool checkStarPlus( Node t );\r
- void simplifyRegExp( Node s, Node r, std::vector< Node > &new_nodes );\r
+ void simplifyPRegExp( Node s, Node r, std::vector< Node > &new_nodes );\r
+ void simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes );\r
std::string niceChar( Node r );\r
int gcd ( int a, int b );\r
\r
public:\r
RegExpOpr();\r
bool checkConstRegExp( Node r );\r
- void simplify(Node t, std::vector< Node > &new_nodes);\r
+ void simplify(Node t, std::vector< Node > &new_nodes, bool polarity);\r
Node mkAllExceptOne( char c );\r
Node complement( Node r );\r
int delta( Node r );\r
d_str_pos_ctn( c ),
d_str_neg_ctn( c ),
d_reg_exp_mem( c ),
+ d_regexp_deriv_processed( c ),
d_curr_cardinality( c, 0 )
{
// The kinds we are treating as function application in congruence
d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
d_emptyString = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
- d_true = NodeManager::currentNM()->mkConst( true );
+ d_emptyRegexp = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
+ d_true = NodeManager::currentNM()->mkConst( true );
d_false = NodeManager::currentNM()->mkConst( false );
d_all_warning = true;
conc = NodeManager::currentNM()->mkNode( kind::AND, vec_conc );//, len_x_gt_len_y
} // normal case
- //set its antecedant to ant, to say when it is relevant
- d_reg_exp_ant[str_in_re] = ant;
- //unroll the str in re constraint once
- unrollStar( str_in_re );
+ if( !options::stringExp() ) {
+ //set its antecedant to ant, to say when it is relevant
+ d_reg_exp_ant[str_in_re] = ant;
+ //unroll the str in re constraint once
+ unrollStar( str_in_re );
+ }
sendLemma( ant, conc, "LOOP-BREAK" );
++(d_statistics.d_loop_lemmas);
cc.push_back(unr0);
} else {
std::vector< Node > urc;
- d_regexp_opr.simplify(unr1, urc);
+ d_regexp_opr.simplify(unr1, urc, true);
Node unr0 = sk_s.eqNode( d_emptyString ).negate();
cc.push_back(unr0); //cc.push_back(urc1);
cc.insert(cc.end(), urc.begin(), urc.end());
}
bool TheoryStrings::checkMemberships() {
+ bool is_unk = false;
+ bool addedLemma = false;
+ for( unsigned i=0; i<d_reg_exp_mem.size(); i++ ){
+ //check regular expression membership
+ Node assertion = d_reg_exp_mem[i];
+ if(d_regexp_cache.find(assertion) == d_regexp_cache.end()) {
+ Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;
+ Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
+ bool polarity = assertion.getKind()!=kind::NOT;
+ bool flag = true;
+ if( polarity ) {
+ Node x = atom[0];
+ Node r = atom[1];
+ /*if(d_opt_regexp_gcd) {
+ if(d_membership_length.find(atom) == d_membership_length.end()) {
+ addedLemma = addMembershipLength(atom);
+ d_membership_length[atom] = true;
+ } else {
+ Trace("strings-regexp") << "Membership length is already added." << std::endl;
+ }
+ }*/
+ if(d_regexp_deriv_processed.find(atom) != d_regexp_deriv_processed.end()) {
+ flag = false;
+ } else {
+ if(areEqual(x, d_emptyString)) {
+ int rdel = d_regexp_opr.delta(r);
+ if(rdel == 1) {
+ flag = false;
+ d_regexp_deriv_processed[atom] = true;
+ } else if(rdel == 2) {
+ Node antec = x.eqNode(d_emptyString);
+ antec = NodeManager::currentNM()->mkNode(kind::AND, antec, atom);
+ Node conc = Node::null();
+ sendLemma(antec, conc, "RegExp Delta Conflict");
+ addedLemma = true;
+ flag = false;
+ d_regexp_deriv_processed[atom] = true;
+ }
+ } /*else if(splitRegExp( x, r, atom )) {
+ addedLemma = true; flag = false;
+ d_regexp_deriv_processed[ atom ] = true;
+ }*/
+ }
+ } else {
+ //TODO
+ if(! options::stringExp()) {
+ is_unk = true;
+ break;
+ }
+ }
+ if(flag) {
+ std::vector< Node > nvec;
+ d_regexp_opr.simplify(atom, nvec, polarity);
+ Node conc = nvec.size()==1 ? nvec[0] :
+ NodeManager::currentNM()->mkNode(kind::AND, nvec);
+ conc = Rewriter::rewrite(conc);
+ sendLemma( assertion, conc, "REGEXP" );
+ addedLemma = true;
+ d_regexp_cache[assertion] = true;
+ }
+ }
+ if(d_conflict) {
+ break;
+ }
+ }
+ if( addedLemma ){
+ doPendingLemmas();
+ return true;
+ }else{
+ if( is_unk ){
+ Trace("strings-regexp") << "Strings::regexp: possibly incomplete." << std::endl;
+ d_out->setIncomplete();
+ }
+ return false;
+ }
+}
+//TODO remove
+bool TheoryStrings::checkMemberships2() {
bool is_unk = false;
bool addedLemma = false;
for( unsigned i=0; i<d_reg_exp_mem.size(); i++ ){
}
} else {
if(d_str_neg_ctn_rewritten.find(atom) == d_str_neg_ctn_rewritten.end()) {
- Node b1 = NodeManager::currentNM()->mkBoundVar("bi", NodeManager::currentNM()->integerType());
+ 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 ),
NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::MINUS, lenx, lens ), b1 ) ) );
- Node b2 = NodeManager::currentNM()->mkBoundVar("bj", NodeManager::currentNM()->integerType());
+ Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
Node s2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, x, NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ), d_one);
Node s5 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, s, b2, d_one);
- Node s1 = NodeManager::currentNM()->mkBoundVar("s1", NodeManager::currentNM()->stringType());
- Node s3 = NodeManager::currentNM()->mkBoundVar("s3", NodeManager::currentNM()->stringType());
- Node s4 = NodeManager::currentNM()->mkBoundVar("s4", NodeManager::currentNM()->stringType());
- Node s6 = NodeManager::currentNM()->mkBoundVar("s6", NodeManager::currentNM()->stringType());
- Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2, s1, s3, s4, s6);
+ //Node s1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ //Node s3 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ //Node s4 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ //Node s6 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);//, s1, s3, s4, s6);
std::vector< Node > vec_nodes;
Node cc = NodeManager::currentNM()->mkNode( kind::GEQ, b2, d_zero );
cc = NodeManager::currentNM()->mkNode( kind::GEQ, lens, b2 );
vec_nodes.push_back(cc);
- cc = x.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2, s3));
- vec_nodes.push_back(cc);
- cc = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s4, s5, s6));
- vec_nodes.push_back(cc);
+ //cc = x.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s1, s2, s3));
+ //vec_nodes.push_back(cc);
+ //cc = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, s4, s5, s6));
+ //vec_nodes.push_back(cc);
cc = s2.eqNode(s5).negate();
vec_nodes.push_back(cc);
- cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
- vec_nodes.push_back(cc);
- cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2);
- vec_nodes.push_back(cc);
+ //cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s1).eqNode(NodeManager::currentNM()->mkNode( kind::PLUS, b1, b2 ));
+ //vec_nodes.push_back(cc);
+ //cc = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s4).eqNode(b2);
+ //vec_nodes.push_back(cc);
// charAt length
- cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2));
- vec_nodes.push_back(cc);
- cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5));
- vec_nodes.push_back(cc);
+ //cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s2));
+ //vec_nodes.push_back(cc);
+ //cc = d_one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s5));
+ //vec_nodes.push_back(cc);
Node conc = Rewriter::rewrite( NodeManager::currentNM()->mkNode(kind::AND, vec_nodes) );
Node xlss = NodeManager::currentNM()->mkNode( kind::GT, lens, lenx );
for(unsigned i=0; i<s.size(); ++i) {
CVC4::String c = s.substr(i, 1);
dc = d_regexp_opr.derivativeSingle(dc, c);
- if(dc.isNull()) {
+ if(dc == d_emptyRegexp) {
// CONFLICT
flag = false;
break;
conc = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, left, dc );
std::vector< Node > sdc;
- d_regexp_opr.simplify(conc, sdc);
+ d_regexp_opr.simplify(conc, sdc, true);
if(sdc.size() == 1) {
conc = sdc[0];
} else {
private:
// Constants
Node d_emptyString;
+ Node d_emptyRegexp;
Node d_true;
Node d_false;
Node d_zero;
bool checkCardinality();
bool checkInductiveEquations();
bool checkMemberships();
+ bool checkMemberships2();
bool checkContains();
bool checkPosContains();
bool checkNegContains();
private:
// regular expression memberships
NodeList d_reg_exp_mem;
+ std::map< Node, bool > d_regexp_cache;
// antecedant for why reg exp membership must be true
std::map< Node, Node > d_reg_exp_ant;
std::map< Node, bool > d_reg_exp_unroll;
std::map< Node, bool > d_membership_length;
// regular expression derivative
std::map< Node, bool > d_reg_exp_deriv;
+ NodeBoolMap d_regexp_deriv_processed;
// regular expression operations
RegExpOpr d_regexp_opr;
d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
}
-void StringsPreprocess::simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn ) {
+void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret ) {
int k = r.getKind();
switch( k ) {
- case kind::STRING_TO_REGEXP:
- {
- Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s, r[0] );
+ case kind::REGEXP_EMPTY: {
+ Node eq = NodeManager::currentNM()->mkConst( false );
ret.push_back( eq );
+ break;
}
+ case kind::REGEXP_SIGMA: {
+ Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+ Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
+ ret.push_back( eq );
break;
- case kind::REGEXP_CONCAT:
- {
+ }
+ case kind::STRING_TO_REGEXP: {
+ Node eq = s.eqNode( r[0] );
+ ret.push_back( eq );
+ break;
+ }
+ case kind::REGEXP_CONCAT: {
+ bool flag = true;
std::vector< Node > cc;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
if(r[i].getKind() == kind::STRING_TO_REGEXP) {
cc.push_back( r[i][0] );
} else {
- Node sk = NodeManager::currentNM()->mkSkolem( "recsym_$$", s.getType(), "created for regular expression concat" );
- simplifyRegExp( sk, r[i], ret, nn );
- cc.push_back( sk );
+ flag = false;
+ break;
}
}
- Node cc_eq = NodeManager::currentNM()->mkNode( kind::EQUAL, s,
- NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, cc ) );
- nn.push_back( cc_eq );
- }
+ if(flag) {
+ Node eq = s.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, cc));
+ ret.push_back(eq);
+ } else {
+ Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
+ ret.push_back( eq );
+ }
break;
- case kind::REGEXP_OR:
- {
+ }
+ case kind::REGEXP_UNION: {
std::vector< Node > c_or;
for(unsigned i=0; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], c_or, nn );
+ std::vector< Node > ntmp;
+ processRegExp( s, r[i], ntmp );
+ Node lem = ntmp.size()==1 ? ntmp[0] : NodeManager::currentNM()->mkNode(kind::AND, ntmp);
+ c_or.push_back( lem );
}
- Node eq = NodeManager::currentNM()->mkNode( kind::OR, c_or );
+ Node eq = NodeManager::currentNM()->mkNode(kind::OR, c_or);
ret.push_back( eq );
- }
break;
- case kind::REGEXP_INTER:
+ }
+ case kind::REGEXP_INTER: {
for(unsigned i=0; i<r.getNumChildren(); ++i) {
- simplifyRegExp( s, r[i], ret, nn );
+ processRegExp( s, r[i], ret );
}
break;
- case kind::REGEXP_STAR:
- {
- Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
- ret.push_back( eq );
}
+ case kind::REGEXP_STAR: {
+ if(r[0].getKind() == kind::REGEXP_SIGMA) {
+ ret.push_back(NodeManager::currentNM()->mkConst(true));
+ } else {
+ Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
+ ret.push_back( eq );
+ }
break;
- default:
- //TODO: special sym: sigma, none, all
+ }
+ default: {
Trace("strings-preprocess") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
- Assert( false );
- break;
+ AlwaysAssert( false, "Unsupported Term" );
+ }
}
}
d_cache[t] = t;
retNode = t;
}
- } else */if( t.getKind() == kind::STRING_IN_REGEXP ) {
- // t0 in t1
+ } else */
+ if( t.getKind() == kind::STRING_IN_REGEXP ) {
Node t0 = simplify( t[0], new_nodes );
- //if(!checkStarPlus( t[1] )) {
- //rewrite it
- std::vector< Node > ret;
- std::vector< Node > nn;
- simplifyRegExp( t0, t[1], ret, nn );
- new_nodes.insert( new_nodes.end(), nn.begin(), nn.end() );
+ //rewrite it
+ std::vector< Node > ret;
+ processRegExp( t0, t[1], ret );
- Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
- d_cache[t] = (t == n) ? Node::null() : n;
- retNode = n;
- //} else {
- // TODO
- // return (t0 == t[0]) ? t : NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, t0, t[1] );
- //}
+ Node n = ret.size() == 1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
+ n = Rewriter::rewrite(n);
+ d_cache[t] = (t == n) ? Node::null() : n;
+ retNode = n;
} else if( t.getKind() == kind::STRING_SUBSTR_TOTAL ) {
Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, t[0] ),
new_nodes.push_back(lem);
//non-neg
- Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
+ 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 ),
NodeManager::currentNM()->mkNode( kind::GT, lenp, b1 ) ) );
Node cc3 = NodeManager::currentNM()->mkNode(kind::GEQ, ufMx, d_zero);
Node cc4 = NodeManager::currentNM()->mkNode(kind::GEQ, nine, ufMx);
- Node b21 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->stringType());
- Node b22 = NodeManager::currentNM()->mkBoundVar("z", NodeManager::currentNM()->stringType());
+ Node b21 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ Node b22 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b21, b22);
Node c21 = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, b21).eqNode(
Node cc1 = t[0].eqNode(NodeManager::currentNM()->mkConst(::CVC4::String("")));
//cc1 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc1);
//cc2
- Node b1 = NodeManager::currentNM()->mkBoundVar("x", NodeManager::currentNM()->integerType());
- Node z1 = NodeManager::currentNM()->mkBoundVar("z1", NodeManager::currentNM()->stringType());
- Node z2 = NodeManager::currentNM()->mkBoundVar("z2", NodeManager::currentNM()->stringType());
- Node z3 = NodeManager::currentNM()->mkBoundVar("z3", NodeManager::currentNM()->stringType());
- Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1, z1, z2, z3);
std::vector< Node > vec_n;
- Node g = NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero);
- vec_n.push_back(g);
- g = NodeManager::currentNM()->mkNode(kind::GT, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, t[0]), b1);
- vec_n.push_back(g);
- g = b1.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z1) );
- vec_n.push_back(g);
- g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
+ Node z1 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
+ Node z2 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
+ Node z3 = NodeManager::currentNM()->mkSkolem("z1_$$", NodeManager::currentNM()->stringType());
+ Node g = one.eqNode( NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, z2) );
vec_n.push_back(g);
g = t[0].eqNode( NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, z1, z2, z3) );
vec_n.push_back(g);
- //Node z2 = NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR_TOTAL, t[0], one);
char chtmp[2];
chtmp[1] = '\0';
for(unsigned i=0; i<=9; i++) {
vec_n.push_back(g);
}
Node cc2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::AND, vec_n));
- cc2 = NodeManager::currentNM()->mkNode(kind::EXISTS, b1v, cc2);
- //cc2 = NodeManager::currentNM()->mkNode(kind::AND, ufP0.eqNode(negone), cc2);
//cc3
- Node b2 = NodeManager::currentNM()->mkBoundVar("y", NodeManager::currentNM()->integerType());
+ Node b2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
Node b2v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b2);
Node g2 = NodeManager::currentNM()->mkNode(kind::AND,
NodeManager::currentNM()->mkNode(kind::GEQ, b2, d_zero),
Node ufx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, b2);
Node ufx1 = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufP, NodeManager::currentNM()->mkNode(kind::MINUS,b2,one));
Node ufMx = NodeManager::currentNM()->mkNode(kind::APPLY_UF, ufM, b2);
- Node w1 = NodeManager::currentNM()->mkBoundVar("w1", NodeManager::currentNM()->stringType());
- Node w2 = NodeManager::currentNM()->mkBoundVar("w2", NodeManager::currentNM()->stringType());
+ Node w1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
+ Node w2 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->stringType());
Node b3v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, w1, w2);
Node b2gtz = NodeManager::currentNM()->mkNode(kind::GT, b2, d_zero);
Node c3c1 = ufx1.eqNode( NodeManager::currentNM()->mkNode(kind::PLUS,
unsigned num = t.getNumChildren();
if(num == 0) {
return simplify(t, new_nodes);
- } else if(num == 1) {
- Node s = decompose(t[0], new_nodes);
- if(s != t[0]) {
- Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), s );
- return simplify(tmp, new_nodes);
- } else {
- return simplify(t, new_nodes);
- }
} else {
bool changed = false;
std::vector< Node > cc;
+ if (t.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ cc.push_back(t.getOperator());
+ }
for(unsigned i=0; i<t.getNumChildren(); i++) {
Node s = decompose(t[i], new_nodes);
cc.push_back( s );
private:
bool checkStarPlus( Node t );
int checkFixLenVar( Node t );
- void simplifyRegExp( Node s, Node r, std::vector< Node > &ret, std::vector< Node > &nn );
+ 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 retNode = node;
std::vector<Node> node_vec;
Node preNode = Node::null();
- bool emptyflag = false;
for(unsigned int i=0; i<node.getNumChildren(); ++i) {
Node tmpNode = node[i];
- if( tmpNode.getKind() == kind::REGEXP_EMPTY ) {
- emptyflag = true;
- break;
- } else if(node[i].getKind() == kind::STRING_CONCAT) {
+ if(node[i].getKind() == kind::STRING_CONCAT) {
tmpNode = rewriteConcatString(node[i]);
if(tmpNode.getKind() == kind::STRING_CONCAT) {
- unsigned int j=0;
+ unsigned j=0;
if(!preNode.isNull()) {
if(tmpNode[0].isConst()) {
preNode = NodeManager::currentNM()->mkConst( preNode.getConst<String>().concat( tmpNode[0].getConst<String>() ) );
node_vec.push_back( preNode );
preNode = Node::null();
- ++j;
} else {
node_vec.push_back( preNode );
preNode = Node::null();
node_vec.push_back( tmpNode[0] );
- ++j;
}
+ ++j;
}
for(; j<tmpNode.getNumChildren() - 1; ++j) {
node_vec.push_back( tmpNode[j] );
}
}
if(!tmpNode.isConst()) {
- if(preNode != Node::null()) {
+ if(!preNode.isNull()) {
if(preNode.getKind() == kind::CONST_STRING && preNode.getConst<String>().isEmptyString() ) {
preNode = Node::null();
} else {
}
}
}
- if(emptyflag) {
- retNode = NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY );
+ if(preNode != Node::null()) {
+ node_vec.push_back( preNode );
+ }
+ if(node_vec.size() > 1) {
+ retNode = NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, node_vec);
} else {
- if(preNode != Node::null()) {
- node_vec.push_back( preNode );
- }
- if(node_vec.size() > 1) {
- retNode = NodeManager::currentNM()->mkNode(kind::STRING_CONCAT, node_vec);
- } else {
- retNode = node_vec[0];
- }
+ retNode = node_vec[0];
}
Trace("strings-prerewrite") << "Strings::rewriteConcatString end " << retNode << std::endl;
return retNode;
for(unsigned int i=0; i<node.getNumChildren(); ++i) {
Trace("strings-prerewrite") << "Strings::prerewriteConcatRegExp preNode: " << preNode << std::endl;
Node tmpNode = node[i];
- if(node[i].getKind() == kind::REGEXP_CONCAT) {
+ if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
tmpNode = prerewriteConcatRegExp(node[i]);
if(tmpNode.getKind() == kind::REGEXP_CONCAT) {
- unsigned int j=0;
+ unsigned j=0;
if(!preNode.isNull()) {
if(tmpNode[0].getKind() == kind::STRING_TO_REGEXP) {
preNode = rewriteConcatString(
NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, preNode, tmpNode[0][0] ) );
node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
preNode = Node::null();
- ++j;
} else {
node_vec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, preNode ) );
preNode = Node::null();
node_vec.push_back( tmpNode[0] );
- ++j;
}
+ ++j;
}
for(; j<tmpNode.getNumChildren() - 1; ++j) {
node_vec.push_back( tmpNode[j] );
}
Node TheoryStringsRewriter::prerewriteOrRegExp(TNode node) {
- Assert( node.getKind() == kind::REGEXP_OR );
+ Assert( node.getKind() == kind::REGEXP_UNION );
Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
Node retNode = node;
std::vector<Node> node_vec;
- bool flag = true;
- for(unsigned int i=0; i<node.getNumChildren(); ++i) {
- if(node[i].getKind() == kind::REGEXP_OR) {
+ bool flag = false;
+ for(unsigned i=0; i<node.getNumChildren(); ++i) {
+ if(node[i].getKind() == kind::REGEXP_UNION) {
Node tmpNode = prerewriteOrRegExp( node[i] );
for(unsigned int j=0; j<tmpNode.getNumChildren(); ++j) {
- node_vec.push_back( tmpNode[i] );
+ node_vec.push_back( tmpNode[j] );
}
- flag = false;
+ flag = true;
+ } else if(node[i].getKind() == kind::REGEXP_EMPTY) {
+ flag = true;
} else {
- if(node[i].getKind() != kind::REGEXP_EMPTY) {
- node_vec.push_back( node[i] );
- }
+ node_vec.push_back( node[i] );
}
}
if(flag) {
retNode = node_vec.size() == 0 ? NodeManager::currentNM()->mkConst( kind::REGEXP_EMPTY ) :
- node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_OR, node_vec);
+ node_vec.size() == 1 ? node_vec[0] : NodeManager::currentNM()->mkNode(kind::REGEXP_UNION, node_vec);
}
Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp end " << retNode << std::endl;
return retNode;
Assert( index_start <= s.size() );
int k = r.getKind();
switch( k ) {
- case kind::STRING_TO_REGEXP:
- {
+ case kind::STRING_TO_REGEXP: {
CVC4::String s2 = s.substr( index_start, s.size() - index_start );
if(r[0].getKind() == kind::CONST_STRING) {
return ( s2 == r[0].getConst<String>() );
} else {
- Assert( false, "RegExp contains variable" );
+ Assert( false, "RegExp contains variables" );
}
}
- case kind::REGEXP_CONCAT:
- {
+ case kind::REGEXP_CONCAT: {
if( s.size() != index_start ) {
std::vector<int> vec_k( r.getNumChildren(), -1 );
int start = 0;
return true;
}
}
- case kind::REGEXP_OR:
- {
+ case kind::REGEXP_UNION: {
for(unsigned i=0; i<r.getNumChildren(); ++i) {
if(testConstStringInRegExp( s, index_start, r[i] )) return true;
}
return false;
}
- case kind::REGEXP_INTER:
- {
+ case kind::REGEXP_INTER: {
for(unsigned i=0; i<r.getNumChildren(); ++i) {
if(!testConstStringInRegExp( s, index_start, r[i] )) return false;
}
return true;
}
- case kind::REGEXP_STAR:
- {
+ case kind::REGEXP_STAR: {
if( s.size() != index_start ) {
- for(unsigned int k=s.size() - index_start; k>0; --k) {
+ for(unsigned k=s.size() - index_start; k>0; --k) {
CVC4::String t = s.substr(index_start, k);
if( testConstStringInRegExp( t, 0, r[0] ) ) {
if( index_start + k == s.size() || testConstStringInRegExp( s, index_start + k, r ) ) {
return true;
}
}
- case kind::REGEXP_EMPTY:
- {
+ case kind::REGEXP_EMPTY: {
return false;
}
- case kind::REGEXP_SIGMA:
- {
+ case kind::REGEXP_SIGMA: {
if(s.size() == 1) {
return true;
} else {
return false;
}
}
- default:
- //TODO: special sym: sigma, none, all
+ default: {
Trace("strings-postrewrite") << "Unsupported term: " << r << " in testConstStringInRegExp." << std::endl;
- Assert( false );
+ AlwaysAssert( false, "Unsupported Term" );
return false;
+ }
}
}
+
Node TheoryStringsRewriter::rewriteMembership(TNode node) {
Node retNode = node;
Node x = node[0];
//test whether x in node[1]
CVC4::String s = x.getConst<String>();
retNode = NodeManager::currentNM()->mkConst( testConstStringInRegExp( s, 0, node[1] ) );
- } else {
- if( x != node[0] ) {
- retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] );
- }
+ } else if(node[1].getKind() == kind::REGEXP_SIGMA) {
+ Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
+ retNode = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x));
+ } else if(node[1].getKind() == kind::REGEXP_STAR && node[1][0].getKind() == kind::REGEXP_SIGMA) {
+ retNode = NodeManager::currentNM()->mkConst( true );
+ } else if( x != node[0] ) {
+ retNode = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, node[1] );
}
return retNode;
}
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<Rational>().getNumerator().toUnsignedInt();
- int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
- if( i>=0 && j>=0 && node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
- retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
+ } else if( node[1].isConst() && node[2].isConst() ) {
+ if(node[1].getConst<Rational>().sgn()>=0 && node[2].getConst<Rational>().sgn()>=0) {
+ int i = node[1].getConst<Rational>().getNumerator().toUnsignedInt();
+ int j = node[2].getConst<Rational>().getNumerator().toUnsignedInt();
+ if( node[0].isConst() ) {
+ if( node[0].getConst<String>().size() >= (unsigned) (i + j) ) {
+ retNode = NodeManager::currentNM()->mkConst( node[0].getConst<String>().substr(i, j) );
+ } else {
+ retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+ }
+ } else if(node[0].getKind() == kind::STRING_CONCAT && node[0][0].isConst()) {
+ if( node[0][0].getConst<String>().size() >= (unsigned) (i + j) ) {
+ retNode = NodeManager::currentNM()->mkConst( node[0][0].getConst<String>().substr(i, j) );
+ }
+ }
} else {
retNode = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
}
CVC4::String s = node[0].getConst<String>();
if(s.isNumber()) {
std::string stmp = s.toString();
- retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(stmp.c_str()));
+ if(stmp[0] == '0' && stmp.size() != 1) {
+ //TODO: leading zeros
+ retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
+ } else {
+ retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(stmp.c_str()));
+ }
} else {
retNode = NodeManager::currentNM()->mkConst(::CVC4::Rational(-1));
}
retNode = rewriteConcatString(node);
} else if(node.getKind() == kind::REGEXP_CONCAT) {
retNode = prerewriteConcatRegExp(node);
- } else if(node.getKind() == kind::REGEXP_OR) {
+ } else if(node.getKind() == kind::REGEXP_UNION) {
retNode = prerewriteOrRegExp(node);
} else if(node.getKind() == kind::REGEXP_PLUS) {
retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_CONCAT, node[0],
NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, node[0]));
} else if(node.getKind() == kind::REGEXP_OPT) {
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR,
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION,
NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP, NodeManager::currentNM()->mkConst( ::CVC4::String("") ) ),
node[0]);
} else if(node.getKind() == kind::REGEXP_RANGE) {
if(vec_nodes.size() == 1) {
retNode = vec_nodes[0];
} else {
- retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes );
+ retNode = NodeManager::currentNM()->mkNode( kind::REGEXP_UNION, vec_nodes );
}
}
}
};
-class RegExpOrTypeRule {
+class RegExpUnionTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
throw (TypeCheckingExceptionPrivate, AssertionException) {
model001.smt2 \
substr001.smt2 \
regexp001.smt2 \
- regexp002.smt2 \
loop001.smt2 \
loop002.smt2 \
loop003.smt2 \
loop008.smt2 \
loop009.smt2
+#regexp002.smt2
+
FAILING_TESTS =
EXTRA_DIST = $(TESTS)
(set-logic QF_S)\r
+(set-option :strings-exp true)\r
(set-option :strings-fmf true)\r
(set-info :status sat)\r
\r
(set-logic QF_S)\r
+(set-option :strings-exp true)\r
(set-option :strings-fmf true)\r
(set-info :status sat)\r
\r
(set-logic QF_S)
+(set-option :strings-exp true)
(set-info :status sat)
(declare-fun x () String)
(set-logic QF_S)\r
+(set-option :strings-exp true)\r
(set-info :status sat)\r
\r
(declare-fun x () String)\r
(set-logic QF_S)\r
+(set-option :strings-exp true)\r
(set-info :status sat)\r
\r
(declare-fun x () String)\r
(set-logic QF_S)\r
(set-info :status sat)\r
+(set-option :strings-exp true)\r
\r
(declare-fun x () String)\r
\r
(set-logic QF_S)\r
(set-info :status sat)\r
+(set-option :strings-exp true)\r
\r
(declare-fun x () String)\r
(declare-fun y () String)\r
projects / cvc5.git / commitdiff