adds intro vars length cache

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 64f3cd578457f07132ec3ab52aa5516edc7d5dd7..448b94fd2ce6054746d6ab5387d95a88851e0309 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -42,6 +42,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
     d_infer_exp(c),
     d_nf_pairs(c),
        d_loop_antec(u),
+       d_length_intro_vars(u),
        d_length_inst(u),
        d_length_nodes(c),
        d_str_pos_ctn(c),
@@ -50,7 +51,7 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, Outpu
        d_neg_ctn_ulen(u),
        d_pos_ctn_cached(u),
        d_neg_ctn_cached(u),
-       d_reg_exp_mem(c),
+       d_regexp_memberships(c),
        d_regexp_ucached(u),
        d_regexp_ccached(c),
        d_regexp_ant(c),
@@ -432,14 +433,16 @@ void TheoryStrings::preRegisterTerm(TNode n) {
        }
        default: {
                if(n.getType().isString() && n.getKind()!=kind::STRING_CONCAT && n.getKind()!=kind::CONST_STRING ) {
-                 Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
-                 Node n_len_eq_z = n.eqNode(d_emptyString); //n_len.eqNode( d_zero );
-                 n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
-                 Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
-                                                                       NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
-                 Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
-                 d_out->lemma(n_len_geq_zero);
-                 d_out->requirePhase( n_len_eq_z, true );
+                 if( d_length_intro_vars.find(n)==d_length_intro_vars.end() ) {
+                         Node n_len = NodeManager::currentNM()->mkNode( kind::STRING_LENGTH, n);
+                         Node n_len_eq_z = n_len.eqNode( d_zero );
+                         n_len_eq_z = Rewriter::rewrite( n_len_eq_z );
+                         Node n_len_geq_zero = NodeManager::currentNM()->mkNode( kind::OR, n_len_eq_z,
+                                                                               NodeManager::currentNM()->mkNode( kind::GT, n_len, d_zero) );
+                         Trace("strings-lemma") << "Strings::Lemma LENGTH >= 0 : " << n_len_geq_zero << std::endl;
+                         d_out->lemma(n_len_geq_zero);
+                         d_out->requirePhase( n_len_eq_z, true );
+                 }
                  // FMF
                  if( n.getKind() == kind::VARIABLE && options::stringFMF() ) {
                          d_input_vars.insert(n);
@@ -485,7 +488,7 @@ void TheoryStrings::check(Effort e) {
     atom = polarity ? fact : fact[0];
        //must record string in regular expressions
        if ( atom.getKind() == kind::STRING_IN_REGEXP ) {
-               d_reg_exp_mem.push_back( assertion );
+               d_regexp_memberships.push_back( assertion );
                //d_equalityEngine.assertPredicate(atom, polarity, fact);
        } else if (atom.getKind() == kind::STRING_STRCTN) {
                if(polarity) {
@@ -1792,6 +1795,7 @@ bool TheoryStrings::checkSimple() {
                                                        Trace("strings-debug") << "get n: " << n << endl;
                                                        Node sk = NodeManager::currentNM()->mkSkolem( "lsym_$$", n.getType(), "created for length" );
                                                        d_statistics.d_new_skolems += 1;
+                                                       d_length_intro_vars.insert( sk );
                                                        Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, sk, n );
                                                        eq = Rewriter::rewrite(eq);
                                                        Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
@@ -2229,9 +2233,9 @@ bool TheoryStrings::checkMemberships() {
        bool addedLemma = false;
        std::vector< Node > processed;
        std::vector< Node > cprocessed;
-       for( unsigned i=0; i<d_reg_exp_mem.size(); i++ ){
+       for( unsigned i=0; i<d_regexp_memberships.size(); i++ ){
                //check regular expression membership
-               Node assertion = d_reg_exp_mem[i];
+               Node assertion = d_regexp_memberships[i];
                if( d_regexp_ucached.find(assertion) == d_regexp_ucached.end() 
                        && d_regexp_ccached.find(assertion) == d_regexp_ccached.end() ) {
                        Trace("strings-regexp") << "We have regular expression assertion : " << assertion << std::endl;

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index cbfa481c3e3001336558619da67fdbb10ed08846..c8a3748930d5357faaedc01ce258d0eb16060e02 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -156,6 +156,7 @@ private:
        bool isNormalFormPair2( Node n1, Node n2 );
        // loop ant
        NodeSet d_loop_antec;
+       NodeSet d_length_intro_vars;
 
        /////////////////////////////////////////////////////////////////////////////
        // MODEL GENERATION
@@ -295,7 +296,7 @@ private:
        // Regular Expression
 private:
        // regular expression memberships
-       NodeList d_reg_exp_mem;
+       NodeList d_regexp_memberships;
        NodeSet d_regexp_ucached;
        NodeSet d_regexp_ccached;
        // antecedant for why regexp membership must be true