normal form breaking

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index aa3ab12c5e0e436d201656ecabe1f55c8c58c0eb..a2b21aa403df722ab561ebd653a22e107726343d 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -436,8 +436,8 @@ void TheoryStrings::check(Effort e) {
                                        addedLemma = checkMemberships();
                                        Trace("strings-process") << "Done check membership constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
                                        if( !d_conflict && !addedLemma ) {
-                                               addedLemma = checkInclusions();
-                                               Trace("strings-process") << "Done check inclusion constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
+                                               addedLemma = checkContains();
+                                               Trace("strings-process") << "Done check contain constraints, addedLemma = " << addedLemma << ", d_conflict = " << d_conflict << std::endl;
                                        }
                                }
                        }
@@ -721,6 +721,7 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
         Trace("strings-solve") << "--- Normal forms for equivlance class " << eqc << " : " << std::endl;
         for( unsigned i=0; i<normal_forms.size(); i++ ) {
             Trace("strings-solve") << "#" << i << " (from " << normal_form_src[i] << ") : ";
+                       //mergeCstVec(normal_forms[i]);
             for( unsigned j=0; j<normal_forms[i].size(); j++ ) {
                 if(j>0) Trace("strings-solve") << ", ";
                 Trace("strings-solve") << normal_forms[i][j];
@@ -741,6 +742,27 @@ bool TheoryStrings::getNormalForms(Node &eqc, std::vector< Node > & visited, std
        return true;
 }
 
+void TheoryStrings::mergeCstVec(std::vector< Node > &vec_strings) {
+       std::vector< Node >::iterator itr = vec_strings.begin();
+       while(itr != vec_strings.end()) {
+               if(itr->isConst()) {
+                       std::vector< Node >::iterator itr2 = itr + 1;
+                       if(itr2 == vec_strings.end()) {
+                               break;
+                       } else if(itr2->isConst()) {
+                               CVC4::String s1 = itr->getConst<String>();
+                               CVC4::String s2 = itr2->getConst<String>();
+                               *itr = NodeManager::currentNM()->mkConst(s1.concat(s2));
+                               vec_strings.erase(itr2);
+                       } else {
+                               ++itr;
+                       }
+               } else {
+                       ++itr;
+               }
+       }
+}
+
 bool TheoryStrings::detectLoop( std::vector< std::vector< Node > > &normal_forms,
                                                                int i, int j, int index_i, int index_j, 
                                                                int &loop_in_i, int &loop_in_j) {
@@ -2070,12 +2092,12 @@ bool TheoryStrings::checkMemberships() {
        }
 }
 
-bool TheoryStrings::checkInclusions() {
+bool TheoryStrings::checkContains() {
        bool is_unk = false;
        bool addedLemma = false;
        for( unsigned i=0; i<d_str_ctn.size(); i++ ){
                Node assertion = d_str_ctn[i];
-               Trace("strings-inc") << "We have inclusion assertion : " << assertion << std::endl;
+               Trace("strings-ctn") << "We have contain assertion : " << assertion << std::endl;
                Node atom = assertion.getKind()==kind::NOT ? assertion[0] : assertion;
                bool polarity = assertion.getKind()!=kind::NOT;
                if( polarity ) {
@@ -2085,45 +2107,53 @@ bool TheoryStrings::checkInclusions() {
                        if( !areEqual( s, d_emptyString ) && !areEqual( s, x ) ) {
                                if(d_str_ctn_rewritten.find(atom) == d_str_ctn_rewritten.end()) {
                                        // Add lemma
-                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for inclusion" );
-                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for inclusion" );
+                                       Node sk1 = NodeManager::currentNM()->mkSkolem( "sc1_$$", s.getType(), "created for contain" );
+                                       Node sk2 = NodeManager::currentNM()->mkSkolem( "sc2_$$", s.getType(), "created for contain" );
                                        Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
-                                       sendLemma( assertion, eq, "inclusion" );
+                                       sendLemma( assertion, eq, "POS-INC" );
                                        addedLemma = true;
                                        d_str_ctn_rewritten[ atom ] = true;
                                } else {
-                                       Trace("strings-inc") << "... is already rewritten." << std::endl;
+                                       Trace("strings-ctn") << "... is already rewritten." << std::endl;
                                }
                        } else {
-                               Trace("strings-inc") << "... is satisfied." << std::endl;
+                               Trace("strings-ctn") << "... is satisfied." << std::endl;
                        }
                } else {
                        if( areEqual( atom[1], d_emptyString ) ) {
                                Node ant = NodeManager::currentNM()->mkNode( kind::AND, assertion, atom[1].eqNode( d_emptyString ) );
                                Node conc = Node::null();
-                               sendLemma( ant, conc, "inclusion conflict 1" );
+                               sendLemma( ant, conc, "NEG-CTN Conflict 1" );
                                addedLemma = true;
                        } else if( areEqual( atom[1], atom[0] ) ) {
                                Node ant = NodeManager::currentNM()->mkNode( kind::AND, assertion, atom[1].eqNode( atom[0] ) );
                                Node conc = Node::null();
-                               sendLemma( ant, conc, "inclusion conflict 2" );
+                               sendLemma( ant, conc, "NEG-CTN Conflict 2" );
                                addedLemma = true;
                        } else {
-                               if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) {
-                                       if(options::stringExp()) {
-                                               Node x = atom[0];
-                                               Node s = atom[1];
-                                               Node sk1 = NodeManager::currentNM()->mkSkolem( "sc3_$$", s.getType(), "created for inclusion" );
-                                               Node sk2 = NodeManager::currentNM()->mkSkolem( "sc4_$$", s.getType(), "created for inclusion" );
-                                               Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
-                                               Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq ) );
-                                               d_str_ctn_rewritten[ assertion ] = true;
-                                               sendLemma( antc, d_false, "negative inclusion" );
+                               if(options::stringExp()) {
+                                       Node x = atom[0];
+                                       Node s = atom[1];
+                                       Node lenx = getLengthTerm(x);
+                                       Node lens = getLengthTerm(s);
+                                       if(areEqual(lenx, lens)) {
+                                               if(d_str_ctn_eqlen.find(assertion) == d_str_ctn_eqlen.end()) {
+                                                       Node eq = lenx.eqNode(lens);
+                                                       Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq ) );
+                                                       Node xneqs = x.eqNode(s).negate();
+                                                       d_str_ctn_eqlen[ assertion ] = true;
+                                                       sendLemma( antc, xneqs, "NEG-CTN-EQL" );
+                                                       addedLemma = true;
+                                               }
+                                       } else if(!areDisequal(lenx, lens)) {
+                                               sendSplit(lenx, lens, "NEG-CTN-SP");
                                                addedLemma = true;
                                        } else {
-                                               Trace("strings-inc") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
-                                               is_unk = true;
+                                               addedLemma = processNegContains(assertion);
                                        }
+                               } else {
+                                       Trace("strings-ctn") << "Strings Incomplete (due to Negative Contain) by default." << std::endl;
+                                       is_unk = true;
                                }
                        }
                }
@@ -2140,6 +2170,27 @@ bool TheoryStrings::checkInclusions() {
        }
 }
 
+bool TheoryStrings::processNegContains(Node assertion) {
+       Node atom = assertion[0];
+       Node x = atom[0];
+       Node s = atom[1];
+       Node lenx = getLengthTerm(x);
+       Node lens = getLengthTerm(s);
+
+       if(d_str_ctn_rewritten.find(assertion) == d_str_ctn_rewritten.end()) {
+               Node sk1 = NodeManager::currentNM()->mkSkolem( "sc3_$$", s.getType(), "created for contain" );
+               Node sk2 = NodeManager::currentNM()->mkSkolem( "sc4_$$", s.getType(), "created for contain" );
+               Node eq = Rewriter::rewrite( x.eqNode( NodeManager::currentNM()->mkNode( kind::STRING_CONCAT, sk1, s, sk2 ) ) );
+               Node gt = NodeManager::currentNM()->mkNode( kind::GT, lenx, lens );
+               Node antc = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::AND, assertion, eq, gt ) );
+               d_str_ctn_rewritten[ assertion ] = true;
+               sendLemma( antc, d_false, "NEG-INC-BRK" );
+               return true;
+       } else {
+               return false;
+       }
+}
+
 CVC4::String TheoryStrings::getHeadConst( Node x ) {
        if( x.isConst() ) {
                return x.getConst< String >();
@@ -2155,8 +2206,8 @@ CVC4::String TheoryStrings::getHeadConst( Node x ) {
 }
 
 bool TheoryStrings::addMembershipLength(Node atom) {
-       Node x = atom[0];
-       Node r = atom[1];
+       //Node x = atom[0];
+       //Node r = atom[1];
 
        /*std::vector< int > co;
        co.push_back(0);

diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 62524ee1452e9110aaaad2717dca54bbba57e8a8..77ea298bdde098aea51e625c8ee576592c301993 100644 (file)
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -191,6 +191,7 @@ private:
        //maintain which concat terms have the length lemma instantiated
        std::map< Node, bool > d_length_inst;
 private:
+       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,
                                                std::vector< std::vector< Node > > &normal_forms_exp,
@@ -216,7 +217,8 @@ private:
     bool checkCardinality();
     bool checkInductiveEquations();
        bool checkMemberships();
-       bool checkInclusions();
+       bool checkContains();
+       bool processNegContains(Node assertion);
 
 public:
        void preRegisterTerm(TNode n);
@@ -272,6 +274,7 @@ private:
 
        // Special String Functions
        NodeList d_str_ctn;
+       std::map< Node, bool > d_str_ctn_eqlen;
        std::map< Node, bool > d_str_ctn_rewritten;
 
        // Regular Expression