From: Tianyi Liang Date: Tue, 12 Nov 2013 01:45:07 +0000 (-0600) Subject: length lemma is changed, var-split lemma is changed X-Git-Tag: cvc5-1.0.0~7265 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3e8490e19b90e57decbfb380001407bcc7d84ca4;p=cvc5.git length lemma is changed, var-split lemma is changed --- diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index fa686dd9f..a3921bb42 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -237,7 +237,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { vec_nodes.push_back( dc ); } } - Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << (dc.isNull() ? "NULL" : mkString(dc) ) << std::endl; + Trace("strings-regexp-derivative") << "RegExp-derivative OR R[" << i << "]{ " << mkString(r[i]) << " returns " << mkString(dc) << std::endl; } retNode = vec_nodes.size() == 0 ? Node::null() : ( vec_nodes.size()==1 ? vec_nodes[0] : NodeManager::currentNM()->mkNode( kind::REGEXP_OR, vec_nodes ) ); @@ -321,7 +321,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) { } d_dv_cache[dv] = retNode; } - Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << ( retNode.isNull() ? "NULL" : mkString( retNode ) ) << std::endl; + Trace("strings-regexp-derivative") << "RegExp-derivative returns : " << mkString( retNode ) << std::endl; return retNode; } @@ -577,79 +577,83 @@ std::string RegExpOpr::niceChar( Node r ) { } std::string RegExpOpr::mkString( Node r ) { std::string retStr; - int k = r.getKind(); - switch( k ) { - case kind::STRING_TO_REGEXP: - { - retStr += niceChar( r[0] ); - } - break; - case kind::REGEXP_CONCAT: - { - retStr += "("; - for(unsigned i=0; imkNode( kind::STRING_LENGTH, n); - Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero); - Trace("strings-lemma") << "Strings: Add lemma " << n_len_geq_zero << std::endl; + //Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::GEQ, n_len, d_zero); + Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, + n_len.eqNode( d_zero ), + NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) ); + Trace("strings-lemma") << "Strings::Lemma LENGTH geq 0 : " << n_len_geq_zero << std::endl; d_out->lemma(n_len_geq_zero); + + Node n_len_imp_empty = NodeManager::currentNM()->mkNode( kind::IMPLIES, n_len.eqNode( d_zero ), n.eqNode( d_emptyString) ); + Trace("strings-lemma") << "Strings::Lemma ZERO: " << n_len_geq_zero << std::endl; + d_out->lemma(n_len_imp_empty); } // FMF if( options::stringFMF() && n.getKind() == kind::VARIABLE ) { @@ -402,33 +403,11 @@ void TheoryStrings::check(Effort e) { atom = polarity ? fact : fact[0]; //must record string in regular expressions if ( atom.getKind() == kind::STRING_IN_REGEXP ) { - //if(fact[0].getKind() != kind::CONST_STRING) { - //if(polarity) { - d_reg_exp_mem.push_back( assertion ); - /*} else { - Node r = Rewriter::rewrite( atom[1] ); - r = d_regexp_opr.complement( r ); - r = NodeManager::currentNM()->mkNode( kind::STRING_IN_REGEXP, atom[0], r ); - std::vector< Node > vec_r; - vec_r.push_back( r ); - - StringsPreprocess spp; - spp.simplify( vec_r ); - for( unsigned i=1; i & visited, std if( nf.size()!=1 || nf[0]!=d_emptyString ) { for( unsigned r=0; r & v getConcatVec( eqc, nf ); Trace("strings-process") << "Return process equivalence class " << eqc << " : already visited." << std::endl; return false; - } else if( areEqual( eqc, d_emptyString ) ){ + } else if( areEqual( eqc, d_emptyString ) ) { eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ) { Node n = (*eqc_i); if( n.getKind()==kind::STRING_CONCAT ){ for( unsigned i=0; i & v }else{ conc = eqn[0].eqNode( eqn[1] ); Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Endpoint" ); + sendLemma( ant, conc, "ENDPOINT" ); return true; } }else{ @@ -921,7 +900,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //Trace("strings-loop") << "Check for loops i,j = " << (index_i+1) << "/" << normal_forms[i].size() << " " << (index_j+1) << "/" << normal_forms[j].size() << std::endl; int has_loop[2] = { -1, -1 }; //if( !options::stringFMF() ) { - for( unsigned r=0; r<2; r++ ){ + for( unsigned r=0; r<2; r++ ) { int index = (r==0 ? index_i : index_j); int other_index = (r==0 ? index_j : index_i ); int n_index = (r==0 ? i : j); @@ -1091,7 +1070,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v //unroll the str in re constraint once unrollStar( str_in_re ); //conc = NodeManager::currentNM()->mkNode( kind::OR, x_empty, conc ); - sendLemma( ant, conc, "Loop" ); + sendLemma( ant, conc, "LOOP-BREAK" ); //we will be done addNormalFormPair( normal_form_src[i], normal_form_src[j] ); @@ -1145,7 +1124,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v Trace("strings-solve-debug") << "Break normal form constant/variable " << std::endl; Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Constant Split" ); + sendLemma( ant, conc, "CST-SPLIT" ); return true; } }else{ @@ -1157,6 +1136,18 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v }else{ antec_new_lits.push_back(ldeq); } + + //x!=e /\ y!=e + for(unsigned xory=0; xory<2; xory++) { + Node x = xory==0 ? normal_forms[i][index_i] : normal_forms[j][index_j]; + Node xgtz = x.eqNode( d_emptyString ).negate(); + if( areDisequal( x, d_emptyString ) ) { + antec.push_back( xgtz ); + } else { + antec_new_lits.push_back( xgtz ); + } + } + Node sk = NodeManager::currentNM()->mkSkolem( "v_split_$$", normal_forms[i][index_i].getType(), "created for v/v split" ); Node eq1 = NodeManager::currentNM()->mkNode( kind::EQUAL, normal_forms[i][index_i], NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, normal_forms[j][index_j], sk ) ); @@ -1172,7 +1163,7 @@ bool TheoryStrings::normalizeEquivalenceClass( Node eqc, std::vector< Node > & v d_lemma_cache.push_back( sk_gt_zero ); Node ant = mkExplain( antec, antec_new_lits ); - sendLemma( ant, conc, "Split" ); + sendLemma( ant, conc, "VAR-SPLIT" ); return true; } } @@ -1372,14 +1363,14 @@ bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { void TheoryStrings::sendLemma( Node ant, Node conc, const char * c ) { if( conc.isNull() || conc==d_false ){ d_out->conflict(ant); - Trace("strings-conflict") << "CONFLICT : Strings conflict : " << ant << std::endl; + Trace("strings-conflict") << "Strings::Conflict : " << ant << std::endl; d_conflict = true; }else{ Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, ant, conc ); if( ant == d_true ) { lem = conc; } - Trace("strings-lemma") << "Strings " << c << " lemma : " << lem << std::endl; + Trace("strings-lemma") << "Strings::Lemma " << c << " : " << lem << std::endl; d_lemma_cache.push_back( lem ); } } @@ -1389,7 +1380,7 @@ void TheoryStrings::sendSplit( Node a, Node b, const char * c ) { eq = Rewriter::rewrite( eq ); Node neq = NodeManager::currentNM()->mkNode( kind::NOT, eq ); Node lemma_or = NodeManager::currentNM()->mkNode( kind::OR, eq, neq ); - Trace("strings-lemma") << "Strings " << c << " split lemma : " << lemma_or << std::endl; + Trace("strings-lemma") << "Strings::Lemma " << c << " SPLIT : " << lemma_or << std::endl; d_lemma_cache.push_back(lemma_or); d_pending_req_phase[eq] = true; } @@ -1488,18 +1479,18 @@ bool TheoryStrings::checkLengths() { //if n has not instantiatied the concat..length axiom //then, add lemma if( n.getKind() == kind::CONST_STRING || n.getKind() == kind::STRING_CONCAT ) { // || n.getKind() == kind::STRING_CONCAT ){ - if( d_length_inst.find(n)==d_length_inst.end() ){ + if( d_length_inst.find(n)==d_length_inst.end() ) { d_length_inst[n] = true; Trace("strings-debug") << "get n: " << n << endl; Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for concat lemma" ); d_length_intro_vars.push_back( sk ); Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n ); eq = Rewriter::rewrite(eq); - Trace("strings-lemma") << "Strings: Add term lemma " << eq << std::endl; + Trace("strings-lemma") << "Strings::Lemma LENGTH term : " << eq << std::endl; d_out->lemma(eq); Node skl = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, sk ); Node lsum; - if( n.getKind() == kind::STRING_CONCAT ){ + if( n.getKind() == kind::STRING_CONCAT ) { //add lemma std::vector node_vec; for( unsigned i=0; imkNode( kind::PLUS, node_vec ); - }else{ + } else { //add lemma lsum = NodeManager::currentNM()->mkConst( ::CVC4::Rational( n.getConst().size() ) ); } Node ceq = NodeManager::currentNM()->mkNode( kind::EQUAL, skl, lsum ); ceq = Rewriter::rewrite(ceq); - Trace("strings-lemma") << "Strings: Add length lemma " << ceq << std::endl; + Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl; d_out->lemma(ceq); addedLemma = true; } @@ -1695,26 +1686,26 @@ bool TheoryStrings::checkLengthsEqc() { std::vector< Node > nodes; getEquivalenceClasses( nodes ); for( unsigned i=0; i1 ){ + if( d_normal_forms[nodes[i]].size()>1 ) { Trace("strings-process-debug") << "Process length constraints for " << nodes[i] << std::endl; //check if there is a length term for this equivalence class EqcInfo* ei = getOrMakeEqcInfo( nodes[i], false ); Node lt = ei ? ei->d_length_term : Node::null(); - if( !lt.isNull() ){ - Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); - //now, check if length normalization has occurred - if( ei->d_normalized_length.get().isNull() ){ - //if not, add the lemma - std::vector< Node > ant; - ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() ); - ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) ); - Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) ); - lc = Rewriter::rewrite( lc ); - Node eq = llt.eqNode( lc ); - ei->d_normalized_length.set( eq ); - sendLemma( mkExplain( ant ), eq, "Length Normalization" ); - addedLemma = true; - } + if( !lt.isNull() ) { + Node llt = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, lt ); + //now, check if length normalization has occurred + if( ei->d_normalized_length.get().isNull() ) { + //if not, add the lemma + std::vector< Node > ant; + ant.insert( ant.end(), d_normal_forms_exp[nodes[i]].begin(), d_normal_forms_exp[nodes[i]].end() ); + ant.push_back( d_normal_forms_base[nodes[i]].eqNode( lt ) ); + Node lc = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, mkConcat( d_normal_forms[nodes[i]] ) ); + lc = Rewriter::rewrite( lc ); + Node eq = llt.eqNode( lc ); + ei->d_normalized_length.set( eq ); + sendLemma( mkExplain( ant ), eq, "Length Normalization" ); + addedLemma = true; + } } }else{ Trace("strings-process-debug") << "Do not process length constraints for " << nodes[i] << " " << d_normal_forms[nodes[i]].size() << std::endl; @@ -1900,6 +1891,20 @@ void TheoryStrings::printConcat( std::vector< Node >& n, const char * c ) { } } + +//// Measurements +/* +void TheoryStrings::updateMpl( Node n, int b ) { + if(d_mpl.find(n) == d_mpl.end()) { + //d_curr_cardinality.get(); + d_mpl[n] = b; + } else if(b < d_mpl[n]) { + d_mpl[n] = b; + } +} +*/ + +//// Regular Expressions bool TheoryStrings::unrollStar( Node atom ) { Node x = atom[0]; Node r = atom[1]; @@ -2128,6 +2133,8 @@ bool TheoryStrings::splitRegExp( Node x, Node r, Node ant ) { } } +//// Finite Model Finding + Node TheoryStrings::getNextDecisionRequest() { if(options::stringFMF() && !d_conflict) { //Trace("strings-fmf-debug") << "Strings::FMF: Assertion Level = " << d_valuation.getAssertionLevel() << std::endl; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 7d4b740e4..e036d5646 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -36,86 +36,93 @@ namespace strings { */ class TheoryStrings : public Theory { - typedef context::CDChunkList NodeList; - typedef context::CDHashMap NodeListMap; - typedef context::CDHashMap NodeBoolMap; - typedef context::CDHashMap NodeIntMap; - public: - - TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); - ~TheoryStrings(); - - void setMasterEqualityEngine(eq::EqualityEngine* eq); - - std::string identify() const { return std::string("TheoryStrings"); } - - Node getRepresentative( Node t ); - bool hasTerm( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); - Node getLengthTerm( Node t ); - Node getLength( Node t ); - public: - - void propagate(Effort e); - bool propagate(TNode literal); - void explain( TNode literal, std::vector& assumptions ); - Node explain( TNode literal ); - - - // NotifyClass for equality engine - class NotifyClass : public eq::EqualityEngineNotify { - TheoryStrings& d_str; - public: - NotifyClass(TheoryStrings& t_str): d_str(t_str) {} - bool eqNotifyTriggerEquality(TNode equality, bool value) { - Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; - if (value) { - return d_str.propagate(equality); - } else { - // We use only literal triggers so taking not is safe - return d_str.propagate(equality.notNode()); - } - } - bool eqNotifyTriggerPredicate(TNode predicate, bool value) { - Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; - if (value) { - return d_str.propagate(predicate); - } else { - return d_str.propagate(predicate.notNode()); - } - } - bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { - Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; - if (value) { - return d_str.propagate(t1.eqNode(t2)); - } else { - return d_str.propagate(t1.eqNode(t2).notNode()); - } - } - void eqNotifyConstantTermMerge(TNode t1, TNode t2) { - Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; - d_str.conflict(t1, t2); - } - void eqNotifyNewClass(TNode t) { - Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; - d_str.eqNotifyNewClass(t); - } - void eqNotifyPreMerge(TNode t1, TNode t2) { - Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; - d_str.eqNotifyPreMerge(t1, t2); - } - void eqNotifyPostMerge(TNode t1, TNode t2) { - Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; - d_str.eqNotifyPostMerge(t1, t2); - } - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { - Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; - d_str.eqNotifyDisequal(t1, t2, reason); - } - };/* class TheoryStrings::NotifyClass */ - - private: + typedef context::CDChunkList NodeList; + typedef context::CDHashMap NodeListMap; + typedef context::CDHashMap NodeBoolMap; + typedef context::CDHashMap NodeIntMap; + +public: + TheoryStrings(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); + ~TheoryStrings(); + + void setMasterEqualityEngine(eq::EqualityEngine* eq); + + std::string identify() const { return std::string("TheoryStrings"); } + +public: + void propagate(Effort e); + bool propagate(TNode literal); + void explain( TNode literal, std::vector& assumptions ); + Node explain( TNode literal ); + + + // NotifyClass for equality engine + class NotifyClass : public eq::EqualityEngineNotify { + TheoryStrings& d_str; + public: + NotifyClass(TheoryStrings& t_str): d_str(t_str) {} + bool eqNotifyTriggerEquality(TNode equality, bool value) { + Debug("strings") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl; + if (value) { + return d_str.propagate(equality); + } else { + // We use only literal triggers so taking not is safe + return d_str.propagate(equality.notNode()); + } + } + bool eqNotifyTriggerPredicate(TNode predicate, bool value) { + Debug("strings") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl; + if (value) { + return d_str.propagate(predicate); + } else { + return d_str.propagate(predicate.notNode()); + } + } + bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) { + Debug("strings") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl; + if (value) { + return d_str.propagate(t1.eqNode(t2)); + } else { + return d_str.propagate(t1.eqNode(t2).notNode()); + } + } + void eqNotifyConstantTermMerge(TNode t1, TNode t2) { + Debug("strings") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl; + d_str.conflict(t1, t2); + } + void eqNotifyNewClass(TNode t) { + Debug("strings") << "NotifyClass::eqNotifyNewClass(" << t << std::endl; + d_str.eqNotifyNewClass(t); + } + void eqNotifyPreMerge(TNode t1, TNode t2) { + Debug("strings") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << std::endl; + d_str.eqNotifyPreMerge(t1, t2); + } + void eqNotifyPostMerge(TNode t1, TNode t2) { + Debug("strings") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << std::endl; + d_str.eqNotifyPostMerge(t1, t2); + } + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { + Debug("strings") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << std::endl; + d_str.eqNotifyDisequal(t1, t2, reason); + } + };/* class TheoryStrings::NotifyClass */ + +private: + // Constants + Node d_emptyString; + Node d_true; + Node d_false; + Node d_zero; + // Helper functions + Node getRepresentative( Node t ); + bool hasTerm( Node a ); + bool areEqual( Node a, Node b ); + bool areDisequal( Node a, Node b ); + Node getLengthTerm( Node t ); + Node getLength( Node t ); + +private: /** The notify class */ NotifyClass d_notify; /** Equaltity engine */ @@ -123,82 +130,62 @@ class TheoryStrings : public Theory { /** Are we in conflict */ context::CDO d_conflict; std::vector< Node > d_length_intro_vars; - Node d_emptyString; - Node d_true; - Node d_false; - Node d_zero; - // RegExp depth - //int d_regexp_unroll_depth; - //list of pairs of nodes to merge - std::map< Node, Node > d_pending_exp; - std::vector< Node > d_pending; - std::vector< Node > d_lemma_cache; - std::map< Node, bool > d_pending_req_phase; - /** inferences */ - NodeList d_infer; - NodeList d_infer_exp; - /** normal forms */ - std::map< Node, Node > d_normal_forms_base; - std::map< Node, std::vector< Node > > d_normal_forms; - std::map< Node, std::vector< Node > > d_normal_forms_exp; - //map of pairs of terms that have the same normal form - NodeListMap d_nf_pairs; - void addNormalFormPair( Node n1, Node n2 ); - bool isNormalFormPair( Node n1, Node n2 ); - bool isNormalFormPair2( Node n1, Node n2 ); - - //loop - //std::map< Node, bool > d_loop_processed; - - //regular expression memberships - NodeList d_reg_exp_mem; - std::map< Node, bool > d_reg_exp_unroll; - std::map< Node, int > d_reg_exp_unroll_depth; - std::map< Node, bool > d_reg_exp_deriv; - //antecedant for why reg exp membership must be true - std::map< Node, Node > d_reg_exp_ant; - - ///////////////////////////////////////////////////////////////////////////// - // MODEL GENERATION - ///////////////////////////////////////////////////////////////////////////// - public: - - void collectModelInfo(TheoryModel* m, bool fullModel); - - ///////////////////////////////////////////////////////////////////////////// - // NOTIFICATIONS - ///////////////////////////////////////////////////////////////////////////// - - public: - void presolve(); - void shutdown() { } - - ///////////////////////////////////////////////////////////////////////////// - // MAIN SOLVER - ///////////////////////////////////////////////////////////////////////////// - private: - void addSharedTerm(TNode n); - EqualityStatus getEqualityStatus(TNode a, TNode b); - - private: - class EqcInfo - { - public: - EqcInfo( context::Context* c ); - ~EqcInfo(){} - //constant in this eqc - context::CDO< Node > d_const_term; - context::CDO< Node > d_length_term; - context::CDO< unsigned > d_cardinality_lem_k; - // 1 = added length lemma - context::CDO< Node > d_normalized_length; - }; - /** map from representatives to information necessary for equivalence classes */ - std::map< Node, EqcInfo* > d_eqc_info; - EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); - //maintain which concat terms have the length lemma instantiatied - std::map< Node, bool > d_length_inst; - private: + //list of pairs of nodes to merge + std::map< Node, Node > d_pending_exp; + std::vector< Node > d_pending; + std::vector< Node > d_lemma_cache; + std::map< Node, bool > d_pending_req_phase; + /** inferences */ + NodeList d_infer; + NodeList d_infer_exp; + /** normal forms */ + std::map< Node, Node > d_normal_forms_base; + std::map< Node, std::vector< Node > > d_normal_forms; + std::map< Node, std::vector< Node > > d_normal_forms_exp; + //map of pairs of terms that have the same normal form + NodeListMap d_nf_pairs; + void addNormalFormPair( Node n1, Node n2 ); + bool isNormalFormPair( Node n1, Node n2 ); + bool isNormalFormPair2( Node n1, Node n2 ); + + ///////////////////////////////////////////////////////////////////////////// + // MODEL GENERATION + ///////////////////////////////////////////////////////////////////////////// +public: + void collectModelInfo(TheoryModel* m, bool fullModel); + + ///////////////////////////////////////////////////////////////////////////// + // NOTIFICATIONS + ///////////////////////////////////////////////////////////////////////////// +public: + void presolve(); + void shutdown() { } + + ///////////////////////////////////////////////////////////////////////////// + // MAIN SOLVER + ///////////////////////////////////////////////////////////////////////////// +private: + void addSharedTerm(TNode n); + EqualityStatus getEqualityStatus(TNode a, TNode b); + +private: + class EqcInfo { + public: + EqcInfo( context::Context* c ); + ~EqcInfo(){} + //constant in this eqc + context::CDO< Node > d_const_term; + context::CDO< Node > d_length_term; + context::CDO< unsigned > d_cardinality_lem_k; + // 1 = added length lemma + context::CDO< Node > d_normalized_length; + }; + /** map from representatives to information necessary for equivalence classes */ + std::map< Node, EqcInfo* > d_eqc_info; + EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); + //maintain which concat terms have the length lemma instantiatied + std::map< Node, bool > d_length_inst; +private: bool 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); bool normalizeEquivalenceClass( Node n, std::vector< Node > & visited, std::vector< Node > & nf, std::vector< Node > & nf_exp ); @@ -212,57 +199,76 @@ class TheoryStrings : public Theory { bool checkInductiveEquations(); bool checkMemberships(); int gcd(int a, int b); - public: - void preRegisterTerm(TNode n); - void check(Effort e); - - /** Conflict when merging two constants */ - void conflict(TNode a, TNode b); - /** called when a new equivalance class is created */ - void eqNotifyNewClass(TNode t); - /** called when two equivalance classes will merge */ - void eqNotifyPreMerge(TNode t1, TNode t2); - /** called when two equivalance classes have merged */ - void eqNotifyPostMerge(TNode t1, TNode t2); - /** called when two equivalence classes are made disequal */ - void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); + +public: + void preRegisterTerm(TNode n); + void check(Effort e); + + /** Conflict when merging two constants */ + void conflict(TNode a, TNode b); + /** called when a new equivalance class is created */ + void eqNotifyNewClass(TNode t); + /** called when two equivalance classes will merge */ + void eqNotifyPreMerge(TNode t1, TNode t2); + /** called when two equivalance classes have merged */ + void eqNotifyPostMerge(TNode t1, TNode t2); + /** called when two equivalence classes are made disequal */ + void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); protected: - /** compute care graph */ - void computeCareGraph(); - - //do pending merges - void doPendingFacts(); - void doPendingLemmas(); - - void sendLemma( Node ant, Node conc, const char * c ); - void sendSplit( Node a, Node b, const char * c ); - /** mkConcat **/ - Node mkConcat( Node n1, Node n2 ); - Node mkConcat( std::vector< Node >& c ); - /** mkExplain **/ - Node mkExplain( std::vector< Node >& a ); - Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); - /** get concat vector */ - void getConcatVec( Node n, std::vector< Node >& c ); - - //get equivalence classes - void getEquivalenceClasses( std::vector< Node >& eqcs ); - //get final normal form - void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ); - - //seperate into collections with equal length - void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); - void printConcat( std::vector< Node >& n, const char * c ); + /** compute care graph */ + void computeCareGraph(); + + //do pending merges + void doPendingFacts(); + void doPendingLemmas(); + + void sendLemma( Node ant, Node conc, const char * c ); + void sendSplit( Node a, Node b, const char * c ); + /** mkConcat **/ + Node mkConcat( Node n1, Node n2 ); + Node mkConcat( std::vector< Node >& c ); + /** mkExplain **/ + Node mkExplain( std::vector< Node >& a ); + Node mkExplain( std::vector< Node >& a, std::vector< Node >& an ); + /** get concat vector */ + void getConcatVec( Node n, std::vector< Node >& c ); + + //get equivalence classes + void getEquivalenceClasses( std::vector< Node >& eqcs ); + //get final normal form + void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ); + + //seperate into collections with equal length + void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); + void printConcat( std::vector< Node >& n, const char * c ); + + // Measurement +private: + //NodeIntMap d_mpl; + //void updateMpl(Node n, int b); + + //NodeIntMap d_var_lmin; + //NodeIntMap d_var_lmax; // Regular Expression private: + // regular expression memberships + NodeList d_reg_exp_mem; + // 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, int > d_reg_exp_unroll_depth; + // regular expression derivative + std::map< Node, bool > d_reg_exp_deriv; + // regular expression operations RegExpOpr d_regexp_opr; + CVC4::String getHeadConst( Node x ); bool splitRegExp( Node x, Node r, Node ant ); -private: + // Finite Model Finding - //bool d_fmf; +private: std::vector< Node > d_in_vars; Node d_in_var_lsum; std::map< int, Node > d_cardinality_lits;