From c90b5b15ca93e64683c2bbf85def8d7afb4edab8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Sep 2018 14:38:07 -0500 Subject: Make strings model construction robust to lengths that are not propagated equal (#2444) This fixes #2429. This was caused by arithmetic not notifying an equality between shared terms that it assigned to the same value. See explanation in comment. We should investigate a bit more why this is happening. I didnt think arithmetic was allowed to assign the same value to unpropagated shared length terms. I've opened issue https://github.com/CVC4/CVC4/issues/2443 to track this. Regardless, the strings model construction should be robust to handle this case, which this PR does. --- src/theory/strings/theory_strings.cpp | 118 +++++--- src/theory/strings/theory_strings.h | 12 +- test/regress/Makefile.tests | 2 + test/regress/regress1/strings/issue2429-code.smt2 | 61 ++++ test/regress/regress3/issue2429.smt2 | 321 ++++++++++++++++++++++ 5 files changed, 481 insertions(+), 33 deletions(-) create mode 100644 test/regress/regress1/strings/issue2429-code.smt2 create mode 100644 test/regress/regress3/issue2429.smt2 diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 628ffbba7..2e1d6c2c7 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -501,30 +501,38 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) { Trace("strings-model") << "TheoryStrings : Collect model info" << std::endl; Trace("strings-model") << "TheoryStrings : assertEqualityEngine." << std::endl; - - //AJR : no use doing this since we cannot preregister terms with finite types that don't belong to strings. - // change this if we generalize to sequences. - //set termSet; - // Compute terms appearing in assertions and shared terms - //computeRelevantTerms(termSet); - //m->assertEqualityEngine( &d_equalityEngine, &termSet ); - if (!m->assertEqualityEngine(&d_equalityEngine)) + std::set termSet; + + // Compute terms appearing in assertions and shared terms + computeRelevantTerms(termSet); + // assert the (relevant) portion of the equality engine to the model + if (!m->assertEqualityEngine(&d_equalityEngine, &termSet)) { return false; } + std::unordered_set repSet; NodeManager* nm = NodeManager::currentNM(); // Generate model - std::vector< Node > nodes; - getEquivalenceClasses( nodes ); + // get the relevant string equivalence classes + for (const Node& s : termSet) + { + if (s.getType().isString()) + { + Node r = getRepresentative(s); + repSet.insert(r); + } + } + std::vector nodes(repSet.begin(), repSet.end()); std::map< Node, Node > processed; std::vector< std::vector< Node > > col; std::vector< Node > lts; separateByLength( nodes, col, lts ); //step 1 : get all values for known lengths std::vector< Node > lts_values; - std::map< unsigned, bool > values_used; + std::map values_used; + std::vector len_splits; for( unsigned i=0; i() <= Rational(String::maxSize()), + len_value = lts[i]; + } + else if (!lts[i].isNull()) + { + // get the model value for lts[i] + len_value = d_valuation.getModelValue(lts[i]); + } + if (len_value.isNull()) + { + lts_values.push_back(Node::null()); + } + else + { + Assert(len_value.getConst() <= Rational(String::maxSize()), "Exceeded UINT32_MAX in string model"); - unsigned lvalue = lts[i].getConst().getNumerator().toUnsignedInt(); - values_used[ lvalue ] = true; - }else{ - //get value for lts[i]; - if( !lts[i].isNull() ){ - Node v = d_valuation.getModelValue(lts[i]); - Trace("strings-model") << "Model value for " << lts[i] << " is " << v << std::endl; - lts_values.push_back( v ); - Assert(v.getConst() <= Rational(String::maxSize()), - "Exceeded UINT32_MAX in string model"); - unsigned lvalue = v.getConst().getNumerator().toUnsignedInt(); - values_used[ lvalue ] = true; - }else{ - //Trace("strings-model-warn") << "No length for eqc " << col[i][0] << std::endl; - //Assert( false ); - lts_values.push_back( Node::null() ); + unsigned lvalue = + len_value.getConst().getNumerator().toUnsignedInt(); + std::map::iterator itvu = values_used.find(lvalue); + if (itvu == values_used.end()) + { + values_used[lvalue] = lts[i]; + } + else + { + len_splits.push_back(lts[i].eqNode(itvu->second)); } + lts_values.push_back(len_value); } } ////step 2 : assign arbitrary values for unknown lengths? @@ -564,7 +580,8 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) //step 3 : assign values to equivalence classes that are pure variables for( unsigned i=0; i pure_eq; - Trace("strings-model") << "The equivalence classes "; + Trace("strings-model") << "The (" << col[i].size() + << ") equivalence classes "; for (const Node& eqc : col[i]) { Trace("strings-model") << eqc << " "; @@ -614,7 +631,7 @@ bool TheoryStrings::collectModelInfo(TheoryModel* m) } Trace("strings-model") << "*** Decide to make length of " << lvalue << std::endl; lts_values[i] = nm->mkConst(Rational(lvalue)); - values_used[ lvalue ] = true; + values_used[lvalue] = Node::null(); } Trace("strings-model") << "Need to assign values of length " << lts_values[i] << " to equivalence classes "; for( unsigned j=0; jhasTerm(c)) { ++sel; - Assert(!sel.isFinished()); + if (sel.isFinished()) + { + // We are in a case where model construction is impossible due to + // an insufficient number of constants of a given length. + + // Consider an integer equivalence class E whose value is assigned + // n in the model. Let { S_1, ..., S_m } be the set of string + // equivalence classes such that len( x ) is a member of E for + // some member x of each class S1, ...,Sm. Since our calculus is + // saturated with respect to cardinality inference (see Liang + // et al, Figure 6, CAV 2014), we have that m <= A^n, where A is + // the cardinality of our alphabet. + + // Now, consider the case where there exists two integer + // equivalence classes E1 and E2 that are assigned n, and moreover + // we did not received notification from arithmetic that E1 = E2. + // This typically should never happen, but assume in the following + // that it does. + + // Now, it may be the case that there are string equivalence + // classes { S_1, ..., S_m1 } whose lengths are in E1, + // and classes { S'_1, ..., S'_m2 } whose lengths are in E2, where + // m1 + m2 > A^n. In this case, we have insufficient strings to + // assign to { S_1, ..., S_m1, S'_1, ..., S'_m2 }. If this + // happens, we add a split on len( u1 ) = len( u2 ) for some + // len( u1 ) in E1, len( u2 ) in E2. We do this for each pair of + // integer equivalence classes that are assigned to the same value + // in the model. + AlwaysAssert(!len_splits.empty()); + for (const Node& sl : len_splits) + { + Node spl = nm->mkNode(OR, sl, sl.negate()); + d_out->lemma(spl); + } + return false; + } c = *sel; } ++sel; @@ -4139,6 +4191,7 @@ void TheoryStrings::checkCardinality() { std::vector< Node > lts; separateByLength( d_strings_eqc, cols, lts ); + Trace("strings-card") << "Check cardinality...." << std::endl; for( unsigned i = 0; i& eqcs ) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 5bc6b019f..77dae0cf3 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -578,8 +578,18 @@ private: /** get concat vector */ void getConcatVec(Node n, std::vector& c); - // get equivalence classes + /** get equivalence classes + * + * This adds the representative of all equivalence classes to eqcs + */ void getEquivalenceClasses(std::vector& eqcs); + /** get relevant equivalence classes + * + * This adds the representative of all equivalence classes that contain at + * least one term in termSet. + */ + void getRelevantEquivalenceClasses(std::vector& eqcs, + std::set& termSet); // separate into collections with equal length void separateByLength(std::vector& n, diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 45385f9c6..b4f920ca4 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1493,6 +1493,7 @@ REG1_TESTS = \ regress1/strings/issue1105.smt2 \ regress1/strings/issue1684-regex.smt2 \ regress1/strings/issue2060.smt2 \ + regress1/strings/issue2429-code.smt2 \ regress1/strings/kaluza-fl.smt2 \ regress1/strings/loop002.smt2 \ regress1/strings/loop003.smt2 \ @@ -1722,6 +1723,7 @@ REG3_TESTS = \ regress3/hole9.cvc \ regress3/incorrect1.smt \ regress3/incorrect2.smt \ + regress3/issue2429.smt2 \ regress3/pp-regfile.smt \ regress3/qwh.35.405.shuffled-as.sat03-1651.smt diff --git a/test/regress/regress1/strings/issue2429-code.smt2 b/test/regress/regress1/strings/issue2429-code.smt2 new file mode 100644 index 000000000..2d906c1fd --- /dev/null +++ b/test/regress/regress1/strings/issue2429-code.smt2 @@ -0,0 +1,61 @@ +(set-logic QF_S) +(set-option :strings-exp true) +(set-option :produce-models true) +(set-info :status sat) + +(define-fun byte_2_int ((s String)) Int (ite (= (str.len s) 1) (str.code s) 256)) + +(define-fun read_buffer16 ((s1 String) (s2 String)) Int + (+ (* 256 (byte_2_int s1)) + (byte_2_int s2)) +) + + +(define-fun read_buffer32 ((s1 String) (s2 String) (s3 String) (s4 String)) Int + (+ (+ (+ (* 16777216 (byte_2_int s1) ) + (* 65536 (byte_2_int s2) ) ) + (* 256 (byte_2_int s3) ) ) + (byte_2_int s4) ) +) + + +(declare-const magic String) +(declare-const p1 String) +(declare-const p2 String) +(declare-const p3 String) +(declare-const size1 String) +(declare-const size2 String) +(declare-const size3 String) +(declare-const size4 String) +(declare-const off1 String) +(declare-const off2 String) +(declare-const off3 String) +(declare-const off4 String) +(assert (= magic "ABCD")) +(assert (= 1 (str.len size1))) +(assert (= 1 (str.len size2))) +(assert (= 1 (str.len size3))) +(assert (= 1 (str.len size4))) +(assert (= 1 (str.len off1))) +(assert (= 1 (str.len off2))) +(assert (= 1 (str.len off3))) +(assert (= 1 (str.len off4))) + + +(declare-const p3_off Int) +(declare-const before_p3 String) +(assert (= before_p3 (str.++ p1 p2))) +(assert (not (str.contains before_p3 magic))) +(assert (= p3_off (str.len before_p3))) + + +(declare-const p2_size Int) +(declare-const p2_off Int) +(declare-const p2_min_size Int) +(assert (= p2_size (read_buffer32 size1 size2 size3 size4))) +(assert (= p2_off (read_buffer32 off1 off2 off3 off4))) +(assert (<= (+ p2_size p2_off) p3_off)) +(assert (>= p2_size p2_min_size)) +(assert (= p2_min_size 10)) + +(check-sat) diff --git a/test/regress/regress3/issue2429.smt2 b/test/regress/regress3/issue2429.smt2 new file mode 100644 index 000000000..37e932a65 --- /dev/null +++ b/test/regress/regress3/issue2429.smt2 @@ -0,0 +1,321 @@ +(set-logic QF_S) +(set-option :strings-exp true) +(set-option :produce-models true) +(set-info :status sat) + +(define-fun byte_2_int ((s String)) Int + (ite (= s "\x00") 0 + (ite (= s "\x01") 1 + (ite (= s "\x02") 2 + (ite (= s "\x03") 3 + (ite (= s "\x04") 4 + (ite (= s "\x05") 5 + (ite (= s "\x06") 6 + (ite (= s "\x07") 7 + (ite (= s "\x08") 8 + (ite (= s "\x09") 9 + (ite (= s "\x0A") 10 + (ite (= s "\x0B") 11 + (ite (= s "\x0C") 12 + (ite (= s "\x0D") 13 + (ite (= s "\x0E") 14 + (ite (= s "\x0F") 15 + (ite (= s "\x10") 16 + (ite (= s "\x11") 17 + (ite (= s "\x12") 18 + (ite (= s "\x13") 19 + (ite (= s "\x14") 20 + (ite (= s "\x15") 21 + (ite (= s "\x16") 22 + (ite (= s "\x17") 23 + (ite (= s "\x18") 24 + (ite (= s "\x19") 25 + (ite (= s "\x1A") 26 + (ite (= s "\x1B") 27 + (ite (= s "\x1C") 28 + (ite (= s "\x1D") 29 + (ite (= s "\x1E") 30 + (ite (= s "\x1F") 31 + (ite (= s "\x20") 32 + (ite (= s "\x21") 33 + (ite (= s "\x22") 34 + (ite (= s "\x23") 35 + (ite (= s "\x24") 36 + (ite (= s "\x25") 37 + (ite (= s "\x26") 38 + (ite (= s "\x27") 39 + (ite (= s "\x28") 40 + (ite (= s "\x29") 41 + (ite (= s "\x2A") 42 + (ite (= s "\x2B") 43 + (ite (= s "\x2C") 44 + (ite (= s "\x2D") 45 + (ite (= s "\x2E") 46 + (ite (= s "\x2F") 47 + (ite (= s "\x30") 48 + (ite (= s "\x31") 49 + (ite (= s "\x32") 50 + (ite (= s "\x33") 51 + (ite (= s "\x34") 52 + (ite (= s "\x35") 53 + (ite (= s "\x36") 54 + (ite (= s "\x37") 55 + (ite (= s "\x38") 56 + (ite (= s "\x39") 57 + (ite (= s "\x3A") 58 + (ite (= s "\x3B") 59 + (ite (= s "\x3C") 60 + (ite (= s "\x3D") 61 + (ite (= s "\x3E") 62 + (ite (= s "\x3F") 63 + (ite (= s "\x40") 64 + (ite (= s "\x41") 65 + (ite (= s "\x42") 66 + (ite (= s "\x43") 67 + (ite (= s "\x44") 68 + (ite (= s "\x45") 69 + (ite (= s "\x46") 70 + (ite (= s "\x47") 71 + (ite (= s "\x48") 72 + (ite (= s "\x49") 73 + (ite (= s "\x4A") 74 + (ite (= s "\x4B") 75 + (ite (= s "\x4C") 76 + (ite (= s "\x4D") 77 + (ite (= s "\x4E") 78 + (ite (= s "\x4F") 79 + (ite (= s "\x50") 80 + (ite (= s "\x51") 81 + (ite (= s "\x52") 82 + (ite (= s "\x53") 83 + (ite (= s "\x54") 84 + (ite (= s "\x55") 85 + (ite (= s "\x56") 86 + (ite (= s "\x57") 87 + (ite (= s "\x58") 88 + (ite (= s "\x59") 89 + (ite (= s "\x5A") 90 + (ite (= s "\x5B") 91 + (ite (= s "\x5C") 92 + (ite (= s "\x5D") 93 + (ite (= s "\x5E") 94 + (ite (= s "\x5F") 95 + (ite (= s "\x60") 96 + (ite (= s "\x61") 97 + (ite (= s "\x62") 98 + (ite (= s "\x63") 99 + (ite (= s "\x64") 100 + (ite (= s "\x65") 101 + (ite (= s "\x66") 102 + (ite (= s "\x67") 103 + (ite (= s "\x68") 104 + (ite (= s "\x69") 105 + (ite (= s "\x6A") 106 + (ite (= s "\x6B") 107 + (ite (= s "\x6C") 108 + (ite (= s "\x6D") 109 + (ite (= s "\x6E") 110 + (ite (= s "\x6F") 111 + (ite (= s "\x70") 112 + (ite (= s "\x71") 113 + (ite (= s "\x72") 114 + (ite (= s "\x73") 115 + (ite (= s "\x74") 116 + (ite (= s "\x75") 117 + (ite (= s "\x76") 118 + (ite (= s "\x77") 119 + (ite (= s "\x78") 120 + (ite (= s "\x79") 121 + (ite (= s "\x7A") 122 + (ite (= s "\x7B") 123 + (ite (= s "\x7C") 124 + (ite (= s "\x7D") 125 + (ite (= s "\x7E") 126 + (ite (= s "\x7F") 127 + (ite (= s "\x80") 128 + (ite (= s "\x81") 129 + (ite (= s "\x82") 130 + (ite (= s "\x83") 131 + (ite (= s "\x84") 132 + (ite (= s "\x85") 133 + (ite (= s "\x86") 134 + (ite (= s "\x87") 135 + (ite (= s "\x88") 136 + (ite (= s "\x89") 137 + (ite (= s "\x8A") 138 + (ite (= s "\x8B") 139 + (ite (= s "\x8C") 140 + (ite (= s "\x8D") 141 + (ite (= s "\x8E") 142 + (ite (= s "\x8F") 143 + (ite (= s "\x90") 144 + (ite (= s "\x91") 145 + (ite (= s "\x92") 146 + (ite (= s "\x93") 147 + (ite (= s "\x94") 148 + (ite (= s "\x95") 149 + (ite (= s "\x96") 150 + (ite (= s "\x97") 151 + (ite (= s "\x98") 152 + (ite (= s "\x99") 153 + (ite (= s "\x9A") 154 + (ite (= s "\x9B") 155 + (ite (= s "\x9C") 156 + (ite (= s "\x9D") 157 + (ite (= s "\x9E") 158 + (ite (= s "\x9F") 159 + (ite (= s "\xA0") 160 + (ite (= s "\xA1") 161 + (ite (= s "\xA2") 162 + (ite (= s "\xA3") 163 + (ite (= s "\xA4") 164 + (ite (= s "\xA5") 165 + (ite (= s "\xA6") 166 + (ite (= s "\xA7") 167 + (ite (= s "\xA8") 168 + (ite (= s "\xA9") 169 + (ite (= s "\xAA") 170 + (ite (= s "\xAB") 171 + (ite (= s "\xAC") 172 + (ite (= s "\xAD") 173 + (ite (= s "\xAE") 174 + (ite (= s "\xAF") 175 + (ite (= s "\xB0") 176 + (ite (= s "\xB1") 177 + (ite (= s "\xB2") 178 + (ite (= s "\xB3") 179 + (ite (= s "\xB4") 180 + (ite (= s "\xB5") 181 + (ite (= s "\xB6") 182 + (ite (= s "\xB7") 183 + (ite (= s "\xB8") 184 + (ite (= s "\xB9") 185 + (ite (= s "\xBA") 186 + (ite (= s "\xBB") 187 + (ite (= s "\xBC") 188 + (ite (= s "\xBD") 189 + (ite (= s "\xBE") 190 + (ite (= s "\xBF") 191 + (ite (= s "\xC0") 192 + (ite (= s "\xC1") 193 + (ite (= s "\xC2") 194 + (ite (= s "\xC3") 195 + (ite (= s "\xC4") 196 + (ite (= s "\xC5") 197 + (ite (= s "\xC6") 198 + (ite (= s "\xC7") 199 + (ite (= s "\xC8") 200 + (ite (= s "\xC9") 201 + (ite (= s "\xCA") 202 + (ite (= s "\xCB") 203 + (ite (= s "\xCC") 204 + (ite (= s "\xCD") 205 + (ite (= s "\xCE") 206 + (ite (= s "\xCF") 207 + (ite (= s "\xD0") 208 + (ite (= s "\xD1") 209 + (ite (= s "\xD2") 210 + (ite (= s "\xD3") 211 + (ite (= s "\xD4") 212 + (ite (= s "\xD5") 213 + (ite (= s "\xD6") 214 + (ite (= s "\xD7") 215 + (ite (= s "\xD8") 216 + (ite (= s "\xD9") 217 + (ite (= s "\xDA") 218 + (ite (= s "\xDB") 219 + (ite (= s "\xDC") 220 + (ite (= s "\xDD") 221 + (ite (= s "\xDE") 222 + (ite (= s "\xDF") 223 + (ite (= s "\xE0") 224 + (ite (= s "\xE1") 225 + (ite (= s "\xE2") 226 + (ite (= s "\xE3") 227 + (ite (= s "\xE4") 228 + (ite (= s "\xE5") 229 + (ite (= s "\xE6") 230 + (ite (= s "\xE7") 231 + (ite (= s "\xE8") 232 + (ite (= s "\xE9") 233 + (ite (= s "\xEA") 234 + (ite (= s "\xEB") 235 + (ite (= s "\xEC") 236 + (ite (= s "\xED") 237 + (ite (= s "\xEE") 238 + (ite (= s "\xEF") 239 + (ite (= s "\xF0") 240 + (ite (= s "\xF1") 241 + (ite (= s "\xF2") 242 + (ite (= s "\xF3") 243 + (ite (= s "\xF4") 244 + (ite (= s "\xF5") 245 + (ite (= s "\xF6") 246 + (ite (= s "\xF7") 247 + (ite (= s "\xF8") 248 + (ite (= s "\xF9") 249 + (ite (= s "\xFA") 250 + (ite (= s "\xFB") 251 + (ite (= s "\xFC") 252 + (ite (= s "\xFD") 253 + (ite (= s "\xFE") 254 + (ite (= s "\xFF") 255 + 256)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +) + + + +(define-fun read_buffer16 ((s1 String) (s2 String)) Int + (+ (* 256 (byte_2_int s1)) + (byte_2_int s2)) +) + + +(define-fun read_buffer32 ((s1 String) (s2 String) (s3 String) (s4 String)) Int + (+ (+ (+ (* 16777216 (byte_2_int s1) ) + (* 65536 (byte_2_int s2) ) ) + (* 256 (byte_2_int s3) ) ) + (byte_2_int s4) ) +) + + +(declare-const magic String) +(declare-const p1 String) +(declare-const p2 String) +(declare-const p3 String) +(declare-const size1 String) +(declare-const size2 String) +(declare-const size3 String) +(declare-const size4 String) +(declare-const off1 String) +(declare-const off2 String) +(declare-const off3 String) +(declare-const off4 String) +(assert (= magic "ABCD")) +(assert (= 1 (str.len size1))) +(assert (= 1 (str.len size2))) +(assert (= 1 (str.len size3))) +(assert (= 1 (str.len size4))) +(assert (= 1 (str.len off1))) +(assert (= 1 (str.len off2))) +(assert (= 1 (str.len off3))) +(assert (= 1 (str.len off4))) + + +(declare-const p3_off Int) +(declare-const before_p3 String) +(assert (= before_p3 (str.++ p1 p2))) +(assert (not (str.contains before_p3 magic))) +(assert (= p3_off (str.len before_p3))) + + +(declare-const p2_size Int) +(declare-const p2_off Int) +(declare-const p2_min_size Int) +(assert (= p2_size (read_buffer32 size1 size2 size3 size4))) +(assert (= p2_off (read_buffer32 off1 off2 off3 off4))) +(assert (<= (+ p2_size p2_off) p3_off)) +(assert (>= p2_size p2_min_size)) +(assert (= p2_min_size 10)) + +(check-sat) -- cgit v1.2.3