diff options
Diffstat (limited to 'src/theory/strings')
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 511 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 23 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 1 |
6 files changed, 348 insertions, 196 deletions
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 53344dd6c..a665a02c1 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -39,6 +39,10 @@ RegExpOpr::RegExpOpr() d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ); } +RegExpOpr::~RegExpOpr(){ + +} + int RegExpOpr::gcd ( int a, int b ) { int c; while ( a != 0 ) { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index c537553f2..075391370 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -99,6 +99,7 @@ private: public: RegExpOpr(); + ~RegExpOpr(); bool checkConstRegExp( Node r ); void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index b3e1925ae..57344236e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -28,6 +28,7 @@ #include "theory/strings/type_enumerator.h" #include "theory/theory_model.h" #include "theory/valuation.h" +#include "theory/quantifiers/term_database.h" using namespace std; using namespace CVC4::context; @@ -74,9 +75,11 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, d_preproc(u), d_preproc_cache(u), d_extf_infer_cache(c), + d_ee_disequalities(c), d_congruent(c), d_proxy_var(u), d_proxy_var_to_length(u), + d_functionsTerms(c), d_neg_ctn_eqlen(c), d_neg_ctn_ulen(c), d_neg_ctn_cached(u), @@ -124,7 +127,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, } TheoryStrings::~TheoryStrings() { - + for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ + delete it->second; + } } Node TheoryStrings::getRepresentative( Node t ) { @@ -467,18 +472,30 @@ void TheoryStrings::preRegisterTerm(TNode n) { break; } default: { - if( n.getType().isString() ) { + TypeNode tn = n.getType(); + if( tn.isString() ) { registerTerm( n, 0 ); // FMF if( n.getKind() == kind::VARIABLE && options::stringFMF() ){ d_input_vars.insert(n); } - } else if (n.getType().isBoolean()) { + d_equalityEngine.addTerm(n); + } else if (tn.isBoolean()) { // Get triggered for both equal and dis-equal d_equalityEngine.addTriggerPredicate(n); } else { // Function applications/predicates d_equalityEngine.addTerm(n); + if( options::stringExp() ){ + //collect extended functions here: some may not be asserted to strings (such as those with return type Int), + // but we need to record them so they are treated properly + std::map< Node, bool > visited; + collectExtendedFuncTerms( n, visited ); + } + } + //concat terms do not contribute to theory combination? TODO: verify + if( n.hasOperator() && kindToTheoryId( n.getKind() )==THEORY_STRINGS && n.getKind()!=kind::STRING_CONCAT ){ + d_functionsTerms.push_back( n ); } } } @@ -486,6 +503,7 @@ void TheoryStrings::preRegisterTerm(TNode n) { } Node TheoryStrings::expandDefinition(LogicRequest &logicRequest, Node node) { + Trace("strings-exp-def") << "TheoryStrings::expandDefinition : " << node << std::endl; return node; } @@ -740,53 +758,23 @@ void TheoryStrings::eqNotifyNewClass(TNode t){ /** called when two equivalance classes will merge */ void TheoryStrings::eqNotifyPreMerge(TNode t1, TNode t2){ - EqcInfo * e2 = getOrMakeEqcInfo(t2, false); - if( e2 ){ - EqcInfo * e1 = getOrMakeEqcInfo( t1 ); - //add information from e2 to e1 - if( !e2->d_const_term.get().isNull() ){ - e1->d_const_term.set( e2->d_const_term ); - } - if( !e2->d_length_term.get().isNull() ){ - e1->d_length_term.set( e2->d_length_term ); - } - if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) { - e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k ); - } - if( !e2->d_normalized_length.get().isNull() ){ - e1->d_normalized_length.set( e2->d_normalized_length ); - } + EqcInfo * e2 = getOrMakeEqcInfo(t2, false); + if( e2 ){ + EqcInfo * e1 = getOrMakeEqcInfo( t1 ); + //add information from e2 to e1 + if( !e2->d_const_term.get().isNull() ){ + e1->d_const_term.set( e2->d_const_term ); } - /* - if( hasTerm( d_zero ) ){ - Node leqc; - if( areEqual(d_zero, t1) ){ - leqc = t2; - }else if( areEqual(d_zero, t2) ){ - leqc = t1; - } - if( !leqc.isNull() ){ - //scan equivalence class to see if we apply - eq::EqClassIterator eqc_i = eq::EqClassIterator( leqc, &d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Node n = (*eqc_i); - if( n.getKind()==kind::STRING_LENGTH ){ - if( !hasTerm( d_emptyString ) || !areEqual(n[0], d_emptyString ) ){ - //apply the rule length(n[0])==0 => n[0] == "" - Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, n[0], d_emptyString ); - d_pending.push_back( eq ); - Node eq_exp = NodeManager::currentNM()->mkNode( kind::EQUAL, n, d_zero ); - d_pending_exp[eq] = eq_exp; - Trace("strings-infer") << "Strings : Infer Empty : " << eq << " from " << eq_exp << std::endl; - d_infer.push_back(eq); - d_infer_exp.push_back(eq_exp); - } - } - ++eqc_i; - } - } + if( !e2->d_length_term.get().isNull() ){ + e1->d_length_term.set( e2->d_length_term ); + } + if( e2->d_cardinality_lem_k.get()>e1->d_cardinality_lem_k.get() ) { + e1->d_cardinality_lem_k.set( e2->d_cardinality_lem_k ); } - */ + if( !e2->d_normalized_length.get().isNull() ){ + e1->d_normalized_length.set( e2->d_normalized_length ); + } + } } /** called when two equivalance classes have merged */ @@ -796,11 +784,106 @@ void TheoryStrings::eqNotifyPostMerge(TNode t1, TNode t2) { /** called when two equivalance classes are disequal */ void TheoryStrings::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + if( t1.getType().isString() ){ + //store disequalities between strings, may need to check if their lengths are equal/disequal + d_ee_disequalities.push_back( t1.eqNode( t2 ) ); + } +} +void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ) { + if( depth==arity ){ + if( t2!=NULL ){ + Node f1 = t1->getNodeData(); + Node f2 = t2->getNodeData(); + if( !d_equalityEngine.areEqual( f1, f2 ) ){ + Trace("strings-cg-debug") << "TheoryStrings::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; + vector< pair<TNode, TNode> > currentPairs; + for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { + TNode x = f1[k]; + TNode y = f2[k]; + Assert( d_equalityEngine.hasTerm(x) ); + Assert( d_equalityEngine.hasTerm(y) ); + Assert( !d_equalityEngine.areDisequal( x, y, false ) ); + if( !d_equalityEngine.areEqual( x, y ) ){ + if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){ + TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS); + TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS); + EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared); + if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){ + //an argument is disequal, we are done + return; + }else{ + currentPairs.push_back(make_pair(x_shared, y_shared)); + } + } + } + } + for (unsigned c = 0; c < currentPairs.size(); ++ c) { + Trace("strings-cg-pair") << "TheoryStrings::computeCareGraph(): pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; + Trace("ajr-temp") << currentPairs[c].first << ", " << currentPairs[c].second << std::endl; + addCarePair(currentPairs[c].first, currentPairs[c].second); + } + } + } + }else{ + if( t2==NULL ){ + if( depth<(arity-1) ){ + //add care pairs internal to each child + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ + addCarePairs( &it->second, NULL, arity, depth+1 ); + } + } + //add care pairs based on each pair of non-disequal arguments + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ + std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it; + ++it2; + for( ; it2 != t1->d_data.end(); ++it2 ){ + if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ + addCarePairs( &it->second, &it2->second, arity, depth+1 ); + } + } + } + }else{ + //add care pairs based on product of indices, non-disequal arguments + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){ + if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ + addCarePairs( &it->second, &it2->second, arity, depth+1 ); + } + } + } + } + } } void TheoryStrings::computeCareGraph(){ - Theory::computeCareGraph(); + //computing the care graph here is probably still necessary, due to operators that take non-string arguments TODO: verify + Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl; + std::map< Node, quantifiers::TermArgTrie > index; + std::map< Node, unsigned > arity; + unsigned functionTerms = d_functionsTerms.size(); + for (unsigned i = 0; i < functionTerms; ++ i) { + TNode f1 = d_functionsTerms[i]; + Trace("strings-cg") << "...build for " << f1 << std::endl; + Node op = f1.getOperator(); + std::vector< TNode > reps; + bool has_trigger_arg = false; + for( unsigned j=0; j<f1.getNumChildren(); j++ ){ + reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) ); + if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_STRINGS ) ){ + has_trigger_arg = true; + } + } + if( has_trigger_arg ){ + index[op].addTerm( f1, reps ); + arity[op] = reps.size(); + } + } + //for each index + for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){ + Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index " << itii->first << "..." << std::endl; + addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 ); + } } void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) { @@ -1136,8 +1219,12 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { }else{ if( !areEqual( n, nrc ) ){ if( n.getType().isBoolean() ){ - d_extf_exp[n].push_back( nrc==d_true ? n.negate() : n ); - conc = d_false; + if( areEqual( n, nrc==d_true ? d_false : d_true ) ){ + d_extf_exp[n].push_back( nrc==d_true ? n.negate() : n ); + conc = d_false; + }else{ + conc = nrc==d_true ? n : n.negate(); + } }else{ conc = n.eqNode( nrc ); } @@ -1145,7 +1232,7 @@ void TheoryStrings::checkExtendedFuncsEval( int effort ) { } if( !conc.isNull() ){ Trace("strings-extf") << " resolve extf : " << nr << " -> " << nrc << std::endl; - sendInference( d_extf_exp[n], conc, effort==0 ? "EXTF" : "EXTF-N", n.getType().isInteger() || d_extf_exp[n].empty() ); + sendInference( d_extf_exp[n], conc, effort==0 ? "EXTF" : "EXTF-N", true ); if( d_conflict ){ Trace("strings-extf-debug") << " conflict, return." << std::endl; return; @@ -1745,9 +1832,9 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & n } nf.insert( nf.end(), normal_forms[nf_index].begin(), normal_forms[nf_index].end() ); nf_exp.insert( nf_exp.end(), normal_forms_exp[nf_index].begin(), normal_forms_exp[nf_index].end() ); - //if( eqc!=normal_form_src[nf_index] ){ - // nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) ); - //} + if( eqc!=normal_form_src[nf_index] ){ + nf_exp.push_back( eqc.eqNode( normal_form_src[nf_index] ) ); + } Trace("strings-solve-debug2") << "take normal form ... done" << std::endl; d_normal_forms_base[eqc] = normal_form_src[nf_index]; //*/ @@ -2639,23 +2726,17 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){ if( !isNormalFormPair( n1, n2 ) ){ - //Assert( !isNormalFormPair( n1, n2 ) ); - NodeList* lst; - NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); - if( nf_i == d_nf_pairs.end() ){ - if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){ - addNormalFormPair( n2, n1 ); - return; - } - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_nf_pairs.insertDataFromContextMemory( n1, lst ); - Trace("strings-nf") << "Create cache for " << n1 << std::endl; - } else { - lst = (*nf_i).second; - } - Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl; - lst->push_back( n2 ); + int index = 0; + NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + } + d_nf_pairs[n1] = index + 1; + if( index<(int)d_nf_pairs_data[n1].size() ){ + d_nf_pairs_data[n1][index] = n2; + }else{ + d_nf_pairs_data[n1].push_back( n2 ); + } Assert( isNormalFormPair( n1, n2 ) ); } else { Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl; @@ -2668,15 +2749,14 @@ bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) { } bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { - //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; - NodeList* lst; - NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); - if( nf_i != d_nf_pairs.end() ) { - lst = (*nf_i).second; - for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) { - Node n = *i; - if( n==n2 ) { - return true; + //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; + NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); + if( it!=d_nf_pairs.end() ){ + Assert( d_nf_pairs_data.find( n1 )!=d_nf_pairs_data.end() ); + for( int i=0; i<(*it).second; i++ ){ + Assert( i<(int)d_nf_pairs_data[n1].size() ); + if( d_nf_pairs_data[n1][i]==n2 ){ + return true; } } } @@ -2752,7 +2832,7 @@ void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node > eq = eq.isNull() ? d_false : Rewriter::rewrite( eq ); if( eq!=d_true ){ if( Trace.isOn("strings-infer-debug") ){ - Trace("strings-infer-debug") << "infer : " << eq << " from: " << std::endl; + Trace("strings-infer-debug") << "By " << c << ", infer : " << eq << " from: " << std::endl; for( unsigned i=0; i<exp.size(); i++ ){ Trace("strings-infer-debug") << " " << exp[i] << std::endl; } @@ -2761,8 +2841,8 @@ void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node > } //Trace("strings-infer-debug") << "as lemma : " << asLemma << std::endl; } - bool doSendLemma = ( asLemma || eq==d_false || eq.getKind()==kind::OR || options::stringInferAsLemmas() ); - if( doSendLemma ){ + //check if we should send a lemma or an inference + if( asLemma || eq==d_false || eq.getKind()==kind::OR || !exp_n.empty() || options::stringInferAsLemmas() ){ Node eq_exp; if( options::stringRExplainLemmas() ){ eq_exp = mkExplain( exp, exp_n ); @@ -2780,7 +2860,6 @@ void TheoryStrings::sendInference( std::vector< Node >& exp, std::vector< Node > } sendLemma( eq_exp, eq, c ); }else{ - Assert( exp_n.empty() ); sendInfer( mkAnd( exp ), eq, c ); } } @@ -3064,30 +3143,56 @@ void TheoryStrings::getConcatVec( Node n, std::vector< Node >& c ) { void TheoryStrings::checkDeqNF() { std::vector< std::vector< Node > > cols; std::vector< Node > lts; - separateByLength( d_strings_eqc, cols, lts ); - for( unsigned i=0; i<cols.size(); i++ ){ - if( cols[i].size()>1 && d_lemma_cache.empty() ){ - Trace("strings-solve") << "- Verify disequalities are processed for " << cols[i][0]; - printConcat( d_normal_forms[cols[i][0]], "strings-solve" ); - Trace("strings-solve") << "... #eql = " << cols[i].size() << std::endl; - //must ensure that normal forms are disequal - for( unsigned j=0; j<cols[i].size(); j++ ){ - for( unsigned k=(j+1); k<cols[i].size(); k++ ){ - if( areDisequal( cols[i][j], cols[i][k] ) ){ - Assert( !d_conflict ); - //if( !areDisequal( cols[i][j], cols[i][k] ) ){ - // sendSplit( cols[i][j], cols[i][k], "D-NORM", true ); - // return; - //}else{ - Trace("strings-solve") << "- Compare " << cols[i][j] << " "; - printConcat( d_normal_forms[cols[i][j]], "strings-solve" ); - Trace("strings-solve") << " against " << cols[i][k] << " "; - printConcat( d_normal_forms[cols[i][k]], "strings-solve" ); - Trace("strings-solve") << "..." << std::endl; - if( processDeq( cols[i][j], cols[i][k] ) ){ - return; + std::map< Node, std::map< Node, bool > > processed; + + //for each pair of disequal strings, must determine whether their lengths are equal or disequal + bool addedLSplit = false; + for( NodeList::const_iterator id = d_ee_disequalities.begin(); id != d_ee_disequalities.end(); ++id ) { + Node eq = *id; + Node n[2]; + for( unsigned i=0; i<2; i++ ){ + n[i] = d_equalityEngine.getRepresentative( eq[i] ); + } + if( processed[n[0]].find( n[1] )==processed[n[0]].end() ){ + processed[n[0]][n[1]] = true; + Node lt[2]; + for( unsigned i=0; i<2; i++ ){ + EqcInfo* ei = getOrMakeEqcInfo( n[i], false ); + lt[i] = ei ? ei->d_length_term : Node::null(); + if( lt[i].isNull() ){ + lt[i] = eq[i]; + } + lt[i] = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt[i] ); + } + if( !areEqual( lt[0], lt[1] ) && !areDisequal( lt[0], lt[1] ) ){ + addedLSplit = true; + sendSplit( lt[0], lt[1], "DEQ-LENGTH-SP" ); + } + } + } + + if( !addedLSplit ){ + separateByLength( d_strings_eqc, cols, lts ); + for( unsigned i=0; i<cols.size(); i++ ){ + if( cols[i].size()>1 && d_lemma_cache.empty() ){ + Trace("strings-solve") << "- Verify disequalities are processed for " << cols[i][0] << ", normal form : "; + printConcat( d_normal_forms[cols[i][0]], "strings-solve" ); + Trace("strings-solve") << "... #eql = " << cols[i].size() << std::endl; + //must ensure that normal forms are disequal + for( unsigned j=0; j<cols[i].size(); j++ ){ + for( unsigned k=(j+1); k<cols[i].size(); k++ ){ + //for strings that are disequal, but have the same length + if( areDisequal( cols[i][j], cols[i][k] ) ){ + Assert( !d_conflict ); + Trace("strings-solve") << "- Compare " << cols[i][j] << " "; + printConcat( d_normal_forms[cols[i][j]], "strings-solve" ); + Trace("strings-solve") << " against " << cols[i][k] << " "; + printConcat( d_normal_forms[cols[i][k]], "strings-solve" ); + Trace("strings-solve") << "..." << std::endl; + if( processDeq( cols[i][j], cols[i][k] ) ){ + return; + } } - //} } } } @@ -3149,6 +3254,9 @@ void TheoryStrings::checkCardinality() { //int cardinality = options::stringCharCardinality(); //Trace("strings-solve-debug2") << "get cardinality: " << cardinality << endl; + //AJR: this will create a partition of eqc, where each collection has length that are pairwise propagated to be equal. + // we do not require disequalities between the lengths of each collection, since we split on disequalities between lengths of string terms that are disequal (DEQ-LENGTH-SP). + // TODO: revisit this? std::vector< std::vector< Node > > cols; std::vector< Node > lts; separateByLength( d_strings_eqc, cols, lts ); @@ -3159,54 +3267,51 @@ void TheoryStrings::checkCardinality() { if( cols[i].size() > 1 ) { // size > c^k unsigned card_need = 1; - double curr = (double)cols[i].size()-1; + double curr = (double)cols[i].size(); while( curr>d_card_size ){ curr = curr/(double)d_card_size; card_need++; } + Trace("strings-card") << "Need length " << card_need << " for this number of strings (where alphabet size is " << d_card_size << ")." << std::endl; Node cmp = NodeManager::currentNM()->mkNode( kind::GEQ, lr, NodeManager::currentNM()->mkConst( Rational( card_need ) ) ); cmp = Rewriter::rewrite( cmp ); if( cmp!=d_true ){ unsigned int int_k = (unsigned int)card_need; - bool allDisequal = true; for( std::vector< Node >::iterator itr1 = cols[i].begin(); itr1 != cols[i].end(); ++itr1) { for( std::vector< Node >::iterator itr2 = itr1 + 1; itr2 != cols[i].end(); ++itr2) { if(!areDisequal( *itr1, *itr2 )) { - allDisequal = false; // add split lemma sendSplit( *itr1, *itr2, "CARD-SP" ); return; } } } - if( allDisequal ){ - EqcInfo* ei = getOrMakeEqcInfo( lr, true ); - Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; - if( int_k+1 > ei->d_cardinality_lem_k.get() ){ - Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); - //add cardinality lemma - Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); - std::vector< Node > vec_node; - vec_node.push_back( dist ); - for( std::vector< Node >::iterator itr1 = cols[i].begin(); - itr1 != cols[i].end(); ++itr1) { - Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); - if( len!=lr ) { - Node len_eq_lr = len.eqNode(lr); - vec_node.push_back( len_eq_lr ); - } - } - Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] ); - Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node ); - cons = Rewriter::rewrite( cons ); - ei->d_cardinality_lem_k.set( int_k+1 ); - if( cons!=d_true ){ - sendInference( d_empty_vec, vec_node, cons, "CARDINALITY", true ); - return; + EqcInfo* ei = getOrMakeEqcInfo( lr, true ); + Trace("strings-card") << "Previous cardinality used for " << lr << " is " << ((int)ei->d_cardinality_lem_k.get()-1) << std::endl; + if( int_k+1 > ei->d_cardinality_lem_k.get() ){ + Node k_node = NodeManager::currentNM()->mkConst( ::CVC4::Rational( int_k ) ); + //add cardinality lemma + Node dist = NodeManager::currentNM()->mkNode( kind::DISTINCT, cols[i] ); + std::vector< Node > vec_node; + vec_node.push_back( dist ); + for( std::vector< Node >::iterator itr1 = cols[i].begin(); + itr1 != cols[i].end(); ++itr1) { + Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, *itr1 ); + if( len!=lr ) { + Node len_eq_lr = len.eqNode(lr); + vec_node.push_back( len_eq_lr ); } } + Node len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, cols[i][0] ); + Node cons = NodeManager::currentNM()->mkNode( kind::GEQ, len, k_node ); + cons = Rewriter::rewrite( cons ); + ei->d_cardinality_lem_k.set( int_k+1 ); + if( cons!=d_true ){ + sendInference( d_empty_vec, vec_node, cons, "CARDINALITY", true ); + return; + } } } } @@ -3275,11 +3380,9 @@ void TheoryStrings::separateByLength(std::vector< Node >& n, Assert( d_equalityEngine.getRepresentative(eqc)==eqc ); EqcInfo* ei = getOrMakeEqcInfo( eqc, false ); Node lt = ei ? ei->d_length_term : Node::null(); - Trace("ajr-temp") << "Length term for " << eqc << " is " << lt << std::endl; if( !lt.isNull() ){ lt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); Node r = d_equalityEngine.getRepresentative( lt ); - Trace("ajr-temp") << "Length term rep for " << eqc << " is " << lt << std::endl; if( eqc_to_leqc.find( r )==eqc_to_leqc.end() ){ eqc_to_leqc[r] = leqc_counter; leqc_to_eqc[leqc_counter] = r; @@ -3318,6 +3421,26 @@ void TheoryStrings::updateMpl( Node n, int b ) { } */ + +unsigned TheoryStrings::getNumMemberships( Node n, bool isPos ) { + if( isPos ){ + NodeIntMap::const_iterator it = d_pos_memberships.find( n ); + if( it!=d_pos_memberships.end() ){ + return (*it).second; + } + }else{ + NodeIntMap::const_iterator it = d_neg_memberships.find( n ); + if( it!=d_neg_memberships.end() ){ + return (*it).second; + } + } + return 0; +} + +Node TheoryStrings::getMembership( Node n, bool isPos, unsigned i ) { + return isPos ? d_pos_memberships_data[n][i] : d_neg_memberships_data[n][i]; +} + //// Regular Expressions Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) { if(d_regexp_ant.find(atom) == d_regexp_ant.end()) { @@ -3395,10 +3518,8 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl; - for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); - itr_xr != d_pos_memberships.end(); ++itr_xr ) { + for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){ Node x = (*itr_xr).first; - NodeList* lst = (*itr_xr).second; Node nf_x = x; std::vector< Node > nf_x_exp; if(d_normal_forms.find( x ) != d_normal_forms.end()) { @@ -3412,10 +3533,11 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > std::vector< Node > vec_x; std::vector< Node > vec_r; - for(NodeList::const_iterator itr_lst = lst->begin(); - itr_lst != lst->end(); ++itr_lst) { - Node r = *itr_lst; - Node nf_r = normalizeRegexp((*lst)[0]); + unsigned n_pmem = (*itr_xr).second; + Assert( getNumMemberships( x, true )==n_pmem ); + for( unsigned k=0; k<n_pmem; k++ ){ + Node r = getMembership( x, true, k ); + Node nf_r = normalizeRegexp( r ); //AJR: fixed (was normalizing mem #0 always) Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r); if(d_processed_memberships.find(memb) == d_processed_memberships.end()) { if(d_regexp_opr.checkConstRegExp(nf_r)) { @@ -3645,46 +3767,43 @@ void TheoryStrings::checkMemberships() { Trace("regexp-debug") << "Checking Memberships ... " << std::endl; //if(options::stringEIT()) { //TODO: Opt for normal forms - for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); - itr_xr != d_pos_memberships.end(); ++itr_xr ) { + for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){ bool spflag = false; Node x = (*itr_xr).first; - NodeList* lst = (*itr_xr).second; Trace("regexp-debug") << "Checking Memberships for " << x << std::endl; if(d_inter_index.find(x) == d_inter_index.end()) { d_inter_index[x] = 0; } int cur_inter_idx = d_inter_index[x]; - if(cur_inter_idx != (int)lst->size()) { - if(lst->size() == 1) { - d_inter_cache[x] = (*lst)[0]; + unsigned n_pmem = (*itr_xr).second; + Assert( getNumMemberships( x, true )==n_pmem ); + if( cur_inter_idx != (int)n_pmem ) { + if( n_pmem == 1) { + d_inter_cache[x] = getMembership( x, true, 0 ); d_inter_index[x] = 1; Trace("regexp-debug") << "... only one choice " << std::endl; - } else if(lst->size() > 1) { + } else if(n_pmem > 1) { Node r; if(d_inter_cache.find(x) != d_inter_cache.end()) { r = d_inter_cache[x]; } if(r.isNull()) { - r = (*lst)[0]; + r = getMembership( x, true, 0 ); cur_inter_idx = 1; } - NodeList::const_iterator itr_lst = lst->begin(); - for(int i=0; i<cur_inter_idx; i++) { - ++itr_lst; - } - Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << lst->size() << std::endl; - for(;itr_lst != lst->end(); ++itr_lst) { - Node r2 = *itr_lst; + + unsigned k_start = cur_inter_idx; + Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << n_pmem << std::endl; + for(unsigned k = k_start; k<n_pmem; k++) { + Node r2 = getMembership( x, true, k ); r = d_regexp_opr.intersect(r, r2, spflag); if(spflag) { break; } else if(r == d_emptyRegexp) { std::vector< Node > vec_nodes; - ++itr_lst; - for(NodeList::const_iterator itr2 = lst->begin(); - itr2 != itr_lst; ++itr2) { - Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2); + for( unsigned kk=0; kk<=k; kk++ ){ + Node rr = getMembership( x, true, kk ); + Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, rr); vec_nodes.push_back( n ); } Node conc; @@ -3699,7 +3818,7 @@ void TheoryStrings::checkMemberships() { //updates if(!d_conflict && !spflag) { d_inter_cache[x] = r; - d_inter_index[x] = (int)lst->size(); + d_inter_index[x] = (int)n_pmem; } } } @@ -4322,44 +4441,52 @@ void TheoryStrings::addMembership(Node assertion) { Node x = atom[0]; Node r = atom[1]; if(polarity) { - NodeList* lst; - NodeListMap::iterator itr_xr = d_pos_memberships.find( x ); - if( itr_xr == d_pos_memberships.end() ){ - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_pos_memberships.insertDataFromContextMemory( x, lst ); - } else { - lst = (*itr_xr).second; - } - //check - for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { - if( r == *itr ) { - return; + int index = 0; + NodeIntMap::const_iterator it = d_pos_memberships.find( x ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + for( int k=0; k<index; k++ ){ + if( k<(int)d_pos_memberships_data[x].size() ){ + if( d_pos_memberships_data[x][k]==r ){ + return; + } + }else{ + break; + } } } - lst->push_back( r ); + d_pos_memberships[x] = index + 1; + if( index<(int)d_pos_memberships_data[x].size() ){ + d_pos_memberships_data[x][index] = r; + }else{ + d_pos_memberships_data[x].push_back( r ); + } } else if(!options::stringIgnNegMembership()) { /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { int rt; Node r2 = d_regexp_opr.complement(r, rt); Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2); }*/ - NodeList* lst; - NodeListMap::iterator itr_xr = d_neg_memberships.find( x ); - if( itr_xr == d_neg_memberships.end() ){ - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_neg_memberships.insertDataFromContextMemory( x, lst ); - } else { - lst = (*itr_xr).second; - } - //check - for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { - if( r == *itr ) { - return; + int index = 0; + NodeIntMap::const_iterator it = d_neg_memberships.find( x ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + for( int k=0; k<index; k++ ){ + if( k<(int)d_neg_memberships_data[x].size() ){ + if( d_neg_memberships_data[x][k]==r ){ + return; + } + }else{ + break; + } } } - lst->push_back( r ); + d_neg_memberships[x] = index + 1; + if( index<(int)d_neg_memberships_data[x].size() ){ + d_neg_memberships_data[x][index] = r; + }else{ + d_neg_memberships_data[x].push_back( r ); + } } // old if(polarity || !options::stringIgnNegMembership()) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index b9da524de..2deb09654 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -33,6 +33,11 @@ namespace CVC4 { namespace theory { + +namespace quantifiers{ + class TermArgTrie; +} + namespace strings { /** @@ -45,7 +50,6 @@ typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttri class TheoryStrings : public Theory { typedef context::CDChunkList<Node> NodeList; - typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; @@ -160,7 +164,8 @@ private: std::map< Node, std::vector< Node > > d_normal_forms_exp; std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend; //map of pairs of terms that have the same normal form - NodeListMap d_nf_pairs; + NodeIntMap d_nf_pairs; + std::map< Node, std::vector< Node > > d_nf_pairs_data; void addNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair2( Node n1, Node n2 ); @@ -176,6 +181,8 @@ private: // extended functions inferences cache NodeSet d_extf_infer_cache; std::vector< Node > d_empty_vec; + // + NodeList d_ee_disequalities; private: NodeSet d_congruent; std::map< Node, Node > d_eqc_to_const; @@ -236,6 +243,8 @@ private: //maintain which concat terms have the length lemma instantiated NodeNodeMap d_proxy_var; NodeNodeMap d_proxy_var_to_length; + /** All the function terms that the theory has seen */ + context::CDList<TNode> d_functionsTerms; private: //initial check void checkInit(); @@ -304,6 +313,8 @@ private: //cardinality check void checkCardinality(); +private: + void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); public: /** preregister term */ void preRegisterTerm(TNode n); @@ -410,8 +421,12 @@ private: NodeSet d_regexp_ucached; NodeSet d_regexp_ccached; // stored assertions - NodeListMap d_pos_memberships; - NodeListMap d_neg_memberships; + NodeIntMap d_pos_memberships; + std::map< Node, std::vector< Node > > d_pos_memberships_data; + NodeIntMap d_neg_memberships; + std::map< Node, std::vector< Node > > d_neg_memberships_data; + unsigned getNumMemberships( Node n, bool isPos ); + Node getMembership( Node n, bool isPos, unsigned i ); // semi normal forms for symbolic expression std::map< Node, Node > d_nf_regexps; std::map< Node, std::vector< Node > > d_nf_regexps_exp; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a4f42bddd..ba811644a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -33,6 +33,10 @@ StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){ d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); } +StringsPreprocess::~StringsPreprocess(){ + +} + /* int StringsPreprocess::checkFixLenVar( Node t ) { int ret = 2; diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 5bc9667ea..abc7b5a91 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -40,6 +40,7 @@ private: Node simplify( Node t, std::vector< Node > &new_nodes ); public: StringsPreprocess( context::UserContext* u ); + ~StringsPreprocess(); Node decompose( Node t, std::vector< Node > &new_nodes ); void simplify(std::vector< Node > &vec_node); |