if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-strings-preprocess" << endl;
dumpAssertions("pre-strings-pp", d_assertions);
- ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
- //for (unsigned i = 0; i < d_assertions.size(); ++ i) {
- // d_assertions.replace( i, Rewriter::rewrite( d_assertions[i] ) );
- //}
+ if( !options::stringLazyPreproc() ){
+ ((theory::strings::TheoryStrings*)d_smt.d_theoryEngine->theoryOf(THEORY_STRINGS))->getPreprocess()->simplify( d_assertions.ref() );
+ }
Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-strings-preprocess" << endl;
dumpAssertions("post-strings-pp", d_assertions);
}
d_false = NodeManager::currentNM()->mkConst( false );
d_card_size = 128;
- //d_opt_regexp_gcd = true;
}
TheoryStrings::~TheoryStrings() {
return EQUALITY_UNKNOWN;
}
-void TheoryStrings::propagate(Effort e)
-{
+void TheoryStrings::propagate(Effort e) {
// direct propagation now
}
}
/** explain */
-void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions){
+void TheoryStrings::explain(TNode literal, std::vector<TNode>& assumptions) {
Debug("strings-explain") << "Explain " << literal << " " << d_conflict << std::endl;
bool polarity = literal.getKind() != kind::NOT;
TNode atom = polarity ? literal : literal[0];
void TheoryStrings::presolve() {
Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
- d_opt_fmf = options::stringFMF();
if(!options::stdASCII()) {
d_card_size = 256;
}
////step 2 : assign arbitrary values for unknown lengths?
// confirmed by calculus invariant, see paper
- //for( unsigned i=0; i<col.size(); i++ ){
- // if(
- //}
Trace("strings-model") << "Assign to equivalence classes..." << std::endl;
//step 3 : assign values to equivalence classes that are pure variables
for( unsigned i=0; i<col.size(); i++ ){
d_preproc_cache[ atom ] = true;
std::vector< Node > new_nodes;
Node res = d_preproc.decompose( atom, new_nodes );
+ Assert( res==atom );
+ /*
if( atom!=res ){
//check if reduction/deduction
std::vector< Node > subs_lhs;
}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 );
return addFact;
}
-bool TheoryStrings::hasProcessed() {
- return d_conflict || !d_lemma_cache.empty() || !d_pending.empty();
-}
-
-void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
- if( a!=b ){
- Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
- Assert( areEqual( a, b ) );
- exp.push_back( a.eqNode( b ) );
- }
-}
-void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) {
- if( !lit.isNull() ){
- exp.push_back( lit );
- }
-}
-
TheoryStrings::EqcInfo::EqcInfo( context::Context* c ) : d_const_term(c), d_length_term(c), d_cardinality_lem_k(c), d_normalized_length(c) {
}
d_pending_req_phase.clear();
}
+bool TheoryStrings::hasProcessed() {
+ return d_conflict || !d_lemma_cache.empty() || !d_pending.empty();
+}
+
+void TheoryStrings::addToExplanation( Node a, Node b, std::vector< Node >& exp ) {
+ if( a!=b ){
+ Debug("strings-explain") << "Add to explanation : " << a << " == " << b << std::endl;
+ Assert( areEqual( a, b ) );
+ exp.push_back( a.eqNode( b ) );
+ }
+}
+
+void TheoryStrings::addToExplanation( Node lit, std::vector< Node >& exp ) {
+ if( !lit.isNull() ){
+ exp.push_back( lit );
+ }
+}
+
bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
std::vector< std::vector< Node > > &normal_forms, std::vector< std::vector< Node > > &normal_forms_exp, std::vector< Node > &normal_form_src) {
Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
}
}
-void TheoryStrings::checkNormalForms() {
- Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
- //calculate normal forms for each equivalence class, possibly adding splitting lemmas
- d_normal_forms.clear();
- d_normal_forms_exp.clear();
- std::map< Node, Node > nf_to_eqc;
- std::map< Node, Node > eqc_to_exp;
- for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
- Node eqc = d_strings_eqc[i];
- Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl;
- std::vector< Node > visited;
- std::vector< Node > nf;
- std::vector< Node > nf_exp;
- normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
- Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
- if( d_conflict ) {
- return;
- } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
- Node nf_term = mkConcat( nf );
- if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) {
- //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
- //two equivalence classes have same normal form, merge
- nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] );
- Node eq = eqc.eqNode( nf_to_eqc[nf_term] );
- sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" );
- } else {
- nf_to_eqc[nf_term] = eqc;
- eqc_to_exp[eqc] = mkAnd( nf_exp );
- }
- }
- Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
- }
-
- if(Trace.isOn("strings-nf")) {
- Trace("strings-nf") << "**** Normal forms are : " << std::endl;
- for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
- Trace("strings-nf") << " N[" << it->second << "] = " << it->first << std::endl;
- }
- Trace("strings-nf") << std::endl;
- }
- if( !hasProcessed() ){
- checkExtendedFuncsEval( 1 );
- Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
- if( !hasProcessed() ){
- if( !options::stringEagerLen() ){
- checkLengthsEqc();
- if( hasProcessed() ){
- return;
- }
- }
- //process disequalities between equivalence classes
- checkDeqNF();
- Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
- }
- }
- Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
-}
-
Node TheoryStrings::checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp ){
if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
// a loop
}
+void TheoryStrings::checkNormalForms() {
+ Trace("strings-process") << "Normalize equivalence classes...." << std::endl;
+ //calculate normal forms for each equivalence class, possibly adding splitting lemmas
+ d_normal_forms.clear();
+ d_normal_forms_exp.clear();
+ std::map< Node, Node > nf_to_eqc;
+ std::map< Node, Node > eqc_to_exp;
+ for( unsigned i=0; i<d_strings_eqc.size(); i++ ) {
+ Node eqc = d_strings_eqc[i];
+ Trace("strings-process-debug") << "- Verify normal forms are the same for " << eqc << std::endl;
+ std::vector< Node > visited;
+ std::vector< Node > nf;
+ std::vector< Node > nf_exp;
+ normalizeEquivalenceClass(eqc, visited, nf, nf_exp);
+ Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
+ if( d_conflict ) {
+ return;
+ } else if ( d_pending.empty() && d_lemma_cache.empty() ) {
+ Node nf_term = mkConcat( nf );
+ if( nf_to_eqc.find( nf_term )!=nf_to_eqc.end() ) {
+ //Trace("strings-debug") << "Merge because of normal form : " << eqc << " and " << nf_to_eqc[nf_term] << " both have normal form " << nf_term << std::endl;
+ //two equivalence classes have same normal form, merge
+ nf_exp.push_back( eqc_to_exp[nf_to_eqc[nf_term]] );
+ Node eq = eqc.eqNode( nf_to_eqc[nf_term] );
+ sendInfer( mkAnd( nf_exp ), eq, "Normal_Form" );
+ } else {
+ nf_to_eqc[nf_term] = eqc;
+ eqc_to_exp[eqc] = mkAnd( nf_exp );
+ }
+ }
+ Trace("strings-process-debug") << "Done verifying normal forms are the same for " << eqc << std::endl;
+ }
+
+ if(Trace.isOn("strings-nf")) {
+ Trace("strings-nf") << "**** Normal forms are : " << std::endl;
+ for( std::map< Node, Node >::iterator it = nf_to_eqc.begin(); it != nf_to_eqc.end(); ++it ){
+ Trace("strings-nf") << " N[" << it->second << "] = " << it->first << std::endl;
+ }
+ Trace("strings-nf") << std::endl;
+ }
+ if( !hasProcessed() ){
+ checkExtendedFuncsEval( 1 );
+ Trace("strings-process-debug") << "Done check extended functions re-eval, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+ if( !hasProcessed() ){
+ if( !options::stringEagerLen() ){
+ checkLengthsEqc();
+ if( hasProcessed() ){
+ return;
+ }
+ }
+ //process disequalities between equivalence classes
+ checkDeqNF();
+ Trace("strings-process-debug") << "Done check disequalities, addedFact = " << !d_pending.empty() << " " << !d_lemma_cache.empty() << ", d_conflict = " << d_conflict << std::endl;
+ }
+ }
+ Trace("strings-solve") << "Finished check normal forms, #lemmas = " << d_lemma_cache.size() << ", conflict = " << d_conflict << std::endl;
+}
+
void TheoryStrings::checkDeqNF() {
if( !d_conflict && d_lemma_cache.empty() ){
std::vector< std::vector< Node > > cols;
}
void TheoryStrings::checkExtendedFuncsEval( int effort ) {
+ Trace("strings-extf-list") << "Active extended functions, effort=" << effort << " : " << std::endl;
if( effort==0 ){
d_extf_vars.clear();
}
+ d_extf_pol.clear();
d_extf_exp.clear();
d_extf_info.clear();
Trace("strings-extf-debug") << "Checking " << d_ext_func_terms.size() << " extended functions." << std::endl;
for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
if( (*it).second ){
Node n = (*it).first;
- int n_pol = 0;
+ d_extf_pol[n] = 0;
if( n.getType().isBoolean() ){
if( areEqual( n, d_true ) ){
- n_pol = 1;
+ d_extf_pol[n] = 1;
}else if( areEqual( n, d_false ) ){
- n_pol = -1;
+ d_extf_pol[n] = -1;
}
}
- Trace("strings-extf-debug") << "Check extf " << n << "..." << std::endl;
+ Trace("strings-extf-debug") << "Check extf " << n << ", pol = " << d_extf_pol[n] << "..." << std::endl;
if( effort==0 ){
std::map< Node, bool > visited;
collectVars( n, d_extf_vars[n], visited );
return;
}
}
- }else if( ( nrc.getKind()==kind::OR && n_pol==-1 ) || ( nrc.getKind()==kind::AND && n_pol==1 ) ){
+ }else if( ( nrc.getKind()==kind::OR && d_extf_pol[n]==-1 ) || ( nrc.getKind()==kind::AND && d_extf_pol[n]==1 ) ){
//infer the consequence of each
d_ext_func_terms[n] = false;
- d_extf_exp[n].push_back( n_pol==-1 ? n.negate() : n );
+ d_extf_exp[n].push_back( d_extf_pol[n]==-1 ? n.negate() : n );
Trace("strings-extf-debug") << " decomposable..." << std::endl;
- Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << n_pol << std::endl;
+ Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << ", pol = " << d_extf_pol[n] << std::endl;
for( unsigned i=0; i<nrc.getNumChildren(); i++ ){
- sendInfer( mkAnd( d_extf_exp[n] ), n_pol==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
+ sendInfer( mkAnd( d_extf_exp[n] ), d_extf_pol[n]==-1 ? nrc[i].negate() : nrc[i], effort==0 ? "EXTF_d" : "EXTF_d-N" );
}
}else{
to_reduce = nrc;
to_reduce = n;
}
if( !to_reduce.isNull() ){
- checkExtfInference( n, to_reduce, n_pol, effort );
+ checkExtfInference( n, to_reduce, effort );
if( effort==1 ){
Trace("strings-extf") << " cannot rewrite extf : " << to_reduce << std::endl;
}
+ if( Trace.isOn("strings-extf-list") ){
+ Trace("strings-extf-list") << " * " << to_reduce;
+ if( d_extf_pol[n]!=0 ){
+ Trace("strings-extf-list") << ", pol = " << d_extf_pol[n];
+ }
+ if( n!=to_reduce ){
+ Trace("strings-extf-list") << ", from " << n;
+ }
+ Trace("strings-extf-list") << std::endl;
+ }
}
}else{
Trace("strings-extf-debug") << " already reduced " << (*it).first << std::endl;
}
}
- /*
- for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
- if( (*it).second ){
-
- }
- }
- */
+ //for( NodeBoolMap::iterator it = d_ext_func_terms.begin(); it != d_ext_func_terms.end(); ++it ){
+ // if( (*it).second ){
+ // }
+ //}
}
-void TheoryStrings::checkExtfInference( Node n, Node nr, int n_pol, int effort ){
+void TheoryStrings::checkExtfInference( Node n, Node nr, int effort ){
+ int n_pol = d_extf_pol[n];
if( n_pol!=0 ){
//add original to explanation
d_extf_exp[n].push_back( n_pol==1 ? n : n.negate() );
Assert( effort==0 || nr[0]==getRepresentative( nr[0] ) );
bool pol = n_pol==1;
if( std::find( d_extf_info[nr[0]].d_ctn[pol].begin(), d_extf_info[nr[0]].d_ctn[pol].end(), nr[1] )==d_extf_info[nr[0]].d_ctn[pol].end() ){
+ Trace("strings-extf-debug") << " store contains info : " << nr[0] << " " << pol << " " << nr[1] << std::endl;
d_extf_info[nr[0]].d_ctn[pol].push_back( nr[1] );
d_extf_info[nr[0]].d_ctn_from[pol].push_back( n );
+ //transitive closure for contains
+ bool opol = !pol;
+ for( unsigned i=0; i<d_extf_info[nr[0]].d_ctn[opol].size(); i++ ){
+ Node onr = d_extf_info[nr[0]].d_ctn[opol][i];
+ Node conc = NodeManager::currentNM()->mkNode( kind::STRING_STRCTN, pol ? nr[1] : onr, pol ? onr : nr[1] ).negate();
+ std::vector< Node > exp;
+ exp.insert( exp.end(), d_extf_exp[n].begin(), d_extf_exp[n].end() );
+ Node ofrom = d_extf_info[nr[0]].d_ctn_from[opol][i];
+ Assert( d_extf_exp.find( ofrom )!=d_extf_exp.end() );
+ exp.insert( exp.end(), d_extf_exp[ofrom].begin(), d_extf_exp[ofrom].end() );
+ sendInfer( mkAnd( exp ), conc, "CTN_Trans" );
+ }
}else{
Trace("strings-extf-debug") << " redundant." << std::endl;
d_ext_func_terms[n] = false;
//// Finite Model Finding
Node TheoryStrings::getNextDecisionRequest() {
- if(d_opt_fmf && !d_conflict) {
+ if( options::stringFMF() && !d_conflict ){
Node in_var_lsum = d_input_var_lsum.get();
//Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl;
//initialize the term we will minimize
return Node::null();
}
-void TheoryStrings::assertNode( Node lit ) {
-}
-
void TheoryStrings::collectExtendedFuncTerms( Node n, std::map< Node, bool >& visited ) {
if( visited.find( n )==visited.end() ){
visited[n] = true;
Node d_one;
CVC4::Rational RMAXINT;
unsigned d_card_size;
- // Options
- bool d_opt_fmf;
- bool d_opt_regexp_gcd;
// Helper functions
Node getRepresentative( Node t );
bool hasTerm( Node a );
NodeSet d_extf_infer_cache;
bool doPreprocess( Node atom );
- bool hasProcessed();
- void addToExplanation( Node a, Node b, std::vector< Node >& exp );
- void addToExplanation( Node lit, std::vector< Node >& exp );
+
private:
NodeSet d_congruent;
NodeNodeMap d_proxy_var;
NodeNodeMap d_proxy_var_to_length;
private:
+
+ //initial check
+ void checkInit();
+ void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
+ //extended functions evaluation check
+ void checkExtendedFuncsEval( int effort = 0 );
+ void checkExtfInference( Node n, Node nr, int effort );
+ void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited );
+ Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
+ //flat forms check
+ void checkFlatForms();
+ Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
+ //normal forms check
+ void checkNormalForms();
void mergeCstVec(std::vector< Node > &vec_strings);
bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf,
std::vector< std::vector< Node > > &normal_forms,
bool processDeq( Node n1, Node n2 );
int processReverseDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj );
int processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >& nfj, Node ni, Node nj, unsigned& index, bool isRev );
- //bool unrollStar( Node atom );
- Node mkRegExpAntec(Node atom, Node ant);
-
- void checkInit();
- void checkConstantEquivalenceClasses( TermIndex* ti, std::vector< Node >& vecc );
- void checkExtendedFuncsEval( int effort = 0 );
- void checkExtfInference( Node n, Node nr, int n_pol, int effort );
- void collectVars( Node n, std::map< Node, std::vector< Node > >& vars, std::map< Node, bool >& visited );
- void checkFlatForms();
- void checkNormalForms();
- Node checkCycles( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp );
void checkDeqNF();
- void checkLengthsEqc();
- void checkCardinality();
- bool checkInductiveEquations();
+
+ //check for extended functions
+ void checkExtendedFuncs();
//check membership constraints
+ Node mkRegExpAntec(Node atom, Node ant);
Node normalizeRegexp(Node r);
bool normalizePosMemberships(std::map< Node, std::vector< Node > > &memb_with_exps);
bool applyRConsume( CVC4::String &s, Node &r);
std::map< Node, std::vector< Node > > &memb_with_exps,
std::map< Node, std::vector< Node > > &XinR_with_exps);
void checkMemberships();
- //temp
bool checkMemberships2();
bool checkPDerivative(Node x, Node r, Node atom, bool &addedLemma,
std::vector< Node > &processed, std::vector< Node > &cprocessed,
std::vector< Node > &nf_exp);
- void checkExtendedFuncs();
+ //check contains
void checkPosContains( std::vector< Node >& posContains );
void checkNegContains( std::vector< Node >& negContains );
- Node getSymbolicDefinition( Node n, std::vector< Node >& exp );
-
+ //lengths normalize check
+ void checkLengthsEqc();
+ //cardinality check
+ void checkCardinality();
+
public:
+ /** preregister term */
void preRegisterTerm(TNode n);
+ /** Expand definition */
Node expandDefinition(LogicRequest &logicRequest, Node n);
+ /** Check at effort e */
void check(Effort e);
-
/** Conflict when merging two constants */
void conflict(TNode a, TNode b);
/** called when a new equivalence class is created */
protected:
/** compute care graph */
void computeCareGraph();
-
+
//do pending merges
void assertPendingFact(Node atom, bool polarity, Node exp);
void doPendingFacts();
void doPendingLemmas();
-
+ bool hasProcessed();
+ void addToExplanation( Node a, Node b, std::vector< Node >& exp );
+ void addToExplanation( Node lit, std::vector< Node >& exp );
+
//register term
bool registerTerm( Node n );
//send lemma
//extended string terms and whether they have been reduced
NodeBoolMap d_ext_func_terms;
std::map< Node, std::map< Node, std::vector< Node > > > d_extf_vars;
+ // list of terms that something (does not) contain and their explanation
class ExtfInfo {
public:
std::map< bool, std::vector< Node > > d_ctn;
std::map< bool, std::vector< Node > > d_ctn_from;
};
+ std::map< Node, int > d_extf_pol;
std::map< Node, std::vector< Node > > d_extf_exp;
std::map< Node, ExtfInfo > d_extf_info;
//collect extended operator terms
public:
//for finite model finding
Node getNextDecisionRequest();
- void assertNode( Node lit );
public:
/** statistics class */
/*! \file theory_strings_preprocess.cpp
** \verbatim
** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Andrew Reynolds
+ ** Major contributors: Andrew Reynolds
+ ** Minor contributors (to current version): Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) );
}
-void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &ret ) {
- int k = r.getKind();
+void StringsPreprocess::processRegExp( Node s, Node r, std::vector< Node > &new_nodes ) {
+ CVC4::Kind k = r.getKind();
switch( k ) {
- 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_RANGE: {
Node one = NodeManager::currentNM()->mkConst( ::CVC4::Rational(1) );
Node eq = one.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s));
- ret.push_back( eq );
- eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
- ret.push_back( eq );
- break;
- }
- 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 {
- flag = false;
- break;
- }
- }
- 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_UNION: {
- std::vector< Node > c_or;
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- 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);
- ret.push_back( eq );
- break;
- }
- case kind::REGEXP_INTER: {
- for(unsigned i=0; i<r.getNumChildren(); ++i) {
- processRegExp( s, r[i], ret );
- }
- break;
- }
- 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 );
- }
+ new_nodes.push_back( eq );
break;
}
+ case kind::REGEXP_STAR:
+ case kind::REGEXP_CONCAT:
case kind::REGEXP_LOOP: {
- Node eq = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, s, r );
- ret.push_back( eq );
+ //do nothing
break;
}
default: {
- Trace("strings-error") << "Unsupported term: " << r << " in simplifyRegExp." << std::endl;
+ //all others should be rewritten by now
+ Trace("strings-error") << "Unsupported term: " << r << " in processRegExp." << std::endl;
Assert( false, "Unsupported Term" );
}
}
}
-bool StringsPreprocess::checkStarPlus( Node t ) {
- if( t.getKind() != kind::REGEXP_STAR && t.getKind() != kind::REGEXP_PLUS ) {
- for( unsigned i = 0; i<t.getNumChildren(); ++i ) {
- if( checkStarPlus(t[i]) ){
- return true;
- }
- }
- return false;
- } else {
- return true;
- }
-}
+/*
int StringsPreprocess::checkFixLenVar( Node t ) {
int ret = 2;
if(t.getKind() == kind::EQUAL) {
}
return ret;
}
-Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes, bool during_pp ) {
+*/
+Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
NodeNodeMap::const_iterator i = d_cache.find(t);
if(i != d_cache.end()) {
return (*i).second.isNull() ? t : (*i).second;
Trace("strings-preprocess") << "StringsPreprocess::simplify: " << t << std::endl;
Node retNode = t;
- if( options::stringLazyPreproc() ){
- //only process extended operators after preprocess
- if( during_pp && ( t.getKind() == kind::STRING_SUBSTR || t.getKind() == kind::STRING_STRIDOF ||
- t.getKind() == kind::STRING_ITOS || t.getKind() == kind::STRING_U16TOS || t.getKind() == kind::STRING_U32TOS ||
- t.getKind() == kind::STRING_STOI || t.getKind() == kind::STRING_STOU16 || t.getKind() == kind::STRING_STOU32 ||
- t.getKind() == kind::STRING_STRREPL ) ){
- return t;
- }
- }
/*int c_id = checkFixLenVar(t);
if( c_id != 2 ) {
}
} else */
if( t.getKind() == kind::STRING_IN_REGEXP ) {
- Node t0 = simplify( t[0], new_nodes, during_pp );
-
- //rewrite it
+ //process any reductions
std::vector< Node > ret;
- processRegExp( t0, t[1], ret );
-
- 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;
+ processRegExp( t[0], t[1], ret );
+ Node conc;
+ if( !ret.empty() ){
+ conc = ret.size()==1 ? ret[0] : NodeManager::currentNM()->mkNode( kind::AND, ret );
+ }
+ if( options::stringLazyPreproc() ){
+ //implication as lemma
+ if( !conc.isNull() ){
+ new_nodes.push_back( NodeManager::currentNM()->mkNode( kind::IMPLIES, t, conc ) );
+ }
+ d_cache[t] = t;
+ }else{
+ //rewrite as conjunction
+ Node n = t;
+ if( !conc.isNull() ){
+ n = NodeManager::currentNM()->mkNode( kind::AND, t, conc );
+ n = Rewriter::rewrite( n );
+ }
+ d_cache[t] = n;
+ retNode = n;
+ }
} else if( t.getKind() == kind::STRING_SUBSTR ) {
/*
Node lenxgti = NodeManager::currentNM()->mkNode( kind::GEQ,
return retNode;
}
-Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes, bool during_pp) {
+Node StringsPreprocess::decompose(Node t, std::vector< Node > & new_nodes) {
NodeNodeMap::const_iterator i = d_cache.find(t);
if(i != d_cache.end()) {
return (*i).second.isNull() ? t : (*i).second;
unsigned num = t.getNumChildren();
if(num == 0) {
- return simplify(t, new_nodes, during_pp);
+ return simplify(t, new_nodes);
} else {
bool changed = false;
std::vector< Node > cc;
cc.push_back(t.getOperator());
}
for(unsigned i=0; i<t.getNumChildren(); i++) {
- Node s = decompose(t[i], new_nodes, during_pp);
+ Node s = decompose(t[i], new_nodes);
cc.push_back( s );
if(s != t[i]) {
changed = true;
}
if(changed) {
Node tmp = NodeManager::currentNM()->mkNode( t.getKind(), cc );
- return simplify(tmp, new_nodes, during_pp);
+ return simplify(tmp, new_nodes);
} else {
- return simplify(t, new_nodes, during_pp);
+ return simplify(t, new_nodes);
}
}
}
void StringsPreprocess::simplify(std::vector< Node > &vec_node) {
for( unsigned i=0; i<vec_node.size(); i++ ){
std::vector< Node > new_nodes;
- Node curr = decompose( vec_node[i], new_nodes, true );
+ Node curr = decompose( vec_node[i], new_nodes );
if( !new_nodes.empty() ){
new_nodes.insert( new_nodes.begin(), curr );
curr = NodeManager::currentNM()->mkNode( kind::AND, new_nodes );
/*! \file theory_strings_preprocess.h
** \verbatim
** Original author: Tianyi Liang
- ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): Andrew Reynolds
+ ** Major contributors: Morgan Deters, Andrew Reynolds
+ ** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
//Constants
Node d_zero;
private:
- bool checkStarPlus( Node t );
- int checkFixLenVar( Node t );
- void processRegExp( Node s, Node r, std::vector< Node > &ret );
- Node simplify( Node t, std::vector< Node > &new_nodes, bool during_pp );
+ //int checkFixLenVar( Node t );
+ void processRegExp( Node s, Node r, std::vector< Node > &new_nodes );
+ Node simplify( Node t, std::vector< Node > &new_nodes );
public:
StringsPreprocess( context::UserContext* u );
- Node decompose( Node t, std::vector< Node > &new_nodes, bool during_pp = false );
+ Node decompose( Node t, std::vector< Node > &new_nodes );
void simplify(std::vector< Node > &vec_node);
};
Trace("strings-prerewrite") << "Strings::prerewriteOrRegExp start " << node << std::endl;
Node retNode = node;
std::vector<Node> node_vec;
- bool emptyflag = false;
//Node allNode = Node::null();
for(unsigned i=0; i<node.getNumChildren(); ++i) {
if(node[i].getKind() == kind::REGEXP_INTER) {
}
}
} else if(tmpNode.getKind() == kind::REGEXP_EMPTY) {
- emptyflag = true;
retNode = tmpNode;
break;
} else if(tmpNode.getKind() == kind::REGEXP_STAR && tmpNode[0].getKind() == kind::REGEXP_SIGMA) {
}
}
} else if(node[i].getKind() == kind::REGEXP_EMPTY) {
- emptyflag = true;
retNode = node[i];
break;
} else if(node[i].getKind() == kind::REGEXP_STAR && node[i][0].getKind() == kind::REGEXP_SIGMA) {
}
}
}
- if(!emptyflag) {
+ if( retNode==node ){
std::vector< Node > nvec;
retNode = node_vec.size() == 0 ?
NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, NodeManager::currentNM()->mkNode(kind::REGEXP_SIGMA, nvec)) :
retNode = NodeManager::currentNM()->mkConst( true );
}
}else if( r.getKind() == kind::REGEXP_CONCAT ){
- bool flag = true;
+ bool allSigma = true;
+ bool allString = true;
+ std::vector< Node > cc;
for(unsigned i=0; i<r.getNumChildren(); i++) {
Assert( r[i].getKind() != kind::REGEXP_EMPTY );
if( r[i].getKind() != kind::REGEXP_SIGMA ){
- flag = false;
- break;
+ allSigma = false;
+ }
+ if( r[i].getKind() != kind::STRING_TO_REGEXP ){
+ allString = false;
+ }else{
+ cc.push_back( r[i] );
}
}
- if( flag ){
+ if( allSigma ){
Node num = NodeManager::currentNM()->mkConst( ::CVC4::Rational( r.getNumChildren() ) );
retNode = num.eqNode(NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, x));
+ }else if( allString ){
+ retNode = x.eqNode( mkConcat( kind::STRING_CONCAT, cc ) );
+ }
+ }else if( r.getKind()==kind::REGEXP_INTER || r.getKind()==kind::REGEXP_UNION ){
+ std::vector< Node > mvec;
+ for( unsigned i=0; i<r.getNumChildren(); i++ ){
+ mvec.push_back( NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, x, r[i] ) );
}
+ retNode = NodeManager::currentNM()->mkNode( r.getKind()==kind::REGEXP_INTER ? kind::AND : kind::OR, mvec );
}else if(r.getKind() == kind::STRING_TO_REGEXP) {
retNode = x.eqNode(r[0]);
}else if(x != node[0] || r != node[1]) {
projects / cvc5.git / commitdiff